Explicit model checking engines respect restrictStratToReach setting in exportAdv mode. Also set that flag to true by default since only used here currently.

prism/src/explicit/MDPModelChecker.java

@@ -526,8 +526,10 @@ public class MDPModelChecker extends ProbModelChecker
 		}
 		// Export adversary
 		if (exportAdv) {
-			// Prune strategy
-			restrictStrategyToReachableStates(mdp, strat);
+			// Prune strategy, if needed
+			if (getRestrictStratToReach()) {
+				restrictStrategyToReachableStates(mdp, strat);
+			}
 			// Export
 			PrismLog out = new PrismFileLog(exportAdvFilename);
 			new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out);
@@ -2200,8 +2202,10 @@ public class MDPModelChecker extends ProbModelChecker
 		}
 		// Export adversary
 		if (exportAdv) {
-			// Prune strategy
-			restrictStrategyToReachableStates(mdp, strat);
+			// Prune strategy, if needed
+			if (getRestrictStratToReach()) {
+				restrictStrategyToReachableStates(mdp, strat);
+			}
 			// Export
 			PrismLog out = new PrismFileLog(exportAdvFilename);
 			new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out);

prism/src/explicit/StateModelChecker.java

@@ -112,6 +112,8 @@ public class StateModelChecker extends PrismComponent
 
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
+	// Should any generated strategies should be restricted to the states reachable under them?
+	protected boolean restrictStratToReach = true;
 
 	// Do bisimulation minimisation before model checking?
 	protected boolean doBisim = false;
@@ -220,6 +222,7 @@ public class StateModelChecker extends PrismComponent
 		setExportProductVectorFilename(other.getExportProductVectorFilename());
 		setStoreVector(other.getStoreVector());
 		setGenStrat(other.getGenStrat());
+		setRestrictStratToReach(other.getRestrictStratToReach());
 		setDoBisim(other.getDoBisim());
 		setDoIntervalIteration(other.getDoIntervalIteration());
 		setDoPmaxQuotient(other.getDoPmaxQuotient());
@@ -299,6 +302,14 @@ public class StateModelChecker extends PrismComponent
 		this.genStrat = genStrat;
 	}
 
+	/**
+	 * Specify whether or not any generated strategies should be restricted to the states reachable under them.
+	 */
+	public void setRestrictStratToReach(boolean restrictStratToReach)
+	{
+		this.restrictStratToReach = restrictStratToReach;
+	}
+
 	/**
 	 * Specify whether or not to do bisimulation minimisation before model checking.
 	 */
@@ -394,6 +405,14 @@ public class StateModelChecker extends PrismComponent
 		return genStrat;
 	}
 
+	/**
+	 * Whether or not any generated strategies should be restricted to the states reachable under them.
+	 */
+	public boolean getRestrictStratToReach()
+	{
+		return restrictStratToReach;
+	}
+
 	/**
 	 * Whether or not to do bisimulation minimisation before model checking.
 	 */

prism/src/prism/Prism.java

@@ -200,7 +200,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
 	// Should any generated strategies should be restricted to the states reachable under them?
-	protected boolean restrictStratToReach = false;
+	protected boolean restrictStratToReach = true;
 	// Do bisimulation minimisation before model checking?
 	protected boolean doBisim = false;
 
@@ -3782,6 +3782,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		mc.setExportProductVectorFilename(exportProductVectorFilename);
 		mc.setStoreVector(storeVector);
 		mc.setGenStrat(genStrat);
+		mc.setRestrictStratToReach(restrictStratToReach);
 		mc.setDoBisim(doBisim);
 		mc.setDoIntervalIteration(settings.getBoolean(PrismSettings.PRISM_INTERVAL_ITER));
 		mc.setDoTopologicalValueIteration(settings.getBoolean(PrismSettings.PRISM_TOPOLOGICAL_VI));