## lustrec / test / src / kind_fmcad08 / simulation / ums_e8_1032.lus @ 65f71d05

History | View | Annotate | Download (2.46 KB)

1 | |
---|---|

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

3 |
let |

4 |
Sofar = X -> X and pre Sofar; |

5 |
tel |

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

7 |
let |

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

9 |
tel |

10 |
node after(A: bool) returns(afterA: bool); |

11 |
let |

12 |
afterA = false -> pre(A and afterA); |

13 |
tel |

14 |
node always_since(B, A: bool) returns(alwaysBsinceA: bool); |

15 |
let |

16 |
alwaysBsinceA = if A then B else if after(A) then |

17 |
B and pre(alwaysBsinceA) else true; |

18 |
tel |

19 |
node once_since(C, A: bool) returns(onceCsinceA: bool); |

20 |
let |

21 |
onceCsinceA = if A then C else if after(A) then |

22 |
C or pre(onceCsinceA) else true; |

23 |
tel |

24 |
node implies(A, B: bool) returns(AimpliesB: bool); |

25 |
let |

26 |
AimpliesB = not A or B; |

27 |
tel |

28 |
node always_from_to(B, A, C: bool) returns(X: bool); |

29 |
let |

30 |
X = implies(after(A), always_since(B, A) or once_since(C, A)); |

31 |
tel |

32 |
node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool) |

33 |
returns(grant_access, grant_exit, do_AB, do_BC: bool); |

34 |
var |

35 |
empty_section, only_on_B: bool; |

36 |
let |

37 |
grant_access = empty_section and ack_AB; |

38 |
grant_exit = only_on_B and ack_BC; |

39 |
do_AB = not ack_AB and empty_section; |

40 |
do_BC = not ack_BC and only_on_B; |

41 |
empty_section = not(on_A or on_B or on_C); |

42 |
only_on_B = on_B and not(on_A or on_C); |

43 |
tel |

44 |
--@ ensures OK; |

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

46 |
returns(OK: bool); |

47 |
var |

48 |
grant_access, grant_exit: bool; |

49 |
do_AB, do_BC: bool; |

50 |
no_collision, exclusive_req: bool; |

51 |
no_derail_AB, no_derail_BC: bool; |

52 |
empty_section, only_on_B: bool; |

53 |
env : bool; |

54 |
let |

55 |
empty_section = not(on_A or on_B or on_C); |

56 |
only_on_B = on_B and not(on_A or on_C); |

57 |
(grant_access, grant_exit, do_AB, do_BC) = |

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

59 |
env = Sofar( not(ack_AB and ack_BC) and |

60 |
always_from_to(ack_AB, ack_AB, do_BC) and |

61 |
always_from_to(ack_BC, ack_BC, do_AB) and |

62 |
(empty_section -> true) and |

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

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

65 |
implies(edge(not on_A), on_B) and |

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

67 |
no_collision = implies(grant_access, empty_section); |

68 |
exclusive_req = not(do_AB and do_BC); |

69 |
no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B); |

70 |
no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section); |

71 |
OK = env => no_collision and exclusive_req and |

72 |
no_derail_AB and no_derail_BC; |

73 |
--%MAIN; |

74 |
--%PROPERTY OK=true; |

75 |
tel |