lustrec / test / src / kind_fmcad08 / misc / ticket3i_1.lus @ 22fe1c93
History | View | Annotate | Download (3.53 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
|
7 |
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); |
8 |
let |
9 |
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 |
10 |
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 |
11 |
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 |
12 |
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 |
13 |
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 |
14 |
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 |
15 |
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 |
16 |
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 |
17 |
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 |
18 |
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; |
19 |
tel |
20 |
|
21 |
node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; |
22 |
init_a1, init_a2, init_a3, init_t : int) returns ( |
23 |
p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool); |
24 |
var |
25 |
g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; |
26 |
let |
27 |
|
28 |
erreur_ticket3i = if((p1>=3) or (p2>=3) or (p3>=3)) then true else false; |
29 |
|
30 |
g1 = pre p1 = 0; |
31 |
g2 = pre p1 = 1 and pre s >= a1; |
32 |
g3 = pre p1 = 2; |
33 |
g4 = pre p2 = 0; |
34 |
g5 = pre p2 = 1 and pre s >= a2; |
35 |
g6 = pre p2 = 2; |
36 |
g7 = pre p3 = 0; |
37 |
g8 = pre p3 = 1 and pre s >= a3; |
38 |
g9 = pre p3 = 2; |
39 |
|
40 |
p1 = 0 -> |
41 |
if(e1) then if(g1) then 1 else pre p1 else |
42 |
if(e2) then if(g2) then 2 else pre p1 else |
43 |
if(e3) then if(g3) then 0 else pre p1 else |
44 |
pre p1; |
45 |
|
46 |
p2 = 0 -> |
47 |
if(e4) then if(g4) then 1 else pre p2 else |
48 |
if(e5) then if(g5) then 2 else pre p2 else |
49 |
if(e6) then if(g6) then 0 else pre p2 else |
50 |
pre p2; |
51 |
|
52 |
p3 = 0 -> |
53 |
if(e7) then if(g7) then 1 else pre p3 else |
54 |
if(e8) then if(g8) then 2 else pre p3 else |
55 |
if(e9) then if(g9) then 0 else pre p3 else |
56 |
pre p3; |
57 |
|
58 |
t = init_t -> |
59 |
if(e1) then if(g1) then pre t+1 else pre t else |
60 |
if(e4) then if(g4) then pre t+1 else pre t else |
61 |
if(e7) then if(g7) then pre t+1 else pre t else |
62 |
pre t; |
63 |
|
64 |
s = t -> |
65 |
if(e3) then if(g3) then pre s+1 else pre s else |
66 |
if(e6) then if(g6) then pre s+1 else pre s else |
67 |
if(e9) then if(g9) then pre s+1 else pre s else |
68 |
pre s; |
69 |
|
70 |
a1 = init_a1 -> |
71 |
if(e1) then if(g1) then pre t else pre a1 else |
72 |
pre a1; |
73 |
|
74 |
a2 = init_a2 -> |
75 |
if(e4) then if(g4) then pre t else pre a2 else |
76 |
pre a2; |
77 |
|
78 |
a3 = init_a3 -> |
79 |
if(e7) then if(g7) then pre t else pre a3 else |
80 |
pre a3; |
81 |
|
82 |
tel |
83 |
|
84 |
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; |
85 |
init_a1, init_a2, init_a3, init_t : int ) |
86 |
returns ( OK : bool ); |
87 |
var p1, p2, p3, t, s, a1, a2, a3 : int; |
88 |
erreur_ticket3i : bool; |
89 |
let |
90 |
( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) = |
91 |
ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9, |
92 |
init_a1, init_a2, init_a3, init_t ); |
93 |
OK = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |
94 |
init_a1 >= 0 and |
95 |
init_a2 >= 0 and |
96 |
init_a3 >= 0 and |
97 |
init_t >= 0 ) |
98 |
=> not erreur_ticket3i; |
99 |
--%PROPERTY OK=true; |
100 |
--%MAIN; |
101 |
|
102 |
tel |