LTL2RabinLibrary and model checkers: support automata based constructions for temporal bounds for simple path formulas. Now, the constantValues from the model checker have to be passed to LTL2RabinLibrary to allow resolving constants in the bounds. [Joachim Klein]

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

prism/src/explicit/LTLModelChecker.java

@@ -41,6 +41,7 @@ import java.util.Vector;
 import acceptance.AcceptanceRabin;
 import common.IterableStateSet;
 import parser.State;
+import parser.Values;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionLabel;
@@ -103,10 +104,12 @@ public class LTLModelChecker extends PrismComponent
 	/**
 	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
 	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the LTL formula
+	 * @param constantValues values for constants in the formula
 	 */
-	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
+	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constantValues) throws PrismException
 	{
-		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl);
+		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constantValues);
 	}
 
 	/**
@@ -179,9 +182,23 @@ public class LTLModelChecker extends PrismComponent
 		LTLProduct<DTMC> product;
 		long time;
 
-		// Can't do LTL with time-bounded variants of the temporal operators
 		if (Expression.containsTemporalTimeBounds(expr)) {
-			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			if (dtmc.getModelType().continuousTime()) {
+				throw new PrismException("DRA construction for time-bounded operators not supported for " + dtmc.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 {
+				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			}
 		}
 
 		// Model check maximal state formulas
@@ -191,7 +208,7 @@ public class LTLModelChecker extends PrismComponent
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
-		dra = convertLTLFormulaToDRA(ltl);
+		dra = convertLTLFormulaToDRA(ltl, mc.getConstantValues());
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
 		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
@@ -352,10 +369,24 @@ public class LTLModelChecker extends PrismComponent
 		DA<BitSet,AcceptanceRabin> dra;
 		LTLProduct<MDP> product;
 		long time;
-		
-		// Can't do LTL with time-bounded variants of the temporal operators
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
-			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			if (model.getModelType().continuousTime()) {
+				throw new PrismException("DRA 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 {
+				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			}
 		}
 
 		// Model check maximal state formulas
@@ -365,7 +396,7 @@ public class LTLModelChecker extends PrismComponent
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
-		dra = convertLTLFormulaToDRA(ltl);
+		dra = convertLTLFormulaToDRA(ltl, mc.getConstantValues());
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
 		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");

prism/src/prism/LTL2RabinLibrary.java

@@ -33,6 +33,7 @@ import java.util.*;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceRabin.RabinPair;
 import jltl2dstar.*;
+import parser.Values;
 import parser.ast.*;
 import parser.visitor.ASTTraverse;
 import parser.visitor.ASTTraverseModify;
@@ -67,8 +68,10 @@ public class LTL2RabinLibrary
 	/**
 	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
 	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the LTL formula
+	 * @param constants values for constants in the formula (may be {@code null})
 	 */
-	public static DA<BitSet, AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
+	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException
 	{
 		// Get list of labels appearing
 		labels = new ArrayList<String>();
@@ -99,7 +102,27 @@ public class LTL2RabinLibrary
 		if (draString != null)
 			return createDRAFromString(draString, labels);
 		
-		// If none, convert using jltl2dstar library
+		
+		// handle simple until formula with time bounds
+		if (Expression.containsTemporalTimeBounds(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 PrismException("Unsupported LTL formula: "+ltl);
+			}
+		}
+		
+		// No time-bounded operators, convert using jltl2dstar library
 		return LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba());
 	}
 	
@@ -109,9 +132,10 @@ public class LTL2RabinLibrary
 	 * a and b are either ExpressionLabels or true/false.
 	 * The operator can have integer bounds.
 	 * @param expr the until formula
+	 * @param constants values for constants (in bounds)
 	 * @param negated create DRA for the complement, i.e., !(a U b)
 	 */
-	public static DA<BitSet,AcceptanceRabin> constructDRAForSimpleUntilFormula(ExpressionTemporal expr, boolean negated) throws PrismException
+	public static DA<BitSet,AcceptanceRabin> constructDRAForSimpleUntilFormula(ExpressionTemporal expr, Values constants, boolean negated) throws PrismException
 	{
 		IntegerBound bounds;
 		DA<BitSet,AcceptanceRabin> dra;
@@ -121,7 +145,7 @@ public class LTL2RabinLibrary
 		}
 
 		// get and check bounds information (non-negative, non-empty)
-		bounds = IntegerBound.fromExpressionTemporal(expr, true);
+		bounds = IntegerBound.fromExpressionTemporal(expr, constants, true);
 
 		// extract information about the operands of the until operator, either a label (extracted to labelA)
 		// or true/false (stored in aBoolean, labelA=null).
@@ -564,7 +588,7 @@ public class LTL2RabinLibrary
 			System.out.println(ltl.equals(expr.toString()));
 			DA<BitSet,AcceptanceRabin> dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
 			System.out.println(dra1);
-			DA<BitSet,AcceptanceRabin> dra2 = convertLTLFormulaToDRA(expr);
+			DA<BitSet,AcceptanceRabin> dra2 = convertLTLFormulaToDRA(expr, null);
 			System.out.println(dra2);
 			System.out.println(dra1.toString().equals(dra2.toString()));
 			//dra2.printDot(new PrintStream(new File("dra")));

prism/src/prism/LTLModelChecker.java

@@ -36,6 +36,7 @@ import acceptance.AcceptanceRabin;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import parser.Values;
 import parser.VarList;
 import parser.ast.Declaration;
 import parser.ast.DeclarationInt;
@@ -63,10 +64,12 @@ public class LTLModelChecker extends PrismComponent
 	/**
 	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
 	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the LTL formula
+	 * @param constants values for constants, may be {@code null}
 	 */
-	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
+	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException
 	{
-		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl);
+		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constants);
 	}
 
 	/**

prism/src/prism/MultiObjModelChecker.java

@@ -68,6 +68,9 @@ public class MultiObjModelChecker extends PrismComponent
 	protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DA<BitSet,AcceptanceRabin> dra[], Operator operator,
 			Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException
 	{
+
+		// TODO (JK): Adapt to support simple path formulas with bounds via DRA construction
+
 		// Model check maximal state formulas
 		Vector<JDDNode> labelDDs = new Vector<JDDNode>();
 		ltl = mcLtl.checkMaximalStateFormulas(modelChecker, model, targetExpr.deepCopy(), labelDDs);
@@ -79,7 +82,7 @@ public class MultiObjModelChecker extends PrismComponent
 			ltl = Expression.Not(Expression.Parenth(ltl));
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		long l = System.currentTimeMillis();
-		dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl);
+		dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues());
 		mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");

prism/src/prism/NondetModelChecker.java

@@ -35,7 +35,6 @@ import java.util.*;
 
 import acceptance.AcceptanceRabin;
 import odd.ODDUtils;
-
 import jdd.*;
 import dv.*;
 import explicit.MinMax;
@@ -949,9 +948,30 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// Can't do LTL with time-bounded variants of the temporal operators
+		// For min probabilities, need to negate the formula
+		// (But check fairness setting since this may affect min/max)
+		// (add parentheses to allow re-parsing if required)
+		if (min && !fairness) {
+			expr = Expression.Not(Expression.Parenth(expr));
+		}
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
-			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			if (model.getModelType().continuousTime()) {
+				throw new PrismException("DRA 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 {
+				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			}
 		}
 
 		// Can't do "dfa" properties yet
@@ -967,15 +987,9 @@ public class NondetModelChecker extends NonProbModelChecker
 		ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
 
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
-		// For min probabilities, need to negate the formula
-		// (But check fairness setting since this may affect min/max)
-		// (add parentheses to allow re-parsing if required)
-		if (min && !fairness) {
-			ltl = Expression.Not(Expression.Parenth(ltl));
-		}
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
-		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
+		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl, constantValues);
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");

prism/src/prism/ProbModelChecker.java

@@ -496,9 +496,23 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// Can't do LTL with time-bounded variants of the temporal operators
 		if (Expression.containsTemporalTimeBounds(expr)) {
-			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			if (model.getModelType().continuousTime()) {
+				throw new PrismException("DRA 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 {
+				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+			}
 		}
 
 		// For LTL model checking routines
@@ -511,7 +525,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
-		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
+		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl, constantValues);
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");