external definitions files are now supported

src/main/java/de/tlc4b/Translator.java

@@ -5,6 +5,7 @@ import java.io.IOException;
 import java.util.ArrayList;
 
 import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
 import de.be4.classicalb.core.parser.exceptions.BException;
 import de.be4.classicalb.core.parser.node.APredicateParseUnit;
 import de.be4.classicalb.core.parser.node.PPredicate;
@@ -68,6 +69,10 @@ public class Translator {
 		BParser parser = new BParser(machineName);
 		start = parser.parseFile(machineFile, false);
 
+		// Definitions of definitions files are injected in the ast of the main machine
+		final RecursiveMachineLoader rml = new RecursiveMachineLoader(
+				machineFile.getParent(), parser.getContentProvider());
+		rml.loadAllMachines(machineFile, start, null, parser.getDefinitions(), parser.getPragmas());
 		
 		if(constantSetup!= null){
 			BParser con = new BParser();
@@ -93,10 +98,10 @@ public class Translator {
 	}
 
 	public void translate() {
-		new DefinitionsEliminator(start);
-
 		new NotSupportedConstructs(start);
 		
+		new DefinitionsEliminator(start);
+
 		MachineContext machineContext = new MachineContext(machineName, start,
 				ltlFormula, constantsSetup);
 		this.machineName = machineContext.getMachineName();

src/main/java/de/tlc4b/analysis/MachineContext.java

@@ -101,7 +101,6 @@ public class MachineContext extends DepthFirstAdapter {
 	private AConstantsMachineClause constantsMachineClause;
 	private ADefinitionsMachineClause definitionMachineClause;
 	private APropertiesMachineClause propertiesMachineClause;
-	private AVariablesMachineClause variablesMachineClause;
 	private AInvariantMachineClause invariantMachineClause;
 	private AInitialisationMachineClause initialisationMachineClause;
 	private AOperationsMachineClause operationMachineClause;
@@ -437,8 +436,6 @@ public class MachineContext extends DepthFirstAdapter {
 		}
 	}
 
-	// TODO import, include, ..
-
 	@Override
 	public void caseASetsContextClause(ASetsContextClause node) {
 		this.setsMachineClause = node;
@@ -490,7 +487,19 @@ public class MachineContext extends DepthFirstAdapter {
 
 	@Override
 	public void caseAVariablesMachineClause(AVariablesMachineClause node) {
-		this.variablesMachineClause = node;
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			AIdentifierExpression v = (AIdentifierExpression) e;
+			String name = Utils.getIdentifierAsString(v.getIdentifier());
+			exist(v.getIdentifier());
+			variables.put(name, v);
+		}
+	}
+
+	@Override
+	public void caseAConcreteVariablesMachineClause(
+			AConcreteVariablesMachineClause node) {
 		List<PExpression> copy = new ArrayList<PExpression>(
 				node.getIdentifiers());
 		for (PExpression e : copy) {
@@ -724,8 +733,6 @@ public class MachineContext extends DepthFirstAdapter {
 
 	@Override
 	public void caseAAssignSubstitution(AAssignSubstitution node) {
-		// TODO maybe give better feedback to the user, e.g. cannot assign a
-		// value to constant 'c'
 		ArrayList<LinkedHashMap<String, Node>> temp = contextTable;
 		{
 			List<PExpression> copy = new ArrayList<PExpression>(
@@ -788,10 +795,7 @@ public class MachineContext extends DepthFirstAdapter {
 		if (node.getName() != null) {
 			AIdentifierExpression op = (AIdentifierExpression) node.getName();
 			String name = Utils.getIdentifierAsString(op.getIdentifier());
-			Node o = operations.get(name); // TODO operation
-											// of an
-											// external
-			// machine
+			Node o = operations.get(name);
 			if (o != null) {
 				this.referencesTable.put(op, o);
 			} else {
@@ -1060,10 +1064,6 @@ public class MachineContext extends DepthFirstAdapter {
 		this.propertiesMachineClause = propertiesMachineClause;
 	}
 
-	public AVariablesMachineClause getVariablesMachineClause() {
-		return variablesMachineClause;
-	}
-
 	public AInvariantMachineClause getInvariantMachineClause() {
 		return invariantMachineClause;
 	}

src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java

@@ -2,7 +2,14 @@ package de.tlc4b.analysis;
 
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
+import de.be4.classicalb.core.parser.node.AImportsMachineClause;
+import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
+import de.be4.classicalb.core.parser.node.APromotesMachineClause;
+import de.be4.classicalb.core.parser.node.ARefinesModelClause;
+import de.be4.classicalb.core.parser.node.ASeesModelClause;
 import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
+import de.be4.classicalb.core.parser.node.AUsesMachineClause;
 import de.be4.classicalb.core.parser.node.AWhileSubstitution;
 import de.be4.classicalb.core.parser.node.Start;
 import de.tlc4b.exceptions.NotSupportedException;
@@ -13,20 +20,54 @@ public class NotSupportedConstructs extends DepthFirstAdapter{
 		start.apply(this);
 	}
 
-    public void inAWhileSubstitution(AWhileSubstitution node)
-    {
-    	throw new NotSupportedException("While substitutions are currently not supported.");
+	public void inARefinesModelClause(ARefinesModelClause node) {
+		throw new NotSupportedException(
+				"Refines clause is currently not supported.");
 	}
 
-    public void inACaseSubstitution(ACaseSubstitution node)
-    {
-    	throw new NotSupportedException("Case substitutions are currently not supported.");
+	public void inAUsesMachineClause(AUsesMachineClause node) {
+		throw new NotSupportedException(
+				"USES clause is currently not supported.");
 	}
 
-    public void inASequenceSubstitution(ASequenceSubstitution node)
-    {
-    	throw new NotSupportedException("Sequence substitutions ';' are currently not supported.");
+	public void inAPromotesMachineClause(APromotesMachineClause node) {
+		throw new NotSupportedException(
+				"Promotes clause is currently not supported.");
 	}
 
+	public void inASeesModelClause(ASeesModelClause node) {
+		throw new NotSupportedException(
+				"Sees clause is currently not supported.");
+	}
+
+	public void inAIncludesMachineClause(AIncludesMachineClause node) {
+		throw new NotSupportedException(
+				"INCLUDES clause is currently not supported.");
+	}
+
+	public void inAExtendsMachineClause(AExtendsMachineClause node) {
+		throw new NotSupportedException(
+				"EXTENDS clause is currently not supported.");
+	}
+
+	public void inAImportsMachineClause(AImportsMachineClause node) {
+		throw new NotSupportedException(
+				"IMPORTS clause is currently not supported.");
+	}
+
+	public void inAWhileSubstitution(AWhileSubstitution node) {
+		throw new NotSupportedException(
+				"While substitutions are currently not supported.");
+	}
+
+	public void inACaseSubstitution(ACaseSubstitution node) {
+		throw new NotSupportedException(
+				"Case substitutions are currently not supported.");
+	}
+
+	public void inASequenceSubstitution(ASequenceSubstitution node) {
+		throw new NotSupportedException(
+				"Sequence substitutions ';' are currently not supported.");
+	}
 
 }

src/main/java/de/tlc4b/analysis/PrecedenceCollector.java

@@ -5,12 +5,14 @@ import java.util.Hashtable;
 
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
+import de.be4.classicalb.core.parser.node.ADomainExpression;
 import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
 import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
 import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.Start;
 import de.tlc4b.analysis.typerestriction.TypeRestrictor;
 import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.FunctionType;
 import de.tlc4b.btypes.IntegerType;
 
 public class PrecedenceCollector extends DepthFirstAdapter {
@@ -58,7 +60,9 @@ public class PrecedenceCollector extends DepthFirstAdapter {
 		put("AAddExpression", 10, 10, true);
 
 		put("AModuloExpression", 10, 11, true);
+		put("AUnaryMinusExpression", 12, 12, false);
 		put("AConcatExpression", 13, 13, true);
+		put("ADivExpression", 13, 13, false);
 		
 	}
 
@@ -144,6 +148,25 @@ public class PrecedenceCollector extends DepthFirstAdapter {
 		}
 	}
 	
+	@Override
+	public void inADomainExpression(ADomainExpression node)  {
+		BType type = typechecker.getType(node.getExpression());
+
+		Precedence p;
+		if (type instanceof FunctionType) {
+			// Function
+			p = new Precedence("ADomainExpression", 9, 9, false);
+		
+			precedenceTable.put(node, p);
+
+			Precedence parent = precedenceTable.get(node.parent());
+			if (Precedence.makeBrackets(p, parent)) {
+				brackets.add(node);
+			}
+		}
+
+	}
+
 	@Override
 	public void inAMinusOrSetSubtractExpression(
 			AMinusOrSetSubtractExpression node) {

src/main/java/de/tlc4b/analysis/Renamer.java

@@ -10,6 +10,7 @@ import java.util.Map.Entry;
 
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AAnySubstitution;
 import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
 import de.be4.classicalb.core.parser.node.AExistsPredicate;
@@ -19,11 +20,13 @@ import de.be4.classicalb.core.parser.node.AGeneralProductExpression;
 import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.ALambdaExpression;
+import de.be4.classicalb.core.parser.node.ALetSubstitution;
 import de.be4.classicalb.core.parser.node.AOperation;
 import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
 import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
 import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.AVarSubstitution;
 import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.PDefinition;
 import de.be4.classicalb.core.parser.node.PExpression;
@@ -341,6 +344,52 @@ public class Renamer extends DepthFirstAdapter {
 		localContexts.add(context);
 	}
 
+	@Override
+	public void caseAAnySubstitution(AAnySubstitution node) {
+		List<PExpression> list = new ArrayList<PExpression>();
+		list.addAll(node.getIdentifiers());
+		evalBoundedVariables(node, list);
+
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			e.apply(this);
+		}
+		node.getWhere().apply(this);
+		node.getThen().apply(this);
+		removeLastContext();
+	}
+
+	@Override
+	public void caseALetSubstitution(ALetSubstitution node) {
+		List<PExpression> list = new ArrayList<PExpression>();
+		list.addAll(node.getIdentifiers());
+		evalBoundedVariables(node, list);
+
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			e.apply(this);
+		}
+		node.getPredicate().apply(this);
+		node.getSubstitution().apply(this);
+		removeLastContext();
+	}
+
+	@Override
+	public void caseAVarSubstitution(AVarSubstitution node) {
+		List<PExpression> list = new ArrayList<PExpression>();
+		list.addAll(node.getIdentifiers());
+		evalBoundedVariables(node, list);
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			e.apply(this);
+		}
+		node.getSubstitution().apply(this);
+		removeLastContext();
+	}
+
 	public void removeLastContext() {
 		localContexts.remove(localContexts.size() - 1);
 	}

src/main/java/de/tlc4b/analysis/StandardMadules.java

@@ -143,6 +143,8 @@ public final class StandardMadules {
 	public static final String REL_SEQUENCE_SIZE = "RelSeqSize";
 	public static final String IS_REL_SEQUENCE = "isRelSeq";
 	public static final String REL_SEQUENCE_SET = "RelSeqSet";
+	public static final String REL_SET_OF_SEQUENCES = "RelSeq";
+	public static final String REL_SET_OF_NON_EMPTY_SEQUENCES = "RelSeq1";
 	public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
 	public static final String REL_SEQUENCE_1_SET = "RelSeqSet1";
 	public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";

src/main/java/de/tlc4b/analysis/Typechecker.java

@@ -57,6 +57,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		c.getTree().apply(this);
 
 		checkLTLFormulas();
+		checkConstantsSetup();
 	}
 
 	private void checkLTLFormulas() {
@@ -76,6 +77,23 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 
 	}
 	
+	private void checkConstantsSetup() {
+		PPredicate p = machineContext.getConstantsSetup();
+		if (p != null) {
+			setType(p, BoolType.getInstance());
+			p.apply(this);
+			for (Entry<String, Node> entry : machineContext.getConstants()
+					.entrySet()) {
+				String c = entry.getKey();
+				Node n = entry.getValue();
+				if (getType(n).isUntyped()) {
+					throw new TypeErrorException("Can not infer type of constant '"
+							+ c + "': " + getType(n));
+				}
+			}
+		}
+	}
+
 	@Override
 	public void caseAPredicateParseUnit(APredicateParseUnit node) {
 		setType(node.getPredicate(), BoolType.getInstance());
@@ -198,6 +216,18 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		}
 	}
 	
+	@Override
+	public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			AIdentifierExpression v = (AIdentifierExpression) e;
+			UntypedType u = new UntypedType();
+			setType(v, u);
+		}
+	}
+	
+	
 	/**
 	 * Definitions
 	 */

src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java

@@ -4,6 +4,7 @@ import java.util.Hashtable;
 
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
 import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
 import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
@@ -26,16 +27,25 @@ import de.be4.classicalb.core.parser.node.Start;
 public class DefinitionCollector extends DepthFirstAdapter {
 
 	private Hashtable<String, PDefinition> definitionsTable;
+	private ADefinitionsMachineClause definitionsMachineClause;
 
 	public Hashtable<String, PDefinition> getDefinitions(){
 		return new Hashtable<String, PDefinition>(definitionsTable);
 	}
+	public ADefinitionsMachineClause getDefinitionsMachineClause(){
+		return this.definitionsMachineClause;
+	}
 	
 	public DefinitionCollector(Start tree) {
 		definitionsTable = new Hashtable<String, PDefinition>();
 		tree.apply(this);
 	}
 	
+	@Override
+	public void inADefinitionsMachineClause(ADefinitionsMachineClause node) {
+		this.definitionsMachineClause = node;
+	}
+	
 
 	@Override
 	public void caseAPredicateDefinitionDefinition(

src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java

@@ -63,16 +63,26 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 		List<PDefinition> copy = new ArrayList<PDefinition>(
 				node.getDefinitions());
 		for (PDefinition e : copy) {
+			if (e instanceof AExpressionDefinitionDefinition) {
+				String name = ((AExpressionDefinitionDefinition) e).getName()
+						.getText().toString();
+				if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")
+						|| name.startsWith("SET_PREF_")
+						|| name.startsWith("ANIMATION_FUNCTION"))
+					continue;
+			}
 			e.apply(this);
 		}
 		for (PDefinition e : copy) {
 			if (e instanceof AExpressionDefinitionDefinition) {
 				String name = ((AExpressionDefinitionDefinition) e).getName()
 						.getText().toString();
-				if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")|| name.startsWith("SET_PREF_"))
+				if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_")
+						|| name.startsWith("SET_PREF_"))
 					continue;
 			} else if (e instanceof APredicateDefinitionDefinition) {
-				String name = ((APredicateDefinitionDefinition) e).getName().getText().toString();
+				String name = ((APredicateDefinitionDefinition) e).getName()
+						.getText().toString();
 				if (name.equals("GOAL"))
 					continue;
 			}
@@ -124,7 +134,6 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 			context.put(paramName, node.getParameters().get(i));
 		}
 		contextStack.add(context);
-		
 		clone.getRhs().apply(this);
 		node.replaceBy(clone.getRhs());
 		contextStack.remove(context);
@@ -154,7 +163,6 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 		clone.getRhs().apply(this);
 		node.replaceBy(clone.getRhs());
 
-
 		contextStack.remove(context);
 	}
 

src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java

@@ -198,6 +198,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 
 			if (list.contains(r_left)
 					&& isAConstantExpression(right, list, ignoreList)) {
+				right.apply(this);
 				ArrayList<PExpression> element = new ArrayList<PExpression>();
 				element.add(right);
 				if (machineContext.getVariables().values().contains(r_left)) {
@@ -207,9 +208,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				removedNodes.add(n);
 			}
 			if (list.contains(r_right)
-					&& isAConstantExpression(right, list, ignoreList)) {
+					&& isAConstantExpression(left, list, ignoreList)) {
+				left.apply(this);
 				ArrayList<PExpression> element = new ArrayList<PExpression>();
-				element.add(right);
+				element.add(left);
 				if (machineContext.getVariables().values().contains(r_right)) {
 					r_right = variablesHashTable.get(r_right);
 				}
@@ -256,6 +258,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 
 			if (list.contains(r_left)
 					&& isAConstantExpression(right, list, ignoreList)) {
+				right.apply(this);
 				if (machineContext.getVariables().values().contains(r_left)) {
 					r_left = variablesHashTable.get(r_left);
 				}
@@ -268,10 +271,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		if (n instanceof AConjunctPredicate) {
 			Node left = ((AConjunctPredicate) n).getLeft();
 			Node right = ((AConjunctPredicate) n).getRight();
-			analysePredicate(left, list,
-					ignoreList);
-			analysePredicate(right, list,
-					ignoreList);
+			analysePredicate(left, list, ignoreList);
+			analysePredicate(right, list, ignoreList);
 			if (removedNodes.contains(left) && removedNodes.contains(right)) {
 				removedNodes.add(n);
 			}
@@ -474,6 +475,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				node.getIdentifiers()));
 	}
 
+
 	@Override
 	public void inALetSubstitution(ALetSubstitution node) {
 		HashSet<Node> list = new HashSet<Node>();

src/main/java/de/tlc4b/prettyprint/TLAPrinter.java

@@ -1715,7 +1715,8 @@ public class TLAPrinter extends DepthFirstAdapter {
 			tlaModuleString.append("]");
 		} else {
 			if (node.parent() instanceof AMemberPredicate
-					&& !typeRestrictor.isARemovedNode(node.parent())) {
+					&& !typeRestrictor.isARemovedNode(node.parent())
+					&& !this.tlaModule.getInitPredicates().contains(node.parent())) {
 				tlaModuleString.append(REL_TOTAL_FUNCTION_ELEMENT_OF);
 			} else {
 				tlaModuleString.append(REL_TOTAL_FUNCTION);
@@ -1732,8 +1733,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		Node parent = node.parent();
 		if (parent instanceof AMemberPredicate
 				&& !typeRestrictor.isARemovedNode(parent)
-		// && !this.tlaModule.getInitPredicates().contains(parent)
-		) {
+				&& !this.tlaModule.getInitPredicates().contains(parent)) {
 			return true;
 		} else {
 			String clazz = parent.getClass().getName();
@@ -1883,9 +1883,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 			}
 			tlaModuleString.append(")");
 			return;
-
 		}
-
 		tlaModuleString.append("{");
 		{
 			List<PExpression> copy = new ArrayList<PExpression>(
@@ -2461,32 +2459,14 @@ public class TLAPrinter extends DepthFirstAdapter {
 	public void caseASeqExpression(ASeqExpression node) {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
-			if (node.parent() instanceof AMemberPredicate) {
-				AMemberPredicate member = (AMemberPredicate) node.parent();
-				tlaModuleString.append(REL_SEQUENCE_SET);
-				tlaModuleString.append("(");
-				member.getLeft().apply(this);
-				tlaModuleString.append(", ");
-				node.getExpression().apply(this);
-				tlaModuleString.append(")");
-			} else if (node.parent() instanceof ANotMemberPredicate) {
-				ANotMemberPredicate member = (ANotMemberPredicate) node
-						.parent();
-				tlaModuleString.append(REL_SEQUENCE_SET);
-				tlaModuleString.append("(");
-				member.getLeft().apply(this);
-				tlaModuleString.append(", ");
-				node.getExpression().apply(this);
-				tlaModuleString.append(")");
-			}
-
+			tlaModuleString.append(REL_SET_OF_SEQUENCES);
 		} else {
 			tlaModuleString.append("Seq");
+		}
 		tlaModuleString.append("(");
 		node.getExpression().apply(this);
 		tlaModuleString.append(")");
 	}
-	}
 
 	@Override
 	public void caseASizeExpression(ASizeExpression node) {
@@ -2593,32 +2573,14 @@ public class TLAPrinter extends DepthFirstAdapter {
 	public void caseASeq1Expression(ASeq1Expression node) {
 		SetType set = (SetType) typechecker.getType(node);
 		if (set.getSubtype() instanceof SetType) {
-			if (node.parent() instanceof AMemberPredicate) {
-				AMemberPredicate member = (AMemberPredicate) node.parent();
-				tlaModuleString.append(REL_SEQUENCE_1_SET);
-				tlaModuleString.append("(");
-				member.getLeft().apply(this);
-				tlaModuleString.append(", ");
-				node.getExpression().apply(this);
-				tlaModuleString.append(")");
-			} else if (node.parent() instanceof ANotMemberPredicate) {
-				ANotMemberPredicate member = (ANotMemberPredicate) node
-						.parent();
-				tlaModuleString.append(REL_SEQUENCE_1_SET);
-				tlaModuleString.append("(");
-				member.getLeft().apply(this);
-				tlaModuleString.append(", ");
-				node.getExpression().apply(this);
-				tlaModuleString.append(")");
-			}
+			tlaModuleString.append(REL_SET_OF_NON_EMPTY_SEQUENCES);
 		} else {
-
 			tlaModuleString.append(SEQUENCE_1);
+		}
 		tlaModuleString.append("(");
 		node.getExpression().apply(this);
 		tlaModuleString.append(")");
 	}
-	}
 
 	@Override
 	public void caseALastExpression(ALastExpression node) {

src/main/java/de/tlc4b/tla/Generator.java

@@ -10,6 +10,7 @@ import java.util.Map.Entry;
 
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
+import de.be4.classicalb.core.parser.node.AConcreteVariablesMachineClause;
 import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
 import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
 import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
@@ -239,7 +240,8 @@ public class Generator extends DepthFirstAdapter {
 			return;
 		LinkedHashMap<Node, Node> conValueTable = constantsEvaluator
 				.getValueOfIdentifierMap();
-		Iterator<Entry<Node, Node>> iterator = conValueTable.entrySet().iterator();
+		Iterator<Entry<Node, Node>> iterator = conValueTable.entrySet()
+				.iterator();
 		while (iterator.hasNext()) {
 			Entry<Node, Node> entry = iterator.next();
 			AIdentifierExpression con = (AIdentifierExpression) entry.getKey();
@@ -259,7 +261,7 @@ public class Generator extends DepthFirstAdapter {
 
 		Node propertiesPerdicate = machineContext.getPropertiesMachineClause()
 				.getPredicates();
-		if (remainingConstants.size() != 0) {
+		if (remainingConstants.size() > 0) {
 			boolean init = false;
 			int numberOfIteratedConstants = 0;
 
@@ -302,8 +304,11 @@ public class Generator extends DepthFirstAdapter {
 			}
 
 		} else {
-			tlaModule.assumes.addAll(constantsEvaluator.getPropertiesList());
-			// tlaModule.addAssume(propertiesPerdicate);
+			if (machineContext.getConstantsSetup() == null){
+				tlaModule.assumes
+				.addAll(constantsEvaluator.getPropertiesList());
+			}
+			tlaModule.addAssume(propertiesPerdicate);
 		}
 
 	}
@@ -324,6 +329,15 @@ public class Generator extends DepthFirstAdapter {
 		}
 	}
 	
+	@Override
+	public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		for (PExpression e : copy) {
+			this.tlaModule.variables.add(e);
+		}
+	}
+
 	@Override
 	public void inAAssertionsMachineClause(AAssertionsMachineClause node) {
 		List<PPredicate> copy = new ArrayList<PPredicate>(node.getPredicates());

src/main/resources/standardModules/SequencesAsRelations.tla

@@ -6,11 +6,23 @@ IsRelSeq(x, S) == \A n \in 1..Cardinality(x): RelCall(x,n) \in S
 
 RelSeqSet(x, S) == IF IsRelSeq(x,S) THEN {x} ELSE {}
 
+RelSeq(S) == {p \in SUBSET(Nat \times S): 
+    LET d == {q[1] : q \in p} 
+    IN /\ Cardinality(p) = Cardinality(d)
+       /\ d = 1..Cardinality(d)}
+
 IsRelSeq1(x, S) == x # {} /\ IsRelSeq(x, S)
  \* Testing if x is a non-empty sequence with elements of the set S
  
 RelSeqSet1(x, S) == IF IsRelSeq1(x,S) THEN {x} ELSE {}
 
+RelSeq1(S) == {p \in SUBSET(Nat \times S): 
+    LET d == {q[1] : q \in p} 
+    IN /\ Cardinality(p) > 0
+       /\ Cardinality(p) = Cardinality(d)
+       /\ d = 1..Cardinality(d)}
+
+
 LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)} 
                         : n \in 0..Cardinality(S)}
                         

src/test/java/de/tlc4b/tlc/integration/SpecialTest.java

@@ -42,5 +42,12 @@ public class SpecialTest {
 	}
 	
 	
+	@Test
+	public void testDefinitionsLoad() throws Exception {
+		String[] a = new String[] {
+				"./src/test/resources/special/LoadDefinitions.mch"};
+		assertEquals(NoError, test(a));
+	}
+	
 	
 }

src/test/java/testing/Testing2.java

 package testing;
 
-
 import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
+import static de.tlc4b.util.TestUtil.test;
 
 import java.io.File;
 import java.util.ArrayList;
@@ -28,9 +28,11 @@ public class Testing2 extends AbstractParseMachineTest{
 
 	@Test
 	public void testRunTLC() throws Exception {
-		String[] a = new String[] {machine.getPath()};
+		String[] a = new String[] {
+				machine.getPath()};
 		TLC4B.main(a);
 		//TLC4B.test(a,false);
+		//test(a);
 	}
 
 	@Config

src/test/resources/laws/SequencesAsRelationsTest.mch

@@ -10,6 +10,11 @@ PROPERTIES
 & {} : seq({1+0})
 & {} : seq({})
 
+& {x,y| x : 1..10 & y : {3}} : seq({3})
+& {} \/ {} : seq({1})
+& {x,y| x : 1..10 & y : {3}} : seq1({3})
+& {} \/ {} /: seq1({1})
+
 
 /* Set of sequences */
 & {(1+0,1)} : seq1({1})

src/test/resources/special/Definitions.def

+DEFINITIONS
+d3 == 3;
+d4 == 4;
\ No newline at end of file

src/test/resources/special/LoadDefinitions.mch

+MACHINE LoadDefinitions
+DEFINITIONS
+"Definitions.def";
+d1 == 1;
+d2 == 2;
+PROPERTIES
+d1+ d2 = d3 & d4 = d3 + d1  
+END
\ No newline at end of file