diff --git a/.gitignore b/.gitignore
index c86a830e3ba3a770db28316eadff1e968a76d478..f3654b08020d6631b523fafd8d052529cbdb9689 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,5 @@ src/test/java/testing
src/test/resources/other
src/test/resources/testing
src/test/resources/todo
+TLC4B.jar
+temp
diff --git a/build.gradle b/build.gradle
index 1a58fbd4c55bb87845c82d5e783c6e8614a3e8db..109ab016a4c97d866f5541a1a310cda69141e7c3 100644
--- a/build.gradle
+++ b/build.gradle
@@ -44,7 +44,7 @@ dependencies {
//compile(group: 'de.hhu.stups', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
testCompile (group: 'junit', name: 'junit', version: '4.11')
- testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8-SNAPSHOT')
+ testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8-SNAPSHOT')
releaseJars (group: 'de.hhu.stups', name: 'tlatools', version: '1.0.0')
releaseJars (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 7a57201338ebffc0cf234cee4ec60f64f36e4316..747e3007d4fabc7b5adea8bb72f0ed5fd06dabe8 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -172,7 +172,49 @@ public class TLC4B {
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
tlc4b.buildDir);
MP.TLCOutputStream.resetOutputStream();
- ;
+ TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
+ results.evalResults();
+ tlc4b.printResults(results, false);
+
+ System.exit(0);
+ }
+ }
+
+ public static void testString(String machineString, boolean deleteFiles)
+ throws Exception {
+ System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up
+ // windows
+ TLC4BGlobals.resetGlobals();
+ TLC4BGlobals.setDeleteOnExit(deleteFiles);
+ TLC4BGlobals.setCreateTraceFile(false);
+ TLC4BGlobals.setTestingMode(true);
+ // B2TLAGlobals.setCleanup(true);
+ TLC4B tlc4b = new TLC4B();
+ tlc4b.buildDir = new File("temp/");
+
+ tlc4b.machineFileNameWithoutFileExtension = "Test";
+
+ StopWatch.start(PARSING_TIME);
+ MP.print("Parsing... ");
+ tlc4b.translator = new Translator(machineString);
+ StopWatch.stop(PARSING_TIME);
+ println("(" + StopWatch.getRunTimeAsString(PARSING_TIME) + "ms)");
+
+ StopWatch.start(TRANSLATION_TIME);
+ MP.print("Translating... ");
+ tlc4b.translator.translate();
+ tlc4b.tlaModule = tlc4b.translator.getModuleString();
+ tlc4b.config = tlc4b.translator.getConfigString();
+ tlc4b.tlcOutputInfo = tlc4b.translator.getTLCOutputInfo();
+ StopWatch.stop(TRANSLATION_TIME);
+ println("(" + StopWatch.getRunTimeAsString(TRANSLATION_TIME) + "ms)");
+ tlc4b.createFiles();
+
+ if (TLC4BGlobals.isRunTLC()) {
+ MP.TLCOutputStream.changeOutputStream();
+ TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
+ tlc4b.buildDir);
+ MP.TLCOutputStream.resetOutputStream();
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
tlc4b.printResults(results, false);
@@ -276,7 +318,6 @@ public class TLC4B {
}
public void process(String[] args) throws IOException, BException {
- handleParameter(args);
MP.print("Arguments: ");
for (int i = 0; i < args.length; i++) {
@@ -286,6 +327,8 @@ public class TLC4B {
}
println("");
+ handleParameter(args);
+
handleMainFileName();
if (TLC4BGlobals.isTranslate()) {
StopWatch.start(PARSING_TIME);
@@ -310,7 +353,7 @@ public class TLC4B {
}
private void handleMainFileName() {
- // the following is fix to handle incorrect file names
+ // the following lines fix incorrect file names
filename = filename.replace("\\", File.separator);
filename = filename.replace("/", File.separator);
if (!filename.toLowerCase().endsWith(".mch")) {
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
index 26838921cb183496410b2b0bf97ae8b52b257761..90fc65e1714e708fa843c1261d1d051ca28c16ae 100644
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
@@ -11,6 +11,7 @@ import de.be4.classicalb.core.parser.node.ASeesMachineClause;
import de.be4.classicalb.core.parser.node.ASeesModelClause;
import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
import de.be4.classicalb.core.parser.node.AUsesMachineClause;
+import de.be4.classicalb.core.parser.node.AVarSubstitution;
import de.be4.classicalb.core.parser.node.AWhileSubstitution;
import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.exceptions.NotSupportedException;
@@ -25,12 +26,11 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
throw new NotSupportedException(
"Refines clause is currently not supported.");
}
-
- public void inASeesMachineClause(ASeesMachineClause node)
- {
- throw new NotSupportedException(
+
+ public void inASeesMachineClause(ASeesMachineClause node) {
+ throw new NotSupportedException(
"SEES clause is currently not supported.");
- }
+ }
public void inAUsesMachineClause(AUsesMachineClause node) {
throw new NotSupportedException(
@@ -62,19 +62,29 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
"IMPORTS clause is currently not supported.");
}
+ /**
+ * Substitutions
+ */
+
public void inAWhileSubstitution(AWhileSubstitution node) {
throw new NotSupportedException(
"While substitutions are currently not supported.");
}
- public void inACaseSubstitution(ACaseSubstitution node) {
+ public void inASequenceSubstitution(ASequenceSubstitution node) {
throw new NotSupportedException(
- "Case substitutions are currently not supported.");
+ "Sequence substitutions ';' are currently not supported.");
}
- public void inASequenceSubstitution(ASequenceSubstitution node) {
+ public void inAVarSubstitution(AVarSubstitution node) {
throw new NotSupportedException(
- "Sequence substitutions ';' are currently not supported.");
+ "VAR substitutions are currently not supported.");
+ }
+
+ public void inACaseSubstitution(ACaseSubstitution node) {
+ // TODO it is possible to support this substitution
+ throw new NotSupportedException(
+ "Case substitutions are currently not supported.");
}
}
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 8ff4abbe734a2f12e40c98ff195b220e5d24447e..3d2d5b6e508f61b54fcf7110c46ae42c1f834fdc 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -198,6 +198,8 @@ public final class StandardMadules {
public static final String POW_1 = "Pow1";
public static final String FINITE_SUBSETS = "Fin";
public static final String FINITE_1_SUBSETS = "Fin1";
+ public static final String B_MODULO = "BModulo";
+ public static final String B_DIVISION = "BDivision";
public static final String GENERAL_SUMMATION = "Sigma";
public static final String GENERAL_PRODUCT = "Pi";
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index b3f4cda30b9f1c6083d15b666b0ff6cf407b091c..10d65ec3e98f36731421ff1431a464e015417376 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -275,18 +275,10 @@ public class UsedStandardModules extends DepthFirstAdapter {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
- public void inADivExpression(ADivExpression node) {
- extendedStandardModules.add(STANDARD_MODULES.Naturals);
- }
-
public void inAPowerOfExpression(APowerOfExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
- public void inAModuloExpression(AModuloExpression node) {
- extendedStandardModules.add(STANDARD_MODULES.Naturals);
- }
-
public void inAMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression node) {
BType t = typechecker.getType(node);
@@ -343,6 +335,14 @@ public class UsedStandardModules extends DepthFirstAdapter {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
+ public void inAModuloExpression(AModuloExpression node) {
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ }
+
+ public void inADivExpression(ADivExpression node) {
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ }
+
public void inAGeneralSumExpression(AGeneralSumExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 2f3596d35a33a43fa00b42e8ffc1abb0dea904e7..3afd929d53bc04865bc681eafd7cda71c4d66a6d 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1637,9 +1637,12 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseADivExpression(ADivExpression node) {
inADivExpression(node);
+ moduleStringAppend(B_DIVISION);
+ moduleStringAppend("(");
node.getLeft().apply(this);
- moduleStringAppend(" \\div ");
+ moduleStringAppend(", ");
node.getRight().apply(this);
+ moduleStringAppend(")");
outADivExpression(node);
}
@@ -1654,13 +1657,14 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAModuloExpression(AModuloExpression node) {
- /**
- * TODO a mod b: IF a < 0 THEN ERROR ELSE a % b
- */
+
inAModuloExpression(node);
+ moduleStringAppend(B_MODULO);
+ moduleStringAppend("(");
node.getLeft().apply(this);
- moduleStringAppend(" % ");
+ moduleStringAppend(", ");
node.getRight().apply(this);
+ moduleStringAppend(")");
outAModuloExpression(node);
}
diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla
index 6255367e63bae1e6a60f1945285e6986d4c71a07..392ca03e331a37c2587cd6163869e379e842944f 100644
--- a/src/main/resources/standardModules/BBuiltIns.tla
+++ b/src/main/resources/standardModules/BBuiltIns.tla
@@ -3,24 +3,37 @@ EXTENDS Integers, FiniteSets, TLC
Max(S) == CHOOSE x \in S : \A p \in S : x >= p
\* The largest element of the set S
-
+
Min(S) == CHOOSE x \in S : \A p \in S : x =< p
\* The smallest element of the set S
-
+
succ[x \in Int] == x + 1
\* The successor function
pred[x \in Int] == x - 1
\* The predecessor function
-
-RECURSIVE Sigma(_)
+
+BDivision(a,b) ==
+ CASE a >= 0 /\ b > 0 -> a \div b
+ [] a < 0 /\ b > 0 -> -((-a) \div b)
+ [] a >= 0 /\ b < 0 -> -(a \div (-b))
+ [] a < 0 /\ b < 0 -> (-a) \div (-b)
+ [] b = 0 -> Assert(FALSE, "Error: Division by zero.")
+\* Rules from AtelierB reference manual (see page 40)
+
+BModulo(a,b) ==
+ IF a > 0 /\ b > 0
+ THEN a % b
+ ELSE Assert(FALSE, "Error: Both operands of the modulo operator must be natural numbers.")
+
+RECURSIVE Sigma(_)
Sigma(S) == LET e == CHOOSE e \in S: TRUE
- IN IF S = {} THEN 0 ELSE e[2] + Sigma(S \ {e})
+ IN IF S = {} THEN 0 ELSE e[2] + Sigma(S \ {e})
\* The sum of all second components of pairs which are elements of S
-RECURSIVE Pi(_)
+RECURSIVE Pi(_)
Pi(S) == LET e == CHOOSE e \in S: TRUE
- IN IF S = {} THEN 0 ELSE e[2] + Pi(S \ {e})
+ IN IF S = {} THEN 0 ELSE e[2] + Pi(S \ {e})
\* The product of all second components of pairs which are elements of S
Pow1(S) == (SUBSET S) \ {{}}
@@ -28,10 +41,10 @@ Pow1(S) == (SUBSET S) \ {{}}
Fin(S) == {x \in SUBSET S: IsFiniteSet(x)}
\* The set of all finite subsets.
-
+
Fin1(S) == {x \in SUBSET S: IsFiniteSet(x) /\ x # {}}
\* The set of all non-empty finite subsets
-
+
S \subset T == S \subseteq T /\ S # T
\* The predicate becomes true if S is a strict subset of T
@@ -40,13 +53,13 @@ NotSubset(S, T) == ~ (S \subseteq T)
NotStrictSubset(S, T) == ~ (S \subset T)
\* The predicate becomes true if S is not a strict subset of T
-
+
RECURSIVE Inter(_)
Inter(S) == IF S = {}
THEN Assert(FALSE, "Error: Applied the inter operator to an empty set.")
ELSE LET e == (CHOOSE e \in S: TRUE)
- IN IF Cardinality(S) = 1
- THEN e
+ IN IF Cardinality(S) = 1
+ THEN e
ELSE e \cap Inter(S \ {e})
\* The intersection of all elements of S.
=============================================================================
diff --git a/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java b/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..0f2a13079d7cd665726d845750ad2987037818b2
--- /dev/null
+++ b/src/test/java/de/tlc4b/prettyprint/ArithmeticTest.java
@@ -0,0 +1,173 @@
+package de.tlc4b.prettyprint;
+
+/**
+ * Test of arithmetic operators.
+ * Modulo and Division are not tested here because their translation is defined in the module BBuiltins
+ * and they are only tested via integration tests.
+ */
+import static de.tlc4b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ArithmeticTest {
+
+ @Test
+ public void testInteger() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES INTEGER = INTEGER\n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ + "ASSUME Int = Int\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testNatural() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES NATURAL = NATURAL\n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME Nat = Nat\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testNatural1() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES NATURAL1 = NATURAL1\n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME Nat \\ {0} = Nat \\ {0}\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testInt() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES INT = INT\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ + "ASSUME (-1..3) = (-1..3)\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testNat() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES NAT = NAT\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME (0..3) = (0..3)\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testNat1() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES NAT1 = NAT1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME (1..3) = (1..3)\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testInterval() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES {1,2,3} = 1..3\n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME {1,2,3} = 1..3\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testGreaterThan() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 2 > 1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME 2 > 1\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testLessThan() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 < 2\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME 1 < 2\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testGreaterThanEquals() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 >= 2\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME 1 >= 2\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testLessThanEquals() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 <= 2\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ + "ASSUME 1 =< 2\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testAdd() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 2 = 1 + 1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals \n"
+ + "ASSUME 2 = 1 + 1 \n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testMinus() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 = 2 - 1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals \n"
+ + "ASSUME 1 = 2 - 1 \n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testMult() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 = 1 * 1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals \n"
+ + "ASSUME 1 = 1 * 1 \n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testPower() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES 1 = 1 ** 1\n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Naturals \n"
+ + "ASSUME 1 = 1 ^ 1 \n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testUnaryMinus() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES -1 = 1 \n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ + "ASSUME -1 = 1\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testMinInt() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES MININT = MININT \n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ + "ASSUME -1 = -1\n" + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testMaxInt() throws Exception {
+ String machine = "MACHINE test\n" + "PROPERTIES MAXINT = MAXINT \n"
+ + "END";
+ String expected = "---- MODULE test----\n" + "ASSUME 3 = 3\n"
+ + "======";
+ compare(expected, machine);
+ }
+
+ @Test
+ public void testSetComprehensionInt() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES {x| 1=1 => x = 1} = {} \n" + "END";
+ String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
+ + "ASSUME {x \\in (Int): 1 = 1 => x = 1} = {}\n" + "======";
+ compare(expected, machine);
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
deleted file mode 100644
index 11f5d92a01aee92263ae562de9ef07b1904186b7..0000000000000000000000000000000000000000
--- a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
+++ /dev/null
@@ -1,266 +0,0 @@
-package de.tlc4b.prettyprint;
-
-import static de.tlc4b.util.TestUtil.compare;
-
-import org.junit.Test;
-
-public class NumbersTest {
-
-
- @Test
- public void testInteger() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES INTEGER = INTEGER\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Integers\n"
- + "ASSUME Int = Int\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testNatural() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES NATURAL = NATURAL\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME Nat = Nat\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testNatural1() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES NATURAL1 = NATURAL1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME Nat \\ {0} = Nat \\ {0}\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testInt() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES INT = INT\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Integers\n"
- + "ASSUME (-1..3) = (-1..3)\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testNat() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES NAT = NAT\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME (0..3) = (0..3)\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testNat1() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES NAT1 = NAT1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME (1..3) = (1..3)\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testInterval() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES {1,2,3} = 1..3\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME {1,2,3} = 1..3\n"
- + "======";
- compare(expected, machine);
- }
-
-
- @Test
- public void testGreaterThan() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 2 > 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME 2 > 1\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testLessThan() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 < 2\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME 1 < 2\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testGreaterThanEquals() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 >= 2\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME 1 >= 2\n"
- + "======";
- compare(expected, machine);
- }
-
-
- @Test
- public void testLessThanEquals() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 <= 2\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals\n"
- + "ASSUME 1 =< 2\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testAdd() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 2 = 1 + 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 2 = 1 + 1 \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testMinus() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 2 - 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 1 = 2 - 1 \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testMult() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 1 * 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 1 = 1 * 1 \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testDiv() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 1 / 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 1 = 1 \\div 1 \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testPower() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 1 = 1 ** 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 1 = 1 ^ 1 \n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testModulo() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES 0 = 1 mod 1\n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Naturals \n"
- + "ASSUME 0 = 1 % 1 \n"
- + "======";
- compare(expected, machine);
- }
-
-
- @Test
- public void testUnaryMinus() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES -1 = 1 \n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Integers\n"
- + "ASSUME -1 = 1\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testMinInt() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES MININT = MININT \n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Integers\n"
- + "ASSUME -1 = -1\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testMaxInt() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES MAXINT = MAXINT \n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "ASSUME 3 = 3\n"
- + "======";
- compare(expected, machine);
- }
-
- @Test
- public void testSetComprehensionInt() throws Exception {
- String machine = "MACHINE test\n"
- + "PROPERTIES {x| 1=1 => x = 1} = {} \n"
- + "END";
- String expected = "---- MODULE test----\n"
- + "EXTENDS Integers\n"
- + "ASSUME {x \\in (Int): 1 = 1 => x = 1} = {}\n"
- + "======";
- compare(expected, machine);
- }
-
-
-
-}
diff --git a/src/test/java/de/tlc4b/tlc/integration/ArithmeticTest.java b/src/test/java/de/tlc4b/tlc/integration/ArithmeticTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..b295afd3f2ea91a454028b6aa2c2ffd7dcac4d3b
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/ArithmeticTest.java
@@ -0,0 +1,56 @@
+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+
+import org.junit.Test;
+
+public class ArithmeticTest {
+
+ @Test
+ public void testModulo() throws Exception {
+ String machine =
+ "MACHINE Test\n"
+ + "PROPERTIES \n"
+ + "3 mod 3 = 0 & 6 mod 3 = 0 & 4 mod 3 = 1 & 3 mod 6 = 3 \n"
+ + "END";
+ assertEquals(NoError, testString(machine));
+ }
+
+ @Test
+ public void testModuloErrorFirstOperandIsNegative() throws Exception {
+ String machine = "MACHINE Test\n" + "PROPERTIES -1 mod 1 = 0 \n" + "END";
+ assertEquals(WellDefinednessError, testString(machine));
+ }
+
+ @Test
+ public void testModuloErrorSecondOperandIsNegative() throws Exception {
+ String machine = "MACHINE Test\n" + "PROPERTIES 1 mod -1 = 0 \n" + "END";
+ assertEquals(WellDefinednessError, testString(machine));
+ }
+
+ @Test
+ public void testModuloErrorSecondOperandIsZero() throws Exception {
+ String machine = "MACHINE Test\n" + "PROPERTIES 1 mod 0 = 0 \n" + "END";
+ assertEquals(WellDefinednessError, testString(machine));
+ }
+
+ @Test
+ public void testDivision() throws Exception {
+ String machine =
+ "MACHINE Test\n"
+ + "PROPERTIES \n"
+ + "3 / 3 = 1 & 4 / 3 = 1 & 0 / 3 = 0 & \n"
+ + "-1/3 = 0 & 1/-3 = 0 & -1/-3 = 0 \n"
+ + "END";
+ assertEquals(NoError, testString(machine));
+ }
+
+ @Test
+ public void testDivisionErrorDivisionByZero() throws Exception {
+ String machine = "MACHINE Test\n" + "PROPERTIES 1 / 0 = 0 \n" + "END";
+ assertEquals(WellDefinednessError, testString(machine));
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
new file mode 100644
index 0000000000000000000000000000000000000000..477da9de6eb72e470e6ca7396ec1eff2ce7b6519
--- /dev/null
+++ b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
@@ -0,0 +1,11 @@
+package de.tlc4b.util;
+
+import de.tlc4b.TLC4B;
+
+public class TLC4BRunnerTestString {
+
+ public static void main(String[] args) throws Exception {
+ System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
+ TLC4B.testString(args[0],true);
+ }
+}
diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java
index 438b8c00fb31fc1c39cc14434fa57270b86b0dc7..acf6c516c7990d40234a0e0b0247a3899d92b7a0 100644
--- a/src/test/java/de/tlc4b/util/TLC4BTester.java
+++ b/src/test/java/de/tlc4b/util/TLC4BTester.java
@@ -4,10 +4,11 @@ package de.tlc4b.util;
import de.tlc4b.TLC4B;
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);
+ }
- public static void main(String[] args) throws Exception {
- System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
- TLC4B.test(args,true);
- }
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 831ec92b1b4d8a1345f9b2b86b5beafbc06b566a..5c868dc78ce8f6661f1ed52d9e7c12e12ddd2a99 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -23,12 +23,12 @@ import de.tlc4b.tlc.TLCResults.TLCResult;
public class TestUtil {
- public static void compare(String expectedModule, String machine)
+ public static void compare(String expectedModule, String machineString)
throws Exception {
TLC4BGlobals.setForceTLCToEvalConstants(false);
ToolIO.setMode(ToolIO.TOOL);
- Translator b2tlaTranslator = new Translator(machine);
+ Translator b2tlaTranslator = new Translator(machineString);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
@@ -53,7 +53,8 @@ public class TestUtil {
// assertEquals(sb2.toString(), sb1.toString());
}
- public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
+ public static String translateTLA2B(String moduleName, String tlaString)
+ throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName,
tlaString, null);
}
@@ -150,10 +151,22 @@ public class TestUtil {
return translator.getModuleString();
}
+ public static TLCResult testString(String machineString) throws IOException {
+ String[] args = new String[] { machineString };
+ String runnerClassName = TLC4BRunnerTestString.class.getCanonicalName();
+
+ return runTLC(runnerClassName, args);
+ }
+
public static TLCResult test(String[] args) throws IOException {
+ String runnerClassName = TLC4BTester.class.getCanonicalName();
+ return runTLC(runnerClassName, args);
+ }
+
+ private static TLCResult runTLC(String runnerClassName, String[] args)
+ throws IOException {
System.out.println("Starting JVM...");
- final Process p = startJVM("", TLC4BTester.class.getCanonicalName(),
- args);
+ final Process p = startJVM("", runnerClassName, args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
StreamGobbler errOut = new StreamGobbler(p.getErrorStream());
@@ -176,8 +189,11 @@ public class TestUtil {
}
System.out.println("No result found.");
return null;
+
}
+
+
private static Process startJVM(final String optionsAsString,
final String mainClass, final String[] arguments)
throws IOException {
diff --git a/src/test/resources/basics/BBuiltInsTest.mch b/src/test/resources/basics/BBuiltInsTest.mch
index 360c9bd10ed4092ea19e810b466b18faef6be903..b1bde6daf604b3b069af1f34a6f054862f7690c5 100644
--- a/src/test/resources/basics/BBuiltInsTest.mch
+++ b/src/test/resources/basics/BBuiltInsTest.mch
@@ -76,4 +76,4 @@ PROPERTIES
/* MinInt */
& MININT = -1
-END
\ No newline at end of file
+END
diff --git a/src/test/resources/basics/BBuiltInsTest.prob b/src/test/resources/basics/BBuiltInsTest.prob
new file mode 100644
index 0000000000000000000000000000000000000000..a7413e19385cb59d6d23b9ed9fad1050427ebce8
--- /dev/null
+++ b/src/test/resources/basics/BBuiltInsTest.prob
@@ -0,0 +1,3 @@
+parser_version('2015-09-11 09:12:44.923').
+classical_b('BBuiltInsTest',['/Users/hansen/git/tlc4b/src/test/resources/basics/BBuiltInsTest.mch']).
+machine(abstract_machine(pos(1,1,1,1,79,3),machine(pos(2,1,1,1,1,7)),machine_header(pos(3,1,1,9,1,21),'BBuiltInsTest',[]),[properties(pos(4,1,2,1,77,13),conjunct(pos(5,1,4,1,77,13),conjunct(pos(6,1,4,1,74,12),conjunct(pos(7,1,4,1,71,16),conjunct(pos(8,1,4,1,70,14),conjunct(pos(9,1,4,1,67,16),conjunct(pos(10,1,4,1,66,14),conjunct(pos(11,1,4,1,63,14),conjunct(pos(12,1,4,1,62,13),conjunct(pos(13,1,4,1,61,13),conjunct(pos(14,1,4,1,58,14),conjunct(pos(15,1,4,1,57,13),conjunct(pos(16,1,4,1,56,13),conjunct(pos(17,1,4,1,53,28),conjunct(pos(18,1,4,1,52,37),conjunct(pos(19,1,4,1,51,31),conjunct(pos(20,1,4,1,48,33),conjunct(pos(21,1,4,1,47,40),conjunct(pos(22,1,4,1,46,34),conjunct(pos(23,1,4,1,43,67),conjunct(pos(24,1,4,1,42,34),conjunct(pos(25,1,4,1,39,63),conjunct(pos(26,1,4,1,38,31),conjunct(pos(27,1,4,1,35,33),conjunct(pos(28,1,4,1,34,19),conjunct(pos(29,1,4,1,33,15),conjunct(pos(30,1,4,1,30,36),conjunct(pos(31,1,4,1,29,22),conjunct(pos(32,1,4,1,28,16),conjunct(pos(33,1,4,1,25,33),conjunct(pos(34,1,4,1,24,19),conjunct(pos(35,1,4,1,23,15),conjunct(pos(36,1,4,1,20,18),conjunct(pos(37,1,4,1,19,21),conjunct(pos(38,1,4,1,18,12),conjunct(pos(39,1,4,1,17,14),conjunct(pos(40,1,4,1,16,14),conjunct(pos(41,1,4,1,13,18),conjunct(pos(42,1,4,1,12,20),conjunct(pos(43,1,4,1,11,15),conjunct(pos(44,1,4,1,10,13),conjunct(pos(45,1,4,1,7,18),conjunct(pos(46,1,4,1,6,16),conjunct(pos(47,1,4,1,5,12),subset_strict(pos(48,1,4,1,4,13),set_extension(pos(49,1,4,1,4,3),[integer(pos(50,1,4,2,4,2),1)]),set_extension(pos(51,1,4,9,4,13),[integer(pos(52,1,4,10,4,10),1),integer(pos(53,1,4,12,4,12),2)])),subset_strict(pos(54,1,5,3,5,12),empty_set(pos(55,1,5,3,5,4)),set_extension(pos(56,1,5,10,5,12),[integer(pos(57,1,5,11,5,11),1)]))),negation(pos(58,1,6,3,6,16),subset_strict(pos(59,1,6,7,6,15),empty_set(pos(60,1,6,7,6,8)),empty_set(pos(61,1,6,14,6,15))))),negation(pos(62,1,7,3,7,18),subset_strict(pos(63,1,7,7,7,17),set_extension(pos(64,1,7,7,7,9),[integer(pos(65,1,7,8,7,8),1)]),set_extension(pos(66,1,7,15,7,17),[integer(pos(67,1,7,16,7,16),1)])))),not_subset(pos(68,1,10,3,10,13),set_extension(pos(69,1,10,3,10,5),[integer(pos(70,1,10,4,10,4),1)]),set_extension(pos(71,1,10,11,10,13),[integer(pos(72,1,10,12,10,12),2)]))),not_subset(pos(73,1,11,3,11,15),set_extension(pos(74,1,11,3,11,7),[integer(pos(75,1,11,4,11,4),1),integer(pos(76,1,11,6,11,6),2)]),set_extension(pos(77,1,11,13,11,15),[integer(pos(78,1,11,14,11,14),2)]))),negation(pos(79,1,12,3,12,20),not_subset(pos(80,1,12,7,12,19),set_extension(pos(81,1,12,7,12,9),[integer(pos(82,1,12,8,12,8),1)]),set_extension(pos(83,1,12,15,12,19),[integer(pos(84,1,12,16,12,16),1),integer(pos(85,1,12,18,12,18),2)])))),negation(pos(86,1,13,3,13,18),not_subset(pos(87,1,13,7,13,17),set_extension(pos(88,1,13,7,13,9),[integer(pos(89,1,13,8,13,8),1)]),set_extension(pos(90,1,13,15,13,17),[integer(pos(91,1,13,16,13,16),1)])))),not_subset_strict(pos(92,1,16,3,16,14),set_extension(pos(93,1,16,3,16,5),[integer(pos(94,1,16,4,16,4),1)]),set_extension(pos(95,1,16,12,16,14),[integer(pos(96,1,16,13,16,13),2)]))),not_subset_strict(pos(97,1,17,3,17,14),set_extension(pos(98,1,17,3,17,5),[integer(pos(99,1,17,4,17,4),1)]),set_extension(pos(100,1,17,12,17,14),[integer(pos(101,1,17,13,17,13),1)]))),not_subset_strict(pos(102,1,18,3,18,12),empty_set(pos(103,1,18,3,18,4)),empty_set(pos(104,1,18,11,18,12)))),negation(pos(105,1,19,3,19,21),not_subset_strict(pos(106,1,19,7,19,20),set_extension(pos(107,1,19,7,19,9),[integer(pos(108,1,19,8,19,8),1)]),set_extension(pos(109,1,19,16,19,20),[integer(pos(110,1,19,17,19,17),1),integer(pos(111,1,19,19,19,19),2)])))),negation(pos(112,1,20,3,20,18),not_subset_strict(pos(113,1,20,7,20,17),empty_set(pos(114,1,20,7,20,8)),set_extension(pos(115,1,20,15,20,17),[integer(pos(116,1,20,16,20,16),1)])))),equal(pos(117,1,23,3,23,15),pow1_subset(pos(118,1,23,3,23,10),empty_set(pos(119,1,23,8,23,9))),empty_set(pos(120,1,23,14,23,15)))),equal(pos(121,1,24,3,24,19),pow1_subset(pos(122,1,24,3,24,11),set_extension(pos(123,1,24,8,24,10),[integer(pos(124,1,24,9,24,9),1)])),set_extension(pos(125,1,24,15,24,19),[set_extension(pos(126,1,24,16,24,18),[integer(pos(127,1,24,17,24,17),1)])]))),equal(pos(128,1,25,3,25,33),pow1_subset(pos(129,1,25,3,25,13),set_extension(pos(130,1,25,8,25,12),[integer(pos(131,1,25,9,25,9),1),integer(pos(132,1,25,11,25,11),2)])),set_extension(pos(133,1,25,17,25,33),[set_extension(pos(134,1,25,18,25,20),[integer(pos(135,1,25,19,25,19),1)]),set_extension(pos(136,1,25,23,25,25),[integer(pos(137,1,25,24,25,24),2)]),set_extension(pos(138,1,25,28,25,32),[integer(pos(139,1,25,29,25,29),1),integer(pos(140,1,25,31,25,31),2)])]))),equal(pos(141,1,28,3,28,16),fin_subset(pos(142,1,28,3,28,9),empty_set(pos(143,1,28,7,28,8))),set_extension(pos(144,1,28,13,28,16),[empty_set(pos(145,1,28,14,28,15))]))),equal(pos(146,1,29,3,29,22),fin_subset(pos(147,1,29,3,29,10),set_extension(pos(148,1,29,7,29,9),[integer(pos(149,1,29,8,29,8),1)])),set_extension(pos(150,1,29,14,29,22),[empty_set(pos(151,1,29,15,29,16)),set_extension(pos(152,1,29,19,29,21),[integer(pos(153,1,29,20,29,20),1)])]))),equal(pos(154,1,30,3,30,36),fin_subset(pos(155,1,30,3,30,12),set_extension(pos(156,1,30,7,30,11),[integer(pos(157,1,30,8,30,8),1),integer(pos(158,1,30,10,30,10),2)])),set_extension(pos(159,1,30,16,30,36),[empty_set(pos(160,1,30,17,30,18)),set_extension(pos(161,1,30,21,30,23),[integer(pos(162,1,30,22,30,22),1)]),set_extension(pos(163,1,30,26,30,28),[integer(pos(164,1,30,27,30,27),2)]),set_extension(pos(165,1,30,31,30,35),[integer(pos(166,1,30,32,30,32),1),integer(pos(167,1,30,34,30,34),2)])]))),equal(pos(168,1,33,3,33,15),fin1_subset(pos(169,1,33,3,33,10),empty_set(pos(170,1,33,8,33,9))),empty_set(pos(171,1,33,14,33,15)))),equal(pos(172,1,34,3,34,19),fin1_subset(pos(173,1,34,3,34,11),set_extension(pos(174,1,34,8,34,10),[integer(pos(175,1,34,9,34,9),1)])),set_extension(pos(176,1,34,15,34,19),[set_extension(pos(177,1,34,16,34,18),[integer(pos(178,1,34,17,34,17),1)])]))),equal(pos(179,1,35,3,35,33),fin1_subset(pos(180,1,35,3,35,13),set_extension(pos(181,1,35,8,35,12),[integer(pos(182,1,35,9,35,9),1),integer(pos(183,1,35,11,35,11),2)])),set_extension(pos(184,1,35,17,35,33),[set_extension(pos(185,1,35,18,35,20),[integer(pos(186,1,35,19,35,19),1)]),set_extension(pos(187,1,35,23,35,25),[integer(pos(188,1,35,24,35,24),2)]),set_extension(pos(189,1,35,28,35,32),[integer(pos(190,1,35,29,35,29),1),integer(pos(191,1,35,31,35,31),2)])]))),equal(pos(192,1,38,3,38,31),quantified_intersection(pos(193,1,38,3,38,26),[identifier(pos(194,1,38,9,38,9),z)],member(pos(195,1,38,13,38,20),identifier(pos(196,1,38,13,38,13),z),set_extension(pos(197,1,38,16,38,20),[integer(pos(198,1,38,17,38,17),1),integer(pos(199,1,38,19,38,19),2)])),set_extension(pos(200,1,38,23,38,25),[identifier(pos(201,1,38,24,38,24),z)])),empty_set(pos(202,1,38,30,38,31)))),equal(pos(203,1,39,3,39,63),quantified_intersection(pos(204,1,39,3,39,53),[identifier(pos(205,1,39,9,39,10),x1)],member(pos(206,1,39,14,39,22),identifier(pos(207,1,39,14,39,15),x1),set_extension(pos(208,1,39,18,39,22),[integer(pos(209,1,39,19,39,19),2),integer(pos(210,1,39,21,39,21),4)])),comprehension_set(pos(211,1,39,25,39,52),[identifier(pos(212,1,39,26,39,27),y1)],conjunct(pos(213,1,39,31,39,51),member(pos(214,1,39,31,39,40),identifier(pos(215,1,39,31,39,32),y1),interval(pos(216,1,39,36,39,40),integer(pos(217,1,39,36,39,36),0),integer(pos(218,1,39,39,39,40),10))),less_equal(pos(219,1,39,44,39,51),identifier(pos(220,1,39,44,39,45),y1),identifier(pos(221,1,39,50,39,51),x1))))),set_extension(pos(222,1,39,57,39,63),[integer(pos(223,1,39,58,39,58),0),integer(pos(224,1,39,60,39,60),1),integer(pos(225,1,39,62,39,62),2)]))),equal(pos(226,1,42,3,42,34),quantified_union(pos(227,1,42,3,42,26),[identifier(pos(228,1,42,9,42,9),z)],member(pos(229,1,42,13,42,20),identifier(pos(230,1,42,13,42,13),z),set_extension(pos(231,1,42,16,42,20),[integer(pos(232,1,42,17,42,17),1),integer(pos(233,1,42,19,42,19),2)])),set_extension(pos(234,1,42,23,42,25),[identifier(pos(235,1,42,24,42,24),z)])),set_extension(pos(236,1,42,30,42,34),[integer(pos(237,1,42,31,42,31),1),integer(pos(238,1,42,33,42,33),2)]))),equal(pos(239,1,43,3,43,67),quantified_union(pos(240,1,43,3,43,53),[identifier(pos(241,1,43,9,43,10),x1)],member(pos(242,1,43,14,43,22),identifier(pos(243,1,43,14,43,15),x1),set_extension(pos(244,1,43,18,43,22),[integer(pos(245,1,43,19,43,19),2),integer(pos(246,1,43,21,43,21),4)])),comprehension_set(pos(247,1,43,25,43,52),[identifier(pos(248,1,43,26,43,27),y1)],conjunct(pos(249,1,43,31,43,51),member(pos(250,1,43,31,43,40),identifier(pos(251,1,43,31,43,32),y1),interval(pos(252,1,43,36,43,40),integer(pos(253,1,43,36,43,36),0),integer(pos(254,1,43,39,43,40),10))),less_equal(pos(255,1,43,44,43,51),identifier(pos(256,1,43,44,43,45),y1),identifier(pos(257,1,43,50,43,51),x1))))),set_extension(pos(258,1,43,57,43,67),[integer(pos(259,1,43,58,43,58),0),integer(pos(260,1,43,60,43,60),1),integer(pos(261,1,43,62,43,62),2),integer(pos(262,1,43,64,43,64),3),integer(pos(263,1,43,66,43,66),4)]))),equal(pos(264,1,46,3,46,34),general_sum(pos(265,1,46,3,46,29),[identifier(pos(266,1,46,9,46,9),z)],member(pos(267,1,46,13,46,23),identifier(pos(268,1,46,13,46,13),z),set_extension(pos(269,1,46,17,46,23),[integer(pos(270,1,46,18,46,18),1),integer(pos(271,1,46,20,46,20),2),integer(pos(272,1,46,22,46,22),3)])),add(pos(273,1,46,26,46,28),identifier(pos(274,1,46,26,46,26),z),identifier(pos(275,1,46,28,46,28),z))),integer(pos(276,1,46,33,46,34),12))),equal(pos(277,1,47,3,47,40),general_sum(pos(278,1,47,3,47,35),[identifier(pos(279,1,47,9,47,9),z)],conjunct(pos(280,1,47,13,47,29),member(pos(281,1,47,13,47,23),identifier(pos(282,1,47,13,47,13),z),set_extension(pos(283,1,47,17,47,23),[integer(pos(284,1,47,18,47,18),1),integer(pos(285,1,47,20,47,20),2),integer(pos(286,1,47,22,47,22),3)])),equal(pos(287,1,47,27,47,29),integer(pos(288,1,47,27,47,27),1),integer(pos(289,1,47,29,47,29),1))),add(pos(290,1,47,32,47,34),identifier(pos(291,1,47,32,47,32),z),identifier(pos(292,1,47,34,47,34),z))),integer(pos(293,1,47,39,47,40),12))),equal(pos(294,1,48,3,48,33),general_sum(pos(295,1,48,3,48,29),[identifier(pos(296,1,48,9,48,9),x)],member(pos(297,1,48,13,48,23),identifier(pos(298,1,48,13,48,13),x),set_extension(pos(299,1,48,17,48,23),[integer(pos(300,1,48,18,48,18),1),integer(pos(301,1,48,20,48,20),2),integer(pos(302,1,48,22,48,22),3)])),add(pos(303,1,48,26,48,28),identifier(pos(304,1,48,26,48,26),x),integer(pos(305,1,48,28,48,28),1))),integer(pos(306,1,48,33,48,33),9))),equal(pos(307,1,51,3,51,31),general_product(pos(308,1,51,3,51,26),[identifier(pos(309,1,51,6,51,6),z)],member(pos(310,1,51,10,51,20),identifier(pos(311,1,51,10,51,10),z),set_extension(pos(312,1,51,14,51,20),[integer(pos(313,1,51,15,51,15),1),integer(pos(314,1,51,17,51,17),2),integer(pos(315,1,51,19,51,19),3)])),add(pos(316,1,51,23,51,25),identifier(pos(317,1,51,23,51,23),z),identifier(pos(318,1,51,25,51,25),z))),integer(pos(319,1,51,30,51,31),12))),equal(pos(320,1,52,3,52,37),general_product(pos(321,1,52,3,52,32),[identifier(pos(322,1,52,6,52,6),z)],conjunct(pos(323,1,52,10,52,26),member(pos(324,1,52,10,52,20),identifier(pos(325,1,52,10,52,10),z),set_extension(pos(326,1,52,14,52,20),[integer(pos(327,1,52,15,52,15),1),integer(pos(328,1,52,17,52,17),2),integer(pos(329,1,52,19,52,19),3)])),equal(pos(330,1,52,24,52,26),integer(pos(331,1,52,24,52,24),1),integer(pos(332,1,52,26,52,26),1))),add(pos(333,1,52,29,52,31),identifier(pos(334,1,52,29,52,29),z),identifier(pos(335,1,52,31,52,31),z))),integer(pos(336,1,52,36,52,37),12))),equal(pos(337,1,53,3,53,28),general_product(pos(338,1,53,3,53,24),[identifier(pos(339,1,53,6,53,6),x)],member(pos(340,1,53,10,53,20),identifier(pos(341,1,53,10,53,10),x),set_extension(pos(342,1,53,14,53,20),[integer(pos(343,1,53,15,53,15),1),integer(pos(344,1,53,17,53,17),2),integer(pos(345,1,53,19,53,19),3)])),identifier(pos(346,1,53,23,53,23),x)),integer(pos(347,1,53,28,53,28),6))),equal(pos(348,1,56,3,56,13),function(pos(349,1,56,3,56,9),successor(pos(350,1,56,3,56,6)),[integer(pos(351,1,56,8,56,8),3)]),integer(pos(352,1,56,13,56,13),4))),equal(pos(353,1,57,3,57,13),function(pos(354,1,57,3,57,9),successor(pos(355,1,57,3,57,6)),[integer(pos(356,1,57,8,57,8),0)]),integer(pos(357,1,57,13,57,13),1))),equal(pos(358,1,58,3,58,14),function(pos(359,1,58,3,58,10),successor(pos(360,1,58,3,58,6)),[unary_minus(pos(361,1,58,8,58,9),integer(pos(362,1,58,9,58,9),1))]),integer(pos(363,1,58,14,58,14),0))),equal(pos(364,1,61,3,61,13),function(pos(365,1,61,3,61,9),predecessor(pos(366,1,61,3,61,6)),[integer(pos(367,1,61,8,61,8),3)]),integer(pos(368,1,61,13,61,13),2))),equal(pos(369,1,62,3,62,13),function(pos(370,1,62,3,62,9),predecessor(pos(371,1,62,3,62,6)),[integer(pos(372,1,62,8,62,8),1)]),integer(pos(373,1,62,13,62,13),0))),equal(pos(374,1,63,3,63,14),function(pos(375,1,63,3,63,9),predecessor(pos(376,1,63,3,63,6)),[integer(pos(377,1,63,8,63,8),0)]),unary_minus(pos(378,1,63,13,63,14),integer(pos(379,1,63,14,63,14),1)))),equal(pos(380,1,66,3,66,14),min(pos(381,1,66,3,66,10),set_extension(pos(382,1,66,7,66,9),[integer(pos(383,1,66,8,66,8),1)])),integer(pos(384,1,66,14,66,14),1))),equal(pos(385,1,67,3,67,16),min(pos(386,1,67,3,67,12),set_extension(pos(387,1,67,7,67,11),[integer(pos(388,1,67,8,67,8),1),integer(pos(389,1,67,10,67,10),2)])),integer(pos(390,1,67,16,67,16),1))),equal(pos(391,1,70,3,70,14),max(pos(392,1,70,3,70,10),set_extension(pos(393,1,70,7,70,9),[integer(pos(394,1,70,8,70,8),1)])),integer(pos(395,1,70,14,70,14),1))),equal(pos(396,1,71,3,71,16),max(pos(397,1,71,3,71,12),set_extension(pos(398,1,71,7,71,11),[integer(pos(399,1,71,8,71,8),1),integer(pos(400,1,71,10,71,10),2)])),integer(pos(401,1,71,16,71,16),2))),equal(pos(402,1,74,3,74,12),max_int(pos(403,1,74,3,74,8)),integer(pos(404,1,74,12,74,12),3))),equal(pos(405,1,77,3,77,13),min_int(pos(406,1,77,3,77,8)),unary_minus(pos(407,1,77,12,77,13),integer(pos(408,1,77,13,77,13),1)))))])).