diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/kind2-examples/a_microwave.scade | 1428 | ||||
| -rw-r--r-- | tests/kind2-examples/a_mode_benchmark.scade | 449 | ||||
| -rw-r--r-- | tests/kind2-examples/a_two_counters.scade | 25 |
3 files changed, 1902 insertions, 0 deletions
diff --git a/tests/kind2-examples/a_microwave.scade b/tests/kind2-examples/a_microwave.scade new file mode 100644 index 0000000..ae66058 --- /dev/null +++ b/tests/kind2-examples/a_microwave.scade @@ -0,0 +1,1428 @@ + +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 diff --git a/tests/kind2-examples/a_mode_benchmark.scade b/tests/kind2-examples/a_mode_benchmark.scade new file mode 100644 index 0000000..d2abda6 --- /dev/null +++ b/tests/kind2-examples/a_mode_benchmark.scade @@ -0,0 +1,449 @@ + +node mode_logic(START: bool; + CLEAR: bool; + DOOR_CLOSED: bool; + STEPS_TO_COOK: int) + returns (MODE: int; -- subrange [0, 3] of int + STEPS_REMAINING: int) + +var + m0, m1, m2, m3:bool; + r0, r1, r2: bool; + + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING: int; -- subrange [0, 2] of int + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state5_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state3_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state13_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_simp_rlt_node_state25_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state25_rlt_chart_data_outports_mode: int; + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic: int; + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_outports_mode: int; + mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic: int; + mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic_RUNNING: int; + mode_logic_main_rlt_state_in_rlt_chart_data_outports_mode: int; + mode_logic_main_rlt_state_in_rlt_chart_data_outports_steps_remaining: int; + mode_logic_main_rlt__ARROW: bool; + all_asserts_ok: bool; + added_invariant_1, added_invariant_2, added_invariants: bool; + +let --%MAIN + + -- bla + + m0 = pre (MODE = 0); + m1 = pre (MODE = 1); + m2 = pre (MODE = 2); + m3 = pre (MODE = 3); + r0 = pre (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = 0); + r1 = pre (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = 1); + r2 = pre (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = 2); + + -- the code + + mode_logic_main_rlt__ARROW = (true -> false); + + mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic = (0 -> ( pre mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic)); + + mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic_RUNNING = (0 -> ( pre mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING)); + + mode_logic_main_rlt_state_in_rlt_chart_data_outports_mode = (0 -> ( pre MODE)); + + mode_logic_main_rlt_state_in_rlt_chart_data_outports_steps_remaining = (0 -> ( pre STEPS_REMAINING)); + + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = + (if mode_logic_main_rlt__ARROW + then 0 + else mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = + (if mode_logic_main_rlt__ARROW + then 0 + else mode_logic_main_rlt_state_in_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode = + (if mode_logic_main_rlt__ARROW + then 0 + else mode_logic_main_rlt_state_in_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining = + (if mode_logic_main_rlt__ARROW + then 0 + else mode_logic_main_rlt_state_in_rlt_chart_data_outports_steps_remaining); + + + + mode_logic_main_simp_rlt_node_state3_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 1) + then 0 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + + + mode_logic_main_simp_rlt_node_state13_rlt_chart_data_outports_steps_remaining = (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining - 1); + + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: uint8((steps_remaining > FcnToAny)) + Destination: mode_logic>RUNNING>rlt_outerloop_0 */ + 1 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: uint8((steps_remaining > FcnToAny)) + Destination: mode_logic>RUNNING>rlt_outerloop_0 */ + 2 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining > 0) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: uint8((steps_remaining > FcnToAny)) + Destination: mode_logic>RUNNING>rlt_outerloop_0 */ + mode_logic_main_simp_rlt_node_state13_rlt_chart_data_outports_steps_remaining + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining); + + + + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_states_mode_logic_RUNNING = + (if (CLEAR or + ( not DOOR_CLOSED)) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: (clear or (not door_closed)) + Destination: mode_logic>RUNNING>SUSPENDED */ + 2 + else mode_logic_main_simp_rlt_node_state16_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_mode = + (if (CLEAR or + ( not DOOR_CLOSED)) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: (clear or (not door_closed)) + Destination: mode_logic>RUNNING>SUSPENDED */ + 3 + else mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_steps_remaining = + (if (CLEAR or + ( not DOOR_CLOSED)) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: (clear or (not door_closed)) + Destination: mode_logic>RUNNING>SUSPENDED */ + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining + else mode_logic_main_simp_rlt_node_state16_rlt_chart_data_outports_steps_remaining); + + + mode_logic_main_simp_rlt_node_state5_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state3_rlt_chart_data_states_mode_logic_RUNNING = 2) + then 0 + else mode_logic_main_simp_rlt_node_state3_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state25_rlt_chart_data_states_mode_logic_RUNNING = + (if (START and + DOOR_CLOSED) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>SUSPENDED + Transition Guarded By: (start and door_closed) + Destination: mode_logic>RUNNING>COOKING */ + 1 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state25_rlt_chart_data_outports_mode = + (if (START and + DOOR_CLOSED) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>SUSPENDED + Transition Guarded By: (start and door_closed) + Destination: mode_logic>RUNNING>COOKING */ + 2 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic = + (if CLEAR + then 2 + else + /* Evaluating Transition + Source: mode_logic>RUNNING>SUSPENDED + Transition Guarded By: (start and door_closed) + Destination: mode_logic>RUNNING>COOKING */ + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic_RUNNING = + (if CLEAR + then + /* Exiting state: mode_logic>RUNNING. */ + 0 + else mode_logic_main_simp_rlt_node_state25_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_mode = + (if CLEAR + then 1 + else mode_logic_main_simp_rlt_node_state25_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_steps_remaining = + (if CLEAR + then STEPS_TO_COOK + else + /* Evaluating Transition + Source: mode_logic>RUNNING>SUSPENDED + Transition Guarded By: (start and door_closed) + Destination: mode_logic>RUNNING>COOKING */ + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 2) + then mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 2) + then mode_logic_main_simp_rlt_node_state26_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 2) + then mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_mode + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 2) + then mode_logic_main_simp_rlt_node_state26_rlt_chart_data_outports_steps_remaining + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 1) + then + /* Evaluating Transition + Source: mode_logic>RUNNING>COOKING + Transition Guarded By: (clear or (not door_closed)) + Destination: mode_logic>RUNNING>SUSPENDED */ + mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic + else mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 1) + then mode_logic_main_simp_rlt_node_state17_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state27_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 1) + then mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_mode + else mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING = 1) + then mode_logic_main_simp_rlt_node_state17_rlt_chart_data_outports_steps_remaining + else mode_logic_main_simp_rlt_node_state27_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) + then + /* Entering state: mode_logic>SETUP. */ + 2 + else mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) + then + /* Entering state: mode_logic>SETUP. */ + mode_logic_main_simp_rlt_node_state5_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state28_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) + then + /* Evaluating Transition + Source: mode_logic>RUNNING + Transition Guarded By: uint8((steps_remaining <= FcnToAny)) + Destination: mode_logic>junc9 */ + 1 + else mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining <= 0) + then STEPS_TO_COOK + else mode_logic_main_simp_rlt_node_state28_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic = + (if (START and + (STEPS_TO_COOK > 0)) + then + /* Entering state: mode_logic>RUNNING>COOKING. + Evaluating Transition + Source: mode_logic>SETUP.mode_logic>junc8 + Transition Guarded By: (uint8(start) and uint8((steps_remaining > FcnToAny))) + Destination: mode_logic>RUNNING */ + 1 + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic_RUNNING = + (if (START and + (STEPS_TO_COOK > 0)) + then + /* Evaluating Transition + Source: mode_logic>SETUP.mode_logic>junc8 + Transition Guarded By: (uint8(start) and uint8((steps_remaining > FcnToAny))) + Destination: mode_logic>RUNNING */ + + (if DOOR_CLOSED + then + /* Entering state: mode_logic>RUNNING>COOKING. */ + 1 + else + /* Entering state: mode_logic>RUNNING>SUSPENDED. */ + 2) + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state37_rlt_chart_data_outports_mode = + (if (START and + (STEPS_TO_COOK > 0)) + then + /* Evaluating Transition + Source: mode_logic>SETUP.mode_logic>junc8 + Transition Guarded By: (uint8(start) and uint8((steps_remaining > FcnToAny))) + Destination: mode_logic>RUNNING */ + + (if DOOR_CLOSED + then 2 + else 3) + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode); + + + + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 2) + then mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 2) + then mode_logic_main_simp_rlt_node_state37_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 2) + then mode_logic_main_simp_rlt_node_state37_rlt_chart_data_outports_mode + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 2) + then STEPS_TO_COOK + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 1) + then mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic + else mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic); + + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic_RUNNING = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 1) + then mode_logic_main_simp_rlt_node_state29_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state38_rlt_chart_data_states_mode_logic_RUNNING); + + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_mode = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 1) + then mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_mode + else mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_mode); + + mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_steps_remaining = + (if (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 1) + then mode_logic_main_simp_rlt_node_state29_rlt_chart_data_outports_steps_remaining + else mode_logic_main_simp_rlt_node_state38_rlt_chart_data_outports_steps_remaining); + + mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic = + (if (not (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 0)) + then mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic + else 2); + + mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = + (if (not (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 0)) + then mode_logic_main_simp_rlt_node_state39_rlt_chart_data_states_mode_logic_RUNNING + else mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic_RUNNING); + + + + + + MODE = + (if (not (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 0)) + then mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_mode + else 1); + + STEPS_REMAINING = + (if (not (mode_logic_main_simp_rlt_node_state1_rlt_chart_data_states_mode_logic = 0)) + then mode_logic_main_simp_rlt_node_state39_rlt_chart_data_outports_steps_remaining + else STEPS_TO_COOK); + + -- ADDED INVARIANTS + + + added_invariant_1 = ((not (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic <> 1)) or (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = 0)); + added_invariant_2 = ((MODE = 2) = (mode_logic_main_simp_rlt_node_state43_rlt_chart_data_states_mode_logic_RUNNING = 1)); + added_invariants = added_invariant_1 and added_invariant_2 ; + + + all_asserts_ok = (added_invariants -> (( pre all_asserts_ok) and added_invariants)); + + + -- second part of this property is the necessary invariant. + + + + --%PROPERTY ((MODE = 2) => DOOR_CLOSED); + guarantee PROPERTY: (not DOOR_CLOSED) or (MODE = 2); + +tel + + diff --git a/tests/kind2-examples/a_two_counters.scade b/tests/kind2-examples/a_two_counters.scade new file mode 100644 index 0000000..687c54a --- /dev/null +++ b/tests/kind2-examples/a_two_counters.scade @@ -0,0 +1,25 @@ +node top + (x: bool) +returns + (OK: bool) + +var + V13_b: bool; + V14_d: bool; + V40_a: bool; + V41_b: bool; + V51_time: int; + +let + + V51_time = (0 -> (if ((pre V51_time) = 3) then 0 else ((pre V51_time) + 1))); + V41_b = (false -> (pre V40_a)); + V40_a = (false -> (not (pre V41_b))); + V14_d = (V51_time = 2); + V13_b = (V40_a and V41_b); + OK = (V13_b = V14_d); + + guarantee PROPERTY: OK; + +tel + |