From e0bd1c22cb4ebb7e08792783476270f49fc540ba Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Feb 2016 14:39:32 +0000 Subject: [PATCH] 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 | 15 ++++++++++----- prism/src/explicit/LTLModelChecker.java | 10 +--------- prism/src/prism/LTLModelChecker.java | 11 +---------- prism/src/prism/ProbModelChecker.java | 11 +---------- 4 files changed, 13 insertions(+), 34 deletions(-) diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java index 2792ed8a..c8f30ad8 100644 --- a/prism/src/automata/LTL2RabinLibrary.java +++ b/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"); } } diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 591355f7..11adf611 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/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); } } diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index f8552cce..58c2af6b 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/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); } } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index a6d3355a..3cebbe1c 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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); } }