CristalCaveGem » LustreC

node __sin(x:real) returns (out:real);

let

out = if (0.0<=x and x<=0.15707963267) then 0.0 + (0.99589273524 * (x-0.0)) else 

      if (0.15707963267<=x and x<=0.31415926535) then 0.15643446504 + (0.97137055092 * (x-0.15707963267)) else 

      if (0.31415926535<=x and x<=0.47123889803) then 0.30901699437 + (0.92292999984 * (x-0.31415926535)) else 

      if (0.47123889803<=x and x<=0.62831853071) then 0.45399049974 + (0.85176384914 * (x-0.47123889803)) else 

      if (0.62831853071<=x and x<=0.78539816339) then 0.58778525229 + (0.75962444563 * (x-0.62831853071)) else 

      if (0.78539816339<=x and x<=0.94247779607) then 0.70710678118 + (0.64878056721 * (x-0.78539816339)) else 

      if (0.94247779607<=x and x<=1.09955742876) then 0.80901699437 + (0.52196155806 * (x-0.94247779607)) else 

      if (1.09955742876<=x and x<=1.25663706144) then 0.89100652418 + (0.38229012305 * (x-1.09955742876)) else 

      if (1.25663706144<=x and x<=1.41371669412) then 0.95105651629 + (0.23320543647 * (x-1.25663706144)) else 

      if (1.41371669412<=x and x<=1.57079632679) then 0.98768834059 + (0.07837845807 * (x-1.41371669412)) else -1.0;

tel

node my_sin(x:real) returns (out:real);

let

out = if (0.0<=x and x<=1.57079632679) then __sin(x) else 

      if (1.57079632679<=x and x<=3.14159265359) then __sin(3.14159265359-x) else 

      if (3.14159265359<=x and x<=4.71238898038) then -(__sin(x-3.14159265359)) else 

      if (4.71238898038<=x and x<=6.28318530718) then -(__sin(6.28318530718-x))  else -1.0;

tel

node my_cos(x:real) returns (out:real);

let

out = if (0.0<=x and x<=4.71238898038) then my_sin(1.57079632679+x) else 

      if (4.71238898038<=x and x<=6.28318530718) then my_sin(x-4.71238898038) else -1.0;

tel

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 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 manual else auto;

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 TransferFcn ( x_Out1_753  : real  ) 

   returns ( y_In1_836  : real  ) ;

var asharp1_Out1_762  : real ;

 b0sharp0_Out1_771  : real ;

 b0sharp1_Out1_780  : real ;

 delaysharp1_Out1_785  : real ;

 output_sum_Out1_795  : real ;

 samplesharp1_Out1_804  : real ;

 sum11_Out1_814  : real ;

 sum21_Out1_824  : real ;

 asharp1_In1_761  : real ;

 b0sharp0_In1_770  : real ;

 b0sharp1_In1_779  : real ;

 delaysharp1_In1_784  : real ;

 output_sum_In1_793  : real ;

 output_sum_In2_794  : real ;

 samplesharp1_In1_803  : real ;

 sum11_In1_812  : real ;

 sum11_In2_813  : real ;

 sum21_In1_822  : real ;

 sum21_In2_823  : real ;

let

asharp1_Out1_762  = 0.062500 * asharp1_In1_761;

b0sharp0_Out1_771  = b0sharp0_In1_770;

b0sharp1_Out1_780  = - (b0sharp1_In1_779);

delaysharp1_Out1_785  = 0.000000 -> pre delaysharp1_In1_784;

output_sum_Out1_795  = output_sum_In1_793 + output_sum_In2_794;

samplesharp1_Out1_804  = 0.020000 * samplesharp1_In1_803;

sum11_Out1_814  = sum11_In1_812 + - sum11_In2_813;

sum21_Out1_824  = sum21_In1_822 + sum21_In2_823;

asharp1_In1_761  = delaysharp1_Out1_785;

sum21_In2_823  = delaysharp1_Out1_785;

sum11_In2_813  = asharp1_Out1_762;

b0sharp1_In1_779  = asharp1_Out1_762;

output_sum_In1_793  = b0sharp0_Out1_771;

output_sum_In2_794  = b0sharp1_Out1_780;

samplesharp1_In1_803  = sum11_Out1_814;

sum21_In1_822  = samplesharp1_Out1_804;

delaysharp1_In1_784  = sum21_Out1_824;

sum11_In1_812  = x_Out1_753;

b0sharp0_In1_770  = x_Out1_753;

y_In1_836  = output_sum_Out1_795;

 tel 

node AutoThrottle ( ATEng_Out1_19  : bool ; maxThrot_Out1_29  : real ; minThrot_Out1_39  : real ; leverThrot_Out1_49  : real ; Phidegf_Out1_59  : real ; Ktas_Abstracted_Out1_69  : real ; Cas_ktsf_Out1_79  : real ; Vgdotf_Out1_89  : real ; ICthrot_Out1_99  : real  ) 

   returns ( ThrotCmd_In1_782  : real  ) ;

var Divide_Out1_119  : real ;

 DynamicSaturation_Out1_128  : real ;

 EngageORzero_Out1_219  : real ;

 Gain1_Out1_297  : real ;

 Kcas_Out1_306  : real ;

 Kr_Out1_315  : real ;

 Kr1_Out1_324  : real ;

 Logical_Operator_Out1_329  : bool ;

 ManualOverride_Out1_345  : real ;

 PHIMC1_Out1_399  : real ;

 Sum_Out1_417  : real ;

 Sum1_Out1_428  : real ;

 Sum2_Out1_438  : real ;

 Sum3_Out1_448  : real ;

 Sum5_Out1_458  : real ;

 Trigonometric_Function_Out1_463  : real ;

 VarLimIntegAT_Out1_474  : real ;

 kt2fps_Out1_650  : real ;

 transfer_Fcn_Out1_665  : real ;

 Divide_In1_117  : real ;

 -- Divide_In2_118  : real ;

 DynamicSaturation_In1_125  : real ;

 DynamicSaturation_In2_126  : real ;

 DynamicSaturation_In3_127  : real ;

 EngageORzero_In1_217  : bool ;

 EngageORzero_In2_218  : real ;

 Gain1_In1_296  : real ;

 Kcas_In1_305  : real ;

 Kr_In1_314  : real ;

 Kr1_In1_323  : real ;

 Logical_Operator_In1_328  : bool ;

 ManualOverride_In1_343  : real ;

 ManualOverride_In2_344  : real ;

 PHIMC1_In1_396  : real ;

 PHIMC1_In2_397  : bool ;

 PHIMC1_In3_398  : real ;

 Sum_In1_415  : real ;

 Sum_In2_416  : real ;

 Sum1_In1_425  : real ;

 Sum1_In2_426  : real ;

 Sum1_In3_427  : real ;

 Sum2_In1_436  : real ;

 Sum2_In2_437  : real ;

 Sum3_In1_446  : real ;

 Sum3_In2_447  : real ;

 Sum5_In1_456  : real ;

 Sum5_In2_457  : real ;

 Trigonometric_Function_In1_462  : real ;

 VarLimIntegAT_In1_469  : real ;

 VarLimIntegAT_In2_470  : real ;

 VarLimIntegAT_In3_471  : real ;

 VarLimIntegAT_In4_472  : bool ;

 VarLimIntegAT_In5_473  : real ;

 kt2fps_In1_649  : real ;

 transfer_Fcn_In1_664  : real ;

let

Divide_Out1_119  = Divide_In1_117 / 3.141500;

DynamicSaturation_Out1_128  = DynamicSaturation ( DynamicSaturation_In1_125 , DynamicSaturation_In2_126 , DynamicSaturation_In3_127  );

EngageORzero_Out1_219  = EngageORzero ( EngageORzero_In1_217 , EngageORzero_In2_218  );

Gain1_Out1_297  = 5.0 * Gain1_In1_296;

Kcas_Out1_306  = 0.200000 * Kcas_In1_305;

Kr_Out1_315  = 2.500000 * Kr_In1_314;

Kr1_Out1_324  = 1.200000 * Kr1_In1_323;

Logical_Operator_Out1_329  = not Logical_Operator_In1_328;

ManualOverride_Out1_345  = ManualOverride ( ManualOverride_In1_343 , ManualOverride_In2_344  );

PHIMC1_Out1_399  = if PHIMC1_In2_397 then PHIMC1_In1_396 else PHIMC1_In3_398;

Sum_Out1_417  = Sum_In1_415 + - Sum_In2_416;

Sum1_Out1_428  = Sum1_In1_425 + ( Sum1_In2_426 + - Sum1_In3_427  );

Sum2_Out1_438  = Sum2_In1_436 + - Sum2_In2_437;

Sum3_Out1_448  = Sum3_In1_446 + - Sum3_In2_447;

Sum5_Out1_458  = Sum5_In1_456 + - Sum5_In2_457;

Trigonometric_Function_Out1_463  = my_cos ( Trigonometric_Function_In1_462  );

VarLimIntegAT_Out1_474  = VarLimInteg ( VarLimIntegAT_In1_469 , VarLimIntegAT_In2_470 , VarLimIntegAT_In3_471 , VarLimIntegAT_In4_472 , VarLimIntegAT_In5_473  );

kt2fps_Out1_650  = 1.687800 * kt2fps_In1_649;

transfer_Fcn_Out1_665  = TransferFcn ( transfer_Fcn_In1_664  );

Sum2_In1_436  = 250.0;

kt2fps_In1_649  = Sum2_Out1_438;

Kr_In1_314  = Sum1_Out1_428;

Kcas_In1_305  = kt2fps_Out1_650;

VarLimIntegAT_In1_469  = Kr_Out1_315;

Sum1_In3_427  = Vgdotf_Out1_89;

Kr1_In1_323  = Vgdotf_Out1_89;

Sum3_In2_447  = Kr1_Out1_324;

transfer_Fcn_In1_664  = Gain1_Out1_297;

Gain1_In1_296  = Sum_Out1_417;

Sum_In2_416  = Trigonometric_Function_Out1_463;

Sum_In1_415  = 1.0;

Trigonometric_Function_In1_462  = Divide_Out1_119;

EngageORzero_In2_218  = Sum5_Out1_458;

VarLimIntegAT_In5_473  = ICthrot_Out1_99;

Sum5_In2_457  = ICthrot_Out1_99;

DynamicSaturation_In1_125  = maxThrot_Out1_29;

VarLimIntegAT_In2_470  = maxThrot_Out1_29;

VarLimIntegAT_In3_471  = minThrot_Out1_39;

DynamicSaturation_In3_127  = minThrot_Out1_39;

Sum3_In1_446  = VarLimIntegAT_Out1_474;

DynamicSaturation_In2_126  = Sum3_Out1_448;

Sum5_In1_456  = DynamicSaturation_Out1_128;

Sum1_In2_426  = PHIMC1_Out1_399;

PHIMC1_In3_398  = Kcas_Out1_306;

Sum1_In1_425  = transfer_Fcn_Out1_665;

Divide_In1_117  = Phidegf_Out1_59;

Sum2_In2_437  = Cas_ktsf_Out1_79;

VarLimIntegAT_In4_472  = Logical_Operator_Out1_329;

EngageORzero_In1_217  = ATEng_Out1_19;

Logical_Operator_In1_328  = ATEng_Out1_19;

PHIMC1_In2_397  = if 0 = 0 then false else true;

PHIMC1_In1_396  = Ktas_Abstracted_Out1_69;

ManualOverride_In1_343  = leverThrot_Out1_49;

ThrotCmd_In1_782  = ManualOverride_Out1_345;

ManualOverride_In2_344  = EngageORzero_Out1_219;

 tel 

node top ( ATEng : bool ; maxThrot : real ; minThrot : real ; leverThrot : real ; Phidegf : real ; Ktas_Abstracted: real ;Cas_ktsf : real ; Vgdotf : real ; ICthrot  : real  ) 

   returns (obs: bool) ;

  var ThrotCmd  : real;

let

  -- ICthrot = throt.bias

  ThrotCmd =   AutoThrottle (ATEng , maxThrot, minThrot, leverThrot, Phidegf,  Ktas_Abstracted, Cas_ktsf, Vgdotf, ICthrot);

  assert ATEng = true;

  assert leverThrot = 0.0;

  assert maxThrot > (minThrot + 10.0);

  assert minThrot >= 5.0;

  assert maxThrot <= 100.0;

  assert true -> maxThrot = pre(maxThrot);

  assert true -> minThrot = pre(minThrot);

  assert ICthrot = 0.0;

  obs =  ThrotCmd <= maxThrot and ThrotCmd >= minThrot;

 --!MAIN : true;

 --!PROPERTY: obs = true;

tel