Skip to content
Snippets Groups Projects
Select Git revision
  • d0dff197253673a11eb94eb65c7955fbe193ee80
  • master default protected
  • exec_auto_adjust_trace
  • let_variables
  • v1.4.1
  • v1.4.0
  • v1.3.0
  • v1.2.0
  • v1.1.0
  • v1.0.0
10 results

scheduler_large.mch

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    BAstCreator.java 86.33 KiB
    package de.tla2bAst;
    
    import de.be4.classicalb.core.parser.Definitions;
    import de.be4.classicalb.core.parser.node.*;
    import de.hhu.stups.sablecc.patch.PositionedNode;
    import de.hhu.stups.sablecc.patch.SourcePosition;
    import de.tla2b.analysis.*;
    import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
    import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
    import de.tla2b.config.ConfigfileEvaluator;
    import de.tla2b.config.ValueObj;
    import de.tla2b.exceptions.NotImplementedException;
    import de.tla2b.global.*;
    import de.tla2b.translation.BMacroHandler;
    import de.tla2b.translation.RecursiveFunctionHandler;
    import de.tla2b.types.*;
    import de.tla2b.util.DebugUtils;
    import tla2sany.semantic.*;
    import tla2sany.st.Location;
    import tlc2.tool.BuiltInOPs;
    import tlc2.value.ValueConstants;
    import tlc2.value.impl.*;
    
    import java.util.*;
    import java.util.Map.Entry;
    
    public class BAstCreator extends BuiltInOPs
    	implements TranslationGlobals, ASTConstants, BBuildIns, Priorities, ValueConstants {
    
    	List<PMachineClause> machineClauseList;
    	ConfigfileEvaluator conEval;
    	final SpecAnalyser specAnalyser;
    	private final PredicateVsExpression predicateVsExpression;
    	private final BMacroHandler bMacroHandler;
    	private final RecursiveFunctionHandler recursiveFunctionHandler;
    
    	private List<OpDeclNode> bConstants;
    
    	private final ModuleNode moduleNode;
    	private UsedExternalFunctions usedExternalFunctions;
    
    	private final Definitions bDefinitions = new Definitions();
    
    	private Start start;
    	private final Hashtable<Node, TLAType> typeTable = new Hashtable<>();
    	private final HashSet<PositionedNode> sourcePosition = new HashSet<>();
    	private List<String> toplevelUnchangedVariableNames = new ArrayList<>();
    
    	public Start expressionStart;
    
    	/**
    	 * Creates a B AST node for a TLA expression
    	 */
    	public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
    		this.moduleNode = moduleNode;
    		this.specAnalyser = specAnalyser;
    		this.bMacroHandler = new BMacroHandler();
    		this.predicateVsExpression = new PredicateVsExpression(moduleNode);
    		this.recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
    
    		ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1].getBody();
    		if (expressionIsAPredicate(expr)) {
    			APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
    			predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
    			expressionStart = new Start(predicateParseUnit, new EOF());
    		} else {
    			AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
    			expressionParseUnit.setExpression(visitExprNodeExpression(expr));
    			expressionStart = new Start(expressionParseUnit, new EOF());
    		}
    	}
    
    	private boolean expressionIsAPredicate(ExprNode expr) {
    		if (expr.getKind() == OpApplKind) {
    			OpApplNode opApplNode = (OpApplNode) expr;
    			int kind = opApplNode.getOperator().getKind();
    			if (kind == BuiltInKind) {
    				int opcode = getOpCode(opApplNode.getOperator().getName());
    				return OperatorTypes.tlaOperatorIsPredicate(opcode);
    			} else if (kind == UserDefinedOpKind && BBuiltInOPs.contains(opApplNode.getOperator().getName())) {
    				int opcode = BBuiltInOPs.getOpcode(opApplNode.getOperator().getName());
    				return OperatorTypes.bbuiltInOperatorIsPredicate(opcode);
    			}
    		} else if (expr.getKind() == LetInKind) {
    			LetInNode letInNode = (LetInNode) expr;
    			return expressionIsAPredicate(letInNode.getBody());
    		}
    		return false;
    	}
    
    	public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval, SpecAnalyser specAnalyser,
    	                   UsedExternalFunctions usedExternalFunctions, PredicateVsExpression predicateVsExpression,
    	                   BMacroHandler bMacroHandler, RecursiveFunctionHandler recursiveFunctionHandler) {
    		this.predicateVsExpression = predicateVsExpression;
    		this.bMacroHandler = bMacroHandler;
    		this.recursiveFunctionHandler = recursiveFunctionHandler;
    
    		this.conEval = conEval;
    		this.moduleNode = moduleNode;
    		this.specAnalyser = specAnalyser;
    		this.usedExternalFunctions = usedExternalFunctions;
    
    		if (conEval != null) {
    			this.bConstants = conEval.getbConstantList();
    		} else {
    			this.bConstants = Arrays.asList(moduleNode.getConstantDecls());
    		}
    
    		machineClauseList = new ArrayList<>();
    
    		AAbstractMachineParseUnit aAbstractMachineParseUnit = new AAbstractMachineParseUnit();
    		aAbstractMachineParseUnit.setVariant(new AMachineMachineVariant());
    		AMachineHeader machineHeader = new AMachineHeader();
    		List<TIdentifierLiteral> headerName = createTIdentifierLiteral(getName(moduleNode));
    		machineHeader.setName(headerName);
    		aAbstractMachineParseUnit.setHeader(machineHeader);
    
    		createSetsClause();
    		createDefinitionClause();
    		createAbstractConstantsClause();
    		createConstantsClause();
    		createPropertyClause();
    		createVariableClause();
    		createInvariantClause();
    		createInitClause();
    		createOperationsClause();
    
    		aAbstractMachineParseUnit.setMachineClauses(machineClauseList);
    		start = new Start(aAbstractMachineParseUnit, new EOF());
    
    	}
    
    	private void createSetsClause() {
    		if (conEval == null || conEval.getEnumerationSet() == null || conEval.getEnumerationSet().isEmpty())
    			return;
    		ASetsMachineClause setsClause = new ASetsMachineClause();
    
    		ArrayList<EnumType> printed = new ArrayList<>();
    		OpDeclNode[] cons = moduleNode.getConstantDecls();
    		for (OpDeclNode con : cons) {
    			TLAType type = (TLAType) con.getToolObject(TYPE_ID);
    
    			EnumType e = null;
    			if (type instanceof SetType) {
    				if (((SetType) type).getSubType() instanceof EnumType) {
    					e = (EnumType) ((SetType) type).getSubType();
    					if (!printed.contains(e)) {
    						printed.add(e);
    					}
    				}
    			} else if ((type instanceof EnumType)) {
    				e = (EnumType) type;
    				if (!printed.contains(e)) {
    					printed.add(e);
    				}
    			}
    		}
    
    		ArrayList<PSet> sets = new ArrayList<>();
    		for (int i = 0; i < printed.size(); i++) {
    			AEnumeratedSetSet eSet = new AEnumeratedSetSet();
    			printed.get(i).id = i + 1;
    			eSet.setIdentifier(createTIdentifierLiteral("ENUM" + (i + 1)));
    			List<PExpression> list = new ArrayList<>();
    			for (String s : printed.get(i).modelvalues) {
    				list.add(createIdentifierNode(s));
    			}
    			eSet.setElements(list);
    			sets.add(eSet);
    		}
    		setsClause.setSetDefinitions(sets);
    		machineClauseList.add(setsClause);
    
    	}
    
    	private void createDefinitionClause() {
    		ArrayList<OpDefNode> bDefs = new ArrayList<>();
    		for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
    			OpDefNode def = moduleNode.getOpDefs()[i];
    			if (specAnalyser.getBDefinitions().contains(def)) {
    				if (conEval != null && conEval.getConstantOverrideTable().containsValue(def)) {
    			        DebugUtils.printVeryVerboseMsg("Not creating B DEFINITION (in Override Table) " + def.getName() + " " + def);
    					continue;
    				}
    				if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
    					continue;
    				}
    			    //debugUtils.printVeryVerboseMsg("Creating B DEFINITION " + def.getName() + " " + def);
    
    				bDefs.add(def);
    			} else {
    			    DebugUtils.printVeryVerboseMsg("Not creating unused B DEFINITION for " + def.getName() + " " + def);
    			}
    
    		}
    
    		Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions.getUsedExternalFunctions();
    		List<PDefinition> defs = new ArrayList<>(createDefinitionsForExternalFunctions(set));
    
    		for (OpDefNode opDefNode : bDefs) {
    			List<PExpression> list = new ArrayList<>();
    			for (int i = 0; i < opDefNode.getParams().length; i++) {
    				FormalParamNode p = opDefNode.getParams()[i];
    				list.add(createIdentifierNode(p));
    			}
    			// TLAType type = (TLAType) opDefNode.getToolObject(TYPE_ID);
    			// if (opDefNode.level == 2 || type instanceof BoolType) {
    			if (predicateVsExpression.getDefinitionType(opDefNode) == DefinitionType.PREDICATE) {
    				APredicateDefinitionDefinition d = new APredicateDefinitionDefinition();
    				d.setName(new TDefLiteralPredicate(getName(opDefNode)));
    				d.setParameters(list);
    				d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
    				defs.add(createPositionedNode(d,opDefNode));
    			} else {
    				AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
    				d.setName(new TIdentifierLiteral(getName(opDefNode)));
    				// System.out.println("Creating Expression DEFINITION " + getName(opDefNode));
    				// TODO: these definitions have no position info in the definition_decl term nor at the top-level body
    
    				d.setParameters(list);
    				d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
    				defs.add(createPositionedNode(d,opDefNode));
    			}
    
    		}
    
    		if (!defs.isEmpty()) {
    			ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
    			defClause.setDefinitions(defs);
    			machineClauseList.add(defClause);
    
    			for (PDefinition def : defs) {
    				if (def instanceof AExpressionDefinitionDefinition) {
    					bDefinitions.addDefinition((AExpressionDefinitionDefinition) def, Definitions.Type.Expression);
    				} else if (def instanceof APredicateDefinitionDefinition) {
    					bDefinitions.addDefinition((APredicateDefinitionDefinition) def, Definitions.Type.Predicate);
    				} else {
    					bDefinitions.addDefinition((ASubstitutionDefinitionDefinition) def, Definitions.Type.Substitution);
    				}
    			}
    
    		}
    
    	}
    
    	private ArrayList<PDefinition> createDefinitionsForExternalFunctions(Set<EXTERNAL_FUNCTIONS> set) {
    		ArrayList<PDefinition> list = new ArrayList<>();
    
    		if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.CHOOSE)) {
    			AExpressionDefinitionDefinition def1 = new AExpressionDefinitionDefinition();
    			def1.setName(new TIdentifierLiteral("CHOOSE"));
    			def1.setParameters(createIdentifierList("X"));
    			def1.setRhs(new AStringExpression(new TStringLiteral("a member of X")));
    			list.add(def1);
    			AExpressionDefinitionDefinition def2 = new AExpressionDefinitionDefinition();
    			def2.setName(new TIdentifierLiteral("EXTERNAL_FUNCTION_CHOOSE"));
    			def2.setParameters(createIdentifierList("T"));
    			ATotalFunctionExpression total = new ATotalFunctionExpression();
    			total.setLeft(new APowSubsetExpression(createIdentifierNode("T")));
    			total.setRight(createIdentifierNode("T"));
    			def2.setRhs(total);
    			list.add(def2);
    		}
    		if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.ASSERT)) {
    			APredicateDefinitionDefinition def1 = new APredicateDefinitionDefinition();
    			def1.setName(new TDefLiteralPredicate("ASSERT_TRUE"));
    			ArrayList<PExpression> params = new ArrayList<>();
    			params.add(createIdentifierNode("P"));
    			params.add(createIdentifierNode("Msg"));
    			def1.setParameters(params);
    			def1.setRhs(new AEqualPredicate(new AIntegerExpression(new TIntegerLiteral("1")),
    				new AIntegerExpression(new TIntegerLiteral("1"))));
    			list.add(def1);
    
    			AExpressionDefinitionDefinition def2 = new AExpressionDefinitionDefinition();
    			def2.setName(new TIdentifierLiteral("EXTERNAL_PREDICATE_ASSERT_TRUE"));
    			def2.setParameters(new ArrayList<>());
    			AMultOrCartExpression cart = new AMultOrCartExpression();
    			cart.setLeft(new ABoolSetExpression());
    			cart.setRight(new AStringSetExpression());
    			def2.setRhs(cart);
    			list.add(def2);
    		}
    		return list;
    	}
    
    	private void createOperationsClause() {
    		ArrayList<BOperation> bOperations = specAnalyser.getBOperations();
    		if (bOperations == null || bOperations.isEmpty()) {
    			return;
    		}
    
    		List<POperation> opList = new ArrayList<>();
    		for (BOperation op : bOperations) {
    			opList.add(createPositionedNode(op.getBOperation(this), op.getNode()));
    		}
    
    		machineClauseList.add(new AOperationsMachineClause(opList));
    	}
    
    	private void createInitClause() {
    		OpDeclNode[] vars = moduleNode.getVariableDecls();
    		if (vars.length == 0)
    			return;
    		List<PExpression> varList = new ArrayList<>();
    		for (OpDeclNode var : vars) {
    			varList.add(createIdentifierNode(var));
    		}
    		ABecomesSuchSubstitution becomes = new ABecomesSuchSubstitution();
    		becomes.setIdentifiers(varList);
    
    		List<PPredicate> predList = new ArrayList<>();
    		for (ExprNode node : specAnalyser.getInits()) {
    			predList.add(visitExprNodePredicate(node));
    		}
    		if (predList.isEmpty()) {
    			throw new NotImplementedException("Could not find a definition of Init.");
    		}
    		becomes.setPredicate(createConjunction(predList));
    		AInitialisationMachineClause initClause = new AInitialisationMachineClause(becomes);
    		machineClauseList.add(initClause);
    	}
    
    	private void createVariableClause() {
    		List<OpDeclNode> bVariables = Arrays.asList(moduleNode.getVariableDecls());
    		if (!bVariables.isEmpty()) {
    			List<PExpression> list = new ArrayList<>();
    			for (OpDeclNode opDeclNode : bVariables) {
    
    				AIdentifierExpression id = createPositionedNode(
    					new AIdentifierExpression(createTIdentifierLiteral(getName(opDeclNode))), opDeclNode);
    				list.add(id);
    				TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
    				typeTable.put(id, type);
    			}
    			AVariablesMachineClause varClause = new AVariablesMachineClause(list);
    			machineClauseList.add(varClause);
    		}
    	}
    
    	private void createAbstractConstantsClause() {
    		List<PExpression> constantsList = new ArrayList<>();
    
    		for (RecursiveDefinition recDef : specAnalyser.getRecursiveDefinitions()) {
    			AIdentifierExpression id = createPositionedNode(
    				new AIdentifierExpression(createTIdentifierLiteral(getName(recDef.getOpDefNode()))),
    				recDef.getOpDefNode());
    			constantsList.add(id);
    			TLAType type = (TLAType) recDef.getOpDefNode().getToolObject(TYPE_ID);
    			typeTable.put(id, type);
    		}
    
    		for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
    			AIdentifierExpression id = new AIdentifierExpression(createTIdentifierLiteral(getName(recFunc)));
    			constantsList.add(id);
    			TLAType type = (TLAType) recFunc.getToolObject(TYPE_ID);
    			typeTable.put(id, type);
    		}
    
    		if (!constantsList.isEmpty()) {
    			AAbstractConstantsMachineClause abstractConstantsClause = new AAbstractConstantsMachineClause(
    				constantsList);
    			machineClauseList.add(abstractConstantsClause);
    		}
    	}
    
    	private void createConstantsClause() {
    		List<OpDeclNode> bConstants;
    		if (conEval != null) {
    			bConstants = conEval.getbConstantList();
    		} else {
    			bConstants = Arrays.asList(moduleNode.getConstantDecls());
    		}
    
    		List<PExpression> constantsList = new ArrayList<>();
    		for (OpDeclNode opDeclNode : bConstants) {
    			AIdentifierExpression id = createPositionedNode(
    				new AIdentifierExpression(createTIdentifierLiteral(getName(opDeclNode))), opDeclNode);
    			constantsList.add(id);
    			TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
    			typeTable.put(id, type);
    		}
    		if (!constantsList.isEmpty()) {
    			AConstantsMachineClause constantsClause = new AConstantsMachineClause(constantsList);
    			machineClauseList.add(constantsClause);
    		}
    	}
    
    	public AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
    		if (bMacroHandler.containsSymbolNode(symbolNode)) {
    			return createPositionedNode(createIdentifierNode(bMacroHandler.getNewName(symbolNode)), symbolNode);
    		} else {
    			return createPositionedNode(createIdentifierNode(symbolNode.getName().toString()), symbolNode);
    		}
    	}
    
    	private void createPropertyClause() {
    		List<PPredicate> propertiesList = new ArrayList<>();
    		propertiesList.addAll(evalRecursiveDefinitions());
    		propertiesList.addAll(evalRecursiveFunctions());
    		for (OpDeclNode con : bConstants) {
    			if (conEval != null && conEval.getConstantAssignments().containsKey(con) && bConstants.contains(con)) {
    				ValueObj v = conEval.getConstantAssignments().get(con);
    				TLAType t = v.getType();
    				boolean isEnum = false;
    				if (t instanceof SetType) {
    					TLAType sub = ((SetType) t).getSubType();
    					if (sub instanceof EnumType) {
    						EnumType en = (EnumType) sub;
    						SetEnumValue set = (SetEnumValue) v.getValue();
    						if (set.elems.size() == en.modelvalues.size()) {
    							isEnum = true;
    						}
    					}
    				}
    				AEqualPredicate equal = new AEqualPredicate();
    				if (isEnum) {
    					equal.setLeft(createIdentifierNode(con));
    					equal.setRight(createIdentifierNode(((SetType) t).getSubType().toString()));
    				} else {
    					equal.setLeft(createIdentifierNode(con));
    					Value tlcValue = v.getValue();
    					equal.setRight(createTLCValue(tlcValue));
    				}
    				propertiesList.add(equal);
    			} else {
    				AMemberPredicate member = new AMemberPredicate();
    				member.setLeft(createIdentifierNode(con));
    				TLAType t = (TLAType) con.getToolObject(TYPE_ID);
    				member.setRight(t.getBNode());
    				propertiesList.add(member);
    			}
    		}
    
    		if (conEval != null) {
    			for (Entry<OpDeclNode, OpDefNode> entry : conEval.getConstantOverrideTable().entrySet()) {
    				OpDeclNode con = entry.getKey();
    				OpDefNode generatedDef = entry.getValue();
    				OpDefNode def = null;
    				try {
    					OpApplNode opApplNode = (OpApplNode) generatedDef.getBody();
    					if (opApplNode.getKind() == UserDefinedOpKind) {
    						def = (OpDefNode) opApplNode.getOperator();
    					} else {
    						def = generatedDef;
    					}
    				} catch (ClassCastException e) {
    					def = generatedDef;
    				}
    
    				AEqualPredicate equal = new AEqualPredicate();
    				equal.setLeft(createIdentifierNode(con));
    				equal.setRight(visitExprNodeExpression(def.getBody()));
    				propertiesList.add(equal);
    			}
    		}
    
    		AssumeNode[] assumes = moduleNode.getAssumptions();
    		List<PPredicate> assertionList = new ArrayList<>();
    		for (AssumeNode assumeNode : assumes) {
    			ThmOrAssumpDefNode def = assumeNode.getDef();
    			if (def != null) {
    				ALabelPredicate aLabelPredicate = new ALabelPredicate(new TPragmaIdOrString(def.getName().toString()),
    					createPositionedNode(visitAssumeNode(assumeNode), assumeNode));
    				assertionList.add(aLabelPredicate);
    			} else {
    				propertiesList.add(visitAssumeNode(assumeNode));
    			}
    		}
    		if (!propertiesList.isEmpty()) {
    			APropertiesMachineClause propertiesClause = new APropertiesMachineClause();
    			propertiesClause.setPredicates(createConjunction(propertiesList));
    			machineClauseList.add(propertiesClause);
    		}
    		if (!assertionList.isEmpty()) {
    			AAssertionsMachineClause assertionClause = new AAssertionsMachineClause();
    			assertionClause.setPredicates(assertionList);
    			machineClauseList.add(assertionClause);
    		}
    
    	}
    
    	private List<PPredicate> evalRecursiveFunctions() {
    		List<PPredicate> propertiesList = new ArrayList<>();
    		for (OpDefNode def : specAnalyser.getRecursiveFunctions()) {
    			AEqualPredicate equals = new AEqualPredicate(createIdentifierNode(def),
    				visitExprNodeExpression(def.getBody()));
    			propertiesList.add(equals);
    		}
    		return propertiesList;
    	}
    
    	private List<PPredicate> evalRecursiveDefinitions() {
    		List<PPredicate> propertiesList = new ArrayList<>();
    
    		for (RecursiveDefinition recDef : specAnalyser.getRecursiveDefinitions()) {
    			OpDefNode def = recDef.getOpDefNode();
    			// TLAType t = (TLAType) def.getToolObject(TYPE_ID);
    			// OpApplNode ifThenElse = recDef.getIfThenElse();
    			FormalParamNode[] params = def.getParams();
    			ArrayList<PExpression> paramList1 = new ArrayList<>();
    			ArrayList<PPredicate> typeList = new ArrayList<>();
    			// ArrayList<PExpression> paramList2 = new ArrayList<PExpression>();
    			for (FormalParamNode p : params) {
    				paramList1.add(createIdentifierNode(p));
    				// paramList2.add(createIdentifierNode(p.getName().toString()));
    				TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
    				AEqualPredicate equal = new AEqualPredicate(createIdentifierNode(p), paramType.getBNode());
    				typeList.add(equal);
    			}
    			ALambdaExpression lambda1 = new ALambdaExpression();
    			lambda1.setIdentifiers(paramList1);
    			lambda1.setPredicate(createConjunction(typeList));
    			lambda1.setExpression(visitExprNodeExpression(def.getBody()));
    			// lambda1.setPredicate(visitExprOrOpArgNodePredicate(ifThenElse.getArgs()[0]));
    			// lambda1.setExpression(visitExprOrOpArgNodeExpression(ifThenElse.getArgs()[1]));
    
    			// ALambdaExpression lambda2 = new ALambdaExpression();
    			// lambda2.setIdentifiers(paramList2);
    			// ANegationPredicate not = new
    			// ANegationPredicate(visitExprOrOpArgNodePredicate(ifThenElse.getArgs()[0]));
    			// lambda2.setPredicate(not);
    			// lambda2.setExpression(visitExprOrOpArgNodeExpression(ifThenElse.getArgs()[2]));
    			// AUnionExpression union = new AUnionExpression(lambda1, lambda2);
    
    			AEqualPredicate equals = new AEqualPredicate(createIdentifierNode(def), lambda1);
    			propertiesList.add(equals);
    		}
    
    		return propertiesList;
    	}
    
    	private PExpression createTLCValue(Value tlcValue) {
    		switch (tlcValue.getKind()) {
    			case INTVALUE:
    				return new AIntegerExpression(new TIntegerLiteral(tlcValue.toString()));
    			case SETENUMVALUE: {
    				SetEnumValue s = (SetEnumValue) tlcValue;
    				ArrayList<PExpression> list = new ArrayList<>();
    				for (int i = 0; i < s.elems.size(); i++) {
    					Value v = s.elems.elementAt(i);
    					list.add(createTLCValue(v));
    				}
    				return new ASetExtensionExpression(list);
    			}
    			case MODELVALUE: {
    				ModelValue m = (ModelValue) tlcValue;
    				return createIdentifierNode(m.toString());
    			}
    			case STRINGVALUE: {
    				StringValue stringValue = (StringValue) tlcValue;
    				return new AStringExpression(new TStringLiteral(stringValue.getVal().toString()));
    			}
    			default:
    				throw new NotImplementedException("TLC value in configuration file: " + tlcValue.getClass());
    		}
    	}
    
    	private void createInvariantClause() {
    		OpDeclNode[] vars = moduleNode.getVariableDecls();
    
    		List<PPredicate> predList = new ArrayList<>();
    		for (OpDeclNode var : vars) {
    			TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
    
    			AMemberPredicate member = new AMemberPredicate();
    			member.setLeft(createIdentifierNode(var));
    			member.setRight(varType.getBNode());
    
    			predList.add(member);
    		}
    
    		for (OpDefNode def : specAnalyser.getInvariants()) {
    			if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
    				predList.add(visitExprNodePredicate(def.getBody()));
    			} else {
    				if (predicateVsExpression.getDefinitionType(def) == DefinitionType.PREDICATE) {
    					ADefinitionPredicate defPred = new ADefinitionPredicate();
    					defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
    					predList.add(defPred);
    				} else {
    					ADefinitionExpression defExpr = new ADefinitionExpression();
    					defExpr.setDefLiteral(new TIdentifierLiteral(getName(def)));
    					predList.add(new AEqualPredicate(defExpr, new ABooleanTrueExpression()));
    				}
    
    			}
    		}
    
    		if (!predList.isEmpty()) {
    			AInvariantMachineClause invClause = new AInvariantMachineClause(createConjunction(predList));
    			machineClauseList.add(invClause);
    		}
    
    	}
    
    	private PPredicate visitAssumeNode(AssumeNode assumeNode) {
    		return visitExprNodePredicate(assumeNode.getAssume());
    	}
    
    	public PPredicate visitExprNodePredicate(ExprNode exprNode) {
    		switch (exprNode.getKind()) {
    			case OpApplKind:
    				return visitOpApplNodePredicate((OpApplNode) exprNode);
    			case LetInKind: {
    				LetInNode letInNode = (LetInNode) exprNode;
    				return visitExprNodePredicate(letInNode.getBody());
    			}
    			case NumeralKind:
    			case DecimalKind: {
    				throw new RuntimeException();
    			}
    			default:
    				throw new NotImplementedException(exprNode.getClass().toString());
    		}
    
    	}
    
    	private PExpression visitExprNodeExpression(ExprNode exprNode) {
    		switch (exprNode.getKind()) {
    			case OpApplKind:
    				return visitOpApplNodeExpression((OpApplNode) exprNode);
    			case NumeralKind: {
    				String number = String.valueOf(((NumeralNode) exprNode).val());
    				return createPositionedNode(new AIntegerExpression(new TIntegerLiteral(number)), exprNode);
    			}
    			case DecimalKind: {
    				return createPositionedNode(new ARealExpression(new TRealLiteral(exprNode.toString())), exprNode);
    			}
    			case StringKind: {
    				StringNode s = (StringNode) exprNode;
    				return createPositionedNode(new AStringExpression(new TStringLiteral(s.getRep().toString())), exprNode);
    			}
    			case AtNodeKind: { // @
    				AtNode at = (AtNode) exprNode;
    				TLAType type = (TLAType) at.getExceptRef().getToolObject(TYPE_ID);
    				OpApplNode seq = at.getAtModifier();
    				LinkedList<ExprOrOpArgNode> list = new LinkedList<>(Arrays.asList(seq.getArgs()));
    				// PExpression base = visitExprNodeExpression(at.getAtBase());
    				PExpression base = (PExpression) at.getExceptComponentRef().getToolObject(EXCEPT_BASE);
    				return evalAtNode(list, type, base.clone());
    			}
    			case LetInKind: {
    				LetInNode letInNode = (LetInNode) exprNode;
    				return visitExprNodeExpression(letInNode.getBody());
    			}
    			default:
    				throw new NotImplementedException(exprNode.getClass().toString());
    		}
    
    	}
    
    	private PExpression evalAtNode(LinkedList<ExprOrOpArgNode> list, TLAType type, PExpression base) {
    		if (list.isEmpty()) {
    			return base;
    		}
    		if (type instanceof FunctionType) {
    			FunctionType funcType = (FunctionType) type;
    			PExpression param = visitExprOrOpArgNodeExpression(list.poll());
    			List<PExpression> params = new ArrayList<>();
    			params.add(param);
    			AFunctionExpression funCall = new AFunctionExpression();
    			funCall.setIdentifier(base);
    			funCall.setParameters(params);
    			return evalAtNode(list, funcType.getRange(), funCall);
    		} else {
    			StructType structType = (StructType) type;
    			ARecordFieldExpression select = new ARecordFieldExpression();
    			select.setRecord(base);
    			StringNode stringNode = (StringNode) list.poll();
    			// TODO rename field name
    			String fieldName = stringNode.getRep().toString();
    			select.setIdentifier(createIdentifierNode(fieldName));
    			return evalAtNode(list, structType.getType(fieldName), select);
    		}
    	}
    
    	private PPredicate visitOpApplNodePredicate(OpApplNode opApplNode) {
    		switch (opApplNode.getOperator().getKind()) {
    			case VariableDeclKind:
    			case ConstantDeclKind:
    			case FormalParamKind: {
    				return createPositionedNode(
    					new AEqualPredicate(createIdentifierNode(opApplNode.getOperator()), new ABooleanTrueExpression()),
    					opApplNode);
    			}
    			case BuiltInKind:
    				return visitBuiltInKindPredicate(opApplNode);
    
    			case UserDefinedOpKind: {
    				return visitUserdefinedOpPredicate(opApplNode);
    			}
    			default:
    				throw new NotImplementedException(opApplNode.getClass().toString());
    		}
    
    	}
    
    	private PExpression visitOpApplNodeExpression(OpApplNode n) {
    		switch (n.getOperator().getKind()) {
    			case ConstantDeclKind:
    			case VariableDeclKind: {
    				return createIdentifierNode(n.getOperator());
    			}
    			case FormalParamKind: {
    				FormalParamNode param = (FormalParamNode) n.getOperator();
    				ExprOrOpArgNode e = (ExprOrOpArgNode) param.getToolObject(SUBSTITUTE_PARAM);
    				if (e != null) {
    					return visitExprOrOpArgNodeExpression(e);
    				}
    
    				if (recursiveFunctionHandler.isRecursiveFunction(param)) {
    					ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(param);
    					if (!list.isEmpty()) {
    						AFunctionExpression call = new AFunctionExpression();
    						call.setIdentifier(createIdentifierNode(param));
    						ArrayList<PExpression> params = new ArrayList<>();
    						for (SymbolNode symbolNode : list) {
    							params.add(createIdentifierNode(symbolNode));
    						}
    						call.setParameters(params);
    						return call;
    					}
    				}
    				FormalParamNode[] tuple = (FormalParamNode[]) param.getToolObject(TUPLE);
    				if (tuple != null) {
    					if (tuple.length == 1) {
    						AFunctionExpression functionCall = new AFunctionExpression();
    						functionCall.setIdentifier(createIdentifierNode(n.getOperator()));
    						List<PExpression> paramList = new ArrayList<>();
    						paramList.add(new AIntegerExpression(new TIntegerLiteral("1")));
    						functionCall.setParameters(paramList);
    						return functionCall;
    					} else {
    
    						StringBuilder sb = new StringBuilder();
    						List<TLAType> typeList = new ArrayList<>();
    						int number = -1;
    						for (int j = 0; j < tuple.length; j++) {
    							FormalParamNode p = tuple[j];
    							sb.append(p.getName().toString());
    							TLAType type = (TLAType) p.getToolObject(TYPE_ID);
    							typeList.add(type);
    							if (p == param) {
    								number = j + 1;
    							}
    						}
    						TupleType tupleType = new TupleType(typeList);
    						PExpression id = createIdentifierNode(sb.toString());
    						return createProjectionFunction(id, number, tupleType);
    					}
    				}
    				return createIdentifierNode(n.getOperator());
    			}
    			case BuiltInKind:
    				return visitBuiltInKindExpression(n);
    
    			case UserDefinedOpKind: {
    				return visitUserdefinedOpExpression(n);
    			}
    			default:
    				throw new NotImplementedException(n.getOperator().getName().toString());
    		}
    	}
    
    	private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
    		OpDefNode def = (OpDefNode) n.getOperator();
    		if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in
    			// operator
    			&& STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
    			return visitBBuiltInsPredicate(n);
    		}
    		if (specAnalyser.getRecursiveFunctions().contains(def)) {
    			return new AEqualPredicate(createIdentifierNode(def), new ABooleanTrueExpression());
    		}
    		if (Arrays.asList(moduleNode.getOpDefs()).contains(def)) {
    			List<PExpression> params = new ArrayList<>();
    			for (int i = 0; i < n.getArgs().length; i++) {
    				params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
    			}
    			if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) {
    				ADefinitionExpression defCall = new ADefinitionExpression();
    				defCall.setDefLiteral(new TIdentifierLiteral(getName(def)));
    				defCall.setParameters(params);
    				return new AEqualPredicate(defCall, new ABooleanTrueExpression());
    			} else {
    				ADefinitionPredicate defCall = new ADefinitionPredicate();
    				defCall.setDefLiteral(new TDefLiteralPredicate(getName(def)));
    				defCall.setParameters(params);
    				return defCall;
    			}
    		} else {
    			FormalParamNode[] params = def.getParams();
    			for (int i = 0; i < params.length; i++) {
    				FormalParamNode param = params[i];
    				param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
    			}
    			return visitExprNodePredicate(def.getBody());
    		}
    	}
    
    	private String getName(SymbolNode def) {
    		return def.getName().toString();
    	}
    
    	private PExpression visitUserdefinedOpExpression(OpApplNode n) {
    		OpDefNode def = (OpDefNode) n.getOperator();
    		// Operator is a B built-in operator
    		if (BBuiltInOPs.contains(def.getName())
    			&& STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
    			return visitBBuiltInsExpression(n);
    		}
    
    		if (specAnalyser.getRecursiveFunctions().contains(def)) {
    			ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
    			if (!list.isEmpty()) {
    				AFunctionExpression call = new AFunctionExpression();
    				call.setIdentifier(createIdentifierNode(def));
    				ArrayList<PExpression> params = new ArrayList<>();
    				for (SymbolNode symbolNode : list) {
    					params.add(createIdentifierNode(symbolNode));
    				}
    				call.setParameters(params);
    				return call;
    			} else {
    				return createIdentifierNode(def);
    			}
    		}
    
    		if (Arrays.asList(moduleNode.getOpDefs()).contains(def)) {
    			List<PExpression> params = new ArrayList<>();
    			for (int i = 0; i < n.getArgs().length; i++) {
    				params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
    			}
    
    			if (conEval != null && conEval.getConstantOverrideTable().containsValue(def)) {
    				// used constants name instead of the definition overriding the
    				// constant
    				Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval.getConstantOverrideTable().entrySet().iterator();
    				String name = null;
    				while (iter.hasNext()) {
    					Entry<OpDeclNode, OpDefNode> entry = iter.next();
    					if (entry.getValue().equals(def)) {
    						name = getName(entry.getKey());
    					}
    				}
    				if (params.isEmpty()) {
    					return createIdentifierNode(name);
    				} else {
    					AFunctionExpression funcCall = new AFunctionExpression();
    					funcCall.setIdentifier(createIdentifierNode(name));
    					funcCall.setParameters(params);
    					return funcCall;
    				}
    			} else {
    				if (predicateVsExpression.getDefinitionType(def) == DefinitionType.PREDICATE) {
    					ADefinitionPredicate defPred = new ADefinitionPredicate();
    					defPred.setDefLiteral(new TDefLiteralPredicate(getName(n.getOperator())));
    					defPred.setParameters(params);
    					return new AConvertBoolExpression(defPred);
    				} else {
    					ADefinitionExpression defExpr = new ADefinitionExpression();
    					defExpr.setDefLiteral(new TIdentifierLiteral(getName(n.getOperator())));
    					defExpr.setParameters(params);
    					return defExpr;
    				}
    			}
    
    		} else {
    			FormalParamNode[] params = def.getParams();
    			for (int i = 0; i < params.length; i++) {
    				FormalParamNode param = params[i];
    				param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
    			}
    			return visitExprNodeExpression(def.getBody());
    		}
    
    	}
    
    	private PPredicate visitBBuiltInsPredicate(OpApplNode opApplNode) {
    		PPredicate returnNode = null;
    		switch (BBuiltInOPs.getOpcode(opApplNode.getOperator().getName())) {
    			case B_OPCODE_lt: // <
    				returnNode = new ALessPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_gt: // >
    				returnNode = new AGreaterPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_leq: // <=
    				returnNode = new ALessEqualPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_geq: // >=
    				returnNode = new AGreaterEqualPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_finite: // IsFiniteSet({1,2,3})
    			{
    				AMemberPredicate member = new AMemberPredicate();
    				member.setLeft(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				member.setRight(new AFinSubsetExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0])));
    				returnNode = member;
    				break;
    			}
    			case B_OPCODE_true: // TRUE
    				returnNode = new AEqualPredicate(new ABooleanTrueExpression(), new ABooleanTrueExpression());
    				break;
    
    			case B_OPCODE_false: // FALSE
    				returnNode = new AEqualPredicate(new ABooleanFalseExpression(), new ABooleanTrueExpression());
    				break;
    
    			case B_OPCODE_assert: {
    				ADefinitionPredicate pred = new ADefinitionPredicate();
    				pred.setDefLiteral(new TDefLiteralPredicate("ASSERT_TRUE"));
    				ArrayList<PExpression> list = new ArrayList<>();
    				list.add(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				if (opApplNode.getArgs()[1] instanceof StringNode) {
    					StringNode stringNode = (StringNode) opApplNode.getArgs()[1];
    					list.add(new AStringExpression(new TStringLiteral(stringNode.getRep().toString())));
    				} else {
    					list.add(new AStringExpression(new TStringLiteral("Error")));
    				}
    				pred.setParameters(list);
    				returnNode = pred;
    				break;
    			}
    		}
    		if (returnNode != null) {
    			return createPositionedNode(returnNode, opApplNode);
    		} else {
    			throw new RuntimeException("Unexpected operator: " + opApplNode.getOperator().getName().toString() + "\n"
    				+ opApplNode.stn.getLocation());
    		}
    	}
    
    	private PExpression visitBBuiltInsExpression(OpApplNode opApplNode) {
    		PExpression returnNode = null;
    		switch (BBuiltInOPs.getOpcode(opApplNode.getOperator().getName())) {
    			case B_OPCODE_bool: // BOOLEAN
    				returnNode = new ABoolSetExpression();
    				break;
    			case B_OPCODE_true: // TRUE
    				returnNode = new ABooleanTrueExpression();
    				break;
    			case B_OPCODE_false: // FALSE
    				returnNode = new ABooleanFalseExpression();
    				break;
    
    			/*
    			 * Standard Module Naturals
    			 */
    			case B_OPCODE_nat: // Nat
    				returnNode = new ANaturalSetExpression();
    				break;
    
    			case B_OPCODE_plus: // +
    				returnNode = new AAddExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_minus: // -
    				returnNode = new AMinusOrSetSubtractExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_times: // *
    				returnNode = new AMultOrCartExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_exp: // x^y
    				returnNode = new APowerOfExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_lt: // <
    				returnNode = new AConvertBoolExpression(
    					new ALessPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    						visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1])));
    				break;
    
    			case B_OPCODE_gt: // >
    				returnNode = new AConvertBoolExpression(
    					new AGreaterPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    						visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1])));
    				break;
    			case B_OPCODE_leq: // <=
    				returnNode = new AConvertBoolExpression(
    					new ALessEqualPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    						visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1])));
    				break;
    
    			case B_OPCODE_geq: // >=
    				returnNode = new AConvertBoolExpression(
    					new AGreaterEqualPredicate(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    						visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1])));
    				break;
    
    			case B_OPCODE_mod: // modulo a % b = a - b* (a/b)
    			{
    				PExpression a = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]);
    				PExpression b = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]);
    				PExpression a2 = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]);
    				PExpression b2 = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]);
    
    				AFlooredDivExpression div = new AFlooredDivExpression(a, b);
    				AMultOrCartExpression mult = new AMultOrCartExpression(b2, div);
    				returnNode = new AMinusOrSetSubtractExpression(a2, mult);
    				break;
    			}
    
    			case B_OPCODE_div: // \div
    				AFlooredDivExpression aFlooredDivExpression = new AFlooredDivExpression(
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    
    				setPosition(aFlooredDivExpression, opApplNode);
    				returnNode = aFlooredDivExpression;
    				break;
    
    			case B_OPCODE_realdiv: // /
    				ADivExpression aDivExpression = new ADivExpression(
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    
    				setPosition(aDivExpression, opApplNode);
    				returnNode = aDivExpression;
    				break;
    
    			case B_OPCODE_dotdot: // ..
    				returnNode = new AIntervalExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_int: // Int
    				returnNode = new AIntegerSetExpression();
    				break;
    
    			case B_OPCODE_real: // Real
    				returnNode = new ARealSetExpression();
    				break;
    
    			case B_OPCODE_uminus: // -x
    				returnNode = new AUnaryMinusExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_card: // Cardinality
    				returnNode = new ACardExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_finite: // IsFiniteSet({1,2,3})
    			{
    				AMemberPredicate member = new AMemberPredicate();
    				member.setLeft(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				member.setRight(new AFinSubsetExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0])));
    				returnNode = new AConvertBoolExpression(member);
    				break;
    			}
    
    			case B_OPCODE_string: // STRING
    				returnNode = new AStringSetExpression();
    				break;
    			/*
    			 * Standard Module Sequences
    			 */
    
    			case B_OPCODE_seq: // Seq(S) - set of sequences
    				returnNode = new ASeqExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_len: // length of the sequence
    				returnNode = new ASizeExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_conc: // s \o s2 - concatenation of s and s2
    				returnNode = new AConcatExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_append: // Append(s,x)
    				returnNode = new AInsertTailExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				break;
    
    			case B_OPCODE_head: // Head(s)
    				returnNode = new AFirstExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_tail: // Tail(s)
    				returnNode = new ATailExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				break;
    
    			case B_OPCODE_subseq: { // SubSeq(s,a,b)
    				// %p.(p : 1..(b-a+1)| s(p+a-1))
    				ALambdaExpression lambda = new ALambdaExpression();
    				lambda.setIdentifiers(createIdentifierList("t_"));
    				AMemberPredicate member = new AMemberPredicate();
    				member.setLeft(createIdentifierNode("t_"));
    				AIntervalExpression interval = new AIntervalExpression();
    				interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral("1")));
    				AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression();
    				minus.setLeft(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[2]));
    				minus.setRight(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				AAddExpression add = new AAddExpression();
    				add.setLeft(minus);
    				add.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
    				interval.setRightBorder(add);
    				member.setRight(interval);
    				lambda.setPredicate(member);
    				AAddExpression add2 = new AAddExpression();
    				add2.setLeft(createIdentifierNode("t_"));
    				add2.setRight(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
    				AMinusOrSetSubtractExpression minus2 = new AMinusOrSetSubtractExpression();
    				minus2.setLeft(add2);
    				minus2.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
    				ArrayList<PExpression> params = new ArrayList<>();
    				params.add(minus2);
    				AFunctionExpression func = new AFunctionExpression();
    				func.setIdentifier(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				func.setParameters(params);
    				lambda.setExpression(func);
    				returnNode = lambda;
    				break;
    			}
    
    			case B_OPCODE_assert: {
    				ADefinitionPredicate pred = new ADefinitionPredicate();
    				pred.setDefLiteral(new TDefLiteralPredicate("ASSERT_TRUE"));
    				ArrayList<PExpression> list = new ArrayList<>();
    				list.add(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				list.add(new AStringExpression(new TStringLiteral("Error")));
    				pred.setParameters(list);
    				returnNode = new AConvertBoolExpression(pred);
    				break;
    			}
    
    			case B_OPCODE_setsum: {
    				AGeneralSumExpression sum = new AGeneralSumExpression();
    				String variableName = "t_"; // TODO unused identifier name
    				List<PExpression> exprList = createPexpressionList(createIdentifierNode(variableName));
    				sum.setIdentifiers(exprList);
    				AMemberPredicate memberPredicate = new AMemberPredicate();
    				memberPredicate.setLeft(createIdentifierNode(variableName));
    				memberPredicate.setRight(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
    				sum.setPredicates(memberPredicate);
    				sum.setExpression(createIdentifierNode(variableName));
    				returnNode = sum;
    				break;
    			}
    		}
    		if (returnNode != null) {
    			return createPositionedNode(returnNode, opApplNode);
    		} else {
    			throw new RuntimeException("Unexpected operator: " + opApplNode.getOperator().getName().toString() + "\n"
    				+ opApplNode.stn.getLocation());
    		}
    
    	}
    
    	private <T extends PositionedNode> T createPositionedNode(T positionedNode, SemanticNode semanticNode) {
    		Location location = semanticNode.getTreeNode().getLocation();
    		SourcePosition startPos = new SourcePosition(location.beginLine(), location.beginColumn());
    		SourcePosition endPos = new SourcePosition(location.endLine(), location.endColumn());
    		positionedNode.setStartPos(startPos);
    		positionedNode.setEndPos(endPos);
    		sourcePosition.add(positionedNode);
    		return positionedNode;
    	}
    
    	private void setPosition(PositionedNode positionNode, OpApplNode opApplNode) {
    		Location location = opApplNode.getTreeNode().getLocation();
    		SourcePosition startPos = new SourcePosition(location.beginLine(), location.beginColumn());
    		SourcePosition endPos = new SourcePosition(location.endLine(), location.endColumn());
    		positionNode.setStartPos(startPos);
    		positionNode.setEndPos(endPos);
    		sourcePosition.add(positionNode);
    	}
    
    	private PExpression visitBuiltInKindExpression(OpApplNode n) {
    		switch (getOpCode(n.getOperator().getName())) {
    
    			case OPCODE_land: // \land
    			{
    				AConjunctPredicate conjunction = new AConjunctPredicate();
    				conjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				return new AConvertBoolExpression(conjunction);
    			}
    
    			case OPCODE_equiv: // \equiv
    				AEquivalencePredicate equiv = new AEquivalencePredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]),
    					visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				return new AConvertBoolExpression(equiv);
    
    			case OPCODE_implies: // =>
    				AImplicationPredicate impl = new AImplicationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]),
    					visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				new AConvertBoolExpression(impl);
    
    			case OPCODE_cl: // $ConjList
    			{
    				List<PPredicate> list = new ArrayList<>();
    				for (int i = 0; i < n.getArgs().length; i++) {
    					list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
    				}
    				return new AConvertBoolExpression(createConjunction(list));
    			}
    
    			case OPCODE_dl: // $DisjList
    			{
    				List<PPredicate> list = new ArrayList<>();
    				for (int i = 0; i < n.getArgs().length; i++) {
    					list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
    				}
    				return new AConvertBoolExpression(createDisjunction(list));
    			}
    
    			case OPCODE_lor: // \/
    			{
    				ADisjunctPredicate disjunction = new ADisjunctPredicate();
    				disjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				disjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				return new AConvertBoolExpression(disjunction);
    			}
    
    			case OPCODE_lnot: // \lnot
    				return new AConvertBoolExpression(new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0])));
    
    			case OPCODE_in: // \in
    			{
    				AMemberPredicate memberPredicate = new AMemberPredicate();
    				memberPredicate.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				memberPredicate.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return new AConvertBoolExpression(memberPredicate);
    			}
    
    			case OPCODE_notin: // \notin
    			{
    				ANotMemberPredicate notMemberPredicate = new ANotMemberPredicate();
    				notMemberPredicate.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				notMemberPredicate.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return new AConvertBoolExpression(notMemberPredicate);
    			}
    
    			case OPCODE_eq: { // =
    				AEqualPredicate equal = new AEqualPredicate();
    				equal.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				equal.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return new AConvertBoolExpression(equal);
    			}
    
    			case OPCODE_noteq: // /=
    			{
    				ANotEqualPredicate notEqual = new ANotEqualPredicate();
    				notEqual.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				notEqual.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return new AConvertBoolExpression(notEqual);
    			}
    
    			/*
    			 * Set Operators
    			 */
    
    			case OPCODE_se: // SetEnumeration {..}
    			{
    				if (n.getArgs().length == 0) {
    					return new AEmptySetExpression();
    				} else {
    					List<PExpression> list = new ArrayList<>();
    
    					for (int i = 0; i < n.getArgs().length; i++) {
    						list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
    					}
    					return new ASetExtensionExpression(list);
    				}
    			}
    
    			case 0: {
    				return visitBBuiltInsExpression(n);
    			}
    
    			case OPCODE_setdiff: // set difference
    			{
    				AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression();
    				minus.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				minus.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return minus;
    			}
    
    			case OPCODE_cup: // set union
    			{
    				AUnionExpression union = new AUnionExpression();
    				union.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				union.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return union;
    			}
    
    			case OPCODE_cap: // set intersection
    			{
    				AIntersectionExpression inter = new AIntersectionExpression();
    				inter.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				inter.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return inter;
    			}
    
    			case OPCODE_subset: // SUBSET
    			{
    				APowSubsetExpression pow = new APowSubsetExpression();
    				pow.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				return pow;
    			}
    
    			case OPCODE_union: // Union - Union{{1},{2}}
    			{
    				AGeneralUnionExpression union = new AGeneralUnionExpression();
    				union.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				return union;
    			}
    
    			case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
    			{
    				ASubsetPredicate subset = new ASubsetPredicate();
    				subset.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				subset.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				return new AConvertBoolExpression(subset);
    			}
    
    			case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				List<PExpression> list = new ArrayList<>();
    				for (int i = 0; i < params[0].length; i++) {
    					FormalParamNode p = params[0][i];
    					list.add(createIdentifierNode(p));
    				}
    				return new AComprehensionSetExpression(
    					list,
    					new AConjunctPredicate(
    						visitBoundsOfFunctionsVariables(n),
    						visitExprOrOpArgNodePredicate(n.getArgs()[0])
    					)
    				);
    			}
    
    			case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				List<PExpression> idList = createListOfIdentifier(params);
    				List<PPredicate> predList = new ArrayList<>();
    				predList.add(visitBoundsOfLocalVariables(n));
    
    				// currently not used:
    				/* final String nameOfTempVariable = "t_";
    
    				AEqualPredicate equals = new AEqualPredicate(
    					createIdentifierNode(nameOfTempVariable),
    					visitExprOrOpArgNodeExpression(n.getArgs()[0])
    				);
    				// predList.add(equals);
    				AExistsPredicate exist = new AExistsPredicate(
    					idList,
    					createConjunction(predList)
    				);
    
    				AComprehensionSetExpression compre = new AComprehensionSetExpression();
    				List<PExpression> tList = new ArrayList<>();
    				tList.add(createIdentifierNode(nameOfTempVariable));
    				compre.setIdentifiers(tList);
    				compre.setPredicates(exist);*/
    
    				// UNION(p1,p2,p3).(P | {e})
    				return new AQuantifiedUnionExpression(
    					idList,
    					createConjunction(predList),
    					new ASetExtensionExpression(
    						Collections.singletonList(visitExprOrOpArgNodeExpression(n.getArgs()[0])))
    				);
    			}
    
    			case OPCODE_nrfs:
    			case OPCODE_fc: // Represents [x \in S |-> e].
    			case OPCODE_rfs: {
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				List<PExpression> idList = new ArrayList<>();
    				for (FormalParamNode[] param : params) {
    					for (FormalParamNode p : param) {
    						idList.add(createIdentifierNode(p));
    					}
    				}
    				boolean[] isTuple = n.isBdedQuantATuple();
    				ALambdaExpression lambda = new ALambdaExpression();
    				List<PExpression> idList2 = new ArrayList<>();
    				for (int i = 0; i < params.length; i++) {
    					if (isTuple[i] && i > 0) {
    						StringBuilder sb = new StringBuilder();
    						for (int j = 0; j < params[i].length; j++) {
    							FormalParamNode p = params[i][j];
    							sb.append(p.getName().toString());
    
    						}
    						idList2.add(createIdentifierNode(sb.toString()));
    					} else {
    						for (int j = 0; j < params[i].length; j++) {
    							FormalParamNode p = params[i][j];
    							idList2.add(createIdentifierNode(p.getName().toString()));
    						}
    					}
    				}
    
    				lambda.setIdentifiers(idList2);
    				lambda.setPredicate(visitBoundsOfFunctionsVariables(n));
    				lambda.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    
    				if (recursiveFunctionHandler.isRecursiveFunction(n)) {
    
    					ArrayList<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
    					if (!externParams.isEmpty()) {
    						ALambdaExpression lambda2 = new ALambdaExpression();
    						ArrayList<PExpression> shiftedParams = new ArrayList<>();
    						List<PPredicate> predList2 = new ArrayList<>();
    						for (SymbolNode p : externParams) {
    							shiftedParams.add(createIdentifierNode(p));
    
    							AMemberPredicate member = new AMemberPredicate();
    							member.setLeft(createIdentifierNode(p));
    							TLAType t = (TLAType) p.getToolObject(TYPE_ID);
    							member.setRight(t.getBNode());
    							predList2.add(member);
    						}
    						lambda2.setIdentifiers(shiftedParams);
    						lambda2.setPredicate(createConjunction(predList2));
    						lambda2.setExpression(lambda);
    						return lambda2;
    					}
    				}
    				return lambda;
    			}
    
    			case OPCODE_fa: { // f[1]
    				TLAType t = (TLAType) n.getArgs()[0].getToolObject(TYPE_ID);
    				if (t instanceof TupleType) {
    					NumeralNode num = (NumeralNode) n.getArgs()[1];
    					int field = num.val();
    					PExpression pair = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
    					return createProjectionFunction(pair, field, t);
    				} else {
    					AFunctionExpression func = new AFunctionExpression();
    					func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    					List<PExpression> paramList = new ArrayList<>();
    
    					ExprOrOpArgNode dom = n.getArgs()[1];
    					if (dom instanceof OpApplNode
    						&& ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
    						OpApplNode domOpAppl = (OpApplNode) dom;
    						if (domOpAppl.getArgs().length == 1) {
    							List<PExpression> list = new ArrayList<>();
    							list.add(visitExprOrOpArgNodeExpression(domOpAppl.getArgs()[0]));
    							ASequenceExtensionExpression seq = new ASequenceExtensionExpression(list);
    							paramList.add(seq);
    						} else {
    							for (int i = 0; i < domOpAppl.getArgs().length; i++) {
    								paramList.add(visitExprOrOpArgNodeExpression(domOpAppl.getArgs()[i]));
    							}
    						}
    
    					} else {
    						paramList.add(visitExprOrOpArgNodeExpression(dom));
    					}
    					func.setParameters(paramList);
    					return func;
    				}
    
    			}
    
    			case OPCODE_domain:
    				return new ADomainExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    
    			case OPCODE_sof: // [ A -> B]
    				return new ATotalFunctionExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    
    			case OPCODE_tup: { // $Tuple
    				List<PExpression> list = new ArrayList<>();
    				for (int i = 0; i < n.getArgs().length; i++) {
    					list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
    				}
    				TLAType t = (TLAType) n.getToolObject(TYPE_ID);
    				if (t instanceof TupleType) {
    					return new ACoupleExpression(list);
    				} else {
    					if (list.isEmpty()) {
    						return new AEmptySequenceExpression();
    					} else {
    						return new ASequenceExtensionExpression(list);
    					}
    				}
    			}
    
    			case OPCODE_cp: // $CartesianProd A \X B \X C
    			{
    				PExpression first = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
    				for (int i = 1; i < n.getArgs().length; i++) {
    					PExpression second = visitExprOrOpArgNodeExpression(n.getArgs()[i]);
    					first = new AMultOrCartExpression(first, second);
    				}
    				return first;
    			}
    
    			case OPCODE_sor: { // $SetOfRcds [L1 : e1, L2 : e2]
    				SetType pow = (SetType) n.getToolObject(TYPE_ID);
    				StructType struct = (StructType) pow.getSubType();
    				ExprOrOpArgNode[] args = n.getArgs();
    				Hashtable<String, PExpression> pairTable = new Hashtable<>();
    				for (ExprOrOpArgNode arg : args) {
    					OpApplNode pair = (OpApplNode) arg;
    					StringNode stringNode = (StringNode) pair.getArgs()[0];
    					pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
    
    				}
    				List<PRecEntry> recList = new ArrayList<>();
    				if (struct.isExtensible()) {
    					for (int i = 0; i < struct.getFields().size(); i++) {
    						String fieldName = struct.getFields().get(i); // name
    						AIdentifierExpression field = createIdentifierNode(fieldName);
    						ARecEntry rec = new ARecEntry();
    						rec.setIdentifier(field);
    						AMultOrCartExpression cart = new AMultOrCartExpression();
    						cart.setLeft(new ABoolSetExpression());
    						if (pairTable.containsKey(fieldName)) {
    							cart.setRight(pairTable.get(fieldName));
    						} else {
    							cart.setRight(struct.getType(fieldName).getBNode());
    						}
    						rec.setValue(new APowSubsetExpression(cart));
    						recList.add(rec);
    					}
    				} else {
    					for (int i = 0; i < struct.getFields().size(); i++) {
    						String fieldName = struct.getFields().get(i);
    						AIdentifierExpression field = createIdentifierNode(fieldName);
    						ARecEntry rec = new ARecEntry();
    						rec.setIdentifier(field);
    						if (pairTable.containsKey(fieldName)) {
    							rec.setValue(pairTable.get(fieldName));
    						} else {
    							rec.setValue(struct.getType(fieldName).getBNode());
    						}
    						recList.add(rec);
    					}
    
    				}
    				return new AStructExpression(recList);
    			}
    
    			case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2]
    				StructType struct = (StructType) n.getToolObject(TYPE_ID);
    				if (struct.isExtensible()) {
    					Hashtable<String, PExpression> pairTable = new Hashtable<>();
    					ExprOrOpArgNode[] args = n.getArgs();
    					for (ExprOrOpArgNode arg : args) {
    						OpApplNode pair = (OpApplNode) arg;
    						StringNode stringNode = (StringNode) pair.getArgs()[0];
    						pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
    					}
    					List<PRecEntry> recList = new ArrayList<>();
    					for (int i = 0; i < struct.getFields().size(); i++) {
    						String fieldName = struct.getFields().get(i);
    						AIdentifierExpression field = createIdentifierNode(fieldName);
    						ARecEntry rec = new ARecEntry();
    						rec.setIdentifier(field);
    						if (pairTable.containsKey(fieldName)) {
    
    							ACoupleExpression couple = new ACoupleExpression();
    							List<PExpression> coupleList = new ArrayList<>();
    							coupleList.add(new ABooleanTrueExpression());
    							coupleList.add(pairTable.get(fieldName));
    							couple.setList(coupleList);
    							ASetExtensionExpression set = new ASetExtensionExpression(createPexpressionList(couple));
    							rec.setValue(set);
    						} else {
    							AEmptySetExpression emptySet = new AEmptySetExpression();
    							rec.setValue(emptySet);
    						}
    						recList.add(rec);
    					}
    					return new ARecExpression(recList);
    
    				} else {
    					Hashtable<String, PExpression> pairTable = new Hashtable<>();
    					ExprOrOpArgNode[] args = n.getArgs();
    					for (ExprOrOpArgNode arg : args) {
    						OpApplNode pair = (OpApplNode) arg;
    						StringNode stringNode = (StringNode) pair.getArgs()[0];
    						pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
    					}
    					List<PRecEntry> recList = new ArrayList<>();
    					for (int i = 0; i < struct.getFields().size(); i++) {
    						String fieldName = struct.getFields().get(i);
    						AIdentifierExpression field = createIdentifierNode(fieldName);
    						ARecEntry rec = new ARecEntry();
    						rec.setIdentifier(field);
    						if (pairTable.containsKey(fieldName)) {
    							rec.setValue(pairTable.get(fieldName));
    						} else {
    							// this struct is extensible
    							throw new NotImplementedException("Missing case handling extensible structs.");
    						}
    						recList.add(rec);
    					}
    					return new ARecExpression(recList);
    				}
    
    			}
    
    			case OPCODE_rs: { // $RcdSelect r.c
    				StructType struct = (StructType) n.getArgs()[0].getToolObject(TYPE_ID);
    				if (struct.isExtensible()) {
    					ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
    					rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    					StringNode stringNode = (StringNode) n.getArgs()[1];
    					rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep().toString()));
    					AFunctionExpression funcCall = new AFunctionExpression();
    					funcCall.setIdentifier(rcdSelect);
    					funcCall.setParameters(createPexpressionList(new ABooleanTrueExpression()));
    					return funcCall;
    				} else {
    					ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
    					rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    					StringNode stringNode = (StringNode) n.getArgs()[1];
    					rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep().toString()));
    					return rcdSelect;
    				}
    			}
    
    			case OPCODE_prime: // prime
    			{
    				OpApplNode node = (OpApplNode) n.getArgs()[0];
    				return createIdentifierNode(node.getOperator().getName().toString() + "_n");
    			}
    
    			case OPCODE_ite: { // IF THEN ELSE
    				List<PExpression> Elsifs = new ArrayList<>();
    				AIfThenElseExpression ifthenElse = new AIfThenElseExpression(visitExprOrOpArgNodePredicate(n.getArgs()[0]),
    					visitExprOrOpArgNodeExpression(n.getArgs()[1]), Elsifs,
    					visitExprOrOpArgNodeExpression(n.getArgs()[2]));
    				return ifthenElse;
    
    				// ALambdaExpression lambda1 = new ALambdaExpression();
    				// lambda1.setIdentifiers(createIdentifierList("t_"));
    				// AEqualPredicate eq1 = new AEqualPredicate(
    				// createIdentifierNode("t_"), new AIntegerExpression(
    				// new TIntegerLiteral("0")));
    				// AConjunctPredicate c1 = new AConjunctPredicate();
    				// c1.setLeft(eq1);
    				// c1.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				// lambda1.setPredicate(c1);
    				// lambda1.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				//
    				// ALambdaExpression lambda2 = new ALambdaExpression();
    				// lambda2.setIdentifiers(createIdentifierList("t_"));
    				// AEqualPredicate eq2 = new AEqualPredicate(
    				// createIdentifierNode("t_"), new AIntegerExpression(
    				// new TIntegerLiteral("0")));
    				// AConjunctPredicate c2 = new AConjunctPredicate();
    				// c2.setLeft(eq2);
    				// ANegationPredicate not = new ANegationPredicate(
    				// visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				// c2.setRight(not);
    				// lambda2.setPredicate(c2);
    				// lambda2.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
    				//
    				// AUnionExpression union = new AUnionExpression(lambda1, lambda2);
    				// AFunctionExpression funCall = new AFunctionExpression();
    				// funCall.setIdentifier(union);
    				// List<PExpression> list = new ArrayList<PExpression>();
    				// list.add(new AIntegerExpression(new TIntegerLiteral("0")));
    				// funCall.setParameters(list);
    				// return funCall;
    			}
    
    			case OPCODE_case: {
    				return createCaseNode(n);
    			}
    
    			case OPCODE_exc: // $Except
    			{
    				TLAType type = (TLAType) n.getToolObject(TYPE_ID);
    
    				if (type.getKind() == IType.STRUCT) {
    					StructType structType = (StructType) type;
    					PExpression res = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
    					for (int i = 1; i < n.getArgs().length; i++) {
    						OpApplNode pair = (OpApplNode) n.getArgs()[i];
    						ExprOrOpArgNode first = pair.getArgs()[0];
    						ExprOrOpArgNode val = pair.getArgs()[1];
    						OpApplNode seq = (OpApplNode) first;
    
    						LinkedList<ExprOrOpArgNode> seqList = new LinkedList<>();
    						Collections.addAll(seqList, seq.getArgs());
    
    						pair.setToolObject(EXCEPT_BASE, res.clone());
    						res = evalExceptValue(res.clone(), seqList, structType, val);
    					}
    					return res;
    
    				} else {
    					FunctionType func = (FunctionType) type;
    
    					PExpression res = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
    					for (int i = 1; i < n.getArgs().length; i++) {
    						OpApplNode pair = (OpApplNode) n.getArgs()[i];
    
    						ExprOrOpArgNode first = pair.getArgs()[0];
    						ExprOrOpArgNode val = pair.getArgs()[1];
    						OpApplNode seq = (OpApplNode) first;
    
    						LinkedList<ExprOrOpArgNode> seqList = new LinkedList<>();
    						Collections.addAll(seqList, seq.getArgs());
    
    						pair.setToolObject(EXCEPT_BASE, res.clone());
    						res = evalExceptValue(res.clone(), seqList, func, val);
    					}
    					return res;
    				}
    			}
    
    			case OPCODE_seq: // !
    			{
    				return visitExprOrOpArgNodeExpression(n.getArgs()[0]);
    			}
    
    			case OPCODE_uc: { // CHOOSE x : P
    				return createUnboundedChoose(n);
    			}
    
    			case OPCODE_bc: { // CHOOSE x \in S: P
    				return createBoundedChoose(n);
    			}
    
    			case OPCODE_bf: { // \A x \in S : P
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				ArrayList<PExpression> list = new ArrayList<>();
    				for (FormalParamNode[] param : params) {
    					for (FormalParamNode formalParamNode : param) {
    						list.add(createIdentifierNode(formalParamNode));
    					}
    				}
    				AImplicationPredicate implication = new AImplicationPredicate();
    				implication.setLeft(visitBoundsOfLocalVariables(n));
    				implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				return new AConvertBoolExpression(new AForallPredicate(list, implication));
    			}
    
    			case OPCODE_be: { // \E x \in S : P
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				ArrayList<PExpression> list = new ArrayList<>();
    				for (FormalParamNode[] param : params) {
    					for (FormalParamNode formalParamNode : param) {
    						list.add(createIdentifierNode(formalParamNode));
    					}
    				}
    				AConjunctPredicate conjunction = new AConjunctPredicate();
    				conjunction.setLeft(visitBoundsOfLocalVariables(n));
    				conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				AExistsPredicate exists = new AExistsPredicate(list, conjunction);
    				return new AConvertBoolExpression(exists);
    			}
    
    		}
    
    		throw new NotImplementedException("Missing support for operator: " + n.getOperator().getName());
    	}
    
    	private List<PExpression> createListOfIdentifier(FormalParamNode[][] params) {
    		List<PExpression> list = new ArrayList<>();
    		for (FormalParamNode[] formalParamNodes : params) {
    			for (FormalParamNode param : formalParamNodes) {
    				list.add(createIdentifierNode(param));
    			}
    		}
    		return list;
    	}
    
    	private PExpression evalExceptValue(PExpression prefix, LinkedList<ExprOrOpArgNode> seqList, TLAType tlaType,
    	                                    ExprOrOpArgNode val) {
    
    		ExprOrOpArgNode head = seqList.poll();
    		if (head == null) {
    			return visitExprOrOpArgNodeExpression(val);
    		}
    
    		if (tlaType instanceof StructType) {
    			StructType structType = (StructType) tlaType;
    			String field = ((StringNode) head).getRep().toString();
    
    			List<PRecEntry> list = new ArrayList<>();
    			for (int i = 0; i < structType.getFields().size(); i++) {
    				ARecEntry entry = new ARecEntry();
    				String fieldName = structType.getFields().get(i);
    				entry.setIdentifier(createIdentifierNode(fieldName));
    
    				PExpression value;
    				ARecordFieldExpression select = new ARecordFieldExpression();
    				select.setRecord(prefix.clone());
    				select.setIdentifier(createIdentifierNode(fieldName));
    				if (fieldName.equals(field)) {
    					value = evalExceptValue(select, seqList, structType.getType(fieldName), val);
    				} else {
    					value = select;
    				}
    				entry.setValue(value);
    				list.add(entry);
    
    			}
    
    			return new ARecExpression(list);
    
    		} else {
    			FunctionType func = (FunctionType) tlaType;
    
    			ACoupleExpression couple = new ACoupleExpression();
    			List<PExpression> coupleList = new ArrayList<>();
    			coupleList.add(visitExprOrOpArgNodeExpression(head));
    
    			AFunctionExpression funcCall = new AFunctionExpression();
    			funcCall.setIdentifier(prefix);
    			List<PExpression> argList = new ArrayList<>();
    			argList.add(visitExprOrOpArgNodeExpression(head));
    			funcCall.setParameters(argList);
    			coupleList.add(evalExceptValue(funcCall, seqList, func.getRange(), val));
    			couple.setList(coupleList);
    			List<PExpression> setList = new ArrayList<>();
    			setList.add(couple);
    			ASetExtensionExpression setExtension = new ASetExtensionExpression(setList);
    			AOverwriteExpression overwrite = new AOverwriteExpression();
    			overwrite.setLeft(prefix.clone());
    			overwrite.setRight(setExtension);
    			return overwrite;
    		}
    	}
    
    	private PExpression createProjectionFunction(PExpression pair, int field, TLAType t) {
    		TupleType tuple = (TupleType) t;
    		int size = tuple.getTypes().size();
    
    		AFunctionExpression returnFunc = new AFunctionExpression();
    		int index;
    		if (field == 1) {
    			index = 2;
    			AFirstProjectionExpression first = new AFirstProjectionExpression();
    			first.setExp1(tuple.getTypes().get(0).getBNode());
    			first.setExp2(tuple.getTypes().get(1).getBNode());
    			returnFunc.setIdentifier(first);
    		} else {
    			index = field;
    			ASecondProjectionExpression second = new ASecondProjectionExpression();
    			ArrayList<TLAType> typeList = new ArrayList<>();
    			for (int i = 0; i < field - 1; i++) {
    				typeList.add(tuple.getTypes().get(i));
    			}
    			second.setExp1(createNestedCouple(typeList));
    			second.setExp2(tuple.getTypes().get(field - 1).getBNode());
    			returnFunc.setIdentifier(second);
    		}
    		AFunctionExpression func = returnFunc;
    		for (int i = index; i < size; i++) {
    			AFunctionExpression newfunc = new AFunctionExpression();
    			AFirstProjectionExpression first = new AFirstProjectionExpression();
    			ArrayList<TLAType> typeList = new ArrayList<>();
    			for (int j = 0; j < i; j++) {
    				typeList.add(tuple.getTypes().get(j));
    			}
    			first.setExp1(createNestedCouple(typeList));
    			first.setExp2(tuple.getTypes().get(i).getBNode());
    			newfunc.setIdentifier(first);
    
    			ArrayList<PExpression> list = new ArrayList<>();
    			list.add(newfunc);
    			func.setParameters(list);
    			func = newfunc;
    		}
    		ArrayList<PExpression> list = new ArrayList<>();
    		list.add(pair);
    		func.setParameters(list);
    		return returnFunc;
    	}
    
    	public static PExpression createNestedCouple(List<TLAType> typeList) {
    		if (typeList.size() == 1) {
    			return typeList.get(0).getBNode();
    		}
    		List<PExpression> list = new ArrayList<>();
    		for (TLAType t : typeList) {
    			list.add(t.getBNode());
    		}
    		AMultOrCartExpression card = new AMultOrCartExpression();
    		card.setLeft(list.get(0));
    		for (int i = 1; i < list.size(); i++) {
    			if (i < list.size() - 1) {
    				AMultOrCartExpression old = card;
    				old.setRight(list.get(i));
    				card = new AMultOrCartExpression();
    				card.setLeft(old);
    			} else {
    				card.setRight(list.get(i));
    			}
    		}
    		return card;
    	}
    
    	private PExpression createUnboundedChoose(OpApplNode n) {
    		ADefinitionExpression defCall = new ADefinitionExpression();
    		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
    		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
    		List<PExpression> paramList = new ArrayList<>();
    		for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
    			paramList.add(createIdentifierNode(param));
    		}
    		comprehension.setIdentifiers(paramList);
    		comprehension.setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    		List<PExpression> list = new ArrayList<>();
    		list.add(comprehension);
    		defCall.setParameters(list);
    		return defCall;
    	}
    
    	private PExpression createBoundedChoose(OpApplNode n) {
    		ADefinitionExpression defCall = new ADefinitionExpression();
    		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
    		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
    		List<PExpression> paramList = new ArrayList<>();
    		for (FormalParamNode param : n.getBdedQuantSymbolLists()[0]) {
    			paramList.add(createIdentifierNode(param));
    		}
    		comprehension.setIdentifiers(paramList);
    		PPredicate typingPredicate = visitBoundsOfLocalVariables(n);
    		AConjunctPredicate conj = new AConjunctPredicate();
    		conj.setLeft(typingPredicate);
    		conj.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    		comprehension.setPredicates(conj);
    		List<PExpression> list = new ArrayList<>();
    		list.add(comprehension);
    		defCall.setParameters(list);
    		return defCall;
    	}
    
    	private PExpression createCaseNode(OpApplNode n) {
    		List<PPredicate> conditions = new ArrayList<>();
    		List<PPredicate> disjunctionList = new ArrayList<>();
    		for (int i = 0; i < n.getArgs().length; i++) {
    			OpApplNode pair = (OpApplNode) n.getArgs()[i];
    
    			AConjunctPredicate conj = new AConjunctPredicate();
    			if (pair.getArgs()[0] == null) {
    				ANegationPredicate neg = new ANegationPredicate();
    				neg.setPredicate(createDisjunction(conditions));
    				conj.setLeft(neg);
    			} else {
    				conditions.add(visitExprOrOpArgNodePredicate(pair.getArgs()[0]));
    				conj.setLeft(visitExprOrOpArgNodePredicate(pair.getArgs()[0]));
    			}
    			AEqualPredicate equals = new AEqualPredicate();
    			equals.setLeft(createIdentifierNode("t_"));
    			equals.setRight(visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
    			conj.setRight(equals);
    			disjunctionList.add(conj);
    		}
    		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
    		comprehension.setIdentifiers(createIdentifierList("t_"));
    		comprehension.setPredicates(createDisjunction(disjunctionList));
    		ADefinitionExpression defCall = new ADefinitionExpression();
    		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
    		List<PExpression> params = new ArrayList<>();
    		params.add(comprehension);
    		defCall.setParameters(params);
    		return defCall;
    	}
    
    	private List<PExpression> createIdentifierList(String name) {
    		ArrayList<PExpression> list = new ArrayList<>();
    		list.add(createIdentifierNode(name));
    		return list;
    	}
    
    	private PPredicate visitBuiltInKindPredicate(OpApplNode n) {
    		PPredicate returnNode;
    		switch (getOpCode(n.getOperator().getName())) {
    			case OPCODE_land: // \land
    			{
    				AConjunctPredicate conjunction = new AConjunctPredicate();
    				conjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				returnNode = conjunction;
    				break;
    			}
    			case OPCODE_cl: // $ConjList
    			{
    				List<PPredicate> list = new ArrayList<>();
    				for (int i = 0; i < n.getArgs().length; i++) {
    					list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
    				}
    				returnNode = createConjunction(list);
    				break;
    			}
    			case OPCODE_lor: // \/
    			{
    				ADisjunctPredicate disjunction = new ADisjunctPredicate();
    				disjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				disjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				returnNode = disjunction;
    				break;
    			}
    			case OPCODE_dl: // $DisjList
    			{
    				List<PPredicate> list = new ArrayList<>();
    				for (int i = 0; i < n.getArgs().length; i++) {
    					list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
    				}
    				returnNode = createDisjunction(list);
    				break;
    			}
    			case OPCODE_lnot: // \lnot
    				returnNode = new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				break;
    			case OPCODE_equiv: // \equiv
    				returnNode = new AEquivalencePredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]),
    					visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				break;
    
    			case OPCODE_implies: // =>
    				returnNode = new AImplicationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]),
    					visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    				break;
    
    			case OPCODE_be: { // \E x \in S : P
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				ArrayList<PExpression> list = new ArrayList<>();
    				for (FormalParamNode[] param : params) {
    					for (FormalParamNode formalParamNode : param) {
    						list.add(createIdentifierNode(formalParamNode));
    					}
    				}
    				AConjunctPredicate conjunction = new AConjunctPredicate();
    				conjunction.setLeft(visitBoundsOfLocalVariables(n));
    				conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				returnNode = new AExistsPredicate(list, conjunction);
    				break;
    			}
    
    			case OPCODE_bf: { // \A x \in S : P
    				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    				ArrayList<PExpression> list = new ArrayList<>();
    				for (FormalParamNode[] param : params) {
    					for (FormalParamNode formalParamNode : param) {
    						list.add(createIdentifierNode(formalParamNode));
    					}
    				}
    				AImplicationPredicate implication = new AImplicationPredicate();
    				implication.setLeft(visitBoundsOfLocalVariables(n));
    				implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				returnNode = new AForallPredicate(list, implication);
    				break;
    			}
    
    			case OPCODE_eq: { // =
    				AEqualPredicate equal = new AEqualPredicate();
    				equal.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				equal.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				returnNode = equal;
    				break;
    			}
    			case OPCODE_noteq: // /=
    			{
    				ANotEqualPredicate notEqual = new ANotEqualPredicate();
    				notEqual.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				notEqual.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				returnNode = notEqual;
    				break;
    			}
    			case OPCODE_in: // \in
    			{
    				AMemberPredicate memberPredicate = new AMemberPredicate();
    				memberPredicate.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				memberPredicate.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				returnNode = memberPredicate;
    				break;
    			}
    
    			case OPCODE_notin: // \notin
    			{
    				ANotMemberPredicate notMemberPredicate = new ANotMemberPredicate();
    				notMemberPredicate.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				notMemberPredicate.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				returnNode = notMemberPredicate;
    				break;
    			}
    
    			case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
    			{
    				ASubsetPredicate subset = new ASubsetPredicate();
    				subset.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				subset.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
    				returnNode = subset;
    				break;
    			}
    
    			case OPCODE_fa: { // f[1]
    				AFunctionExpression func = new AFunctionExpression();
    				func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				List<PExpression> paramList = new ArrayList<>();
    
    				ExprOrOpArgNode dom = n.getArgs()[1];
    				if (dom instanceof OpApplNode && ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
    					OpApplNode domOpAppl = (OpApplNode) dom;
    					for (int i = 0; i < domOpAppl.getArgs().length; i++) {
    						paramList.add(visitExprOrOpArgNodeExpression(domOpAppl.getArgs()[i]));
    					}
    				} else {
    					paramList.add(visitExprOrOpArgNodeExpression(dom));
    				}
    				func.setParameters(paramList);
    				returnNode = new AEqualPredicate(func, new ABooleanTrueExpression());
    				break;
    			}
    
    			case OPCODE_rs: { // $RcdSelect r.c
    				ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
    				rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
    				StringNode stringNode = (StringNode) n.getArgs()[1];
    				rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep().toString()));
    				returnNode = new AEqualPredicate(rcdSelect, new ABooleanTrueExpression());
    				break;
    			}
    
    			case OPCODE_case: {
    				returnNode = new AEqualPredicate(createCaseNode(n), new ABooleanTrueExpression());
    				break;
    			}
    			case OPCODE_prime: // prime
    			{
    				OpApplNode node = (OpApplNode) n.getArgs()[0];
    				returnNode = new AEqualPredicate(createIdentifierNode(getName(node.getOperator()) + "_n"),
    					new ABooleanTrueExpression());
    				break;
    			}
    			case OPCODE_unchanged: {
    				OpApplNode node = (OpApplNode) n.getArgs()[0];
    				// System.out.println(" Translating UNCHANGED : " + node.toString());
    				// System.out.println(" Top-level unchanged for this operation: " + this.toplevelUnchangedVariableNames);
    				if (node.getOperator().getKind() == VariableDeclKind) {
    					return CreateUnchangedPrimeEquality(node);
    
    				} else if (node.getOperator().getKind() == UserDefinedOpKind) {
    					OpDefNode operator = (OpDefNode) node.getOperator();
    					ExprNode e = operator.getBody();
    					node = (OpApplNode) e;
    				}
    
    				ArrayList<PPredicate> list = new ArrayList<>();
    				for (int i = 0; i < node.getArgs().length; i++) {
    					OpApplNode var = (OpApplNode) node.getArgs()[i];
    					list.add(CreateUnchangedPrimeEquality(var));
    				}
    				returnNode = createConjunction(list);
    				// returnNode = new AEqualPredicate(new ABooleanTrueExpression(),
    				// new ABooleanTrueExpression());
    				break;
    			}
    			case OPCODE_uc: { // CHOOSE x : P
    				returnNode = new AEqualPredicate(createUnboundedChoose(n), new ABooleanTrueExpression());
    				break;
    			}
    			case OPCODE_bc: { // CHOOSE x \in S: P
    				returnNode = new AEqualPredicate(createBoundedChoose(n), new ABooleanTrueExpression());
    				break;
    			}
    			case OPCODE_ite: // IF THEN ELSE
    			{
    				AImplicationPredicate impl1 = new AImplicationPredicate();
    				impl1.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				impl1.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
    
    				AImplicationPredicate impl2 = new AImplicationPredicate();
    				ANegationPredicate neg = new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
    				impl2.setLeft(neg);
    				impl2.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[2]));
    				returnNode = new AConjunctPredicate(impl1, impl2);
    				break;
    			}
    			case 0:
    				return visitBBuiltInsPredicate(n);
    			default:
    				throw new NotImplementedException(n.getOperator().getName().toString());
    		}
    		return createPositionedNode(returnNode, n);
    	}
    
    	// create an equality predicate var_n = var if required
    	private AEqualPredicate CreateUnchangedPrimeEquality(OpApplNode var) {
    		if (!this.toplevelUnchangedVariableNames.contains(getName(var.getOperator()))) {
    			AEqualPredicate equal = new AEqualPredicate();
    			equal.setLeft(createIdentifierNode(getName(var.getOperator()) + "_n"));
    			equal.setRight(createIdentifierNode(var.getOperator()));
    			return equal;
    		} else {
    			// the variable is marked UNCHANGED in a top-level UNCHANGED predicate
    			// Hence it will not be added to the ANY variables and we do not need it
    			return new AEqualPredicate(new ABooleanTrueExpression(), new ABooleanTrueExpression());
    		}
    
    	}
    
    	public PPredicate visitBoundsOfLocalVariables(OpApplNode n) {
    		FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    		ExprNode[] in = n.getBdedQuantBounds();
    		boolean[] isTuple = n.isBdedQuantATuple();
    
    		List<PPredicate> predList = new ArrayList<>();
    		for (int i = 0; i < params.length; i++) {
    			if (isTuple[i]) {
    				if (params[i].length == 1) {
    					// one-tuple is handled is translated as a sequence
    					FormalParamNode param = params[i][0];
    					AMemberPredicate member = new AMemberPredicate();
    					ASequenceExtensionExpression seq = new ASequenceExtensionExpression();
    					List<PExpression> list = new ArrayList<>();
    					list.add(createIdentifierNode(param));
    					seq.setExpression(list);
    					member.setLeft(seq);
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    
    				} else {
    					ArrayList<PExpression> list = new ArrayList<>();
    					for (int j = 0; j < params[i].length; j++) {
    						FormalParamNode param = params[i][j];
    						list.add(createIdentifierNode(param));
    					}
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(new ACoupleExpression(list));
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    				}
    			} else {
    				for (int j = 0; j < params[i].length; j++) {
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(createIdentifierNode(params[i][j]));
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    				}
    			}
    		}
    		return createConjunction(predList);
    	}
    
    	public PPredicate visitBoundsOfFunctionsVariables(OpApplNode n) {
    		FormalParamNode[][] params = n.getBdedQuantSymbolLists();
    		ExprNode[] in = n.getBdedQuantBounds();
    		boolean[] isTuple = n.isBdedQuantATuple();
    
    		List<PPredicate> predList = new ArrayList<>();
    		for (int i = 0; i < params.length; i++) {
    			if (isTuple[i]) {
    				if (params[i].length == 1) { // one-tuple is handled as a
    					// sequence
    					FormalParamNode param = params[i][0];
    					param.setToolObject(TUPLE, params[i]);
    
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(createIdentifierNode(param));
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    
    				} else if (i == 0) {
    					ArrayList<PExpression> list = new ArrayList<>();
    					for (int j = 0; j < params[i].length; j++) {
    						FormalParamNode param = params[i][j];
    						list.add(createIdentifierNode(param));
    					}
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(new ACoupleExpression(list));
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    				} else {
    					ArrayList<PExpression> list = new ArrayList<>();
    					StringBuilder sb = new StringBuilder();
    					for (int j = 0; j < params[i].length; j++) {
    						FormalParamNode param = params[i][j];
    						if (i > 0) { // do not use prj1 & prj2 if it is the
    							// first tuple
    							param.setToolObject(TUPLE, params[i]);
    						}
    						sb.append(param.getName().toString());
    						list.add(createIdentifierNode(param));
    					}
    					PExpression id = createIdentifierNode(sb.toString());
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(id);
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    				}
    			} else {
    				for (int j = 0; j < params[i].length; j++) {
    					AMemberPredicate member = new AMemberPredicate();
    					member.setLeft(createIdentifierNode(params[i][j]));
    					member.setRight(visitExprNodeExpression(in[i]));
    					predList.add(member);
    				}
    			}
    		}
    		return createConjunction(predList);
    	}
    
    	public PPredicate visitExprOrOpArgNodePredicate(ExprOrOpArgNode n) {
    		if (n instanceof ExprNode) {
    			return visitExprNodePredicate((ExprNode) n);
    		} else {
    			throw new RuntimeException("OpArgNode not implemented jet");
    		}
    	}
    
    	public PExpression visitExprOrOpArgNodeExpression(ExprOrOpArgNode n) {
    		if (n instanceof ExprNode) {
    			return visitExprNodeExpression((ExprNode) n);
    		} else {
    			throw new RuntimeException("OpArgNode not implemented jet");
    		}
    	}
    
    	public static AIdentifierExpression createIdentifierNode(String name) {
    		return new AIdentifierExpression(createTIdentifierLiteral(name));
    	}
    
    	public PPredicate createConjunction(List<PPredicate> list) {
    		if (list.size() == 1)
    			return list.get(0);
    		AConjunctPredicate conj = new AConjunctPredicate();
    		conj.setLeft(list.get(0));
    		for (int i = 1; i < list.size(); i++) {
    			if (i < list.size() - 1) {
    				AConjunctPredicate old = conj;
    				old.setRight(list.get(i));
    				conj = new AConjunctPredicate();
    				conj.setLeft(old);
    			} else {
    				conj.setRight(list.get(i));
    			}
    		}
    		return conj;
    	}
    
    	private PPredicate createDisjunction(List<PPredicate> list) {
    		if (list.size() == 1)
    			return list.get(0);
    		ADisjunctPredicate disjunction = new ADisjunctPredicate();
    		disjunction.setLeft(list.get(0));
    		for (int i = 1; i < list.size(); i++) {
    			if (i < list.size() - 1) {
    				disjunction.setRight(list.get(i));
    				disjunction = new ADisjunctPredicate(disjunction, null);
    			} else {
    				disjunction.setRight(list.get(i));
    			}
    		}
    		return disjunction;
    	}
    
    	public static List<TIdentifierLiteral> createTIdentifierLiteral(String name) {
    		List<TIdentifierLiteral> list = new ArrayList<>();
    		TIdentifierLiteral tid = new TIdentifierLiteral(name);
    		list.add(tid);
    		return list;
    	}
    
    	public static List<PExpression> createPexpressionList(PExpression expr) {
    		ArrayList<PExpression> list = new ArrayList<>();
    		list.add(expr);
    		return list;
    	}
    
    	public Start getStartNode() {
    		return start;
    	}
    
    	public Definitions getBDefinitions() {
    		// used for the recursive machine loader
    		return bDefinitions;
    	}
    
    	public Hashtable<Node, TLAType> getTypeTable() {
    		return this.typeTable;
    	}
    
    	public HashSet<PositionedNode> getSourcePositions() {
    		return this.sourcePosition;
    	}
    
    	public List<String> getUnchangedVariablesNames() {
    		return toplevelUnchangedVariableNames;
    	}
    
    	public void setUnchangedVariablesNames(List<String> unchangedVariablesNames) {
    		this.toplevelUnchangedVariableNames = unchangedVariablesNames;
    	}
    
    }