### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / test / src / kind_fmcad08 / simulation / ums_e7_1700.lus @ 22fe1c93

History | View | Annotate | Download (2.44 KB)

1 2 3 22fe1c93 ploc ```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); ``` ```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`