lustrec / test / src / kind_fmcad08 / memory2 / MESI_3.lus @ 65f71d05
History | View | Annotate | Download (2.74 KB)
| 1 | 22fe1c93 | ploc | |
|---|---|---|---|
| 2 | node Sofar( X : bool ) returns ( Sofar : bool ); |
||
| 3 | let |
||
| 4 | Sofar = X -> X and pre Sofar; |
||
| 5 | tel |
||
| 6 | |||
| 7 | node Abs( X : int ) returns ( Abs : int ); |
||
| 8 | let |
||
| 9 | Abs = if X < 0 then -X else X; |
||
| 10 | tel |
||
| 11 | |||
| 12 | node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
||
| 13 | let |
||
| 14 | excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or |
||
| 15 | X2 and X3 or X2 and X4 or |
||
| 16 | X3 and X4 ); |
||
| 17 | tel |
||
| 18 | |||
| 19 | node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool |
||
| 20 | ) returns ( |
||
| 21 | modified_me, exclusive_me, shared_me, invalid_me : int |
||
| 22 | ); |
||
| 23 | var |
||
| 24 | garde_me1, garde_me2, garde_me3, garde_me4 : bool; |
||
| 25 | let |
||
| 26 | |||
| 27 | garde_me1 = pre invalid_me >= 1; |
||
| 28 | garde_me2 = pre exclusive_me>=1; |
||
| 29 | garde_me3 = pre shared_me>=1; |
||
| 30 | garde_me4 = pre invalid_me>=1; |
||
| 31 | |||
| 32 | modified_me = 0 -> |
||
| 33 | if(etat_me1) then if(garde_me1) then 0 else pre modified_me else |
||
| 34 | if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else |
||
| 35 | if(etat_me3) then if(garde_me3) then 0 else pre modified_me else |
||
| 36 | if(etat_me4) then if(garde_me4) then 0 else pre modified_me else |
||
| 37 | pre modified_me; |
||
| 38 | |||
| 39 | exclusive_me = 0 -> |
||
| 40 | if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else |
||
| 41 | if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else |
||
| 42 | if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else |
||
| 43 | if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else |
||
| 44 | pre exclusive_me; |
||
| 45 | |||
| 46 | shared_me = 0 -> |
||
| 47 | if(etat_me1) then if(garde_me1) then pre shared_me + pre exclusive_me + pre modified_me - 1 else pre shared_me else |
||
| 48 | if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else |
||
| 49 | if(etat_me3) then if(garde_me3) then 0 else pre shared_me else |
||
| 50 | if(etat_me4) then if(garde_me4) then 0 else pre shared_me else |
||
| 51 | pre shared_me; |
||
| 52 | |||
| 53 | invalid_me = 3 -> |
||
| 54 | if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else |
||
| 55 | if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else |
||
| 56 | if(etat_me3) then if(garde_me3) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
||
| 57 | if(etat_me4) then if(garde_me4) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
||
| 58 | pre invalid_me; |
||
| 59 | |||
| 60 | tel |
||
| 61 | |||
| 62 | -- Only provable in nbac |
||
| 63 | 65f71d05 | ploc | --@ ensures OK; |
| 64 | 22fe1c93 | ploc | node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); |
| 65 | var modified_me, exclusive_me, shared_me, invalid_me : int; |
||
| 66 | env : bool; |
||
| 67 | let |
||
| 68 | ( modified_me, exclusive_me, shared_me, invalid_me ) = |
||
| 69 | mesi( etat_me1, etat_me2, etat_me3, etat_me4 ); |
||
| 70 | env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) ); |
||
| 71 | OK = env => (Abs(modified_me)+Abs(exclusive_me)+ |
||
| 72 | Abs(shared_me)+Abs(invalid_me)) <= 3; |
||
| 73 | --%PROPERTY OK=true; |
||
| 74 | --%MAIN; |
||
| 75 | tel |