From e57f270042ab8fcdbada8561f187ccb20702e36d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 8 Dec 2020 09:27:09 +0000 Subject: [PATCH] Bug fix in (recent) explicit engine simple->sparse conversion of actions. And a test case. --- prism-tests/bugfixes/mdp-action-storage-bug.prism | 11 +++++++++++ .../bugfixes/mdp-action-storage-bug.prism.props | 2 ++ .../bugfixes/mdp-action-storage-bug.prism.props.args | 2 ++ prism/src/explicit/ChoiceActionsSimple.java | 4 +++- prism/src/explicit/MDPSparse.java | 8 ++++++-- 5 files changed, 24 insertions(+), 3 deletions(-) create mode 100644 prism-tests/bugfixes/mdp-action-storage-bug.prism create mode 100644 prism-tests/bugfixes/mdp-action-storage-bug.prism.props create mode 100644 prism-tests/bugfixes/mdp-action-storage-bug.prism.props.args diff --git a/prism-tests/bugfixes/mdp-action-storage-bug.prism b/prism-tests/bugfixes/mdp-action-storage-bug.prism new file mode 100644 index 00000000..3a5dc365 --- /dev/null +++ b/prism-tests/bugfixes/mdp-action-storage-bug.prism @@ -0,0 +1,11 @@ +mdp + +module M + + s:[0..3]; + + [a] s=0 -> (s'=2); + [b] s=2 -> (s'=1); + +endmodule + diff --git a/prism-tests/bugfixes/mdp-action-storage-bug.prism.props b/prism-tests/bugfixes/mdp-action-storage-bug.prism.props new file mode 100644 index 00000000..fb62ce9f --- /dev/null +++ b/prism-tests/bugfixes/mdp-action-storage-bug.prism.props @@ -0,0 +1,2 @@ +// RESULT: true +P>=1 [ F s=1 ]; diff --git a/prism-tests/bugfixes/mdp-action-storage-bug.prism.props.args b/prism-tests/bugfixes/mdp-action-storage-bug.prism.props.args new file mode 100644 index 00000000..a92958b9 --- /dev/null +++ b/prism-tests/bugfixes/mdp-action-storage-bug.prism.props.args @@ -0,0 +1,2 @@ +-ex +-m diff --git a/prism/src/explicit/ChoiceActionsSimple.java b/prism/src/explicit/ChoiceActionsSimple.java index 0df91356..d4b6ef42 100644 --- a/prism/src/explicit/ChoiceActionsSimple.java +++ b/prism/src/explicit/ChoiceActionsSimple.java @@ -166,6 +166,8 @@ public class ChoiceActionsSimple * Convert to "sparse" storage for a given model, * i.e., a single array where all actions are stored in * order, per state and then per choice. + * A corresponding NondetModel is required because the + * number of states and choices per state may be unknown. * If this action storage is completely empty, * then this method may simply return null. */ @@ -180,7 +182,7 @@ public class ChoiceActionsSimple for (int s = 0; s < numStates; s++) { int numChoices = model.getNumChoices(s); for (int i = 0; i < numChoices; i++) { - arr[count++] = model.getAction(s, i); + arr[count++] = getAction(s, i); } } return arr; diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index f7df0539..81d3a0dc 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -231,7 +231,9 @@ public class MDPSparse extends MDPExplicit } choiceStarts[numDistrs] = numTransitions; rowStarts[numStates] = numDistrs; - actions = mdp.actions.convertToSparseStorage(mdp); + // Copy the actions too + // Note: could pass 'mdp' or 'this' to convertToSparseStorage (use latter for consistency) + actions = mdp.actions.convertToSparseStorage(this); } /** @@ -295,7 +297,9 @@ public class MDPSparse extends MDPExplicit } choiceStarts[numDistrs] = numTransitions; rowStarts[numStates] = numDistrs; - actions = mdp.actions.convertToSparseStorage(mdp); + // Copy the actions too (after permuting) + // Note: we pass _this_ new, permuted model to convertToSparseStorage + actions = new ChoiceActionsSimple(mdp.actions, permut).convertToSparseStorage(this); } /**