diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index ba72ed6f..5f46ed86 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -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) { + } } } }