## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / protocol / swimmingpool_7.lus @ 2d37a1e1

History | View | Annotate | Download (2.72 KB)

1 | b8dc00eb | bourbouh | -- |
---|---|---|---|

2 | -- Source: David Merchat (node swimingpool) |
||

3 | -- |
||

4 | |||

5 | node First( X : int ) returns ( First : int ); |
||

6 | let |
||

7 | First = X -> pre First; |
||

8 | tel |
||

9 | |||

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

11 | let |
||

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

13 | tel |
||

14 | |||

15 | node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool ); |
||

16 | let |
||

17 | excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or |
||

18 | X1 and not X2 and not X3 and not X4 and not X5 and not X6 or |
||

19 | not X1 and X2 and not X3 and not X4 and not X5 and not X6 or |
||

20 | not X1 and not X2 and X3 and not X4 and not X5 and not X6 or |
||

21 | not X1 and not X2 and not X3 and X4 and not X5 and not X6 or |
||

22 | not X1 and not X2 and not X3 and not X4 and X5 and not X6 or |
||

23 | not X1 and not X2 and not X3 and not X4 and not X5 and X6; |
||

24 | tel |
||

25 | |||

26 | node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns |
||

27 | (x1, x2, x3, x4, x5, x6, x7, p1, p2 : int); |
||

28 | var |
||

29 | g1, g2, g3, g4, g5, g6 : bool; |
||

30 | let |
||

31 | |||

32 | g1 = false -> pre x6>=1; |
||

33 | g2 = false -> pre x1>=1 and pre x7>=1; |
||

34 | g3 = false -> pre x2>=1; |
||

35 | g4 = false -> pre x3>=1 and pre x6>=1; |
||

36 | g5 = false -> pre x4>=1; |
||

37 | g6 = false -> pre x5>=1; |
||

38 | |||

39 | x1 = 0 -> |
||

40 | if(e1) then if(g1) then pre x1+1 else pre x1 else |
||

41 | if(e2) then if(g2) then pre x1-1 else pre x1 else |
||

42 | pre x1; |
||

43 | |||

44 | x2 = 0 -> |
||

45 | if(e2) then if(g2) then pre x2+1 else pre x2 else |
||

46 | if(e3) then if(g3) then pre x2-1 else pre x2 else |
||

47 | pre x2; |
||

48 | |||

49 | x3 = 0 -> |
||

50 | if(e3) then if(g3) then pre x3+1 else pre x3 else |
||

51 | if(e4) then if(g4) then pre x3-1 else pre x3 else |
||

52 | pre x3; |
||

53 | |||

54 | x4 = 0 -> |
||

55 | if(e4) then if(g4) then pre x4+1 else pre x4 else |
||

56 | if(e5) then if(g4) then pre x4-1 else pre x4 else |
||

57 | pre x4; |
||

58 | |||

59 | x5 = 0 -> |
||

60 | if(e5) then if(g5) then pre x5+1 else pre x5 else |
||

61 | if(e6) then if(g6) then pre x5-1 else pre x5 else |
||

62 | pre x5; |
||

63 | |||

64 | x6 = p1 -> |
||

65 | if(e1) then if(g1) then pre x6-1 else pre x6 else |
||

66 | if(e3) then if(g3) then pre x6+1 else pre x6 else |
||

67 | if(e4) then if(g4) then pre x6-1 else pre x6 else |
||

68 | if(e6) then if(g6) then pre x6+1 else pre x6 else |
||

69 | pre x6; |
||

70 | |||

71 | x7 = p2 -> |
||

72 | if(e2) then if(g2) then pre x7-1 else pre x7 else |
||

73 | if(e5) then if(g5) then pre x7+1 else pre x7 else |
||

74 | pre x7; |
||

75 | |||

76 | p1 = init_p1 -> |
||

77 | pre p1; |
||

78 | |||

79 | p2 = init_p2 -> |
||

80 | pre p2; |
||

81 | |||

82 | tel |
||

83 | |||

84 | node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int) |
||

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

86 | 2d37a1e1 | ploc | --@ contract guarantees OK; |

87 | b8dc00eb | bourbouh | var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int; |

88 | env : bool; |
||

89 | let |
||

90 | (x1, x2, x3, x4, x5, x6, x7, p1, p2) = |
||

91 | swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2); |
||

92 | env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and |
||

93 | 0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000; |
||

94 | OK = env => x5 < 2; |
||

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

96 | --%MAIN; |
||

97 | tel |