lustrec / test / src / kind_fmcad08 / simulation / PRODUCER_CONSUMER_3.lus @ 22fe1c93
History | View | Annotate | Download (1.51 KB)
1 |
node First( X : int ) returns ( First : int ); |
---|---|
2 |
let |
3 |
First = X -> pre First; |
4 |
tel |
5 |
|
6 |
node FirstB( X : bool ) returns ( First : bool ); |
7 |
let |
8 |
First = X -> pre First; |
9 |
tel |
10 |
|
11 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
12 |
let |
13 |
Sofar = X -> X and pre Sofar; |
14 |
tel |
15 |
|
16 |
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool ); |
17 |
let |
18 |
excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 ); |
19 |
tel |
20 |
|
21 |
node PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int |
22 |
) returns(i, b, a, o1, o2 : int); |
23 |
var |
24 |
garde1, garde2, garde3 : bool; |
25 |
let |
26 |
garde1 = pre i >= 1; |
27 |
garde2 = pre b >= 1; |
28 |
garde3 = pre b >= 1; |
29 |
|
30 |
i = a -> |
31 |
if(etat1) then if(garde1) then pre i -1 else pre i else |
32 |
pre i; |
33 |
|
34 |
b = 0 -> |
35 |
if(etat1) then if(garde1) then pre b+1 else pre b else |
36 |
if(etat2) then if(garde2) then pre b-1 else pre b else |
37 |
if(garde3) then pre b-1 else pre b; |
38 |
|
39 |
a = a_init -> pre a; |
40 |
|
41 |
o1 = 0 -> |
42 |
if(etat2) then if(garde2) then pre o1+1 else pre o1 else |
43 |
pre o1; |
44 |
|
45 |
o2 = 0 -> |
46 |
if(etat3) then if(garde3) then pre o2+1 else pre o2 else |
47 |
pre o2; |
48 |
|
49 |
tel |
50 |
|
51 |
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool ); |
52 |
var i, b, a, o1, o2 : int; |
53 |
env : bool; |
54 |
let |
55 |
( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER(etat1, etat2, etat3, a_init ); |
56 |
env = Sofar( excludes3( etat1, etat2, etat3 ) or |
57 |
not ( etat1 or etat2 or etat3 ) ) and |
58 |
FirstB( not ( etat1 or etat2 or etat3 ) ) and |
59 |
First( a_init ) > 0; |
60 |
OK = env => (true -> pre etat1 and etat2 => (o1 = pre o1+1 or o1 = pre o1)); |
61 |
--%PROPERTY OK=true; |
62 |
--%MAIN; |
63 |
tel |