diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 4109c10a..6024c782 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -70,9 +70,6 @@ public class ProbModelChecker extends StateModelChecker protected boolean exportAdv = false; protected String exportAdvFilename; - // Additional flags/settings not included in PrismSettings - protected boolean getStrat = false; - // Enums for flags/settings // Method used for numerical solution diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 28ff2b50..4cb46864 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -87,6 +87,11 @@ public class StateModelChecker // Method used for numerical solution protected SCCMethod sccMethod = SCCMethod.TARJAN; + // Additional flags/settings not included in PrismSettings + + // Generate/store a strategy during model checking? + protected boolean genStrat = false; + // Model file (for reward structures, etc.) protected ModulesFile modulesFile = null; @@ -208,6 +213,14 @@ public class StateModelChecker this.verbosity = verbosity; } + /** + * Specify whether or not a strategy should be generated during model checking. + */ + public void setGenStrat(boolean genStrat) + { + this.genStrat = genStrat; + } + // Get methods for flags/settings public int getVerbosity() @@ -215,6 +228,14 @@ public class StateModelChecker return verbosity; } + /** + * Whether or not a strategy should be generated during model checking. + */ + public boolean getGenStrat() + { + return genStrat; + } + // Model checking functions /** diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5bc39584..d8c5259c 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -176,7 +176,7 @@ public class Prism implements PrismSettingsListener protected String exportProductTransFilename = null; protected boolean exportProductStates = false; protected String exportProductStatesFilename = null; - // Generate a strategy during model checking? + // Generate/store a strategy during model checking? protected boolean genStrat = false; // A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.) @@ -2466,13 +2466,10 @@ public class Prism implements PrismSettingsListener // Create new model checker object and do model checking if (!getExplicit()) { - ModelChecker mc = StateModelChecker.createModelChecker(currentModelType, this, currentModel, propertiesFile); + ModelChecker mc = createModelChecker(propertiesFile); res = mc.check(prop.getExpression()); } else { - explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType); - mc.setLog(mainLog); - mc.setSettings(settings); - mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + explicit.StateModelChecker mc = createModelCheckerExplicit(propertiesFile); res = mc.check(currentModelExpl, prop.getExpression()); } } finally { @@ -3094,6 +3091,37 @@ public class Prism implements PrismSettingsListener } } + /** + * Utility method to create and initialiser a (symbolic) model checker based on the current model. + * @param propertiesFile Optional properties file for extra info needed durinng model checking (can be null) + */ + private ModelChecker createModelChecker(PropertiesFile propertiesFile) throws PrismException + { + // Create model checker + ModelChecker mc = StateModelChecker.createModelChecker(currentModelType, this, currentModel, propertiesFile); + // Pass any additional local settings + // TODO + + return mc; + } + + /** + * Utility method to create and initialiser an (explicit) model checker based on the current model. + * @param propertiesFile Optional properties file for extra info needed durinng model checking (can be null) + */ + private explicit.StateModelChecker createModelCheckerExplicit(PropertiesFile propertiesFile) throws PrismException + { + // Create model checker + explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType); + mc.setLog(mainLog); + mc.setSettings(settings); + mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); + // Pass any additional local settings + mc.setGenStrat(genStrat); + + return mc; + } + /** * Either create a new PrismFileLog for {@code file} or, * if {@code file} is null, return {@code mainLog}.