[DAG-copy] Implement DAG-aware vistitors

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph.
Most often it is not required to visit a node of this DAG multiply times.
The new class DAGVisitor keeps track of the nodes already seen and visits each node only once.

Author: Steffen Märcker

prism/src/automata/LTL2RabinLibrary.java

@@ -132,7 +132,7 @@ public static DA<BitSet, AcceptanceRabin> getDRAforLTL(Expression ltl, Values co
 		labels = new ArrayList<String>();
 		ltl.accept(new ASTTraverse()
 		{
-			public Object visit(ExpressionLabel e) throws PrismLangException
+			public Object visitNow(ExpressionLabel e) throws PrismLangException
 			{
 				labels.add(e.getName());
 				return null;
@@ -144,7 +144,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException
 		Expression ltl2 = ltl.deepCopy();
 		ltl2.accept(new ASTTraverseModify()
 		{
-			public Object visit(ExpressionLabel e) throws PrismLangException
+			public Object visitNow(ExpressionLabel e) throws PrismLangException
 			{
 				int i = labels.indexOf(e.getName());
 				//char letter = (char) ('a' + i);

prism/src/parser/BooleanUtils.java

@@ -118,18 +118,18 @@ private static Expression removeImpliesIffAndParentheses(Expression expr)
 		try {
 			exprMod = (Expression) expr.accept(new ASTTraverseModify()
 			{
-				public Object visit(ExpressionUnaryOp e) throws PrismLangException
+				public Object visitNow(ExpressionUnaryOp e) throws PrismLangException
 				{
 					// Remove parentheses: (a)
 					if (Expression.isParenth(e)) {
 						Expression a = (Expression) (e.getOperand().accept(this));
 						// (a)  ==  a 
 						return a;
 					}
-					return super.visit(e);
+					return super.visitNow(e);
 				}
 
-				public Object visit(ExpressionBinaryOp e) throws PrismLangException
+				public Object visitNow(ExpressionBinaryOp e) throws PrismLangException
 				{
 					// Remove implication: a => b
 					if (Expression.isImplies(e)) {
@@ -145,7 +145,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException
 						// a <=> b  ==  (a | !b) & (!a | b) 
 						return Expression.And(Expression.Or(a, Expression.Not(b)), Expression.Or(Expression.Not(a.deepCopy()), b.deepCopy()));
 					}
-					return super.visit(e);
+					return super.visitNow(e);
 				}
 			});
 		} catch (PrismLangException e) {

prism/src/parser/PrismParser.java

@@ -80,7 +80,7 @@ else if (args[0].equals("-expression") || args[0].equals("-e")) {
                         else if (args[0].equals("-ltl") || args[0].equals("-l")) {
                                 Expression expr = p.parseSingleLTLFormula(str);
                                 expr = (Expression) expr.accept(new ASTTraverseModify() {
-                                        public Object visit(ExpressionIdent e) throws PrismLangException
+                                        public Object visitNow(ExpressionIdent e) throws PrismLangException
                                         {
                                                 return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance());
                                         }
@@ -99,7 +99,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException
                                         System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf));
                                 }
                                 Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() {
-                                        public Object visit(ExpressionVar e) throws PrismLangException
+                                        public Object visitNow(ExpressionVar e) throws PrismLangException
                                         {
                                                         return new parser.ast.ExpressionLabel(e.getName());
                                         }

prism/src/parser/ast/ASTElement.java

@@ -35,7 +35,7 @@
 
 // Abstract class for PRISM language AST elements
 
-public abstract class ASTElement
+public abstract class ASTElement implements Cloneable
 {
 	// Type - default to null (unknown)
 	protected Type type = null;

prism/src/parser/ast/Updates.java

@@ -148,6 +148,7 @@ public Command getParent()
 	/**
 	 * Visitor method.
 	 */
+	@Override
 	public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);