diff --git a/src/test/java/de/hhu/stups/codegenerator/python/TestOperators.java b/src/test/java/de/hhu/stups/codegenerator/python/TestOperators.java
index 77155f8e80b96008431a59d892c59e16f204a92f..8ca04dcb3a3ffd4ed305ca7553d296d81f69009e 100644
--- a/src/test/java/de/hhu/stups/codegenerator/python/TestOperators.java
+++ b/src/test/java/de/hhu/stups/codegenerator/python/TestOperators.java
@@ -195,7 +195,7 @@ public class TestOperators extends TestPython {
@Test
public void testGeneralizedUnion() throws Exception {
- testPython("GeneralizedUnion");
+ testPython("GeneralizedUnion", "GeneralizedUnion", "GeneralizedUnionAddition.stpy", true);
}
@Test
@@ -216,7 +216,7 @@ public class TestOperators extends TestPython {
@Test
public void testGeneralizedIntersection() throws Exception {
- testPython("GeneralizedIntersection");
+ testPython("GeneralizedIntersection", "GeneralizedIntersection", "GeneralizedIntersectionAddition.stpy", true);
}
@Test
diff --git a/src/test/java/de/hhu/stups/codegenerator/python/TestPython.java b/src/test/java/de/hhu/stups/codegenerator/python/TestPython.java
index 01a3ecc2efff1c33b064da2e665dc9286e0c314f..4e4230bc746b8c13f514dc9ac388ff1b5a886418 100644
--- a/src/test/java/de/hhu/stups/codegenerator/python/TestPython.java
+++ b/src/test/java/de/hhu/stups/codegenerator/python/TestPython.java
@@ -64,8 +64,8 @@ public class TestPython {
}
ProcessBuilder processBuilder = new ProcessBuilder();
- processBuilder.environment().put("PYTHONPATH", "btypes_primitives/src/main/python");
- processBuilder.command("python", "build/resources/test/de/hhu/stups/codegenerator/" + machinePath.substring(0, machinePath.length() - machineName.length()) + machineName + ".py");
+ processBuilder.environment().put("PYTHONPATH", "btypes_primitives/src/main/python_magicstack_immutable");
+ processBuilder.command("pypy3", "build/resources/test/de/hhu/stups/codegenerator/" + machinePath.substring(0, machinePath.length() - machineName.length()) + machineName + ".py");
Process executeProcess = processBuilder.start();
executeProcess.waitFor();
diff --git a/src/test/resources/de/hhu/stups/codegenerator/GeneralizedIntersectionAddition.stpy b/src/test/resources/de/hhu/stups/codegenerator/GeneralizedIntersectionAddition.stpy
new file mode 100644
index 0000000000000000000000000000000000000000..f6b65b53cd759a112189bd9390789442d6508b6a
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/GeneralizedIntersectionAddition.stpy
@@ -0,0 +1,4 @@
+if __name__ == '__main__':
+ calc = GeneralizedIntersection()
+ calc.calculate()
+ print(calc.getRes().card())
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/GeneralizedUnionAddition.stpy b/src/test/resources/de/hhu/stups/codegenerator/GeneralizedUnionAddition.stpy
new file mode 100644
index 0000000000000000000000000000000000000000..ce1792f7c1f4497cdfe7c27067fae16703db3be6
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/GeneralizedUnionAddition.stpy
@@ -0,0 +1,4 @@
+if __name__ == '__main__':
+ calc = GeneralizedUnion()
+ calc.calculate()
+ print(calc.getRes().card())
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
index 813cab6e770d151d40093579a5a3c5cddc01e7ba..8793824d8eac2df19b4c5d882261efaf14372921 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
@@ -14,8 +14,7 @@ ABSTRACT_VARIABLES
OCC,
resbl,
resrt,
- rsrtbl,
- visited
+ rsrtbl
/* PROMOTED OPERATIONS
route_reservation,
route_freeing,
@@ -63,7 +62,6 @@ INVARIANT
& /* @inv6 */ !(r).(r : ROUTES => nxt(r)[(rtbl~)[{r}] \ (rsrtbl~)[{r}]] /\ (rsrtbl~)[{r}] \ OCC = {})
& /* @inv7 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}]] <: (rsrtbl~)[{r}])
& /* @inv8 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}] \ OCC] <: (rsrtbl~)[{r}] \ OCC)
- & visited : POW(INTEGER)
ASSERTIONS
/* @thm1 */ !(b).(b : OCC & b : dom(TRK) => nxt(rsrtbl(b))(b) = TRK(b));
/* @thm2 */ ran(lst) /\ dom(TRK) \ ran(fst) = {};
@@ -82,8 +80,6 @@ INITIALISATION
frm := {}
||
LBT := {}
- ||
- visited := {}
OPERATIONS
route_reservation(r) =
@@ -97,8 +93,6 @@ OPERATIONS
rsrtbl := rsrtbl \/ (rtbl |> {r})
||
resbl := resbl \/ (rtbl~)[{r}]
- ||
- visited := visited \/ {1}
END;
route_freeing(r) =
@@ -108,8 +102,6 @@ OPERATIONS
resrt := resrt \ {r}
||
frm := frm \ {r}
- ||
- visited := visited \/ {2}
END;
FRONT_MOVE_1(r) =
@@ -121,8 +113,6 @@ OPERATIONS
OCC := OCC \/ {fst(r)}
||
LBT := LBT \/ {fst(r)}
- ||
- visited := visited \/ {3}
END;
FRONT_MOVE_2(b) =
@@ -132,8 +122,6 @@ OPERATIONS
& /* @grd3 */ TRK(b) /: OCC
THEN
OCC := OCC \/ {TRK(b)}
- ||
- visited := visited \/ {4}
END;
BACK_MOVE_1(b) =
@@ -148,8 +136,6 @@ OPERATIONS
resbl := resbl \ {b}
||
LBT := LBT \ {b}
- ||
- visited := visited \/ {5}
END;
BACK_MOVE_2(b) =
@@ -165,8 +151,6 @@ OPERATIONS
resbl := resbl \ {b}
||
LBT := LBT \ {b} \/ {TRK(b)}
- ||
- visited := visited \/ {6}
END;
@@ -175,8 +159,6 @@ OPERATIONS
/* @grd1 */ r : resrt \ frm
THEN
TRK := ((dom(nxt(r)) <<| TRK) |>> ran(nxt(r))) \/ nxt(r)
- ||
- visited := visited \/ {7}
END;
route_formation(r) =
@@ -185,7 +167,5 @@ OPERATIONS
& /* @grd2 */ (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK
THEN
frm := frm \/ {r}
- ||
- visited := visited \/ {8}
END
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_exec.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_exec.mch
index 3ba59ad71e863364e18f9dc0658fad8049abb933..d743038a9e9c287a9d4b4c26141ca06387b8ea17 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_exec.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_exec.mch
@@ -10,7 +10,7 @@ INITIALISATION counter := 0
OPERATIONS
simulate =
- WHILE counter < 1000 DO
+ WHILE counter < 10000 DO
route_reservation(R1);
route_reservation(R4);
point_positionning(R1);
@@ -107,7 +107,7 @@ OPERATIONS
route_freeing(R9);
counter := counter + 1
INVARIANT 1 = 1
- VARIANT 1000 - counter
+ VARIANT 10000 - counter
END
END