From c5eaee22f7948ad0835241089ef151733f49e9a7 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 4 Jul 2017 08:34:15 +0000
Subject: [PATCH] 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 | 27 +++++++++++++++++++++++++++
 prism/src/prism/Prism.java           |  8 +++++++-
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index fecc1ef7..6569c666 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/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 
 	 */
diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 0b1557f9..2279cf1e 100644
--- a/prism/src/prism/Prism.java
+++ b/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();