From e9545cac7ce0354133f07271d19365490f587741 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 28 Oct 2010 21:29:28 +0000 Subject: [PATCH] Added option to verify PTAs in GUI (no experiments yet). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2191 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 18 ++- .../properties/GUIMultiProperties.java | 99 +++++++------- .../computation/ModelCheckThread.java | 124 +++++++++++------- 3 files changed, 139 insertions(+), 102 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 248a0a76..635ffd0e 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -266,17 +266,17 @@ public class PrismCL tmpLog.print(mfTmp.toString()); } - // decide if model construction is necessary + // Decide if model construction is necessary boolean doBuild = true; - // if explicitly disabled... + // If explicitly disabled... if (nobuild) doBuild = false; - // no need if using approximate (simulation-based) model checking... + // No need if using approximate (simulation-based) model checking... if (simulate) doBuild = false; - // no need for PTA model checking (when not using digital clocks)... - else if (modulesFile.getModelType() == ModelType.PTA - && !prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) + // No need if doing PTA model checking... + // (NB: PTA digital clocks excluded - has already been reduced to an MDP) + if (modulesFile.getModelType() == ModelType.PTA) doBuild = false; // do model construction (if necessary) @@ -396,12 +396,10 @@ public class PrismCL // exact (non-appoximate) model checking if (!simulate) { // PTA model checking - if (modulesFile.getModelType() == ModelType.PTA - && !prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals( - "Digital clocks")) { + if (modulesFile.getModelType() == ModelType.PTA) { res = prism.modelCheckPTA(modulesFile, propertiesFile, propertiesToCheck[j]); } - // non-PTA model checking + // Non-PTA model checking else { res = prism.modelCheck(model, propertiesFile, propertiesToCheck[j]); } diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 866362e0..889ef74c 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -61,14 +61,15 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List public static final int WARN_INVALID_PROPS = 1; public static final int NEVER_INVALID_PROPS = 2; - //ATTRIBUTES + // ATTRIBUTES - // current model (gets updated only by event listening to GUIModel) + // Current model (gets updated only by event listening to GUIModel) private ModulesFile parsedModel; private Model builtModel; - private Values lastBuildValues; + // Constants for model (updated by events or locally) + private Values mfConstants; - //state + // State private boolean modified; private boolean modifiedSinceBuild; private boolean computing; @@ -77,10 +78,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List private PropertiesFile parsedProperties; private ArrayList propertiesToBeVerified; private File activeFile; - private Values lastPFConstants; - private Values lastSimulateValues; + private Values pfConstants; - //gui + // GUI private GUIPrismFileFilter propsFilter[]; private GUIPrismFileFilter textFilter[]; private JMenu propMenu; @@ -90,11 +90,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List private JScrollPane expScroller; private JLabel fileLabel; private Vector clipboardVector; - private Action newProps, openProps, saveProps, savePropsAs, insertProps, verifySelected, newProperty, editProperty, newConstant, removeConstant, newLabel, removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults, exportResults, simulate, details; - //current properties + // Current properties private GUIPropertiesList propList; private GUIPropConstantList consTable; private GUIPropLabelList labTable; @@ -103,7 +102,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List private Font displayFontFast; private Color backgroundFast, warningFast; - //CONSTRUCTORS + // CONSTRUCTORS /** Creates a new instance of GUIMultiProperties */ public GUIMultiProperties(GUIPrism pr, GUISimulator simulator) @@ -184,14 +183,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List protected void verifyAfterBuild() { verifyAfterReceiveBuildNotification = false; - - // Re-enable GUI elements - propList.setEnabled(true); - consTable.setEnabled(true); - labTable.setEnabled(true); + // Start model check process if (builtModel != null && parsedProperties != null && propertiesToBeVerified != null) { - Thread t = new ModelCheckThread(this, builtModel, parsedProperties, propertiesToBeVerified, lastBuildValues, lastPFConstants); + Thread t = new ModelCheckThread(this, builtModel, parsedProperties, propertiesToBeVerified, mfConstants, pfConstants); t.setPriority(Thread.NORM_PRIORITY); t.start(); } @@ -200,46 +195,54 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List protected void verifyAfterParse() { ArrayList validGUIProperties; - Values buildValues; UndefinedConstants uCon; - + verifyAfterReceiveParseNotification = false; - - // Get valid/selected properties + try { + // Get valid/selected properties String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedString(); // Get PropertiesFile for valid/selected properties parsedProperties = getPrism().parsePropertiesString(parsedModel, propertiesString); // And get list of corresponding GUIProperty objects validGUIProperties = propList.getValidSelectedProperties(); - } catch (PrismException e) { - error(e.getMessage()); - return; - } - // Query user for undefined constant values (if required) - try { + // Query user for undefined constant values (if required) uCon = new UndefinedConstants(parsedModel, parsedProperties); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { - int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, lastBuildValues, lastPFConstants); + // Use previous constant values as defaults in dialog + int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants); if (result != GUIConstantsPicker.VALUES_DONE) return; } - buildValues = uCon.getMFConstantValues(); - lastPFConstants = uCon.getPFConstantValues(); - parsedProperties.setUndefinedConstants(lastPFConstants); + // Store model constants (even though will be stored again after build) + // Don't set in model: this will be done during build process + mfConstants = uCon.getMFConstantValues(); + // Store property constants and set in file + pfConstants = uCon.getPFConstantValues(); + parsedProperties.setUndefinedConstants(pfConstants); + + // Store properties to be verified + propertiesToBeVerified = validGUIProperties; + // If required, trigger build then verify + if (parsedModel.getModelType() != ModelType.PTA) { + verifyAfterReceiveBuildNotification = true; + notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.REQUEST_MODEL_BUILD, mfConstants)); + } + // If no build required (e.g. for PTAs), just do model checking now + else { + // Start model check process + parsedModel.setUndefinedConstants(mfConstants); + if (parsedProperties != null && propertiesToBeVerified != null) { + Thread t = new ModelCheckThread(this, parsedModel, parsedProperties, propertiesToBeVerified, mfConstants, pfConstants); + t.setPriority(Thread.NORM_PRIORITY); + t.start(); + } + } } catch (PrismException e) { error(e.getMessage()); return; } - - // Disable GUI elements in Properties tab - propList.setEnabled(false); - consTable.setEnabled(false); - // Trigger build then verify - verifyAfterReceiveBuildNotification = true; - propertiesToBeVerified = validGUIProperties; - notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.REQUEST_MODEL_BUILD, buildValues)); } public void simulateAfterParse() @@ -285,15 +288,16 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List try { uCon = new UndefinedConstants(parsedModel, parsedProperties); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { - int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, lastSimulateValues, lastPFConstants); + // Use previous constant values as defaults in dialog + int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants); if (result != GUIConstantsPicker.VALUES_DONE) return; } - - lastSimulateValues = uCon.getMFConstantValues(); - lastPFConstants = uCon.getPFConstantValues(); - parsedModel.setUndefinedConstants(lastSimulateValues); - parsedProperties.setUndefinedConstants(lastPFConstants); + // Store model/property constants and set in files + mfConstants = uCon.getMFConstantValues(); + pfConstants = uCon.getPFConstantValues(); + parsedModel.setUndefinedConstants(mfConstants); + parsedProperties.setUndefinedConstants(pfConstants); SimulationInformation info = GUISimulationPicker.defineSimulationWithDialog(this.getGUI(), parsedModel.getInitialValues(), parsedModel); if (info == null) @@ -308,7 +312,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List new GUISimulatorDistributionDialog(getGUI(), getPrism().getSimulator(), true).show(this, parsedModel, parsedProperties, validGUIProperties, info); } else { - Thread t = new SimulateModelCheckThread(this, parsedModel, parsedProperties, validGUIProperties, lastSimulateValues, lastPFConstants, + Thread t = new SimulateModelCheckThread(this, parsedModel, parsedProperties, validGUIProperties, mfConstants, pfConstants, initialState, noIterations, maxPathLength, info); t.setPriority(Thread.NORM_PRIORITY); t.start(); @@ -541,8 +545,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List newProperty.setEnabled(!computing); editProperty.setEnabled(!computing && propList.getSelectedProperties().size() > 0); // constants list + consTable.setEnabled(!computing); removeConstant.setEnabled(consTable.getSelectedRowCount() > 0); // label list + labTable.setEnabled(!computing); removeLabel.setEnabled(labTable.getSelectedRowCount() > 0); // newExperiment: enabled if there is exactly one prop selected and it is valid @@ -1032,7 +1038,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List } else if (me.getID() == GUIModelEvent.MODEL_BUILT) { setBuiltModel(me.getModel()); if (me.getBuildValues() != null) - lastBuildValues = me.getBuildValues(); + mfConstants = me.getBuildValues(); modifiedSinceBuild = false; if (verifyAfterReceiveBuildNotification) verifyAfterBuild(); @@ -1820,7 +1826,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List stopExperiment.putValue(Action.LONG_DESCRIPTION, "Stops the Experiment that is currently running"); stopExperiment.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStop.png")); stopExperiment.setEnabled(false); - } /** diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index c509293e..86887c43 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -38,35 +38,57 @@ import userinterface.util.*; import userinterface.properties.*; /** - * - * @author ug60axh + * Thread that executes model checking of a property via PRISM. */ public class ModelCheckThread extends GUIComputationThread { + // Access to GUI (to send notifications etc.) private GUIMultiProperties parent; + // Model (in most cases, have a Model object; in others, e.g. PTA model checking, + // we just have the language-level model description, i.e. a ModulesFile). + // Currently exactly one-of m/mf is non-null private Model m; - private PropertiesFile prFi; + private ModulesFile mf; + // Properties file and GUI properties (these are assumed to match) + // (Also need properties file for access to constants/labels/etc.) + private PropertiesFile pf; private ArrayList guiProps; + // Values give to constants private Values definedMFConstants; private Values definedPFConstants; - - /** Creates a new instance of ModelCheckThread */ - public ModelCheckThread(GUIMultiProperties parent, Model m, PropertiesFile prFi, ArrayList guiProps, Values definedMFConstants, Values definedPFConstants) + + /** + * Create a new instance of ModelCheckThread (where a Model has been built) + */ + public ModelCheckThread(GUIMultiProperties parent, Model m, PropertiesFile pf, ArrayList guiProps, Values definedMFConstants, + Values definedPFConstants) { super(parent); this.parent = parent; this.m = m; - this.prFi = prFi; + this.mf = null; + this.pf = pf; this.guiProps = guiProps; this.definedMFConstants = definedMFConstants; this.definedPFConstants = definedPFConstants; } - + + /** + * Create a new instance of ModelCheckThread (where no Model has been built, e.g. PTAs) + */ + public ModelCheckThread(GUIMultiProperties parent, ModulesFile mf, PropertiesFile pf, ArrayList guiProps, Values definedMFConstants, + Values definedPFConstants) + { + this(parent, (Model) null, pf, guiProps, definedMFConstants, definedPFConstants); + this.mf = mf; + } + public void run() { - if(m == null) return; - - //Notify user interface of the start of computation + if (m == null && mf == null) + return; + + // Notify user interface of the start of computation SwingUtilities.invokeLater(new Runnable() { public void run() @@ -76,54 +98,67 @@ public class ModelCheckThread extends GUIComputationThread parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, parent)); } }); - + Result result = null; - - //Set icon for all properties to be verified to a clock - for(int i = 0; i < guiProps.size(); i++) - { + + // Set icon for all properties to be verified to a clock + for (int i = 0; i < guiProps.size(); i++) { GUIProperty gp = guiProps.get(i); gp.setStatus(GUIProperty.STATUS_DOING); parent.repaintList(); } - + IconThread ic = new IconThread(null); - - for(int i = 0; i < prFi.getNumProperties(); i++) - { - // get property + + // Work through list of properties + for (int i = 0; i < pf.getNumProperties(); i++) { + + // Get ith property GUIProperty gp = guiProps.get(i); - // animate it's clock icon + // Animate it's clock icon ic = new IconThread(gp); ic.start(); - // do model checking - try - { + + // Do model checking + try { + // Print info to log logln("\n-------------------------------------------"); - logln("\nModel checking: " + prFi.getProperty(i)); - if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); - if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); - result = prism.modelCheck(m, prFi, prFi.getProperty(i)); - } - catch(PrismException e) - { + logln("\nModel checking: " + pf.getProperty(i)); + if (definedMFConstants != null) + if (definedMFConstants.getNumValues() > 0) + logln("Model constants: " + definedMFConstants); + if (definedPFConstants != null) + if (definedPFConstants.getNumValues() > 0) + logln("Property constants: " + definedPFConstants); + // No model (PTA) case + if (m == null) { + if (mf.getModelType() != ModelType.PTA) + throw new PrismException("No model to verify"); + result = prism.modelCheckPTA(mf, pf, pf.getProperty(i)); + } + // Normal model checking + else { + result = prism.modelCheck(m, pf, pf.getProperty(i)); + } + + } catch (PrismException e) { result = new Result(e); error(e.getMessage()); } ic.interrupt(); - try - { + try { ic.join(); + } catch (InterruptedException e) { } - catch(InterruptedException e) - {} //while(!ic.canContinue){} gp.setResult(result); gp.setMethodString("Verification"); gp.setConstants(definedMFConstants, definedPFConstants); - + parent.repaintList(); } + + // Notify user interface of the end of computation SwingUtilities.invokeLater(new Runnable() { public void run() @@ -136,11 +171,13 @@ public class ModelCheckThread extends GUIComputationThread }); } + // Clock animation icon class IconThread extends Thread { GUIProperty gp; ImageIcon[] images; boolean canContinue = false; + public IconThread(GUIProperty gp) { this.gp = gp; @@ -154,22 +191,19 @@ public class ModelCheckThread extends GUIComputationThread images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png"); images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png"); } + public void run() { - try - { + try { int counter = 0; - while(!interrupted() && gp != null) - { + while (!interrupted() && gp != null) { counter++; - counter = counter%8; + counter = counter % 8; gp.setDoingImage(images[counter]); parent.repaintList(); sleep(150); } - } - catch(InterruptedException e) - { + } catch (InterruptedException e) { } canContinue = true; }