CristalCaveGem » LustreC

node integrator_reset ( Fx  : real ; ResetLevel  : bool ; x0  : real  ) 

   returns ( out  : real  ) ;

let

  out  = x0 -> if ( ResetLevel  ) then x0 else ( Fx * 1.000000  ) + pre ( out  );

tel 

node ANGL ( in_Out1_76  : real  ) 

   returns ( _180_In1_238  : real  ) ;

var Abs_Out1_79  : real ;

 Relational_Operator_ANGL_Out1_101  : bool ;

 Sum6_Out1_111  : real ;

 Switch1_ANGL_Out1_120  : real ;

 -- sign_Out1_127  : real ;

 times360_Out1_226  : real ;

 Abs_In1_78  : real ;

 Relational_Operator_ANGL_In1_99  : real ;

 Sum6_In1_109  : real ;

 Sum6_In2_110  : real ;

 Switch1_ANGL_In1_117  : real ;

 Switch1_ANGL_In2_118  : bool ;

 Switch1_ANGL_In3_119  : real ;

 sign_In1_126  : real ;

let

Abs_Out1_79  = if Abs_In1_78 < 0.000000 then - Abs_In1_78 else Abs_In1_78;

Relational_Operator_ANGL_Out1_101  = Relational_Operator_ANGL_In1_99 > 180.0;

Sum6_Out1_111  = - Sum6_In1_109 + Sum6_In2_110;

Switch1_ANGL_Out1_120  = if Switch1_ANGL_In2_118 then Switch1_ANGL_In1_117 else Switch1_ANGL_In3_119;

-- sign_Out1_127  = ANGL_sign ( sign_In1_126  );

-- times360_Out1_226  = 360.0 *  sign_Out1_127;

times360_Out1_226  = if (sign_In1_126 >= 0.0) then 360.0 else -360.0;

Relational_Operator_ANGL_In1_99  = Abs_Out1_79;

Abs_In1_78  = in_Out1_76;

Switch1_ANGL_In3_119  = in_Out1_76;

Sum6_In2_110  = in_Out1_76;

sign_In1_126  = in_Out1_76;

_180_In1_238  = Switch1_ANGL_Out1_120;

Sum6_In1_109  = times360_Out1_226;

Switch1_ANGL_In1_117  = Sum6_Out1_111;

Switch1_ANGL_In2_118  = Relational_Operator_ANGL_Out1_101;

tel 

node DynamicSaturation ( up_Out1_293  : real ; u_Out1_303  : real ; lo_Out1_313  : real  ) 

   returns ( y1_In1_355  : real  ) ;

   var low_lim  : real ;

let

  y1_In1_355 = if (low_lim <= up_Out1_293) then low_lim else up_Out1_293;

  low_lim = if (lo_Out1_313 >= u_Out1_303) then lo_Out1_313 else u_Out1_303;  

 tel 

node HgdCmdProcessor ( Vt_Out1_19  : real ; HdgCmdMCP_Out1_29  : real ; Heading_Out1_39  : real  ) 

   returns ( HdgCmd_In1_947  : real ; HdgRteCmd_In1_959  : real ; 

   Integrator1 : real ; DynamicSat : real ) ;

var 

 var2zetaOmega_Out1_59  : real ;

 ANGL_Out1_66  : real ;

 DynamicSaturation_Out1_283  : real ;

 Integrator1_Out1_380  : real ;

 Logical_Operator_Out1_385  : bool ;

 Sum2_Out1_489  : real ;

 Sum3_Out1_499  : real ;

 k_Out1_723  : real ;

 k1_Out1_732  : real ;

 omegaSq2_Out1_783  : real ;

 omega_calc_Out1_790  : real ;

 rateLim_calc_Out1_875  : real ;

 times514dot8_Out1_890  : real ;

 Integrator1_1_Out1_598  : real ;

 Logical_Operator1_1_Out1_604  : bool ;

 Logical_Operator1_2_Out1_610  : bool ;

 Logical_Operator1_3_Out1_616  : bool ;

 Relational_Operator_Out1_622  : bool ;

 Relational_Operator1_Out1_628  : bool ;

 Relational_Operator2_Out1_634  : bool ;

 Relational_Operator3_Out1_640  : bool ;

 Switch1_Out1_649  : real ;

 Switch2_Out1_658  : real ;

 Switch3_Out1_667  : real ;

 var2zetaOmega_In1_57  : real ;

 ANGL_In1_65  : real ;

 DynamicSaturation_In1_280  : real ;

 DynamicSaturation_In2_281  : real ;

 DynamicSaturation_In3_282  : real ;

 Integrator1_In1_377  : real ;

 Integrator1_In2_378  : bool ;

 Integrator1_In3_379  : real ;

 Logical_Operator_In1_384  : bool ;

 Sum2_In1_487  : real ;

 Sum2_In2_488  : real ;

 Sum3_In1_497  : real ;

 Sum3_In2_498  : real ;

 k_In1_722  : real ;

 k1_In1_731  : real ;

 omegaSq2_In2_782  : real ;

 Integrator1_1_In1_595  : real ;

 Integrator1_1_In2_596  : bool ;

 -- Integrator1_1_In3_597  : real ;

 Logical_Operator1_1_In1_602  : bool ;

 Logical_Operator1_1_In2_603  : bool ;

 Logical_Operator1_2_In1_608  : bool ;

 Logical_Operator1_2_In2_609  : bool ;

 Logical_Operator1_3_In1_614  : bool ;

 Logical_Operator1_3_In2_615  : bool ;

 Relational_Operator_In1_620  : real ;

 Relational_Operator_In2_621  : real ;

 Relational_Operator1_In1_626  : real ;

 Relational_Operator1_In2_627  : real ;

 Relational_Operator2_In1_632  : real ;

 -- Relational_Operator2_In2_633  : real ;

 Relational_Operator3_In1_638  : real ;

 -- Relational_Operator3_In2_639  : real ;

 Switch1_In1_646  : real ;

 Switch1_In2_647  : bool ;

 Switch1_In3_648  : real ;

 Switch2_In1_655  : real ;

 Switch2_In2_656  : bool ;

 Switch2_In3_657  : real ;

 Switch3_In2_665  : bool ;

 Switch3_In3_666  : real ;

let

 var2zetaOmega_Out1_59  = var2zetaOmega_In1_57 * -3.2;

-- I 'sliced' the model (we would need to add simpler versions

-- for the other cases to be complete)

-- ANGL_Out1_66  = ANGL ( ANGL_In1_65  );

ANGL_Out1_66  = ANGL_In1_65;

DynamicSaturation_Out1_283  = DynamicSaturation ( DynamicSaturation_In1_280 , DynamicSaturation_In2_281 , DynamicSaturation_In3_282  );

DynamicSat = ANGL_Out1_66;

Integrator1_Out1_380  = integrator_reset( Integrator1_In1_377 , Integrator1_In2_378 , Integrator1_In3_379);

Logical_Operator_Out1_385  = not Logical_Operator_In1_384;

Sum2_Out1_489  = Sum2_In1_487 + - Sum2_In2_488;

Sum3_Out1_499  = Sum3_In1_497 + - Sum3_In2_498;

k_Out1_723  = - 1.000000 * k_In1_722;

k1_Out1_732  = - 1.000000 * k1_In1_731;

omegaSq2_Out1_783  = 2.56 * omegaSq2_In2_782;

omega_calc_Out1_790  = - 1.6;

-- FALK: fix the constant between 90 and 600.

-- this is the output of ratelim. 

rateLim_calc_Out1_875  = 300.0 * Vt_Out1_19;

-- times block (548 / (Vt * 1.6))

times514dot8_Out1_890  = 305.0 * Vt_Out1_19 ;

Integrator1_1_Out1_598  = integrator_reset ( Integrator1_1_In1_595 , Integrator1_1_In2_596 , 0.000000);

Logical_Operator1_1_Out1_604  = Logical_Operator1_1_In1_602 and Logical_Operator1_1_In2_603;

Logical_Operator1_2_Out1_610  = Logical_Operator1_2_In1_608 and Logical_Operator1_2_In2_609;

Logical_Operator1_3_Out1_616  = Logical_Operator1_3_In1_614 or Logical_Operator1_3_In2_615;

Relational_Operator_Out1_622  = Relational_Operator_In1_620 <= Relational_Operator_In2_621;

Relational_Operator1_Out1_628  = Relational_Operator1_In1_626 >= Relational_Operator1_In2_627;

Relational_Operator2_Out1_634  = Relational_Operator2_In1_632 > 0.000000;

Relational_Operator3_Out1_640  = Relational_Operator3_In1_638 < 0.000000;

Switch1_Out1_649  = if Switch1_In2_647 then Switch1_In1_646 else Switch1_In3_648;

Switch2_Out1_658  = if Switch2_In2_656 then Switch2_In1_655 else Switch2_In3_657;

Switch3_Out1_667  = if Switch3_In2_665 then 0.000000 else Switch3_In3_666;

Sum2_In2_488  = Integrator1_Out1_380;

HdgCmd_In1_947  = Integrator1_Out1_380;

DynamicSaturation_In3_282  = k_Out1_723;

DynamicSaturation_In2_281  = Sum3_Out1_499;

k1_In1_731  = rateLim_calc_Out1_875;

var2zetaOmega_In1_57  = Switch2_Out1_658;

HdgRteCmd_In1_959  = Switch2_Out1_658;

Integrator1_In1_377  = Switch2_Out1_658;

Sum3_In2_498  = var2zetaOmega_Out1_59;

DynamicSaturation_In1_280  = times514dot8_Out1_890;

k_In1_722  = times514dot8_Out1_890;

Sum3_In1_497  = omegaSq2_Out1_783;

ANGL_In1_65  = Sum2_Out1_489;

Logical_Operator_In1_384  = if HdgCmdMCP_Out1_29 = 0.000000 then false else true;

Sum2_In1_487  = HdgCmdMCP_Out1_29;

omegaSq2_In2_782  = ANGL_Out1_66;

Integrator1_In2_378  = Logical_Operator_Out1_385;

Integrator1_In3_379  = Heading_Out1_39;

Relational_Operator1_In1_626  = k1_Out1_732;

Switch2_In1_655  = k1_Out1_732;

Integrator1_1_In2_596  = Logical_Operator_Out1_385;

Switch3_In3_666  = DynamicSaturation_Out1_283;

Relational_Operator3_In1_638  = DynamicSaturation_Out1_283;

Relational_Operator2_In1_632  = DynamicSaturation_Out1_283;

Relational_Operator_In1_620  = rateLim_calc_Out1_875;

Switch1_In1_646  = rateLim_calc_Out1_875;

Logical_Operator1_2_In2_609  = Relational_Operator1_Out1_628;

Switch2_In2_656  = Relational_Operator1_Out1_628;

Switch2_In3_657  = Switch1_Out1_649;

Relational_Operator1_In2_627  = Switch1_Out1_649;

Logical_Operator1_2_In1_608  = Relational_Operator3_Out1_640;

Logical_Operator1_3_In2_615  = Logical_Operator1_2_Out1_610;

Logical_Operator1_3_In1_614  = Logical_Operator1_1_Out1_604;

Switch3_In2_665  = Logical_Operator1_3_Out1_616;

Logical_Operator1_1_In2_603  = Relational_Operator2_Out1_634;

Integrator1_1_In1_595  = Switch3_Out1_667;

Logical_Operator1_1_In1_602  = Relational_Operator_Out1_622;

Switch1_In2_647  = Relational_Operator_Out1_622;

Relational_Operator_In2_621  = Integrator1_1_Out1_598;

Switch1_In3_648  = Integrator1_1_Out1_598;

Integrator1 = Integrator1_1_Out1_598;

 tel 

node top ( Vt : real ; HdgCmdMCP  : real ; Heading  : real)

returns (obs : bool);

  var  HdgCmd  : real ; 

  HdgRteCmd  : real;

  preCmd : real;

  prePreCmd : real;

  prePrePreCmd : real;

  count : int;

  integ : real;

  preInteg : real;

  dsat : real;

let

  HdgCmd, HdgRteCmd, integ, dsat =  HgdCmdProcessor ( Vt, HdgCmdMCP , Heading);

  assert (Vt >= 0.005) and (Vt <= 0.01);

  assert true -> Vt = pre(Vt);

  assert (HdgCmdMCP > 10.0) and (HdgCmdMCP < 170.0);

  assert (Heading > 0.0) and (Heading < 180.0);

  assert Heading = 20.0;

  assert HdgCmdMCP = 30.0;

  assert true -> (HdgCmdMCP = pre(HdgCmdMCP));

  assert (HdgCmdMCP >= Heading + 10);

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

  preCmd = 0.0 -> pre(HdgCmd);

  prePreCmd = 0.0 -> pre(preCmd);

  prePrePreCmd = 0.0 -> pre(prePreCmd);  

  preInteg = 0.0 -> pre(integ);

  -- TIMEOUT

  -- obs = true -> (count < 5) or

  --  (((not (HdgCmdMCP > prePrePreCmd and prePrePreCmd > prePreCmd  )) or ((HdgRteCmd > pre(HdgRteCmd)) or (HdgRteCmd > 0.0)) ) 

  --  and ((not (HdgCmdMCP < prePrePreCmd and prePrePreCmd < prePreCmd )) or ((HdgRteCmd < pre(HdgRteCmd)) or (HdgRteCmd < 0.0)) ));

  -- TIMEOUT

  -- obs = true -> (count < 5) or ((HdgCmdMCP - HdgCmd < 10.0) and (HdgCmdMCP - HdgCmd > -10.0));

  -- TIMEOUT

  -- obs = true -> (count < 5) or

  --  (((not (HdgCmdMCP > prePrePreCmd and prePrePreCmd > prePreCmd  )) or ((integ > pre(integ)) or (integ > 0.0)) ) and 

  --  ((not (HdgCmdMCP < prePrePreCmd and prePrePreCmd < prePreCmd )) or ((integ < pre(integ)) or (integ < 0.0)) ));

  -- TIMEOUT

  -- obs = ((not (HdgRteCmd < 1.0)) and (HdgRteCmd > -1.0)) and

   -- ((HdgCmdMCP = Heading) or

   -- ((HdgCmdMCP > Heading) and (HdgCmd > Heading)) or

   -- ((HdgCmdMCP < Heading) and (HdgCmd < Heading))); 

  obs = true -> (count < 2) or

    ((HdgCmdMCP > preCmd) and (dsat > 0.0)) or 

    ((HdgCmdMCP < preCmd) and (dsat < 0.01)); 

  --!MAIN : true;

  --!PROPERTY: obs = true;

tel