From a97d6d9841f05f7e4d11b03f1db6e7ae0b3abc5a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 29 Oct 2010 10:28:38 +0000 Subject: [PATCH] Digitsl clocks enabled for model checking in GUI. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2198 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../properties/GUIExperiment.java | 46 +++++++++--- .../computation/ModelCheckThread.java | 71 ++++++++++++++----- 2 files changed, 90 insertions(+), 27 deletions(-) diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 5f46ed86..dfd318d4 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 pta.DigitalClocks; import javax.swing.*; import userinterface.*; @@ -218,6 +219,7 @@ public class GUIExperiment boolean clear = true; Model model = null; + ModulesFile modulesFileToCheck; Expression propertyToCheck = propertiesFile.getProperty(0); SimulationInformation info = null; boolean reuseInfo = false, reuseInfoAsked = false; @@ -390,7 +392,7 @@ public class GUIExperiment propertiesFile.setUndefinedConstants(definedPFConstants); } - // do model checking + // log output logln("\n-------------------------------------------"); logln("\n" + (useSimulation ? "Simulating" : "Model checking") + ": " + propertyToCheck); if (definedMFConstants != null) @@ -399,21 +401,49 @@ public class GUIExperiment 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"); + // for PTAs via digital clocks, do model translation and build + if (modulesFile.getModelType() == ModelType.PTA + && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { + DigitalClocks dc = new DigitalClocks(prism); + dc.translate(modulesFile, propertiesFile, propertyToCheck); + modulesFileToCheck = dc.getNewModulesFile(); + modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); + // build model + logln("\n-------------------------------------------"); + model = prism.buildModel(modulesFileToCheck); + clear = false; + // remove any deadlocks (don't prompt - probably should) + StateList states = model.getDeadlockStates(); + 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()); + } else { + modulesFileToCheck = modulesFile; + } + + // exact (non-approximate) model checking if (!useSimulation) { // PTA model checking - if (modulesFile.getModelType() == ModelType.PTA) { - res = prism.modelCheckPTA(modulesFile, propertiesFile, propertyToCheck); + if (modulesFileToCheck.getModelType() == ModelType.PTA) { + res = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertyToCheck); } // Non-PTA model checking else { res = prism.modelCheck(model, propertiesFile, propertyToCheck); } - } else { - res = prism.modelCheckSimulator(modulesFile, propertiesFile, propertyToCheck, info.getInitialState(), info + } + // approximate (simulation-based) model checking + else { + log("Simulation parameters: approx = " + info.getApprox() + ", conf = " + info.getConfidence() + ", num samples = " + + info.getNoIterations() + ", max path len = " + info.getMaxPathLength() + ")\n"); + res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertyToCheck, info.getInitialState(), info .getNoIterations(), info.getMaxPathLength()); } } catch (PrismException e) { diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 86887c43..d6891392 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -33,6 +33,7 @@ import javax.swing.*; import parser.*; import parser.ast.*; import prism.*; +import pta.DigitalClocks; import userinterface.*; import userinterface.util.*; import userinterface.properties.*; @@ -46,12 +47,12 @@ public class ModelCheckThread extends GUIComputationThread 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 ModulesFile mf; + // Currently exactly one-of model/modulesFile is non-null + private Model model; + private ModulesFile modulesFile; // Properties file and GUI properties (these are assumed to match) // (Also need properties file for access to constants/labels/etc.) - private PropertiesFile pf; + private PropertiesFile propertiesFile; private ArrayList guiProps; // Values give to constants private Values definedMFConstants; @@ -60,14 +61,14 @@ public class ModelCheckThread extends GUIComputationThread /** * Create a new instance of ModelCheckThread (where a Model has been built) */ - public ModelCheckThread(GUIMultiProperties parent, Model m, PropertiesFile pf, ArrayList guiProps, Values definedMFConstants, + public ModelCheckThread(GUIMultiProperties parent, Model model, PropertiesFile propertiesFile, ArrayList guiProps, Values definedMFConstants, Values definedPFConstants) { super(parent); this.parent = parent; - this.m = m; - this.mf = null; - this.pf = pf; + this.model = model; + this.modulesFile = null; + this.propertiesFile = propertiesFile; this.guiProps = guiProps; this.definedMFConstants = definedMFConstants; this.definedPFConstants = definedPFConstants; @@ -76,16 +77,19 @@ public class ModelCheckThread extends GUIComputationThread /** * 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, + public ModelCheckThread(GUIMultiProperties parent, ModulesFile modulesFile, PropertiesFile propertiesFile, ArrayList guiProps, Values definedMFConstants, Values definedPFConstants) { - this(parent, (Model) null, pf, guiProps, definedMFConstants, definedPFConstants); - this.mf = mf; + this(parent, (Model) null, propertiesFile, guiProps, definedMFConstants, definedPFConstants); + this.modulesFile = modulesFile; } public void run() { - if (m == null && mf == null) + ModulesFile modulesFileToCheck; + boolean clear = true; + + if (model == null && modulesFile == null) return; // Notify user interface of the start of computation @@ -111,7 +115,7 @@ public class ModelCheckThread extends GUIComputationThread IconThread ic = new IconThread(null); // Work through list of properties - for (int i = 0; i < pf.getNumProperties(); i++) { + for (int i = 0; i < propertiesFile.getNumProperties(); i++) { // Get ith property GUIProperty gp = guiProps.get(i); @@ -123,24 +127,53 @@ public class ModelCheckThread extends GUIComputationThread try { // Print info to log logln("\n-------------------------------------------"); - logln("\nModel checking: " + pf.getProperty(i)); + logln("\nModel checking: " + propertiesFile.getProperty(i)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); + // for PTAs via digital clocks, do model translation and build + if (modulesFile.getModelType() == ModelType.PTA + && prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) { + DigitalClocks dc = new DigitalClocks(prism); + dc.translate(modulesFile, propertiesFile, propertiesFile.getProperty(i)); + modulesFileToCheck = dc.getNewModulesFile(); + modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); + // build model + logln("\n-------------------------------------------"); + model = prism.buildModel(modulesFileToCheck); + clear = false; + // remove any deadlocks (don't prompt - probably should) + StateList states = model.getDeadlockStates(); + if (states != null) { + if (states.size() > 0) { + log("\nWarning: " + states.size() + " deadlock states detected; adding self-loops in these states...\n"); + model.fixDeadlocks(); + } + } + // print some model info + log("\n"); + model.printTransInfo(parent.getGUI().getLog()); + } else { + modulesFileToCheck = modulesFile; + } // No model (PTA) case - if (m == null) { - if (mf.getModelType() != ModelType.PTA) + if (model == null) { + if (modulesFile.getModelType() != ModelType.PTA) throw new PrismException("No model to verify"); - result = prism.modelCheckPTA(mf, pf, pf.getProperty(i)); + result = prism.modelCheckPTA(modulesFileToCheck, propertiesFile, propertiesFile.getProperty(i)); } // Normal model checking else { - result = prism.modelCheck(m, pf, pf.getProperty(i)); + result = prism.modelCheck(model, propertiesFile, propertiesFile.getProperty(i)); + } + // Clear model, if required + if (!clear) { + model.clear(); + clear = true; } - } catch (PrismException e) { result = new Result(e); error(e.getMessage());