Auto-switch to explicit engine for non-probabilistic LTL model checking.

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

prism/src/parser/ast/Expression.java

@@ -836,6 +836,33 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 	
+	/**
+	 * Test if an expression contains a non-probabilistic LTL formula (i.e., a non-simple path formula). 
+	 */
+	public static boolean containsNonProbLTLFormula(Expression expr)
+	{
+		try {
+			ASTTraverse astt = new ASTTraverse()
+			{
+				public void visitPost(ExpressionForAll e) throws PrismLangException
+				{
+					if (!e.getExpression().isSimplePathFormula())
+						throw new PrismLangException("Found one", e);
+				}
+				
+				public void visitPost(ExpressionExists e) throws PrismLangException
+				{
+					if (!e.getExpression().isSimplePathFormula())
+						throw new PrismLangException("Found one", e);
+				}
+			};
+			expr.accept(astt);
+		} catch (PrismLangException e) {
+			return true;
+		}
+		return false;
+	}
+	
 	/**
 	 * Test if an expression contains a multi(...) property within 
 	 */

prism/src/prism/Prism.java

@@ -2872,7 +2872,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			return fauMC.check(prop.getExpression());
 		}
 		// Auto-switch engine if required
-		else if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
+		if (currentModelType == ModelType.MDP && !Expression.containsMultiObjective(prop.getExpression())) {
 			if (getMDPSolnMethod() != Prism.MDP_VALITER && !getExplicit()) {
 				mainLog.printWarning("Switching to explicit engine to allow use of chosen MDP solution method.");
 				engineSwitch = true;
@@ -2880,6 +2880,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 				setEngine(Prism.EXPLICIT);
 			}
 		}
+		if (Expression.containsNonProbLTLFormula(prop.getExpression())) {
+			mainLog.printWarning("Switching to explicit engine to allow non-probabilistuc LTL mocel checking.");
+			engineSwitch = true;
+			lastEngine = getEngine();
+			setEngine(Prism.EXPLICIT);
+		}
 		try {
 			// Build model, if necessary
 			buildModelIfRequired();