From d81ef64ff2b81e7bc021abaf736a7df7a3c12fa0 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 22 Dec 2013 00:08:21 +0000 Subject: [PATCH] Code refactoring (checking for LTL with time bounds). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7731 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 17 +------- prism/src/explicit/MDPModelChecker.java | 19 ++------- prism/src/parser/ast/Expression.java | 22 +++++++++++ prism/src/prism/NondetModelChecker.java | 49 +++--------------------- prism/src/prism/ProbModelChecker.java | 17 +------- 5 files changed, 35 insertions(+), 89 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 426a3351..699b7878 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -215,21 +215,8 @@ public class DTMCModelChecker extends ProbModelChecker long time; // Can't do LTL with time-bounded variants of the temporal operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for LTL properties"; - throw new PrismException(s); + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); } // For LTL model checking routines diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index dcdc9c3a..ce05ec6b 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -228,23 +228,10 @@ public class MDPModelChecker extends ProbModelChecker long time; // Can't do LTL with time-bounded variants of the temporal operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for LTL properties"; - throw new PrismException(s); + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); } - + // For LTL model checking routines mcLtl = new LTLModelChecker(this); diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 108f0d5e..773a253e 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -666,6 +666,28 @@ public abstract class Expression extends ASTElement return false; } + /** + * Test if an expression contains time bounds on temporal operators + */ + public static boolean containsTemporalTimeBounds(Expression expr) + { + try { + expr.accept(new ASTTraverse() + { + public void visitPre(ExpressionTemporal e) throws PrismLangException + { + if (e.getLowerBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + if (e.getUpperBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + } + }); + } catch (PrismLangException e) { + return true; + } + return false; + } + /** * Test if an expression contains a multi(...) property within */ diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 33a9bfe5..0218f695 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -679,32 +679,6 @@ public class NondetModelChecker extends NonProbModelChecker } } - /** - * This function throws an exception if the parameter expr contains - * a subexpression which is a time-bounded operator. - * @param expr A multi objective - * @throws PrismException - */ - private void ensureNoTimeBounded(ExpressionFunc expr) throws PrismException - { - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for multi-objective properties"; - throw new PrismException(s); - } - } - protected void addDummyFormula(NondetModel modelProduct, LTLModelChecker mcLtl, List targetDDs, OpsAndBoundsList opsAndBounds) throws PrismException { @@ -845,10 +819,12 @@ public class NondetModelChecker extends NonProbModelChecker List rewards = new ArrayList(numTargets); List rewardsIndex = new ArrayList(numTargets); - // No time-bounded variants of the temporal operators allowed for multi-objective (or LTL) + // Can't do LTL with time-bounded variants of the temporal operators // TODO removed since it is allowed for valiter. // TODO make sure it is treated correctly for all params - //ensureNoTimeBounded(expr); + /*if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); + }*/ ArrayList targetName = new ArrayList(); targetExprs = new ArrayList(numTargets); @@ -1500,21 +1476,8 @@ public class NondetModelChecker extends NonProbModelChecker long l; // Can't do LTL with time-bounded variants of the temporal operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for LTL properties"; - throw new PrismException(s); + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); } // Can't do "dfa" properties yet diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 6c2e501f..a12715f0 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -555,21 +555,8 @@ public class ProbModelChecker extends NonProbModelChecker long l; // Can't do LTL with time-bounded variants of the temporal operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for LTL properties"; - throw new PrismException(s); + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); } // For LTL model checking routines