Static methods to create model checkers by type.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5314 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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);

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
 	 */