Improve handling of constants in parametric model checking - avoid conversion of fractional constants such as 1/3 to doubles and the resulting loss of precision.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9346 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/param/ModelBuilder.java

@@ -28,18 +28,21 @@ package param;
 
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Map;
 
 import parser.State;
+import parser.ast.ConstantList;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionConstant;
 import parser.ast.ExpressionLiteral;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.ModulesFile;
+import parser.visitor.ASTTraverseModify;
 import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
-import prism.PrismLog;
+import prism.PrismLangException;
 import prism.PrismSettings;
 import explicit.IndexedSet;
 import explicit.StateStorage;
@@ -69,6 +72,9 @@ public final class ModelBuilder extends PrismComponent
 	/** maximal error probability of DAG function representation */
 	private double dagMaxError;
 
+	/** local storage made static for use in anonymous class */
+	private static Map<String,Expression> constExprs;
+	
 	/**
 	 * Constructor
 	 */
@@ -206,7 +212,21 @@ public final class ModelBuilder extends PrismComponent
 
 		// build model
 		time = System.currentTimeMillis();
-		modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(modulesFile.getConstantValues()).simplify();
+		// First, set values for any constants in the model
+		// (but do this *symbolically* - partly because some constants are parameters and therefore unknown,
+		// but also to keep values like 1/3 as expressions rather than being converted to doubles,
+		// resulting in a loss of precision)
+		ConstantList constantList = modulesFile.getConstantList();
+		constExprs = constantList.evaluateConstantsPartially(modulesFile.getUndefinedConstantValues(), null);
+		modulesFile = (ModulesFile) modulesFile.deepCopy();
+		modulesFile = (ModulesFile) modulesFile.accept(new ASTTraverseModify()
+		{
+			public Object visit(ExpressionConstant e) throws PrismLangException
+			{
+				Expression expr = constExprs.get(e.getName());
+				return (expr != null) ? expr.deepCopy() : e;
+			}
+		});
 		ParamModel modelExpl = constructModel(modulesFile);
 		time = System.currentTimeMillis() - time;
 

prism/src/parser/ast/ConstantList.java

@@ -26,6 +26,8 @@
 
 package parser.ast;
 
+import java.util.HashMap;
+import java.util.Map;
 import java.util.Vector;
 
 import parser.*;
@@ -288,6 +290,71 @@ public class ConstantList extends ASTElement
 		return allValues;
 	}
 
+	/**
+	 * Set values for some undefined constants, then partially evaluate values for constants where possible
+	 * and return a map from constant names to the Expression representing its value. 
+	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined.
+	 * Argument 'otherValues' contains any other values which may be needed, null if none.
+	 */
+	public Map<String,Expression> evaluateConstantsPartially(Values someValues, Values otherValues) throws PrismLangException
+	{
+		ConstantList cl;
+		Expression e;
+		int i, j, n, numToEvaluate;
+		Type t = null;
+		ExpressionIdent s;
+		
+		// Create new copy of this ConstantList
+		// (copy existing constant definitions, add new ones where undefined)
+		cl = new ConstantList();
+		n = constants.size();
+		for (i = 0; i < n; i++) {
+			s = getConstantNameIdent(i);
+			e = getConstant(i);
+			t = getConstantType(i);
+			if (e != null) {
+				cl.addConstant((ExpressionIdent)s.deepCopy(), e.deepCopy(), t);
+			} else {
+				// Create new literal expression using values passed in (if possible and needed)
+				if (someValues != null && (j = someValues.getIndexOf(s.getName())) != -1) {
+					cl.addConstant((ExpressionIdent) s.deepCopy(), new ExpressionLiteral(t, t.castValueTo(someValues.getValue(j))), t);
+				}
+			}
+		}
+		numToEvaluate = cl.size();
+		
+		// Now add constants corresponding to the 'otherValues' argument to the new constant list
+		if (otherValues != null) {
+			n = otherValues.getNumValues();
+			for (i = 0; i < n; i++) {
+				Type iType = otherValues.getType(i);
+				cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(iType, iType.castValueTo(otherValues.getValue(i))), iType);
+			}
+		}
+		
+		// Go trough and expand definition of each constant
+		// (i.e. replace other constant references with their definitions)
+		// Note: work with new copy of constant list, don't need to expand 'otherValues' ones.
+		for (i = 0; i < numToEvaluate; i++) {
+			try {
+				e = (Expression)cl.getConstant(i).expandConstants(cl);
+				cl.setConstant(i, e);
+			} catch (PrismLangException ex) {
+				cl.setConstant(i, null);
+			}
+		}
+		
+		// Store final expressions for each constant in a map and return
+		Map<String,Expression> constExprs = new HashMap<>();
+		for (i = 0; i < numToEvaluate; i++) {
+			if (cl.getConstant(i) != null) {
+				constExprs.put(cl.getConstantName(i), cl.getConstant(i).deepCopy());
+			}
+		}
+		
+		return constExprs;
+	}
+
 	// Methods required for ASTElement:
 	
 	/**

prism/src/parser/ast/ModulesFile.java

@@ -66,7 +66,9 @@ public class ModulesFile extends ASTElement
 	private Vector<String> varNames;
 	private Vector<Type> varTypes;
 
-	// actual values of (some or all) constants
+	// Values set for undefined constants (null if none)
+	private Values undefinedConstantValues;
+	// Actual values of (some or all) constants
 	private Values constantValues;
 
 	// Constructor
@@ -89,6 +91,7 @@ public class ModulesFile extends ASTElement
 		varDecls = new Vector<Declaration>();
 		varNames = new Vector<String>();
 		varTypes = new Vector<Type>();
+		undefinedConstantValues = null;
 		constantValues = null;
 	}
 
@@ -937,6 +940,7 @@ public class ModulesFile extends ASTElement
 	 */
 	public void setUndefinedConstants(Values someValues) throws PrismLangException
 	{
+		undefinedConstantValues = someValues == null ? null : new Values(someValues);
 		constantValues = constantList.evaluateConstants(someValues, null);
 		semanticCheckAfterConstants(this, null);
 	}
@@ -949,6 +953,7 @@ public class ModulesFile extends ASTElement
 	 */
 	public void setSomeUndefinedConstants(Values someValues) throws PrismLangException
 	{
+		undefinedConstantValues = someValues == null ? null : new Values(someValues);
 		constantValues = constantList.evaluateSomeConstants(someValues, null);
 		semanticCheckAfterConstants(this, null);
 	}
@@ -962,6 +967,15 @@ public class ModulesFile extends ASTElement
 		return constantList.isDefinedConstant(name);
 	}
 	
+	/**
+	 * Get access to the values that have been provided for undefined constants in the model 
+	 * (e.g. via the method {@link #setUndefinedConstants(Values)}).
+	 */
+	public Values getUndefinedConstantValues()
+	{
+		return undefinedConstantValues;
+	}
+
 	/**
 	 * Get access to the values for all constants in the model, including the 
 	 * undefined constants set previously via the method {@link #setUndefinedConstants(Values)}.