diff --git a/prism-tests/functionality/verify/exact/exact-eval-2.prism b/prism-tests/functionality/verify/exact/exact-eval-2.prism new file mode 100644 index 00000000..046972e4 --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-2.prism.props b/prism-tests/functionality/verify/exact/exact-eval-2.prism.props new file mode 100644 index 00000000..2ae9248a --- /dev/null +++ b/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 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-2.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-2.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-2.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-3.prism b/prism-tests/functionality/verify/exact/exact-eval-3.prism new file mode 100644 index 00000000..fb37139f --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-3.prism.props b/prism-tests/functionality/verify/exact/exact-eval-3.prism.props new file mode 100644 index 00000000..2ae9248a --- /dev/null +++ b/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 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-3.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-3.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-3.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-4.prism b/prism-tests/functionality/verify/exact/exact-eval-4.prism new file mode 100644 index 00000000..17dfab73 --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-4.prism.props b/prism-tests/functionality/verify/exact/exact-eval-4.prism.props new file mode 100644 index 00000000..2ae9248a --- /dev/null +++ b/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 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-4.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-4.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-4.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-5.prism b/prism-tests/functionality/verify/exact/exact-eval-5.prism new file mode 100644 index 00000000..72520e9b --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-5.prism.props b/prism-tests/functionality/verify/exact/exact-eval-5.prism.props new file mode 100644 index 00000000..f49657bc --- /dev/null +++ b/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 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-5.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-5.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-5.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-6.prism b/prism-tests/functionality/verify/exact/exact-eval-6.prism new file mode 100644 index 00000000..1b21afe1 --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-6.prism.props b/prism-tests/functionality/verify/exact/exact-eval-6.prism.props new file mode 100644 index 00000000..2ded4d16 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-6.prism.props @@ -0,0 +1,3 @@ +// RESULT: 2 +Rmax=?[ F s>0 ] + diff --git a/prism-tests/functionality/verify/exact/exact-eval-6.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-6.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-6.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-7.prism b/prism-tests/functionality/verify/exact/exact-eval-7.prism new file mode 100644 index 00000000..df903dcc --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-7.prism.props b/prism-tests/functionality/verify/exact/exact-eval-7.prism.props new file mode 100644 index 00000000..2ae9248a --- /dev/null +++ b/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 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-7.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-7.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-7.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-8.prism b/prism-tests/functionality/verify/exact/exact-eval-8.prism new file mode 100644 index 00000000..f7f06d57 --- /dev/null +++ b/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 diff --git a/prism-tests/functionality/verify/exact/exact-eval-8.prism.props b/prism-tests/functionality/verify/exact/exact-eval-8.prism.props new file mode 100644 index 00000000..063f88ad --- /dev/null +++ b/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) diff --git a/prism-tests/functionality/verify/exact/exact-eval-8.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-8.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-8.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism/src/param/ChoiceListFlexi.java b/prism/src/param/ChoiceListFlexi.java index 2b85307a..aaec89ae 100644 --- a/prism/src/param/ChoiceListFlexi.java +++ b/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) diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 0ae24c4d..44acbac5 100644 --- a/prism/src/param/ModelBuilder.java +++ b/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 { diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 1b4a843a..f0791acf 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/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; diff --git a/prism/src/param/ParamResult.java b/prism/src/param/ParamResult.java index 10dcbb9f..b90de345 100644 --- a/prism/src/param/ParamResult.java +++ b/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 + ")"); diff --git a/prism/src/param/SymbolicEngine.java b/prism/src/param/SymbolicEngine.java index 8b16008c..6c15fb11 100644 --- a/prism/src/param/SymbolicEngine.java +++ b/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); diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java index 69c9907e..47c1ed94 100644 --- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java +++ b/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. + *
+ * Used by the parametric / exact engine to build models. + *
+ * 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 initStates = new ArrayList(); // 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 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;