lustrec / test / src / kind_fmcad08 / misc / ticket3i_3_e8_1703_e7_3491.lus @ 0cbf0839
History | View | Annotate | Download (3.52 KB)
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) and (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 |
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; |
71 |
init_a1, init_a2, init_a3, init_t : int ) |
72 |
returns ( OK : bool ); |
73 |
var p1, p2, p3, t, s, a1, a2, a3 : int; |
74 |
erreur_ticket3i : bool; |
75 |
env : bool; |
76 |
let |
77 |
( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) = |
78 |
ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9, |
79 |
init_a1, init_a2, init_a3, init_t ); |
80 |
env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |
81 |
init_a1 >= 0 and |
82 |
init_a2 >= 0 and |
83 |
init_a3 >= 0 and |
84 |
init_t >= 0 ); |
85 |
OK = env => t >= 0; |
86 |
--%MAIN; |
87 |
--%PROPERTY OK=true; |
88 |
tel |