From 043c776914c1742c8aaad103c42ff90c99352f9d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 19 Nov 2015 16:34:28 +0000 Subject: [PATCH] Refactor ConvertForJltl2ba (fix regression due to custom equals/hashCode for ASTElements) In SVN 10565, custom equals/hashCode methods were introduced for the various ASTElements/Expressions, providing semantic equality. In the implementation of ConvertForJltl2ba, a Hashtable was used to store SimpleLTL formulas for the already handled Expression objects. With the new equals/hashCode, this can lead to SimpleLTL formulas that share subtrees, resulting in a DAG instead of a tree. The SimpleLTL.simplify() function behaves incorrectly for DAGs, e.g., for "! (X (s1=7)) | (X (X s1=7))", producing wrong output formulas. We refactor ConvertForJltl2ba to do a simple recursive transformation from Expression-based LTL to SimpleLTL. Optionally, sharing of identical subtrees can be enabled. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10894 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/Expression.java | 5 +- .../src/parser/visitor/ConvertForJltl2ba.java | 125 ++++++++++++++---- 2 files changed, 100 insertions(+), 30 deletions(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index fc69ebe8..1b61c050 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -158,9 +158,8 @@ public abstract class Expression extends ASTElement */ public jltl2ba.SimpleLTL convertForJltl2ba() throws PrismLangException { - ConvertForJltl2ba visitor = new ConvertForJltl2ba(); - accept(visitor); - return visitor.getFormula(this); + ConvertForJltl2ba converter = new ConvertForJltl2ba(); + return converter.convert(this); } /** diff --git a/prism/src/parser/visitor/ConvertForJltl2ba.java b/prism/src/parser/visitor/ConvertForJltl2ba.java index 5299f94d..7c667191 100644 --- a/prism/src/parser/visitor/ConvertForJltl2ba.java +++ b/prism/src/parser/visitor/ConvertForJltl2ba.java @@ -4,6 +4,7 @@ // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) // * Carlos S. Bederián (Universidad Nacional de Córdoba) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -27,41 +28,102 @@ package parser.visitor; -import java.util.Hashtable; +import java.util.HashMap; import parser.ast.*; import prism.PrismLangException; import jltl2ba.*; import parser.type.*; + /* * Convert a property expression (an LTL formula) into the classes used by * the jltl2ba (and jltl2dstar) libraries. + * + * Optionally, during this conversion, identical subtrees are shared, i.e., + * the resulting SimpleLTL structure is a directed acyclic graph (DAG) + * instead of a tree. This is controlled via the {@code allowSharing} flag. + * + * Note that, currently, the jltl2ba LTL to NBA translator requires that the + * SimpleLTL formula does not share subtrees. */ -public class ConvertForJltl2ba extends ASTTraverseModify +public class ConvertForJltl2ba { - private Hashtable formulas; + /** Flag: allow sharing (produce DAG instead of tree) */ + private boolean allowSharing = true; + /** Hash map to lookup already translated subformulas (if sharing is allowed) */ + private HashMap formulas = null; + /** Default constructor (don't allow sharing) */ public ConvertForJltl2ba() { - formulas = new Hashtable(); + this(false); + } + + /** + * Constructor + * @param allowSharing Flag: allow sharing (produce DAG instead of tree) + */ + public ConvertForJltl2ba(boolean allowSharing) + { + this.allowSharing = allowSharing; + if (allowSharing) { + formulas = new HashMap(); + } + } + + /** Convert expression to a SimpleLTL formula */ + public SimpleLTL convert(Expression e) throws PrismLangException + { + SimpleLTL res = null; + + if (allowSharing) { + // if sharing is allowed, lookup the expression and return + // a previously converted SimpleLTL if available + res = getFormula(e); + if (res != null) { + return res; + } + } + + // do the actual conversion + if (e instanceof ExpressionTemporal) { + res = convertTemporal((ExpressionTemporal)e); + } else if (e instanceof ExpressionBinaryOp) { + res = convertBinaryOp((ExpressionBinaryOp)e); + } else if (e instanceof ExpressionUnaryOp) { + res = convertUnaryOp((ExpressionUnaryOp)e); + } else if (e instanceof ExpressionLiteral) { + res = convertLiteral((ExpressionLiteral)e); + } else if (e instanceof ExpressionLabel) { + res = convertLabel((ExpressionLabel)e); + } + + if (allowSharing) { + // store converted formula if sharing is allowed + setFormula(e, res); + } + return res; } - public Object setFormula(ASTElement e, SimpleLTL formula) + /** Helper: store converted formula in hash map */ + private Object setFormula(ASTElement e, SimpleLTL formula) { return formulas.put(e, formula); } - public SimpleLTL getFormula(ASTElement e) + /** Helper: lookup formula in hash map */ + private SimpleLTL getFormula(ASTElement e) { return formulas.get(e); } - public void visitPost(ExpressionTemporal e) throws PrismLangException + /** Convert ExpressionTemporal to a SimpleLTL formula */ + private SimpleLTL convertTemporal(ExpressionTemporal e) throws PrismLangException { SimpleLTL ltl1 = null, ltl2 = null, res = null; Expression until; - if (e.getOperand1() != null) ltl1 = getFormula(e.getOperand1()); - if (e.getOperand2() != null) ltl2 = getFormula(e.getOperand2()); + if (e.getOperand1() != null) ltl1 = convert(e.getOperand1()); + if (e.getOperand2() != null) ltl2 = convert(e.getOperand2()); switch (e.getOperator()) { case ExpressionTemporal.P_X: res = new SimpleLTL(SimpleLTL.LTLType.NEXT, ltl2); @@ -78,20 +140,26 @@ public class ConvertForJltl2ba extends ASTTraverseModify case ExpressionTemporal.P_W: case ExpressionTemporal.P_R: until = e.convertToUntilForm(); - until.accept(this); - res = getFormula(until); + if (allowSharing) { + res = getFormula(until); + } + if (res == null) { + // convert normally + res = convert(until); + } break; default: throw new PrismLangException("Cannot convert expression to jltl2ba form", e); } - setFormula(e, res); + return res; } - - public void visitPost(ExpressionBinaryOp e) throws PrismLangException + + /** Convert ExpressionBinaryOp to a SimpleLTL formula */ + private SimpleLTL convertBinaryOp(ExpressionBinaryOp e) throws PrismLangException { SimpleLTL ltl1 = null, ltl2 = null, res = null; - if (e.getOperand1() != null) ltl1 = getFormula(e.getOperand1()); - if (e.getOperand2() != null) ltl2 = getFormula(e.getOperand2()); + if (e.getOperand1() != null) ltl1 = convert(e.getOperand1()); + if (e.getOperand2() != null) ltl2 = convert(e.getOperand2()); switch (e.getOperator()) { case ExpressionBinaryOp.IMPLIES: res = new SimpleLTL(SimpleLTL.LTLType.IMPLIES, ltl1, ltl2); @@ -108,13 +176,14 @@ public class ConvertForJltl2ba extends ASTTraverseModify default: throw new PrismLangException("Cannot convert expression to jltl2ba form", e); } - setFormula(e, res); + return res; } - - public void visitPost(ExpressionUnaryOp e) throws PrismLangException + + /** Convert ExpressionUnaryOp to a SimpleLTL formula */ + private SimpleLTL convertUnaryOp(ExpressionUnaryOp e) throws PrismLangException { SimpleLTL ltl1 = null, res = null; - if (e.getOperand() != null) ltl1 = getFormula(e.getOperand()); + if (e.getOperand() != null) ltl1 = convert(e.getOperand()); switch (e.getOperator()) { case ExpressionUnaryOp.NOT: res = new SimpleLTL(SimpleLTL.LTLType.NOT, ltl1); @@ -125,19 +194,21 @@ public class ConvertForJltl2ba extends ASTTraverseModify default: throw new PrismLangException("Cannot convert expression to jltl2ba form", e); } - setFormula(e, res); + return res; } - - public void visitPost(ExpressionLiteral e) throws PrismLangException + + /** Convert ExpressionLiteral to a SimpleLTL formula */ + private SimpleLTL convertLiteral(ExpressionLiteral e) throws PrismLangException { if (!(e.getType() instanceof TypeBool)) { throw new PrismLangException("Cannot convert expression to jltl2ba form", e); } - setFormula(e, new SimpleLTL(e.evaluateBoolean())); + return new SimpleLTL(e.evaluateBoolean()); } - - public void visitPost(ExpressionLabel e) throws PrismLangException + + /** Convert ExpressionLabel to a SimpleLTL formula */ + private SimpleLTL convertLabel(ExpressionLabel e) throws PrismLangException { - setFormula(e, new SimpleLTL(e.getName())); + return new SimpleLTL(e.getName()); } }