summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-23 17:41:49 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-23 17:41:49 +0200
commit743f5cd5fb39e3ec58f94e43fe25ae8c25de7443 (patch)
tree34a3e7e660c1d1400f33704a6fc2468407b87c6c /tests
parentd3010ba184f1b2f066efa1b6683e797558e7a21a (diff)
downloadscade-analyzer-743f5cd5fb39e3ec58f94e43fe25ae8c25de7443.tar.gz
scade-analyzer-743f5cd5fb39e3ec58f94e43fe25ae8c25de7443.zip
Add a few examples from KIND2 distribution.
Diffstat (limited to 'tests')
-rw-r--r--tests/kind2-examples/a_microwave.scade1428
-rw-r--r--tests/kind2-examples/a_mode_benchmark.scade449
-rw-r--r--tests/kind2-examples/a_two_counters.scade25
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
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 13:19:55 +0000