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

History | View | Annotate | Download (2.58 KB)

1 |
-- |
---|---|

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 |