CristalCaveGem » LustreC

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 );

    var invalid_s, valid_s, dirty_s : int; mem_init_s : int;

        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 );

    OK = env => dirty_s<1 or valid_s<1;

  --%MAIN;

  --%PROPERTY  OK=true;

tel