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