Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / PRODUCER_CONSUMER_3.lus @ 22fe1c93

History | View | Annotate | Download (1.51 KB)

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

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

    
11
node Sofar( X : bool ) returns ( Sofar : bool );
12
let
13
    Sofar = X -> X and pre Sofar;
14
tel
15

    
16
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );
17
let
18
    excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 );
19
tel
20

    
21
node PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int
22
) returns(i, b, a, o1, o2 : int);
23
var
24
	garde1, garde2, garde3 : bool;
25
let
26
	garde1 = pre i >= 1;
27
	garde2 = pre b >= 1;
28
	garde3 = pre b >= 1;
29

    
30
	i = a ->
31
	if(etat1) then if(garde1) then pre i -1 else pre i else 
32
	pre i;
33

    
34
	b = 0 -> 
35
	if(etat1) then if(garde1) then pre b+1 else pre b else 
36
	if(etat2) then if(garde2) then pre b-1 else pre b else 
37
	if(garde3) then pre b-1 else pre b;
38

    
39
	a = a_init -> pre a;
40

    
41
	o1 = 0 -> 
42
	if(etat2) then if(garde2) then pre o1+1 else pre o1 else 
43
	pre o1;
44

    
45
	o2 = 0 -> 
46
	if(etat3) then if(garde3) then pre o2+1 else pre o2 else
47
	pre o2;
48

    
49
tel
50

    
51
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
52
    var i, b, a, o1, o2 : int;
53
        env : bool;
54
let
55
   ( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER(etat1, etat2, etat3, a_init );
56
   env = Sofar( excludes3( etat1, etat2, etat3 ) or
57
                not ( etat1 or etat2 or etat3 ) ) and
58
         FirstB( not ( etat1 or etat2 or etat3 ) ) and
59
         First( a_init ) > 0;
60
   OK = env => (true -> pre etat1 and etat2 => (o1 = pre o1+1 or o1 = pre o1));
61
    --%PROPERTY OK=true;
62
    --%MAIN;
63
tel