Automatically switch to MTBDD engine before model checking if hybrid/sparse engine can not handle state space

If, after model building with hybrid or sparse engine, we detect that the
configured engine can definitely not handle the model (i.e., if number of states
is larger than Integer.MAX_VALUE), we auto-switch to the MTBDD engine.

prism/src/prism/Prism.java

@@ -2953,6 +2953,17 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 							+ "Either switch to the explicit engine or add more action labels to the model");
 			}
 
+			if (!getExplicit() && !engineSwitch) {
+				// check if we need to switch to MTBDD engine
+				long n = currentModel.getNumStates();
+				if (n == -1 || n > Integer.MAX_VALUE) {
+					mainLog.printWarning("Switching to MTBDD engine, as number of states is too large for " + engineStrings[getEngine()] + " engine.");
+					engineSwitch = true;
+					lastEngine = getEngine();
+					setEngine(Prism.MTBDD);
+				}
+			}
+
 			// Create new model checker object and do model checking
 			if (!getExplicit()) {
 				ModelChecker mc = createModelChecker(propertiesFile);