Skip to content
Snippets Groups Projects
Commit b375a66d authored by hansen's avatar hansen
Browse files

Fixed a bug in the constant eliminator.

parent 6d042348
Branches
Tags
No related merge requests found
...@@ -150,6 +150,7 @@ public class ConstantsEliminator extends DepthFirstAdapter { ...@@ -150,6 +150,7 @@ public class ConstantsEliminator extends DepthFirstAdapter {
for (String key : constants.keySet()) { for (String key : constants.keySet()) {
if (constants.get(key) == id) { if (constants.get(key) == id) {
constantName = key; constantName = key;
break;
} }
} }
constants.remove(constantName); constants.remove(constantName);
...@@ -169,6 +170,12 @@ public class ConstantsEliminator extends DepthFirstAdapter { ...@@ -169,6 +170,12 @@ public class ConstantsEliminator extends DepthFirstAdapter {
Node parentParent = conjunction.parent(); Node parentParent = conjunction.parent();
if (parentParent instanceof APropertiesMachineClause) { if (parentParent instanceof APropertiesMachineClause) {
((APropertiesMachineClause) parentParent).setPredicates(other); ((APropertiesMachineClause) parentParent).setPredicates(other);
}else if (parentParent instanceof AConjunctPredicate){
if (((AConjunctPredicate) parentParent).getLeft() == parent){
((AConjunctPredicate) parentParent).setLeft(other);
}else{
((AConjunctPredicate) parentParent).setRight(other);
}
} }
} else if (parent instanceof APropertiesMachineClause) { } else if (parent instanceof APropertiesMachineClause) {
machineContext.setPropertiesMachineClaus(null); machineContext.setPropertiesMachineClaus(null);
......
...@@ -238,6 +238,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter { ...@@ -238,6 +238,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter {
PExpression left = node.getLeft(); PExpression left = node.getLeft();
Node left_ref = machineContext.getReferences().get(left); Node left_ref = machineContext.getReferences().get(left);
PExpression right = node.getRight(); PExpression right = node.getRight();
System.out.println(node.getStartPos());
Node right_ref = machineContext.getReferences().get(right); Node right_ref = machineContext.getReferences().get(right);
if (left instanceof ACardExpression) { if (left instanceof ACardExpression) {
......
...@@ -103,4 +103,19 @@ public class ConstantsTest { ...@@ -103,4 +103,19 @@ public class ConstantsTest {
compare(expected, machine); compare(expected, machine);
} }
@Test
public void testConstants2() throws Exception {
String machine = "MACHINE test\n"
+ "CONSTANTS N \n"
+ "PROPERTIES N <: NATURAL & N={1,2,3,4}\n"
+ "END";
String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ "N == {1,2,3,4}\n"
+ "ASSUME N \\subseteq Nat \n"
+ "======";
compare(expected, machine);
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment