Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory2 / MOESI_2_e3_929_e3_2294.lus @ 22fe1c93

History | View | Annotate | Download (2.98 KB)

1 22fe1c93 ploc
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 - 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
    var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
54
        erreur_mo : bool;
55
        env : bool;
56
let
57
    ( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) =
58
        moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 );
59
    env = Sofar( excludes4( etat_mo1, etat_mo2, etat_mo3, etat_mo4 ) );
60
    OK = env => (true ->
61
          (modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo) =
62
          pre(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo));
63
  --%MAIN;
64
  --%PROPERTY  OK=true;
65
tel