s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Added option to do experiments for PTAs in GUI. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2193 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
4b3cf8c6b4
commit
dcfc7c59de
1 changed files with 148 additions and 144 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 292
      prism/src/userinterface/properties/GUIExperiment.java

292
prism/src/userinterface/properties/GUIExperiment.java
View File

@ -31,6 +31,7 @@ import parser.*;
import parser.ast.*;
import parser.type.*;
import prism.*;
import javax.swing.*;
import userinterface.*;
import java.util.*;
@ -48,23 +49,24 @@ public class GUIExperiment
private prism.ResultsCollection results;
private String modString;
private boolean finished = false;
private ModulesFile mod;
private UndefinedConstants cons;
private PropertiesFile prop; //contains 1 property only
private boolean running = false;
private Thread theThread;
private boolean useSimulation;
private Values definedMFConstants;
private Values definedPFConstants;
private Result res;
/** Creates a new instance of GUIExperiment */
public GUIExperiment(GUIExperimentTable table, GUIMultiProperties guiProp, PropertiesFile prop, UndefinedConstants cons, ModulesFile mod, String modString, boolean useSimulation)
public GUIExperiment(GUIExperimentTable table, GUIMultiProperties guiProp, PropertiesFile prop, UndefinedConstants cons, ModulesFile mod, String modString,
boolean useSimulation)
{
this.table = table;
this.guiProp = guiProp;
@ -73,76 +75,76 @@ public class GUIExperiment
this.mod = mod;
this.modString = modString;
this.useSimulation = useSimulation;
results = new prism.ResultsCollection(cons, prop.getProperty(0).getResultName());
}
//ACCESS METHODS
public int getTotalIterations()
{
return cons.getNumIterations();
}
public int getCurrentIterations()
{
return results.getCurrentIteration();
}
public Vector getRangingConstants()
{
return cons.getRangingConstants();
}
public String getDefinedConstantsString()
{
return cons.getDefinedConstantsString();
}
public String getPFDefinedConstantsString()
{
return cons.getPFDefinedConstantsString();
}
public String getPropertyString()
{
return prop.getProperty(0).toString();
}
public Type getPropertyType()
{
return prop.getProperty(0).getType();
}
public ResultsCollection getResults()
{
return results;
}
public boolean isFinished()
{
return finished;
}
public boolean isUseSimulation()
{
return useSimulation;
}
public GUIExperimentTable getTable()
{
return table;
}
//UPDATE METHODS
public void startExperiment()
{
theThread = new ExperimentThread(guiProp,this,cons,mod,prop);
theThread = new ExperimentThread(guiProp, this, cons, mod, prop);
running = true;
theThread.start();
}
}
public synchronized void experimentDone()
{
running = false;
@ -150,7 +152,7 @@ public class GUIExperiment
finished = true;
this.table.repaint();
}
// note: presently, this is never actually called
// (in case of errors, these are stored as the results of the experiment and things end normally)
public synchronized void experimentFailed()
@ -160,7 +162,7 @@ public class GUIExperiment
finished = true;
table.repaint();
}
public synchronized void experimentInterrupted()
{
running = false;
@ -168,39 +170,40 @@ public class GUIExperiment
finished = true;
table.repaint();
}
public synchronized void setResult(Values mfValues, Values pfValues, Result res) throws PrismException
{
results.setResult(mfValues, pfValues, res.getResult());
}
public synchronized void setMultipleErrors(Values mfValues, Values pfValues, Exception e) throws PrismException
{
results.setMultipleErrors(mfValues, pfValues, e);
}
public void stop()
{
if(running && theThread != null)
{
if(useSimulation) guiProp.getPrism().getSimulator().stopSampling();
if (running && theThread != null) {
if (useSimulation)
guiProp.getPrism().getSimulator().stopSampling();
theThread.interrupt();
}
}
//tidy up ResultsCollection when it has been removed (to tidy up graphs)
public void clear()
{
}
class ExperimentThread extends GUIComputationThread
{
private UndefinedConstants undefinedConstants;
private ModulesFile modulesFile;
private PropertiesFile propertiesFile;
private GUIExperiment exp;
public ExperimentThread(GUIMultiProperties guiProp, GUIExperiment exp, UndefinedConstants undefinedConstants, ModulesFile modulesFile, PropertiesFile propertiesFile)
public ExperimentThread(GUIMultiProperties guiProp, GUIExperiment exp, UndefinedConstants undefinedConstants, ModulesFile modulesFile,
PropertiesFile propertiesFile)
{
super(guiProp);
this.exp = exp;
@ -208,23 +211,22 @@ public class GUIExperiment
this.modulesFile = modulesFile;
this.propertiesFile = propertiesFile;
}
public void run()
{
int i, k;
boolean clear = true;
Model model = null;
Expression propertyToCheck = propertiesFile.getProperty(0);
SimulationInformation info = null;
boolean reuseInfo = false, reuseInfoAsked = false;
definedMFConstants = null;
definedPFConstants = null;
res = null;
try
{
try {
SwingUtilities.invokeAndWait(new Runnable()
{
public void run()
@ -235,185 +237,186 @@ public class GUIExperiment
guiProp.notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.EXPERIMENT_START));
}
});
for (i = 0; i < undefinedConstants.getNumModelIterations(); i++)
{
for (i = 0; i < undefinedConstants.getNumModelIterations(); i++) {
definedMFConstants = undefinedConstants.getMFConstantValues();
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("\nModel constants: " + definedMFConstants);
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
logln("\nModel constants: " + definedMFConstants);
// set values for ModulesFile constants
try {
modulesFile.setUndefinedConstants(definedMFConstants);
}
catch (PrismException e) {
} catch (PrismException e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
try {
setMultipleErrors(definedMFConstants, null, e);
}
catch (PrismException e2) {
} catch (PrismException e2) {
error("Problem storing results");
}
undefinedConstants.iterateModel();
continue;
}
// only do explicit model construction if necessary
if(!useSimulation)
{
if (!useSimulation && modulesFile.getModelType() != ModelType.PTA) {
// build model
try {
logln("\n-------------------------------------------");
model = prism.buildModel(modulesFile);
clear = false;
}
catch (PrismException e) {
} catch (PrismException e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
try {
setMultipleErrors(definedMFConstants, null, e);
}
catch (PrismException e2) {
} catch (PrismException e2) {
error("Problem storing results");
}
undefinedConstants.iterateModel();
continue;
}
// remove any deadlocks (don't prompt - probably should)
StateList states = model.getDeadlockStates();
if (states != null)
{
if (states.size() > 0)
{
if (states != null) {
if (states.size() > 0) {
guiProp.log("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n");
model.fixDeadlocks();
}
}
// print some model info
guiProp.log("\n");
model.printTransInfo(guiProp.getGUI().getLog());
}
// collect information for simulation if required
if(useSimulation && !reuseInfo)
{
if (useSimulation && !reuseInfo) {
try {
info = null;
info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), modulesFile.getInitialValues(), modulesFile, "("+definedMFConstants+")");
}
catch (PrismException e) {
info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), modulesFile.getInitialValues(), modulesFile, "("
+ definedMFConstants + ")");
} catch (PrismException e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
try {
setMultipleErrors(definedMFConstants, null, e);
}
catch (PrismException e2) {
} catch (PrismException e2) {
error("Problem storing results");
}
if (!clear) model.clear();
if (!clear)
model.clear();
undefinedConstants.iterateModel();
continue;
}
// if info is null, the user clicked cancel
if(info == null) break;
if (info == null)
break;
// if there are multiple models, offer the chance to reuse simulation info
if (undefinedConstants.getNumModelIterations() > 1 && !reuseInfoAsked) {
reuseInfoAsked = true;
int q = guiProp.questionYesNo("Do you want to reuse the same initial state and simulation\n" +
"parameters for the remaining models in this experiment?\n" +
"If not you will be prompted for new values for each one.");
if (q == 0) reuseInfo = true;
int q = guiProp.questionYesNo("Do you want to reuse the same initial state and simulation\n"
+ "parameters for the remaining models in this experiment?\n" + "If not you will be prompted for new values for each one.");
if (q == 0)
reuseInfo = true;
}
}
// for distributed simulation, pass control to the GUISimulatorDistributionDialog
if(useSimulation && info.isDistributed())
{
if (useSimulation && info.isDistributed()) {
try {
GUISimulatorDistributionDialog dist = new GUISimulatorDistributionDialog(guiProp.getGUI(), prism.getSimulator(), true);
dist.show(exp, this, modulesFile, propertiesFile, undefinedConstants, propertyToCheck, info);
//new GUISimulatorDistributionDialog(guiProp.getGUI(), prism.getSimulator(), true).show(modulesFile, undefinedConstants, propertyToCheck, info);
}
catch (PrismException e) {
} catch (PrismException e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
try {
setMultipleErrors(definedMFConstants, null, e);
}
catch (PrismException e2) {
} catch (PrismException e2) {
error("Problem storing results");
}
if (!clear) model.clear();
if (!clear)
model.clear();
undefinedConstants.iterateModel();
continue;
}
}
// for simulation where "simultaneous property checking" is enabled...
else if(useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1)
{
else if (useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS)
&& undefinedConstants.getNumPropertyIterations() > 1) {
try {
logln("\n-------------------------------------------");
logln("\nSimulating: " + propertyToCheck);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
logln("Model constants: " + definedMFConstants);
logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
log("Simulation parameters: approx = "+info.getApprox()+", conf = "+info.getConfidence()+", num samples = "+info.getNoIterations()+", max path len = "+info.getMaxPathLength()+")\n");
prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, info.getInitialState(), info.getNoIterations(), info.getMaxPathLength());
log("Simulation parameters: approx = " + info.getApprox() + ", conf = " + info.getConfidence() + ", num samples = "
+ info.getNoIterations() + ", max path len = " + info.getMaxPathLength() + ")\n");
prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, info
.getInitialState(), info.getNoIterations(), info.getMaxPathLength());
// update progress meter
// (all properties simulated simultaneously so can't get more accurate feedback at the moment anyway)
table.progressChanged();
}
catch (PrismException e) {
} catch (PrismException e) {
// in case of error, report it (in log only), store as result, and go on to the next model
errorLog(e.getMessage());
try {
setMultipleErrors(definedMFConstants, null, e);
}
catch (PrismException e2) {
} catch (PrismException e2) {
error("Problem storing results");
}
undefinedConstants.iterateModel();
continue;
}
}
else
{
} else {
// iterate through as many properties as necessary
for (k = 0; k < undefinedConstants.getNumPropertyIterations(); k++)
{
for (k = 0; k < undefinedConstants.getNumPropertyIterations(); k++) {
// interrupt if requested
if(interrupted()) throw new InterruptedException();
try
{
if (interrupted())
throw new InterruptedException();
try {
// set values for PropertiesFile constants
if (propertiesFile != null)
{
if (propertiesFile != null) {
definedPFConstants = undefinedConstants.getPFConstantValues();
propertiesFile.setUndefinedConstants(definedPFConstants);
}
// do model checking
logln("\n-------------------------------------------");
logln("\n"+(useSimulation?"Simulating":"Model checking")+": " + propertyToCheck);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);
if (useSimulation) log("Simulation parameters: approx = "+info.getApprox()+", conf = "+info.getConfidence()+", num samples = "+info.getNoIterations()+", max path len = "+info.getMaxPathLength()+")\n");
if (!useSimulation)
{
res = prism.modelCheck(model, propertiesFile, propertyToCheck);
}
else {
res = prism.modelCheckSimulator(modulesFile, propertiesFile, propertyToCheck, info.getInitialState(), info.getNoIterations(), info.getMaxPathLength());
logln("\n" + (useSimulation ? "Simulating" : "Model checking") + ": " + propertyToCheck);
if (definedMFConstants != null)
if (definedMFConstants.getNumValues() > 0)
logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null)
if (definedPFConstants.getNumValues() > 0)
logln("Property constants: " + definedPFConstants);
if (useSimulation)
log("Simulation parameters: approx = " + info.getApprox() + ", conf = " + info.getConfidence() + ", num samples = "
+ info.getNoIterations() + ", max path len = " + info.getMaxPathLength() + ")\n");
if (!useSimulation) {
// PTA model checking
if (modulesFile.getModelType() == ModelType.PTA) {
res = prism.modelCheckPTA(modulesFile, propertiesFile, propertyToCheck);
}
// Non-PTA model checking
else {
res = prism.modelCheck(model, propertiesFile, propertyToCheck);
}
} else {
res = prism.modelCheckSimulator(modulesFile, propertiesFile, propertyToCheck, info.getInitialState(), info
.getNoIterations(), info.getMaxPathLength());
}
}
catch(PrismException e)
{
} catch (PrismException e) {
// in case of error, report it (in log only), store exception as the result and proceed
errorLog(e.getMessage());
res = new Result(e);
@ -425,26 +428,26 @@ public class GUIExperiment
{
try {
GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res);
}
catch (PrismException e) {
} catch (PrismException e) {
error("Problem storing results");
}
}
});
table.progressChanged();
// iterate to next property
undefinedConstants.iterateProperty();
yield();
}
}
if (!clear) model.clear();
if (!clear)
model.clear();
// iterate to next model
undefinedConstants.iterateModel();
yield();
}
SwingUtilities.invokeAndWait(new Runnable()
{
public void run()
@ -456,34 +459,35 @@ public class GUIExperiment
}
});
experimentDone();
if (results.containsErrors()) errorDialog("One or more errors occured during this experiment.\nSelect \"View results\" or check the log for more information");
}
catch(InterruptedException e)
{
try
{
if (results.containsErrors())
errorDialog("One or more errors occured during this experiment.\nSelect \"View results\" or check the log for more information");
} catch (InterruptedException e) {
try {
SwingUtilities.invokeAndWait(new Runnable()
{
public void run()
{
guiProp.stopProgress();
guiProp.setTaskBarText("Running experiment... interrupted.");
guiProp.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, guiProp));
guiProp.notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.EXPERIMENT_END));
}
});
}
// catch and ignore possible exceptions from invokeAndWait call
catch (InterruptedException e2) {}
catch (java.lang.reflect.InvocationTargetException e2) {}
if (!clear) model.clear();
catch (InterruptedException e2) {
} catch (java.lang.reflect.InvocationTargetException e2) {
}
if (!clear)
model.clear();
experimentInterrupted();
}
// catch and ignore possible exception from invokeAndWait calls
catch (java.lang.reflect.InvocationTargetException e) {}
catch (java.lang.reflect.InvocationTargetException e) {
}
}
}
}
Write Preview
Loading…
Cancel
Save