Sequences as relations

build.gradle

@@ -35,7 +35,8 @@ dependencies {
 
 
 test { 
-	exclude('de/b2tla/tlc/integration/**')
+	exclude('de/b2tla/tlc/integration/probprivate')
+	exclude('de/b2tla/tlc/integration/testing')
 }
 
 

src/main/java/de/b2tla/B2TLA.java

@@ -226,6 +226,24 @@ public class B2TLA {
 				STANDARD_MODULES.SequencesAsRelations)) {
 			createStandardModule(path,
 					STANDARD_MODULES.SequencesAsRelations.toString());
+			
+			if (!translator.getUsedStandardModule().contains(
+					STANDARD_MODULES.Relations)) {
+				createStandardModule(path,
+						STANDARD_MODULES.Relations.toString());
+			}
+			
+			if (!translator.getUsedStandardModule().contains(
+					STANDARD_MODULES.FunctionsAsRelations)) {
+				createStandardModule(path,
+						STANDARD_MODULES.FunctionsAsRelations.toString());
+			}
+			
+			if (!translator.getUsedStandardModule().contains(
+					STANDARD_MODULES.Functions)) {
+				createStandardModule(path,
+						STANDARD_MODULES.Functions.toString());
+			}
 		}
 	}
 

src/main/java/de/b2tla/TLCRunner.java

@@ -70,8 +70,7 @@ public class TLCRunner {
 
 		String[] args = list.toArray(new String[list.size()]);
 		System.out.println("Starting JVM...");
-		Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
-
+		final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
 		
 		StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
 		stdOut.start();

src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java

@@ -12,6 +12,7 @@ import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.AIntegerExpression;
 import de.be4.classicalb.core.parser.node.AIntervalExpression;
+import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
 import de.be4.classicalb.core.parser.node.Node;
 
 /**
@@ -93,11 +94,19 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
 		if (null != node) {
 			try {
 				AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
-				AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
-				int value = Integer.parseInt(sizeExpr.getLiteral().getText());
+				AIntegerExpression sizeExpr = null;
+				Integer value = null;
+				if (d.getRhs() instanceof AUnaryMinusExpression){
+					AUnaryMinusExpression minus = (AUnaryMinusExpression) d.getRhs();
+					sizeExpr = (AIntegerExpression) minus.getExpression();
+					value = - Integer.parseInt(sizeExpr.getLiteral().getText());
+				}else{
+					sizeExpr = (AIntegerExpression) d.getRhs();
+					value = Integer.parseInt(sizeExpr.getLiteral().getText());
+				}
 				B2TLAGlobals.setMIN_INT(value);
 			} catch (ClassCastException e) {
-
+				e.printStackTrace();
 			}
 		}
 	}

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

@@ -83,8 +83,26 @@ public class StandardMadules {
 	public static final String SEQUENCE_TAKE_FIRST_ELEMENTS = "TakeFirstElements";
 	public static final String SEQUENCE_DROP_FIRST_ELEMENTS = "DropFirstElements";
 
-	public static final String REL_INJECTIVE_SEQUENCES = "RelISeq";
-	public static final String REL_NOT_EMPTY_INJECTIVE_SEQUENCES = "RelISeq1";
+
+	
+	// SequencesAsRelations
+	public static final String REL_SEQUENCE_SIZE = "RelSeqSize";
+	public static final String IS_REL_SEQUENCE = "isRelSeq";
+	public static final String IS_REL_SEQUENCE_1 = "isRelSeq1";
+	public static final String REL_INJECTIVE_SEQUENCE = "RelISeq";
+	public static final String REL_INJECTIVE_SEQUENCE_1 = "RelISeq1";
+	public static final String REL_SEQUENCE_Concat = "RelSeqConcat";
+	public static final String REL_SEQUENCE_PREPAND = "RelSeqPrepand";
+	public static final String REL_SEQUENCE_APPEND = "RelSeqAppend";
+	public static final String REL_SEQUENCE_REVERSE = "RelSeqRev";
+	public static final String REL_SEQUENCE_FIRST_ELEMENT = "RelSeqFirst";
+	public static final String REL_SEQUENCE_LAST_ELEMENT = "RelSeqLast";
+	public static final String REL_SEQUENCE_FRONT = "RelSeqFront";
+	public static final String REL_SEQUENCE_TAIL = "RelSeqTail";
+	public static final String REL_SEQUENCE_PERM = "RelSeqPerm";
+	public static final String REL_SEQUENCE_GENERAL_CONCATINATION = "RelSeqConc";
+	public static final String REL_SEQUENCE_TAKE_FIRST_ELEMENTS = "RelSeqTakeFirstElements";
+	public static final String REL_SEQUENCE_DROP_FIRST_ELEMENTS = "RelSeqDropFirstElements";
 	
 	/*
 	 * BBuiltIns

src/main/java/de/b2tla/analysis/TypeRestrictor.java

@@ -68,15 +68,17 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				Node bNode = visitor.getBAst(ltlNode);
 
 				if (ltlNode instanceof AExistsLtl) {
-					Node id = visitor.getLTLIdentifier(((AExistsLtl) ltlNode).getExistsIdentifier().getText());
+					Node id = visitor.getLTLIdentifier(((AExistsLtl) ltlNode)
+							.getExistsIdentifier().getText());
 					HashSet<Node> list = new HashSet<Node>();
 					list.add(id);
-					analysePredicate(bNode, list);
+					analysePredicate(bNode, list, new HashSet<Node>());
 				} else if (ltlNode instanceof AForallLtl) {
-					Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode).getForallIdentifier().getText());
+					Node id = visitor.getLTLIdentifier(((AForallLtl) ltlNode)
+							.getForallIdentifier().getText());
 					HashSet<Node> list = new HashSet<Node>();
 					list.add(id);
-					analysePredicate(bNode, list);
+					analysePredicate(bNode, list, new HashSet<Node>());
 				}
 				bNode.apply(this);
 			}
@@ -113,24 +115,25 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		HashSet<Node> list = new HashSet<Node>();
 		list.addAll(machineContext.getSetParamter().values());
 		list.addAll(machineContext.getScalarParameter().values());
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	@Override
 	public void inAPropertiesMachineClause(APropertiesMachineClause node) {
 		HashSet<Node> list = new HashSet<Node>();
 		list.addAll(machineContext.getConstants().values());
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
-	private void analysePredicate(Node n, HashSet<Node> list) {
+	private void analysePredicate(Node n, HashSet<Node> list, HashSet<Node> ignoreList) {
 		if (n instanceof AEqualPredicate) {
 			PExpression left = ((AEqualPredicate) n).getLeft();
 			Node r_left = machineContext.getReferences().get(left);
 			PExpression right = ((AEqualPredicate) n).getRight();
 			Node r_right = machineContext.getReferences().get(right);
 
-			if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+			if (list.contains(r_left)
+					&& isAConstantExpression(right, list, ignoreList)) {
 				EqualsNode setNode = new EqualsNode(right);
 				putRestrictedType(r_left, setNode);
 				if (!machineContext.getConstants().containsValue(r_left)) {
@@ -138,7 +141,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				}
 
 			}
-			if (list.contains(r_right) && !identifierDependencies.containsIdentifier(left, list)) {
+			if (list.contains(r_right)
+					&& isAConstantExpression(right, list, ignoreList)) {
 				EqualsNode setNode = new EqualsNode(left);
 				putRestrictedType(r_right, setNode);
 				if (!machineContext.getConstants().containsValue(r_left)) {
@@ -152,7 +156,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			PExpression left = ((AMemberPredicate) n).getLeft();
 			Node r_left = machineContext.getReferences().get(left);
 			PExpression right = ((AMemberPredicate) n).getRight();
-			if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+			if (list.contains(r_left)
+					&& isAConstantExpression(right, list, ignoreList)) {
 				putRestrictedType(r_left, new ElementOfNode(right));
 				if (!machineContext.getConstants().containsValue(r_left)) {
 					removedNodes.add(n);
@@ -166,7 +171,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			Node r_left = machineContext.getReferences().get(left);
 			PExpression right = ((ASubsetPredicate) n).getRight();
 
-			if (list.contains(r_left) && !identifierDependencies.containsIdentifier(right, list)) {
+			if (list.contains(r_left)
+					&& isAConstantExpression(right, list, ignoreList)) {
 				putRestrictedType(r_left, new SubsetNode(right));
 				if (!machineContext.getConstants().containsValue(r_left)) {
 					removedNodes.add(n);
@@ -176,21 +182,40 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 
 		if (n instanceof AConjunctPredicate) {
-			analysePredicate(((AConjunctPredicate) n).getLeft(), list);
-			analysePredicate(((AConjunctPredicate) n).getRight(), list);
+			analysePredicate(((AConjunctPredicate) n).getLeft(), list, ignoreList);
+			analysePredicate(((AConjunctPredicate) n).getRight(), list, ignoreList);
 			return;
 		}
 
+		if (n instanceof AExistsPredicate) {
+			HashSet<Node> set = new HashSet<Node>();
+			for (PExpression e : ((AExistsPredicate) n).getIdentifiers()) {
+				set.add(e);
+			}
+			set.addAll(ignoreList);
+			analysePredicate(((AExistsPredicate) n).getPredicate(), list, set);
+		}
+
 		if (n instanceof Start) {
-			analysePredicate(((Start) n).getPParseUnit(), list);
+			analysePredicate(((Start) n).getPParseUnit(), list, ignoreList);
 		}
 
 		if (n instanceof APredicateParseUnit) {
-			analysePredicate(((APredicateParseUnit) n).getPredicate(), list);
+			analysePredicate(((APredicateParseUnit) n).getPredicate(), list, ignoreList);
 			return;
 		}
 	}
 	
+	public boolean isAConstantExpression(Node node, HashSet<Node> list, HashSet<Node> ignoreList){
+		HashSet<Node> newList = new HashSet<Node>();
+		newList.addAll(list);
+		newList.addAll(ignoreList);
+		if(identifierDependencies.containsIdentifier(node, newList)){
+			return false;
+		}
+		return true;
+	}
+
 	@Override
 	public void inAForallPredicate(AForallPredicate node) {
 		HashSet<Node> list = new HashSet<Node>();
@@ -201,7 +226,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 		AImplicationPredicate implication = (AImplicationPredicate) node
 				.getImplication();
-		analysePredicate(implication.getLeft(), list);
+		analysePredicate(implication.getLeft(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -212,7 +237,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicate(), list);
+		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -223,7 +248,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -235,7 +260,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -247,7 +272,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 			// e.apply(this);
 		}
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -258,7 +283,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicate(), list);
+		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
 	}
 
 	public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -268,7 +293,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -278,7 +303,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (PExpression e : copy) {
 			list.add(e);
 		}
-		analysePredicate(node.getPredicates(), list);
+		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
 	}
 
 	private Hashtable<Node, HashSet<Node>> expectedIdentifieListTable = new Hashtable<Node, HashSet<Node>>();
@@ -317,7 +342,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 	@Override
 	public void inAPreconditionSubstitution(APreconditionSubstitution node) {
 		HashSet<Node> list = getExpectedIdentifier(node);
-		analysePredicate(node.getPredicate(), list);
+		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
 	}
 
 	private HashSet<Node> getExpectedIdentifier(Node node) {
@@ -330,7 +355,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 	@Override
 	public void inASelectSubstitution(ASelectSubstitution node) {
 		HashSet<Node> list = getExpectedIdentifier(node);
-		analysePredicate(node.getCondition(), list);
+		analysePredicate(node.getCondition(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -342,7 +367,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		list.addAll(getExpectedIdentifier(node));
-		analysePredicate(node.getWhere(), list);
+		analysePredicate(node.getWhere(), list, new HashSet<Node>());
 	}
 
 	@Override
@@ -354,7 +379,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		list.addAll(getExpectedIdentifier(node));
-		analysePredicate(node.getPredicate(), list);
+		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
 	}
 
 }

src/main/java/de/b2tla/analysis/UsedStandardModules.java

@@ -105,7 +105,8 @@ import de.be4.classicalb.core.parser.node.PExpression;
 public class UsedStandardModules extends DepthFirstAdapter {
 
 	public static enum STANDARD_MODULES {
-		Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations
+		Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations,
+		FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations,
 	}
 
 	private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<UsedStandardModules.STANDARD_MODULES>();
@@ -569,64 +570,88 @@ public class UsedStandardModules extends DepthFirstAdapter {
 	}
 
 	public void inAFirstExpression(AFirstExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.Sequences);
+		evalSequenceOrRelation(node);
 	}
 
 	public void inATailExpression(ATailExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.Sequences);
+		evalSequenceOrRelation(node);
 	}
 
 	/**
 	 * SequencesExtended
 	 */
 
+	private void evalSequenceExtendedOrRelation(Node node){
+		BType type = typechecker.getType(node);
+		if (type instanceof FunctionType) {
+			usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		} else {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		}
+	}
+	
 	public void inAIseqExpression(AIseqExpression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof FunctionType) {
 			usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		} else {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		}
 	}
 
 	public void inASeq1Expression(ASeq1Expression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof FunctionType) {
 			usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		} else {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		}
 	}
 
-	public void inAInsertFrontExpression(AInsertFrontExpression node) {
+	public void inAIseq1Expression(AIseq1Expression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof FunctionType) {
 			usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		} else {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		}
+	}
+	
+	public void inAInsertFrontExpression(AInsertFrontExpression node) {
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inALastExpression(ALastExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inAFrontExpression(AFrontExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inAPermExpression(APermExpression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof SetType) {
+			usedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
+		} else {
 			usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
 		}
+	}
 
 	public void inARevExpression(ARevExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inAGeneralConcatExpression(AGeneralConcatExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inARestrictFrontExpression(ARestrictFrontExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 	public void inARestrictTailExpression(ARestrictTailExpression node) {
-		usedStandardModules.add(STANDARD_MODULES.SequencesExtended);
-	}
-
-	/**
-	 * sonst
-	 * 
-	 */
-
-	public void inAIseq1Expression(AIseq1Expression node) {
-		usedStandardModules.add(STANDARD_MODULES.Relations);
+		evalSequenceExtendedOrRelation(node);
 	}
 
 }

src/main/java/de/b2tla/btypes/IntegerType.java

 package de.b2tla.btypes;
 
+import de.b2tla.B2TLAGlobals;
 import de.b2tla.analysis.Typechecker;
 import de.b2tla.exceptions.UnificationException;
 import de.be4.classicalb.core.parser.node.AIntegerExpression;
@@ -41,9 +42,11 @@ public class IntegerType implements BType {
 	}
 	
 	public String getTlaType() {
-		return "Int";
+		return B2TLAGlobals.getMIN_INT() + ".." + B2TLAGlobals.getMAX_INT();
 	}
 
+	
+	
 	public boolean isUntyped() {
 		return false;
 	}

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

@@ -23,7 +23,6 @@ import de.b2tla.btypes.FunctionType;
 import de.b2tla.btypes.IntegerType;
 import de.b2tla.btypes.PairType;
 import de.b2tla.btypes.SetType;
-import de.b2tla.btypes.UntypedType;
 import de.b2tla.ltl.LTLFormulaVisitor;
 import de.b2tla.tla.ConfigFile;
 import de.b2tla.tla.TLADefinition;
@@ -196,11 +195,13 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 		}
 
+		if (B2TLAGlobals.isCheckltl()) {
 			for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
-			LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas().get(
-					i);
-			this.configFileString.append("PROPERTIES " + ltlVisitor.getName()
-					+ "\n");
+				LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas()
+						.get(i);
+				this.configFileString.append("PROPERTIES "
+						+ ltlVisitor.getName() + "\n");
+			}
 		}
 
 		// CONSTANTS
@@ -1620,7 +1621,8 @@ public class TLAPrinter extends DepthFirstAdapter {
 				&& !typeRestrictor.removeNode(parent)) {
 			return true;
 		} else {
-			if (parent instanceof ATotalFunctionExpression) {
+			String clazz = parent.getClass().getName();
+			if (clazz.contains("Total") || clazz.contains("Partial")) {
 				return isElementOf(node.parent());
 			} else
 				return false;
@@ -2244,45 +2246,63 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseASizeExpression(ASizeExpression node) {
-		tlaModuleString.append("Len");
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), "Len", REL_SEQUENCE_SIZE,
+				node.getExpression(), null);
 	}
 
 	@Override
 	public void caseAConcatExpression(AConcatExpression node) {
+		BType type = typechecker.getType(node);
+		if (type instanceof SetType) {
+			tlaModuleString.append(REL_SEQUENCE_Concat);
+			tlaModuleString.append("(");
+			node.getLeft().apply(this);
+			tlaModuleString.append(", ");
+			node.getRight().apply(this);
+			tlaModuleString.append(")");
+		} else {
 			inAConcatExpression(node);
 			node.getLeft().apply(this);
 			tlaModuleString.append(" \\o ");
 			node.getRight().apply(this);
 			outAConcatExpression(node);
 		}
+	}
 
 	@Override
 	public void caseAInsertTailExpression(AInsertTailExpression node) {
-		tlaModuleString.append("Append");
+		printSequenceOrRelation(node, "Append",
+				REL_SEQUENCE_APPEND, node.getLeft(), node.getRight());
+	}
+
+	private void printSequenceOrRelation(Node node, String sequence,
+			String relation, Node left, Node right) {
+		BType type = typechecker.getType(node);
+		if (type instanceof SetType) {
+			tlaModuleString.append(relation);
+		} else {
+			tlaModuleString.append(sequence);
+		}
 		tlaModuleString.append("(");
-		node.getLeft().apply(this);
+		left.apply(this);
+
+		if (right != null) {
 			tlaModuleString.append(",");
-		node.getRight().apply(this);
+			right.apply(this);
+		}
 		tlaModuleString.append(")");
 	}
 
 	@Override
 	public void caseAFirstExpression(AFirstExpression node) {
-		tlaModuleString.append("Head");
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), "Head",
+				REL_SEQUENCE_FIRST_ELEMENT, node.getExpression(), null);
 	}
 
 	@Override
 	public void caseATailExpression(ATailExpression node) {
-		tlaModuleString.append("Tail");
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), "Tail",
+				REL_SEQUENCE_TAIL, node.getExpression(), null);
 	}
 
 	/**
@@ -2291,12 +2311,17 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseAIseqExpression(AIseqExpression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof SetType) {
+			tlaModuleString.append(REL_INJECTIVE_SEQUENCE);
+		} else {
 			if (node.parent() instanceof AMemberPredicate
 					&& !typeRestrictor.removeNode(node.parent())) {
 				tlaModuleString.append(INJECTIVE_SEQUENCE_ELEMENT_OF);
 			} else {
 				tlaModuleString.append(INJECTIVE_SEQUENCE);
 			}
+		}
 		tlaModuleString.append("(");
 		node.getExpression().apply(this);
 		tlaModuleString.append(")");
@@ -2304,12 +2329,18 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseAIseq1Expression(AIseq1Expression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		System.out.println(set + " " + node.hashCode());
+		if (set.getSubtype() instanceof SetType) {
+			tlaModuleString.append(REL_INJECTIVE_SEQUENCE_1);
+		} else {
 			if (node.parent() instanceof AMemberPredicate
 					&& !typeRestrictor.removeNode(node.parent())) {
 				tlaModuleString.append(INJECTIVE_SEQUENCE_1_ELEMENT_OF);
 			} else {
 				tlaModuleString.append(INJECTIVE_SEQUENCE_1);
 			}
+		}
 		tlaModuleString.append("(");
 		node.getExpression().apply(this);
 		tlaModuleString.append(")");
@@ -2325,25 +2356,24 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseALastExpression(ALastExpression node) {
-		tlaModuleString.append(SEQUENCE_LAST_ELEMENT);
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), SEQUENCE_LAST_ELEMENT,
+				REL_SEQUENCE_LAST_ELEMENT, node.getExpression(), null);
 	}
 
 	@Override
 	public void caseAInsertFrontExpression(AInsertFrontExpression node) {
-		tlaModuleString.append(SEQUENCE_PREPEND_ELEMENT);
-		tlaModuleString.append("(");
-		node.getLeft().apply(this);
-		tlaModuleString.append(", ");
-		node.getRight().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getRight(), SEQUENCE_PREPEND_ELEMENT,
+				REL_SEQUENCE_PREPAND, node.getLeft(), node.getRight());
 	}
 
 	@Override
 	public void caseAPermExpression(APermExpression node) {
+		SetType set = (SetType) typechecker.getType(node);
+		if (set.getSubtype() instanceof SetType) {
+			tlaModuleString.append(REL_SEQUENCE_PERM);
+		} else {
 			tlaModuleString.append(SEQUENCE_PERMUTATION);
+		}
 		tlaModuleString.append("(");
 		node.getExpression().apply(this);
 		tlaModuleString.append(")");
@@ -2351,46 +2381,34 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseARevExpression(ARevExpression node) {
-		tlaModuleString.append(SEQUENCE_REVERSE);
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node, SEQUENCE_REVERSE, REL_SEQUENCE_REVERSE,
+				node.getExpression(), null);
 	}
 
 	@Override
 	public void caseAFrontExpression(AFrontExpression node) {
-		tlaModuleString.append(SEQUENCE_FRONT);
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), SEQUENCE_FRONT,
+				REL_SEQUENCE_FRONT, node.getExpression(), null);
 	}
 
 	@Override
 	public void caseAGeneralConcatExpression(AGeneralConcatExpression node) {
-		tlaModuleString.append(SEQUENCE_GENERAL_CONCATINATION);
-		tlaModuleString.append("(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node.getExpression(), SEQUENCE_GENERAL_CONCATINATION,
+				REL_SEQUENCE_GENERAL_CONCATINATION, node.getExpression(), null);
 	}
 
 	@Override
 	public void caseARestrictFrontExpression(ARestrictFrontExpression node) {
-		tlaModuleString.append(SEQUENCE_TAKE_FIRST_ELEMENTS);
-		tlaModuleString.append("(");
-		node.getLeft().apply(this);
-		tlaModuleString.append(", ");
-		node.getRight().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node, SEQUENCE_TAKE_FIRST_ELEMENTS,
+				REL_SEQUENCE_TAKE_FIRST_ELEMENTS, node.getLeft(),
+				node.getRight());
 	}
 
 	@Override
 	public void caseARestrictTailExpression(ARestrictTailExpression node) {
-		tlaModuleString.append(SEQUENCE_DROP_FIRST_ELEMENTS);
-		tlaModuleString.append("(");
-		node.getLeft().apply(this);
-		tlaModuleString.append(", ");
-		node.getRight().apply(this);
-		tlaModuleString.append(")");
+		printSequenceOrRelation(node, SEQUENCE_DROP_FIRST_ELEMENTS,
+				REL_SEQUENCE_DROP_FIRST_ELEMENTS, node.getLeft(),
+				node.getRight());
 	}
 
 	/**

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

@@ -15,7 +15,6 @@ import de.b2tla.analysis.TypeRestrictor;
 import de.b2tla.analysis.Typechecker;
 import de.b2tla.analysis.nodes.NodeType;
 import de.b2tla.btypes.BType;
-import de.b2tla.btypes.SetType;
 import de.b2tla.tla.config.ModelValueAssignment;
 import de.b2tla.tla.config.SetOfModelValuesAssignment;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
@@ -91,6 +90,7 @@ public class Generator extends DepthFirstAdapter {
 
 	private void evalSpec() {
 		if (this.configFile.isInit() && this.configFile.isNext()
+				&& B2TLAGlobals.isCheckltl()
 				&& machineContext.getLTLFormulas().size() > 0) {
 			this.configFile.setSpec();
 		}

src/main/java/de/b2tla/tlc/TLCOutput.java

@@ -22,7 +22,7 @@ public class TLCOutput {
 	String parseError;
 
 	public static enum TLCResult {
-		Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
+		Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalPropertyError, WellDefinednessError
 	}
 
 	public long getRunningTime() {
@@ -33,7 +33,7 @@ public class TLCOutput {
 	public String getError() {
 		if (error == TLCResult.InvariantViolation) {
 			return "Invariant Violation";
-		} else if (error == TLCResult.TemporalProperty) {
+		} else if (error == TLCResult.TemporalPropertyError) {
 			return "Temporal Property Violation";
 		}
 		return error.toString();
@@ -170,7 +170,7 @@ public class TLCOutput {
 		} else if (res[1].equals("Assumption")) {
 			return TLCResult.PropertiesError;
 		} else if (res[1].equals("Temporal")) {
-			return TLCResult.TemporalProperty;
+			return TLCResult.TemporalPropertyError;
 		} else if (m.equals("Error: TLC threw an unexpected exception.")) {
 			return null;
 		} else if (m.startsWith("\"Error: Invalid function call to relation")) {

src/main/resources/standardModules/SequencesAsRelations.tla

+------------------------ MODULE SequencesAsRelations ------------------------
+EXTENDS FiniteSets, Naturals, Relations, FunctionsAsRelations
+
+isRelSeq(x, S) == \A n \in 1..Cardinality(x): RelCall(x,n) \in S
+
+isRelSeq1(x, S) == x # {} /\ \A n \in 1..Cardinality(x): RelCall(x,n) \in S
+
+
+LOCAL ISeq(S) == UNION { {x \in [(1..n) -> S]: Cardinality(Range(x)) = Cardinality(DOMAIN x)} 
+                        : n \in 0..Cardinality(S)}
+                        
+RelISeq(S) == {{<<n, x[n]>>:n \in 1..Len(x)} :x \in ISeq(S)}
+
+RelISeq1(S) == RelISeq(S) \ {{}}
+
+RelSeqSize(S) == Cardinality(S)
+
+RelSeqConcat(a, b) == a \cup {<<x[1]+Cardinality(a), x[2]>> : x \in b} 
+
+RelSeqPrepand(E, s) == {<<1,E>>} \cup {<<x[1]+1, x[2]>> : x \in s}
+
+RelSeqAppend(s, E) == s \cup {<<Cardinality(s)+ 1,E>>}
+
+RelSeqRev(s) == LET l == Cardinality(s)
+                IN {<<l-x[1]+1, x[2]>>  : x \in s }                
+RelSeqRev2(s) == LET l == Cardinality(s)
+                 IN {<<i, RelCall(s,l-i+1)>>: i \in 1..l}
+                
+RelSeqFirst(s) == RelCall(s, 1)
+
+RelSeqLast(s) == RelCall(s, Cardinality(s))
+
+RelSeqFront(s) == {x \in s : x[1] # Cardinality(s)}
+\*RelSeqFront2(s) == s \ {<<Cardinality(s), RelCall(s, Cardinality(s))>>}
+
+RelSeqTail(s) == {<<x[1]-1,x[2]>> :x \in {x \in s : x[1] # 1}}
+
+RECURSIVE RelSeqPerm(_)
+RelSeqPerm(S) == IF S = {} 
+           THEN {{}}
+           ELSE LET ps == [x \in S |-> {RelSeqAppend(s, x): s \in RelSeqPerm(S\{x})}]
+                IN UNION {ps[x]: x \in S} 
+
+
+RECURSIVE RelSeqConc(_)
+RelSeqConc(S) == IF S = {}
+           THEN {}
+           ELSE RelSeqConcat(RelSeqFirst(S), RelSeqConc(RelSeqTail(S)) )
+
+RelSeqTakeFirstElements(s, n) == IF Assert(n \in 0..Cardinality(s), "Well defineness condition of take-first-operator is violated") 
+                           THEN {x \in s: x[1] \leq n}
+                           ELSE FALSE 
+
+RelSeqDropFirstElements(s, n) == IF Assert(n \in 0..Cardinality(s), "Well defineness condition of drop-first-operator its violated") 
+                           THEN {<<x[1]-n,x[2]>> :x \in {x \in s: x[1] > n}}
+                           ELSE FALSE                 
+=============================================================================
\ No newline at end of file

src/test/java/de/b2tla/prettyprint/ExpressionConstantTest.java → src/test/java/de/b2tla/analysis/ExpressionConstantTest.java

-package de.b2tla.prettyprint;
+package de.b2tla.analysis;
 
 import static de.b2tla.util.TestUtil.compare;
 
@@ -50,7 +50,7 @@ public class ExpressionConstantTest {
 		
 		String expected = "---- MODULE test----\n"
 				+ "EXTENDS Integers \n"
-				+ "ASSUME \\A x \\in Int, y \\in {1} : x = y => 1 = 1 \n"
+				+ "ASSUME \\A x \\in (-1..4), y \\in {1} : x = y => 1 = 1 \n"
 				+ "======";
 		compare(expected, machine);
 	}

src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java

@@ -80,7 +80,7 @@ public class TypeRestrictionsTest {
 				+ "PROPERTIES #x,y.(x = 1 & x = y) \n" + "END";
 		
 		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
-				+ "ASSUME \\E x \\in {1}, y \\in Int: x = y \n"
+				+ "ASSUME \\E x \\in {1}, y \\in -1..4: x = y \n"
 				+ "======";
 		compare(expected, machine);
 	}
@@ -116,7 +116,19 @@ public class TypeRestrictionsTest {
 		
 		String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
 				+ "k == 1 \n"
-				+ "ASSUME \\E x \\in Int: \\E y \\in {x}: x = 1 \n"
+				+ "ASSUME \\E x \\in {1} : (\\E y \\in {x} : TRUE) \n"
+				+ "====";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testQuantificationsInSetComprehension() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {1} = {x| #y.(x = 1 & y = x) & 1=1}\n" + "END";
+		
+		String expected = "---- MODULE test ----\n" + "EXTENDS Integers\n"
+				+ "k == 1 \n"
+				+ "ASSUME {1} = {x \\in ({1}): (\\E y \\in {x} : TRUE) /\\ 1 = 1}\n"
 				+ "====";
 		compare(expected, machine);
 	}
@@ -193,7 +205,7 @@ public class TypeRestrictionsTest {
 
 		String expected = "---- MODULE test ----\n"
 				+ "EXTENDS Integers \n"
-				+ "ASSUME \\E x \\in {1}, y \\in Int : y = x \n"
+				+ "ASSUME \\E x \\in {1}, y \\in -1..4 : y = x \n"
 				+ "====";
 		compare(expected, machine);
 	}

src/test/java/de/b2tla/prettyprint/FunctionTest.java

@@ -49,7 +49,7 @@ public class FunctionTest {
 				+ "END";
 		String expected = "---- MODULE test ----\n"
 				+ "EXTENDS Integers\n"
-				+ "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in (Int \\times Int) : a = b} |-> a + b][2, 2]\n"
+				+ "ASSUME 4 = [<<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b} |-> a + b][2, 2]\n"
 				+ "====";
 		compare(expected, machine);
 	}
@@ -75,7 +75,7 @@ public class FunctionTest {
 				+ "END";
 		String expected = "---- MODULE test ----\n"
 				+ "EXTENDS Integers\n"
-				+ "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in (Int \\times Int) : a = b}}\n"
+				+ "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((-1..4) \\times (-1..4)) : a = b}}\n"
 				+ "====";
 		compare(expected, machine);
 	}

src/test/java/de/b2tla/prettyprint/NumbersTest.java

@@ -226,6 +226,41 @@ public class NumbersTest {
 		compare(expected, machine);
 	}
 	
+	@Test
+	public void testMinInt() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES MININT = MININT  \n"
+				+ "END";
+		String expected = "---- MODULE test----\n"
+				+ "EXTENDS Integers\n"
+				+ "ASSUME -1 = -1\n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testMaxInt() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES MAXINT = MAXINT  \n"
+				+ "END";
+		String expected = "---- MODULE test----\n"
+				+ "ASSUME 4 = 4\n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSetComprehensionInt() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {x| 1=1 => x = 1} = {} \n"
+				+ "END";
+		String expected = "---- MODULE test----\n"
+				+ "EXTENDS Integers\n"
+				+ "ASSUME {x \\in (-1..4): 1 = 1 => x = 1} = {}\n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
 	
 	
 }

src/test/java/de/b2tla/prettyprint/SequenceTest.java

-package de.b2tla.prettyprint;
-
-import static de.b2tla.util.TestUtil.compareEquals;
-
-import org.junit.Test;
-
-public class SequenceTest {
-
-	
-	@Test
-	public void testConcatination() throws Exception {
-		String machine = "MACHINE test\n"
-				+ "PROPERTIES {(1,2)}^{(2,2)} = {(1,2),(1,3)} \n" + "END";
-		String expected = "---- MODULE test ----\n"
-				+ "EXTENDS SequencesAsRelations\n"
-				+ "ASSUME {<<1, 2>>} \\o {<<2, 2>>} = {<<1, 2>>, <<1, 3>>}\n"
-				+ "====";
-		compareEquals(expected, machine);
-	}
-}

src/test/java/de/b2tla/tlc/integration/BasicsTest.java

@@ -43,6 +43,7 @@ public class BasicsTest extends AbstractParseMachineTest{
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
 		list.add(new TestPair(NoError, "./src/test/resources/basics"));
+		list.add(new TestPair(NoError, "./src/test/resources/laws"));
 		return getConfiguration(list);
 	}
 }

src/test/java/de/b2tla/tlc/integration/ErrorTest.java

@@ -65,4 +65,10 @@ public class ErrorTest {
 		assertEquals(AssertionError, B2TLA.test(a,true));
 	}
 
+	@Test
+	public void testTemporalPropertyError() throws Exception {
+		String[] a = new String[] { "./src/test/resources/errors/LTLError.mch" };
+		assertEquals(TemporalPropertyError, B2TLA.test(a,true));
+	}
+	
 }

src/test/resources/errors/LTLError.mch

+MACHINE LTLError
+DEFINITIONS
+ASSERT_LTL_1 == "F {x = 11}"
+VARIABLES x
+INVARIANT
+ x : 1..10
+INITIALISATION x:=1
+OPERATIONS
+  Inc = PRE x < 10 THEN x:= x + 1 END;
+  Reset = PRE x = 10 THEN x := 1 END
+END
\ No newline at end of file