diff --git a/prism-tests/functionality/verify/ptas/reach/propconst.nm b/prism-tests/functionality/verify/ptas/reach/propconst.nm new file mode 100644 index 00000000..d178684e --- /dev/null +++ b/prism-tests/functionality/verify/ptas/reach/propconst.nm @@ -0,0 +1,10 @@ +pta + +module M + + s : [0..1]; + x : clock; + + [a] x>=4 -> (s'=1); + +endmodule diff --git a/prism-tests/functionality/verify/ptas/reach/propconst.nm.props b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props new file mode 100644 index 00000000..19444271 --- /dev/null +++ b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props @@ -0,0 +1,17 @@ +const int K = 2; +const int L; + +// This tests clocks appearing in the property +// (the use of digital clocks with -ex means that the expression +// is evaluated and all the types have to be correct) +// RESULT: 1.0 +Pmax=? [ F x>=2 ]; + +// This tests (defined) constants from the prop file +// RESULT: 1.0 +Pmax=? [ F x>=K ]; + +// This tests (undefined) constants from the prop file +// RESULT: 1.0 +Pmax=? [ F x>=L ]; + diff --git a/prism-tests/functionality/verify/ptas/reach/propconst.nm.props.args b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props.args new file mode 100644 index 00000000..cafb5e45 --- /dev/null +++ b/prism-tests/functionality/verify/ptas/reach/propconst.nm.props.args @@ -0,0 +1,2 @@ +-ptamethod digital -const L=2 +-ptamethod digital -const L=2 -ex diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props index 0051b4b6..666cc3e7 100644 --- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props +++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props @@ -1,3 +1,14 @@ +const int K=2; +const int L; + // Maximum probability of configuring IP address incorrectly // RESULT: 130321/100130321 "incorrect": Pmax=? [ F s=2 & ip=2 ]; + +// As above but testing using constants +// RESULT: 130321/100130321 +Pmax=? [ F s=2 & ip=K ]; + +// As above but testing using (undefined) constants +// RESULT: 130321/100130321 +Pmax=? [ F s=2 & ip=L ]; diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args index cda609a6..80318d38 100644 --- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args +++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args @@ -1,4 +1,4 @@ --ptamethod digital -e 1e-8 --ptamethod digital -e 1e-8 -ex --ptamethod games --ptamethod backwards +-const L=2 -ptamethod digital -e 1e-8 +-const L=2 -ptamethod digital -e 1e-8 -ex +-const L=2 -ptamethod games +-const L=2 -ptamethod backwards diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index bac31faa..f110870f 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -348,6 +348,7 @@ public class PropertiesFile extends ASTElement // get label list from model file mfLabels = modulesFile.getLabelList(); // add model file labels to combined label list (cloning them just for good measure) + combinedLabelList = new LabelList(); n = mfLabels.size(); for (i = 0; i < n; i++) { combinedLabelList.addLabel(mfLabels.getLabelNameIdent(i), mfLabels.getLabel(i).deepCopy()); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a79ba8b0..bada7c16 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3040,8 +3040,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener DigitalClocks dc = new DigitalClocks(this); dc.translate(oldModulesFile, propertiesFile, expr); loadPRISMModel(dc.getNewModulesFile()); - // evaluate constants (use exact evaluation if we are in exact computation mode) - currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues(), settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED)); // If required, export generated PRISM model if (exportDigital) { try { @@ -3054,7 +3052,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener mainLog.printWarning("PRISM code export failed: " + e.getMessage()); } } - return modelCheck(propertiesFile, expr); + return modelCheck(dc.getNewPropertiesFile(), dc.getNewPropertyToCheck()); } finally { digital = false; currentModulesFile = oldModulesFile; diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 0ccbd58a..291098da 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -44,10 +44,6 @@ public class DigitalClocks private Prism prism; // Log private PrismLog mainLog; - // Model to be converted - private ModulesFile modulesFile; - // Properties to be converted - private PropertiesFile propertiesFile; // Constants from model private Values constantValues; // Variable list for model @@ -67,6 +63,8 @@ public class DigitalClocks private ModulesFile mf; // Translated properties file private PropertiesFile pf; + // Translated property to check + private Expression prop; /** * Constructor. @@ -77,6 +75,7 @@ public class DigitalClocks mainLog = prism.getMainLog(); mf = null; pf = null; + prop = null; } /** @@ -95,6 +94,14 @@ public class DigitalClocks return pf; } + /** + * Get translated property to check. + */ + public Expression getNewPropertyToCheck() + { + return prop; + } + /** * Main method - translate. */ @@ -106,11 +113,11 @@ public class DigitalClocks mainLog.println("\nPerforming digital clocks translation..."); - // Store model/properties files - this.modulesFile = modulesFile; - this.propertiesFile = propertiesFile; + // Store some info for global access constantValues = modulesFile.getConstantValues(); - // TODO: need property constants too? + if (propertiesFile != null ) { + constantValues = new Values(constantValues, propertiesFile.getConstantValues()); + } varList = modulesFile.createVarList(); // Check that model does not contain any closed clock constraints @@ -140,7 +147,7 @@ public class DigitalClocks } // Check that the property is suitable for checking with digital clocks if (propertyToCheck != null) { - checkProperty(propertyToCheck); + checkProperty(propertyToCheck, propertiesFile); } // Choose a new action label to represent time @@ -160,6 +167,7 @@ public class DigitalClocks // Take a copy of the whole model/properties file before translation mf = (ModulesFile) modulesFile.deepCopy(); pf = (propertiesFile == null) ? null : (PropertiesFile) propertiesFile.deepCopy(); + prop = (Expression) propertyToCheck.deepCopy(); // Change the model type mf.setModelType(ModelType.MDP); @@ -289,6 +297,7 @@ public class DigitalClocks if (pf != null) { pf = (PropertiesFile) pf.accept(asttm); } + prop = (Expression) prop.accept(asttm); // Change state rewards in reward structures to use time action) // (transition rewards can be left unchanged) @@ -315,15 +324,21 @@ public class DigitalClocks if (pf != null) { pf.tidyUp(); } + // Copy across undefined constants since these get lost in the call to tidyUp() + mf.setSomeUndefinedConstants(modulesFile.getUndefinedConstantValues()); + pf.setSomeUndefinedConstants(propertiesFile.getUndefinedConstantValues()); } /** * Check that a property is checkable with the digital clocks method. * Throw an explanatory exception if not. + * Optionally, an enclosing PropertiesFile is provided, to look up + * property/label references. Can be null. */ - public void checkProperty(Expression propertyToCheck) throws PrismLangException + public void checkProperty(Expression propertyToCheck, PropertiesFile propertiesFile) throws PrismLangException { ASTElement ast; + LabelList labelList = (propertiesFile == null) ? null : propertiesFile.getLabelList(); // LTL not handled (look in any P operators) try { @@ -362,13 +377,13 @@ public class DigitalClocks } // Check for presence of strict clock constraints - ast = findAStrictClockConstraint(propertyToCheck, propertiesFile.getLabelList()); + ast = findAStrictClockConstraint(propertyToCheck, labelList); if (ast != null) { throw new PrismLangException("Strict clock constraints are not allowed when using the digital clocks method", ast); } // Check for presence of diagonal clock constraints // (for now; should be able to relax this later) - ast = findADiagonalClockConstraint(propertyToCheck, propertiesFile.getLabelList()); + ast = findADiagonalClockConstraint(propertyToCheck, labelList); if (ast != null) { throw new PrismLangException("Diagonal clock constraints are not allowed when using the digital clocks method", ast); }