lustrec / test / src / kind_fmcad08 / memory2 / MOESI_1.lus @ 65f71d05
History | View | Annotate | Download (2.9 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 excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
||
| 8 | let |
||
| 9 | excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or |
||
| 10 | X2 and X3 or X2 and X4 or |
||
| 11 | X3 and X4 ); |
||
| 12 | tel |
||
| 13 | |||
| 14 | node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns( |
||
| 15 | modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool |
||
| 16 | ); |
||
| 17 | var |
||
| 18 | garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool; |
||
| 19 | let |
||
| 20 | |||
| 21 | garde_mo1 = pre invalid_mo >= 1; |
||
| 22 | garde_mo2 = pre exclusive_mo>=1; |
||
| 23 | garde_mo3 = pre shared_mo + pre owned_mo>=1; |
||
| 24 | garde_mo4 = pre invalid_mo>=1; |
||
| 25 | |||
| 26 | erreur_mo = false -> exclusive_mo >= 2; |
||
| 27 | |||
| 28 | modified_mo = 0 -> |
||
| 29 | if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else |
||
| 30 | if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else |
||
| 31 | if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else |
||
| 32 | if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else |
||
| 33 | pre modified_mo; |
||
| 34 | |||
| 35 | exclusive_mo = 0 -> |
||
| 36 | if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else |
||
| 37 | if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else |
||
| 38 | if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else |
||
| 39 | if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else |
||
| 40 | pre exclusive_mo; |
||
| 41 | |||
| 42 | shared_mo = 0 -> |
||
| 43 | if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else |
||
| 44 | if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else |
||
| 45 | if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else |
||
| 46 | pre shared_mo; |
||
| 47 | |||
| 48 | invalid_mo = init_invalid_mo -> |
||
| 49 | if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else |
||
| 50 | 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 |
||
| 51 | 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 |
||
| 52 | pre invalid_mo; |
||
| 53 | |||
| 54 | owned_mo = 0 -> |
||
| 55 | if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else |
||
| 56 | if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else |
||
| 57 | if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else |
||
| 58 | pre owned_mo; |
||
| 59 | |||
| 60 | tel |
||
| 61 | |||
| 62 | 65f71d05 | ploc | --@ ensures OK; |
| 63 | 22fe1c93 | ploc | node top( init_invalid_mo : int; |
| 64 | etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool ) |
||
| 65 | returns ( OK : bool ); |
||
| 66 | var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; |
||
| 67 | erreur_mo : bool; |
||
| 68 | let |
||
| 69 | ( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) = |
||
| 70 | moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 ); |
||
| 71 | OK = Sofar( excludes4(etat_mo1, etat_mo2, etat_mo3, etat_mo4) |
||
| 72 | and init_invalid_mo > 0 ) |
||
| 73 | => not erreur_mo; |
||
| 74 | --%PROPERTY OK=true; |
||
| 75 | --%MAIN; |
||
| 76 | tel |