From 9d5906ff3c24be7a2eb4c69d08971679eda105b5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 12 Jul 2026 11:13:49 +0100 Subject: [PATCH] -exportstrat can export full induced model, including states/labels/rewards. For example: prism ... -exportstrat strat.pexp prism ... -exportstrat strat.umb The -exportstrat switch also gains many of -exportmodel's options: format, states, rewards, labels, actions, precision, zip, text, headers. To avoid an option clash, "obs" now means "show observations", like for -exportmodel, and the existing "obs" option for -exportstrat is now renamed to "mergeobs" (merge observationally equivalent states). We also make reach=true the default. Implementation details: * StrategyExportOptions gains an inducedModelExportOptions field. * Tidy up constructInducedModel and exportInducedModel in Strategy classes for explicit models to respect inducedModelExportOptions and to use new Model.export method, allow full model export to .pexp/.umb. * Induced model construction in both ConstructInducedModel and ConstructStrategyProduct copies/lifts (by default, but optionally) any labels and rewards attached to the original model. * Rewards are pre-emptively built and attached to built models when it is known that strategies are generated (via StateModelChecker.attachRewards) --- .../export/strat/exportstratinduced.nm | 28 ++++ .../export/strat/exportstratinduced.nm.props | 2 + .../strat/exportstratinduced.nm.props.args | 4 + .../exportstratinduced.nm.props.multi.lab | 7 + .../exportstratinduced.nm.props.multi.sta | 8 ++ .../exportstratinduced.nm.props.multi.tra | 10 ++ .../exportstratinduced.nm.props.reach.lab | 6 + .../exportstratinduced.nm.props.reach.sta | 7 + .../exportstratinduced.nm.props.reach.tra | 9 ++ .../exportstratinduced.nm.props.reduce.pexp | 24 ++++ .../exportstratinduced.nm.props.restrict.pexp | 24 ++++ .../strat/exportstratinduced.nm.props.tra | 9 ++ prism/src/explicit/ConstructInducedModel.java | 132 ++++++++++++++++- .../explicit/ConstructStrategyProduct.java | 135 +++++++++++++++++- prism/src/explicit/StateModelChecker.java | 26 +++- prism/src/prism/Prism.java | 37 ++++- prism/src/prism/PrismCL.java | 53 ++++++- prism/src/strat/FMDObsStrategyBeliefs.java | 15 +- prism/src/strat/FMDStrategyProduct.java | 3 +- prism/src/strat/FMDStrategyStep.java | 7 - prism/src/strat/MDStrategyArray.java | 7 - prism/src/strat/MRStrategy.java | 7 - prism/src/strat/Strategy.java | 2 +- prism/src/strat/StrategyExplicit.java | 12 ++ prism/src/strat/StrategyExportOptions.java | 30 +++- 25 files changed, 547 insertions(+), 57 deletions(-) create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.args create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp create mode 100644 prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm b/prism-tests/functionality/export/strat/exportstratinduced.nm new file mode 100644 index 0000000000..3a5e5c73d1 --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm @@ -0,0 +1,28 @@ +// Test for extended -exportstrat induced-model export: separate files (.tra/.sta/.lab), +// combined formats (.pexp), mode=restrict/reduce and reach=true/false, all mirroring +// -exportmodel's file/format/label handling. State 3 is reachable in the full model but +// not under the optimal (Pmax) strategy for reaching "goal1", so it exercises reach=true +// dropping/reindexing of unreachable states (and their labels). + +mdp + +module M + +s:[0..5]; + +[east] s=0 -> 0.6:(s'=1) + 0.4:(s'=0); +[south] s=0 -> 0.8:(s'=3) + 0.1:(s'=1) + 0.1:(s'=4); +[east] s=1 -> 1:(s'=2); +[south] s=1 -> 0.5:(s'=4) + 0.5:(s'=2); +[stuck] s=2 -> 1:(s'=2); +[stuck] s=3 -> 1:(s'=3); +[east] s=4 -> 1:(s'=5); +[west] s=4 -> 0.6:(s'=3) + 0.4:(s'=4); +[north] s=5 -> 0.9:(s'=2) + 0.1:(s'=5); +[west] s=5 -> 1:(s'=4); + +endmodule + +label "hazard" = s=1; +label "goal1" = s=5; +label "goal2" = s=2|s=3; diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props b/prism-tests/functionality/export/strat/exportstratinduced.nm.props new file mode 100644 index 0000000000..b8ba41df0d --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props @@ -0,0 +1,2 @@ +// RESULT: 0.5 +Pmax=? [ F "goal1" ]; diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.args b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.args new file mode 100644 index 0000000000..dc5e092fef --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.args @@ -0,0 +1,4 @@ +-ex -exportstrat exportstratinduced.nm.props.tra +-ex -exportstrat exportstratinduced.nm.props.reduce.pexp:type=induced,mode=reduce +-ex -exportstrat exportstratinduced.nm.props.restrict.pexp:type=induced,mode=restrict +-ex -exportstrat exportstratinduced.nm.props.reach.tra:type=induced,reach=true diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab new file mode 100644 index 0000000000..b2780c4c61 --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab @@ -0,0 +1,7 @@ +# Labels +0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2" +0: 0 +1: 2 +2: 4 +3: 4 +5: 3 diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta new file mode 100644 index 0000000000..a2ff71209b --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta @@ -0,0 +1,8 @@ +# States +(s) +0:(0) +1:(1) +2:(2) +3:(3) +4:(4) +5:(5) diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra new file mode 100644 index 0000000000..74665c739b --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra @@ -0,0 +1,10 @@ +# Transitions (DTMC) +6 8 +0 0 0.4 east +0 1 0.6 east +1 2 0.5 south +1 4 0.5 south +2 2 1 stuck +3 3 1 stuck +4 5 1 east +5 4 1 west diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab new file mode 100644 index 0000000000..2e7408c0b0 --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab @@ -0,0 +1,6 @@ +# Labels +0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2" +0: 0 +1: 2 +2: 4 +4: 3 diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta new file mode 100644 index 0000000000..69f663bee2 --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta @@ -0,0 +1,7 @@ +# States +(s) +0:(0) +1:(1) +2:(2) +3:(4) +4:(5) diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra new file mode 100644 index 0000000000..a613b0e4be --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra @@ -0,0 +1,9 @@ +# Transitions (DTMC) +5 7 +0 0 0.4 east +0 1 0.6 east +1 2 0.5 south +1 3 0.5 south +2 2 1 stuck +3 4 1 east +4 3 1 west diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp new file mode 100644 index 0000000000..8ed732b23e --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp @@ -0,0 +1,24 @@ +# Transitions (DTMC) +5 7 +0 0 0.4 east +0 1 0.6 east +1 2 0.5 south +1 3 0.5 south +2 2 1 stuck +3 4 1 east +4 3 1 west + +# States +(s) +0:(0) +1:(1) +2:(2) +3:(4) +4:(5) + +# Labels +0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2" +0: 0 +1: 2 +2: 4 +4: 3 diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp new file mode 100644 index 0000000000..2062851db6 --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp @@ -0,0 +1,24 @@ +# Transitions (MDP) +5 5 7 +0 0 0 0.4 east +0 0 1 0.6 east +1 0 2 0.5 south +1 0 3 0.5 south +2 0 2 1 stuck +3 0 4 1 east +4 0 3 1 west + +# States +(s) +0:(0) +1:(1) +2:(2) +3:(4) +4:(5) + +# Labels +0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2" +0: 0 +1: 2 +2: 4 +4: 3 diff --git a/prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra new file mode 100644 index 0000000000..a613b0e4be --- /dev/null +++ b/prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra @@ -0,0 +1,9 @@ +# Transitions (DTMC) +5 7 +0 0 0.4 east +0 1 0.6 east +1 2 0.5 south +1 3 0.5 south +2 2 1 stuck +3 4 1 east +4 3 1 west diff --git a/prism/src/explicit/ConstructInducedModel.java b/prism/src/explicit/ConstructInducedModel.java index 10cbdde2b7..0733213916 100644 --- a/prism/src/explicit/ConstructInducedModel.java +++ b/prism/src/explicit/ConstructInducedModel.java @@ -27,7 +27,10 @@ package explicit; import common.Interval; +import explicit.rewards.Rewards; +import explicit.rewards.RewardsSimple; import parser.State; +import prism.Evaluator; import prism.ModelType; import prism.PrismException; import prism.PrismNotSupportedException; @@ -35,12 +38,7 @@ import strat.StrategyExportOptions.InducedModelMode; import strat.StrategyInfo; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.BitSet; -import java.util.Iterator; -import java.util.List; -import java.util.Map; +import java.util.*; /** * Construct the model induced by a memoryless deterministic strategy on a nondeterministic model @@ -59,6 +57,16 @@ public class ConstructInducedModel */ private boolean reachOnly = true; + /** + * Whether to copy labels from the original model to the induced model + */ + private boolean copyLabels = true; + + /** + * Whether to copy rewards from the original model to the induced model + */ + private boolean copyRewards = true; + /** * Set the "mode" of construction: * "restrict" (same model type but restrict to selected action choices); or @@ -79,6 +87,26 @@ public ConstructInducedModel setReachOnly(boolean reachOnly) return this; } + /** + * Set whether to copy labels from the original model to the induced model, + * restricted/reindexed to the induced model's states. + */ + public ConstructInducedModel setCopyLabels(boolean copyLabels) + { + this.copyLabels = copyLabels; + return this; + } + + /** + * Set whether to copy rewards from the original model to the induced model, + * restricted/reindexed to the induced model's states. + */ + public ConstructInducedModel setCopyRewards(boolean copyRewards) + { + this.copyRewards = copyRewards; + return this; + } + /** * Construct the model induced by a memoryless deterministic strategy on a nondeterministic model * @param model The model @@ -134,6 +162,33 @@ public Model doConstructInducedModel(ModelType modelType, ModelTy inducedStatesList = new ArrayList<>(); } + // Create empty label bitsets for the induced model, if needed + Map origLabels = null; + Map inducedLabels = null; + if (copyLabels) { + origLabels = model.getLabelToStatesMap(); + inducedLabels = new LinkedHashMap<>(); + for (String name : origLabels.keySet()) { + inducedLabels.put(name, new BitSet()); + } + } + + // Create empty reward structures for the induced model, if needed + List> origRewardsList = null; + List> inducedRewardsList = null; + if (copyRewards) { + int numRewardStructs = model.getNumRewards(); + origRewardsList = new ArrayList<>(numRewardStructs); + inducedRewardsList = new ArrayList<>(numRewardStructs); + for (int r = 0; r < numRewardStructs; r++) { + Rewards origRews = model.getRewards(r); + origRewardsList.add(origRews); + RewardsSimple inducedRews = new RewardsSimple<>(0); + inducedRews.setEvaluator(origRews.getEvaluator()); + inducedRewardsList.add(inducedRews); + } + } + // Initially create an array with 0s for reachable state indices and -1s for unreachable ones int numStates = model.getNumStates(); int[] map = new int[numStates]; @@ -210,6 +265,27 @@ public Model doConstructInducedModel(ModelType modelType, ModelTy if (reachOnly && inducedStatesList != null) { inducedStatesList.add(model.getStatesList().get(s)); } + if (copyLabels) { + for (Map.Entry e : origLabels.entrySet()) { + if (e.getValue().get(s)) { + inducedLabels.get(e.getKey()).set(map[s]); + } + } + } + // Copy state rewards; also prepare accumulators for transition rewards of chosen choices + // (transition rewards attach to a whole choice, so choices merged into a single induced + // choice/state by the strategy need their transition rewards combined too) + List transRewAcc = null; + if (copyRewards) { + transRewAcc = new ArrayList<>(origRewardsList.size()); + for (int r = 0; r < origRewardsList.size(); r++) { + Rewards origRews = origRewardsList.get(r); + if (origRews.hasStateRewards()) { + inducedRewardsList.get(r).setStateReward(map[s], origRews.getStateReward(s)); + } + transRewAcc.add(origRews.getEvaluator().zero()); + } + } int numChoices = model.getNumChoices(s); // Extract strategy decision @@ -240,6 +316,21 @@ public Model doConstructInducedModel(ModelType modelType, ModelTy if (strat.isRandomised()) { stratChoiceProb = strat.getChoiceActionProbability(decision, act); } + // Accumulate transition rewards for this choice + // (weighted by the strategy's choice probability, if randomised) + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + Rewards origRews = origRewardsList.get(r); + if (origRews.hasTransitionRewards()) { + Evaluator rewEval = origRews.getEvaluator(); + Value rew = origRews.getTransitionReward(s, j); + if (strat.isRandomised()) { + rew = rewEval.multiply(rew, stratChoiceProb); + } + transRewAcc.set(r, rewEval.add(transRewAcc.get(r), rew)); + } + } + } // Get choice action for induced model if needed if (inducedModelType.nondeterministic()) { inducedAction = strat.getInducedAction(decision, act); @@ -326,6 +417,23 @@ public Model doConstructInducedModel(ModelType modelType, ModelTy break; } } + // Store accumulated transition rewards: + // for a nondeterministic induced model, attach to the (sole) induced choice for this state; + // otherwise (induced model has no choices), fold into the induced state reward instead. + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + Value rew = transRewAcc.get(r); + RewardsSimple inducedRews = inducedRewardsList.get(r); + Evaluator rewEval = origRewardsList.get(r).getEvaluator(); + if (!rewEval.isZero(rew)) { + if (inducedModelType.nondeterministic()) { + inducedRews.setTransitionReward(map[s], 0, rew); + } else { + inducedRews.addToStateReward(map[s], rew); + } + } + } + } } inducedModel.findDeadlocks(false); @@ -334,6 +442,18 @@ public Model doConstructInducedModel(ModelType modelType, ModelTy inducedModel.setStatesList(inducedStatesList); } + if (copyLabels) { + for (Map.Entry e : inducedLabels.entrySet()) { + inducedModel.addLabel(e.getKey(), e.getValue()); + } + } + + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + inducedModel.addRewards(model.getRewardName(r), model.getRewardPosition(r), inducedRewardsList.get(r)); + } + } + return inducedModel; } } diff --git a/prism/src/explicit/ConstructStrategyProduct.java b/prism/src/explicit/ConstructStrategyProduct.java index 1c56e03085..8affce1853 100644 --- a/prism/src/explicit/ConstructStrategyProduct.java +++ b/prism/src/explicit/ConstructStrategyProduct.java @@ -31,16 +31,20 @@ import java.util.Arrays; import java.util.BitSet; import java.util.Iterator; +import java.util.LinkedHashMap; import java.util.LinkedList; import java.util.List; import java.util.Map; import common.Interval; +import explicit.rewards.Rewards; +import explicit.rewards.RewardsSimple; import parser.State; import parser.VarList; import parser.ast.Declaration; import parser.ast.DeclarationInt; import parser.ast.Expression; +import prism.Evaluator; import prism.ModelType; import prism.PrismException; import prism.PrismNotSupportedException; @@ -60,6 +64,16 @@ public class ConstructStrategyProduct */ private StrategyExportOptions.InducedModelMode mode = StrategyExportOptions.InducedModelMode.RESTRICT; + /** + * Whether to copy labels from the original model to the product model + */ + private boolean copyLabels = true; + + /** + * Whether to copy rewards from the original model to the product model + */ + private boolean copyRewards = true; + /** * Set the "mode" of construction: * "restrict" (same model type but restrict to selected action choices); or @@ -71,6 +85,26 @@ public ConstructStrategyProduct setMode(StrategyExportOptions.InducedModelMode m return this; } + /** + * Set whether to copy labels from the original model to the product model, + * restricted/reindexed to the product model's states. + */ + public ConstructStrategyProduct setCopyLabels(boolean copyLabels) + { + this.copyLabels = copyLabels; + return this; + } + + /** + * Set whether to copy rewards from the original model to the product model, + * restricted/reindexed to the product model's states. + */ + public ConstructStrategyProduct setCopyRewards(boolean copyRewards) + { + this.copyRewards = copyRewards; + return this; + } + /** * Construct the product model induced by a finite-memory strategy on a nondeterministic model * @param model The model @@ -146,8 +180,35 @@ public Model doConstructProductModel(ModelType modelType, ModelTy } catch (ArithmeticException e) { throw new PrismException("Size of product state space of model and strategy is too large for explicit engine"); } - - // Encoding: + + // Create empty label bitsets for the product model, if needed + Map origLabels = null; + Map inducedLabels = null; + if (copyLabels) { + origLabels = model.getLabelToStatesMap(); + inducedLabels = new LinkedHashMap<>(); + for (String name : origLabels.keySet()) { + inducedLabels.put(name, new BitSet()); + } + } + + // Create empty reward structures for the product model, if needed + List> origRewardsList = null; + List> inducedRewardsList = null; + if (copyRewards) { + int numRewardStructs = model.getNumRewards(); + origRewardsList = new ArrayList<>(numRewardStructs); + inducedRewardsList = new ArrayList<>(numRewardStructs); + for (int r = 0; r < numRewardStructs; r++) { + Rewards origRews = model.getRewards(r); + origRewardsList.add(origRews); + RewardsSimple inducedRews = new RewardsSimple<>(0); + inducedRews.setEvaluator(origRews.getEvaluator()); + inducedRewardsList.add(inducedRews); + } + } + + // Encoding: // each state s' = = s * memSize + q // s(s') = s' / memSize // q(s') = s' % memSize @@ -217,6 +278,28 @@ public Model doConstructProductModel(ModelType modelType, ModelTy visited.set(s_1 * memSize + q_1); int map_1 = map[s_1 * memSize + q_1]; + if (copyLabels) { + for (Map.Entry e : origLabels.entrySet()) { + if (e.getValue().get(s_1)) { + inducedLabels.get(e.getKey()).set(map_1); + } + } + } + // Copy state rewards; also prepare accumulators for transition rewards of chosen choices + // (transition rewards attach to a whole choice, so choices merged into a single induced + // choice/state by the strategy need their transition rewards combined too) + List transRewAcc = null; + if (copyRewards) { + transRewAcc = new ArrayList<>(origRewardsList.size()); + for (int r = 0; r < origRewardsList.size(); r++) { + Rewards origRews = origRewardsList.get(r); + if (origRews.hasStateRewards()) { + inducedRewardsList.get(r).setStateReward(map_1, origRews.getStateReward(s_1)); + } + transRewAcc.add(origRews.getEvaluator().zero()); + } + } + int numChoices = model.getNumChoices(s_1); // Extract strategy decision Object decision = strat.getChoiceAction(s_1, q_1); @@ -246,6 +329,21 @@ public Model doConstructProductModel(ModelType modelType, ModelTy if (strat.isRandomised()) { stratChoiceProb = strat.getChoiceActionProbability(decision, act); } + // Accumulate transition rewards for this choice + // (weighted by the strategy's choice probability, if randomised) + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + Rewards origRews = origRewardsList.get(r); + if (origRews.hasTransitionRewards()) { + Evaluator rewEval = origRews.getEvaluator(); + Value rew = origRews.getTransitionReward(s_1, j); + if (strat.isRandomised()) { + rew = rewEval.multiply(rew, stratChoiceProb); + } + transRewAcc.set(r, rewEval.add(transRewAcc.get(r), rew)); + } + } + } // Get choice action for induced model if needed if (productModelType.nondeterministic()) { inducedAction = strat.getInducedAction(decision, act); @@ -334,14 +432,43 @@ public Model doConstructProductModel(ModelType modelType, ModelTy break; } } + // Store accumulated transition rewards: + // for a nondeterministic product model, attach to the (sole) induced choice for this state; + // otherwise (product model has no choices), fold into the induced state reward instead. + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + Value rew = transRewAcc.get(r); + RewardsSimple inducedRews = inducedRewardsList.get(r); + Evaluator rewEval = origRewardsList.get(r).getEvaluator(); + if (!rewEval.isZero(rew)) { + if (productModelType.nondeterministic()) { + inducedRews.setTransitionReward(map_1, 0, rew); + } else { + inducedRews.addToStateReward(map_1, rew); + } + } + } + } } - + prodModel.findDeadlocks(false); if (prodStatesList != null) { prodModel.setStatesList(prodStatesList); } - + + if (copyLabels) { + for (Map.Entry e : inducedLabels.entrySet()) { + prodModel.addLabel(e.getKey(), e.getValue()); + } + } + + if (copyRewards) { + for (int r = 0; r < origRewardsList.size(); r++) { + prodModel.addRewards(model.getRewardName(r), model.getRewardPosition(r), inducedRewardsList.get(r)); + } + } + return prodModel; } diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 447fe6655c..260ff62c9d 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -1566,7 +1566,7 @@ protected String getRewardStructName(Model model, int r) * If no RewardGenerator is present, any rewards attached to the models are used, * with their names if present, but with any positional info ignored. */ - protected Pair>, List> getAllRewards(Model model) throws PrismException + public Pair>, List> getAllRewards(Model model) throws PrismException { List> rewards = new ArrayList<>(); List rewardNames = new ArrayList<>(); @@ -1593,6 +1593,30 @@ protected Pair>, List> getAllRewards(Model(rewards, rewardNames); } + /** + * Attach reward structures (from the currently stored reward generator, if any; see + * {@link #setModelCheckingInfo}) directly to a model, if not already present, e.g. so + * that they are available when constructing/exporting a model induced by a strategy + * (see {@link ConstructInducedModel}) or lifted onto a product model built during model + * checking (e.g. an LTL automaton product; see {@link LTLModelChecker}). + * Does nothing if the model is not mutable ({@link ModelExplicit}), if rewards are + * already attached, or if no reward generator is available. + * @param model The model + */ + public void attachRewards(Model model) throws PrismException + { + if (!(model instanceof ModelExplicit) || model.getNumRewards() > 0 || rewardGen == null) { + return; + } + Pair>, List> allRewards = getAllRewards(model); + ModelExplicit modelExplicit = (ModelExplicit) model; + List> rewardsList = allRewards.first; + List rewardNames = allRewards.second; + for (int r = 0; r < rewardsList.size(); r++) { + modelExplicit.addRewards(rewardNames.get(r), rewardsList.get(r)); + } + } + /** * Get the names of all the labels relevant/available for a model: those from the * (always present) stored model info, plus any additional labels attached directly diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b9d00e7613..973371af78 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2384,6 +2384,14 @@ private void doBuildModel() throws PrismException default: throw new PrismException("Cannot do explicit model construction for model source " + getModelSource()); } + // If strategy generation/export was requested, eagerly attach reward structures + // to the model now (mirrors how labels are already attached during ConstructModel). + // This needs to happen here, rather than later just before strategy export, since + // e.g. LTL automaton product construction (during model checking, before export) + // already lifts rewards from this model onto the product if/when present. + if (getGenStrat()) { + attachRewardsToModel(newModelExpl); + } break; default: throw new PrismException("Unknown engine " + getCurrentEngine()); @@ -3805,17 +3813,42 @@ public void exportStrategy(Strategy strat, StrategyExportOptions exportOption // Print message mainLog.print("\nExporting strategy " + exportOptions.description() + " "); mainLog.println(getDestinationStringForFile(file)); - + // Merge export options with PRISM settings and do export + StrategyExportOptions mergedExportOptions = exportOptions.clone(); + mergedExportOptions.setInducedModelExportOptions(newMergedModelExportOptions(mergedExportOptions.getInducedModelExportOptions())); + // For induced model export, attach reward structures to the strategy's model + // directly (if not already done, e.g. at model-build time), so that they get + // carried over during induced model construction (see ConstructInducedModel). + // NB: for finite-memory (e.g. LTL-derived) strategies exported without + // restricting to reachable states, this is too late (the relevant states/product + // model were already built earlier, during model checking) - see doBuildModel(). + if (exportOptions.getType() == StrategyExportType.INDUCED_MODEL && strat instanceof strat.StrategyExplicit) { + attachRewardsToModel(((strat.StrategyExplicit) strat).getModel()); + } // Export to file (or use main log) PrismLog tmpLog = getPrismLogForFile(file); exportOptions = exportOptions.clone(); - exportOptions.setModelPrecision(settings.getInteger(PrismSettings.PRISM_EXPORT_MODEL_PRECISION)); strat.export(tmpLog, exportOptions); if (file != null) { tmpLog.close(); } } + /** + * Attach reward structures (from the currently stored reward generator, if any) directly + * to a model, if not already present. Does nothing if no reward generator is available. + * @param model The model + */ + private void attachRewardsToModel(explicit.Model model) throws PrismException + { + if (getRewardGenerator() == null) { + return; + } + explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(model.getModelType(), this); + mc.setModelCheckingInfo(getModelInfo(), null, getRewardGenerator()); + mc.attachRewards(model); + } + /** * Export a strategy. The associated model should be attached to the strategy. * Strictly, speaking that does not need to be the currently loaded model, diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index da49f17781..0f2c4a4942 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1445,15 +1445,48 @@ private void initSwitchHandlers() .when("restrict", () -> exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.RESTRICT)) .when("reduce", () -> exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.REDUCE))) .bool("reach", "whether to restrict the strategy to its reachable states", v -> exportStratOptions.setReachOnly(v)) - .bool("states", "whether to show states, rather than state indices, for actions lists or Dot files", v -> exportStratOptions.setShowStates(v)) - .bool("obs", "for partially observable models, whether to merge observationally equivalent states", v -> exportStratOptions.setMergeObservations(v)), + .bool("states", "whether to include full state information ", v -> { + exportStratOptions.setShowStates(v); + pendingExportOptions.setShowStates(v); + }) + .bool("mergeobs", "for partially observable models, whether to merge observationally equivalent states ", v -> { + exportStratOptions.setMergeObservations(v); + }) + // The following options only apply to induced model export, mirroring the + // corresponding -exportmodel options (see exportModelSwitch above) + .choice("format", "model export format for induced model export", new OptionParser.Choice() + .when("explicit", () -> pendingExportOptions.setFormat(ModelExportFormat.EXPLICIT)) + .when("dot", () -> pendingExportOptions.setFormat(ModelExportFormat.DOT)) + .when("drn", () -> pendingExportOptions.setFormat(ModelExportFormat.DRN)) + .when("umb", () -> pendingExportOptions.setFormat(ModelExportFormat.UMB))) + .bool("rewards", "whether to include rewards for induced model export", + v -> pendingExportOptions.setShowRewards(v)) + .bool("labels", "whether to include labels for induced model export", + v -> pendingExportOptions.setShowLabels(v)) + .bool("actions", "whether to include actions on choices/transitions for induced model export", + v -> pendingExportOptions.setShowActions(v)) + .bool("obs", "whether to include observation details for induced model export", + v -> pendingExportOptions.setShowObservations(v)) + .integer("precision", "", n -> RANGE_EXPORT_DOUBLE_PRECISION.contains(n), + "use significant figures for floating point values (in text) for induced model export", + n -> pendingExportOptions.setModelPrecision(n)) + .choice("zip", "whether to zip files for induced model export", new OptionParser.Choice() + .when("true", () -> pendingExportOptions.setZipped(true)) + .when("false", () -> pendingExportOptions.setZipped(false)) + .when("gzip", "gz", () -> pendingExportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.GZIP)) + .when("xz", () -> pendingExportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.XZ))) + .flag("text", "show binary formats in textual form for induced model export", + () -> pendingExportOptions.setBinaryAsText(true)) + .bool("headers", "include headers in explicit model files for induced model export", + v -> pendingExportOptions.setPrintHeaders(v)), this::processExportStratSwitch); registry.addSwitch("exportstrat", exportStratSwitch, "]>", "Generate and export a strategy to a file", log -> { - log.println("Generate and export a strategy to a file (or to the screen if =\"stdout\")."); - log.println("Use file extension .tra or .dot to export as an induced model or Dot file, respectively."); - log.println("If provided, is a comma-separated list of options taken from:"); + log.println("Generate and export a strategy to a file (or to the screen if \"stdout\")."); + log.println("Use file extension .tra, .pexp, .umb or .dot to export as an induced model."); + log.println("The default (e.g. for file extension .txt) is a list of stat-action choices."); + log.println("\nIf provided, is a comma-separated list of options taken from:"); exportStratSwitch.printOptions(log); }); registry.addSwitch("exportmatlab", new FlagSwitch(() -> { @@ -1930,16 +1963,24 @@ private void processExportStratSwitch(String fileString, StringPlusOptionsSwitch exportStratFilename = basename.equals("stdout") ? "stdout" : fileString; exportStratOptions = new StrategyExportOptions(); prism.setGenStrat(true); + ModelExportTask inducedModelTask = null; + ModelExportOptions inducedModelOptions = new ModelExportOptions(); // Default strategy export type is based on filename extension - if (ext.equals("tra")) { + if (ext.equals("tra") || ext.equals("pexp") || ext.equals("umb")) { exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDUCED_MODEL); + inducedModelOptions = ModelExportTask.fromFilename(basename, ext).getExportOptions(); } else if (ext.equals("dot")) { exportStratOptions.setType(StrategyExportOptions.StrategyExportType.DOT_FILE); } else { exportStratOptions.setType(StrategyExportOptions.StrategyExportType.ACTIONS); } // Process options + pendingExportOptions = new ModelExportOptions(); parse.run(); + if (inducedModelOptions != null) { + inducedModelOptions.apply(pendingExportOptions); + exportStratOptions.setInducedModelExportOptions(inducedModelOptions); + } } // print command line arguments diff --git a/prism/src/strat/FMDObsStrategyBeliefs.java b/prism/src/strat/FMDObsStrategyBeliefs.java index 59c0513814..c643c6a9de 100644 --- a/prism/src/strat/FMDObsStrategyBeliefs.java +++ b/prism/src/strat/FMDObsStrategyBeliefs.java @@ -193,23 +193,12 @@ public void exportIndices(PrismLog out, StrategyExportOptions options) public void exportInducedModel(PrismLog out, StrategyExportOptions options) throws PrismException { if (options.getMergeObservations()) { - exportInducedModelObs(out, options); + mdpStrat.export(out, options.getInducedModelExportOptions()); } else { - exportInducedModelNonObs(out, options); + super.exportInducedModel(out, options); } } - public void exportInducedModelObs(PrismLog out, StrategyExportOptions options) throws PrismException - { - mdpStrat.exportToPrismExplicitTra(out, options.getModelPrecision()); - } - - public void exportInducedModelNonObs(PrismLog out, StrategyExportOptions options) throws PrismException - { - Model prodModel = constructInducedModel(options); - prodModel.exportToPrismExplicitTra(out, options.getModelPrecision()); - } - @Override public void exportDotFile(PrismLog out, StrategyExportOptions options) throws PrismException { diff --git a/prism/src/strat/FMDStrategyProduct.java b/prism/src/strat/FMDStrategyProduct.java index 588c1fb931..7cb577f866 100644 --- a/prism/src/strat/FMDStrategyProduct.java +++ b/prism/src/strat/FMDStrategyProduct.java @@ -204,8 +204,7 @@ public void exportInducedModel(PrismLog out, StrategyExportOptions options) thro { // If restricting to reachable states, construct product afresh if (options.getReachOnly()) { - Model prodModel = constructInducedModel(options); - prodModel.exportToPrismExplicitTra(out, options.getModelPrecision()); + super.exportInducedModel(out, options); } // Otherwise, just export MD strategy, unmodified else { diff --git a/prism/src/strat/FMDStrategyStep.java b/prism/src/strat/FMDStrategyStep.java index 6bb3512548..653039fb56 100644 --- a/prism/src/strat/FMDStrategyStep.java +++ b/prism/src/strat/FMDStrategyStep.java @@ -162,13 +162,6 @@ public void exportIndices(PrismLog out, StrategyExportOptions options) } } - @Override - public void exportInducedModel(PrismLog out, StrategyExportOptions options) throws PrismException - { - Model prodModel = constructInducedModel(options); - prodModel.exportToPrismExplicitTra(out, options.getModelPrecision()); - } - @Override public void exportDotFile(PrismLog out, StrategyExportOptions options) throws PrismException { diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index 7966e8bc97..db1e857e47 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -109,13 +109,6 @@ public void exportActions(PrismLog out, StrategyExportOptions options) } } - @Override - public void exportInducedModel(PrismLog out, StrategyExportOptions options) throws PrismException - { - Model inducedModel = constructInducedModel(options); - inducedModel.exportToPrismExplicitTra(out, options.getModelPrecision()); - } - @Override public void exportDotFile(PrismLog out, StrategyExportOptions options) throws PrismException { diff --git a/prism/src/strat/MRStrategy.java b/prism/src/strat/MRStrategy.java index 07ac03eadc..d083f9f6b0 100644 --- a/prism/src/strat/MRStrategy.java +++ b/prism/src/strat/MRStrategy.java @@ -102,13 +102,6 @@ public void exportIndices(PrismLog out, StrategyExportOptions options) throws Pr } } - @Override - public void exportInducedModel(PrismLog out, StrategyExportOptions options) throws PrismException - { - Model inducedModel = constructInducedModel(options); - inducedModel.exportToPrismExplicitTra(out, options.getModelPrecision()); - } - @Override public void exportDotFile(PrismLog out, StrategyExportOptions options) throws PrismException { diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java index ec66d47996..9976dc45b8 100644 --- a/prism/src/strat/Strategy.java +++ b/prism/src/strat/Strategy.java @@ -228,7 +228,7 @@ public default prism.Model constructInducedModel() throws PrismException } /** - * Export the model induced by this strategy to a PrismLog. + * Construct the model induced by this strategy. */ public prism.Model constructInducedModel(StrategyExportOptions options) throws PrismException; diff --git a/prism/src/strat/StrategyExplicit.java b/prism/src/strat/StrategyExplicit.java index 04613040ca..217276082a 100644 --- a/prism/src/strat/StrategyExplicit.java +++ b/prism/src/strat/StrategyExplicit.java @@ -26,8 +26,11 @@ package strat; +import explicit.Model; import explicit.NondetModel; import prism.Evaluator; +import prism.PrismException; +import prism.PrismLog; /** * Base class for implementations of Strategy associated with an explicit engine model. @@ -58,4 +61,13 @@ public Evaluator getEvaluator() { return model.getEvaluator(); } + + @Override + public abstract Model constructInducedModel(StrategyExportOptions options) throws PrismException; + + @Override + public void exportInducedModel(PrismLog out, StrategyExportOptions options) throws PrismException + { + constructInducedModel(options).export(out, options.getInducedModelExportOptions()); + } } diff --git a/prism/src/strat/StrategyExportOptions.java b/prism/src/strat/StrategyExportOptions.java index fea2138a03..15f5cb7cf9 100644 --- a/prism/src/strat/StrategyExportOptions.java +++ b/prism/src/strat/StrategyExportOptions.java @@ -28,6 +28,12 @@ import static prism.PrismSettings.DEFAULT_EXPORT_MODEL_PRECISION; +import io.ModelExportFormat; +import io.ModelExportOptions; +import io.ModelExportTask; + +import java.io.File; +import java.util.List; import java.util.Optional; /** @@ -107,6 +113,11 @@ public String description() */ private Optional modelPrecision = Optional.empty(); + /** + * For induced model export, the model export options. + */ + private Optional inducedModelExportOptions = Optional.empty();; + // Constructors /** @@ -183,6 +194,15 @@ public StrategyExportOptions setModelPrecision(int modelPrecision) return this; } + /** + * Set the model export tasks specifying details for induced model export. + */ + public StrategyExportOptions setInducedModelExportOptions(ModelExportOptions inducedModelExportOptions) + { + this.inducedModelExportOptions = Optional.of(inducedModelExportOptions); + return this; + } + // Get methods /** @@ -206,7 +226,7 @@ public InducedModelMode getMode() */ public boolean getReachOnly() { - return reachOnly.orElse(!getType().equals(StrategyExportType.INDUCED_MODEL)); + return reachOnly.orElse(true); } /** @@ -233,6 +253,14 @@ public int getModelPrecision() return modelPrecision.orElse(DEFAULT_EXPORT_MODEL_PRECISION); } + /** + * Get the model export options for induced model export. + */ + public ModelExportOptions getInducedModelExportOptions() + { + return inducedModelExportOptions.orElse(new ModelExportOptions()); + } + /** * Get string description for type of strategy export. */