Fixed a precedence bug

build.xml

 <project default="copy">
     <target name="copy">
        <copy file="build/tlc4b/TLC4B.jar" tofile="../../Desktop/ProB/lib/TLC4B.jar"/>
+       <copy file="build/tlc4b/TLC4B.jar" tofile="/Users/hansen/git/prob_prolog/lib/TLC4B.jar"/>
     </target>
 </project>
\ No newline at end of file

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

@@ -69,6 +69,10 @@ public class PrecedenceCollector extends DepthFirstAdapter {
 		put("AConcatExpression", 13, 13, true);
 		put("ADivExpression", 13, 13, false);
 		
+		
+		put("AFunctionExpression", 20, 20, false);
+		
+		
 	}
 
 	private Precedence getPrecedence(Node node) {

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

@@ -7,18 +7,21 @@ import java.util.Hashtable;
 import java.util.List;
 import java.util.Set;
 
+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.ABecomesSuchSubstitution;
 import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
+import de.be4.classicalb.core.parser.node.ACoupleExpression;
 import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
 import de.be4.classicalb.core.parser.node.AEqualPredicate;
 import de.be4.classicalb.core.parser.node.AExistsPredicate;
 import de.be4.classicalb.core.parser.node.AForallPredicate;
 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.AImplicationPredicate;
 import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
 import de.be4.classicalb.core.parser.node.AIntersectionExpression;
@@ -46,6 +49,7 @@ import de.be4.ltl.core.parser.node.AForallLtl;
 import de.tlc4b.analysis.MachineContext;
 import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.btypes.BType;
+import de.tlc4b.exceptions.NotSupportedException;
 import de.tlc4b.ltl.LTLFormulaVisitor;
 
 public class TypeRestrictor extends DepthFirstAdapter {
@@ -60,6 +64,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 	private final Hashtable<Node, ArrayList<Node>> restrictedNodeTable;
 	private final Hashtable<Node, ArrayList<Node>> subtractedNodeTable;
 
+	private final Hashtable<Node, ArrayList<Node>> restrictedCoupleTable;
+
 	public Node getRestrictedNode(Node node) {
 		return restrictedTypeNodeTable.get(node);
 	}
@@ -78,6 +84,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 
 		this.restrictedNodeTable = new Hashtable<Node, ArrayList<Node>>();
 		this.subtractedNodeTable = new Hashtable<Node, ArrayList<Node>>();
+		this.restrictedCoupleTable = new Hashtable<Node, ArrayList<Node>>();
 
 		this.identifierDependencies = new IdentifierDependencies(machineContext);
 
@@ -218,6 +225,24 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				putRestrictedType(r_right, new ASetExtensionExpression(element));
 				removedNodes.add(n);
 			}
+			if (left instanceof ACoupleExpression) {
+				ACoupleExpression couple = (ACoupleExpression) left;
+				PExpression first = couple.getList().get(0);
+				Node r_first = machineContext.getReferenceNode(first);
+				PExpression second = couple.getList().get(0);
+				Node r_second = machineContext.getReferenceNode(second);
+
+				if (list.contains(r_first) && list.contains(r_second)
+						&& isAConstantExpression(right, list, ignoreList)) {
+					ArrayList<PExpression> element = new ArrayList<PExpression>();
+					element.add(right);
+					putRestrictedTypeOfTuple(r_right,
+							new ASetExtensionExpression(element));
+					removedNodes.add(n);
+				}
+
+			}
+
 			return;
 		}
 
@@ -299,6 +324,18 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 	}
 
+	private void putRestrictedTypeOfTuple(Node identifier,
+			PExpression restrictedType) {
+		ArrayList<Node> list = restrictedCoupleTable.get(identifier);
+		if (list == null) {
+			list = new ArrayList<Node>();
+			list.add(restrictedType);
+			restrictedCoupleTable.put(identifier, list);
+		} else {
+			list.add(restrictedType);
+		}
+	}
+
 	public boolean isAConstantExpression(Node node, HashSet<Node> list,
 			HashSet<Node> ignoreList) {
 		HashSet<Node> newList = new HashSet<Node>();
@@ -475,7 +512,6 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				node.getIdentifiers()));
 	}
 
-
 	@Override
 	public void inALetSubstitution(ALetSubstitution node) {
 		HashSet<Node> list = new HashSet<Node>();
@@ -520,6 +556,17 @@ public class TypeRestrictor extends DepthFirstAdapter {
 					conType = typechecker.getType(machineContext
 							.getReferenceNode(e));
 				}
+				if (conType.containsIntegerType()) {
+					AIdentifierExpression id = (AIdentifierExpression) e;
+					String localVariableName = Utils.getIdentifierAsString(id
+							.getIdentifier());
+					throw new NotSupportedException(
+							"Can not restrict the type of the variable '"
+									+ localVariableName
+									+ "' to a finite set. TLC is not able to handle infinite sets.\n"
+									+ e.getStartPos());
+				}
+
 				tree = conType.createSyntaxTreeNode(typechecker);
 			} else {
 				tree = (PExpression) restrictedList.get(0);

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

@@ -2,6 +2,7 @@ package de.tlc4b.analysis;
 
 import static de.tlc4b.util.TestUtil.compare;
 
+import org.junit.Ignore;
 import org.junit.Test;
 
 public class TypeRestrictionsTest {
@@ -240,5 +241,17 @@ public class TypeRestrictionsTest {
 		compare(expected, machine);
 	}
 	
+	@Ignore
+	@Test
+	public void testCoupleOfParameters() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES #a,b.( (a,b) : {(1,1)})\n" + "END";
+		
+		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+				+ "ASSUME \\E <<a,b>> \\in {<<1,1>>} : TRUE \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
 	
 }