param / exact: Evaluate expressions exactly in various places (+tests)

Expressions are now evaluated exactly in parametric / exact model checking mode for:
 - state updates
 - command guards
 - the if part of if-then-else expressions
 - reward guards
 - reward values
 - Boolean expressions in RESULTS in property files

Add various test cases to check that it is now handled properly.

prism-tests/functionality/verify/exact/exact-eval-2.prism

@@ -0,0 +1,13 @@
+// test case, check if int constants are evaluated exactly in exact / parametric mode
+
+dtmc
+
+const int n = (1/3 = 0.333333333333333333333333 ? 1 : 2);
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/2:(s'=n) + 1/2:(s'=2);
+  [] s>=1 -> true;
+endmodule

prism-tests/functionality/verify/exact/exact-eval-2.prism.props

@@ -0,0 +1,5 @@
+// RESULT: 0
+P=?[ F s=1 ]
+
+// RESULT: false
+P>0[ F s=1 ]

prism-tests/functionality/verify/exact/exact-eval-2.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-3.prism

@@ -0,0 +1,12 @@
+// test case, check if int expressions are evaluated exactly in exact / parametric mode
+
+dtmc
+
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/2:(s'=(1/3 = 0.333333333333333333333333 ? 1 : 2)) + 1/2:(s'=2);
+  [] s>=1 -> true;
+endmodule

prism-tests/functionality/verify/exact/exact-eval-3.prism.props

@@ -0,0 +1,5 @@
+// RESULT: 0
+P=?[ F s=1 ]
+
+// RESULT: false
+P>0[ F s=1 ]

prism-tests/functionality/verify/exact/exact-eval-3.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-4.prism

@@ -0,0 +1,12 @@
+// test case, check if int expressions involving state variables are evaluated exactly in exact / parametric mode
+
+dtmc
+
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/2:(s'=((s+1)*1/3 = 0.333333333333333333333333 ? 1 : 2)) + 1/2:(s'=2);
+  [] s>=1 -> true;
+endmodule

prism-tests/functionality/verify/exact/exact-eval-4.prism.props

@@ -0,0 +1,5 @@
+// RESULT: 0
+P=?[ F s=1 ]
+
+// RESULT: false
+P>0[ F s=1 ]

prism-tests/functionality/verify/exact/exact-eval-4.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-5.prism

@@ -0,0 +1,12 @@
+// test case, check if initial expressions are evaluated exactly in exact / parametric mode
+
+dtmc
+
+const double x;  // dummy for parametric
+
+module M1
+  s1: [0..2] init (1/3 = 0.333333333333333333333333 ? 1 : 2);
+  s2: bool init (1/3 = 0.333333333333333333333333 ? true : false);
+
+  [] true -> true;
+endmodule

prism-tests/functionality/verify/exact/exact-eval-5.prism.props

@@ -0,0 +1,11 @@
+// RESULT: 0
+P=?[ F s1=1 ]
+
+// RESULT: false
+P>0[ F s1=1 ]
+
+// RESULT: 0
+P=?[ F s2 ]
+
+// RESULT: false
+P>0[ F s2 ]

prism-tests/functionality/verify/exact/exact-eval-5.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-6.prism

@@ -0,0 +1,16 @@
+// test case, check if reward expressions are evaluated exactly in exact / parametric mode
+
+mdp
+
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..2] init 0;
+
+  [a] s=0 -> 1/2:(s'=1) + 1/2:(s'=2);
+  [] s>=1 -> true;
+endmodule
+
+rewards "r"
+  [a] true : (1/3 = 0.333333333333333333333333 ? 1 : 2);
+endrewards

prism-tests/functionality/verify/exact/exact-eval-6.prism.props

@@ -0,0 +1,3 @@
+// RESULT: 2
+Rmax=?[ F s>0 ]
+

prism-tests/functionality/verify/exact/exact-eval-6.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-7.prism

@@ -0,0 +1,17 @@
+// test case, check if expressions in guards are evaluated exactly in exact / parametric mode
+
+dtmc
+
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..3] init 0;
+
+  // if the if part in the following guard expression is evaluated using
+  // default floating point arithmetic then, ultimately, from state s=0 there are
+  // two transitions, with prob 1/2 to either s=1 or s=2
+  [] s=(1/3 = 0.333333333333333333333333 ? 0 : 3) -> 1:(s'=1);
+  [] s=0 -> 1:(s'=2);
+
+  [] s>=1 -> true;
+endmodule

prism-tests/functionality/verify/exact/exact-eval-7.prism.props

@@ -0,0 +1,5 @@
+// RESULT: 0
+P=?[ F s=1 ]
+
+// RESULT: false
+P>0[ F s=1 ]

prism-tests/functionality/verify/exact/exact-eval-7.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism-tests/functionality/verify/exact/exact-eval-8.prism

@@ -0,0 +1,16 @@
+// test case, check if guards in reward expressions are evaluated exactly in exact / parametric mode
+
+mdp
+
+const double x;  // dummy for parametric
+
+module M1
+  s: [0..2] init 0;
+
+  [a] s=0 -> 1/2:(s'=1) + 1/2:(s'=2);
+  [] s>=1 -> true;
+endmodule
+
+rewards "r"
+  [a] s=(1/3 = 0.333333333333333333333333 ? 1 : 0) : 2;
+endrewards

prism-tests/functionality/verify/exact/exact-eval-8.prism.props

@@ -0,0 +1,6 @@
+// RESULT: 2
+Rmax=?[ F s>0 ]
+
+// test case to check that arithmetic in the property is done exactly
+// RESULT: false
+(1/3 = 0.3333333333333333333333333333)

prism-tests/functionality/verify/exact/exact-eval-8.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

prism/src/param/ChoiceListFlexi.java

@@ -187,7 +187,8 @@ public class ChoiceListFlexi //implements Choice
 					first = false;
 				else
 					s += ", ";
-				s += up.getVar(j) + "'=" + up.getExpression(j).evaluate(currentState);
+				BigRational newValue = up.getExpression(j).evaluateExact(currentState);
+				s += up.getVar(j) + "'=" + up.getExpression(j).getType().castFromBigRational(newValue);
 			}
 		}
 		return s;
@@ -213,14 +214,16 @@ public class ChoiceListFlexi //implements Choice
 	{
 		State newState = new State(currentState);
 		for (Update up : updates.get(i))
-			up.update(currentState, newState);
+			// evaluate and apply update expression (in exact evaluation mode)
+			up.update(currentState, newState, true);
 		return newState;
 	}
 
 	public void computeTarget(int i, State currentState, State newState) throws PrismLangException
 	{
 		for (Update up : updates.get(i))
-			up.update(currentState, newState);
+			// evaluate and apply update expression (in exact evaluation mode)
+			up.update(currentState, newState, true);
 	}
 
 	public Function getProbability(int i)

prism/src/param/ModelBuilder.java

@@ -157,7 +157,7 @@ public final class ModelBuilder extends PrismComponent
 					// non-parametric constants and state variable values have
 					// been already partially expanded, so if this evaluation
 					// succeeds there are no parametric constants involved
-					boolean ifValue = iteExpr.getOperand1().evaluateBoolean();
+					boolean ifValue = iteExpr.getOperand1().evaluateExact().toBoolean();
 					if (ifValue) {
 						return expr2function(factory, iteExpr.getOperand2());
 					} else {

prism/src/param/ParamModelChecker.java

@@ -1124,7 +1124,7 @@ final public class ParamModelChecker extends PrismComponent
 			String action = rewStruct.getSynch(rewItem);
 			boolean isTransitionReward = rewStruct.getRewardStructItem(rewItem).isTransitionReward();
 			for (int state = 0; state < numStates; state++) {
-				if (guard.evaluateBoolean(constantValues, statesList.get(state))) {
+				if (guard.evaluateExact(constantValues, statesList.get(state)).toBoolean()) {
 					int[] varMap = new int[statesList.get(0).varValues.length];
 					for (int i = 0; i < varMap.length; i++) {
 						varMap[i] = i;

prism/src/param/ParamResult.java

@@ -172,7 +172,7 @@ public class ParamResult
 		if (propertyType.equals(TypeBool.getInstance())) {
 			// boolean result
 			boolean boolResult = regionValues.getResult(0).getInitStateValueAsBoolean();
-			boolean boolExpected = expected.evaluateBoolean();
+			boolean boolExpected = expected.evaluateExact().toBoolean();
 
 			if (boolResult != boolExpected) {
 				throw new PrismException("Wrong result (expected " + strExpected + ", got " + boolResult + ")");

prism/src/param/SymbolicEngine.java

@@ -258,7 +258,7 @@ public class SymbolicEngine
 		n = module.getNumCommands();
 		for (i = 0; i < n; i++) {
 			command = module.getCommand(i);
-			if (command.getGuard().evaluateBoolean(state)) {
+			if (command.getGuard().evaluateExact(state).toBoolean()) {
 				j = command.getSynchIndex();
 				updateLists.get(m).get(j).add(command.getUpdates());
 				enabledSynchs.set(j);

prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

@@ -22,6 +22,15 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
 
+/**
+ * A variant of ModulesFileGenerator that is suitable for model generation
+ * at a symbolic level, i.e., where numeric values are kept as expressions
+ * instead of being evaluated.
+ * <br>
+ * Used by the parametric / exact engine to build models.
+ * <br>
+ * Uses exact arithmetic to evaluate the various expressions in a model description.
+ */
 public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 {
 	// Parent PrismComponent (logs, settings etc.)
@@ -246,7 +255,8 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 	public State getInitialState() throws PrismException
 	{
 		if (modulesFile.getInitialStates() == null) {
-			return modulesFile.getDefaultInitialState();
+			// get initial state, using exact evaluation
+			return modulesFile.getDefaultInitialState(true);
 		} else {
 			// Inefficient but probably won't be called
 			return getInitialStates().get(0);
@@ -259,7 +269,8 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		List<State> initStates = new ArrayList<State>();
 		// Easy (normal) case: just one initial state
 		if (modulesFile.getInitialStates() == null) {
-			State state = modulesFile.getDefaultInitialState();
+			// get initial state, using exact evaluation
+			State state = modulesFile.getDefaultInitialState(true);
 			initStates.add(state);
 		}
 		// Otherwise, there may be multiple initial states
@@ -268,7 +279,7 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 			Expression init = modulesFile.getInitialStates();
 			List<State> allPossStates = varList.getAllStates();
 			for (State possState : allPossStates) {
-				if (init.evaluateBoolean(modulesFile.getConstantValues(), possState)) {
+				if (init.evaluateExact(modulesFile.getConstantValues(), possState).toBoolean()) {
 					initStates.add(possState);
 				}
 			}
@@ -369,7 +380,7 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 	public boolean isLabelTrue(int i) throws PrismException
 	{
 		Expression expr = labelList.getLabel(i);
-		return expr.evaluateBoolean(exploreState);
+		return expr.evaluateExact(exploreState).toBoolean();
 	}
 	
 	@Override
@@ -381,8 +392,8 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		for (int i = 0; i < n; i++) {
 			if (!rewStr.getRewardStructItem(i).isTransitionReward()) {
 				Expression guard = rewStr.getStates(i);
-				if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) {
-					double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state);
+				if (guard.evaluateExact(modulesFile.getConstantValues(), state).toBoolean()) {
+					double rew = rewStr.getReward(i).evaluateExact(modulesFile.getConstantValues(), state).doubleValue();
 					if (Double.isNaN(rew))
 						throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i));
 					d += rew;
@@ -403,8 +414,8 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 				Expression guard = rewStr.getStates(i);
 				String cmdAction = rewStr.getSynch(i);
 				if (action == null ? (cmdAction.isEmpty()) : action.equals(cmdAction)) {
-					if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) {
-						double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state);
+					if (guard.evaluateExact(modulesFile.getConstantValues(), state).toBoolean()) {
+						double rew = rewStr.getReward(i).evaluateExact(modulesFile.getConstantValues(), state).doubleValue();
 						if (Double.isNaN(rew))
 							throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i));
 						d += rew;