Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / ums_e7_1700.lus @ 0c9457a0

History | View | Annotate | Download (2.45 KB)

1 2 3 b8dc00eb bourbouh 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 --@ ensures OK; 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