refactor operation handling

src/main/java/de/tla2b/analysis/BOperation.java

@@ -2,109 +2,105 @@ package de.tla2b.analysis;
 
 import de.be4.classicalb.core.parser.node.*;
 import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.TLAType;
 import de.tla2bAst.BAstCreator;
 import tla2sany.semantic.*;
 import tlc2.tool.BuiltInOPs;
 
 import java.util.*;
-import java.util.Map.Entry;
 import java.util.stream.Collectors;
 
-public class BOperation extends BuiltInOPs implements TranslationGlobals {
+import static de.be4.classicalb.core.parser.util.ASTBuilder.createConjunction;
+import static de.be4.classicalb.core.parser.util.ASTBuilder.createIdentifier;
+import static de.tla2b.global.TranslationGlobals.SUBSTITUTE_PARAM;
+
+public class BOperation extends BuiltInOPs {
 	private final String name;
 	private final OpApplNode node;
 	private final List<OpApplNode> existQuans;
-	private List<String> opParams;
-	private List<FormalParamNode> formalParams;
-	private List<String> unchangedVariables;
-	private final List<OpDeclNode> unchangedVariablesList;
-	private final List<ExprOrOpArgNode> guards;
-	private final List<ExprOrOpArgNode> beforeAfterPredicates;
-	private final Map<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
-	private List<OpDeclNode> anyVariables;
-	private final SpecAnalyser specAnalyser;
+	private final List<FormalParamNode> formalParams = new ArrayList<>();
+	private final List<OpDeclNode> unchangedVariables = new ArrayList<>();
+	private final List<ExprOrOpArgNode> guards = new ArrayList<>();
+	private final List<ExprOrOpArgNode> beforeAfterPredicates = new ArrayList<>();
+	private final Map<OpDeclNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
+	private final List<OpDeclNode> anyVariables = new ArrayList<>();
 
 	public BOperation(String name, OpApplNode n, List<OpApplNode> existQuans, SpecAnalyser specAnalyser) {
 		this.name = name;
 		this.node = n;
 		this.existQuans = existQuans;
-		this.specAnalyser = specAnalyser;
-		this.unchangedVariablesList = new ArrayList<>();
-		this.guards = new ArrayList<>();
-		this.beforeAfterPredicates = new ArrayList<>();
-		anyVariables = new ArrayList<>(Arrays.asList(specAnalyser.getModuleNode().getVariableDecls()));
+		OpDeclNode[] variableDecls = specAnalyser.getModuleNode().getVariableDecls();
+		this.anyVariables.addAll(Arrays.asList(variableDecls));
 
-		evalParams();
-		// System.out.println("Construction B Operation for TLA+ action: " + name);
-		findUnchangedVariables();
+		// eval params
+		for (OpApplNode ex : existQuans) {
+			for (FormalParamNode[] param : ex.getBdedQuantSymbolLists()) { // (bounded exists)
+				formalParams.addAll(Arrays.asList(param));
+			}
+		}
+		// DebugUtils.printDebugMsg("Constructing B Operation for TLA+ action: " + name);
+		findUnchangedVariablesInSemanticNode(node);
 		// System.out.println(" UNCHANGED = " + unchangedVariables.toString());
 		separateGuardsAndBeforeAfterPredicates(node);
-		findAssignments();
+		findAssignments(variableDecls);
 	}
 
 	public AOperation getBOperation(BAstCreator bASTCreator) {
-		bASTCreator.setUnchangedVariablesNames(unchangedVariables);
+		bASTCreator.setUnchangedVariablesNames(this.getUnchangedVariables());
+
 		List<PPredicate> whereList = new ArrayList<>();
 		for (OpApplNode o : this.getExistQuans()) {
 			whereList.add(bASTCreator.visitBoundsOfLocalVariables(o));
 		}
-
 		for (ExprOrOpArgNode g : guards) {
 			whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(g));
 		}
 
-		List<PExpression> leftSideOfAssigment = new ArrayList<>();
-		List<PExpression> rightSideOfAssigment = new ArrayList<>();
-		for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
-			leftSideOfAssigment.add(bASTCreator.createIdentifierNode(entry.getKey()));
-			rightSideOfAssigment.add(bASTCreator.visitExprOrOpArgNodeExpression(entry.getValue()));
-		}
+		List<PExpression> lhsAssignment = new ArrayList<>();
+		List<PExpression> rhsAssignment = new ArrayList<>();
+		assignments.forEach((id, assignExpr) -> {
+			lhsAssignment.add(bASTCreator.createIdentifierNode(id));
+			rhsAssignment.add(bASTCreator.visitExprOrOpArgNodeExpression(assignExpr));
+		});
+
 		PSubstitution operationBody;
 		AAssignSubstitution assign = new AAssignSubstitution();
 		if (!anyVariables.isEmpty()) { // ANY x_n WHERE P THEN A END
 			List<PExpression> anyParams = new ArrayList<>();
 			for (OpDeclNode var : anyVariables) {
-				String nextName = var.getName().toString() + "_n";
-				anyParams.add(BAstCreator.createIdentifierNode(nextName));
-
-				whereList.add(new AMemberPredicate(
-						BAstCreator.createIdentifierNode(nextName),
-						((TLAType) var.getToolObject(TYPE_ID)).getBNode()
-				));
-				leftSideOfAssigment.add(bASTCreator.createIdentifierNode(var));
-				rightSideOfAssigment.add(BAstCreator.createIdentifierNode(nextName));
+				AIdentifierExpression nextName = createIdentifier(var.getName().toString() + "_n");
+				anyParams.add(nextName);
+				whereList.add(new AMemberPredicate(nextName.clone(), TypeChecker.getType(var).getBNode()));
+				lhsAssignment.add(bASTCreator.createIdentifierNode(var));
+				rhsAssignment.add(nextName.clone());
 			}
 			whereList.addAll(createBeforeAfterPredicates(bASTCreator));
-			operationBody = new AAnySubstitution(anyParams, bASTCreator.createConjunction(whereList), assign);
+			operationBody = new AAnySubstitution(anyParams, createConjunction(whereList), assign);
 		} else if (!whereList.isEmpty()) { // SELECT P THEN A END
 			whereList.addAll(createBeforeAfterPredicates(bASTCreator));
 			for (ExprOrOpArgNode e : beforeAfterPredicates) {
 				whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(e));
 			}
-			operationBody = new ASelectSubstitution(bASTCreator.createConjunction(whereList), assign, new ArrayList<>(), null);
+			operationBody = new ASelectSubstitution(createConjunction(whereList), assign, new ArrayList<>(), null);
 		} else { // BEGIN A END
 			operationBody = new ABlockSubstitution(assign);
 		}
 
-		if (!leftSideOfAssigment.isEmpty()) {
-			assign.setLhsExpression(leftSideOfAssigment);
-			assign.setRhsExpressions(rightSideOfAssigment);
+		if (!lhsAssignment.isEmpty()) {
+			assign.setLhsExpression(lhsAssignment);
+			assign.setRhsExpressions(rhsAssignment);
 		} else { // skip
 			assign.replaceBy(new ASkipSubstitution());
 		}
 
-		return new AOperation(
-				new ArrayList<>(),
+		return new AOperation(new LinkedList<>(),
 				bASTCreator.createPositionedTIdentifierLiteral(name, getNode()),
 				this.getFormalParams().stream().map(bASTCreator::createIdentifierNode).collect(Collectors.toList()),
 				operationBody
 		);
 	}
 
-	private ArrayList<PPredicate> createBeforeAfterPredicates(BAstCreator bAstCreator) {
-		ArrayList<PPredicate> predicates = new ArrayList<>();
+	private List<PPredicate> createBeforeAfterPredicates(BAstCreator bAstCreator) {
+		List<PPredicate> predicates = new ArrayList<>();
 		for (ExprOrOpArgNode e : beforeAfterPredicates) {
 			PPredicate body = null;
 			if (e instanceof OpApplNode) {
@@ -114,8 +110,7 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 					OpDefNode def = (OpDefNode) opApplNode.getOperator();
 					FormalParamNode[] params = def.getParams();
 					for (int j = 0; j < params.length; j++) {
-						FormalParamNode param = params[j];
-						param.setToolObject(SUBSTITUTE_PARAM, opApplNode.getArgs()[j]);
+						params[j].setToolObject(SUBSTITUTE_PARAM, opApplNode.getArgs()[j]);
 					}
 					body = bAstCreator.visitExprNodePredicate(def.getBody());
 				}
@@ -128,26 +123,24 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 		return predicates;
 	}
 
-	private void findAssignments() {
+	private void findAssignments(OpDeclNode[] variableDecls) {
 		PrimedVariablesFinder primedVariablesFinder = new PrimedVariablesFinder(beforeAfterPredicates);
 		for (ExprOrOpArgNode node : new ArrayList<>(beforeAfterPredicates)) {
 			if (node instanceof OpApplNode) {
 				OpApplNode opApplNode = (OpApplNode) node;
-				if (opApplNode.getOperator().getKind() == BuiltInKind) {
-
-					if (OPCODE_eq == getOpCode(opApplNode.getOperator().getName())) {
+				if (opApplNode.getOperator().getKind() == BuiltInKind
+						&& getOpCode(opApplNode.getOperator().getName()) == OPCODE_eq) {
 					ExprOrOpArgNode arg1 = opApplNode.getArgs()[0]; // we have equality arg1 = RHS
 					try {
-							OpApplNode arg11 = (OpApplNode) arg1;
-							if (getOpCode(arg11.getOperator().getName()) == OPCODE_prime) {
-								OpApplNode v = (OpApplNode) arg11.getArgs()[0];
-								SymbolNode var = v.getOperator();
+						OpApplNode primeAppl = (OpApplNode) arg1;
+						if (getOpCode(primeAppl.getOperator().getName()) == OPCODE_prime) {
+							OpDeclNode var = (OpDeclNode) ((OpApplNode) primeAppl.getArgs()[0]).getOperator(); // var is first arg of prime
 							// we have equality var' = RHS
 							if (!primedVariablesFinder.getTwiceUsedVariables().contains(var)) {
 								// var' is only used once in all before after predicates
 								// meaning we do not need it as parameter of the ANY
 								// and can add an assignment var := RHS
-									assignments.put(v.getOperator(), opApplNode.getArgs()[1]); // RHS of assignment
+								assignments.put(var, opApplNode.getArgs()[1]); // RHS of assignment
 								beforeAfterPredicates.remove(node);
 								// System.out.println("Detected assignment " + var.getName().toString() + "' = <RHS>");
 							}
@@ -155,18 +148,16 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 					} catch (ClassCastException e) {
 					}
 				}
-
-				}
 			}
 		}
-		anyVariables = new ArrayList<>();
-		Collections.addAll(anyVariables, specAnalyser.getModuleNode().getVariableDecls());
+		anyVariables.clear();
+		Collections.addAll(anyVariables, variableDecls);
 
 		// for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
 		// anyVariables.add((OpDeclNode) symbol);
 		// }
 		anyVariables.removeAll(assignments.keySet());
-		anyVariables.removeAll(unchangedVariablesList);
+		anyVariables.removeAll(unchangedVariables);
 	}
 
 	private void separateGuardsAndBeforeAfterPredicates(ExprOrOpArgNode node) {
@@ -174,132 +165,48 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 			OpApplNode opApplNode = (OpApplNode) node;
 			if (opApplNode.getOperator().getKind() == BuiltInKind) {
 				switch (getOpCode(opApplNode.getOperator().getName())) {
-					case OPCODE_land: // \land
-					{
-						separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[0]);
-						separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[1]);
-						return;
-					}
+					case OPCODE_land: // \land (getArgs has 2 args)
 					case OPCODE_cl: // $ConjList
-					{
-						for (int i = 0; i < opApplNode.getArgs().length; i++) {
-							separateGuardsAndBeforeAfterPredicates(opApplNode
-								.getArgs()[i]);
-						}
+						Arrays.stream(opApplNode.getArgs()).forEach(this::separateGuardsAndBeforeAfterPredicates);
 						return;
-					}
-					default: {
-						if (opApplNode.level < 2) {
-							guards.add(node); // should we be checking nonLeibnizParams is empty ?
-						} else {
-							beforeAfterPredicates.add(node);
-						}
+					default:
+						(opApplNode.level < 2 ? guards : beforeAfterPredicates).add(node);
+						// guards: should we check if nonLeibnizParams is empty?
 						return;
 				}
-
-				}
-			}
-		}
-		if (node.level < 2) {
-			guards.add(node);
-		} else {
-			beforeAfterPredicates.add(node);
-		}
-		// beforeAfterPredicates.add(node);
-	}
-
-	private void evalParams() {
-		opParams = new ArrayList<>();
-		formalParams = new ArrayList<>();
-		for (OpApplNode n : existQuans) {
-			FormalParamNode[][] params = n.getBdedQuantSymbolLists();
-			for (FormalParamNode[] param : params) {
-				for (FormalParamNode formalParamNode : param) {
-					formalParams.add(formalParamNode);
-					opParams.add(formalParamNode.getName().toString());
-				}
-			}
-		}
-	}
-
-	public SymbolNode getSymbolNode() {
-		if (node != null && node.getOperator().getKind() == UserDefinedOpKind) {
-			return node.getOperator();
-		}
-		return null;
-	}
-
-	public String getName() {
-		return name;
-	}
-
-	public ExprNode getNode() {
-		return node;
-	}
-
-	public List<OpApplNode> getExistQuans() {
-		return new ArrayList<>(existQuans);
-	}
-
-	public List<String> getOpParams() {
-		return opParams;
 			}
-
-	public List<FormalParamNode> getFormalParams() {
-		return formalParams;
 		}
-
-	public List<String> getUnchangedVariables() {
-		return unchangedVariables;
-	}
-
-	private void findUnchangedVariables() {
-		unchangedVariables = new ArrayList<>();
-		findUnchangedVariablesInSemanticNode(node);
+		(node.level < 2 ? guards : beforeAfterPredicates).add(node); // level = 2 means action predicate
 	}
 
 	private void findUnchangedVariablesInSemanticNode(SemanticNode node) {
 		switch (node.getKind()) {
-			case OpApplKind: {
+			case OpApplKind:
 				findUnchangedVariablesInOpApplNode((OpApplNode) node);
 				return;
-			}
-			case LetInKind: {
-				LetInNode letNode = (LetInNode) node;
-				findUnchangedVariablesInSemanticNode(letNode.getBody());
+			case LetInKind:
+				findUnchangedVariablesInSemanticNode(((LetInNode) node).getBody());
 				return;
-			}
-
-			case SubstInKind: {
-				SubstInNode substInNode = (SubstInNode) node;
-				findUnchangedVariablesInSemanticNode(substInNode.getBody());
-			}
+			case SubstInKind:
+				findUnchangedVariablesInSemanticNode(((SubstInNode) node).getBody());
 		}
 	}
 
 	private void findUnchangedVariablesInOpApplNode(OpApplNode n) {
-
 		int kind = n.getOperator().getKind();
 		if (kind == UserDefinedOpKind && !BBuiltInOPs.contains(n.getOperator().getName())) {
-			OpDefNode def = (OpDefNode) n.getOperator();
-			findUnchangedVariablesInSemanticNode(def.getBody());
+			findUnchangedVariablesInSemanticNode(((OpDefNode) n.getOperator()).getBody());
 		} else if (kind == BuiltInKind) {
-			int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
-			switch (opcode) {
+			switch (BuiltInOPs.getOpCode(n.getOperator().getName())) {
 				case OPCODE_land: // \land
-				case OPCODE_cl: { // $ConjList
-					for (int i = 0; i < n.getArgs().length; i++) {
-						findUnchangedVariablesInSemanticNode(n.getArgs()[i]);
-					}
+				case OPCODE_cl: // $ConjList
+					Arrays.stream(n.getArgs()).forEach(this::findUnchangedVariablesInSemanticNode);
 					return;
-				}
 				case OPCODE_unchanged: {
-					n.setToolObject(USED, false);
+					// n.setToolObject(USED, false); FIXME: this tool object is never used?
 					OpApplNode k = (OpApplNode) n.getArgs()[0];
 					if (k.getOperator().getKind() == VariableDeclKind) {
-						unchangedVariablesList.add((OpDeclNode) k.getOperator());
-						String name = k.getOperator().getName().toString();
-						unchangedVariables.add(name);
+						unchangedVariables.add((OpDeclNode) k.getOperator());
 					} else {
 						// Tuple
 						for (int i = 0; i < k.getArgs().length; i++) {
@@ -310,7 +217,7 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 								// we have a definition
 								OpDefNode def = (OpDefNode) var.getOperator();
 								if (def.getParams().length > 0) {
-									// we do not support definitions with arguments yet
+									// TODO: we do not support definitions with arguments yet
 									throw new RuntimeException("Declaration with parameters not supported for UNCHANGED: " + var.getOperator().getName() + " " + var.getLocation());
 								}
 								ExprNode body = def.getBody();
@@ -323,15 +230,44 @@ public class BOperation extends BuiltInOPs implements TranslationGlobals {
 							} else if (!(var.getOperator() instanceof OpDeclNode)) {
 								throw new RuntimeException("Cannot convert to list of UNCHANGED variables: " + var.getOperator().getName() + " " + var.getLocation());
 							} else {
-								unchangedVariablesList.add((OpDeclNode) var.getOperator());
-								String name = var.getOperator().getName().toString();
-								unchangedVariables.add(name);
+								unchangedVariables.add((OpDeclNode) var.getOperator());
+							}
 						}
 					}
 				}
 			}
 		}
 	}
+
+	public SymbolNode getSymbolNode() {
+		if (node != null && node.getOperator().getKind() == UserDefinedOpKind) {
+			return node.getOperator();
+		}
+		return null;
+	}
+
+	public String getName() {
+		return name;
+	}
+
+	public ExprNode getNode() {
+		return node;
+	}
+
+	public List<OpApplNode> getExistQuans() {
+		return new ArrayList<>(existQuans);
+	}
+
+	public List<String> getOpParams() {
+		return formalParams.stream().map(f -> f.getName().toString()).collect(Collectors.toList());
+	}
+
+	public List<FormalParamNode> getFormalParams() {
+		return formalParams;
+	}
+
+	public List<String> getUnchangedVariables() {
+		return unchangedVariables.stream().map(u -> u.getName().toString()).collect(Collectors.toList());
 	}
 }
 

src/main/java/de/tla2b/translation/OperationsFinder.java

@@ -22,6 +22,7 @@ public class OperationsFinder extends AbstractASTVisitor {
 	private List<OpApplNode> exists;
 	// a list containing all existential quantifier which will be parameters in the resulting B Machine
 	private final List<BOperation> bOperations;
+	private final List<String> generatedOperations = new ArrayList<>();
 
 	public OperationsFinder(SpecAnalyser specAnalyser) {
 		this.specAnalyser = specAnalyser;
@@ -55,7 +56,7 @@ public class OperationsFinder extends AbstractASTVisitor {
 	public void visitUserDefinedNode(OpApplNode n) {
 		OpDefNode def = (OpDefNode) n.getOperator();
 		if (BBuiltInOPs.contains(def.getName())) {
-			bOperations.add(new BOperation(def.getName().toString(), n, exists, specAnalyser));
+			addOperation(def.getName().toString(), n, exists, specAnalyser);
 			return;
 		}
 
@@ -73,32 +74,18 @@ public class OperationsFinder extends AbstractASTVisitor {
 		int opcode = BuiltInOPs.getOpCode(opname);
 		DebugUtils.printDebugMsg("OPCODE of " + opname + " = "+ opcode);
 		switch (opcode) {
-			case OPCODE_dl: { // DisjList: split action further
+			case OPCODE_dl: // DisjList: split action further
 				if (n.getArgs().length == 1) {
 					visitExprOrOpArgNode(n.getArgs()[0]);
 				} else {
-					String oldName = currentName;
-					List<OpApplNode> oldExists = new ArrayList<>(exists);
-
-					for (int i = 0; i < n.getArgs().length; i++) {
-						exists = new ArrayList<>(oldExists);
-						currentName = oldName + i;
-						visitExprOrOpArgNode(n.getArgs()[i]);
-					}
+					visitArgs(n);
 				}
 				return;
-			}
-			case OPCODE_lor: { // logical or: split action further
-				String oldName = currentName;
-				List<OpApplNode> oldExists = new ArrayList<>(exists);
 
-				for (int i = 0; i < n.getArgs().length; i++) {
-					exists = new ArrayList<>(oldExists);
-					currentName = oldName + i;
-					visitExprOrOpArgNode(n.getArgs()[i]);
-				}
+			case OPCODE_lor: // logical or: split action further
+				visitArgs(n);
 				return;
-			}
+
 			case OPCODE_be: { // BoundedExists
 				exists.add(n);
 				visitExprOrOpArgNode(n.getArgs()[0]);
@@ -119,24 +106,45 @@ public class OperationsFinder extends AbstractASTVisitor {
 			case OPCODE_in: // \in
 			case OPCODE_notin: // \notin
 			case OPCODE_subseteq: // \subseteq - subset or equal
-			case OPCODE_fa: // $FcnApply f[1]
+			case OPCODE_fa: // $FcnApply f[1] FIXME: how can FcnApply be an action?
 			case OPCODE_ite: // IF THEN ELSE
-			case OPCODE_case: {
+			case OPCODE_case: // CASE p1 -> e1 [] p2 -> e2
+			// TODO case OPCODE_aa: // <<A>>_e
+			// TODO case OPCODE_sa: // [A]_e
 				// no further decomposing: create a B operation
-				bOperations.add(new BOperation(currentName, n, exists, specAnalyser));
+				addOperation(currentName, n, exists, specAnalyser);
 				return;
 		}
-		}
-		//System.out.println("OPCODE of " + opname + " = "+ opcode);
 
 		if (opname == BBuildIns.OP_false || opname == BBuildIns.OP_true) {
 			// FALSE: always disabled; TRUE: CHAOS
-			bOperations.add(new BOperation(currentName, n, exists, specAnalyser));
+			addOperation(currentName, n, exists, specAnalyser);
 			return;
 		}
 		throw new RuntimeException(String.format("Expected an action at '%s':%n%s", opname, n.getLocation()));
 	}
 
+	private void visitArgs(OpApplNode n) {
+		String oldName = currentName;
+		List<OpApplNode> oldExists = new ArrayList<>(exists);
+
+		for (int i = 0; i < n.getArgs().length; i++) {
+			exists = new ArrayList<>(oldExists);
+			currentName = oldName + i;
+			visitExprOrOpArgNode(n.getArgs()[i]);
+		}
+	}
+
+	private void addOperation(String name, OpApplNode node, List<OpApplNode> exists, SpecAnalyser specAnalyser) {
+		if (!generatedOperations.contains(name)) {
+			bOperations.add(new BOperation(name, node, exists, specAnalyser));
+			generatedOperations.add(name);
+			return;
+		}
+		DebugUtils.printMsg("Duplicate operation not translated: " + name);
+		// TODO: handle fixed parameters of an action definition, e.g. Act1(2) /\ Act1(2)
+	}
+
 	public List<BOperation> getBOperations() {
 		return bOperations;
 	}