Add -heuristic switch to trigger automatic selection of engines/settings.

Currently, just implement some simple defaults for the "speed" settings.

prism/src/prism/Prism.java

@@ -153,6 +153,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	public static final int LOCKSTEP = 2;
 	public static final int SCCFIND = 3;
 
+	// state space cut-off to trigger MTBDD engine
+	protected static final int MTBDD_STATES_THRESHOLD = 100000000;
+	
 	// Options for type of strategy export
 	public enum StrategyExportType {
 		ACTIONS, INDICES, INDUCED_MODEL, DOT_FILE;
@@ -2980,7 +2983,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	{
 		Result res = null;
 		Values definedPFConstants = propertiesFile.getConstantValues();
-		boolean engineSwitch = false;
+		boolean engineSwitch = false, switchToMTBDDEngine = false;
 		int lastEngine = -1;
 
 		if (!digital)
@@ -3009,6 +3012,15 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile);
 			return fauMC.check(prop.getExpression());
 		}
+		// Heuristic choices of engine/method
+		if (settings.getString(PrismSettings.PRISM_HEURISTIC).equals("Speed")) {
+			mainLog.printWarning("Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).");
+			engineSwitch = true;
+			lastEngine = getEngine();
+			setEngine(Prism.SPARSE);
+			settings.set(PrismSettings.PRISM_LIN_EQ_METHOD, "Backwards Gauss-Seidel");
+
+		}
 		// Auto-switch engine if required
 		if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
 			if (getMDPSolnMethod() != Prism.MDP_VALITER && !getExplicit()) {
@@ -3044,14 +3056,26 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 							+ "Either switch to the explicit engine or add more action labels to the model");
 			}
 
-			if (!getExplicit() && !engineSwitch && getEngine() != MTBDD) {
-				// check if we need to switch to MTBDD engine
+			// Check if we need to switch to MTBDD engine
+			if (!getExplicit() && getEngine() != MTBDD) {
 				long n = currentModel.getNumStates();
+				// Either because number of states is two big for double-valued solution vectors
 				if (n == -1 || n > Integer.MAX_VALUE) {
 					mainLog.printWarning("Switching to MTBDD engine, as number of states is too large for " + engineStrings[getEngine()] + " engine.");
+					switchToMTBDDEngine = true;
+				}
+				// Or based on heuristic choices of engine/method
+				// (sparse/hybrid typically v slow if need to work with huge state spaces)
+				else if (settings.getString(PrismSettings.PRISM_HEURISTIC).equals("Speed") && n > MTBDD_STATES_THRESHOLD) {
+					mainLog.printWarning("Switching to MTBDD engine (default for heuristic=speed and this state space size).");
+					switchToMTBDDEngine = true;
+				}
+				// NB: Need to make sure solution methods supported for MTBDDs are used
+				if (switchToMTBDDEngine) {
 					engineSwitch = true;
 					lastEngine = getEngine();
 					setEngine(Prism.MTBDD);
+					settings.set(PrismSettings.PRISM_LIN_EQ_METHOD, "Jacobi");
 				}
 			}
 

prism/src/prism/PrismSettings.java

@@ -72,6 +72,7 @@ public class PrismSettings implements Observer
 	
 	//PRISM
 	public static final	String PRISM_ENGINE							= "prism.engine";
+	public static final	String PRISM_HEURISTIC						= "prism.heuristic";
 	public static final	String PRISM_VERBOSE						= "prism.verbose";
 	public static final	String PRISM_FAIRNESS						= "prism.fairness";
 	public static final	String PRISM_PRECOMPUTATION					= "prism.precomputation";
@@ -233,6 +234,8 @@ public class PrismSettings implements Observer
 			// ENGINES/METHODS:
 			{ CHOICE_TYPE,		PRISM_ENGINE,							"Engine",								"2.1",			"Hybrid",																	"MTBDD,Sparse,Hybrid,Explicit",																		
 																			"Which engine (hybrid, sparse, MTBDD, explicit) should be used for model checking." },
+			{ CHOICE_TYPE,		PRISM_HEURISTIC,						"Heuristic mode",							"4.5",			"None",																		"None,Speed,Memory",																		
+																			"Which heuristic mode to use for picking engines/settings (none, speed, memory)." },
 			{ BOOLEAN_TYPE,		PRISM_EXACT_ENABLED,					"Do exact model checking",			"4.2.1",			new Boolean(false),															"",
 																			"Perform exact model checking." },
 																			
@@ -1031,6 +1034,22 @@ public class PrismSettings implements Observer
 				throw new PrismException("No parameter specified for -" + sw + " switch");
 			}
 		}
+		// Heuristic modes
+		else if (sw.equals("heuristic")) {
+			if (i < args.length - 1) {
+				s = args[++i];
+				if (s.equals("none"))
+					set(PRISM_HEURISTIC, "None");
+				else if (s.equals("speed"))
+					set(PRISM_HEURISTIC, "Speed");
+				else if (s.equals("memory"))
+					set(PRISM_HEURISTIC, "Memory");
+				else
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: none, speed, memory)");
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
+			}
+		}
 
 		// NUMERICAL SOLUTION OPTIONS:
 		
@@ -1766,6 +1785,7 @@ public class PrismSettings implements Observer
 		mainLog.println("-exact ......................... Perform exact (arbitrary precision) model checking");
 		mainLog.println("-ptamethod <name> .............. Specify PTA engine (games, digital, backwards) [default: games]");
 		mainLog.println("-transientmethod <name> ........ CTMC transient analysis methof (unif, fau) [default: unif]");
+		mainLog.println("-heuristic <mode> .............. Automatic choice of engines/settings (none, speed, memory) [default: none]");
 		mainLog.println();
 		mainLog.println("SOLUTION METHODS (LINEAR EQUATIONS):");
 		mainLog.println("-power (or -pow, -pwr) ......... Use the Power method for numerical computation");