CristalCaveGem » LustreC » Lustrec-Tests

--Historically

node H(X:bool) returns (Y:bool);

let

    Y = X -> (X and (pre Y));

tel

--Y since inclusive X

node SI(X,Y: bool) returns (Z:bool);

let

Z = Y and (X or (false -> pre Z));

tel

--Y since X

node S(X,Y: bool) returns (Z:bool);

let

Z = X or (Y and (false -> pre Z));

tel

--Once

node O(X:bool) returns (Y:bool);

let

 Y = X or (false -> pre Y);

tel

node First( X : bool ) returns ( Y : bool );

let

  Y = X -> pre Y;

tel

--Timed Once: less than or equal to N

node OTlore(const N: int; X: bool; ) returns (Y: bool);

    var C:int;

let

    C = if X then 0

        else (-1 -> pre C + (if pre C <0 then 0 else 1));

    Y = First(X)

        ->

        (if pre C < 0  then false

         else C <= N

        );

tel

-- Timed Historically: less than or equal to N

node HTlore(const N: int; X: bool) returns (Y: bool);

let

  Y = not OTlore(N, not X);

tel

-- Timed Since: less than or equal to N

node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);

let

  Z = S(X, Y) and OTlore(N, X);

tel

-- Timed Since Inclusive: less than or equal to N

node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);

let

  Z = SI(X,Y) and OTlore(N, X);

tel

(*@ 

contract integrator_12BSpec(BL:real; ic:real; reset:bool; T:real; TL:real; xin:real; ) returns (yout: real; );

--Block Path: integrator_12B

let

var FTP:bool = true -> false;

var xinpv: real = 0.0 -> pre xin;

var ypv: real = 0.0 -> pre yout;

var normal: bool = not reset and yout <= TL and yout >= BL;

var normal_yout : real = T * 0.5 * ( xin + xinpv ) + ypv;

assume BL <=  TL;

--assume T > 0.0;

guarantee "TUI-002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) );

guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));

guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;

--guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));

tel

*)