1 files changed, 76 insertions, 0 deletions
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