diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index e765ae70..d828439d 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA 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 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 dra; LTLProduct 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."); diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/prism/LTL2RabinLibrary.java index cbbd9ddb..278ff961 100644 --- a/prism/src/prism/LTL2RabinLibrary.java +++ b/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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException { // Get list of labels appearing labels = new ArrayList(); @@ -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 constructDRAForSimpleUntilFormula(ExpressionTemporal expr, boolean negated) throws PrismException + public static DA constructDRAForSimpleUntilFormula(ExpressionTemporal expr, Values constants, boolean negated) throws PrismException { IntegerBound bounds; DA 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 dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba()); System.out.println(dra1); - DA dra2 = convertLTLFormulaToDRA(expr); + DA dra2 = convertLTLFormulaToDRA(expr, null); System.out.println(dra2); System.out.println(dra1.toString().equals(dra2.toString())); //dra2.printDot(new PrintStream(new File("dra"))); diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 7a84c324..adecc971 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException { - return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl); + return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constants); } /** diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 7177ea62..b3305e10 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/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 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 labelDDs = new Vector(); 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."); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index ab06ace4..491c8215 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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."); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index f8815838..49d5bbca 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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.");