|
1
|
|
|
2
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
|
3
|
let
|
|
4
|
Sofar = X -> X and 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 => t >= 0;
|
|
87
|
--%MAIN;
|
|
88
|
--!k:2;
|
|
89
|
--!PROPERTY: OK=true;
|
|
90
|
tel
|