Skip to content

Commit 51f0d1c

Browse files
author
Steffen Märcker
committed
[DAG-copy] Adapt existing visitors to be DAG-aware
Rename the method visit to visitNow in existing visitor classes. This makes them traverse the AST without visiting nodes multiple times.
1 parent 75a6099 commit 51f0d1c

20 files changed

Lines changed: 45 additions & 45 deletions

prism/src/automata/LTL2RabinLibrary.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ public static DA<BitSet, AcceptanceRabin> getDRAforLTL(Expression ltl, Values co
132132
labels = new ArrayList<String>();
133133
ltl.accept(new ASTTraverse()
134134
{
135-
public Object visit(ExpressionLabel e) throws PrismLangException
135+
public Object visitNow(ExpressionLabel e) throws PrismLangException
136136
{
137137
labels.add(e.getName());
138138
return null;
@@ -144,7 +144,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException
144144
Expression ltl2 = ltl.deepCopy();
145145
ltl2.accept(new ASTTraverseModify()
146146
{
147-
public Object visit(ExpressionLabel e) throws PrismLangException
147+
public Object visitNow(ExpressionLabel e) throws PrismLangException
148148
{
149149
int i = labels.indexOf(e.getName());
150150
//char letter = (char) ('a' + i);

prism/src/parser/BooleanUtils.java

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -118,18 +118,18 @@ private static Expression removeImpliesIffAndParentheses(Expression expr)
118118
try {
119119
exprMod = (Expression) expr.accept(new ASTTraverseModify()
120120
{
121-
public Object visit(ExpressionUnaryOp e) throws PrismLangException
121+
public Object visitNow(ExpressionUnaryOp e) throws PrismLangException
122122
{
123123
// Remove parentheses: (a)
124124
if (Expression.isParenth(e)) {
125125
Expression a = (Expression) (e.getOperand().accept(this));
126126
// (a) == a
127127
return a;
128128
}
129-
return super.visit(e);
129+
return super.visitNow(e);
130130
}
131131

132-
public Object visit(ExpressionBinaryOp e) throws PrismLangException
132+
public Object visitNow(ExpressionBinaryOp e) throws PrismLangException
133133
{
134134
// Remove implication: a => b
135135
if (Expression.isImplies(e)) {
@@ -145,7 +145,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException
145145
// a <=> b == (a | !b) & (!a | b)
146146
return Expression.And(Expression.Or(a, Expression.Not(b)), Expression.Or(Expression.Not(a.deepCopy()), b.deepCopy()));
147147
}
148-
return super.visit(e);
148+
return super.visitNow(e);
149149
}
150150
});
151151
} catch (PrismLangException e) {

prism/src/parser/PrismParser.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ else if (args[0].equals("-expression") || args[0].equals("-e")) {
8080
else if (args[0].equals("-ltl") || args[0].equals("-l")) {
8181
Expression expr = p.parseSingleLTLFormula(str);
8282
expr = (Expression) expr.accept(new ASTTraverseModify() {
83-
public Object visit(ExpressionIdent e) throws PrismLangException
83+
public Object visitNow(ExpressionIdent e) throws PrismLangException
8484
{
8585
return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance());
8686
}
@@ -99,7 +99,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException
9999
System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf));
100100
}
101101
Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() {
102-
public Object visit(ExpressionVar e) throws PrismLangException
102+
public Object visitNow(ExpressionVar e) throws PrismLangException
103103
{
104104
return new parser.ast.ExpressionLabel(e.getName());
105105
}

prism/src/parser/visitor/EvaluatePartially.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ public EvaluatePartially(EvaluateContext ec)
4242
this.ec = ec;
4343
}
4444

45-
public Object visit(ExpressionConstant e) throws PrismLangException
45+
public Object visitNow(ExpressionConstant e) throws PrismLangException
4646
{
4747
Object val = ec.getConstantValue(e.getName());
4848
if (val == null) {
@@ -52,7 +52,7 @@ public Object visit(ExpressionConstant e) throws PrismLangException
5252
}
5353
}
5454

55-
public Object visit(ExpressionVar e) throws PrismLangException
55+
public Object visitNow(ExpressionVar e) throws PrismLangException
5656
{
5757
Object val = ec.getVarValue(e.getName(), e.getIndex());
5858
if (val == null) {

prism/src/parser/visitor/ExpandConstants.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ public ExpandConstants(ConstantList constantList)
4242
this.constantList = constantList;
4343
}
4444

45-
public Object visit(ExpressionConstant e) throws PrismLangException
45+
public Object visitNow(ExpressionConstant e) throws PrismLangException
4646
{
4747
int i;
4848
Type t;

prism/src/parser/visitor/ExpandFormulas.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ public ExpandFormulas(FormulaList formulaList, boolean replace)
4848
this.replace = replace;
4949
}
5050

51-
public Object visit(ExpressionFormula e) throws PrismLangException
51+
public Object visitNow(ExpressionFormula e) throws PrismLangException
5252
{
5353
int i;
5454
Type t;

prism/src/parser/visitor/ExpandLabels.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ public ExpandLabels(LabelList labelList)
4444
this.labelList = labelList;
4545
}
4646

47-
public Object visit(ExpressionLabel e) throws PrismLangException
47+
public Object visitNow(ExpressionLabel e) throws PrismLangException
4848
{
4949
int i;
5050
Type t;

prism/src/parser/visitor/ExpandPropRefsAndLabels.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ public ExpandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelLis
4949
this.labelList = labelList;
5050
}
5151

52-
public Object visit(ExpressionLabel e) throws PrismLangException
52+
public Object visitNow(ExpressionLabel e) throws PrismLangException
5353
{
5454
int i;
5555
Type t;
@@ -84,7 +84,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException
8484
return e;
8585
}
8686

87-
public Object visit(ExpressionProp e) throws PrismLangException
87+
public Object visitNow(ExpressionProp e) throws PrismLangException
8888
{
8989
Property prop;
9090
Type t;

prism/src/parser/visitor/ExpressionTraverseNonNested.java

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,9 @@
4242
* <br/>
4343
* Subclasses should not override<br/>
4444
* <ul>
45-
* <li>{@code visit(ExpressionProb)}</li>
46-
* <li>{@code visit(ExpressionReward)}</li>
47-
* <li>{@code visit(ExpressionSS)}</li>
45+
* <li>{@code visitNow(ExpressionProb)}</li>
46+
* <li>{@code visitNow(ExpressionReward)}</li>
47+
* <li>{@code visitNow(ExpressionSS)}</li>
4848
* </ul>
4949
*/
5050
public class ExpressionTraverseNonNested extends ASTTraverse
@@ -74,7 +74,7 @@ private boolean inLimit()
7474
}
7575

7676
@Override
77-
public Object visit(ExpressionProb e) throws PrismLangException
77+
public Object visitNow(ExpressionProb e) throws PrismLangException
7878
{
7979
currentNesting++;
8080
// only visit if we are still in limit
@@ -88,7 +88,7 @@ public Object visit(ExpressionProb e) throws PrismLangException
8888
}
8989

9090
@Override
91-
public Object visit(ExpressionReward e) throws PrismLangException
91+
public Object visitNow(ExpressionReward e) throws PrismLangException
9292
{
9393
currentNesting++;
9494
// only visit if we are still in limit
@@ -102,7 +102,7 @@ public Object visit(ExpressionReward e) throws PrismLangException
102102
}
103103

104104
@Override
105-
public Object visit(ExpressionSS e) throws PrismLangException
105+
public Object visitNow(ExpressionSS e) throws PrismLangException
106106
{
107107
currentNesting++;
108108
// only visit if we are still in limit

prism/src/parser/visitor/FindAllConstants.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ public FindAllConstants(ConstantList constantList)
4141
this.constantList = constantList;
4242
}
4343

44-
public Object visit(ExpressionIdent e) throws PrismLangException
44+
public Object visitNow(ExpressionIdent e) throws PrismLangException
4545
{
4646
int i;
4747
// See if identifier corresponds to a constant

0 commit comments

Comments
 (0)