diff --git a/build.gradle b/build.gradle
index e923aec4563860df131604b47fde5c3c9bb55303..0425b65fac5bb18fd99ddef12319fcccf158007e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -42,7 +42,7 @@ test {
task integrationtests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
- include('de/b2tla/tlc/integration/**')
+ include('de/b2tla/tlc/integration/probprivate/**')
}
jar { from sourceSets.main.allJava }
diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/b2tla/TLCRunner.java
index 7d54661dbbca5a4bb19a17facd0bf3ecbd238db7..44e3b38ad478cca8cad9cf1a7c52c9d47b5790de 100644
--- a/src/main/java/de/b2tla/TLCRunner.java
+++ b/src/main/java/de/b2tla/TLCRunner.java
@@ -82,7 +82,6 @@ public class TLCRunner {
} catch (InterruptedException e) {
e.printStackTrace();
}
-
return stdOut.getLog();
}
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
index 5650143078539df7e6ccbc007f90532c89baaedd..be5c79b119d8c9580146e6810f5bda62cc3fb26f 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
@@ -23,6 +23,7 @@ import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
import de.b2tla.btypes.PairType;
import de.b2tla.btypes.SetType;
+import de.b2tla.btypes.UntypedType;
import de.b2tla.ltl.LTLFormulaVisitor;
import de.b2tla.tla.ConfigFile;
import de.b2tla.tla.TLADefinition;
@@ -1590,6 +1591,9 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseATotalFunctionExpression(ATotalFunctionExpression node) {
BType type = this.typechecker.getType(node);
+ if(type == null){
+ type = new SetType(new FunctionType(new UntypedType(), new UntypedType()));
+ }
BType subtype = ((SetType) type).getSubtype();
if (subtype instanceof FunctionType) {
tlaModuleString.append("[");
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/b2tla/tla/Generator.java
index 1b9a912d57ddf54be5b81a885763ca72428af1ef..083dfc99fe94057bb81e29f2e0d27315be9103ea 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/b2tla/tla/Generator.java
@@ -260,18 +260,19 @@ public class Generator extends DepthFirstAdapter {
init = true;
this.tlaModule.variables.add(con);
BType type = typechecker.getType(con);
- AMemberPredicate member = new AMemberPredicate(
- (PExpression) con.clone(),
- type.createSyntaxTreeNode());
- ArrayList<NodeType> list = this.typeRestrictor.getRestrictedTypesSet(con);
+ PExpression n = type.createSyntaxTreeNode();
+ AMemberPredicate member = new AMemberPredicate(
+ (PExpression) con.clone(), n);
+
+ ArrayList<NodeType> list = this.typeRestrictor
+ .getRestrictedTypesSet(con);
if (list == null || list.size() == 0) {
- System.out.println(con);
tlaModule.addInit(member);
- }else{
-
+ } else {
+
}
-
+
} else {
tlaModule.definitions.add(new TLADefinition(con, value));
}
diff --git a/src/main/java/de/b2tla/tlc/TLCOutput.java b/src/main/java/de/b2tla/tlc/TLCOutput.java
index 3040ef5e5425bb6b33495ad759ade564208e724d..9279f9bb54d9437599d01ba9b66094241d48de7b 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutput.java
+++ b/src/main/java/de/b2tla/tlc/TLCOutput.java
@@ -22,8 +22,7 @@ public class TLCOutput {
String parseError;
public static enum TLCResult {
- Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError,
- PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
+ Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
}
public long getRunningTime() {
@@ -143,8 +142,11 @@ public class TLCOutput {
public static TLCResult findError(ArrayList<String> list) {
for (int i = 0; i < list.size(); i++) {
String m = list.get(i);
- if (m.startsWith("Error:") || m.startsWith("\"Error:")) {
- return findError(m);
+ if (m.startsWith("Error:") || m.startsWith("\"Error:")
+ || m.startsWith("The exception was a")) {
+ TLCResult res = findError(m);
+ if (res != null)
+ return findError(m);
}
}
return TLCResult.NoError;
@@ -163,19 +165,23 @@ public class TLCOutput {
} else if (invName.startsWith("Assertion")) {
return TLCResult.AssertionError;
}
+ } else if (m.contains("The invariant of Assertion")) {
+ return TLCResult.AssertionError;
} else if (res[1].equals("Assumption")) {
return TLCResult.PropertiesError;
} else if (res[1].equals("Temporal")) {
return TLCResult.TemporalProperty;
} else if (m.equals("Error: TLC threw an unexpected exception.")) {
- return TLCResult.TLCError;
- } else if (m.startsWith("\"Error: Invalid function call to relation")){
+ return null;
+ } else if (m.startsWith("\"Error: Invalid function call to relation")) {
return TLCResult.WellDefinednessError;
} else if (m.startsWith("Error: The behavior up to")) {
return null;
- } else if (m.startsWith("Error: The following behavior constitutes a counter-example:")) {
+ } else if (m
+ .startsWith("Error: The following behavior constitutes a counter-example:")) {
return null;
- }else if (m.startsWith("Error: The error occurred when TLC was evaluating the nested")) {
+ } else if (m
+ .startsWith("Error: The error occurred when TLC was evaluating the nested")) {
return null;
}
return TLCResult.TLCError;
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
index 2efca1291415c20f9ae1e8c547216dfd22ed96d4..dad6dd5297fd6b1d52e808a7c6f39c72a114ea27 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
@@ -1,5 +1,6 @@
package de.b2tla.tlc.integration;
+import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static org.junit.Assert.assertEquals;
import org.junit.BeforeClass;
@@ -7,7 +8,6 @@ import org.junit.Test;
import de.b2tla.B2TLA;
import de.b2tla.B2TLAGlobals;
-import de.b2tla.tlc.TLCOutput;
public class ErrorTest {
@@ -19,19 +19,19 @@ public class ErrorTest {
@Test
public void testInvariantError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" };
- assertEquals(TLCOutput.TLCResult.InvariantViolation, B2TLA.test(a,true));
+ assertEquals(InvariantViolation, B2TLA.test(a,true));
}
@Test
public void testDeadlock() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/Deadlock.mch" };
- assertEquals(TLCOutput.TLCResult.Deadlock, B2TLA.test(a,true));
+ assertEquals(Deadlock, B2TLA.test(a,true));
}
@Test
public void testPropertiesError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/PropertiesError.mch" };
- assertEquals(TLCOutput.TLCResult.PropertiesError, B2TLA.test(a,true));
+ assertEquals(PropertiesError, B2TLA.test(a,true));
}
@Test
@@ -43,13 +43,26 @@ public class ErrorTest {
@Test
public void testNoError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/NoError.mch" };
- assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true));
+ assertEquals(NoError, B2TLA.test(a,true));
}
@Test
public void testEnumerationError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/EnumerationError.mch" };
- assertEquals(TLCOutput.TLCResult.TLCError, B2TLA.test(a,true));
+ assertEquals(TLCError, B2TLA.test(a,true));
+ }
+
+ @Test
+ public void testAssertionError() throws Exception {
+ String[] a = new String[] { "./src/test/resources/errors/AssertionError.mch" };
+ assertEquals(AssertionError, B2TLA.test(a,true));
+ }
+
+
+ @Test
+ public void testConstantAssertionError() throws Exception {
+ String[] a = new String[] { "./src/test/resources/errors/AssertionError2.mch" };
+ assertEquals(AssertionError, B2TLA.test(a,true));
}
}
diff --git a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java b/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java
deleted file mode 100644
index b12cd7a16d8ff7402867806b745075dd967c9af5..0000000000000000000000000000000000000000
--- a/src/test/java/de/b2tla/tlc/integration/SingleConfigurations.java
+++ /dev/null
@@ -1,21 +0,0 @@
-package de.b2tla.tlc.integration;
-
-import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
-import static org.junit.Assert.assertEquals;
-
-import org.junit.Test;
-
-import de.b2tla.B2TLA;
-import de.b2tla.B2TLAGlobals;
-
-public class SingleConfigurations {
-
-
-// @Test
-// public void TautologiesPl() throws Exception {
-// B2TLAGlobals.setDeleteOnExit(true);
-// String[] a = new String[] { "../probprivate/public_examples/TLC/others/TautologiesPL.mch", "-nodead"};
-// assertEquals(NoError, B2TLA.test(a));
-// }
-
-}
\ No newline at end of file
diff --git a/src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
similarity index 52%
rename from src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java
rename to src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
index d7357eaa9ff90cedc21f03aacde15be3928b4729..ae6a3480d3f3a8334bb1bdb5cc94f53d6399723c 100644
--- a/src/test/java/de/b2tla/tlc/integration/ProBPrivateTests.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration;
+package de.b2tla.tlc.integration.probprivate;
-import static org.junit.Assert.*;
-import static de.b2tla.tlc.TLCOutput.TLCResult.*;
+import static de.b2tla.tlc.TLCOutput.TLCResult.AssertionError;
+import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
@@ -9,42 +9,35 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
+import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
-import de.b2tla.util.*;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
-import de.b2tla.B2TLA;
-import de.b2tla.B2TLAGlobals;
-
@RunWith(PolySuite.class)
-public class ProBPrivateTests extends AbstractParseMachineTest {
+public class AssertionErrorTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
-
- public ProBPrivateTests(File machine, TLCResult result) {
+
+ public AssertionErrorTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
-
+
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- assertEquals(error, B2TLA.test(a,true));
+ assertEquals(error, B2TLA.test(a, false));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
- list.add(new TestPair(InvariantViolation, "../probprivate/public_examples/TLC/InvariantViolation"));
- list.add(new TestPair(Deadlock, "../probprivate/public_examples/TLC/Deadlock"));
- list.add(new TestPair(Goal, "../probprivate/public_examples/TLC/GOAL"));
- list.add(new TestPair(NoError, "../probprivate/public_examples/TLC/NoError"));
list.add(new TestPair(AssertionError, "../probprivate/public_examples/TLC/AssertionError"));
return getConfiguration(list);
}
-
-
}
-
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..c2ceea8eaa5ee76981d751bd2340dda53732e4ce
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
@@ -0,0 +1,44 @@
+package de.b2tla.tlc.integration.probprivate;
+
+import static de.b2tla.tlc.TLCOutput.TLCResult.Deadlock;
+import static org.junit.Assert.assertEquals;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class DeadlockTest extends AbstractParseMachineTest {
+
+ private final File machine;
+ private final TLCResult error;
+
+ public DeadlockTest(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath() };
+ assertEquals(error, B2TLA.test(a, true));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(Deadlock,
+ "../probprivate/public_examples/TLC/Deadlock"));
+ return getConfiguration(list);
+ }
+}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..0eee8c4fd861b1b92c10560225146eda374315de
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
@@ -0,0 +1,43 @@
+package de.b2tla.tlc.integration.probprivate;
+
+import static org.junit.Assert.assertEquals;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class GoalTest extends AbstractParseMachineTest{
+
+
+ private final File machine;
+ private final TLCResult error;
+
+ public GoalTest(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath()};
+ assertEquals(error, B2TLA.test(a,false));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(TLCResult.Goal, "../probprivate/public_examples/TLC/GOAL"));
+ return getConfiguration(list);
+ }
+}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..47d280bc16cb3aa7a6d8f46701d295868b1e47f0
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
@@ -0,0 +1,44 @@
+package de.b2tla.tlc.integration.probprivate;
+
+import static de.b2tla.tlc.TLCOutput.TLCResult.InvariantViolation;
+import static org.junit.Assert.assertEquals;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class InvariantViolationTest extends AbstractParseMachineTest {
+
+ private final File machine;
+ private final TLCResult error;
+
+ public InvariantViolationTest(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath() };
+ assertEquals(error, B2TLA.test(a, true));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(InvariantViolation,
+ "../probprivate/public_examples/TLC/InvariantViolation"));
+ return getConfiguration(list);
+ }
+}
diff --git a/src/test/java/de/b2tla/tlc/integration/LawsTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
similarity index 95%
rename from src/test/java/de/b2tla/tlc/integration/LawsTest.java
rename to src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
index ae970787a238c3cfef10ece16e4bc52964321fba..d5d0ef0ffb39f13648fc6878a6b9fc47cdb997b4 100644
--- a/src/test/java/de/b2tla/tlc/integration/LawsTest.java
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
@@ -1,4 +1,4 @@
-package de.b2tla.tlc.integration;
+package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..39a75a2e59da71d30dba7b72c5bb23a075735b77
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
@@ -0,0 +1,45 @@
+package de.b2tla.tlc.integration.probprivate;
+
+import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
+import static org.junit.Assert.assertEquals;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class NoErrorTest extends AbstractParseMachineTest {
+
+ private final File machine;
+ private final TLCResult error;
+
+ public NoErrorTest(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath() };
+ assertEquals(error, B2TLA.test(a, true));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(NoError,
+ "../probprivate/public_examples/TLC/NoError"));
+ return getConfiguration(list);
+ }
+
+}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..36bd5813ba50cdd75c91c814d58e714f509b5c53
--- /dev/null
+++ b/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
@@ -0,0 +1,45 @@
+package de.b2tla.tlc.integration.probprivate;
+
+import static de.b2tla.tlc.TLCOutput.TLCResult.WellDefinednessError;
+import static org.junit.Assert.assertEquals;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCOutput.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class WellDefinednessTest extends AbstractParseMachineTest {
+
+
+
+ private final File machine;
+ private final TLCResult error;
+
+ public WellDefinednessTest(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath() };
+ assertEquals(error, B2TLA.test(a,true));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(WellDefinednessError, "../probprivate/public_examples/TLC/WellDefinednessError"));
+ return getConfiguration(list);
+ }
+}
diff --git a/src/test/resources/errors/AssertionError.mch b/src/test/resources/errors/AssertionError.mch
new file mode 100644
index 0000000000000000000000000000000000000000..77ea74ee842bde42c9ead40546783541872e0e16
--- /dev/null
+++ b/src/test/resources/errors/AssertionError.mch
@@ -0,0 +1,8 @@
+MACHINE AssertionError
+ASSERTIONS x = 1
+VARIABLES x
+INVARIANT x : 1..2
+INITIALISATION x := 1
+OPERATIONS
+foo = PRE x = 1 THEN x:= 2 END
+END
\ No newline at end of file
diff --git a/src/test/resources/errors/AssertionError2.mch b/src/test/resources/errors/AssertionError2.mch
new file mode 100644
index 0000000000000000000000000000000000000000..de88790be9a6e621488865bacdc7dde4d1972cf1
--- /dev/null
+++ b/src/test/resources/errors/AssertionError2.mch
@@ -0,0 +1,8 @@
+MACHINE AssertionError
+ASSERTIONS 2 = 1
+VARIABLES x
+INVARIANT x : 1..2
+INITIALISATION x := 1
+OPERATIONS
+foo = PRE x = 1 THEN x:= 2 END
+END
\ No newline at end of file