### 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 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 RegulatorSpec() ``` ```returns (lcvdt_cmd_fcs_dps2 : real; ``` ``` mcvdt_cmd_fcs_dps2 : real; ``` ``` ncvdt_cmd_fcs_dps2 : real; ``` ``` xcvdt_cmd_fcs_fps2: real; ``` ``` hcvdt_cmd_fcs_fps2: real;); ``` ```-- Block path: regs_12B_PP (why do we have _PP?) ``` ```let ``` ```var FTP:bool = true -> false; ``` ```var airspeed_command_acceleration: real = (xcvdt_cmd_fcs_fps2 - (0.0 -> pre xcvdt_cmd_fcs_fps2)) /0.01; ``` ```var count_airspeed_output_exceeding_32: int = 0 -> if (xcvdt_cmd_fcs_fps2 > 32.0) then pre count_airspeed_output_exceeding_32 + 1 else 0; ``` ```var count_height_output_exceeding_32: int = 0 -> if (hcvdt_cmd_fcs_fps2 > 32.0) then pre count_height_output_exceeding_32 + 1 else 0; ``` ```var count_pitch_output_exceeding_50: int = 0 -> if (mcvdt_cmd_fcs_dps2 > 50.0) then pre count_pitch_output_exceeding_50 + 1 else 0; ``` ```var count_roll_output_exceeding_50: int = 0 -> if (lcvdt_cmd_fcs_dps2 > 50.0) then pre count_roll_output_exceeding_50 + 1 else 0; ``` ```var count_yaw_output_exceeding_50: int = 0 -> if (ncvdt_cmd_fcs_dps2 > 50.0) then pre count_yaw_output_exceeding_50 + 1 else 0; ``` ```var height_command_acceleration: real = 0.0 -> (hcvdt_cmd_fcs_fps2 - pre hcvdt_cmd_fcs_fps2) /0.01; ``` ```var pitch_command_acceleration: real = 0.0 -> (mcvdt_cmd_fcs_dps2 - pre mcvdt_cmd_fcs_dps2) /0.01; ``` ```var roll_command_acceleration: real = 0.0 -> (lcvdt_cmd_fcs_dps2 - pre lcvdt_cmd_fcs_dps2) /0.01; ``` ```var yaw_command_acceleration: real = 0.0 -> (ncvdt_cmd_fcs_dps2 - pre ncvdt_cmd_fcs_dps2) /0.01; ``` ```-- Regulator shall always satisfy count_airspeed_output_exceeding_32 <= 100 ``` ``` guarantee "REG004" S( ((count_airspeed_output_exceeding_32 <= 100) and FTP), (count_airspeed_output_exceeding_32 <= 100) ); ``` ```-- Regulator shall always satisfy count_roll_output_exceeding_50 <= 100 ``` ``` guarantee "REG001" S( ((count_roll_output_exceeding_50 <= 100) and FTP), (count_roll_output_exceeding_50 <= 100) ); ``` ``` guarantee count_roll_output_exceeding_50 <= 100; ``` ```-- Regulator shall always satisfy roll_command_acceleration <= 50.0 ``` ``` guarantee "REG006" S( ((roll_command_acceleration <= 50.0) and FTP), (roll_command_acceleration <= 50.0) ); ``` ```-- Regulator shall always satisfy count_height_output_exceeding_32 <= 100 ``` ``` guarantee "REG005" S( ((count_height_output_exceeding_32 <= 100) and FTP), (count_height_output_exceeding_32 <= 100) ); ``` ```-- Regulator shall always satisfy pitch_command_acceleration <= 50.0 ``` ``` guarantee "REG007" S( ((pitch_command_acceleration <= 50.0) and FTP), (pitch_command_acceleration <= 50.0) ); ``` ```-- Regulator shall always satisfy yaw_command_acceleration <= 50.0 ``` ``` guarantee "REG008" S( ((yaw_command_acceleration <= 50.0) and FTP), (yaw_command_acceleration <= 50.0) ); ``` ```-- Regulator shall always satisfy airspeed_command_acceleration <=32.0 ``` ``` guarantee "REG009" S( ((airspeed_command_acceleration <= 32.0) and FTP), (airspeed_command_acceleration <= 32.0) ); ``` ```-- Regulator shall always satisfy height_command_acceleration <= 32.0 ``` ``` guarantee "REG010" S( ((height_command_acceleration <= 32.0) and FTP), (height_command_acceleration <= 32.0) ); ``` ```-- Regulator shall always satisfy count_pitch_output_exceeding_50 <= 100 ``` ``` guarantee "REG002" S( ((count_pitch_output_exceeding_50 <= 100) and FTP), (count_pitch_output_exceeding_50 <= 100) ); ``` ``` -- Regulator shall always satisfy count_yaw_output_exceeding_50 <= 100 ``` ``` guarantee "REG003" S( ((count_yaw_output_exceeding_50 <= 100) and FTP), (count_yaw_output_exceeding_50 <= 100) ); ``` ```tel ```