Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory1 / FIREFLY_luke_1a_e2_284_e7_998.lus @ 22fe1c93

History | View | Annotate | Download (3.55 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X or pre Sofar;
5
tel
6
node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool );
7
let
8
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
9
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
10
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
11
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
12
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 or
13
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 or
14
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 or
15
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 or
16
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8;
17
tel
18
node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 
19
	returns(invalid, dirty, exclusive, shared : int);
20
var
21
	garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool;
22
	mem_invalid : int;
23
let
24
	mem_invalid = i_invalid -> pre mem_invalid;
25
	garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ;
26
	garde2 = pre invalid>=1 and pre dirty>=1;
27
	garde3 = pre invalid>=1 and pre shared+pre exclusive>=1;
28
	garde4 = pre exclusive>=1;
29
	garde5 = pre shared=1;
30
	garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0;
31
	garde7 = pre invalid>=1 and pre dirty>=1;
32
	garde8 = pre invalid>=1 and pre shared+pre exclusive>=1;
33
	invalid = mem_invalid ->
34
	if(e1) then if(garde1) then pre invalid-1 else pre invalid else
35
	if(e2) then if(garde2) then pre invalid-1 else pre invalid else
36
	if(e3) then if(garde3) then pre invalid-1 else pre invalid else
37
	if(e6) then if(garde6) then pre invalid-1 else pre invalid else
38
	if(e7) then if(garde7) then pre invalid-1 else pre invalid else
39
	if(e8) then if(garde8) then pre invalid-1 else pre invalid else
40
	pre invalid;
41
	dirty = 0 -> 
42
	if(e2) then if(garde2) then pre dirty-1 else pre dirty else
43
	if(e4) then if(garde4) then pre dirty+1 else pre dirty else
44
	if(e6) then if(garde6) then 1 else pre dirty else
45
	if(e7) then if(garde7) then pre dirty-1 else pre dirty else
46
	pre dirty;
47
	exclusive = 0 -> 
48
	if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else
49
	if(e3) then if(garde3) then 0 else pre exclusive else 
50
	if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else
51
	if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else
52
	if(e8) then if(garde8) then 0 else pre exclusive else
53
	pre exclusive;
54
	shared = 0 ->
55
	if(e2) then if(garde2) then pre shared+2 else pre shared else
56
	if(e3) then if(garde3) then pre shared -1+ pre exclusive + 1 else pre shared else
57
	if(e5) then if(garde5) then pre 0 else pre shared else
58
	if(e7) then if(garde7) then pre shared+2 else pre shared else
59
	if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else
60
	pre shared;
61
tel
62
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 
63
	returns( OK : bool );
64
    var invalid, dirty, exclusive, shared : int;
65
        env : bool;
66
let
67
    ( invalid, dirty, exclusive, shared ) =
68
        firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid );
69
    env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and
70
                 i_invalid >= 0 );
71
    OK = env => exclusive < 2;
72
  --%MAIN;
73
  --%PROPERTY  OK=true;
74
tel