Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.76 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 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 +1+ pre dirty_s -1 else pre invalid_s else
24
	if(e_s2) then if(garde_s2) then pre invalid_s +1+ 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 => valid_s <= First( init_invalid_s );
47
  --%MAIN;
48
  --%PROPERTY  OK=true;
49
tel