Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory2 / SYNAPSE_2_e8_1118_e1_667.lus @ 22fe1c93

History | View | Annotate | Download (1.72 KB)

1

    
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
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
36
returns( OK : bool );
37
    var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
38
        env : bool;
39
let
40
    ( invalid_s, valid_s, dirty_s, mem_init_s ) = 
41
        synapse(e_s1, e_s2, e_s3, init_invalid_s );
42
    env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
43
    OK = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s));
44
  --%MAIN;
45
  --%PROPERTY  OK=true;
46
tel