BOperation.java

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 tlc2.tool.ToolGlobals;

import java.util.*;
import java.util.Map.Entry;
import java.util.stream.Collectors;

public class BOperation extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
	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 LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
	private List<OpDeclNode> anyVariables;
	private final SpecAnalyser specAnalyser;

	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()));

		evalParams();
		// System.out.println("Construction B Operation for TLA+ action: " + name);
		findUnchangedVariables();
		// System.out.println(" UNCHANGED = " + unchangedVariables.toString());
		separateGuardsAndBeforeAfterPredicates(node);
		findAssignments();
	}

	public AOperation getBOperation(BAstCreator bASTCreator) {
		bASTCreator.setUnchangedVariablesNames(unchangedVariables);
		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()));
		}
		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";