### Profile

 1 ```--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 ``` ```*) ```