lustrec / test / src / kind_fmcad08 / memory2 / SYNAPSE_all_e8_251_e1_1852.lus @ 0cbf0839
History | View | Annotate | Download (1.95 KB)
1 |
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 and pre Sofar; |
8 |
tel |
9 |
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool ); |
10 |
let |
11 |
excludes = not ( X1 and X2 and 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 +1+ 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 |