Digital clocks: manage translation of properties/file properly (+ test cases).

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

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 ];
+

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

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 ];

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

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());

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;

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);
 		}