Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory2 / SYNAPSE_123.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

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

    
59
    env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
60

    
61
    R1 = env => dirty_s < 2;
62
    R2 = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s));
63
    R3 = env => invalid_s+valid_s+dirty_s = First( init_invalid_s );
64
    OK = R2 and R1 and R3;
65
    --%PROPERTY OK=true;
66
    --%MAIN;
67
tel