From 1baba5f119c882160459da01e781416f6c8e7333 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 4 Jul 2014 13:40:23 +0200
Subject: [PATCH] Fixed a precedence bug
---
build.xml | 1 +
.../tlc4b/analysis/PrecedenceCollector.java | 4 ++
.../typerestriction/TypeRestrictor.java | 49 ++++++++++++++++++-
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 2 +-
.../tlc4b/analysis/TypeRestrictionsTest.java | 13 +++++
5 files changed, 67 insertions(+), 2 deletions(-)
diff --git a/build.xml b/build.xml
index 47a9188..52dcde6 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 caabfa8..5033f9b 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 fb9174a..435f47d 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 8f9eff5..c1e861c 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 174c601..afa83cc 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);
+ }
+
}
--
GitLab