From f907e1524c48740d4a3874a9bd08136368bcccdd Mon Sep 17 00:00:00 2001 From: hansen <dominik_hansen@web.de> Date: Thu, 22 May 2014 13:25:00 +0200 Subject: [PATCH] Do not clone nodes, because the clones do not contain all required information (type etc.) --- src/main/java/de/tlc4b/analysis/Typechecker.java | 9 +++++---- src/main/java/de/tlc4b/tla/Generator.java | 2 +- .../java/de/tlc4b/tlc/integration/SpecialTest.java | 8 ++++++++ src/test/java/de/tlc4b/util/TLC4BTester.java | 2 +- src/test/resources/special/ConstantsSetup2.mch | 10 ++++++++++ 5 files changed, 25 insertions(+), 6 deletions(-) create mode 100644 src/test/resources/special/ConstantsSetup2.mch diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index d5939c6..c8595a3 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 cebdacf..d944885 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 ff158fc..180a913 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 438b8c0..651c0e5 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 0000000..ec044dc --- /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 -- GitLab