From 5dc9ab190a6f51e6b04bda2a7835e15d16c630c6 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 10 Feb 2012 17:37:37 +0000 Subject: [PATCH] Change to modelCheck() call in API: don't pass constants, just get from PropertiesFile. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4582 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 8 ++++---- prism/src/prism/PrismCL.java | 2 +- prism/src/prism/PrismTest.java | 6 +++--- prism/src/userinterface/properties/GUIExperiment.java | 2 +- .../src/userinterface/properties/GUIMultiProperties.java | 2 +- .../properties/computation/ModelCheckThread.java | 7 ++----- 6 files changed, 12 insertions(+), 15 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index c3ec154d..5be174ce 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2242,11 +2242,11 @@ public class Prism implements PrismSettingsListener * Perform model checking of a property on the currently loaded model and return result. * @param propertiesFile Parent property file of property (for labels/constants/...) * @param expr The property to check - * @param definedPFConstants Optional values info for properties file (to display in log) */ - public Result modelCheck(PropertiesFile propertiesFile, Expression expr, Values definedPFConstants) throws PrismException, PrismLangException + public Result modelCheck(PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { Result res = null; + Values definedPFConstants = propertiesFile.getConstantValues(); if (!digital) mainLog.printSeparator(); @@ -2349,7 +2349,7 @@ public class Prism implements PrismSettingsListener mainLog.printWarning("PRISM code export failed: " + e.getMessage()); } } - return modelCheck(propertiesFile, expr, definedPFConstants); + return modelCheck(propertiesFile, expr); } finally { digital = false; currentModulesFile = oldModulesFile; @@ -2972,7 +2972,7 @@ public class Prism implements PrismSettingsListener public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { loadBuiltModel(model); - return modelCheck(propertiesFile, expr, null); + return modelCheck(propertiesFile, expr); } /** diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index c7ff6fb1..070f6565 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -285,7 +285,7 @@ public class PrismCL } // Normal model checking if (!simulate) { - res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants); + res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j).getExpression()); } // Approximate (simulation-based) model checking else { diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index 7a583f5b..8652c9f3 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -65,12 +65,12 @@ public class PrismTest // Parse a prop, check on model 1 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0)); System.out.println(result.getResult()); // Parse another prop, check on model 1 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0)); System.out.println(result.getResult()); // Parse/load model 2 @@ -79,7 +79,7 @@ public class PrismTest // Parse a prop, check on model 2 propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]"); - result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0), null); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0)); System.out.println(result.getResult()); // Close down diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 5e44334f..595fb28b 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -325,7 +325,7 @@ public class GUIExperiment } // Normal model checking if (!useSimulation) { - res = prism.modelCheck(propertiesFile, propertyToCheck, definedPFConstants); + res = prism.modelCheck(propertiesFile, propertyToCheck); } // Approximate (simulation-based) model checking else { diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index c2271d07..b70c4427 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -272,7 +272,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List for (GUIProperty gp : propertiesToBeVerified) gp.setConstants(mfConstants, pfConstants); // Start model checking - Thread t = new ModelCheckThread(this, parsedProperties, propertiesToBeVerified, pfConstants); + Thread t = new ModelCheckThread(this, parsedProperties, propertiesToBeVerified); t.setPriority(Thread.NORM_PRIORITY); t.start(); } catch (PrismException e) { diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index bffe834c..5084eb26 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -48,19 +48,16 @@ public class ModelCheckThread extends GUIComputationThread // (Also need properties file for access to constants/labels/etc.) private PropertiesFile propertiesFile; private ArrayList guiProps; - // Values give to constants - private Values definedPFConstants; /** * Create a new instance of ModelCheckThread (where a Model has been built) */ - public ModelCheckThread(GUIMultiProperties parent, PropertiesFile propertiesFile, ArrayList guiProps, Values definedPFConstants) + public ModelCheckThread(GUIMultiProperties parent, PropertiesFile propertiesFile, ArrayList guiProps) { super(parent); this.parent = parent; this.propertiesFile = propertiesFile; this.guiProps = guiProps; - this.definedPFConstants = definedPFConstants; } public void run() @@ -101,7 +98,7 @@ public class ModelCheckThread extends GUIComputationThread // Do model checking try { - result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(i), definedPFConstants); + result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(i)); } catch (PrismException e) { result = new Result(e); error(e.getMessage());