summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/source/updown.scade2
-rw-r--r--tests/source/uturn.scade76
2 files changed, 77 insertions, 1 deletions
diff --git a/tests/source/updown.scade b/tests/source/updown.scade
index 089293a..c736dd8 100644
--- a/tests/source/updown.scade
+++ b/tests/source/updown.scade
@@ -4,7 +4,6 @@ node updown() returns(probe x: int)
var last_x: int;
let
last_x = 0 -> pre x;
- guarantee x_bounded: x >= -bound and x <= bound;
automaton
initial state UP
let x = last_x + 1; tel
@@ -15,6 +14,7 @@ let
until if x <= -bound resume UP;
returns x;
+ guarantee x_bounded: x >= -bound and x <= bound;
tel
node test(i: int) returns(a, b, c: int; exit: bool)
diff --git a/tests/source/uturn.scade b/tests/source/uturn.scade
new file mode 100644
index 0000000..84c9b51
--- /dev/null
+++ b/tests/source/uturn.scade
@@ -0,0 +1,76 @@
+-- U turn system for a subway
+-- See paper HLR-lustre.tse.ps
+
+
+node edge(X: bool) returns (EDGE: bool)
+let
+ EDGE = X -> (X and not pre X);
+tel
+
+node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)
+ returns (grant_access, grant_exit, do_AB, do_BC: bool)
+var empty_section, only_on_B: bool;
+let
+ grant_access = empty_section and ack_AB;
+ grant_exit = only_on_B and ack_BC;
+ do_AB = (not ack_AB) and empty_section;
+ do_BC = (not ack_BC) and only_on_B;
+ empty_section = not (on_A or on_B or on_C);
+ only_on_B = on_B and not (on_C or on_A);
+tel
+
+node always_from_to(B, A, C: bool) returns (X: bool)
+let
+ X = implies(after(A), always_since(B, A) or once_since(C, A));
+tel
+
+node implies(A, B: bool) returns (AimpliesB: bool)
+let
+ AimpliesB = (not A) or B;
+tel
+
+node after(A: bool) returns (afterA: bool)
+let
+ afterA = false -> pre(A or afterA);
+tel
+
+node always_since(B, A: bool) returns (alwaysBsinceA: bool)
+let
+ alwaysBsinceA = if A then B
+ else if after(A) then B and pre alwaysBsinceA
+ else true;
+tel
+
+node once_since(C, A: bool) returns (onceCsinceA: bool)
+let
+ onceCsinceA = if A then C
+ else if after(A) then C or pre onceCsinceA
+ else true;
+tel
+
+node UMS_verif(on_A, on_B, on_C, ack_AB, ack_BC: bool)
+ returns()
+var
+ grant_access, grant_exit: bool;
+ do_AB, do_BC: bool;
+ empty_section, only_on_B: bool;
+let
+ empty_section = not (on_A or on_B or on_C);
+ only_on_B = on_B and not(on_A or on_C);
+
+ assume h1: not(ack_AB and ack_BC);
+ assume h2: always_from_to(ack_AB, ack_AB, do_BC)
+ and always_from_to(ack_BC, ack_BC, do_AB);
+ assume h3: empty_section -> true;
+ assume h4: true -> implies(edge(not empty_section), pre grant_access);
+ assume h5: true -> implies(edge(on_C), pre grant_exit);
+ assume h6: implies(edge(not on_A), on_B);
+ assume h7: implies(edge(not on_B), on_A or on_C);
+
+ grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC);
+
+ guarantee no_collision: implies(grant_access, empty_section);
+ guarantee exclusive_req: not(do_AB and do_BC);
+ guarantee no_derail_AB: always_from_to(ack_AB, grant_access, only_on_B);
+ guarantee no_derail_BC: always_from_to(ack_BC, grant_exit, empty_section);
+tel