diff options
Diffstat (limited to 'tests/kind2-examples/a_mode_benchmark.scade')
| -rw-r--r-- | tests/kind2-examples/a_mode_benchmark.scade | 449 |
1 files changed, 449 insertions, 0 deletions
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 + + |