CristalCaveGem » LustreC » Lustrec-Tests

node top(KP_START: bool; 

      KP_CLEAR: bool; 

      KP_0: bool; 

      KP_1: bool; 

      KP_2: bool; 

      KP_3: bool; 

      KP_4: bool; 

      KP_5: bool; 

      KP_6: bool; 

      KP_7: bool; 

      KP_8: bool; 

      KP_9: bool; 

      DOOR_CLOSED: bool

) returns (OK:bool);

--@ contract guarantees OK;

var

   LEFT_DIGIT: int; 

      SETUP: bool; 

      COOKING: bool; 

      SUSPENDED: bool; 

      START_PRESSED: bool; 

      CLEAR_PRESSED: bool; 

      MIDDLE_DIGIT: int; 

      RIGHT_DIGIT: int; 

      enable: bool; 

      STEPS_TO_COOK: int;

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock: bool; 

   KP_01: bool; 

   KP_11: bool; 

   KP_21: bool; 

   KP_31: bool; 

   KP_41: bool; 

   KP_51: bool; 

   KP_61: bool; 

   KP_71: bool; 

   KP_81: bool; 

   KP_91: bool; 

   rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step: bool; 

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY: int; 

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY: int; 

   microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY: int; 

   rlt__Arrow5: int; 

   rlt__Arrow4: int; 

   rlt__Arrow3: int; 

   rlt__Arrow2: int; 

   rlt__Arrow1: int; 

   rlt__Arrow: int; 

   chart_microwave_mode_logic_start: int; 

   chart_microwave_mode_logic_clear_off: int; 

   chart_microwave_mode_logic_door_closed: int; 

   chart_microwave_mode_logic____wakeup___: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_fired_1: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_fired_2: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_complete_1: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_fired_4: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_complete_2: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_fired_5: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_fired_6: bool; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root: int; 

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode: int; 

   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root: int; 

   rlt_enter_microwave_mode_logic_ON_rlt_fired_0: bool; 

   rlt_enter_microwave_mode_logic_ON_rlt_fired_1: bool; 

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root: int; 

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode: int; 

   rlt_enter_microwave_mode_logic_ON_rlt_fired_2: bool; 

   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root: int; 

   rlt_eval_microwave_mode_logic_rlt_fired_0: bool; 

   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining: int; 

   rlt_eval_microwave_mode_logic_rlt_fired_1: bool; 

   rlt_eval_microwave_mode_logic_rlt_state_2_states___root: int; 

   rlt_eval_microwave_mode_logic_rlt_state_3_states___root: int; 

   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode: int; 

   rlt_enter_microwave_mode_logic_rlt_state_2_states___root: int; 

   chart_microwave_mode_logic_rlt_evtInitStep: bool; 

   chart_microwave_mode_logic_begin_state_states___root: int; 

   chart_microwave_mode_logic_begin_state_outports_mode: int; 

   chart_microwave_mode_logic_begin_state_outports_steps_remaining: int; 

   chart_microwave_mode_logic_final_state_states___root: int; 

   chart_microwave_mode_logic_mode: int; 

   chart_microwave_mode_logic_steps_remaining: int; 

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT: int; 

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT: int; 

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER: int; 

   microwave_microwave_mode_logic_mode: int; 

   MWI_FcnMaxI_In16: int; 

   MWI_FcnMaxI_In15: int; 

   MWI_FcnMaxI_In13: int; 

   MWI_FcnMaxI_In12: int; 

   MWI_FcnMaxI_In11: int; 

   MWI_FcnMaxI_In1: int; 

   p18: bool; 

   p19: bool; 

   p20: bool; 

   p21: bool; 

   p22: bool; 

   p23: bool; 

   p24: bool; 

   p25: bool; 

   p26: bool; 

   p27: bool; 

   p28: bool; 

   p29: bool; 

   p30: bool; 

   p31: bool; 

   p32: bool; 

   p33: bool; 

   p34: bool; 

   p35: bool; 

   p36: bool; 

   p37: bool; 

let 

   rlt__Arrow5 = (639 -> 

      (if (not (not SETUP))

         then 

               (if (MWI_FcnMaxI_In13 > 0)

                  then MWI_FcnMaxI_In13

                  else 0)

         else 639));

   rlt__Arrow4 = (639 -> 

      (if (not SUSPENDED)

         then 

               (if (MWI_FcnMaxI_In12 > 0)

                  then MWI_FcnMaxI_In12

                  else 0)

         else 639));

   rlt__Arrow3 = (639 -> 

      (if (not (not COOKING))

         then 

               (if (MWI_FcnMaxI_In16 > 0)

                  then MWI_FcnMaxI_In16

                  else 0)

         else 639));

   rlt__Arrow2 = (639 -> 

      (if (not (not SUSPENDED))

         then 

               (if (MWI_FcnMaxI_In15 > 0)

                  then MWI_FcnMaxI_In15

                  else 0)

         else 639));

   rlt__Arrow1 = (639 -> 

      (if (not COOKING)

         then 

               (if (MWI_FcnMaxI_In11 > 0)

                  then MWI_FcnMaxI_In11

                  else 0)

         else 639));

   rlt__Arrow = (639 -> 

      (if (not SETUP)

         then 

               (if (MWI_FcnMaxI_In1 > 0)

                  then MWI_FcnMaxI_In1

                  else 0)

         else 639));

   p18 = (((not (enable and 

      (not KP_CLEAR))) or 

      ((not (((((((((KP_1 or 

      KP_2) or 

      KP_3) or 

      KP_4) or 

      KP_5) or 

      KP_6) or 

      KP_7) or 

      KP_8) or 

      KP_9) or 

      KP_0)) or 

      (LEFT_DIGIT = ((STEPS_TO_COOK div 1) div 60)))) -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((((((((((KP_1 and 

      (not (pre KP_1))) or 

      (KP_2 and 

      (not (pre KP_2)))) or 

      (KP_3 and 

      (not (pre KP_3)))) or 

      (KP_4 and 

      (not (pre KP_4)))) or 

      (KP_5 and 

      (not (pre KP_5)))) or 

      (KP_6 and 

      (not (pre KP_6)))) or 

      (KP_7 and 

      (not (pre KP_7)))) or 

      (KP_8 and 

      (not (pre KP_8)))) or 

      (KP_9 and 

      (not (pre KP_9)))) or 

      (KP_0 and 

      (not (pre KP_0))))) or 

      (LEFT_DIGIT = ((STEPS_TO_COOK div 1) div 60)))));

   p23 = (true -> (((not (enable and 

      (not KP_CLEAR))) or 

      (not ((((((((((KP_1 and 

      (not (pre KP_1))) or 

      (KP_2 and 

      (not (pre KP_2)))) or 

      (KP_3 and 

      (not (pre KP_3)))) or 

      (KP_4 and 

      (not (pre KP_4)))) or 

      (KP_5 and 

      (not (pre KP_5)))) or 

      (KP_6 and 

      (not (pre KP_6)))) or 

      (KP_7 and 

      (not (pre KP_7)))) or 

      (KP_8 and 

      (not (pre KP_8)))) or 

      (KP_9 and 

      (not (pre KP_9)))) or 

      (KP_0 and 

      (not (pre KP_0)))))) or 

      (MIDDLE_DIGIT = ((STEPS_TO_COOK - (STEPS_TO_COOK div 60)*60) div 10))));

   p35 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((KP_8 and 

      (not (pre KP_8))) and 

      ((not (KP_7 and 

      (not (pre KP_7)))) and 

      ((not (KP_6 and 

      (not (pre KP_6)))) and 

      ((not (KP_5 and 

      (not (pre KP_5)))) and 

      ((not (KP_4 and 

      (not (pre KP_4)))) and 

      ((not (KP_3 and 

      (not (pre KP_3)))) and 

      ((not (KP_2 and 

      (not (pre KP_2)))) and 

      ((not (KP_1 and 

      (not (pre KP_1)))) and 

      (not (KP_0 and 

      (not (pre KP_0))))))))))))) or 

      (RIGHT_DIGIT = 8))));

   p33 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((KP_6 and 

      (not (pre KP_6))) and 

      ((not (KP_5 and 

      (not (pre KP_5)))) and 

      ((not (KP_4 and 

      (not (pre KP_4)))) and 

      ((not (KP_3 and 

      (not (pre KP_3)))) and 

      ((not (KP_2 and 

      (not (pre KP_2)))) and 

      ((not (KP_1 and 

      (not (pre KP_1)))) and 

      (not (KP_0 and 

      (not (pre KP_0))))))))))) or 

      (RIGHT_DIGIT = 6))));

   MIDDLE_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT;

   RIGHT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER;

   p25 = (enable or 

      (RIGHT_DIGIT = 0));

   p22 = (true -> (((not (enable and 

      (not KP_CLEAR))) or 

      (not ((((((((((KP_1 and 

      (not (pre KP_1))) or 

      (KP_2 and 

      (not (pre KP_2)))) or 

      (KP_3 and 

      (not (pre KP_3)))) or 

      (KP_4 and 

      (not (pre KP_4)))) or 

      (KP_5 and 

      (not (pre KP_5)))) or 

      (KP_6 and 

      (not (pre KP_6)))) or 

      (KP_7 and 

      (not (pre KP_7)))) or 

      (KP_8 and 

      (not (pre KP_8)))) or 

      (KP_9 and 

      (not (pre KP_9)))) or 

      (KP_0 and 

      (not (pre KP_0)))))) or 

      (MIDDLE_DIGIT = (pre RIGHT_DIGIT))));

   p36 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((KP_9 and 

      (not (pre KP_9))) and 

      ((not (KP_8 and 

      (not (pre KP_8)))) and 

      ((not (KP_7 and 

      (not (pre KP_7)))) and 

      ((not (KP_6 and 

      (not (pre KP_6)))) and 

      ((not (KP_5 and 

      (not (pre KP_5)))) and 

      ((not (KP_4 and 

      (not (pre KP_4)))) and 

      ((not (KP_3 and 

      (not (pre KP_3)))) and 

      ((not (KP_2 and 

      (not (pre KP_2)))) and 

      ((not (KP_1 and 

      (not (pre KP_1)))) and 

      (not (KP_0 and 

      (not (pre KP_0)))))))))))))) or 

      (RIGHT_DIGIT = 9))));

   MWI_FcnMaxI_In1 = ((pre rlt__Arrow) - 1);

   CLEAR_PRESSED = (KP_CLEAR -> (KP_CLEAR and 

      (not (pre KP_CLEAR))));

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT = ((chart_microwave_mode_logic_steps_remaining div 1) div 60);

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) - ((((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10) * 10));

   SUSPENDED = 

      (if (3 = microwave_microwave_mode_logic_mode)

         then true

         else false);

   p31 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((KP_4 and 

      (not (pre KP_4))) and 

      ((not (KP_3 and 

      (not (pre KP_3)))) and 

      ((not (KP_2 and 

      (not (pre KP_2)))) and 

      ((not (KP_1 and 

      (not (pre KP_1)))) and 

      (not (KP_0 and 

      (not (pre KP_0))))))))) or 

      (RIGHT_DIGIT = 4))));

   p37 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      (((((((((((KP_1 and 

      (not (pre KP_1))) or 

      (KP_2 and 

      (not (pre KP_2)))) or 

      (KP_3 and 

      (not (pre KP_3)))) or 

      (KP_4 and 

      (not (pre KP_4)))) or 

      (KP_5 and 

      (not (pre KP_5)))) or 

      (KP_6 and 

      (not (pre KP_6)))) or 

      (KP_7 and 

      (not (pre KP_7)))) or 

      (KP_8 and 

      (not (pre KP_8)))) or 

      (KP_9 and 

      (not (pre KP_9)))) or 

      (KP_0 and 

      (not (pre KP_0)))) or 

      (RIGHT_DIGIT = (pre RIGHT_DIGIT)))));

   MWI_FcnMaxI_In11 = ((pre rlt__Arrow1) - 1);

   MWI_FcnMaxI_In15 = ((pre rlt__Arrow2) - 1);

   p24 = (true -> (((not (enable and 

      (not KP_CLEAR))) or 

      ((((((((((KP_1 and 

      (not (pre KP_1))) or 

      (KP_2 and 

      (not (pre KP_2)))) or 

      (KP_3 and 

      (not (pre KP_3)))) or 

      (KP_4 and 

      (not (pre KP_4)))) or 

      (KP_5 and 

      (not (pre KP_5)))) or 

      (KP_6 and 

      (not (pre KP_6)))) or 

      (KP_7 and 

      (not (pre KP_7)))) or 

      (KP_8 and 

      (not (pre KP_8)))) or 

      (KP_9 and 

      (not (pre KP_9)))) or 

      (KP_0 and 

      (not (pre KP_0))))) or 

      (MIDDLE_DIGIT = (pre MIDDLE_DIGIT))));

   p20 = (enable or 

      (MIDDLE_DIGIT = 0));

   p26 = ((not (enable and 

      KP_CLEAR)) or 

      (RIGHT_DIGIT = 0));

   microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT = (((chart_microwave_mode_logic_steps_remaining div 1) - (((chart_microwave_mode_logic_steps_remaining div 1) div 60) * 60)) div 10);

   MWI_FcnMaxI_In16 = ((pre rlt__Arrow3) - 1);

   MWI_FcnMaxI_In12 = ((pre rlt__Arrow4) - 1);

   p30 = (true -> ((not (enable and 

      (not KP_CLEAR))) or 

      ((not ((KP_3 and 

      (not (pre KP_3))) and 

      ((not (KP_2 and 

      (not (pre KP_2)))) and 

      ((not (KP_1 and 

      (not (pre KP_1)))) and 

      (not (KP_0 and 

      (not (pre KP_0)))))))) or 

      (RIGHT_DIGIT = 3))));

   COOKING = 

      (if (2 = microwave_microwave_mode_logic_mode)

         then true

         else false);

   LEFT_DIGIT = microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT;

   START_PRESSED = (KP_START -> (KP_START and 

      (not (pre KP_START))));

   chart_microwave_mode_logic_start = 

      (if (START_PRESSED = false)

         then 0

         else 1);

   chart_microwave_mode_logic_clear_off = 

      (if (CLEAR_PRESSED = false)

         then 0

         else 1);

   chart_microwave_mode_logic_door_closed = 

      (if (DOOR_CLOSED = false)

         then 0

         else 1);

   chart_microwave_mode_logic____wakeup___ = true;

   chart_microwave_mode_logic_rlt_evtInitStep = (true -> 

      (if (pre chart_microwave_mode_logic____wakeup___)

         then false

         else (pre chart_microwave_mode_logic_rlt_evtInitStep)));

   chart_microwave_mode_logic_begin_state_states___root = (0 -> (pre chart_microwave_mode_logic_final_state_states___root));

   chart_microwave_mode_logic_begin_state_outports_mode = (0 -> (pre chart_microwave_mode_logic_mode));

   chart_microwave_mode_logic_begin_state_outports_steps_remaining = (0 -> (pre chart_microwave_mode_logic_steps_remaining));

   chart_microwave_mode_logic_final_state_states___root = 

      (if chart_microwave_mode_logic____wakeup___

         then 

               (if chart_microwave_mode_logic_rlt_evtInitStep

                  then rlt_enter_microwave_mode_logic_rlt_state_2_states___root

                  else 

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

                  then 

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

                           then 

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

                                    then 

                                          3

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root)

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root))

         else chart_microwave_mode_logic_begin_state_states___root);

   chart_microwave_mode_logic_mode = 

      (if chart_microwave_mode_logic____wakeup___

         then 

               (if chart_microwave_mode_logic_rlt_evtInitStep

                  then 

                        (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

                           then 1

                           else chart_microwave_mode_logic_begin_state_outports_mode)

                  else 

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

                  then 

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

                           then 

                                 (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 3))

                                    then 3

                                    else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode)

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))

         else chart_microwave_mode_logic_begin_state_outports_mode);

   chart_microwave_mode_logic_steps_remaining = 

      (if chart_microwave_mode_logic____wakeup___

         then 

               (if chart_microwave_mode_logic_rlt_evtInitStep

                  then chart_microwave_mode_logic_begin_state_outports_steps_remaining

                  else 

               (if ((not rlt_eval_microwave_mode_logic_rlt_fired_1) and 

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3)))

                  then 

                        (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

                           then (rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining - 1)

                           else rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining)

                  else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining))

         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_rlt_fired_0 = (chart_microwave_mode_logic_begin_state_states___root = 4);

   rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining = 

      (if rlt_eval_microwave_mode_logic_rlt_fired_0

         then STEPS_TO_COOK

         else chart_microwave_mode_logic_begin_state_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_rlt_fired_1 = (rlt_eval_microwave_mode_logic_rlt_fired_0 and 

      ((chart_microwave_mode_logic_begin_state_states___root = 4) and 

      (

      (if (chart_microwave_mode_logic_start <> 0)

         then true

         else false) and 

      (if (

         (if ((STEPS_TO_COOK > 0) = false)

            then 0

            else 1) <> 0)

         then true

         else false))));

   rlt_eval_microwave_mode_logic_rlt_state_2_states___root = 

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

         then 

               (if (chart_microwave_mode_logic_begin_state_states___root = 4)

                  then 

                        0

                  else chart_microwave_mode_logic_begin_state_states___root)

         else chart_microwave_mode_logic_begin_state_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

         then rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode = 

      (if rlt_eval_microwave_mode_logic_rlt_fired_1

         then 

               (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

                  then 

                        (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

                           then 3

                           else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode)

         else chart_microwave_mode_logic_begin_state_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_1 = (((rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2) and 

      (rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining <= 0)) and 

      (rlt_eval_microwave_mode_logic_rlt_state_3_states___root = 2));

   rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

         then 

               (if 

                  ((rlt_eval_microwave_mode_logic_rlt_state_3_states___root >= 1) and 

                  (rlt_eval_microwave_mode_logic_rlt_state_3_states___root <= 3))

                  then 

                        0

                  else rlt_eval_microwave_mode_logic_rlt_state_3_states___root)

         else rlt_eval_microwave_mode_logic_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

                  then 

                        4

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_2 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3) and 

      ((

      (if (chart_microwave_mode_logic_start <> 0)

         then true

         else false) and 

      (if (chart_microwave_mode_logic_door_closed <> 0)

         then true

         else false)) and 

      (not rlt_eval_microwave_mode_logic_ON_rlt_fired_1)));

   rlt_eval_microwave_mode_logic_ON_rlt_complete_1 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_2 or 

      rlt_eval_microwave_mode_logic_ON_rlt_fired_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

         then 

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root = 3)

                  then 

                        1

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_1

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root = 4))

                  then 1

                  else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode)

         else rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

                  then 

                        2

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_2

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root = 2))

                  then 2

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_4 = (((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and 

      (

      (if (chart_microwave_mode_logic_clear_off <> 0)

         then true

         else false) and 

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1))) and 

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root = 3) and 

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_1)));

   rlt_eval_microwave_mode_logic_ON_rlt_complete_2 = (rlt_eval_microwave_mode_logic_ON_rlt_fired_4 or 

      rlt_eval_microwave_mode_logic_ON_rlt_complete_1);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

         then 

               (if 

                  ((rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root >= 1) and 

                  (rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root <= 3))

                  then 

                        0

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

         then 0

         else rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining);

   rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

                  then 

                        4

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_5 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2) and 

      ((rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining > 0) and 

      (not rlt_eval_microwave_mode_logic_ON_rlt_complete_2)));

   rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_4

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root = 4))

                  then 1

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode);

   rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

         then 

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root = 2)

                  then 

                        1

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

                  then 

                        2

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_fired_6 = ((rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2) and 

      ((

      (if (chart_microwave_mode_logic_clear_off <> 0)

         then true

         else false) or 

      (not 

      (if (chart_microwave_mode_logic_door_closed <> 0)

         then true

         else false))) and 

      (not (rlt_eval_microwave_mode_logic_ON_rlt_fired_5 or 

      rlt_eval_microwave_mode_logic_ON_rlt_complete_2))));

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_6

         then 

               (if (rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root = 2)

                  then 

                        1

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root);

   rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode = 

      (if rlt_eval_microwave_mode_logic_ON_rlt_fired_5

         then 

               (if (not (rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root = 2))

                  then 2

                  else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode)

         else rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode);

   rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 

      (if (not 

         ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and 

         (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3)))

         then 

               1

         else rlt_eval_microwave_mode_logic_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_fired_0 = ((not 

      ((rlt_eval_microwave_mode_logic_rlt_state_2_states___root >= 1) and 

      (rlt_eval_microwave_mode_logic_rlt_state_2_states___root <= 3))) and 

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and 

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)));

   rlt_enter_microwave_mode_logic_ON_rlt_fired_1 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and 

      (

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root >= 1) and 

      (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root <= 3)) and 

      (if (chart_microwave_mode_logic_door_closed <> 0)

         then true

         else false)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

         then 

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

                  then 

                        2

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root)

         else rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root);

   rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode = 

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_1

         then 

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root = 2))

                  then 2

                  else chart_microwave_mode_logic_begin_state_outports_mode)

         else chart_microwave_mode_logic_begin_state_outports_mode);

   rlt_enter_microwave_mode_logic_ON_rlt_fired_2 = (rlt_enter_microwave_mode_logic_ON_rlt_fired_0 and 

      (

      ((rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root >= 1) and 

      (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root <= 3)) and 

      (not rlt_enter_microwave_mode_logic_ON_rlt_fired_1)));

   rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root = 

      (if rlt_enter_microwave_mode_logic_ON_rlt_fired_2

         then 

               (if (not (rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root = 3))

                  then 

                        3

                  else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root)

         else rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root);

   rlt_enter_microwave_mode_logic_rlt_state_2_states___root = 

      (if (not (chart_microwave_mode_logic_begin_state_states___root = 4))

         then 

               4

         else chart_microwave_mode_logic_begin_state_states___root);

   microwave_microwave_mode_logic_mode = chart_microwave_mode_logic_mode;

   OK = (((not (enable and 

      (not KP_CLEAR))) or 

      ((not (((((((((KP_1 or 

      KP_2) or 

      KP_3) or 

      KP_4) or 

      KP_5) or 

      KP_6) or 

      KP_7) or 

      KP_8) or