From 9ad8e8165e6f5db5ca5c56c993c56c8757666cf0 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 10:45:19 +0000 Subject: [PATCH] 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 | 49 ++++++++++++++++++----- prism/src/prism/LTL2RabinLibrary.java | 34 +++++++++++++--- prism/src/prism/LTLModelChecker.java | 7 +++- prism/src/prism/MultiObjModelChecker.java | 5 ++- prism/src/prism/NondetModelChecker.java | 34 +++++++++++----- prism/src/prism/ProbModelChecker.java | 20 +++++++-- 6 files changed, 119 insertions(+), 30 deletions(-) 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.");