CristalCaveGem » LustreC

node AutoPilot ( HeadMode  : real ; ailStick  : real ; elevStick  : real ; AltMode_Out1_41  : real ; FPAMode_Out1_51  : real ; ATMode_Out1_61  : real ; AltCmd_Out1_71  : real ; Altitude_Out1_81  : real ; CAS_Out1_91  : real ; CASCmdMCP_Out1_101  : real  ) 

   returns ( HeadEng  : bool ; AltEng  : bool ; FPAEng_In1_1051  : bool ; ATEng_In1_1063  : bool ; CASCmd_In1_1075  : real  ) ;

let

  -- GUIDE-180

  assert (FPAMode_Out1_51 = 0.0) or (not (ailStick = 0.0)) or (not (elevStick = 0.0)) or (FPAEng_In1_1051 = true);

  -- ALT-1

  assert (not (AltMode_Out1_41 = 0.0)) or (AltEng = false);

tel 

node AltitudeControl ( AntEng  : bool ; AltCmd_Out1_29  : real ; Alt_Out1_39  : real ; GsKts_Out1_49  : real ; hdot_Out1_59  : real ; hdotChgRate_Out1_69  : real  ) 

   returns ( altgammacmd_In1_661  : real  ) ;  

let

  -- ALT-2

  assert (AntEng = true) or (altgammacmd_In1_661 = 0.0);

tel 

node FPAControl ( engage  : bool ; gamcmd_Out1_25  : real ; gamma_Out1_35  : real ; thetadeg_Out1_45  : real ; VT_Out1_55  : real  ) 

   returns ( PitchCmd_In1_487  : real ; prePitch : real) ;  

let

  assert true -> (engage = false) or (gamcmd_Out1_25 =  gamma_Out1_35) 

             or ((gamcmd_Out1_25 > gamma_Out1_35) and  (PitchCmd_In1_487 >  pre(prePitch)))

             or  ((gamcmd_Out1_25 < gamma_Out1_35) and  (PitchCmd_In1_487 < pre(prePitch)));

 tel 

node top (HeadMode  : real ; ailStick  : real ; elevStick  : real ; AltMode  : real ; FPAMode  : real ; ATMode_Out1_61  : real ; AltCmd_Out1_71  : real ; Altitude_Out1_81  : real ; CAS_Out1_91  : real ; CASCmdMCP_Out1_101  : real ; AltCmd : real ; Altitude : real ; gskts  : real ; hdot  : real;  hdot_change_rate  : real ; gamcmd_Out1_25  : real ; gamma_Out1_35  : real ; thetadeg_Out1_45  : real ; VT_Out1_55  : real ) 

   returns ( obs: bool) ;

  var 

    altgammaCmd  : real;

    fpain : real;

    tempAlt : real;

    tempFPA : real;

    HeadEng : bool;

    AltEng : bool;

    FPAEng : bool;

    ATEng : bool;

    CasCmd : real;

    PitchCmd : real;

    prePitch : real;

let

  HeadEng, AltEng, FPAEng, ATEng, CasCmd = AutoPilot(HeadMode, ailStick, elevStick, AltMode, FPAMode, ATMode_Out1_61, AltCmd_Out1_71, Altitude_Out1_81, CAS_Out1_91, CASCmdMCP_Out1_101);

  altgammaCmd =  AltitudeControl (AltEng, AltCmd,  Altitude, gskts, hdot, hdot_change_rate );

  -- FIXME: if we write this as code and not as assertion, the property cannot be proven, why??

  assert fpain = (altgammaCmd + gamcmd_Out1_25);

  PitchCmd, prePitch = FPAControl(FPAEng ,fpain ,gamma_Out1_35 , thetadeg_Out1_45, VT_Out1_55);

  assert (AltMode = 0.0);

  assert (not (FPAMode = 0.0));

  assert (elevStick = 0.0);

  assert (ailStick = 0.0);

  assert (gamcmd_Out1_25 < -1.0 and gamcmd_Out1_25 > -10.0);

  obs = true -> (gamcmd_Out1_25 =  gamma_Out1_35) 

             or ((gamcmd_Out1_25 > gamma_Out1_35) and  (PitchCmd >  pre(prePitch)))

             or  ((gamcmd_Out1_25 < gamma_Out1_35) and  (PitchCmd < pre(prePitch)));

 --!MAIN : true;

--!PROPERTY: obs = true;

tel