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 FSMSpec(apfail:bool; limits:bool; standby:bool; supported:bool; ) returns (pullup: bool; );

--Block Path: fsm_12B

let

var FTP:bool = true -> false;

--guarantee "FSM001" S( (((limits and not standby and not apfail and supported) => (pullup)) and FTP), ((limits and not standby and not apfail and supported) => (pullup)) );

guarantee "FSM001V2" limits and not standby and not apfail and supported => pullup;

tel

*)

(*@ contract FSM_AutopilotSpec(apfail:bool; good:bool; prevState:real; standby:bool; supported:bool; ) returns (pullup:bool; state_1:real; );

--Block Path: fsm_12B/FiniteStateMachine/Manager

let

var FTP:bool = true -> false;

--valid

guarantee "FSM002" S( (((standby and prevState = 0.0) => (state_1 = 3.0)) and FTP), ((standby and prevState = 0.0) => (state_1 = 3.0)) );

--guarantee "FSM003" S( (((prevState = 0.0 and good and supported) => (state_1 = 1.0)) and FTP), ((prevState = 0.0 and good and supported) => (state_1 = 1.0)) );

--the reuirement is not correct as they didn't clearly mentionned the pilot is not in control (not standby).

-- the correct version should be 

-- "3.	The autopilot shall change states from TRANSITION to NOMINAL when the pilot is not in control and the system is supported and sensor data is good.

guarantee "FSM003V2" prevState = 0.0 and not standby and good and supported => state_1 = 1.0;

--guarantee "FSM008" S( (((prevState = 3.0 and not standby) => (state_1 = 0.0)) and FTP), ((prevState = 3.0 and not standby) => (state_1 = 0.0)) );

-- the requirement is not correct, they forgot to mention "a failure does not occur (not apfail)" 

guarantee "FSM008V2" prevState = 3.0 and not standby and not apfail => state_1 = 0.0;

--valid

guarantee "FSM009" S( (((prevState = 3.0 and apfail) => (state_1 = 2.0)) and FTP), ((prevState = 3.0 and apfail) => (state_1 = 2.0)) );

--valid

guarantee "FSM005" S( (((prevState = 1.0 and standby) => (state_1 = 3.0)) and FTP), ((prevState = 1.0 and standby) => (state_1 = 3.0)) );

--guarantee "FSM007" S( (((pullup and supported and good) => (state_1 = 0.0)) and FTP), ((pullup and supported and good) => (state_1 = 0.0)) );

-- the formalization is not correct. In the table in definition of pullup: "True when the autopilot is in the MANEUVER state"

-- the requirement is also not correct as it did not mentioned "not standby".

guarantee "FSM007V2" prevState = 2.0 and supported and good and not standby => (state_1 = 0.0) ;

--guarantee "FSM004" S( (((not good and prevState = 1.0) => (state_1 = 2.0)) and FTP), ((not good and prevState = 1.0) => (state_1 = 2.0)) );

-- the requirement is also not correct as it did not mentioned "not standby".

guarantee "FSM004V2" not good and prevState = 1.0 and not standby => state_1 = 2.0;

--valid

guarantee "FSM006" S( (((prevState = 2.0 and standby and good) => (state_1 = 3.0)) and FTP), ((prevState = 2.0 and standby and good) => (state_1 = 3.0)) );

tel

*)

(*@contract FSM_SensorSpec(MODE:bool; limits:bool; prevSensState:real; request:bool; ) returns (sensState: real; );

--Block Path: fsm_12B/FiniteStateMachine/Sen

let

var FTP:bool = true -> false;

--guarantee "FSM011" S( (((prevSensState = 0.0 and not request) => (sensState = 1.0)) and FTP), ((prevSensState = 0.0 and not request) => (sensState = 1.0)) );

-- This requirement is not correct as they did not mention "when limits are not exceeded" which is implicitly implicated from  "FSM010" requirement. 

-- To rewrtie it: "11.	The sensor shall change states from NOMINAL to TRANSITION when the autopilot is not requesting support and limits are not exceeded."

guarantee "FSM011V2" (prevSensState = 0.0 and not request and not limits) => (sensState = 1.0);

--valid

guarantee "FSM012" S( (((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) and FTP), ((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) );

--valid

guarantee "FSM010" S( (((prevSensState = 0.0 and limits) => (sensState = 2.0)) and FTP), ((prevSensState = 0.0 and limits) => (sensState = 2.0)) );

--valid

guarantee "FSM013" S( (((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) and FTP), ((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) );

tel

*)