lustrec / test / src / kind_fmcad08 / memory2 / SYNAPSE_2_e8_1118_e2_237.lus @ 65f71d05
History | View | Annotate | Download (1.73 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 excludes3( X1, X2, X3 : bool ) returns ( excludes : bool ); |
||
| 7 | let |
||
| 8 | excludes = not ( X1 and X2 and X1 and X3 or X2 and X3 ); |
||
| 9 | tel |
||
| 10 | node synapse(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) |
||
| 11 | returns(invalid_s, valid_s, dirty_s : int; mem_init_s : int ); |
||
| 12 | var |
||
| 13 | garde_s1, garde_s2, garde_s3 : bool; |
||
| 14 | let |
||
| 15 | garde_s1 = pre invalid_s>=1; |
||
| 16 | garde_s2 = pre valid_s>=1; |
||
| 17 | garde_s3 = pre invalid_s>=1; |
||
| 18 | mem_init_s = init_invalid_s -> pre mem_init_s; |
||
| 19 | invalid_s = mem_init_s -> |
||
| 20 | if(e_s1) then if(garde_s1) then pre invalid_s -1+ pre dirty_s -1 else pre invalid_s else |
||
| 21 | if(e_s2) then if(garde_s2) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else |
||
| 22 | if(e_s3) then if(garde_s3) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else |
||
| 23 | pre invalid_s; |
||
| 24 | valid_s = 0 -> |
||
| 25 | if(e_s1) then if(garde_s1) then pre valid_s +1 else pre valid_s else |
||
| 26 | if(e_s2) then if(garde_s2) then 0 else pre valid_s else |
||
| 27 | if(e_s3) then if(garde_s3) then 0 else pre valid_s else |
||
| 28 | pre valid_s; |
||
| 29 | dirty_s = 0 -> |
||
| 30 | if(e_s1) then if(garde_s1) then 0 else pre dirty_s else |
||
| 31 | if(e_s2) then if(garde_s2) then 1 else pre dirty_s else |
||
| 32 | if(e_s3) then if(garde_s3) then 1 else pre dirty_s else |
||
| 33 | pre dirty_s; |
||
| 34 | tel |
||
| 35 | 65f71d05 | ploc | --@ ensures OK; |
| 36 | 22fe1c93 | ploc | node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) |
| 37 | returns( OK : bool ); |
||
| 38 | var invalid_s, valid_s, dirty_s : int; mem_init_s : int; |
||
| 39 | env : bool; |
||
| 40 | let |
||
| 41 | ( invalid_s, valid_s, dirty_s, mem_init_s ) = |
||
| 42 | synapse(e_s1, e_s2, e_s3, init_invalid_s ); |
||
| 43 | env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 ); |
||
| 44 | OK = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s)); |
||
| 45 | --%MAIN; |
||
| 46 | --%PROPERTY OK=true; |
||
| 47 | tel |