CristalCaveGem » LustreC » Lustrec-Tests

--@ ensures OK;

node top(onOff: bool; 

      decelSet: bool; 

      accelResume: bool; 

      cancel: bool; 

      brakePedal: bool; 

      carGear: int; 

      carSpeed: real; 

      validInputs: bool)

   returns (OK:bool);

var

mode: int; 

      cruiseThrottle: real; 

      desiredSpeed: real;

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock: bool; 

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_init_step: bool; 

   newDesiredSpeed1: real; 

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock: bool; 

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_init_step: bool; 

   newDesiredSpeed: real; 

   chart_CruiseController_ModeLogic_mode_logic_onOff: int; 

   chart_CruiseController_ModeLogic_mode_logic_decel: int; 

   chart_CruiseController_ModeLogic_mode_logic_set: int; 

   chart_CruiseController_ModeLogic_mode_logic_accel: int; 

   chart_CruiseController_ModeLogic_mode_logic_safetyCondition: int; 

   chart_CruiseController_ModeLogic_mode_logic____wakeup___: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_outports_setDesiredSpeed: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_setDesiredSpeed: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_2: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_3: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_15_states___root: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_02: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_02: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_01: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_01: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_0: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_4_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_2: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_3: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_8_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_outports_setDesiredSpeed: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_outports_mode: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rltCheckEntryStateConsistency_0: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_complete_1: bool; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_outports_mode: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root: int; 

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_outports_mode: int; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_rltCheckEntryStateConsistency_0: bool; 

   rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root: int; 

   chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep: bool; 

   chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root: int; 

   chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode: int; 

   chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed: int; 

   chart_CruiseController_ModeLogic_mode_logic_final_state_states___root: int; 

   chart_CruiseController_ModeLogic_mode_logic_setDesiredSpeed: int; 

   cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out: int; 

   cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out: int; 

   cruise_controller_CruiseController_ModeLogic_resumeEvent_Out: bool; 

   cruise_controller_CruiseController_ModeLogic_safetyCondition_safetyCondition: bool; 

   cruise_controller_CruiseController_ModeLogic_setEvent_Out: bool; 

   cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed: bool; 

   cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed: real; 

   cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed: real; 

   cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta: real;

let 

   cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out = (

      (if (

         (if (0 >= 

            (if accelResume

               then 1

               else 0))

            then 0

            else 

         (if accelResume

            then 1

            else 0)) <= 20)

         then 

               (if (0 >= 

                  (if accelResume

                     then 1

                     else 0))

                  then 0

                  else 

               (if accelResume

                  then 1

                  else 0))

         else 20) -> 

      (if (

         (if (0 >= 

            (if accelResume

               then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out) + 1)

               else 0))

            then 0

            else 

         (if accelResume

            then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out) + 1)

            else 0)) <= 20)

         then 

               (if (0 >= 

                  (if accelResume

                     then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out) + 1)

                     else 0))

                  then 0

                  else 

               (if accelResume

                  then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out) + 1)

                  else 0))

         else 20));

   cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out = (

      (if (

         (if (0 >= 

            (if decelSet

               then 1

               else 0))

            then 0

            else 

         (if decelSet

            then 1

            else 0)) <= 20)

         then 

               (if (0 >= 

                  (if decelSet

                     then 1

                     else 0))

                  then 0

                  else 

               (if decelSet

                  then 1

                  else 0))

         else 20) -> 

      (if (

         (if (0 >= 

            (if decelSet

               then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out) + 1)

               else 0))

            then 0

            else 

         (if decelSet

            then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out) + 1)

            else 0)) <= 20)

         then 

               (if (0 >= 

                  (if decelSet

                     then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out) + 1)

                     else 0))

                  then 0

                  else 

               (if decelSet

                  then ((pre cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out) + 1)

                  else 0))

         else 20));

   chart_CruiseController_ModeLogic_mode_logic_onOff = 

      (if (onOff = false)

         then 0

         else 1);

   chart_CruiseController_ModeLogic_mode_logic_decel = 

      (if (

         (if (cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out = 20)

            then true

            else false) = false)

         then 0

         else 1);

   chart_CruiseController_ModeLogic_mode_logic_set = 

      (if (cruise_controller_CruiseController_ModeLogic_setEvent_Out = false)

         then 0

         else 1);

   chart_CruiseController_ModeLogic_mode_logic_accel = 

      (if (

         (if (cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out = 20)

            then true

            else false) = false)

         then 0

         else 1);

   chart_CruiseController_ModeLogic_mode_logic_safetyCondition = 

      (if (cruise_controller_CruiseController_ModeLogic_safetyCondition_safetyCondition = false)

         then 0

         else 1);

   chart_CruiseController_ModeLogic_mode_logic____wakeup___ = true;

   chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep = (true -> 

      (if (pre chart_CruiseController_ModeLogic_mode_logic____wakeup___)

         then false

         else (pre chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep)));

   chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root = (0 -> (pre chart_CruiseController_ModeLogic_mode_logic_final_state_states___root));

   chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode = (0 -> (pre mode));

   chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed = (0 -> (pre chart_CruiseController_ModeLogic_mode_logic_setDesiredSpeed));

   chart_CruiseController_ModeLogic_mode_logic_final_state_states___root = 

      (if chart_CruiseController_ModeLogic_mode_logic____wakeup___

         then 

               (if chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep

                  then rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root

                  else 

               (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_complete_1) and 

                  ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 2) and 

                  (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 8)))

                  then 

                        (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_3) and 

                           ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root >= 3) and 

                           (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root <= 6)))

                           then rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_15_states___root

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root))

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root);

   mode = 

      (if chart_CruiseController_ModeLogic_mode_logic____wakeup___

         then 

               (if chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep

                  then 

                        (if (not (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root = 1))

                           then 1

                           else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode)

                  else 

               (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_complete_1) and 

                  ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 2) and 

                  (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 8)))

                  then 

                        (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_3) and 

                           ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root >= 3) and 

                           (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root <= 6)))

                           then 

                                 (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4

                                    then 

                                          (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root = 4))

                                             then 4

                                             else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_outports_mode)

                                    else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_outports_mode)

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_outports_mode)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_outports_mode))

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode);

   chart_CruiseController_ModeLogic_mode_logic_setDesiredSpeed = 

      (if chart_CruiseController_ModeLogic_mode_logic____wakeup___

         then 

               (if chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep

                  then chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed

                  else 

               (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_complete_1) and 

                  ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 2) and 

                  (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 8)))

                  then 

                        (if ((not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_3) and 

                           ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root >= 3) and 

                           (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root <= 6)))

                           then 

                                 (if ((not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4 or 

                                    rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_3)) and 

                                    (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_15_states___root = 4))

                                    then 0

                                    else 

                                 (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2

                                    then 

                                          (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root = 4)

                                             then 0

                                             else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_setDesiredSpeed)

                                    else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_setDesiredSpeed))

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_outports_setDesiredSpeed)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed))

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0 = (

      ((chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root >= 2) and 

      (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root <= 8)) and 

      (not 

      (if (chart_CruiseController_ModeLogic_mode_logic_onOff <> 0)

         then true

         else false)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0

         then 

               (if 

                  ((chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root >= 2) and 

                  (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root <= 8))

                  then 

                        0

                  else chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root)

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root = 1))

                  then 

                        1

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0

         then 

               (if 

                  ((chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root >= 2) and 

                  (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root <= 8))

                  then 

                        (if 

                           ((chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root >= 3) and 

                           (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root <= 6))

                           then 

                                 (if (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root = 4)

                                    then 0

                                    else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed)

                           else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed)

                  else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed)

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_setDesiredSpeed);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root = 1) and 

      (

      (if (chart_CruiseController_ModeLogic_mode_logic_onOff <> 0)

         then true

         else false) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_complete_1 = (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root = 1)

                  then 

                        0

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_1_states___root = 1))

                  then 1

                  else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode)

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1

         then rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_fired_1

         then 

               (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

                  then 

                        (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 7))

                           then 2

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_outports_mode)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0 = (

      ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 3) and 

      (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 6)) and 

      (not 

      (if (chart_CruiseController_ModeLogic_mode_logic_safetyCondition <> 0)

         then true

         else false)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

         then 

               (if 

                  ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 3) and 

                  (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 6))

                  then 

                        2

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 8))

                  then 

                        8

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root = 8) and 

      ((

      (if (

         (if ((chart_CruiseController_ModeLogic_mode_logic_set = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false) and 

      (if (

         (if ((chart_CruiseController_ModeLogic_mode_logic_safetyCondition = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false)) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_1 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root = 8)

                  then 

                        2

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_2_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_4_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 8))

                  then 3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1

         then rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root = 8) and 

      ((

      (if (

         (if ((

            (if (cruise_controller_CruiseController_ModeLogic_resumeEvent_Out = false)

               then 0

               else 1) = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false) and 

      (if (

         (if ((chart_CruiseController_ModeLogic_mode_logic_safetyCondition = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false)) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_1)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_2 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_1);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root = 8)

                  then 

                        2

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_5_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1

         then 

               (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

                  then 

                        (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root = 4))

                           then 4

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_4_outports_mode)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_4_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_4_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2

         then rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root = 7) and 

      ((

      (if (

         (if ((chart_CruiseController_ModeLogic_mode_logic_set = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false) and 

      (if (

         (if ((chart_CruiseController_ModeLogic_mode_logic_safetyCondition = 1) = false)

            then 0

            else 1) <> 0)

         then true

         else false)) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_2)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_3 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_complete_2);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_8_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_2

         then 

               (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_01

                  then 

                        (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1 = 4))

                           then 4

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_outports_mode)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root = 7)

                  then 

                        2

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_7_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_outports_setDesiredSpeed = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3

         then 1

         else 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_1

         then 1

         else 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

         then 

               (if 

                  ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root >= 3) and 

                  (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root <= 6))

                  then 

                        (if (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_4_states___root = 4)

                           then 0

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_2_outports_setDesiredSpeed)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3

         then rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_fired_3

         then 

               (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_02

                  then 

                        (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2 = 4))

                           then 4

                           else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_8_outports_mode)

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_8_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_8_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root = 4) and 

      (chart_CruiseController_ModeLogic_mode_logic_set = 1));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root = 4)

                  then 

                        3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_outports_setDesiredSpeed = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

         then 1

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_outports_setDesiredSpeed);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root = 4))

                  then 

                        4

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 4) and 

      ((chart_CruiseController_ModeLogic_mode_logic_accel = 1) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_1 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 4)

                  then 

                        3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_states___root = 4))

                  then 4

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_10_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_setDesiredSpeed = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 4)

                  then 0

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_outports_setDesiredSpeed)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_2_outports_setDesiredSpeed);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root = 5))

                  then 

                        5

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root = 4) and 

      ((chart_CruiseController_ModeLogic_mode_logic_decel = 1) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_1)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_2 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_1);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root = 4)

                  then 

                        3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_5_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_1

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_states___root = 5))

                  then 6

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_4_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root = 6))

                  then 

                        6

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root = 6) and 

      ((chart_CruiseController_ModeLogic_mode_logic_decel = 0) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_2)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_3 = (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3 or 

      rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_2);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root = 6)

                  then 

                        3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_7_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_2

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_states___root = 6))

                  then 5

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_6_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root = 4))

                  then 

                        4

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_outports_mode = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_3

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_states___root = 4))

                  then 4

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_outports_mode)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_8_outports_mode);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4 = ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root = 5) and 

      ((chart_CruiseController_ModeLogic_mode_logic_accel = 0) and 

      (not rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_complete_3)));

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4

         then 

               (if (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root = 5)

                  then 

                        3

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_9_states___root);

   rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_15_states___root = 

      (if rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_4

         then 

               (if (not (rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root = 4))

                  then 

                        4

                  else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root)

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_10_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2 = 

      (if (not 

         ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root >= 3) and 

         (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root <= 6)))

         then 

               3

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_02 = ((not 

      ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root >= 3) and 

      (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_9_states___root <= 6))) and 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2 >= 3) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2 <= 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2 = 

      (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_02

         then 

               (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2 = 4))

                  then 

                        4

                  else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2)

         else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root2);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_02 = ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2 = 4) or 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2 = 5) or 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root2 = 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1 = 

      (if (not 

         ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root >= 3) and 

         (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root <= 6)))

         then 

               3

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_01 = ((not 

      ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root >= 3) and 

      (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_6_states___root <= 6))) and 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1 >= 3) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1 <= 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1 = 

      (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_01

         then 

               (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1 = 4))

                  then 

                        4

                  else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1)

         else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root1);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_01 = ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1 = 4) or 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1 = 5) or 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root1 = 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root = 

      (if (not 

         ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root >= 3) and 

         (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root <= 6)))

         then 

               3

         else rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0 = ((not 

      ((rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root >= 3) and 

      (rlt_eval_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root <= 6))) and 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root >= 3) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root <= 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 

      (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_fired_0

         then 

               (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root = 4))

                  then 

                        4

                  else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root)

         else rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_1_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rltCheckEntryStateConsistency_0 = ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 4) or 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 5) or 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_Active_rlt_state_3_states___root = 6)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 

      (if (not 

         ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root >= 2) and 

         (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root <= 8)))

         then 

               2

         else rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0 = ((not 

      ((rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root >= 2) and 

      (rlt_eval_CruiseController_ModeLogic_mode_logic_rlt_state_3_states___root <= 8))) and 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root >= 2) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root <= 8)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root = 

      (if rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_fired_0

         then 

               (if (not (rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root = 7))

                  then 

                        7

                  else rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root)

         else rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_1_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_On_rltCheckEntryStateConsistency_0 = (

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root >= 3) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root <= 6)) or 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root = 7) or 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_On_rlt_state_3_states___root = 8)));

   rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root = 

      (if (not (chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root = 1))

         then 

               1

         else chart_CruiseController_ModeLogic_mode_logic_begin_state_states___root);

   rlt_enter_CruiseController_ModeLogic_mode_logic_rltCheckEntryStateConsistency_0 = ((rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root = 1) or 

      ((rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root >= 2) and 

      (rlt_enter_CruiseController_ModeLogic_mode_logic_rlt_state_2_states___root <= 8)));

   cruise_controller_CruiseController_ModeLogic_resumeEvent_Out = (false -> ((not (pre accelResume)) and 

      accelResume));

   cruise_controller_CruiseController_ModeLogic_safetyCondition_safetyCondition = (((((not cancel) and 

      (not brakePedal)) and 

      (if (carGear = 3)

         then true

         else false)) and 

      (if (carSpeed >= 15.0)

         then true

         else false)) and 

      validInputs);

   cruise_controller_CruiseController_ModeLogic_setEvent_Out = (false -> ((not (pre decelSet)) and 

      decelSet));

   cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed = 

      (if (chart_CruiseController_ModeLogic_mode_logic_setDesiredSpeed <> 0)

         then true

         else false);

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock = 

      (if (mode = 5)

         then true

         else false);

   newDesiredSpeed1 = (

      (if (rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_init_step and 

         (not rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock))

         then 0.0

         else (cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed - 0.05)) -> 

      (if (rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_init_step and 

         (not rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock))

         then 0.0

         else 

      (if rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock

         then (cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed - 0.05)

         else (pre newDesiredSpeed1))));

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_init_step = (true -> 

      (if (pre rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_clock)

         then false

         else (pre rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeDecreaseInDesiredSpeed_rlt_init_step)));

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock = 

      (if (mode = 6)

         then true

         else false);

   newDesiredSpeed = (

      (if (rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_init_step and 

         (not rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock))

         then 0.0

         else (cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed + 0.05)) -> 

      (if (rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_init_step and 

         (not rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock))

         then 0.0

         else 

      (if rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock

         then (cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed + 0.05)

         else (pre newDesiredSpeed))));

   rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_init_step = (true -> 

      (if (pre rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_clock)

         then false

         else (pre rlt_condact_cruise_controller_CruiseController_SetDesiredSpeed_computeIncreaseInDesiredSpeed_rlt_init_step)));

   cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed = 

      (if 

         (if (mode = 6)

            then true

            else false)

         then newDesiredSpeed

         else 

      (if 

         (if (mode = 5)

            then true

            else false)

         then newDesiredSpeed1

         else 

      (if 

         (if (mode = 4)

            then true

            else false)

         then cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed

         else 

      (if 

         (if (mode = 3)

            then true

            else false)

         then cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed

         else 0.0))));

   cruise_controller_CruiseController_SetDesiredSpeed_GOTOL_prevDesiredSpeed = (0.0 -> 

      (if (

         (if (pre cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed)

            then (pre carSpeed)

            else (pre cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed)) < 0.0)

         then 0.0

         else 

      (if (

         (if (pre cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed)

            then (pre carSpeed)

            else (pre cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed)) > 100.0)

         then 100.0

         else 

      (if (pre cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed)

         then (pre carSpeed)

         else (pre cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed)))));

   cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta = (((

      (if (((

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

            then 0.0

            else 

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

            then 100.0

            else 

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0) < ( -10.0))

         then ( -10.0)

         else 

      (if (((

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

            then 0.0

            else 

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

            then 100.0

            else 

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0) > 10.0)

         then 10.0

         else ((

               (if (

                  (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                     then carSpeed

                     else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

                  then 0.0

                  else 

               (if (

                  (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                     then carSpeed

                     else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

                  then 100.0

                  else 

               (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                  then carSpeed

                  else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0))) / 20.0) + 0.0) -> ((

      (if (((

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

            then 0.0

            else 

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

            then 100.0

            else 

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0) < ( -10.0))

         then ( -10.0)

         else 

      (if (((

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

            then 0.0

            else 

         (if (

            (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

               then carSpeed

               else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

            then 100.0

            else 

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0) > 10.0)

         then 10.0

         else ((

               (if (

                  (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                     then carSpeed

                     else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

                  then 0.0

                  else 

               (if (

                  (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                     then carSpeed

                     else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

                  then 100.0

                  else 

               (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

                  then carSpeed

                  else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed))) - carSpeed) * 1.0))) / 20.0) + 

      (if ((

         (if ((pre mode) = 4)

            then true

            else false) or 

         (if ((pre mode) = 5)

            then true

            else false)) or 

         (if ((pre mode) = 6)

            then true

            else false))

         then 

               (if ((pre cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta) < 0.0)

                  then 0.0

                  else 

               (if ((pre cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta) > 100.0)

                  then 100.0

                  else (pre cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta)))

         else 0.0)));

   cruiseThrottle = 

      (if ((

         (if (mode = 4)

            then true

            else false) or 

         (if (mode = 5)

            then true

            else false)) or 

         (if (mode = 6)

            then true

            else false))

         then 

               (if (cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta < 0.0)

                  then 0.0

                  else 

               (if (cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta > 100.0)

                  then 100.0

                  else cruise_controller_CruiseController_SetThrottle_cruiseThrottlePrevPlusDelta))

         else 0.0);

   desiredSpeed = 

      (if (

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) < 0.0)

         then 0.0

         else 

      (if (

         (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

            then carSpeed

            else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed) > 100.0)

         then 100.0

         else 

      (if cruise_controller_CruiseController_SetDesiredSpeed_setDesiredSpeed

         then carSpeed

         else cruise_controller_CruiseController_SetDesiredSpeed_IncreaseDesiredSpeed)));

  OK = ( not (mode = 4) or ( cruiseThrottle =  (0.0 -> pre cruiseThrottle) ) ) ;

  --%PROPERTY OK=true;

  --%MAIN;

tel