diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index b21726ba..fb1052c6 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -60,6 +60,7 @@ import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypeInt; import prism.Filter; +import prism.ModelType; import prism.PrismException; import prism.PrismLangException; import prism.PrismLog; @@ -93,6 +94,34 @@ public class StateModelChecker // The result of model checking will be stored here protected Result result; + /** + * Create a model checker (a subclass of this one) for a given model type + */ + public static StateModelChecker createModelChecker(ModelType modelType) throws PrismException + { + explicit.StateModelChecker mc = null; + switch (modelType) { + case DTMC: + mc = new DTMCModelChecker(); + break; + case MDP: + mc = new MDPModelChecker(); + break; + case CTMC: + mc = new CTMCModelChecker(); + break; + case CTMDP: + mc = new CTMDPModelChecker(); + break; + case STPG: + mc = new STPGModelChecker(); + break; + default: + throw new PrismException("Cannot create model checker for model type " + modelType); + } + return mc; + } + // Flags/settings // Verbosity level diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e0901157..984753ca 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2353,42 +2353,10 @@ public class Prism implements PrismSettingsListener // Create new model checker object and do model checking if (!getExplicit()) { - ModelChecker mc = null; - switch (currentModelType) { - case DTMC: - mc = new ProbModelChecker(this, currentModel, propertiesFile); - break; - case MDP: - mc = new NondetModelChecker(this, currentModel, propertiesFile); - break; - case CTMC: - mc = new StochModelChecker(this, currentModel, propertiesFile); - break; - default: - throw new PrismException("Unknown model type " + currentModelType); - } + ModelChecker mc = StateModelChecker.createModelChecker(currentModelType, this, currentModel, propertiesFile); res = mc.check(prop.getExpression()); } else { - explicit.StateModelChecker mc = null; - switch (currentModelType) { - case DTMC: - mc = new DTMCModelChecker(); - break; - case MDP: - mc = new MDPModelChecker(); - break; - case CTMC: - mc = new CTMCModelChecker(); - break; - case CTMDP: - mc = new CTMDPModelChecker(); - break; - case STPG: - mc = new STPGModelChecker(); - break; - default: - throw new PrismException("Unknown model type " + currentModelType); - } + explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType); mc.setLog(mainLog); mc.setSettings(settings); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 8ab5934f..2b563bba 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -129,6 +129,28 @@ public class StateModelChecker implements ModelChecker null, 0, varList, varDDRowVars, null, constantValues); } + /** + * Create a model checker (a subclass of this one) for a given model type + */ + public static ModelChecker createModelChecker(ModelType modelType, Prism prism, Model model, PropertiesFile propertiesFile) throws PrismException + { + ModelChecker mc = null; + switch (modelType) { + case DTMC: + mc = new ProbModelChecker(prism, model, propertiesFile); + break; + case MDP: + mc = new NondetModelChecker(prism, model, propertiesFile); + break; + case CTMC: + mc = new StochModelChecker(prism, model, propertiesFile); + break; + default: + throw new PrismException("Cannot create model checker for model type " + modelType); + } + return mc; + } + /** * Clean up the dummy model created when using the abbreviated constructor */