Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.96 KB)

1
node First( X : int ) returns ( First : int );
2
let
3
    First = X -> pre First;
4
tel
5

    
6
node Sofar( X : bool ) returns ( Sofar : bool );
7
let
8
    Sofar = X -> X and pre Sofar;
9
tel
10

    
11
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );
12
let
13
    excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 );
14
tel
15

    
16
node synapse(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) 
17
returns(invalid_s, valid_s, dirty_s : int; mem_init_s : int );
18
var
19
	garde_s1, garde_s2, garde_s3 : bool;
20

    
21
let
22

    
23
	garde_s1 = pre invalid_s>=1;
24
	garde_s2 = pre valid_s>=1;
25
	garde_s3 = pre invalid_s>=1;
26

    
27
	mem_init_s = init_invalid_s -> pre mem_init_s;
28

    
29
	invalid_s = mem_init_s -> 
30
	if(e_s1) then if(garde_s1) then pre invalid_s + pre dirty_s -1 else pre invalid_s else
31
	if(e_s2) then if(garde_s2) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else
32
	if(e_s3) then if(garde_s3) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else 
33
	pre invalid_s;
34

    
35
	valid_s = 0 ->
36
	if(e_s1) then if(garde_s1) then pre valid_s +1 else pre valid_s else
37
	if(e_s2) then if(garde_s2) then 0 else pre valid_s else
38
	if(e_s3) then if(garde_s3) then 0 else pre valid_s else 
39
	pre valid_s;
40

    
41
	dirty_s = 0 ->
42
	if(e_s1) then if(garde_s1) then 0 else pre dirty_s else 
43
	if(e_s2) then if(garde_s2) then 1 else pre dirty_s else 
44
	if(e_s3) then if(garde_s3) then 1 else pre dirty_s else 
45
	pre dirty_s;
46

    
47
tel
48

    
49
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
50
returns( OK : bool );
51
    var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
52
        env : bool;
53
let
54
    ( invalid_s, valid_s, dirty_s, mem_init_s ) = 
55
        synapse(e_s1, e_s2, e_s3, init_invalid_s );
56

    
57
    env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
58

    
59
    OK = env => dirty_s < 2 and
60
                  (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s)) and
61
                  invalid_s+valid_s+dirty_s = First( init_invalid_s ) and
62
                  (dirty_s<1 or valid_s<1);
63
    --%PROPERTY OK=true;
64
    --%MAIN;
65
tel