diff --git a/prism-tests/bugfixes/stratgenreach.nm b/prism-tests/bugfixes/stratgenreach.nm new file mode 100644 index 00000000..8bc5bdc9 --- /dev/null +++ b/prism-tests/bugfixes/stratgenreach.nm @@ -0,0 +1,11 @@ +// bugfix: -exportstrat for MDP using -sparse, missing restriction +// to reachable state space when initializing strategy storage vector + +mdp + +module m + s: [0..2] init 0; + + [a] s=0 -> 1/2:(s'=0) + 1/2:(s'=1); + [b] s=0 -> 1/3:(s'=2) + 2/3:(s'=1); +endmodule diff --git a/prism-tests/bugfixes/stratgenreach.nm.props b/prism-tests/bugfixes/stratgenreach.nm.props new file mode 100644 index 00000000..76ba065f --- /dev/null +++ b/prism-tests/bugfixes/stratgenreach.nm.props @@ -0,0 +1,2 @@ +// RESULT: 1.0 +Pmax=?[ F s=1 ] diff --git a/prism-tests/bugfixes/stratgenreach.nm.props.args b/prism-tests/bugfixes/stratgenreach.nm.props.args new file mode 100644 index 00000000..d2fce89e --- /dev/null +++ b/prism-tests/bugfixes/stratgenreach.nm.props.args @@ -0,0 +1 @@ +-sparse -exportstrat stratgenreach.nm.props.strat diff --git a/prism-tests/bugfixes/stratgenreach.nm.props.strat b/prism-tests/bugfixes/stratgenreach.nm.props.strat new file mode 100644 index 00000000..2d786a38 --- /dev/null +++ b/prism-tests/bugfixes/stratgenreach.nm.props.strat @@ -0,0 +1 @@ +0:a diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index c1a6b446..6bc674cb 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -2048,7 +2048,10 @@ public class NondetModelChecker extends NonProbModelChecker case Prism.SPARSE: IntegerVector strat = null; if (genStrat) { - JDDNode ddStrat = JDD.ITE(yes, JDD.Constant(-2), JDD.Constant(-1)); + // prepare strategy storage for the sparse engine computation + JDDNode ddStrat = JDD.ITE(yes.copy(), JDD.Constant(-2), JDD.Constant(-1)); + // restrict to the reachable state space of the model (required for conversion to integer array) + ddStrat = JDD.Times(ddStrat, reach.copy()); strat = new IntegerVector(ddStrat, allDDRowVars, odd); JDD.Deref(ddStrat); }