imported patch activate-ltl-step-bounds.patch

prism-tests/bugfixes/supersimple.pm.boundedltl.props

@@ -8,12 +8,12 @@ P>=1 [ F<=1 P>0 [ X F "a" ] ]
 // RESULT: true
 P>0.5 [ F>=1 P>0 [ X F "a" ] ]
 
-// These ones *should* fail for now
-// since there is no support for timed LTL currently
+// These ones are now supported
+// as well
 
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F P>0 [ X F<=4 "a" ] ]
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F<=1 P>0 [ X F "a" ] ]
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F P>0 [ X F<=1 "a" ] ]

prism/src/automata/LTL2DA.java

@@ -49,6 +49,7 @@ import jltl2ba.LTLFragments;
 import jltl2dstar.LTL2Rabin;
 import parser.Values;
 import parser.ast.Expression;
+import parser.visitor.ExpandStepBoundsSyntactically;
 import parser.ast.ExpressionHOA;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionUnaryOp;
@@ -102,9 +103,6 @@ public class LTL2DA extends PrismComponent
 
 		boolean useExternal = useExternal();
 		boolean containsTemporalBounds = Expression.containsTemporalTimeBounds(ltl);
-		if (containsTemporalBounds) {
-			useExternal = false;
-		}
 
 		if (!useExternal) {
 			try {
@@ -114,21 +112,22 @@ public class LTL2DA extends PrismComponent
 					getLog().println("Taking "+result.getAutomataType()+" from library...");
 				}
 			} catch (Exception e) {
-				if (containsTemporalBounds) {
-					// there is (currently) no other way to translate LTL with temporal bounds,
-					// so treat an exception as a "real" one
-					throw e;
-				} else {
 				// there is the possibility that we might be able to construct
 				// an automaton below, just issue a warning
 				getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
 				getLog().println(" " + e.getMessage());
 			}
 		}
-		}
 
 		if (result == null) {
-			if (!containsTemporalBounds) {
+			if (containsTemporalBounds) {
+				// remove time bounds syntactically
+				ExpandStepBoundsSyntactically visitor = new ExpandStepBoundsSyntactically(constants);
+				ltl = (Expression)ltl.deepCopy().accept(visitor);
+
+				mainLog.println("LTL formula with syntactically expanded bounds: "+ltl);
+			}
+
 			if (useExternal) {
 				result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
 			} else {
@@ -137,6 +136,7 @@ public class LTL2DA extends PrismComponent
 				// don't use LTL2WDBA translation yet
 				boolean allowLTL2WDBA = false;
 				if (allowLTL2WDBA) {
+
 					LTLFragments fragments = LTLFragments.analyse(simpleLTL);
 					mainLog.println(fragments);
 
@@ -157,9 +157,6 @@ public class LTL2DA extends PrismComponent
 					result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
 				}
 			}
-			} else {
-				throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");
-			}
 		}
 
 		if (result == null) {

prism/src/automata/LTL2RabinLibrary.java

@@ -160,7 +160,7 @@ public class LTL2RabinLibrary
 		// handle simple until formula with time bounds
 		if (Expression.containsTemporalTimeBounds(ltl)) {
 			if (!ltl.isSimplePathFormula()) {
-				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+				return null;
 			}
 
 			ltl = Expression.convertSimplePathFormulaToCanonicalForm(ltl);

prism/src/explicit/LTLModelChecker.java

@@ -135,11 +135,6 @@ public class LTLModelChecker extends PrismComponent
 				// Only support temporal bounds for discrete time models
 				return false;
 			}
-			
-			if (!expr.isSimplePathFormula()) {
-				// Only support temporal bounds for simple path formulas
-				return false;
-			}
 		}
 
 		if (Expression.isHOA(expr))
@@ -239,10 +234,6 @@ public class LTLModelChecker extends PrismComponent
 			if (model.getModelType().continuousTime()) {
 				throw new PrismNotSupportedException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 
 		if (Expression.isHOA(expr)) {

prism/src/prism/LTLModelChecker.java

@@ -177,11 +177,6 @@ public class LTLModelChecker extends PrismComponent
 				// Only support temporal bounds for discrete time models
 				return false;
 			}
-			
-			if (!expr.isSimplePathFormula()) {
-				// Only support temporal bounds for simple path formulas
-				return false;
-			}
 		}
 
 		if (Expression.isHOA(expr)) {
@@ -326,10 +321,6 @@ public class LTLModelChecker extends PrismComponent
 			if (model.getModelType().continuousTime()) {
 				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 		
 		long time;

prism/src/prism/ProbModelChecker.java

@@ -1023,11 +1023,6 @@ public class ProbModelChecker extends NonProbModelChecker
 				JDD.Deref(statesOfInterest);
 				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				JDD.Deref(statesOfInterest);
-				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 
 		// Can't do "dfa" properties yet