node microwave(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 (LEFT_DIGIT: int; MIDDLE_DIGIT: int; RIGHT_DIGIT: int; MODE: int) var microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic: int; microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING: int; microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining: int; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step: bool; microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1: int; microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1: int; microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1: int; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8: bool; rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9: bool; microwave_microwave_LE_Detector12_Logical_Operator1: bool; microwave_microwave_LE_Detector1_Logical_Operator1: bool; microwave_microwave_Unit_Delay2: bool; s1: bool; r1: bool; r3: bool; r4: bool; s2: bool; r7: bool; r8: bool; r2: bool; r5: bool; r6: bool; r10: bool; r11: bool; r12: bool; all_asserts_ok: bool; let --%MAIN r6 = ((( not (false and (0 > 0))) or (( not (( not DOOR_CLOSED) or false)) or (MODE = 3))) -> (( not (( pre (MODE = 2)) and (( pre (((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT)) > 0))) or (( not (( not DOOR_CLOSED) or (KP_CLEAR and ( not ( pre KP_CLEAR))))) or (MODE = 3)))); r5 = ((( not (false and (0 <= 0))) or (MODE = 1)) -> (( not (( pre ((MODE = 2) or (MODE = 3))) and (( pre (((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT)) <= 0))) or (MODE = 1))); r2 = ((( not false) or (( not (false and ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) > 0))) or ((MODE = 2) or (MODE = 3)))) -> (( not (MODE = 1)) or (( not ((KP_START and ( not ( pre KP_START))) and ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) > 0))) or ((MODE = 2) or (MODE = 3))))); microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 = (0 -> (if microwave_microwave_Unit_Delay2 then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR then 0 else (if ( (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0))) then 0 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1))) then 1 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2))) then 2 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3))) then 3 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4))) then 4 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5))) then 5 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6))) then 6 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7))) then 7 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8))) then 8 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9))) then 9 else 10)))))))))) <= 9) then ( pre microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1) else ( pre microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1)))) else ( pre microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1))); microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 = (0 -> (if microwave_microwave_Unit_Delay2 then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR then 0 else (if ( (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0))) then 0 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1))) then 1 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2))) then 2 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3))) then 3 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4))) then 4 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5))) then 5 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6))) then 6 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7))) then 7 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8))) then 8 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9))) then 9 else 10)))))))))) <= 9) then ( pre microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1) else ( pre microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1)))) else ( pre microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1))); microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 = ( (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR then 0 else (if ( (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 then 1 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 then 2 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 then 3 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 then 4 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 then 5 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 then 6 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 then 7 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 then 8 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 then 9 else 10)))))))))) <= 9) then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 then 1 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 then 2 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 then 3 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 then 4 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 then 5 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 then 6 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 then 7 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 then 8 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 then 9 else 10)))))))))) else 0)) -> (if microwave_microwave_Unit_Delay2 then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR then 0 else (if ( (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 then 1 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 then 2 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 then 3 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 then 4 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 then 5 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 then 6 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 then 7 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 then 8 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 then 9 else 10)))))))))) <= 9) then (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 then 0 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 then 1 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 then 2 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 then 3 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 then 4 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 then 5 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 then 6 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 then 7 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 then 8 else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 then 9 else 10)))))))))) else 0)) else (if rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR then 0 else (if ( (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0))) then 0 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1))) then 1 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2))) then 2 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3))) then 3 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4))) then 4 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5))) then 5 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6))) then 6 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7))) then 7 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8))) then 8 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9))) then 9 else 10)))))))))) <= 9) then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0))) then 0 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1))) then 1 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2))) then 2 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3))) then 3 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4))) then 4 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5))) then 5 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6))) then 6 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7))) then 7 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8))) then 8 else (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 and ( not ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9))) then 9 else 10)))))))))) else ( pre microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1)))) else ( pre microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1))); microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining = (0 -> ( pre (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)))); microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = (0 -> ( pre (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if ( (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then 0 else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING) = 2) then 0 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then 0 else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ 2 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: uint8((steps_remaining > uint16(0))) Destination: microwave_mode_logic>RUNNING>rlt_outerloop_0 */ 1 else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then /* Exiting state: microwave_mode_logic>RUNNING. */ 0 else (if (microwave_microwave_LE_Detector12_Logical_Operator1 and DOOR_CLOSED) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ 1 else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING)) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if (microwave_microwave_LE_Detector12_Logical_Operator1 and ( (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) > 0)) then /* Evaluating Transition Source: microwave_mode_logic>SETUP.microwave_mode_logic>junc8 Transition Guarded By: (uint8(start) and uint8((steps_remaining > uint16(0)))) Destination: microwave_mode_logic>RUNNING */ (if DOOR_CLOSED then /* Entering state: microwave_mode_logic>RUNNING>COOKING. */ 1 else /* Entering state: microwave_mode_logic>RUNNING>SUSPENDED. */ 2) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING)) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING))); microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = (0 -> ( pre (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then /* Entering state: microwave_mode_logic>SETUP. */ 2 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then 2 else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if (microwave_microwave_LE_Detector12_Logical_Operator1 and ( (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) > 0)) then /* Entering state: microwave_mode_logic>RUNNING>COOKING. Evaluating Transition Source: microwave_mode_logic>SETUP.microwave_mode_logic>junc8 Transition Guarded By: (uint8(start) and uint8((steps_remaining > uint16(0)))) Destination: microwave_mode_logic>RUNNING */ 1 else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic)) else 2))); MODE = ( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING Transition Guarded By: uint8((steps_remaining <= uint16(0))) Destination: microwave_mode_logic>junc9 */ 1 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ 3 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: uint8((steps_remaining > uint16(0))) Destination: microwave_mode_logic>RUNNING>rlt_outerloop_0 */ 2 else 0)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then 1 else (if (microwave_microwave_LE_Detector12_Logical_Operator1 and DOOR_CLOSED) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ 2 else 0)) else 0))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if (microwave_microwave_LE_Detector12_Logical_Operator1 and ( (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) > 0)) then /* Evaluating Transition Source: microwave_mode_logic>SETUP.microwave_mode_logic>junc8 Transition Guarded By: (uint8(start) and uint8((steps_remaining > uint16(0)))) Destination: microwave_mode_logic>RUNNING */ (if DOOR_CLOSED then 2 else 3) else 0) else 0)) else 1) -> (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING Transition Guarded By: uint8((steps_remaining <= uint16(0))) Destination: microwave_mode_logic>junc9 */ 1 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ 3 else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: uint8((steps_remaining > uint16(0))) Destination: microwave_mode_logic>RUNNING>rlt_outerloop_0 */ 2 else ( pre MODE))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then 1 else (if (microwave_microwave_LE_Detector12_Logical_Operator1 and DOOR_CLOSED) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ 2 else ( pre MODE))) else ( pre MODE)))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if (microwave_microwave_LE_Detector12_Logical_Operator1 and ( (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) > 0)) then /* Evaluating Transition Source: microwave_mode_logic>SETUP.microwave_mode_logic>junc8 Transition Guarded By: (uint8(start) and uint8((steps_remaining > uint16(0)))) Destination: microwave_mode_logic>RUNNING */ (if DOOR_CLOSED then 2 else 3) else ( pre MODE)) else ( pre MODE))) else 1)); MIDDLE_DIGIT = ((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) - ((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) / 60) * 60)) / 10); RIGHT_DIGIT = ((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) - ((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) / 60) * 60)) - (((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) - ((( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) / 60) * 60)) / 10) * 10)); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8 = (KP_8 -> (if microwave_microwave_Unit_Delay2 then KP_8 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_8))); s1 = ((not (MODE = 2)) or DOOR_CLOSED); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1 = (KP_1 -> (if microwave_microwave_Unit_Delay2 then KP_1 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_1))); microwave_microwave_Unit_Delay2 = (true -> ( pre (1 = MODE))); r8 = ((( not false) or (( not ((false and DOOR_CLOSED) and ( not false))) or (MODE = 2))) -> (( not ( pre (MODE = 3))) or (( not (((KP_START and ( not ( pre KP_START))) and DOOR_CLOSED) and ( not (KP_CLEAR and ( not ( pre KP_CLEAR)))))) or (MODE = 2)))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0 = (KP_0 -> (if microwave_microwave_Unit_Delay2 then KP_0 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_0))); r4 = ((false or (( not ((MODE = 2) or (MODE = 3))) or (DOOR_CLOSED or (MODE = 3)))) -> (( pre ((MODE = 2) or (MODE = 3))) or (( not ((MODE = 2) or (MODE = 3))) or (DOOR_CLOSED or (MODE = 3))))); r11 = ((( not false) or ((not (MODE = 2)) or (((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) + 1) = 0))) -> (( not ( pre (MODE = 2))) or ((not (MODE = 2)) or (((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) + 1) = ( pre (((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT)))))); r7 = ((( not false) or (( not false) or (MODE = 1))) -> (( not ( pre (MODE = 3))) or (( not (KP_CLEAR and ( not ( pre KP_CLEAR)))) or (MODE = 1)))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9 = (KP_9 -> (if microwave_microwave_Unit_Delay2 then KP_9 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_9))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5 = (KP_5 -> (if microwave_microwave_Unit_Delay2 then KP_5 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_5))); r10 = ((( not false) or (( not ((MODE = 2) or (MODE = 3))) or ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) <= 0))) -> (( not ( pre ((MODE = 2) or (MODE = 3)))) or (( not ((MODE = 2) or (MODE = 3))) or ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) <= ( pre (((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT)))))); LEFT_DIGIT = (( (if (not (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 0)) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 1) then (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 1) then (if (microwave_microwave_LE_Detector1_Logical_Operator1 or ( not DOOR_CLOSED)) then /* Evaluating Transition Source: microwave_mode_logic>RUNNING>COOKING Transition Guarded By: (clear or (not door_closed)) Destination: microwave_mode_logic>RUNNING>SUSPENDED */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) then (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING = 2) then (if microwave_microwave_LE_Detector1_Logical_Operator1 then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else /* Evaluating Transition Source: microwave_mode_logic>RUNNING>SUSPENDED Transition Guarded By: (start and door_closed) Destination: microwave_mode_logic>RUNNING>COOKING */ microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining))) else (if (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic = 2) then (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0) else microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining)) else (if microwave_microwave_Unit_Delay2 then (if (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step and ( not microwave_microwave_Unit_Delay2)) then 0 else (((microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 + (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 * 10)) + (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 * 60)) * 1)) else 0)) / 1) / 60); microwave_microwave_LE_Detector1_Logical_Operator1 = (KP_CLEAR -> (KP_CLEAR and ( not ( pre KP_CLEAR)))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR = (KP_CLEAR -> (if microwave_microwave_Unit_Delay2 then KP_CLEAR else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_CLEAR))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7 = (KP_7 -> (if microwave_microwave_Unit_Delay2 then KP_7 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_7))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6 = (KP_6 -> (if microwave_microwave_Unit_Delay2 then KP_6 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_6))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2 = (KP_2 -> (if microwave_microwave_Unit_Delay2 then KP_2 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_2))); r3 = ((false or (( not ((MODE = 2) or (MODE = 3))) or (( not DOOR_CLOSED) or (MODE = 2)))) -> (( pre ((MODE = 2) or (MODE = 3))) or (( not ((MODE = 2) or (MODE = 3))) or (( not DOOR_CLOSED) or (MODE = 2))))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4 = (KP_4 -> (if microwave_microwave_Unit_Delay2 then KP_4 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_4))); r1 = ((MODE = 1) -> true); s2 = ((( not false) or (( not false) or (not (MODE = 2)))) -> (( not ( pre (MODE = 2))) or (( not (KP_CLEAR and ( not ( pre KP_CLEAR)))) or (not (MODE = 2))))); r12 = ((( not false) or ((not (MODE = 3)) or ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) = 0))) -> (( not ( pre (MODE = 3))) or ((not (MODE = 3)) or ((((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT) = ( pre (((LEFT_DIGIT * 60) + (MIDDLE_DIGIT * 10)) + RIGHT_DIGIT)))))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3 = (KP_3 -> (if microwave_microwave_Unit_Delay2 then KP_3 else ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_KP_3))); rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step = (true -> (( not microwave_microwave_Unit_Delay2) or (( not ( pre microwave_microwave_Unit_Delay2)) and ( pre rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step)))); microwave_microwave_LE_Detector12_Logical_Operator1 = (KP_START -> (KP_START and ( not ( pre KP_START)))); all_asserts_ok = (true -> (( pre all_asserts_ok) and true)); -- assert (microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 >= 0 and microwave_microwave_KEYPAD_PROCESSING_RIGHT_DIGIT_Switch1 < 128); -- assert (microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 >= 0 and microwave_microwave_KEYPAD_PROCESSING_MIDDLE_DIGIT_Switch1 < 128); -- assert (microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 >= 0 and microwave_microwave_KEYPAD_PROCESSING_LEFT_DIGIT_Switch1 < 128); -- assert (rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_STEPS_PER_SECOND >= 0 and rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clocked_inp_STEPS_PER_SECOND < 128); --assert (LEFT_DIGIT >= 0 and LEFT_DIGIT <= 9); --assert (MIDDLE_DIGIT >= 0 and MIDDLE_DIGIT <= 9); --assert (RIGHT_DIGIT >= 0 and RIGHT_DIGIT <= 9); --assert (MODE >= 1 and MODE <= 3); --assert (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic >= 0 and microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic <= 2); --assert (microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING >= 0 and microwave_mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_microwave_mode_logic_RUNNING <= 2); --Line 59 -compression --%PROPERTY r1; guarantee p1: r1; --Line 64 -compression --%PROPERTY r3; --Line 68 -compression --%PROPERTY r4; --Line 72 -compression (hard) --%PROPERTY s2; --Line 76 -compression (hard) --%PROPERTY r7; --Line 56 -compression (hard) --%PROPERTY r8; --Line 97 -compression --%PROPERTY r5; --Line 105 -compression --%PROPERTY r10; --Line 109 -compression --%PROPERTY r11; --Line 113 -compression --%PROPERTY r12; tel