## lustrec / test / src / kind_fmcad08 / protocol / swimmingpool_4.lus @ 22fe1c93

History | View | Annotate | Download (2.7 KB)

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

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 | |

16 | |

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

18 |
let |

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

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

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

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

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

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

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

26 |
tel |

27 | |

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

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

30 |
var |

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

32 |
let |

33 | |

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

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

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

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

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

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

40 | |

41 |
x1 = 0 -> |

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

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

44 |
pre x1; |

45 | |

46 |
x2 = 0 -> |

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

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

49 |
pre x2; |

50 | |

51 |
x3 = 0 -> |

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

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

54 |
pre x3; |

55 | |

56 |
x4 = 0 -> |

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

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

59 |
pre x4; |

60 | |

61 |
x5 = 0 -> |

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

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

64 |
pre x5; |

65 | |

66 |
x6 = p1 -> |

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

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

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

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

71 |
pre x6; |

72 | |

73 |
x7 = p2 -> |

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

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

76 |
pre x7; |

77 | |

78 |
p1 = init_p1 -> |

79 |
pre p1; |

80 | |

81 |
p2 = init_p2 -> |

82 |
pre p2; |

83 | |

84 |
tel |

85 | |

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

87 |
returns ( OK : bool ); |

88 |
var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int; |

89 |
env : bool; |

90 |
let |

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

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

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

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

95 |
OK = env => x3 < 1; |

96 |
--%PROPERTY OK=true; |

97 |
--%MAIN; |

98 |
tel |