diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 7e419d18..f1cfed5f 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -85,6 +85,9 @@ public class StateModelChecker extends PrismComponent // Additional flags/settings not included in PrismSettings + // Store the final results vector after model checking? + protected boolean storeVector = false; + // Generate/store a strategy during model checking? protected boolean genStrat = false; @@ -192,6 +195,14 @@ public class StateModelChecker extends PrismComponent this.verbosity = verbosity; } + /** + * Specify whether or not to store the final results vector after model checking. + */ + public void setStoreVector(boolean storeVector) + { + this.storeVector = storeVector; + } + /** * Specify whether or not a strategy should be generated during model checking. */ @@ -215,6 +226,14 @@ public class StateModelChecker extends PrismComponent return verbosity; } + /** + * Whether or not to store the final results vector after model checking. + */ + public boolean getStoreVector() + { + return storeVector; + } + /** * Whether or not a strategy should be generated during model checking. */ @@ -271,7 +290,11 @@ public class StateModelChecker extends PrismComponent // Wrap a filter round the property, if needed // (in order to extract the final result of model checking) - expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1); + ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1); + // And if we need to store a copy of the results vector, make a note of this + if (storeVector) { + exprFilter.setStoreVector(true); + } // If required, do bisimulation minimisation if (doBisim) { diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index bf37dfc4..58b3a4b1 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -54,8 +54,11 @@ public class ExpressionFilter extends Expression private boolean invisible = false; // Whether or not an explanation should be displayed when model checking private boolean explanationEnabled = true; + // Do we need to store a copy of the results vector when model checking this? + private boolean storeVector = false; // whether this is a filter over parameters private boolean param = false; + // Constructors @@ -127,6 +130,11 @@ public class ExpressionFilter extends Expression this.explanationEnabled = explanationEnabled; } + public void setStoreVector(boolean storeVector) + { + this.storeVector = storeVector; + } + public void setParam() { param = true; @@ -164,6 +172,11 @@ public class ExpressionFilter extends Expression return explanationEnabled; } + public boolean getStoreVector() + { + return storeVector; + } + public boolean isParam() { return param; @@ -257,7 +270,7 @@ public class ExpressionFilter extends Expression * @param expr Expression to be model checked * @param singleInit Does the model on which it is being checked have a single initial states? */ - public static Expression addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException + public static ExpressionFilter addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException { ExpressionFilter exprFilter = null; @@ -301,7 +314,8 @@ public class ExpressionFilter extends Expression exprFilter.typeCheck(); return exprFilter; } else { - return expr; + // If no new filter was created, we no expr is an ExpressionFilter + return (ExpressionFilter) expr; } } } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 35020bae..b0abae84 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -193,6 +193,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener protected String exportProductTransFilename = null; protected boolean exportProductStates = false; protected String exportProductStatesFilename = null; + // Store the final results vector after model checking? + protected boolean storeVector = false; // Generate/store a strategy during model checking? protected boolean genStrat = false; // Do bisimulation minimisation before model checking? @@ -588,6 +590,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener exportProductStatesFilename = s; } + /** + * Specify whether or not to store the final results vector after model checking. + */ + public void setStoreVector(boolean storeVector) + { + this.storeVector = storeVector; + } + /** * Specify whether or not a strategy should be generated during model checking. */ @@ -886,6 +896,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener return exportProductStatesFilename; } + /** + * Whether or not to store the final results vector after model checking. + */ + public boolean getStoreVector() + { + return storeVector; + } + /** * Whether or not a strategy should be generated during model checking. */ @@ -3461,6 +3479,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); // Pass any additional local settings + mc.setStoreVector(storeVector); mc.setGenStrat(genStrat); mc.setDoBisim(doBisim); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 97ab0754..f8b096d6 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -76,6 +76,8 @@ public class StateModelChecker implements ModelChecker protected double termCritParam; // Verbose mode? protected boolean verbose; + // Store the final results vector after model checking? + protected boolean storeVector = false; // Generate/store a strategy during model checking? protected boolean genStrat = false; @@ -179,7 +181,12 @@ public class StateModelChecker implements ModelChecker // Wrap a filter round the property, if needed // (in order to extract the final result of model checking) - expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1); + ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1); + // And if we need to store a copy of the results vector, make a note of this + if (storeVector) { + exprFilter.setStoreVector(true); + } + expr = exprFilter; // Do model checking and store result vector timer = System.currentTimeMillis();