lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / memory2 / MOESI_2_e3_929_e5_1826.lus @ 2d37a1e1
History | View | Annotate | Download (3 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
7 |
let |
8 |
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or |
9 |
X2 and X3 or X2 and X4 or |
10 |
X3 and X4 ); |
11 |
tel |
12 |
node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns( |
13 |
modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool |
14 |
); |
15 |
var |
16 |
garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool; |
17 |
let |
18 |
garde_mo1 = pre invalid_mo >= 1; |
19 |
garde_mo2 = pre exclusive_mo>=1; |
20 |
garde_mo3 = pre shared_mo -1- pre owned_mo>=1; |
21 |
garde_mo4 = pre invalid_mo>=1; |
22 |
erreur_mo = false -> exclusive_mo >= 2; |
23 |
modified_mo = 0 -> |
24 |
if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else |
25 |
if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else |
26 |
if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else |
27 |
if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else |
28 |
pre modified_mo; |
29 |
exclusive_mo = 0 -> |
30 |
if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else |
31 |
if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else |
32 |
if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else |
33 |
if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else |
34 |
pre exclusive_mo; |
35 |
shared_mo = 0 -> |
36 |
if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else |
37 |
if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else |
38 |
if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else |
39 |
pre shared_mo; |
40 |
invalid_mo = init_invalid_mo -> |
41 |
if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else |
42 |
if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else |
43 |
if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else |
44 |
pre invalid_mo; |
45 |
owned_mo = 0 -> |
46 |
if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else |
47 |
if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else |
48 |
if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else |
49 |
pre owned_mo; |
50 |
tel |
51 |
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool ) |
52 |
returns ( OK : bool ); |
53 |
--@ contract guarantees OK; |
54 |
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; |
55 |
erreur_mo : bool; |
56 |
env : bool; |
57 |
let |
58 |
( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) = |
59 |
moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 ); |
60 |
env = Sofar( excludes4( etat_mo1, etat_mo2, etat_mo3, etat_mo4 ) ); |
61 |
OK = env => (true -> |
62 |
(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo) = |
63 |
pre(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo)); |
64 |
--%MAIN; |
65 |
--%PROPERTY OK=true; |
66 |
tel |