-- 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: true -> implies(edge(not on_A), on_B);
  assume h7: true -> 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