### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / test / src / kind_fmcad08 / simulation / PRODUCER_CONSUMER_all.lus @ 0cbf0839

1 2 3 0cbf0839 ploc ```node First( X : int ) returns ( First : int ); ``` ```let ``` ``` First = X -> pre First; ``` ```tel ``` ```node FirstB( X : bool ) returns ( First : bool ); ``` ```let ``` ``` First = X -> pre First; ``` ```tel ``` ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 ); ``` ```tel ``` ```node PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int ``` ```) returns(i, b, a, o1, o2 : int); ``` ```var ``` ``` garde1, garde2, garde3 : bool; ``` ```let ``` ``` garde1 = pre i >= 1; ``` ``` garde2 = pre b >= 1; ``` ``` garde3 = pre b >= 1; ``` ``` i = a -> ``` ``` if(etat1) then if(garde1) then pre i -1 else pre i else ``` ``` pre i; ``` ``` b = 0 -> ``` ``` if(etat1) then if(garde1) then pre b+1 else pre b else ``` ``` if(etat2) then if(garde2) then pre b-1 else pre b else ``` ``` if(garde3) then pre b-1 else pre b; ``` ``` a = a_init -> pre a; ``` ``` o1 = 0 -> ``` ``` if(etat2) then if(garde2) then pre o1+1 else pre o1 else ``` ``` pre o1; ``` ``` o2 = 0 -> ``` ``` if(etat3) then if(garde3) then pre o2+1 else pre o2 else ``` ``` pre o2; ``` ```tel ``` ```node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool ); ``` ``` var i, b, a, o1, o2 : int; ``` ``` env : bool; ``` ```let ``` ``` ( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER(etat1, etat2, etat3, a_init ); ``` ``` env = Sofar( excludes3( etat1, etat2, etat3 ) or ``` ``` not ( etat1 or etat2 or etat3 ) ) and ``` ``` FirstB( not ( etat1 or etat2 or etat3 ) ) and ``` ``` First( a_init ) > 0; ``` ``` OK = env => i >= 0 and ``` ``` (true -> pre etat1 and etat2 => ``` ``` (o1 = pre o1+1 or o1 = pre o1)); ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` `tel`