test.lus

type FGS__Guidance_Commands__Guidance_Commands_Impl = struct {Pitch_Delta : real; Pitch_Valid : bool};
type FGS__Lateral_Modes__Lateral_Modes_Impl = struct {HDG_active : bool; ROLL_active : bool};
type FGS__Flight_Modes__Flight_Modes_Impl = struct {active : bool; lat : FGS__Lateral_Modes__Lateral_Modes_Impl; ver : int};
type FGS__Guidance_Data__Guidance_Data_Impl = struct {cmds : FGS__Guidance_Commands__Guidance_Commands_Impl; mds : FGS__Flight_Modes__Flight_Modes_Impl};
type LDS__Leader_Selection_Data__Leader_Selection_Data_Impl = struct {Leader : int; Valid : bool};
type APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl = struct {CSA_Pitch_Delta : real; CSA_Pitch_Valid : bool};
type ADS__Airspeed__Airspeed_Impl = struct {Val : real; Valid : bool};
type ADS__Pitch__Pitch_Impl = struct {Val : real; Valid : bool};
type ADS__Air_Data__Air_Data_Impl = struct {AirSpeed : ADS__Airspeed__Airspeed_Impl; Pitch : ADS__Pitch__Pitch_Impl};

node FCS__Flight_Control_System__abs(
  Flight_Control_System_Flight_Control_System_Impl_Instance__x : real
) returns (
  _outvar : real
);
let
  _outvar = (if (Flight_Control_System_Flight_Control_System_Impl_Instance__x > 0.0) then Flight_Control_System_Flight_Control_System_Impl_Instance__x else (-Flight_Control_System_Flight_Control_System_Impl_Instance__x));

tel;

node __NODE_AP(
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_L : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_R : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl
) returns (
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta : real;
  __GUAR_AP_0 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta_correct : bool
);
var
  ___kind2_record_access_workaround_0 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_1 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_2 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_3 : FGS__Guidance_Commands__Guidance_Commands_Impl;
let
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta = (if ___kind2_record_access_workaround_0.active then ___kind2_record_access_workaround_1.Pitch_Delta else (if ___kind2_record_access_workaround_2.active then ___kind2_record_access_workaround_3.Pitch_Delta else (0.0 -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta))));

  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta_correct = (((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta > 0.0) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA.CSA_Pitch_Delta > 0.0) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA.CSA_Pitch_Delta <= Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta))) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta <= 0.0) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA.CSA_Pitch_Delta <= 0.0) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA.CSA_Pitch_Delta >= Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta))));

  __GUAR_AP_0 = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta_correct;

  ___kind2_record_access_workaround_0 = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L.mds;

  ___kind2_record_access_workaround_1 = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L.cmds;

  ___kind2_record_access_workaround_2 = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R.mds;

  ___kind2_record_access_workaround_3 = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R.cmds;

tel;

node FGS__Flight_Guidance_System__abs(
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__x : real
) returns (
  _outvar : real
);
let
  _outvar = (if (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__x > 0.0) then Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__x else (-Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__x));

tel;

node __NODE_FGS_L(
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__NAV : bool
) returns (
  __GUAR_FGS_L_0 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__gc_ok : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__leader_implies_active : bool;
  __GUAR_FGS_L_3 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control : bool;
  __GUAR_FGS_L_2 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__active_implies_valid : bool;
  __GUAR_FGS_L_1 : bool;
  __GUAR_FGS_L_4 : bool
);
var
  ___kind2_record_access_workaround_4 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_5 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_6 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_7 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_8 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_9 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_10 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_11 : FGS__Guidance_Commands__Guidance_Commands_Impl;
let
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control = ___kind2_record_access_workaround_4.active;

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__active_implies_valid = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control => Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__leader_implies_active = ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = 1) => ___kind2_record_access_workaround_5.active);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__gc_ok = ((true -> (FGS__Flight_Guidance_System__abs((___kind2_record_access_workaround_6.Pitch_Delta - (0.0 -> (pre ___kind2_record_access_workaround_7.Pitch_Delta)))) < 1.0)) and (FGS__Flight_Guidance_System__abs(___kind2_record_access_workaround_8.Pitch_Delta) < 5.0));

  __GUAR_FGS_L_0 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__active_implies_valid;

  __GUAR_FGS_L_1 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__leader_implies_active;

  __GUAR_FGS_L_2 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid = ___kind2_record_access_workaround_9.Valid);

  __GUAR_FGS_L_3 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control => Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__gc_ok);

  __GUAR_FGS_L_4 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control => (___kind2_record_access_workaround_10.Val = ___kind2_record_access_workaround_11.Pitch_Delta));

  ___kind2_record_access_workaround_4 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.mds;

  ___kind2_record_access_workaround_5 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.mds;

  ___kind2_record_access_workaround_6 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.cmds;

  ___kind2_record_access_workaround_7 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.cmds;

  ___kind2_record_access_workaround_8 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.cmds;

  ___kind2_record_access_workaround_9 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD.Pitch;

  ___kind2_record_access_workaround_10 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD.Pitch;

  ___kind2_record_access_workaround_11 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC.cmds;

tel;

node __NODE_FGS_R(
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl
) returns (
  __GUAR_FGS_R_1 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__leader_implies_active : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__active_implies_valid : bool;
  __GUAR_FGS_R_3 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__gc_ok : bool;
  __GUAR_FGS_R_4 : bool;
  __GUAR_FGS_R_0 : bool;
  __GUAR_FGS_R_2 : bool
);
var
  ___kind2_record_access_workaround_12 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_13 : FGS__Flight_Modes__Flight_Modes_Impl;
  ___kind2_record_access_workaround_14 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_15 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_16 : FGS__Guidance_Commands__Guidance_Commands_Impl;
  ___kind2_record_access_workaround_17 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_18 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_19 : FGS__Guidance_Commands__Guidance_Commands_Impl;
let
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control = ___kind2_record_access_workaround_12.active;

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__active_implies_valid = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control => Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__leader_implies_active = ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader = 2) => ___kind2_record_access_workaround_13.active);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__gc_ok = ((true -> (FGS__Flight_Guidance_System__abs((___kind2_record_access_workaround_14.Pitch_Delta - (0.0 -> (pre ___kind2_record_access_workaround_15.Pitch_Delta)))) < 1.0)) and (FGS__Flight_Guidance_System__abs(___kind2_record_access_workaround_16.Pitch_Delta) < 5.0));

  __GUAR_FGS_R_0 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__active_implies_valid;

  __GUAR_FGS_R_1 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__leader_implies_active;

  __GUAR_FGS_R_2 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid = ___kind2_record_access_workaround_17.Valid);

  __GUAR_FGS_R_3 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control => Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__gc_ok);

  __GUAR_FGS_R_4 = (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control => (___kind2_record_access_workaround_18.Val = ___kind2_record_access_workaround_19.Pitch_Delta));

  ___kind2_record_access_workaround_12 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.mds;

  ___kind2_record_access_workaround_13 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.mds;

  ___kind2_record_access_workaround_14 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.cmds;

  ___kind2_record_access_workaround_15 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.cmds;

  ___kind2_record_access_workaround_16 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.cmds;

  ___kind2_record_access_workaround_17 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD.Pitch;

  ___kind2_record_access_workaround_18 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD.Pitch;

  ___kind2_record_access_workaround_19 = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC.cmds;

tel;

node _MAIN(
  __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FCI : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__FCI : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FCI__THROT_R : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_L : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_R : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__THROT_L : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__THROT_R : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FCI__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FCI__YOKE_R : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FCI__YOKE_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R : bool;
  __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSI : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__YOKE_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FCI : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L : bool;
  __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R : ADS__Air_Data__Air_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__YOKE_R : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R : bool;
  ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__NAV : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FCI__THROT_L : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD : ADS__Air_Data__Air_Data_Impl
) returns (

);
var
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__leader_implies_active : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__gc_ok : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__gc_ok : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__active_implies_valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__leader_implies_active : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__right_side_valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__prop2 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO : LDS__Leader_Selection_Data__Leader_Selection_Data_Impl;
  __GUAR_FGS_R_2 : bool;
  __GUAR_FGS_R_3 : bool;
  __GUAR_FGS_R_4 : bool;
  __GUAR_FGS_L_4 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  __GUAR_FGS_R_0 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__active_implies_valid : bool;
  __GUAR_FGS_R_1 : bool;
  __GUAR_FGS_L_0 : bool;
  __GUAR_FGS_L_1 : bool;
  __GUAR_FGS_L_2 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta_correct : bool;
  __GUAR_FGS_L_3 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta : real;
  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC : FGS__Guidance_Data__Guidance_Data_Impl;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  __GUAR_AP_0 : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid : bool;
  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA : APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl;
  _TOTAL_COMP_HIST : bool;
  _SYSTEM_ASSUMP_HIST : bool;
  __CONSIST_COUNTER : int;
  _Hist_AP : bool;
  _Hist_FGS_L : bool;
  _Hist_FGS_R : bool;
  _CONTR_HIST_AP : bool;
  _NULL_CONTR_HIST_AP : bool;
  _CONTR_HIST_FGS_L : bool;
  _NULL_CONTR_HIST_FGS_L : bool;
  _CONTR_HIST_FGS_R : bool;
  _NULL_CONTR_HIST_FGS_R : bool;
  _SYS_GUARANTEE_0 : bool;
  _SYS_GUARANTEE_1 : bool;
  _TOTAL_COMP_FINITE_CONSIST : bool;
  _THIS_CONTRACT_CONSIST : bool;
  _THIS_CONTRACT_HIST : bool;
  ___kind2_record_access_workaround_20 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_21 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_22 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_23 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_24 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_25 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_26 : ADS__Pitch__Pitch_Impl;
  ___kind2_record_access_workaround_27 : ADS__Pitch__Pitch_Impl;
let
  --%MAIN
  Flight_Control_System_Flight_Control_System_Impl_Instance__prop2 = ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = 1)))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = 1)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 = ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader = 2)))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader = 2)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid = (true -> (FCS__Flight_Control_System__abs((___kind2_record_access_workaround_20.Val - (0.0 -> (pre ___kind2_record_access_workaround_21.Val)))) < 1.0));

  Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid = (true -> (FCS__Flight_Control_System__abs((___kind2_record_access_workaround_22.Val - (0.0 -> (pre ___kind2_record_access_workaround_23.Val)))) < 1.0));

  Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok = (FCS__Flight_Control_System__abs((___kind2_record_access_workaround_24.Val - ___kind2_record_access_workaround_25.Val)) < 2.0);

  Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid = ___kind2_record_access_workaround_26.Valid;

  Flight_Control_System_Flight_Control_System_Impl_Instance__right_side_valid = ___kind2_record_access_workaround_27.Valid;

  Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid = (Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid or Flight_Control_System_Flight_Control_System_Impl_Instance__right_side_valid);

  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta, __GUAR_AP_0, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__leader_pitch_delta_correct = condact(__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP, __NODE_AP(Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_L, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__GC_R, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R, Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA), 0.0, true, true);

  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__AP__APP__CSA)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)));

  __GUAR_FGS_L_0, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__gc_ok, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__leader_implies_active, __GUAR_FGS_L_3, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__this_side_in_control, __GUAR_FGS_L_2, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__active_implies_valid, __GUAR_FGS_L_1, __GUAR_FGS_L_4 = condact(__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L, __NODE_FGS_L(Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AD, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__FCI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__AH, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FCI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__VNAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__NAV), true, true, true, true, true, true, true, true, true);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__LSO)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__FGP__GC)));

  __GUAR_FGS_R_1, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__leader_implies_active, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__active_implies_valid, __GUAR_FGS_R_3, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__this_side_in_control, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__gc_ok, __GUAR_FGS_R_4, __GUAR_FGS_R_0, __GUAR_FGS_R_2 = condact(__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R, __NODE_FGS_R(Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AH, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__AD, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__FCI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FCI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__VNAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSI, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__NAV, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH, Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO), true, true, true, true, true, true, true, true, true);

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__LSO)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__FGP__GC)));

  Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO = (if __CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R then ___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO else (___DUMMY_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)));

  _TOTAL_COMP_HIST = (((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2)))) -> (((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2)))) and (pre _TOTAL_COMP_HIST)));

  _SYSTEM_ASSUMP_HIST = ((((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2))) -> ((((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2))) and (pre _SYSTEM_ASSUMP_HIST)));

  __CONSIST_COUNTER = (0 -> ((pre __CONSIST_COUNTER) + 1));

  _Hist_AP = ((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (_SYSTEM_ASSUMP_HIST and (true -> (pre ((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2)))))))) => (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => true));

  _Hist_FGS_L = ((true and (_SYSTEM_ASSUMP_HIST and (true -> (pre ((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2)))))))) => (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => true));

  _Hist_FGS_R = ((true and (_SYSTEM_ASSUMP_HIST and (true -> (pre ((((true and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4)))) and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4)))) and (((Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((((((((((((((((((((Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC) and (Flight_Control_System_Flight_Control_System_Impl_Instance__AP__GC_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__CSA = Flight_Control_System_Flight_Control_System_Impl_Instance__AP__CSA)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_L)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_L = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSI = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AH = Flight_Control_System_Flight_Control_System_Impl_Instance__AH_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__VNAV = Flight_Control_System_Flight_Control_System_Impl_Instance__FM_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__NAV = Flight_Control_System_Flight_Control_System_Impl_Instance__NAV_R)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FD_R = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__GC)) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__AD = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader = Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <> 1)))) and ((false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <> 2)))) and ((false -> (pre (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid or Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid))) => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L__LSO.Leader <= 2))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Valid => ((Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader >= 1) and (Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R__LSO.Leader <= 2)))))) and (Flight_Control_System_Flight_Control_System_Impl_Instance__prop1 and Flight_Control_System_Flight_Control_System_Impl_Instance__prop2)))))))) => (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => true));

  _NULL_CONTR_HIST_AP = (not (_CONTR_HIST_AP and (__CONSIST_COUNTER = 5)));

  _CONTR_HIST_AP = ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0)) -> ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP => ((true and true) and __GUAR_AP_0)) and (pre _CONTR_HIST_AP)));

  _NULL_CONTR_HIST_FGS_L = (not (_CONTR_HIST_FGS_L and (__CONSIST_COUNTER = 5)));

  _CONTR_HIST_FGS_L = ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4))) -> ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L => ((true and true) and ((((__GUAR_FGS_L_0 and __GUAR_FGS_L_1) and __GUAR_FGS_L_2) and __GUAR_FGS_L_3) and __GUAR_FGS_L_4))) and (pre _CONTR_HIST_FGS_L)));

  _NULL_CONTR_HIST_FGS_R = (not (_CONTR_HIST_FGS_R and (__CONSIST_COUNTER = 5)));

  _CONTR_HIST_FGS_R = ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4))) -> ((__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R => ((true and true) and ((((__GUAR_FGS_R_0 and __GUAR_FGS_R_1) and __GUAR_FGS_R_2) and __GUAR_FGS_R_3) and __GUAR_FGS_R_4))) and (pre _CONTR_HIST_FGS_R)));

  _SYS_GUARANTEE_0 = ((_SYSTEM_ASSUMP_HIST and _TOTAL_COMP_HIST) => (true -> (FCS__Flight_Control_System__abs(Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta) < 5.0)));

  _SYS_GUARANTEE_1 = ((_SYSTEM_ASSUMP_HIST and _TOTAL_COMP_HIST) => (true -> (FCS__Flight_Control_System__abs((Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta - (0.0 -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta)))) < 5.0)));

  _TOTAL_COMP_FINITE_CONSIST = (not (_TOTAL_COMP_HIST and (__CONSIST_COUNTER = 5)));

  _THIS_CONTRACT_HIST = (((((true and Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid) and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((true and (true -> (FCS__Flight_Control_System__abs(Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta) < 5.0))) and (true -> (FCS__Flight_Control_System__abs((Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta - (0.0 -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta)))) < 5.0)))) -> (((((true and Flight_Control_System_Flight_Control_System_Impl_Instance__some_side_valid) and (((false -> (pre (false -> (pre (not Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))))) and (false -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid))) => Flight_Control_System_Flight_Control_System_Impl_Instance__left_side_valid)) and ((Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L_Pitch_Step_Delta_Valid and Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R_Pitch_Step_Delta_Valid) and Flight_Control_System_Flight_Control_System_Impl_Instance__pitch_lr_ok)) and ((true and (true -> (FCS__Flight_Control_System__abs(Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta) < 5.0))) and (true -> (FCS__Flight_Control_System__abs((Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta - (0.0 -> (pre Flight_Control_System_Flight_Control_System_Impl_Instance__CSA.CSA_Pitch_Delta)))) < 5.0)))) and (pre _THIS_CONTRACT_HIST)));

  _THIS_CONTRACT_CONSIST = (not (_THIS_CONTRACT_HIST and (__CONSIST_COUNTER = 5)));

  ___kind2_record_access_workaround_20 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L.Pitch;

  ___kind2_record_access_workaround_21 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L.Pitch;

  ___kind2_record_access_workaround_22 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R.Pitch;

  ___kind2_record_access_workaround_23 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R.Pitch;

  ___kind2_record_access_workaround_24 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L.Pitch;

  ___kind2_record_access_workaround_25 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R.Pitch;

  ___kind2_record_access_workaround_26 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_L.Pitch;

  ___kind2_record_access_workaround_27 = Flight_Control_System_Flight_Control_System_Impl_Instance__AD_R.Pitch;

  assert (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L and (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP and true)));

  assert (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_R or (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__FGS_L or (__CLOCK_Flight_Control_System_Flight_Control_System_Impl_Instance__AP or false)));

  assert true;

  assert true;

  --%PROPERTY _SYS_GUARANTEE_0;
  --%PROPERTY _SYS_GUARANTEE_1;

tel;