CristalCaveGem » LustreC » Lustrec-Tests

node Sofar( X : bool ) returns ( Sofar : bool );

let

    Sofar = X -> X or pre Sofar;

tel

node edge(X: bool) returns(Y: bool);

let

    Y = X -> X and not pre(X);

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 implies(A, B: bool) returns(AimpliesB: bool);

let

    AimpliesB = not A or B;

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 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_A or on_C);

tel

node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)

returns(OK: bool);

--@ contract guarantees OK;

var

   grant_access, grant_exit: bool;

   do_AB, do_BC: bool;

   no_collision, exclusive_req: bool;

   no_derail_AB, no_derail_BC: bool;

   empty_section, only_on_B: bool;

   env : 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);

   (grant_access, grant_exit, do_AB, do_BC) =

       UMS(on_A, on_B, on_C, ack_AB, ack_BC);

   env = Sofar( not(ack_AB and ack_BC) and

               always_from_to(ack_AB, ack_AB, do_BC) and

               always_from_to(ack_BC, ack_BC, do_AB) and

               (empty_section -> true) and

               (true -> implies(edge(not empty_section), pre grant_access)) and

               (true -> implies(edge(on_C), pre grant_exit)) and

               implies(edge(not on_A), on_B) and

               implies(edge(not on_B), on_A or on_C) );

   no_collision = implies(grant_access, empty_section);

   exclusive_req = not(do_AB and do_BC);

   no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B);

   no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section);

   OK = env => no_collision and exclusive_req and

                     no_derail_AB and no_derail_BC;

  --%MAIN;

  --%PROPERTY  OK=true;

tel