CristalCaveGem » LustreC

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

   returns ( RollCmd  : real  ) ;

var right : bool;

let

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

  -- 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 ( HdgCmdMCP: real ; Heading : real ; psidot : real ; Vt : real ; Roll : real ; HeadEng : bool ; rollLimitInput : real  ) 

   returns (obs : bool);

  var  RollCmd : real;

let

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

  -- Put properties here

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

  assert (HeadEng = true);

  obs = (HdgCmdMCP = Heading) or ((not (HdgCmdMCP = Heading)) and ((not (Roll = 0)) or (not (RollCmd = 0))));

  --!MAIN : true;

  --!PROPERTY: obs = true;

tel