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 ; adiff : bool ) 

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

let

  -- GUIDE-180

  assert (adiff = true) or (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);

  -- GUIDE-120

  assert ( ((adiff = true) or (FPAMode_Out1_51 = 0.0)) and (ailStick = 0.0) and (elevStick = 0.0)) or (AltEng = false);

  assert (adiff = false) or (AltMode_Out1_41 = 0.0) or (not (ailStick = 0.0)) or (not (elevStick = 0.0)) or ((FPAEng_In1_1051 = false) and (AltEng = true));

tel 

node AltitudeControl ( AltEng  : bool ; AltCmd_Out1_29  : real ; Alt_Out1_39  : real ; GsKts_Out1_49  : real ; hdot_Out1_59  : real ; hdotChgRate_Out1_69  : real ;   preAltGammaCmd : real; count : int ) 

   returns ( altgammacmd_In1_661  : real ) ;  

let

  -- ALT-2

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

  -- GUIDE-200

  assert true -> (count < 2) or (AltEng = false) or ((AltCmd_Out1_29 = Alt_Out1_39) or 

     ((AltCmd_Out1_29 > Alt_Out1_39) and ( (altgammacmd_In1_661 > pre(preAltGammaCmd)) or (altgammacmd_In1_661 > 0) )) or 

     ((AltCmd_Out1_29 < Alt_Out1_39) and ( (altgammacmd_In1_661 < pre(preAltGammaCmd)) or (altgammacmd_In1_661 < 0) )) );

tel 

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

   returns ( PitchCmd_In1_487  : real) ;  

let

  -- GUIDE-120

  assert true -> (engage = false) or  (count < 2) 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 ; 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;

    preAltGammaCmd : real;

    count : int;

    guide200 : bool;

    guide120 : bool;

    adiff : bool;

 let

  HeadEng, AltEng, FPAEng, ATEng, CasCmd = AutoPilot(HeadMode, ailStick, elevStick, AltMode, FPAMode, ATMode_Out1_61, AltCmd, Altitude, CAS_Out1_91, CASCmdMCP_Out1_101, adiff);

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

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

  assert fpain = (altgammaCmd + gamcmd_Out1_25);

  prePitch = 3.0 -> pre(PitchCmd);

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

  preAltGammaCmd = 0.0 -> pre(altgammaCmd);

  adiff = (Altitude - AltCmd <= 200) and (Altitude - AltCmd >= -200);

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

  assert (not (AltMode = 0.0));

  assert (not (FPAMode = 0.0));

  assert (elevStick = 0.0);

  assert (ailStick = 0.0);

  assert true -> AltCmd = pre (AltCmd);

  assert AltCmd > 3000 ;

  assert true -> (Altitude = pre(Altitude) + pre (hdot));

  assert (-40.0 < hdot) and (hdot < 40.0);  

  assert (-100.0 > Altitude - AltCmd) or (100.0 < Altitude - AltCmd);

  assert (hdot_change_rate = 3.2);

  assert (AltCmd > Altitude +  300) -> true;

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

  guide120 = true -> (count < 2) or (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)));

  guide200 = true -> (count < 2) or ((AltCmd = Altitude) or 

    ((AltCmd > Altitude) and ( (altgammaCmd > pre(preAltGammaCmd)) or (altgammaCmd > 0) )) or 

    ((AltCmd < Altitude) and ( (altgammaCmd < pre(preAltGammaCmd)) or (altgammaCmd < 0) )) );

  obs = ((adiff = true) and (guide200 = true)) or ((adiff = false) and (guide120 = true));

 --!MAIN : true;

--!PROPERTY: obs = true;

tel