Skip to content
Snippets Groups Projects
Commit 64787ee5 authored by Chris's avatar Chris
Browse files

Update Tests to match benchmarks

parent 26a8eb9d
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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();
......
if __name__ == '__main__':
calc = GeneralizedIntersection()
calc.calculate()
print(calc.getRes().card())
\ No newline at end of file
if __name__ == '__main__':
calc = GeneralizedUnion()
calc.calculate()
print(calc.getRes().card())
\ No newline at end of file
......@@ -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
......@@ -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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment