diff --git a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java b/src/main/java/de/b2tla/analysis/ConstantsEliminator.java index e2398e6a0e145233a3e6fbb807f1015046dba661..4d47eb7f0f6196006f671d329d60d7d7d1fddc87 100644 --- a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java +++ b/src/main/java/de/b2tla/analysis/ConstantsEliminator.java @@ -150,6 +150,7 @@ public class ConstantsEliminator extends DepthFirstAdapter { for (String key : constants.keySet()) { if (constants.get(key) == id) { constantName = key; + break; } } constants.remove(constantName); @@ -169,6 +170,12 @@ public class ConstantsEliminator extends DepthFirstAdapter { Node parentParent = conjunction.parent(); if (parentParent instanceof APropertiesMachineClause) { ((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) { machineContext.setPropertiesMachineClaus(null); diff --git a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java index f97bc01b9e688a11a7b132214fdfc7c1c4ea737d..477edd5e5000a2fc532f74c4c29f54c226c40ac2 100644 --- a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java +++ b/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java @@ -238,6 +238,7 @@ public class ConstantsEvaluator extends DepthFirstAdapter { PExpression left = node.getLeft(); Node left_ref = machineContext.getReferences().get(left); PExpression right = node.getRight(); + System.out.println(node.getStartPos()); Node right_ref = machineContext.getReferences().get(right); if (left instanceof ACardExpression) { diff --git a/src/test/java/de/b2tla/analysis/ConstantsTest.java b/src/test/java/de/b2tla/analysis/ConstantsTest.java index 56e1dc0001aa5630eebdc94c8af29e1a30f2729f..cea3868c0bb6cbdcd86f96490a80b7e6df5019fb 100644 --- a/src/test/java/de/b2tla/analysis/ConstantsTest.java +++ b/src/test/java/de/b2tla/analysis/ConstantsTest.java @@ -103,4 +103,19 @@ public class ConstantsTest { 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); + } + }