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_In1_1039  : bool ; FPAEng_In1_1051  : bool ; ATEng_In1_1063  : bool ; CASCmd_In1_1075  : real  ) ;

let

  -- GUIDE-220

  assert (HeadMode = 0.0) or (not (ailStick = 0.0)) or (not (elevStick = 0.0)) or (HeadEng = true);

tel 

node HeadingControl ( HdgCmdMCP  : real ; Heading  : real ; psidot_Out1_39  : real ; Vt_Out1_49  : real ; Roll  : real ; HeadEng  : bool ; rollLimitinput  : real; right : bool  ) 

   returns ( RollCmd  : real  ) ;

let

  -- GUIDE-260

  assert 

    (HeadEng = false) or

    (HdgCmdMCP = Heading) or

    ((right = true)  and ((RollCmd > Roll) or (RollCmd = rollLimitinput))) or

    ((right = false) and ((RollCmd < Roll) or (RollCmd = -rollLimitinput)));

 tel 

node top(HeadMode: real ; ailStick: real ; elevStick : real ; AltMode : real ; FPAMode : real ; ATMode : real ; AltCmd : real ; Altitude  : real ; CAS : real ; CASCmdMCP : real; HdgCmdMCP: real ; Heading : real ; psidot : real ; Vt : real ; Roll : real ; rollLimitInput : real) returns (obs : bool);

var 

    HeadEng  : bool ; 

    AltEng : bool; 

    FPAEng  : bool ; 

    ATEng  : bool ; 

    CASCmd  : real;

    RollCmd : real;

    right : bool;

let

   HeadEng, AltEng, FPAEng, ATEng, CASCmd= AutoPilot ( HeadMode,  ailStick, elevStick,  AltMode, FPAMode, ATMode, AltCmd, Altitude, CAS, CASCmdMCP);

   RollCmd =  HeadingControl ( HdgCmdMCP , Heading , psidot , Vt , Roll , HeadEng , rollLimitInput, right);

   assert (not (HeadMode = 0.0));

   assert (ailStick = 0.0);  

   assert (elevStick = 0.0); 

   assert (Heading >= 0) and (Heading < 360); 

   assert (HdgCmdMCP >= 0) and (HdgCmdMCP < 360); 

   assert (rollLimitInput > 0) and (rollLimitInput <= 30);

   right = ((HdgCmdMCP - Heading > 0) and (HdgCmdMCP - Heading < 180)) or (Heading - HdgCmdMCP > 180);

   obs  =  (HdgCmdMCP = Heading) or

     ((right = true)  and ((RollCmd > Roll) or (RollCmd = rollLimitInput))) or

     ((right = false) and ((RollCmd < Roll) or (RollCmd = -rollLimitInput)));

  --!MAIN : true;

  --!PROPERTY: obs = true;

tel