diff --git a/build.xml b/build.xml
index 47a9188af65a2cbe6f315938c584579e5c617041..52dcde683431ffdb4ae244df5e3462d21624e571 100644
--- a/build.xml
+++ b/build.xml
@@ -1,5 +1,6 @@
<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
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index caabfa87be2ede1460e6f724ece6795ebbaf8a0e..5033f9bf9ac0ae1ed8e368461626e60dad844e60 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/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) {
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index fb9174a0abbd14b772a095acd3e2ecd8c5a2a800..435f47dc9d7ed573bdd8db6b44d3991ee4d1f348 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/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);
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 8f9eff5e0e2d5cfedeb33f5b2b01878949b473a7..c1e861c23962689b6ff2d3bbde139d178fa15969 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1639,7 +1639,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
@Override
- // Functioncall
+ // Function call
public void caseAFunctionExpression(AFunctionExpression node) {
inAFunctionExpression(node);
diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index 174c60175ca0c8557d6bebefa27a6c1ac5433a78..afa83cc430c763a1f22e67f265ac1ca1affe392d 100644
--- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+++ b/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);
+ }
+
}