Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / memory2 / SYNAPSE_123_e8_953_e8_941.lus @ 2d37a1e1

 1 ```node First( X : int ) returns ( First : int ); ``` ```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 and X1 and X3 and X2 and X3 ); ``` ```tel ``` ```node synapse(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) ``` ```returns(invalid_s, valid_s, dirty_s : int; mem_init_s : int ); ``` ```var ``` ``` garde_s1, garde_s2, garde_s3 : bool; ``` ```let ``` ``` garde_s1 = pre invalid_s>=1; ``` ``` garde_s2 = pre valid_s>=1; ``` ``` garde_s3 = pre invalid_s>=1; ``` ``` mem_init_s = init_invalid_s -> pre mem_init_s; ``` ``` invalid_s = mem_init_s -> ``` ``` if(e_s1) then if(garde_s1) then pre invalid_s + pre dirty_s -1 else pre invalid_s else ``` ``` if(e_s2) then if(garde_s2) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else ``` ``` if(e_s3) then if(garde_s3) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else ``` ``` pre invalid_s; ``` ``` valid_s = 0 -> ``` ``` if(e_s1) then if(garde_s1) then pre valid_s +1 else pre valid_s else ``` ``` if(e_s2) then if(garde_s2) then 0 else pre valid_s else ``` ``` if(e_s3) then if(garde_s3) then 0 else pre valid_s else ``` ``` pre valid_s; ``` ``` dirty_s = 0 -> ``` ``` if(e_s1) then if(garde_s1) then 0 else pre dirty_s else ``` ``` if(e_s2) then if(garde_s2) then 1 else pre dirty_s else ``` ``` if(e_s3) then if(garde_s3) then 1 else pre dirty_s else ``` ``` pre dirty_s; ``` ```tel ``` ```node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) ``` ```returns( OK : bool ); ``` ```--@ contract guarantees OK; ``` ``` var invalid_s, valid_s, dirty_s : int; mem_init_s : int; ``` ``` R1, R2, R3 : bool; ``` ``` env : bool; ``` ```let ``` ``` ( invalid_s, valid_s, dirty_s, mem_init_s ) = ``` ``` synapse(e_s1, e_s2, e_s3, init_invalid_s ); ``` ``` env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 ); ``` ``` R1 = env => dirty_s < 2; ``` ``` R2 = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s)); ``` ``` R3 = env => invalid_s+valid_s+dirty_s = First( init_invalid_s ); ``` ``` --%MAIN; ``` ``` OK = R2 and R1 and R3; ``` ``` --%PROPERTY OK=true; ``` ```tel ```