-exportstrat can export full induced model, including states/labels/rewards

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;

prism-tests/functionality/export/strat/exportstratinduced.nm.props

@@ -0,0 +1,2 @@
+// RESULT: 0.5
+Pmax=? [ F "goal1" ];

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

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

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)

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

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

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)

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

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

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

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

prism/src/explicit/ConstructInducedModel.java

@@ -27,20 +27,18 @@
 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;
 import strat.Strategy;
 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 <Value> Model<Value> doConstructInducedModel(ModelType modelType, ModelTy
 			inducedStatesList = new ArrayList<>();
 		}
 
+		// Create empty label bitsets for the induced model, if needed
+		Map<String, BitSet> origLabels = null;
+		Map<String, BitSet> 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<Rewards<Value>> origRewardsList = null;
+		List<RewardsSimple<Value>> inducedRewardsList = null;
+		if (copyRewards) {
+			int numRewardStructs = model.getNumRewards();
+			origRewardsList = new ArrayList<>(numRewardStructs);
+			inducedRewardsList = new ArrayList<>(numRewardStructs);
+			for (int r = 0; r < numRewardStructs; r++) {
+				Rewards<Value> origRews = model.getRewards(r);
+				origRewardsList.add(origRews);
+				RewardsSimple<Value> 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 <Value> Model<Value> doConstructInducedModel(ModelType modelType, ModelTy
 			if (reachOnly && inducedStatesList != null) {
 				inducedStatesList.add(model.getStatesList().get(s));
 			}
+			if (copyLabels) {
+				for (Map.Entry<String, BitSet> 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<Value> transRewAcc = null;
+			if (copyRewards) {
+				transRewAcc = new ArrayList<>(origRewardsList.size());
+				for (int r = 0; r < origRewardsList.size(); r++) {
+					Rewards<Value> 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 <Value> Model<Value> 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<Value> origRews = origRewardsList.get(r);
+						if (origRews.hasTransitionRewards()) {
+							Evaluator<Value> 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 <Value> Model<Value> 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<Value> inducedRews = inducedRewardsList.get(r);
+					Evaluator<Value> 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 <Value> Model<Value> doConstructInducedModel(ModelType modelType, ModelTy
 			inducedModel.setStatesList(inducedStatesList);
 		}
 
+		if (copyLabels) {
+			for (Map.Entry<String, BitSet> 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;
 	}
 }