Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.28 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 PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int
12
) returns(i, b, a, o1, o2 : int);
13
var
14
	garde1, garde2, garde3 : bool;
15
let
16
	garde1 = pre i >= 1;
17
	garde2 = pre b >= 1;
18
	garde3 = pre b >= 1;
19

    
20
	i = a ->
21
	if(etat1) then if(garde1) then pre i -1 else pre i else 
22
	pre i;
23

    
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

    
29
	a = a_init -> pre a;
30

    
31
	o1 = 0 -> 
32
	if(etat2) then if(garde2) then pre o1+1 else pre o1 else 
33
	pre o1;
34

    
35
	o2 = 0 -> 
36
	if(etat3) then if(garde3) then pre o2+1 else pre o2 else
37
	pre o2;
38

    
39
tel
40

    
41
-- Not provable with luke-bitvec
42
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );
43
    var i, b, a, o1, o2 : int;
44
        env : bool;
45
let
46
   ( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER(etat1, etat2, etat3, a_init );
47
   env = Sofar( not (etat2 and etat3) and o1 <= 32767 and o2 <= 32767 ) and
48
         ( not etat1 -> true ) and
49
         First( a_init ) > 0 and First( a_init ) < 10;
50
   OK = env => o1 >= 0;
51
   --OK = env => o2 >= 0;
52

    
53
   --%PROPERTY OK=true;
54
   --%MAIN;
55
   
56
tel