Cleanup DA-based simple path formula with bounds handling

The routines in LTL2RabinLibrary for generating DA for
simple path formulas with time bounds have been adapted
to deal with negated labels. This makes the special
preprocessing for such formulas unnecessary and we remove it.


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

prism/src/automata/LTL2RabinLibrary.java

@@ -115,24 +115,29 @@ public class LTL2RabinLibrary
 		String draString = dras.get(ltl2.toString());
 		if (draString != null)
 			return createDRAFromString(draString, labels);
-		
-		
+
 		// handle simple until formula with time bounds
 		if (Expression.containsTemporalTimeBounds(ltl)) {
+			if (!ltl.isSimplePathFormula()) {
+				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+			}
+
+			ltl = Expression.convertSimplePathFormulaToCanonicalForm(ltl);
 			boolean negated = false;
-			
+
 			if (ltl instanceof ExpressionUnaryOp &&
 			    ((ExpressionUnaryOp)ltl).getOperator() == ExpressionUnaryOp.NOT) {
 				// negated
 				negated = true;
 				ltl = ((ExpressionUnaryOp)ltl).getOperand();
 			}
-			
+
 			if (ltl instanceof ExpressionTemporal &&
 			    ((ExpressionTemporal)ltl).getOperator() == ExpressionTemporal.P_U) {
 				return constructDRAForSimpleUntilFormula((ExpressionTemporal)ltl, constants, negated);				
 			} else {
-				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+				// should not be reached
+				throw new PrismException("Implementation error");
 			}
 		}
 		

prism/src/explicit/LTLModelChecker.java

@@ -226,15 +226,7 @@ public class LTLModelChecker extends PrismComponent
 				throw new PrismException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DA is then generated by LTL2RabinLibrary.
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}

prism/src/prism/LTLModelChecker.java

@@ -177,16 +177,7 @@ public class LTLModelChecker extends PrismComponent
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DRA is then generated by LTL2RabinLibrary.
-				//
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}

prism/src/prism/ProbModelChecker.java

@@ -880,16 +880,7 @@ public class ProbModelChecker extends NonProbModelChecker
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DA is then generated by LTL2RabinLibrary.
-				//
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}