## lustrec / test / src / kind_fmcad08 / simulation / ums.lus @ 0cbf0839

History | View | Annotate | Download (2.58 KB)

1 | 0cbf0839 | ploc | -- |
---|---|---|---|

2 | -- Source: Magnus Ljung |
||

3 | -- This is the source to the UMS example. It is taken from HLR92. |
||

4 | -- |
||

5 | |||

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

7 | let |
||

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

9 | tel |
||

10 | |||

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

12 | let |
||

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

14 | tel |
||

15 | |||

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

17 | let |
||

18 | afterA = false -> pre(A or afterA); |
||

19 | tel |
||

20 | |||

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

22 | let |
||

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

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

25 | tel |
||

26 | |||

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

28 | let |
||

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

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

31 | tel |
||

32 | |||

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

34 | let |
||

35 | AimpliesB = not A or B; |
||

36 | tel |
||

37 | |||

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

39 | let |
||

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

41 | tel |
||

42 | |||

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

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

45 | var |
||

46 | empty_section, only_on_B: bool; |
||

47 | let |
||

48 | grant_access = empty_section and ack_AB; |
||

49 | grant_exit = only_on_B and ack_BC; |
||

50 | do_AB = not ack_AB and empty_section; |
||

51 | do_BC = not ack_BC and only_on_B; |
||

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

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

54 | tel |
||

55 | |||

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

57 | returns(OK: bool); |
||

58 | var |
||

59 | grant_access, grant_exit: bool; |
||

60 | do_AB, do_BC: bool; |
||

61 | no_collision, exclusive_req: bool; |
||

62 | no_derail_AB, no_derail_BC: bool; |
||

63 | empty_section, only_on_B: bool; |
||

64 | env : bool; |
||

65 | let |
||

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

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

68 | |||

69 | -- UMS CALL |
||

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

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

72 | |||

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

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

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

76 | (empty_section -> true) and |
||

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

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

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

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

81 | |||

82 | -- PROPERTIES |
||

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

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

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

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

87 | |||

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

89 | no_derail_AB and no_derail_BC; |
||

90 | --%PROPERTY OK=true; |
||

91 | --%MAIN; |
||

92 | tel |