1


2

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

3

let

4

First = X > pre First;

5

tel

6

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

7

let

8

Sofar = X > X or pre Sofar;

9

tel

10

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

11

let

12

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

13

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

14

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

15

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

16

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

17

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

18

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

19

tel

20

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

21

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

22

var

23

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

24

let

25

g1 = false > pre x6>=1;

26

g2 = false > pre x1>=1 and pre x7>=1;

27

g3 = false > pre x2>=1;

28

g4 = false > pre x3>=1 and pre x6>=1;

29

g5 = false > pre x4>=1;

30

g6 = false > pre x5>=1;

31

x1 = 0 >

32

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

33

if(e2) then if(g2) then pre x11 else pre x1 else

34

pre x1;

35

x2 = 0 >

36

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

37

if(e3) then if(g3) then pre x21 else pre x2 else

38

pre x2;

39

x3 = 0 >

40

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

41

if(e4) then if(g4) then pre x31 else pre x3 else

42

pre x3;

43

x4 = 0 >

44

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

45

if(e5) then if(g4) then pre x41 else pre x4 else

46

pre x4;

47

x5 = 0 >

48

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

49

if(e6) then if(g6) then pre x51 else pre x5 else

50

pre x5;

51

x6 = p1 >

52

if(e1) then if(g1) then pre x61 else pre x6 else

53

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

54

if(e4) then if(g4) then pre x61 else pre x6 else

55

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

56

pre x6;

57

x7 = p2 >

58

if(e2) then if(g2) then pre x71 else pre x7 else

59

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

60

pre x7;

61

p1 = init_p1 >

62

pre p1;

63

p2 = init_p2 >

64

pre p2;

65

tel

66

@ ensures OK;

67

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

68

returns ( OK : bool );

69

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

70

env : bool;

71

let

72

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

73

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

74

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

75

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

76

OK = env => x5 < 1;

77

%MAIN;

78

%PROPERTY OK=true;

79

tel
