diff --git a/build.gradle b/build.gradle index 5d6e98870c561c1cbe16c23b66f7ae4f6bb786fd..7d9929a7a6cbf0fa29dc7673ecd169a68a7c0211 100644 --- a/build.gradle +++ b/build.gradle @@ -26,7 +26,7 @@ configurations.all { resolutionStrategy.cacheChangingModulesFor 0, 'seconds' } -def parser_version = '2.5.1' +def parser_version = '2.5.2-SNAPSHOT' def tlatools_version = '1.0.2-SNAPSHOT' dependencies { diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index 1e438a3123681907661fe1eec768a3466c2a76fc..bf7dcf73f1347eae70672c2c61aa13e403eb4800 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -471,6 +471,20 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { node.getRight().apply(this); } + @Override + public void caseAIfThenElseExpression(AIfThenElseExpression node) { + setType(node.getCondition(), BoolType.getInstance()); + node.getCondition().apply(this); + + UntypedType x = new UntypedType(); + setType(node.getThen(), x); + setType(node.getElse(), x); + node.getThen().apply(this); + node.getElse().apply(this); + BType found = getType(node.getThen()); + unify(getType(node), found, node); + } + @Override public void caseANotEqualPredicate(ANotEqualPredicate node) { try { diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index 8791cb0f10074e827712512142cc03fe8457a661..55687a654ac6ddbff32fe620ffa8c0d8a3fd913b 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -1196,6 +1196,17 @@ public class TLAPrinter extends DepthFirstAdapter { node.getRight().apply(this); outANotEqualPredicate(node); } + + @Override + public void caseAIfThenElseExpression(AIfThenElseExpression node) { + moduleStringAppend("(IF "); + node.getCondition().apply(this); + moduleStringAppend(" THEN "); + node.getThen().apply(this); + moduleStringAppend(" ELSE "); + node.getElse().apply(this); + moduleStringAppend(")"); + } @Override public void caseAConjunctPredicate(AConjunctPredicate node) { diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java index 97c016efb8a6f8a49f768a7a23568b2812266de0..ca2b6c666c923f365ad4b58819f9843a31a06808 100644 --- a/src/main/java/de/tlc4b/tla/Generator.java +++ b/src/main/java/de/tlc4b/tla/Generator.java @@ -70,7 +70,7 @@ public class Generator extends DepthFirstAdapter { evalMachineSets(); evalDefinitions(); evalConstants(); - + evalInvariant(); evalOperations(); evalGoal(); @@ -143,13 +143,12 @@ public class Generator extends DepthFirstAdapter { Node value = idValueTable.get(param); if (value != null) { - tlaModule.tlaDefinitions.add(new TLADefinition(param, value)); + tlaModule.addTLADefinition(new TLADefinition(param, value)); continue; } Integer intValue = constantsEvaluator.getIntValue(param); if (intValue != null) { - tlaModule.tlaDefinitions - .add(new TLADefinition(param, intValue)); + tlaModule.addTLADefinition(new TLADefinition(param, intValue)); continue; } @@ -205,7 +204,7 @@ public class Generator extends DepthFirstAdapter { Node n = itr2.next(); AEnumeratedSetSet e = (AEnumeratedSetSet) n; TLADefinition def = new TLADefinition(e, e); - this.tlaModule.tlaDefinitions.add(def); + this.tlaModule.addTLADefinition(def); List<PExpression> copy = new ArrayList<PExpression>(e.getElements()); for (PExpression element : copy) { this.tlaModule.constants.add(element); diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java index d373d37c99b9e9a37afb1e0b5cdb3ca9f4d5ee46..2135d0cabf3a506bac5888539a90c40cf2fdedd0 100644 --- a/src/main/java/de/tlc4b/tla/TLAModule.java +++ b/src/main/java/de/tlc4b/tla/TLAModule.java @@ -9,14 +9,14 @@ public class TLAModule { protected String moduleName; - protected final ArrayList<TLADefinition> tlaDefinitions; + private final ArrayList<TLADefinition> tlaDefinitions; protected final ArrayList<Node> constants; protected final ArrayList<Node> assumes; protected final ArrayList<Node> variables; protected final ArrayList<Node> invariants; private final ArrayList<Node> initPredicates; protected final ArrayList<POperation> operations; - private ArrayList<PDefinition> bDefinitions; + private ArrayList<PDefinition> bDefinitions; private final ArrayList<Node> assertions; protected ArrayList<PDefinition> allDefinitions; @@ -110,4 +110,7 @@ public class TLAModule { return this.initPredicates.size() > 0; } + public void addTLADefinition(TLADefinition defintion) { + this.tlaDefinitions.add(defintion); + } } diff --git a/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java new file mode 100644 index 0000000000000000000000000000000000000000..399fb6ecc37af9207a0c52eaab751fccf1cb5666 --- /dev/null +++ b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java @@ -0,0 +1,20 @@ +package de.tlc4b.prettyprint; + +import static de.tlc4b.util.TestUtil.compare; + +import org.junit.Test; + + +public class SyntaxExtensionsTest { + + @Test + public void testIfThenElseg() throws Exception { + String machine = "MACHINE test\n" + + "PROPERTIES 1 = (IF 1=1 THEN 1 ELSE 2 END) \n" + "END"; + + String expected = "---- MODULE test----\n" + + "ASSUME 1 = (IF 1 = 1 THEN 1 ELSE 2) \n" + + "======"; + compare(expected, machine); + } +}