1


2

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

3

let

4

Sofar = X > X or pre Sofar;

5

tel

6

node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool );

7

let

8

excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

9

X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

10

not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

11

not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

12

not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 and not X9 or

13

not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 and not X9 or

14

not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 and not X9 or

15

not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 and not X9 or

16

not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8 and not X9 or

17

not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and X9;

18

tel

19

node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;

20

init_a1, init_a2, init_a3, init_t : int) returns (

21

p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool);

22

var

23

g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;

24

let

25

erreur_ticket3i = if((p1>=3) or (p2>=3) or (p3>=3)) then true else false;

26

g1 = pre p1 = 0;

27

g2 = pre p1 = 1 and pre s >= a1;

28

g3 = pre p1 = 2;

29

g4 = pre p2 = 0;

30

g5 = pre p2 = 1 and pre s >= a2;

31

g6 = pre p2 = 2;

32

g7 = pre p3 = 0;

33

g8 = pre p3 = 1 and pre s >= a3;

34

g9 = pre p3 = 2;

35

p1 = 0 >

36

if(e1) then if(g1) then 1 else pre p1 else

37

if(e2) then if(g2) then 2 else pre p1 else

38

if(e3) then if(g3) then 0 else pre p1 else

39

pre p1;

40

p2 = 0 >

41

if(e4) then if(g4) then 1 else pre p2 else

42

if(e5) then if(g5) then 2 else pre p2 else

43

if(e6) then if(g6) then 0 else pre p2 else

44

pre p2;

45

p3 = 0 >

46

if(e7) then if(g7) then 1 else pre p3 else

47

if(e8) then if(g8) then 2 else pre p3 else

48

if(e9) then if(g9) then 0 else pre p3 else

49

pre p3;

50

t = init_t >

51

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

52

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

53

if(e7) then if(g7) then pre t+1 else pre t else

54

pre t;

55

s = t >

56

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

57

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

58

if(e9) then if(g9) then pre s+1 else pre s else

59

pre s;

60

a1 = init_a1 >

61

if(e1) then if(g1) then pre t else pre a1 else

62

pre a1;

63

a2 = init_a2 >

64

if(e4) then if(g4) then pre t else pre a2 else

65

pre a2;

66

a3 = init_a3 >

67

if(e7) then if(g7) then pre t else pre a3 else

68

pre a3;

69

tel

70

@ ensures OK;

71

node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;

72

init_a1, init_a2, init_a3, init_t : int )

73

returns ( OK : bool );

74

var p1, p2, p3, t, s, a1, a2, a3 : int;

75

erreur_ticket3i : bool;

76

env : bool;

77

let

78

( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) =

79

ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9,

80

init_a1, init_a2, init_a3, init_t );

81

env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and

82

init_a1 >= 0 and

83

init_a2 >= 0 and

84

init_a3 >= 0 and

85

init_t >= 0 );

86

OK = env => not erreur_ticket3i and

87

0 <= p1 and p1 <= 3 and

88

0 <= p2 and p2 <= 3 and

89

0 <= p3 and p3 <= 3 and

90

p1  p2 + p3 <= 9;

91

%MAIN;

92

%PROPERTY OK=true;

93

tel
