diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index d5939c6544ac8753e0a7a4e513c8f594a87cb32c..c8595a335e210ca306e0fb9d24c16b7bff5b208a 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -50,14 +50,15 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { this.referenceTable = machineContext.getReferences(); } - public Typechecker(MachineContext c) { + public Typechecker(MachineContext context) { this.types = new Hashtable<Node, BType>(); - this.referenceTable = c.getReferences(); - this.machineContext = c; - c.getTree().apply(this); + this.referenceTable = context.getReferences(); + this.machineContext = context; + context.getTree().apply(this); checkLTLFormulas(); checkConstantsSetup(); + } private void checkLTLFormulas() { diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java index cebdacfd065e4fda30b7643456656a3dbf27a4ea..d944885186b5b731891dca208d553902d356a54b 100644 --- a/src/main/java/de/tlc4b/tla/Generator.java +++ b/src/main/java/de/tlc4b/tla/Generator.java @@ -249,7 +249,7 @@ public class Generator extends DepthFirstAdapter { AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition( con.getIdentifier().get(0), new LinkedList<PExpression>(), - (PExpression) value.clone()); + (PExpression) value);//.clone()); machineContext.addReference(exprDef, con); this.tlaModule.addToAllDefinitions(exprDef); diff --git a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java index ff158fce7be4a80a4c2c73051cab7fbfa9bf6d1c..180a91334c1d5d0a808b42bb8e10abe1316d2a14 100644 --- a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java @@ -34,6 +34,14 @@ public class SpecialTest { } + @Test + public void testConstantSetupFile2() throws Exception { + String[] a = new String[] { + "./src/test/resources/special/ConstantsSetup2.mch", + "-constantsSetup", "a = {(1,TRUE)}" }; + assertEquals(NoError, test(a)); + } + @Test public void testTraceFile() throws Exception { String[] a = new String[] { diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java index 438b8c00fb31fc1c39cc14434fa57270b86b0dc7..651c0e5c249d54e8d92917a10739c159c017ae03 100644 --- a/src/test/java/de/tlc4b/util/TLC4BTester.java +++ b/src/test/java/de/tlc4b/util/TLC4BTester.java @@ -7,7 +7,7 @@ public class TLC4BTester { public static void main(String[] args) throws Exception { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows - TLC4B.test(args,true); + TLC4B.test(args,false); } } diff --git a/src/test/resources/special/ConstantsSetup2.mch b/src/test/resources/special/ConstantsSetup2.mch new file mode 100644 index 0000000000000000000000000000000000000000..ec044dc3f52e3b91276439f23f7df5442841bd71 --- /dev/null +++ b/src/test/resources/special/ConstantsSetup2.mch @@ -0,0 +1,10 @@ +MACHINE ConstantSetup2 +CONSTANTS a +PROPERTIES a : 1..1 --> {TRUE} +VARIABLES x, y +INVARIANT + x : BOOL & y : NAT +INITIALISATION x := a(1) || y := 1 +OPERATIONS +foo = skip +END \ No newline at end of file