/* * Copyright (c) 2024-2024 Felix Ingrand, CNRS/LAAS * * Permission to use, copy, modify, and distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. */ /* * This Behavior Tree FIACRE model has been automatically generated by bt2f 1.0b0. * DO NOT EDIT. */ /* * This Behavior Tree FIACRE model is for verification with the TINA tools. */ type ret_status is union // regular returned status success | failure | running | halt_me | no_ret_status end type btnode_caller is union None | caller_Eval11_btn5 | caller_Eval13_btn6 | caller_Sequence9_sequence_1 | caller_Eval17_btn8 | caller_Eval19_btn9 | caller_Sequence15_sequence_2 | caller_Fallback7_fallback_1 | caller_Eval25_btn12 | caller_Eval27_btn13 | caller_Sequence23_sequence_3 | caller_Eval31_btn15 | caller_Eval33_btn16 | caller_Sequence29_sequence_4 | caller_Fallback21_fallback_2 | caller_Sequence5_root_sequence | caller_KeepRunningUntilFailure3_btn1 | caller_MainTree_maintree end type btnode_record is record // record to hold the shared information on a btnode caller : btnode_caller, // who called it ArgIndex : nat, // its functional level arguments in rstatus : ret_status // its last returned status end const Eval11_btn5: 0..0 is 0 const Eval13_btn6: 1..1 is 1 const Sequence9_sequence_1: 2..2 is 2 const Eval17_btn8: 3..3 is 3 const Eval19_btn9: 4..4 is 4 const Sequence15_sequence_2: 5..5 is 5 const Fallback7_fallback_1: 6..6 is 6 const Eval25_btn12: 7..7 is 7 const Eval27_btn13: 8..8 is 8 const Sequence23_sequence_3: 9..9 is 9 const Eval31_btn15: 10..10 is 10 const Eval33_btn16: 11..11 is 11 const Sequence29_sequence_4: 12..12 is 12 const Fallback21_fallback_2: 13..13 is 13 const Sequence5_root_sequence: 14..14 is 14 const KeepRunningUntilFailure3_btn1: 15..15 is 15 const MainTree_maintree: 16..16 is 16 type btnode_array is array 17 of btnode_record /* state variable integer types*/ type sv_speed is 0..10 type sv_stopped is 0..1 type sv_door_open is 0..1 /* state variable FSM types*/ /* Process automata controlling the proper transition of resources/SV */ process btnode_Eval11_btn5 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, failure, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval11_btn5].caller <> None); if (btnode[Eval11_btn5].rstatus = halt_me) then to halt end; btnode[Eval11_btn5].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; if (speed = 0) then to success else to failure end from success wait [0,0]; btnode[Eval11_btn5].rstatus := success; to done from failure wait [0,0]; btnode[Eval11_btn5].rstatus := failure; to done from halted wait [0,0]; to failure from done wait [0,0]; btnode[Eval11_btn5].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval13_btn6 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval13_btn6].caller <> None); if (btnode[Eval13_btn6].rstatus = halt_me) then to halt end; btnode[Eval13_btn6].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; // will assign: stopped := 1 stopped := 1; to success from success wait [0,0]; btnode[Eval13_btn6].rstatus := success; to done from done wait [0,0]; btnode[Eval13_btn6].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Sequence9_sequence_1 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Eval11_btn5, Eval11_btn5_done, Eval13_btn6, Eval13_btn6_done, done, ether var ignorep: nat, ignoreb: bool, next_seq: 1..3 := 1 from start_ wait [0,0]; on (btnode[Sequence9_sequence_1].caller <> None); if (btnode[Sequence9_sequence_1].rstatus = halt_me) then to halt end; btnode[Sequence9_sequence_1].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Eval11_btn5].rstatus = running) then btnode[Eval11_btn5].rstatus := halt_me; btnode[Eval11_btn5].caller := caller_Sequence9_sequence_1; to halt_wait end; if (btnode[Eval13_btn6].rstatus = running) then btnode[Eval13_btn6].rstatus := halt_me; btnode[Eval13_btn6].caller := caller_Sequence9_sequence_1; to halt_wait end; to halted from halt_wait on ( (btnode[Eval11_btn5].caller = None) and (btnode[Eval13_btn6].caller = None) and true); to halted from tick_node wait [1,1]; if (next_seq = 1) then to Eval11_btn5 end; if (next_seq = 2) then to Eval13_btn6 end; to error from Eval11_btn5 wait [0,0]; btnode[Eval11_btn5].caller := caller_Sequence9_sequence_1; to Eval11_btn5_done from Eval11_btn5_done wait [0,0]; on (btnode[Eval11_btn5].caller = None); if (btnode[Eval11_btn5].rstatus = success) then to Eval13_btn6 elsif (btnode[Eval11_btn5].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval11_btn5].rstatus = running) then next_seq := 1; to running else to error end from Eval13_btn6 wait [0,0]; btnode[Eval13_btn6].caller := caller_Sequence9_sequence_1; to Eval13_btn6_done from Eval13_btn6_done wait [0,0]; on (btnode[Eval13_btn6].caller = None); if (btnode[Eval13_btn6].rstatus = success) then next_seq := 1; to success elsif (btnode[Eval13_btn6].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval13_btn6].rstatus = running) then next_seq := 2; to running else to error end from success wait [0,0]; btnode[Sequence9_sequence_1].rstatus := success; to done from failure wait [0,0]; btnode[Sequence9_sequence_1].rstatus := failure; to done from halted wait [0,0]; next_seq := 1; to failure from running wait [0,0]; btnode[Sequence9_sequence_1].rstatus := running; to done from done wait [0,0]; btnode[Sequence9_sequence_1].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval17_btn8 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, failure, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval17_btn8].caller <> None); if (btnode[Eval17_btn8].rstatus = halt_me) then to halt end; btnode[Eval17_btn8].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; if (stopped = 1) then to success else to failure end from success wait [0,0]; btnode[Eval17_btn8].rstatus := success; to done from failure wait [0,0]; btnode[Eval17_btn8].rstatus := failure; to done from halted wait [0,0]; to failure from done wait [0,0]; btnode[Eval17_btn8].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval19_btn9 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval19_btn9].caller <> None); if (btnode[Eval19_btn9].rstatus = halt_me) then to halt end; btnode[Eval19_btn9].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; // will assign: door_open := 1 door_open := 1; to success from success wait [0,0]; btnode[Eval19_btn9].rstatus := success; to done from done wait [0,0]; btnode[Eval19_btn9].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Sequence15_sequence_2 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Eval17_btn8, Eval17_btn8_done, Eval19_btn9, Eval19_btn9_done, done, ether var ignorep: nat, ignoreb: bool, next_seq: 1..3 := 1 from start_ wait [0,0]; on (btnode[Sequence15_sequence_2].caller <> None); if (btnode[Sequence15_sequence_2].rstatus = halt_me) then to halt end; btnode[Sequence15_sequence_2].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Eval17_btn8].rstatus = running) then btnode[Eval17_btn8].rstatus := halt_me; btnode[Eval17_btn8].caller := caller_Sequence15_sequence_2; to halt_wait end; if (btnode[Eval19_btn9].rstatus = running) then btnode[Eval19_btn9].rstatus := halt_me; btnode[Eval19_btn9].caller := caller_Sequence15_sequence_2; to halt_wait end; to halted from halt_wait on ( (btnode[Eval17_btn8].caller = None) and (btnode[Eval19_btn9].caller = None) and true); to halted from tick_node wait [1,1]; if (next_seq = 1) then to Eval17_btn8 end; if (next_seq = 2) then to Eval19_btn9 end; to error from Eval17_btn8 wait [0,0]; btnode[Eval17_btn8].caller := caller_Sequence15_sequence_2; to Eval17_btn8_done from Eval17_btn8_done wait [0,0]; on (btnode[Eval17_btn8].caller = None); if (btnode[Eval17_btn8].rstatus = success) then to Eval19_btn9 elsif (btnode[Eval17_btn8].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval17_btn8].rstatus = running) then next_seq := 1; to running else to error end from Eval19_btn9 wait [0,0]; btnode[Eval19_btn9].caller := caller_Sequence15_sequence_2; to Eval19_btn9_done from Eval19_btn9_done wait [0,0]; on (btnode[Eval19_btn9].caller = None); if (btnode[Eval19_btn9].rstatus = success) then next_seq := 1; to success elsif (btnode[Eval19_btn9].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval19_btn9].rstatus = running) then next_seq := 2; to running else to error end from success wait [0,0]; btnode[Sequence15_sequence_2].rstatus := success; to done from failure wait [0,0]; btnode[Sequence15_sequence_2].rstatus := failure; to done from halted wait [0,0]; next_seq := 1; to failure from running wait [0,0]; btnode[Sequence15_sequence_2].rstatus := running; to done from done wait [0,0]; btnode[Sequence15_sequence_2].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Fallback7_fallback_1 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Sequence9_sequence_1, Sequence9_sequence_1_done, Sequence15_sequence_2, Sequence15_sequence_2_done, done, ether var ignorep: nat, ignoreb: bool, next_fb: 1..2 := 1 from start_ wait [0,0]; on (btnode[Fallback7_fallback_1].caller <> None); if (btnode[Fallback7_fallback_1].rstatus = halt_me) then to halt end; btnode[Fallback7_fallback_1].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Sequence9_sequence_1].rstatus = running) then btnode[Sequence9_sequence_1].rstatus := halt_me; btnode[Sequence9_sequence_1].caller := caller_Fallback7_fallback_1; to halt_wait end; if (btnode[Sequence15_sequence_2].rstatus = running) then btnode[Sequence15_sequence_2].rstatus := halt_me; btnode[Sequence15_sequence_2].caller := caller_Fallback7_fallback_1; to halt_wait end; to halted from halt_wait on ( (btnode[Sequence9_sequence_1].caller = None) and (btnode[Sequence15_sequence_2].caller = None) and true); to halted from tick_node wait [1,1]; if (next_fb = 1) then to Sequence9_sequence_1 end; if (next_fb = 2) then to Sequence15_sequence_2 end; to error from Sequence9_sequence_1 wait [0,0]; btnode[Sequence9_sequence_1].caller := caller_Fallback7_fallback_1; to Sequence9_sequence_1_done from Sequence9_sequence_1_done wait [0,0]; on (btnode[Sequence9_sequence_1].caller = None); if (btnode[Sequence9_sequence_1].rstatus = success) then next_fb := 1; to success elsif (btnode[Sequence9_sequence_1].rstatus = failure) then to Sequence15_sequence_2 elsif (btnode[Sequence9_sequence_1].rstatus = running) then next_fb := 1; to running else to error end from Sequence15_sequence_2 wait [0,0]; btnode[Sequence15_sequence_2].caller := caller_Fallback7_fallback_1; to Sequence15_sequence_2_done from Sequence15_sequence_2_done wait [0,0]; on (btnode[Sequence15_sequence_2].caller = None); if (btnode[Sequence15_sequence_2].rstatus = success) then next_fb := 1; to success elsif (btnode[Sequence15_sequence_2].rstatus = failure) then next_fb := 1; to failure elsif (btnode[Sequence15_sequence_2].rstatus = running) then next_fb := 2; to running else to error end from success wait [0,0]; btnode[Fallback7_fallback_1].rstatus := success; to done from failure wait [0,0]; btnode[Fallback7_fallback_1].rstatus := failure; to done from halted wait [0,0]; next_fb := 1; to failure from running wait [0,0]; btnode[Fallback7_fallback_1].rstatus := running; to done from done wait [0,0]; btnode[Fallback7_fallback_1].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval25_btn12 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, failure, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval25_btn12].caller <> None); if (btnode[Eval25_btn12].rstatus = halt_me) then to halt end; btnode[Eval25_btn12].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; if ((door_open = 0) and (speed < 10)) then to success else to failure end from success wait [0,0]; btnode[Eval25_btn12].rstatus := success; to done from failure wait [0,0]; btnode[Eval25_btn12].rstatus := failure; to done from halted wait [0,0]; to failure from done wait [0,0]; btnode[Eval25_btn12].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval27_btn13 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval27_btn13].caller <> None); if (btnode[Eval27_btn13].rstatus = halt_me) then to halt end; btnode[Eval27_btn13].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; // will assign: speed := (speed + 1) speed := (speed + 1); to success from success wait [0,0]; btnode[Eval27_btn13].rstatus := success; to done from done wait [0,0]; btnode[Eval27_btn13].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Sequence23_sequence_3 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Eval25_btn12, Eval25_btn12_done, Eval27_btn13, Eval27_btn13_done, done, ether var ignorep: nat, ignoreb: bool, next_seq: 1..3 := 1 from start_ wait [0,0]; on (btnode[Sequence23_sequence_3].caller <> None); if (btnode[Sequence23_sequence_3].rstatus = halt_me) then to halt end; btnode[Sequence23_sequence_3].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Eval25_btn12].rstatus = running) then btnode[Eval25_btn12].rstatus := halt_me; btnode[Eval25_btn12].caller := caller_Sequence23_sequence_3; to halt_wait end; if (btnode[Eval27_btn13].rstatus = running) then btnode[Eval27_btn13].rstatus := halt_me; btnode[Eval27_btn13].caller := caller_Sequence23_sequence_3; to halt_wait end; to halted from halt_wait on ( (btnode[Eval25_btn12].caller = None) and (btnode[Eval27_btn13].caller = None) and true); to halted from tick_node wait [1,1]; if (next_seq = 1) then to Eval25_btn12 end; if (next_seq = 2) then to Eval27_btn13 end; to error from Eval25_btn12 wait [0,0]; btnode[Eval25_btn12].caller := caller_Sequence23_sequence_3; to Eval25_btn12_done from Eval25_btn12_done wait [0,0]; on (btnode[Eval25_btn12].caller = None); if (btnode[Eval25_btn12].rstatus = success) then to Eval27_btn13 elsif (btnode[Eval25_btn12].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval25_btn12].rstatus = running) then next_seq := 1; to running else to error end from Eval27_btn13 wait [0,0]; btnode[Eval27_btn13].caller := caller_Sequence23_sequence_3; to Eval27_btn13_done from Eval27_btn13_done wait [0,0]; on (btnode[Eval27_btn13].caller = None); if (btnode[Eval27_btn13].rstatus = success) then next_seq := 1; to success elsif (btnode[Eval27_btn13].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval27_btn13].rstatus = running) then next_seq := 2; to running else to error end from success wait [0,0]; btnode[Sequence23_sequence_3].rstatus := success; to done from failure wait [0,0]; btnode[Sequence23_sequence_3].rstatus := failure; to done from halted wait [0,0]; next_seq := 1; to failure from running wait [0,0]; btnode[Sequence23_sequence_3].rstatus := running; to done from done wait [0,0]; btnode[Sequence23_sequence_3].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval31_btn15 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, failure, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval31_btn15].caller <> None); if (btnode[Eval31_btn15].rstatus = halt_me) then to halt end; btnode[Eval31_btn15].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; if (speed > 0) then to success else to failure end from success wait [0,0]; btnode[Eval31_btn15].rstatus := success; to done from failure wait [0,0]; btnode[Eval31_btn15].rstatus := failure; to done from halted wait [0,0]; to failure from done wait [0,0]; btnode[Eval31_btn15].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Eval33_btn16 (&btnode: btnode_array, &speed: sv_speed, &stopped: sv_stopped, &door_open: sv_door_open) is states start_, tick_node, success, halt, halted, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[Eval33_btn16].caller <> None); if (btnode[Eval33_btn16].rstatus = halt_me) then to halt end; btnode[Eval33_btn16].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; // will assign: speed := (speed - 1) speed := (speed - 1); to success from success wait [0,0]; btnode[Eval33_btn16].rstatus := success; to done from done wait [0,0]; btnode[Eval33_btn16].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Sequence29_sequence_4 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Eval31_btn15, Eval31_btn15_done, Eval33_btn16, Eval33_btn16_done, done, ether var ignorep: nat, ignoreb: bool, next_seq: 1..3 := 1 from start_ wait [0,0]; on (btnode[Sequence29_sequence_4].caller <> None); if (btnode[Sequence29_sequence_4].rstatus = halt_me) then to halt end; btnode[Sequence29_sequence_4].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Eval31_btn15].rstatus = running) then btnode[Eval31_btn15].rstatus := halt_me; btnode[Eval31_btn15].caller := caller_Sequence29_sequence_4; to halt_wait end; if (btnode[Eval33_btn16].rstatus = running) then btnode[Eval33_btn16].rstatus := halt_me; btnode[Eval33_btn16].caller := caller_Sequence29_sequence_4; to halt_wait end; to halted from halt_wait on ( (btnode[Eval31_btn15].caller = None) and (btnode[Eval33_btn16].caller = None) and true); to halted from tick_node wait [1,1]; if (next_seq = 1) then to Eval31_btn15 end; if (next_seq = 2) then to Eval33_btn16 end; to error from Eval31_btn15 wait [0,0]; btnode[Eval31_btn15].caller := caller_Sequence29_sequence_4; to Eval31_btn15_done from Eval31_btn15_done wait [0,0]; on (btnode[Eval31_btn15].caller = None); if (btnode[Eval31_btn15].rstatus = success) then to Eval33_btn16 elsif (btnode[Eval31_btn15].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval31_btn15].rstatus = running) then next_seq := 1; to running else to error end from Eval33_btn16 wait [0,0]; btnode[Eval33_btn16].caller := caller_Sequence29_sequence_4; to Eval33_btn16_done from Eval33_btn16_done wait [0,0]; on (btnode[Eval33_btn16].caller = None); if (btnode[Eval33_btn16].rstatus = success) then next_seq := 1; to success elsif (btnode[Eval33_btn16].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Eval33_btn16].rstatus = running) then next_seq := 2; to running else to error end from success wait [0,0]; btnode[Sequence29_sequence_4].rstatus := success; to done from failure wait [0,0]; btnode[Sequence29_sequence_4].rstatus := failure; to done from halted wait [0,0]; next_seq := 1; to failure from running wait [0,0]; btnode[Sequence29_sequence_4].rstatus := running; to done from done wait [0,0]; btnode[Sequence29_sequence_4].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Fallback21_fallback_2 (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Sequence23_sequence_3, Sequence23_sequence_3_done, Sequence29_sequence_4, Sequence29_sequence_4_done, done, ether var ignorep: nat, ignoreb: bool, next_fb: 1..2 := 1 from start_ wait [0,0]; on (btnode[Fallback21_fallback_2].caller <> None); if (btnode[Fallback21_fallback_2].rstatus = halt_me) then to halt end; btnode[Fallback21_fallback_2].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Sequence23_sequence_3].rstatus = running) then btnode[Sequence23_sequence_3].rstatus := halt_me; btnode[Sequence23_sequence_3].caller := caller_Fallback21_fallback_2; to halt_wait end; if (btnode[Sequence29_sequence_4].rstatus = running) then btnode[Sequence29_sequence_4].rstatus := halt_me; btnode[Sequence29_sequence_4].caller := caller_Fallback21_fallback_2; to halt_wait end; to halted from halt_wait on ( (btnode[Sequence23_sequence_3].caller = None) and (btnode[Sequence29_sequence_4].caller = None) and true); to halted from tick_node wait [1,1]; if (next_fb = 1) then to Sequence23_sequence_3 end; if (next_fb = 2) then to Sequence29_sequence_4 end; to error from Sequence23_sequence_3 wait [0,0]; btnode[Sequence23_sequence_3].caller := caller_Fallback21_fallback_2; to Sequence23_sequence_3_done from Sequence23_sequence_3_done wait [0,0]; on (btnode[Sequence23_sequence_3].caller = None); if (btnode[Sequence23_sequence_3].rstatus = success) then next_fb := 1; to success elsif (btnode[Sequence23_sequence_3].rstatus = failure) then to Sequence29_sequence_4 elsif (btnode[Sequence23_sequence_3].rstatus = running) then next_fb := 1; to running else to error end from Sequence29_sequence_4 wait [0,0]; btnode[Sequence29_sequence_4].caller := caller_Fallback21_fallback_2; to Sequence29_sequence_4_done from Sequence29_sequence_4_done wait [0,0]; on (btnode[Sequence29_sequence_4].caller = None); if (btnode[Sequence29_sequence_4].rstatus = success) then next_fb := 1; to success elsif (btnode[Sequence29_sequence_4].rstatus = failure) then next_fb := 1; to failure elsif (btnode[Sequence29_sequence_4].rstatus = running) then next_fb := 2; to running else to error end from success wait [0,0]; btnode[Fallback21_fallback_2].rstatus := success; to done from failure wait [0,0]; btnode[Fallback21_fallback_2].rstatus := failure; to done from halted wait [0,0]; next_fb := 1; to failure from running wait [0,0]; btnode[Fallback21_fallback_2].rstatus := running; to done from done wait [0,0]; btnode[Fallback21_fallback_2].caller := None; to ether from ether wait [0,0]; to start_ process btnode_Sequence5_root_sequence (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, halt_wait, running, error, Fallback7_fallback_1, Fallback7_fallback_1_done, Fallback21_fallback_2, Fallback21_fallback_2_done, done, ether var ignorep: nat, ignoreb: bool, next_seq: 1..3 := 1 from start_ wait [0,0]; on (btnode[Sequence5_root_sequence].caller <> None); if (btnode[Sequence5_root_sequence].rstatus = halt_me) then to halt end; btnode[Sequence5_root_sequence].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Fallback7_fallback_1].rstatus = running) then btnode[Fallback7_fallback_1].rstatus := halt_me; btnode[Fallback7_fallback_1].caller := caller_Sequence5_root_sequence; to halt_wait end; if (btnode[Fallback21_fallback_2].rstatus = running) then btnode[Fallback21_fallback_2].rstatus := halt_me; btnode[Fallback21_fallback_2].caller := caller_Sequence5_root_sequence; to halt_wait end; to halted from halt_wait on ( (btnode[Fallback7_fallback_1].caller = None) and (btnode[Fallback21_fallback_2].caller = None) and true); to halted from tick_node wait [1,1]; if (next_seq = 1) then to Fallback7_fallback_1 end; if (next_seq = 2) then to Fallback21_fallback_2 end; to error from Fallback7_fallback_1 wait [0,0]; btnode[Fallback7_fallback_1].caller := caller_Sequence5_root_sequence; to Fallback7_fallback_1_done from Fallback7_fallback_1_done wait [0,0]; on (btnode[Fallback7_fallback_1].caller = None); if (btnode[Fallback7_fallback_1].rstatus = success) then to Fallback21_fallback_2 elsif (btnode[Fallback7_fallback_1].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Fallback7_fallback_1].rstatus = running) then next_seq := 1; to running else to error end from Fallback21_fallback_2 wait [0,0]; btnode[Fallback21_fallback_2].caller := caller_Sequence5_root_sequence; to Fallback21_fallback_2_done from Fallback21_fallback_2_done wait [0,0]; on (btnode[Fallback21_fallback_2].caller = None); if (btnode[Fallback21_fallback_2].rstatus = success) then next_seq := 1; to success elsif (btnode[Fallback21_fallback_2].rstatus = failure) then next_seq := 1; to failure elsif (btnode[Fallback21_fallback_2].rstatus = running) then next_seq := 2; to running else to error end from success wait [0,0]; btnode[Sequence5_root_sequence].rstatus := success; to done from failure wait [0,0]; btnode[Sequence5_root_sequence].rstatus := failure; to done from halted wait [0,0]; next_seq := 1; to failure from running wait [0,0]; btnode[Sequence5_root_sequence].rstatus := running; to done from done wait [0,0]; btnode[Sequence5_root_sequence].caller := None; to ether from ether wait [0,0]; to start_ process btnode_KeepRunningUntilFailure3_btn1 (&btnode: btnode_array) is states start_, tick_node, failure, halt, halted, halt_wait, running, error, Sequence5_root_sequence, Sequence5_root_sequence_done, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[KeepRunningUntilFailure3_btn1].caller <> None); if (btnode[KeepRunningUntilFailure3_btn1].rstatus = halt_me) then to halt end; btnode[KeepRunningUntilFailure3_btn1].rstatus := no_ret_status; to tick_node from halt wait [0,0]; if (btnode[Sequence5_root_sequence].rstatus = running) then btnode[Sequence5_root_sequence].rstatus := halt_me; btnode[Sequence5_root_sequence].caller := caller_KeepRunningUntilFailure3_btn1; to halt_wait end; to halted from halt_wait on (btnode[Sequence5_root_sequence].caller = None); to halted from tick_node wait [1,1]; to Sequence5_root_sequence from Sequence5_root_sequence wait [0,0]; btnode[Sequence5_root_sequence].caller := caller_KeepRunningUntilFailure3_btn1; to Sequence5_root_sequence_done from Sequence5_root_sequence_done wait [0,0]; on (btnode[Sequence5_root_sequence].caller = None); if (btnode[Sequence5_root_sequence].rstatus = success) then to running elsif (btnode[Sequence5_root_sequence].rstatus = failure) then to failure elsif (btnode[Sequence5_root_sequence].rstatus = running) then to running else to error end from failure wait [0,0]; btnode[KeepRunningUntilFailure3_btn1].rstatus := failure; to done from halted wait [0,0]; to failure from running wait [0,0]; btnode[KeepRunningUntilFailure3_btn1].rstatus := running; to done from done wait [0,0]; btnode[KeepRunningUntilFailure3_btn1].caller := None; to ether from ether wait [0,0]; to start_ process btnode_MainTree_maintree (&btnode: btnode_array) is states start_, tick_node, success, failure, halt, halted, running, error, KeepRunningUntilFailure3_btn1, KeepRunningUntilFailure3_btn1_done, done, ether var ignorep: nat, ignoreb: bool from start_ wait [0,0]; on (btnode[MainTree_maintree].caller <> None); if (btnode[MainTree_maintree].rstatus = halt_me) then to halt end; btnode[MainTree_maintree].rstatus := no_ret_status; to tick_node from halt wait [0,0]; to halted from tick_node wait [1,1]; to KeepRunningUntilFailure3_btn1 from KeepRunningUntilFailure3_btn1 wait [0,0]; btnode[KeepRunningUntilFailure3_btn1].caller := caller_MainTree_maintree; to KeepRunningUntilFailure3_btn1_done from KeepRunningUntilFailure3_btn1_done wait [0,0]; on (btnode[KeepRunningUntilFailure3_btn1].caller = None); if (btnode[KeepRunningUntilFailure3_btn1].rstatus = success) then to success elsif (btnode[KeepRunningUntilFailure3_btn1].rstatus = failure) then to failure elsif (btnode[KeepRunningUntilFailure3_btn1].rstatus = running) then to running else to error end from success wait [0,0]; btnode[MainTree_maintree].rstatus := success; to done from failure wait [0,0]; btnode[MainTree_maintree].rstatus := failure; to done from halted wait [0,0]; to failure from running wait [0,0]; btnode[MainTree_maintree].rstatus := running; to tick_node from done wait [0,0]; btnode[MainTree_maintree].caller := None; to ether component maintree is var btnode: btnode_array := [ {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = None, ArgIndex = 0, rstatus = no_ret_status}, {caller = caller_MainTree_maintree, ArgIndex = 0, rstatus = no_ret_status}], // **** state variables ****, speed: sv_speed := 0, stopped: sv_stopped := 1, door_open: sv_door_open := 0 par * in // **** state variables processes **** // **** btnode processes **** btnode_Eval11_btn5(&btnode, &speed, &stopped, &door_open) || btnode_Eval13_btn6(&btnode, &speed, &stopped, &door_open) || btnode_Sequence9_sequence_1(&btnode) || btnode_Eval17_btn8(&btnode, &speed, &stopped, &door_open) || btnode_Eval19_btn9(&btnode, &speed, &stopped, &door_open) || btnode_Sequence15_sequence_2(&btnode) || btnode_Fallback7_fallback_1(&btnode) || btnode_Eval25_btn12(&btnode, &speed, &stopped, &door_open) || btnode_Eval27_btn13(&btnode, &speed, &stopped, &door_open) || btnode_Sequence23_sequence_3(&btnode) || btnode_Eval31_btn15(&btnode, &speed, &stopped, &door_open) || btnode_Eval33_btn16(&btnode, &speed, &stopped, &door_open) || btnode_Sequence29_sequence_4(&btnode) || btnode_Fallback21_fallback_2(&btnode) || btnode_Sequence5_root_sequence(&btnode) || btnode_KeepRunningUntilFailure3_btn1(&btnode) || btnode_MainTree_maintree(&btnode) // **** end of the component **** end maintree /* Some properties to model check */ /* Can the btn5 btnode properly execute? */ property Eval_Eval11_btn5_undoable is absent maintree/1/state ether prove Eval_Eval11_btn5_undoable /* Can the btn5 btnode success? */ property Eval_Eval11_btn5_cannot_succeed is absent maintree/1/value (btnode[Eval11_btn5].rstatus=success) prove Eval_Eval11_btn5_cannot_succeed /* Can the btn5 btnode return failure? */ property Eval_Eval11_btn5_cannot_fail is absent maintree/1/value (btnode[Eval11_btn5].rstatus=failure) prove Eval_Eval11_btn5_cannot_fail /* Can the btn5 btnode be halted? */ property Eval_Eval11_btn5_cannot_be_halted is absent maintree/1/state halted prove Eval_Eval11_btn5_cannot_be_halted /* Can the btn6 btnode properly execute? */ property Eval_Eval13_btn6_undoable is absent maintree/2/state ether prove Eval_Eval13_btn6_undoable /* Can the btn6 btnode success? */ property Eval_Eval13_btn6_cannot_succeed is absent maintree/2/value (btnode[Eval13_btn6].rstatus=success) prove Eval_Eval13_btn6_cannot_succeed /* Can the btn6 btnode return failure? */ property Eval_Eval13_btn6_cannot_fail is absent maintree/2/value (btnode[Eval13_btn6].rstatus=failure) prove Eval_Eval13_btn6_cannot_fail /* Can the btn6 btnode be halted? */ property Eval_Eval13_btn6_cannot_be_halted is absent maintree/2/state halted prove Eval_Eval13_btn6_cannot_be_halted /* Can the sequence_1 btnode properly execute? */ property Sequence_Sequence9_sequence_1_undoable is absent maintree/3/state ether prove Sequence_Sequence9_sequence_1_undoable /* Can the sequence_1 btnode success? */ property Sequence_Sequence9_sequence_1_cannot_succeed is absent maintree/3/value (btnode[Sequence9_sequence_1].rstatus=success) prove Sequence_Sequence9_sequence_1_cannot_succeed /* Can the sequence_1 btnode return failure? */ property Sequence_Sequence9_sequence_1_cannot_fail is absent maintree/3/value (btnode[Sequence9_sequence_1].rstatus=failure) prove Sequence_Sequence9_sequence_1_cannot_fail /* Can the sequence_1 btnode be halted? */ property Sequence_Sequence9_sequence_1_cannot_be_halted is absent maintree/3/state halted prove Sequence_Sequence9_sequence_1_cannot_be_halted /* Can the sequence_1 btnode return running? */ property Sequence_Sequence9_sequence_1_cannot_return_running is absent maintree/3/state running prove Sequence_Sequence9_sequence_1_cannot_return_running /* Can the sequence_1 btnode go in error? */ property Sequence_Sequence9_sequence_1_cannot_error is absent maintree/3/state error prove Sequence_Sequence9_sequence_1_cannot_error /* Can the btn8 btnode properly execute? */ property Eval_Eval17_btn8_undoable is absent maintree/4/state ether prove Eval_Eval17_btn8_undoable /* Can the btn8 btnode success? */ property Eval_Eval17_btn8_cannot_succeed is absent maintree/4/value (btnode[Eval17_btn8].rstatus=success) prove Eval_Eval17_btn8_cannot_succeed /* Can the btn8 btnode return failure? */ property Eval_Eval17_btn8_cannot_fail is absent maintree/4/value (btnode[Eval17_btn8].rstatus=failure) prove Eval_Eval17_btn8_cannot_fail /* Can the btn8 btnode be halted? */ property Eval_Eval17_btn8_cannot_be_halted is absent maintree/4/state halted prove Eval_Eval17_btn8_cannot_be_halted /* Can the btn9 btnode properly execute? */ property Eval_Eval19_btn9_undoable is absent maintree/5/state ether prove Eval_Eval19_btn9_undoable /* Can the btn9 btnode success? */ property Eval_Eval19_btn9_cannot_succeed is absent maintree/5/value (btnode[Eval19_btn9].rstatus=success) prove Eval_Eval19_btn9_cannot_succeed /* Can the btn9 btnode return failure? */ property Eval_Eval19_btn9_cannot_fail is absent maintree/5/value (btnode[Eval19_btn9].rstatus=failure) prove Eval_Eval19_btn9_cannot_fail /* Can the btn9 btnode be halted? */ property Eval_Eval19_btn9_cannot_be_halted is absent maintree/5/state halted prove Eval_Eval19_btn9_cannot_be_halted /* Can the sequence_2 btnode properly execute? */ property Sequence_Sequence15_sequence_2_undoable is absent maintree/6/state ether prove Sequence_Sequence15_sequence_2_undoable /* Can the sequence_2 btnode success? */ property Sequence_Sequence15_sequence_2_cannot_succeed is absent maintree/6/value (btnode[Sequence15_sequence_2].rstatus=success) prove Sequence_Sequence15_sequence_2_cannot_succeed /* Can the sequence_2 btnode return failure? */ property Sequence_Sequence15_sequence_2_cannot_fail is absent maintree/6/value (btnode[Sequence15_sequence_2].rstatus=failure) prove Sequence_Sequence15_sequence_2_cannot_fail /* Can the sequence_2 btnode be halted? */ property Sequence_Sequence15_sequence_2_cannot_be_halted is absent maintree/6/state halted prove Sequence_Sequence15_sequence_2_cannot_be_halted /* Can the sequence_2 btnode return running? */ property Sequence_Sequence15_sequence_2_cannot_return_running is absent maintree/6/state running prove Sequence_Sequence15_sequence_2_cannot_return_running /* Can the sequence_2 btnode go in error? */ property Sequence_Sequence15_sequence_2_cannot_error is absent maintree/6/state error prove Sequence_Sequence15_sequence_2_cannot_error /* Can the fallback_1 btnode properly execute? */ property Fallback_Fallback7_fallback_1_undoable is absent maintree/7/state ether prove Fallback_Fallback7_fallback_1_undoable /* Can the fallback_1 btnode success? */ property Fallback_Fallback7_fallback_1_cannot_succeed is absent maintree/7/value (btnode[Fallback7_fallback_1].rstatus=success) prove Fallback_Fallback7_fallback_1_cannot_succeed /* Can the fallback_1 btnode return failure? */ property Fallback_Fallback7_fallback_1_cannot_fail is absent maintree/7/value (btnode[Fallback7_fallback_1].rstatus=failure) prove Fallback_Fallback7_fallback_1_cannot_fail /* Can the fallback_1 btnode be halted? */ property Fallback_Fallback7_fallback_1_cannot_be_halted is absent maintree/7/state halted prove Fallback_Fallback7_fallback_1_cannot_be_halted /* Can the fallback_1 btnode return running? */ property Fallback_Fallback7_fallback_1_cannot_return_running is absent maintree/7/state running prove Fallback_Fallback7_fallback_1_cannot_return_running /* Can the fallback_1 btnode go in error? */ property Fallback_Fallback7_fallback_1_cannot_error is absent maintree/7/state error prove Fallback_Fallback7_fallback_1_cannot_error /* Can the btn12 btnode properly execute? */ property Eval_Eval25_btn12_undoable is absent maintree/8/state ether prove Eval_Eval25_btn12_undoable /* Can the btn12 btnode success? */ property Eval_Eval25_btn12_cannot_succeed is absent maintree/8/value (btnode[Eval25_btn12].rstatus=success) prove Eval_Eval25_btn12_cannot_succeed /* Can the btn12 btnode return failure? */ property Eval_Eval25_btn12_cannot_fail is absent maintree/8/value (btnode[Eval25_btn12].rstatus=failure) prove Eval_Eval25_btn12_cannot_fail /* Can the btn12 btnode be halted? */ property Eval_Eval25_btn12_cannot_be_halted is absent maintree/8/state halted prove Eval_Eval25_btn12_cannot_be_halted /* Can the btn13 btnode properly execute? */ property Eval_Eval27_btn13_undoable is absent maintree/9/state ether prove Eval_Eval27_btn13_undoable /* Can the btn13 btnode success? */ property Eval_Eval27_btn13_cannot_succeed is absent maintree/9/value (btnode[Eval27_btn13].rstatus=success) prove Eval_Eval27_btn13_cannot_succeed /* Can the btn13 btnode return failure? */ property Eval_Eval27_btn13_cannot_fail is absent maintree/9/value (btnode[Eval27_btn13].rstatus=failure) prove Eval_Eval27_btn13_cannot_fail /* Can the btn13 btnode be halted? */ property Eval_Eval27_btn13_cannot_be_halted is absent maintree/9/state halted prove Eval_Eval27_btn13_cannot_be_halted /* Can the sequence_3 btnode properly execute? */ property Sequence_Sequence23_sequence_3_undoable is absent maintree/10/state ether prove Sequence_Sequence23_sequence_3_undoable /* Can the sequence_3 btnode success? */ property Sequence_Sequence23_sequence_3_cannot_succeed is absent maintree/10/value (btnode[Sequence23_sequence_3].rstatus=success) prove Sequence_Sequence23_sequence_3_cannot_succeed /* Can the sequence_3 btnode return failure? */ property Sequence_Sequence23_sequence_3_cannot_fail is absent maintree/10/value (btnode[Sequence23_sequence_3].rstatus=failure) prove Sequence_Sequence23_sequence_3_cannot_fail /* Can the sequence_3 btnode be halted? */ property Sequence_Sequence23_sequence_3_cannot_be_halted is absent maintree/10/state halted prove Sequence_Sequence23_sequence_3_cannot_be_halted /* Can the sequence_3 btnode return running? */ property Sequence_Sequence23_sequence_3_cannot_return_running is absent maintree/10/state running prove Sequence_Sequence23_sequence_3_cannot_return_running /* Can the sequence_3 btnode go in error? */ property Sequence_Sequence23_sequence_3_cannot_error is absent maintree/10/state error prove Sequence_Sequence23_sequence_3_cannot_error /* Can the btn15 btnode properly execute? */ property Eval_Eval31_btn15_undoable is absent maintree/11/state ether prove Eval_Eval31_btn15_undoable /* Can the btn15 btnode success? */ property Eval_Eval31_btn15_cannot_succeed is absent maintree/11/value (btnode[Eval31_btn15].rstatus=success) prove Eval_Eval31_btn15_cannot_succeed /* Can the btn15 btnode return failure? */ property Eval_Eval31_btn15_cannot_fail is absent maintree/11/value (btnode[Eval31_btn15].rstatus=failure) prove Eval_Eval31_btn15_cannot_fail /* Can the btn15 btnode be halted? */ property Eval_Eval31_btn15_cannot_be_halted is absent maintree/11/state halted prove Eval_Eval31_btn15_cannot_be_halted /* Can the btn16 btnode properly execute? */ property Eval_Eval33_btn16_undoable is absent maintree/12/state ether prove Eval_Eval33_btn16_undoable /* Can the btn16 btnode success? */ property Eval_Eval33_btn16_cannot_succeed is absent maintree/12/value (btnode[Eval33_btn16].rstatus=success) prove Eval_Eval33_btn16_cannot_succeed /* Can the btn16 btnode return failure? */ property Eval_Eval33_btn16_cannot_fail is absent maintree/12/value (btnode[Eval33_btn16].rstatus=failure) prove Eval_Eval33_btn16_cannot_fail /* Can the btn16 btnode be halted? */ property Eval_Eval33_btn16_cannot_be_halted is absent maintree/12/state halted prove Eval_Eval33_btn16_cannot_be_halted /* Can the sequence_4 btnode properly execute? */ property Sequence_Sequence29_sequence_4_undoable is absent maintree/13/state ether prove Sequence_Sequence29_sequence_4_undoable /* Can the sequence_4 btnode success? */ property Sequence_Sequence29_sequence_4_cannot_succeed is absent maintree/13/value (btnode[Sequence29_sequence_4].rstatus=success) prove Sequence_Sequence29_sequence_4_cannot_succeed /* Can the sequence_4 btnode return failure? */ property Sequence_Sequence29_sequence_4_cannot_fail is absent maintree/13/value (btnode[Sequence29_sequence_4].rstatus=failure) prove Sequence_Sequence29_sequence_4_cannot_fail /* Can the sequence_4 btnode be halted? */ property Sequence_Sequence29_sequence_4_cannot_be_halted is absent maintree/13/state halted prove Sequence_Sequence29_sequence_4_cannot_be_halted /* Can the sequence_4 btnode return running? */ property Sequence_Sequence29_sequence_4_cannot_return_running is absent maintree/13/state running prove Sequence_Sequence29_sequence_4_cannot_return_running /* Can the sequence_4 btnode go in error? */ property Sequence_Sequence29_sequence_4_cannot_error is absent maintree/13/state error prove Sequence_Sequence29_sequence_4_cannot_error /* Can the fallback_2 btnode properly execute? */ property Fallback_Fallback21_fallback_2_undoable is absent maintree/14/state ether prove Fallback_Fallback21_fallback_2_undoable /* Can the fallback_2 btnode success? */ property Fallback_Fallback21_fallback_2_cannot_succeed is absent maintree/14/value (btnode[Fallback21_fallback_2].rstatus=success) prove Fallback_Fallback21_fallback_2_cannot_succeed /* Can the fallback_2 btnode return failure? */ property Fallback_Fallback21_fallback_2_cannot_fail is absent maintree/14/value (btnode[Fallback21_fallback_2].rstatus=failure) prove Fallback_Fallback21_fallback_2_cannot_fail /* Can the fallback_2 btnode be halted? */ property Fallback_Fallback21_fallback_2_cannot_be_halted is absent maintree/14/state halted prove Fallback_Fallback21_fallback_2_cannot_be_halted /* Can the fallback_2 btnode return running? */ property Fallback_Fallback21_fallback_2_cannot_return_running is absent maintree/14/state running prove Fallback_Fallback21_fallback_2_cannot_return_running /* Can the fallback_2 btnode go in error? */ property Fallback_Fallback21_fallback_2_cannot_error is absent maintree/14/state error prove Fallback_Fallback21_fallback_2_cannot_error /* Can the root_sequence btnode properly execute? */ property Sequence_Sequence5_root_sequence_undoable is absent maintree/15/state ether prove Sequence_Sequence5_root_sequence_undoable /* Can the root_sequence btnode success? */ property Sequence_Sequence5_root_sequence_cannot_succeed is absent maintree/15/value (btnode[Sequence5_root_sequence].rstatus=success) prove Sequence_Sequence5_root_sequence_cannot_succeed /* Can the root_sequence btnode return failure? */ property Sequence_Sequence5_root_sequence_cannot_fail is absent maintree/15/value (btnode[Sequence5_root_sequence].rstatus=failure) prove Sequence_Sequence5_root_sequence_cannot_fail /* Can the root_sequence btnode be halted? */ property Sequence_Sequence5_root_sequence_cannot_be_halted is absent maintree/15/state halted prove Sequence_Sequence5_root_sequence_cannot_be_halted /* Can the root_sequence btnode return running? */ property Sequence_Sequence5_root_sequence_cannot_return_running is absent maintree/15/state running prove Sequence_Sequence5_root_sequence_cannot_return_running /* Can the root_sequence btnode go in error? */ property Sequence_Sequence5_root_sequence_cannot_error is absent maintree/15/state error prove Sequence_Sequence5_root_sequence_cannot_error /* Can the btn1 btnode properly execute? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_undoable is absent maintree/16/state ether prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_undoable /* Can the btn1 btnode success? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_succeed is absent maintree/16/value (btnode[KeepRunningUntilFailure3_btn1].rstatus=success) prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_succeed /* Can the btn1 btnode return failure? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_fail is absent maintree/16/value (btnode[KeepRunningUntilFailure3_btn1].rstatus=failure) prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_fail /* Can the btn1 btnode be halted? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_be_halted is absent maintree/16/state halted prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_be_halted /* Can the btn1 btnode return running? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_return_running is absent maintree/16/state running prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_return_running /* Can the btn1 btnode go in error? */ property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_error is absent maintree/16/state error prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_error /* Can the maintree btnode properly execute? */ property BehaviorTree_MainTree_maintree_undoable is absent maintree/17/state ether prove BehaviorTree_MainTree_maintree_undoable /* Can the maintree btnode success? */ property BehaviorTree_MainTree_maintree_cannot_succeed is absent maintree/17/value (btnode[MainTree_maintree].rstatus=success) prove BehaviorTree_MainTree_maintree_cannot_succeed /* Can the maintree btnode return failure? */ property BehaviorTree_MainTree_maintree_cannot_fail is absent maintree/17/value (btnode[MainTree_maintree].rstatus=failure) prove BehaviorTree_MainTree_maintree_cannot_fail /* Can the maintree btnode be halted? */ property BehaviorTree_MainTree_maintree_cannot_be_halted is absent maintree/17/state halted prove BehaviorTree_MainTree_maintree_cannot_be_halted /* Can the maintree btnode return running? */ property BehaviorTree_MainTree_maintree_cannot_return_running is absent maintree/17/state running prove BehaviorTree_MainTree_maintree_cannot_return_running /* Can the maintree btnode go in error? */ property BehaviorTree_MainTree_maintree_cannot_error is absent maintree/17/state error prove BehaviorTree_MainTree_maintree_cannot_error /*End of File */ prove absent maintree/12/value (speed=1 and door_open=1 and stopped =1)