diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 8b01a24f..da75c465 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index fc5ca04a..0adf1077 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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. */ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 0486509b..1bb6ce4e 100644 --- a/prism/src/prism/Prism.java +++ b/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));