CristalCaveGem » LustreC

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

   returns ( ir_out  : real  ) ;

let

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

 tel 

node DynamicSaturation ( up_Out1_148  : real ; u_Out1_158  : real ; lo_Out1_168  : real  ) 

   returns ( y1_In1_210  : real  ) ;

var LowerRelop1_Out1_174  : bool ;

 Switch_Out1_183  : real ;

 Switch2_Out1_192  : real ;

 UpperRelop_Out1_198  : bool ;

 LowerRelop1_In1_172  : real ;

 LowerRelop1_In2_173  : real ;

 Switch_In1_180  : real ;

 Switch_In2_181  : bool ;

 Switch_In3_182  : real ;

 Switch2_In1_189  : real ;

 Switch2_In2_190  : bool ;

 Switch2_In3_191  : real ;

 UpperRelop_In1_196  : real ;

 UpperRelop_In2_197  : real ;

let

LowerRelop1_Out1_174  = LowerRelop1_In1_172 > LowerRelop1_In2_173;

Switch_Out1_183  = if Switch_In2_181 then Switch_In1_180 else Switch_In3_182;

Switch2_Out1_192  = if Switch2_In2_190 then Switch2_In1_189 else Switch2_In3_191;

UpperRelop_Out1_198  = UpperRelop_In1_196 < UpperRelop_In2_197;

Switch2_In1_189  = up_Out1_148;

LowerRelop1_In2_173  = up_Out1_148;

Switch_In3_182  = u_Out1_158;

LowerRelop1_In1_172  = u_Out1_158;

UpperRelop_In1_196  = u_Out1_158;

Switch_In1_180  = lo_Out1_168;

UpperRelop_In2_197  = lo_Out1_168;

Switch2_In3_191  = Switch_Out1_183;

y1_In1_210  = Switch2_Out1_192;

Switch2_In2_190  = LowerRelop1_Out1_174;

Switch_In2_181  = UpperRelop_Out1_198;

 tel 

node VarLimInteg ( Input_Out1_545  : real ; Max_Out1_555  : real ; Min_Out1_565  : real ; ICtrig_Out1_575  : bool ; IC_Out1_585  : real  ) 

   returns ( Out_In1_681  : real  ) ;

var Integrator1_Out1_618  : real ;

 Logical_Operator1_Out1_624  : bool ;

 Logical_Operator2_Out1_630  : bool ;

 Logical_Operator3_Out1_636  : bool ;

 Relational_Operator1_Out1_642  : bool ;

 Relational_Operator2_Out1_648  : bool ;

 Relational_Operator3_Out1_654  : bool ;

 Relational_Operator4_Out1_660  : bool ;

 Switch1_Out1_669  : real ;

 Integrator1_In1_615  : real ;

 Integrator1_In2_616  : bool ;

 Integrator1_In3_617  : real ;

 Logical_Operator1_In1_622  : bool ;

 Logical_Operator1_In2_623  : bool ;

 Logical_Operator2_In1_628  : bool ;

 Logical_Operator2_In2_629  : bool ;

 Logical_Operator3_In1_634  : bool ;

 Logical_Operator3_In2_635  : bool ;

 Relational_Operator1_In1_640  : real ;

 Relational_Operator1_In2_641  : real ;

 Relational_Operator2_In1_646  : real ;

 Relational_Operator2_In2_647  : real ;

 Relational_Operator3_In1_652  : real ;

 -- Relational_Operator3_In2_653  : real ;

 Relational_Operator4_In1_658  : real ;

 -- Relational_Operator4_In2_659  : real ;

 -- Switch1_In1_666  : real ;

 Switch1_In2_667  : bool ;

 Switch1_In3_668  : real ;

let

Integrator1_Out1_618  = Integrator1_In3_617 -> pre integrator_reset ( Integrator1_In1_615 , Integrator1_In2_616 , Integrator1_In3_617  );

Logical_Operator1_Out1_624  = Logical_Operator1_In1_622 or Logical_Operator1_In2_623;

Logical_Operator2_Out1_630  = Logical_Operator2_In1_628 and Logical_Operator2_In2_629;

Logical_Operator3_Out1_636  = Logical_Operator3_In1_634 and Logical_Operator3_In2_635;

Relational_Operator1_Out1_642  = Relational_Operator1_In1_640 <= Relational_Operator1_In2_641;

Relational_Operator2_Out1_648  = Relational_Operator2_In1_646 >= Relational_Operator2_In2_647;

Relational_Operator3_Out1_654  = Relational_Operator3_In1_652 > 0.0;

Relational_Operator4_Out1_660  = Relational_Operator4_In1_658 < 0.0;

Switch1_Out1_669  = if Switch1_In2_667 then 0.0 else Switch1_In3_668;

Integrator1_In3_617  = IC_Out1_585;

Integrator1_In2_616  = ICtrig_Out1_575;

Relational_Operator1_In2_641  = Min_Out1_565;

Relational_Operator2_In2_647  = Max_Out1_555;

-- Relational_Operator4_In2_659  = 0.0;

Switch1_In3_668  = Input_Out1_545;

Relational_Operator3_In1_652  = Input_Out1_545;

Relational_Operator4_In1_658  = Input_Out1_545;

Logical_Operator1_In2_623  = Logical_Operator3_Out1_636;

Logical_Operator3_In2_635  = Relational_Operator4_Out1_660;

Logical_Operator3_In1_634  = Relational_Operator1_Out1_642;

-- Relational_Operator3_In2_653  = 0.0;

Logical_Operator1_In1_622  = Logical_Operator2_Out1_630;

Logical_Operator2_In2_629  = Relational_Operator3_Out1_654;

Logical_Operator2_In1_628  = Relational_Operator2_Out1_648;

Switch1_In2_667  = Logical_Operator1_Out1_624;

Relational_Operator2_In1_646  = Integrator1_Out1_618;

Relational_Operator1_In1_640  = Integrator1_Out1_618;

Out_In1_681  = Integrator1_Out1_618;

Integrator1_In1_615  = Switch1_Out1_669;

-- Switch1_In1_666  = 0.0;

 tel 

node EngageORzero ( engage  : bool ; signal  : real  ) 

   returns ( out : real  ) ;  

let

  out  = if engage then signal else 0.0;

 tel 

node ManualOverride (manual  : real ; auto : real  ) 

   returns ( manual_out  : real  ) ;

var 

  temp  : bool ;

let

  temp  = if manual = 0.000000 then false else true;

  manual_out = if temp then auto else manual;

tel

node AutoThrottle ( ATEng_Out1_19  : bool ; maxThrot_Out1_29  : real ; minThrot_Out1_39  : real ; leverThrot_Out1_49  : real ; Vgdotf_Out1_59  : real ; ICthrot_Out1_69  : real ; Ktas_Cas_Abstracted_Out1_79  : real ; phi_abstracted_Out1_89  : real  ) 

   returns ( ThrotCmd_In1_555  : real  ) ;

var DynamicSaturation_Out1_98  : real ;

 EngageORzero_Out1_189  : real ;

 Kr_Out1_267  : real ;

 Kr1_Out1_276  : real ;

 Logical_Operator_Out1_281  : bool ;

 ManualOverride_Out1_289  : real ;

 Sum1_Out1_345  : real ;

 Sum3_Out1_355  : real ;

 Sum5_Out1_365  : real ;

 VarLimIntegAT_Out1_376  : real ;

 DynamicSaturation_In1_95  : real ;

 DynamicSaturation_In2_96  : real ;

 DynamicSaturation_In3_97  : real ;

 EngageORzero_In1_187  : bool ;

 EngageORzero_In2_188  : real ;

 Kr_In1_266  : real ;

 Kr1_In1_275  : real ;

 Logical_Operator_In1_280  : bool ;

 ManualOverride_In1_287  : real ;

 ManualOverride_In2_288  : real ;

 Sum1_In1_342  : real ;

 Sum1_In2_343  : real ;

 Sum1_In3_344  : real ;

 Sum3_In1_353  : real ;

 Sum3_In2_354  : real ;

 Sum5_In1_363  : real ;

 Sum5_In2_364  : real ;

 VarLimIntegAT_In1_371  : real ;

 VarLimIntegAT_In2_372  : real ;

 VarLimIntegAT_In3_373  : real ;

 VarLimIntegAT_In4_374  : bool ;

 VarLimIntegAT_In5_375  : real ;

let

DynamicSaturation_Out1_98  = DynamicSaturation ( DynamicSaturation_In1_95 , DynamicSaturation_In2_96 , DynamicSaturation_In3_97  );

EngageORzero_Out1_189  = EngageORzero ( EngageORzero_In1_187 , EngageORzero_In2_188  );

Kr_Out1_267  = 2.500000 * Kr_In1_266;

Kr1_Out1_276  = 1.200000 * Kr1_In1_275;

Logical_Operator_Out1_281  = not Logical_Operator_In1_280;

ManualOverride_Out1_289  = ManualOverride ( ManualOverride_In1_287 , ManualOverride_In2_288  );

Sum1_Out1_345  = Sum1_In1_342 + ( Sum1_In2_343 + - Sum1_In3_344  );

Sum3_Out1_355  = Sum3_In1_353 + - Sum3_In2_354;

Sum5_Out1_365  = Sum5_In1_363 + - Sum5_In2_364;

VarLimIntegAT_Out1_376  = VarLimInteg ( VarLimIntegAT_In1_371 , VarLimIntegAT_In2_372 , VarLimIntegAT_In3_373 , VarLimIntegAT_In4_374 , VarLimIntegAT_In5_375  );

Kr_In1_266  = Sum1_Out1_345;

VarLimIntegAT_In1_371  = Kr_Out1_267;

Sum1_In3_344  = Vgdotf_Out1_59;

Kr1_In1_275  = Vgdotf_Out1_59;

Sum3_In2_354  = Kr1_Out1_276;

EngageORzero_In2_188  = Sum5_Out1_365;

VarLimIntegAT_In5_375  = ICthrot_Out1_69;

Sum5_In2_364  = ICthrot_Out1_69;

DynamicSaturation_In1_95  = maxThrot_Out1_29;

VarLimIntegAT_In2_372  = maxThrot_Out1_29;

VarLimIntegAT_In3_373  = minThrot_Out1_39;

DynamicSaturation_In3_97  = minThrot_Out1_39;

Sum3_In1_353  = VarLimIntegAT_Out1_376;

DynamicSaturation_In2_96  = Sum3_Out1_355;

Sum5_In1_363  = DynamicSaturation_Out1_98;

VarLimIntegAT_In4_374  = Logical_Operator_Out1_281;

EngageORzero_In1_187  = ATEng_Out1_19;

Logical_Operator_In1_280  = ATEng_Out1_19;

ManualOverride_In1_287  = leverThrot_Out1_49;

ThrotCmd_In1_555  = ManualOverride_Out1_289;

ManualOverride_In2_288  = EngageORzero_Out1_189;

Sum1_In2_343  = Ktas_Cas_Abstracted_Out1_79;

Sum1_In1_342  = phi_abstracted_Out1_89;

 tel 

node top ( ATEng : bool ; maxThrot : real ; minThrot : real ; leverThrot : real ; Vgdotf : real ;   ICthrot  : real ; Ktas_Cas_Abstracted: real ; Phi_Abstracted : real) 

   returns ( obs: bool) ;

  var ThrotCmd  : real;

let

  -- ICthrot = throt.bias

  -- KTas_Cas_Abstracted // abstracted in the model they talk about the calibrated speed

  ThrotCmd =   AutoThrottle (ATEng , maxThrot, minThrot, leverThrot, Vgdotf,  ICthrot , Ktas_Cas_Abstracted, Phi_Abstracted);

  assert ATEng = true;

  assert leverThrot = 0.0;

  assert maxThrot > (minThrot + 10.0);

  assert minThrot >= 0.0;

  assert maxThrot <= 100.0;

  assert true -> maxThrot = pre(maxThrot);

  assert true -> minThrot = pre(minThrot);

  assert ICthrot = 0.0;

  -- GUIDE 100

  obs =  true -> (Ktas_Cas_Abstracted >= pre (Ktas_Cas_Abstracted)) => (ThrotCmd <= pre(ThrotCmd)) and  (Ktas_Cas_Abstracted <= pre (Ktas_Cas_Abstracted)) => (ThrotCmd <= pre(ThrotCmd)); 

 --!MAIN : true;

--!PROPERTY: obs = true;

tel