CristalCaveGem » LustreC

node FlipFlop ( S : bool ; R: bool  ) 

   returns ( Q: bool ; notQ  : bool  ) ;

let

notQ = ((not S) or R) -> if (not (S or R)) then pre notQ else R;

Q = not notQ;

 tel

node AutoPilot_AltAndFPAMode ( ActiavteFPA_Out1_123  : real ; Deactivate_Out1_133  : bool ; Altitude_Out1_143  : real ; AltCmd_Out1_153  : real ; ActiavteAlt_Out1_163  : real  ) 

   returns ( AltEng_In1_480  : bool ; FPAEng_In1_492  : bool  ) ;

var Abs_Out1_174  : real ;

 Add_Out1_184  : real ;

 FlipFlop2_Out1_192  : bool ;

 FlipFlop2_Out2_193  : bool ;

 FlipFlop1_Out1_299  : bool ;

 FlipFlop1_Out2_300  : bool ;

 LogicalOperator1_Out1_404  : bool ;

 LogicalOperator2_Out1_409  : bool ;

 LogicalOperator3_Out1_415  : bool ;

 LogicalOperator4_Out1_421  : bool ;

 LogicalOperator5_Out1_427  : bool ;

 LogicalOperator7_Out1_432  : bool ;

 comapare1_Out1_450  : bool ;

 comapare2_Out1_456  : bool ;

 comapare3_Out1_462  : bool ;

 comapare4_Out1_468  : bool ;

 Abs_In1_173  : real ;

 Add_In1_182  : real ;

 Add_In2_183  : real ;

 FlipFlop2_In1_190  : bool ;

 FlipFlop2_In2_191  : bool ;

 FlipFlop1_In1_297  : bool ;

 FlipFlop1_In2_298  : bool ;

 LogicalOperator1_In1_402  : bool ;

 LogicalOperator1_In2_403  : bool ;

 LogicalOperator2_In1_408  : bool ;

 LogicalOperator3_In1_413  : bool ;

 LogicalOperator3_In2_414  : bool ;

 LogicalOperator4_In1_419  : bool ;

 LogicalOperator4_In2_420  : bool ;

 LogicalOperator5_In1_425  : bool ;

 LogicalOperator5_In2_426  : bool ;

 LogicalOperator7_In1_431  : bool ;

 Terminator_In1_434  : bool ;

 Terminator1_In1_436  : bool ;

 comapare1_In1_448  : int ;

 comapare1_In2_449  : int ;

 comapare2_In1_454  : real ;

 comapare2_In2_455  : real ;

 comapare3_In1_460  : real ;

 comapare3_In2_461  : real ;

 comapare4_In1_466  : real ;

 comapare4_In2_467  : real ;

let

Abs_Out1_174  = if Abs_In1_173 < 0.000000 then - Abs_In1_173 else Abs_In1_173;

Add_Out1_184  = Add_In1_182 + - Add_In2_183;

FlipFlop2_Out1_192 , FlipFlop2_Out2_193  = FlipFlop ( FlipFlop2_In1_190 , FlipFlop2_In2_191  );

FlipFlop1_Out1_299 , FlipFlop1_Out2_300  = FlipFlop ( FlipFlop1_In1_297 , FlipFlop1_In2_298  );

LogicalOperator1_Out1_404  = LogicalOperator1_In1_402 or LogicalOperator1_In2_403;

LogicalOperator2_Out1_409  = not LogicalOperator2_In1_408;

LogicalOperator3_Out1_415  = LogicalOperator3_In1_413 and LogicalOperator3_In2_414;

LogicalOperator4_Out1_421  = LogicalOperator4_In1_419 and LogicalOperator4_In2_420;

LogicalOperator5_Out1_427  = LogicalOperator5_In1_425 and LogicalOperator5_In2_426;

LogicalOperator7_Out1_432  = not LogicalOperator7_In1_431;

comapare1_Out1_450  = comapare1_In1_448 <> comapare1_In2_449;

comapare2_Out1_456  = comapare2_In1_454 <> comapare2_In2_455;

comapare3_Out1_462  = comapare3_In1_460 <> comapare3_In2_461;

comapare4_Out1_468  = comapare4_In1_466 <= comapare4_In2_467;

Terminator_In1_434  = FlipFlop2_Out2_193;

comapare2_In1_454  = ActiavteFPA_Out1_123;

LogicalOperator3_In1_413  = FlipFlop2_Out1_192;

LogicalOperator2_In1_408  = FlipFlop2_Out1_192;

comapare1_In1_448  = if Deactivate_Out1_133 then 1 else 0;

FlipFlop2_In1_190  = comapare2_Out1_456;

Terminator1_In1_436  = FlipFlop1_Out2_300;

LogicalOperator5_In1_425  = FlipFlop1_Out1_299;

LogicalOperator4_In1_419  = FlipFlop1_Out1_299;

FlipFlop1_In1_297  = comapare3_Out1_462;

FlipFlop1_In2_298  = comapare1_Out1_450;

FlipFlop2_In2_191  = comapare1_Out1_450;

comapare3_In2_461  = ActiavteAlt_Out1_163;

Add_In1_182  = Altitude_Out1_143;

Add_In2_183  = AltCmd_Out1_153;

Abs_In1_173  = Add_Out1_184;

comapare4_In1_466  = Abs_Out1_174;

FPAEng_In1_492  = LogicalOperator3_Out1_415;

LogicalOperator1_In1_402  = LogicalOperator2_Out1_409;

AltEng_In1_480  = LogicalOperator4_Out1_421;

LogicalOperator5_In2_426  = comapare4_Out1_468;

LogicalOperator1_In2_403  = comapare4_Out1_468;

LogicalOperator4_In2_420  = LogicalOperator1_Out1_404;

LogicalOperator3_In2_414  = LogicalOperator7_Out1_432;

comapare3_In1_460  =  0.0;

comapare1_In2_449  = 0;

comapare2_In2_455  = 0.0;

comapare4_In2_467  = 200.0 ;

LogicalOperator7_In1_431  = LogicalOperator5_Out1_427;

 tel 

node AutoPilot_HeadingMode ( Actiavte_Out1_539  : real ; Deactivate_Out1_549  : bool  ) 

   returns ( HeadEng_In1_690  : bool  ) ;

var SRFlipFlopRepl_Out1_557  : bool ;

 SRFlipFlopRepl_Out2_558  : bool ;

 comapare1_Out1_672  : bool ;

 comapare2_Out1_678  : bool ;

 SRFlipFlopRepl_In1_555  : bool ;

 SRFlipFlopRepl_In2_556  : bool ;

 Terminator_In1_658  : bool ;

 comapare1_In1_670  : real ;

 comapare1_In2_671  : real ;

 comapare2_In1_676  : int ;

 comapare2_In2_677  : int ;

let

SRFlipFlopRepl_Out1_557 , SRFlipFlopRepl_Out2_558  = FlipFlop ( SRFlipFlopRepl_In1_555 , SRFlipFlopRepl_In2_556  );

comapare1_Out1_672  = comapare1_In1_670 <> comapare1_In2_671;

comapare2_Out1_678  = comapare2_In1_676 <> comapare2_In2_677;

Terminator_In1_658  = SRFlipFlopRepl_Out2_558;

comapare1_In1_670  = Actiavte_Out1_539;

HeadEng_In1_690  = SRFlipFlopRepl_Out1_557;

comapare2_In2_677  = if Deactivate_Out1_549 then 1 else 0;

SRFlipFlopRepl_In1_555  = comapare1_Out1_672;

SRFlipFlopRepl_In2_556  = comapare2_Out1_678;

comapare2_In1_676  = 0;

comapare1_In2_671  = 0.0;

 tel 

node AutoPilot_SpeedMode ( Activate_Out1_725  : real ; AltEng_Out1_735  : bool ; CAS_Out1_745  : real ; CASCmdMCP_Out1_755  : real  ) 

   returns ( ATEng_In1_959  : bool ; CASCmd_In1_971  : real  ) ;

var Add_Out1_765  : int ;

 LogicalOperator_Out1_771  : bool ;

 LogicalOperator1_Out1_776  : bool ;

 LogicalOperator2_Out1_782  : bool ;

 SRFlipFlopRepl0_Out1_790  : bool ;

 SRFlipFlopRepl0_Out2_791  : bool ;

 Switch_Out1_898  : real ;

 Switch1_Out1_907  : real ;

 UnitDelay1_Out1_914  : bool ;

 UnitDelay2_Out1_919  : real ;

 comapare1_Out1_941  : bool ;

 comapare2_Out1_947  : bool ;

 Add_In1_763  : int ;

 Add_In2_764  : int ;

 LogicalOperator_In1_769  : bool ;

 LogicalOperator_In2_770  : bool ;

 LogicalOperator1_In1_775  : bool ;

 LogicalOperator2_In1_780  : bool ;

 LogicalOperator2_In2_781  : bool ;

 SRFlipFlopRepl0_In1_788  : bool ;

 SRFlipFlopRepl0_In2_789  : bool ;

 Switch_In1_895  : real ;

 Switch_In2_896  : bool ;

 Switch_In3_897  : real ;

 Switch1_In1_904  : real ;

 Switch1_In2_905  : bool ;

 Switch1_In3_906  : real ;

 Terminator_In1_909  : bool ;

 UnitDelay1_In1_913  : bool ;

 UnitDelay2_In1_918  : real ;

 comapare1_In1_939  : real ;

 comapare1_In2_940  : real ;

 comapare2_In1_945  : int ;

 comapare2_In2_946  : int ;

let

Add_Out1_765  = Add_In1_763 + Add_In2_764;

LogicalOperator_Out1_771  = LogicalOperator_In1_769 and LogicalOperator_In2_770;

LogicalOperator1_Out1_776  = not LogicalOperator1_In1_775;

LogicalOperator2_Out1_782  = LogicalOperator2_In1_780 or LogicalOperator2_In2_781;

SRFlipFlopRepl0_Out1_790 , SRFlipFlopRepl0_Out2_791  = FlipFlop ( SRFlipFlopRepl0_In1_788 , SRFlipFlopRepl0_In2_789  );

Switch_Out1_898  = if Switch_In2_896 then Switch_In1_895 else Switch_In3_897;

Switch1_Out1_907  = if Switch1_In2_905 then Switch1_In1_904 else Switch1_In3_906;

UnitDelay1_Out1_914  = false -> pre UnitDelay1_In1_913;

UnitDelay2_Out1_919  = 0.000000 -> pre UnitDelay2_In1_918;

comapare1_Out1_941  = comapare1_In1_939 <> comapare1_In2_940;

comapare2_Out1_947  = comapare2_In1_945 <> comapare2_In2_946;

Terminator_In1_909  = SRFlipFlopRepl0_Out2_791;

comapare1_In1_939  = Activate_Out1_725;

UnitDelay1_In1_913  = SRFlipFlopRepl0_Out1_790;

ATEng_In1_959  = SRFlipFlopRepl0_Out1_790;

LogicalOperator_In1_769  = AltEng_Out1_735;

LogicalOperator_In2_770  = LogicalOperator1_Out1_776;

SRFlipFlopRepl0_In1_788  = LogicalOperator2_Out1_782;

Add_In2_764  = if LogicalOperator_Out1_771 then 1 else 0;

LogicalOperator2_In2_781  = LogicalOperator_Out1_771;

Switch1_In3_906  = CAS_Out1_745;

Switch1_In1_904  = CASCmdMCP_Out1_755;

Add_In1_763  = if comapare1_Out1_941 then 1 else 0;

LogicalOperator2_In1_780  = comapare1_Out1_941;

Switch1_In2_905  = if Add_Out1_765 = 0 then false else true;

Switch_In2_896  = if Add_Out1_765 = 0 then false else true;

Switch_In3_897  = Switch1_Out1_907;

UnitDelay2_In1_918  = Switch_Out1_898;

Switch_In1_895  = UnitDelay2_Out1_919;

CASCmd_In1_971  = UnitDelay2_Out1_919;

comapare2_In1_945  = 0;

comapare1_In2_940  =  0.0;

LogicalOperator1_In1_775  = UnitDelay1_Out1_914;

comapare2_In2_946  = 0;

SRFlipFlopRepl0_In2_789  = comapare2_Out1_947;

 tel 

--@requires AltMode_Out1_41 = 1.0;

--@ensures ( (((((Altitude_Out1_81 - AltCmd_Out1_71) <= 200.0) and ((Altitude_Out1_81 - AltCmd_Out1_71) >= -200.0)) = true) or (FPAMode_Out1_51 = 0.0)) and (ailStick_Out1_21 = 0.0) and (elevStick_Out1_31 = 0.0)) or (AltEng_In1_1039 = false);

node AutoPilot ( HeadMode_Out1_11  : real ; ailStick_Out1_21  : real ; elevStick_Out1_31  : 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_In1_1027  : bool ; AltEng_In1_1039  : bool ; FPAEng_In1_1051  : bool ; ATEng_In1_1063  : bool ; CASCmd_In1_1075  : real  ) ;

var AltAndFPAMode_Out1_112  : bool ;

 AltAndFPAMode_Out2_113  : bool ;

 HeadingMode_Out1_529  : bool ;

 LogicalOperator_Out1_704  : bool ;

 SpeedMode_Out1_714  : bool ;

 SpeedMode_Out2_715  : real ;

 comapare_Out1_1009  : bool ;

 comapare1_Out1_1015  : bool ;

 AltAndFPAMode_In1_107  : real ;

 AltAndFPAMode_In2_108  : bool ;

 AltAndFPAMode_In3_109  : real ;

 AltAndFPAMode_In4_110  : real ;

 AltAndFPAMode_In5_111  : real ;

 HeadingMode_In1_527  : real ;

 HeadingMode_In2_528  : bool ;

 LogicalOperator_In1_702  : bool ;

 LogicalOperator_In2_703  : bool ;

 SpeedMode_In1_710  : real ;

 SpeedMode_In2_711  : bool ;

 SpeedMode_In3_712  : real ;

 SpeedMode_In4_713  : real ;

 comapare_In1_1007  : real ;

 comapare_In2_1008  : real ;

 comapare1_In1_1013  : real ;

 comapare1_In2_1014  : real ;

let

--!k:2;

AltAndFPAMode_Out1_112 , AltAndFPAMode_Out2_113  = AutoPilot_AltAndFPAMode ( AltAndFPAMode_In1_107 , AltAndFPAMode_In2_108 , AltAndFPAMode_In3_109 , AltAndFPAMode_In4_110 , AltAndFPAMode_In5_111  );

HeadingMode_Out1_529  = AutoPilot_HeadingMode ( HeadingMode_In1_527 , HeadingMode_In2_528  );

LogicalOperator_Out1_704  = LogicalOperator_In1_702 or LogicalOperator_In2_703;

SpeedMode_Out1_714 , SpeedMode_Out2_715  = AutoPilot_SpeedMode ( SpeedMode_In1_710 , SpeedMode_In2_711 , SpeedMode_In3_712 , SpeedMode_In4_713  );

comapare_Out1_1009  = comapare_In1_1007 <> comapare_In2_1008;

comapare1_Out1_1015  = comapare1_In1_1013 <> comapare1_In2_1014;

ATEng_In1_1063  = SpeedMode_Out1_714;

comapare_In2_1008  = ailStick_Out1_21;

SpeedMode_In2_711  = AltAndFPAMode_Out2_113;

FPAEng_In1_1051  = AltAndFPAMode_Out2_113;

AltEng_In1_1039  = AltAndFPAMode_Out1_112;

HeadEng_In1_1027  = HeadingMode_Out1_529;

HeadingMode_In1_527  = HeadMode_Out1_11;

LogicalOperator_In2_703  = comapare1_Out1_1015;

LogicalOperator_In1_702  = comapare_Out1_1009;

comapare1_In2_1014  = elevStick_Out1_31;

SpeedMode_In1_710  = ATMode_Out1_61;

AltAndFPAMode_In1_107  = FPAMode_Out1_51;

AltAndFPAMode_In3_109  = Altitude_Out1_81;

AltAndFPAMode_In5_111  = AltMode_Out1_41;

AltAndFPAMode_In2_108  = LogicalOperator_Out1_704;

HeadingMode_In2_528  = LogicalOperator_Out1_704;

SpeedMode_In4_713  = CASCmdMCP_Out1_101;

AltAndFPAMode_In4_110  = AltCmd_Out1_71;

CASCmd_In1_1075  = SpeedMode_Out2_715;

SpeedMode_In3_712  = CAS_Out1_91;

comapare1_In1_1013  = 0.0;

comapare_In1_1007  = 0.0;

 tel