Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.27 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 PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int
14
) returns(i, b, a, o1, o2 : int);
15
var
16
	garde1, garde2, garde3 : bool;
17
let
18
	garde1 = pre i >= 1;
19
	garde2 = pre b >= 1;
20
	garde3 = pre b >= 1;
21
	i = a ->
22
	if(etat1) then if(garde1) then pre i -1 else pre i else 
23
	pre i;
24
	b = 0 -> 
25
	if(etat1) then if(garde1) then pre b+1 else pre b else 
26
	if(etat2) then if(garde2) then pre b-1 else pre b else 
27
	if(garde3) then pre b-1 else pre b;
28
	a = a_init -> pre a;
29
	o1 = 0 -> 
30
	if(etat2) then if(garde2) then pre o1+1 else pre o1 else 
31
	pre o1;
32
	o2 = 0 -> 
33
	if(etat3) then if(garde3) then pre o2+1 else pre o2 else
34
	pre o2;
35
tel
36
node top( etat1, etat2, etat3 : bool; a_init : int )
37
returns ( OK : bool );
38
    var i, b, a, o1, o2 : int;
39
        env : bool;
40
let
41
    ( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER (etat1, etat2, etat3, a_init );
42
    env = Sofar( excludes3( etat1, etat2, etat3 ) ) and
43
          First( a_init ) > 0;
44
    OK = env => o1+o2 <= a;
45
  --%MAIN;
46
  --%PROPERTY  OK=true;
47
tel