From 15482e84580a41cc4b4d57ba0dd313ff27e7c03f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 25 Oct 2018 15:48:34 +0200 Subject: [PATCH] Sparse engine with -exportstrat: Fix crash during strategy initialization When converting an MTBDD to an integer vector (as is done to prepare the storage for the computed strategy for Pmax-Until using the sparse engine), the MTBDD has to be zero for non-reachable states, as that could lead to out-of-bounds writes to the array during conversion. This commit adds the required restriction to reach in prism.NondetModelChecker. + test case + fixes deref of 'yes' during initialization --- prism-tests/bugfixes/stratgenreach.nm | 11 +++++++++++ prism-tests/bugfixes/stratgenreach.nm.props | 2 ++ prism-tests/bugfixes/stratgenreach.nm.props.args | 1 + prism-tests/bugfixes/stratgenreach.nm.props.strat | 1 + prism/src/prism/NondetModelChecker.java | 5 ++++- 5 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 prism-tests/bugfixes/stratgenreach.nm create mode 100644 prism-tests/bugfixes/stratgenreach.nm.props create mode 100644 prism-tests/bugfixes/stratgenreach.nm.props.args create mode 100644 prism-tests/bugfixes/stratgenreach.nm.props.strat 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); }