/*
 * 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.
 */


type ret_status is union // regular returned status
	  success
	| failure
	| running
	| halt_me
	| no_ret_status
end

type node_status is union // regular node status
	  ns_idle
	| ns_ticked
	| ns_tick_passed
	| ns_success
	| ns_failure
	| ns_halt
	| ns_halted
	| ns_running
end

type btnode_caller is union
	  None
	| caller_ParallelAll5_btn2
	| caller_measure_battery_btn9
	| caller_fail_btn8
	| caller_Eval21_btn10
	| caller_Fallback15_btn7
	| caller_Eval25_btn12
	| caller_Eval29_btn14
	| caller_Fallback27_btn13
	| caller_Sequence13_btn6
	| caller_fail_btn18
	| caller_Fallback33_btn16
	| caller_Eval53_btn26
	| caller_Sequence51_btn25
	| caller_Repeat49_btn24
	| caller_Parallel45_btn22
	| caller_Eval73_btn36
	| caller_Sequence41_btn20
	| caller_ReactiveSequence11_btn5
	| caller_Sequence3_btn1
	| caller_BehaviorTree1_drone
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 start_drone_btn3: 0..0 is 0
const start_camera_btn4: 1..1 is 1
const ParallelAll5_btn2: 2..2 is 2
const measure_battery_btn9: 3..3 is 3
const fail_btn8: 4..4 is 4
const Eval21_btn10: 5..5 is 5
const land_btn11: 6..6 is 6
const Fallback15_btn7: 7..7 is 7
const Eval25_btn12: 8..8 is 8
const Eval29_btn14: 9..9 is 9
const goto_waypoint_btn15: 10..10 is 10
const Fallback27_btn13: 11..11 is 11
const Sequence13_btn6: 12..12 is 12
const localization_ok_btn17: 13..13 is 13
const land_btn19: 14..14 is 14
const fail_btn18: 15..15 is 15
const Fallback33_btn16: 16..16 is 16
const takeoff_btn21: 17..17 is 17
const camera_tracking_camera_track: 18..18 is 18
const Eval53_btn26: 19..19 is 19
const goto_waypoint_btn27: 20..20 is 20
const goto_waypoint_btn28: 21..21 is 21
const goto_waypoint_btn29: 22..22 is 22
const goto_waypoint_btn30: 23..23 is 23
const goto_waypoint_btn31: 24..24 is 24
const goto_waypoint_btn32: 25..25 is 25
const Sequence51_btn25: 26..26 is 26
const Repeat49_btn24: 27..27 is 27
const Parallel45_btn22: 28..28 is 28
const goto_waypoint_btn33: 29..29 is 29
const land_btn34: 30..30 is 30
const shutdown_drone_btn35: 31..31 is 31
const Eval73_btn36: 32..32 is 32
const Sequence41_btn20: 33..33 is 33
const ReactiveSequence11_btn5: 34..34 is 34
const Sequence3_btn1: 35..35 is 35
const BehaviorTree1_drone: 36..36 is 36

type btnode_array is array 37 of btnode_record


/* state variable integer types*/
type sv_fls is 0..3

/* state variable FSM types*/
type sv_localization_status is union
	  Invalid
	| Coarse
	| Valid
end

type sv_battery is union
	  Good
	| Low
	| Critical
end


/* Process automata controlling the proper transition of resources/SV */

process sv_localization_status_automata (&localization_status:sv_localization_status) is

	states Invalid, Coarse , Valid 

	from Invalid
		wait [0,0];
		select
			on (localization_status = Coarse);
			to Coarse
		[]
			on (localization_status = Valid);
			to Valid
		end

	from Coarse
		wait [0,0];
		select
			on (localization_status = Invalid);
			to Invalid
		[]
			on (localization_status = Valid);
			to Valid
		end

	from Valid
		wait [0,0];
		select
			on (localization_status = Invalid);
			to Invalid
		[]
			on (localization_status = Coarse);
			to Coarse
		end

process sv_battery_automata (&battery:sv_battery) is

	states Good, Low , Critical 

	from Good
		wait [0,0];
		select
			on (battery = Low);
			to Low
		[]
			on (battery = Critical);
			to Critical
		end

	from Low
		wait [0,0];
		select
			on (battery = Good);
			to Good
		[]
			on (battery = Critical);
			to Critical
		end

	from Critical
		wait [0,0];
		select
			on (battery = Good);
			to Good
		[]
			on (battery = Low);
			to Low
		end

process btnode_start_drone_btn3 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[start_drone_btn3].caller = None));
		if (btnode[start_drone_btn3].rstatus = halt_me) then to halt end;
		btnode[start_drone_btn3].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[start_drone_btn3].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[start_drone_btn3].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[start_drone_btn3].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[start_drone_btn3].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[start_drone_btn3].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_start_camera_btn4 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[start_camera_btn4].caller = None));
		if (btnode[start_camera_btn4].rstatus = halt_me) then to halt end;
		btnode[start_camera_btn4].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[start_camera_btn4].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[start_camera_btn4].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[start_camera_btn4].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[start_camera_btn4].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[start_camera_btn4].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_ParallelAll5_btn2 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait,
		running, ParallelAll5_btn2_par, ParallelAll5_btn2_par_done, failure_wait, failure_wait2, success_wait, success_wait2,
		done, ether

	var ignorep: nat, ignoreb: bool,
		runningb:bool := false,
		halt_called_by_me:bool := false,
		force_success:bool := false

	from start_
		wait [0,0];
		on (not (btnode[ParallelAll5_btn2].caller = None));
		if (btnode[ParallelAll5_btn2].rstatus = halt_me) then to halt end;
		btnode[ParallelAll5_btn2].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[start_drone_btn3].rstatus = running) then
			btnode[start_drone_btn3].rstatus := halt_me;
			btnode[start_drone_btn3].caller := caller_ParallelAll5_btn2
		end;
		if (btnode[start_camera_btn4].rstatus = running) then
			btnode[start_camera_btn4].rstatus := halt_me;
			btnode[start_camera_btn4].caller := caller_ParallelAll5_btn2
		end;
		to halt_wait

	from halt_wait
		on (
			(btnode[start_drone_btn3].caller = None) and
			(btnode[start_camera_btn4].caller = None) and
			true);

	to halted

	from tick_node
		wait [0,0];
	to ParallelAll5_btn2_par

	from ParallelAll5_btn2_par
		wait [0,0];
		if (runningb) then
			if (btnode[start_drone_btn3].rstatus = running) then
				btnode[start_drone_btn3].caller := caller_ParallelAll5_btn2
			end;
			if (btnode[start_camera_btn4].rstatus = running) then
				btnode[start_camera_btn4].caller := caller_ParallelAll5_btn2
			end;
			null
		else
			btnode[start_drone_btn3].caller := caller_ParallelAll5_btn2;
			btnode[start_camera_btn4].caller := caller_ParallelAll5_btn2;
			null
		end;
		to ParallelAll5_btn2_par_done

	from ParallelAll5_btn2_par_done
		wait [0,0];
		on (
			(btnode[start_drone_btn3].caller = None) and
			(btnode[start_camera_btn4].caller = None) and
			true);
		if (
			(btnode[start_drone_btn3].rstatus = success) and
			(btnode[start_camera_btn4].rstatus = success) and
			true) then
				runningb := false;
			to success
		elsif (
			(btnode[start_drone_btn3].rstatus = failure) or
			(btnode[start_camera_btn4].rstatus = failure) or
			false) then
				runningb := false;
			to failure_wait
		else 
				runningb := true;
			to running
		end

	from success_wait
		wait [0,0];
		if (btnode[start_drone_btn3].rstatus = running) then
			btnode[start_drone_btn3].caller := caller_ParallelAll5_btn2
			end;
		if (btnode[start_camera_btn4].rstatus = running) then
			btnode[start_camera_btn4].caller := caller_ParallelAll5_btn2
			end;
	to success_wait2

	from success_wait2
		wait [0,0];
		on (
			(btnode[start_drone_btn3].caller = None) and
			(btnode[start_camera_btn4].caller = None) and
			true);
		if (
			(btnode[start_drone_btn3].rstatus = running) or
			(btnode[start_camera_btn4].rstatus = running) or
			false) then
			to success_wait
		else
			to success
		end

	from failure_wait
		wait [0,0];
		if (btnode[start_drone_btn3].rstatus = running) then
			btnode[start_drone_btn3].caller := caller_ParallelAll5_btn2
		end;
		if (btnode[start_camera_btn4].rstatus = running) then
			btnode[start_camera_btn4].caller := caller_ParallelAll5_btn2
		end;
	to failure_wait2

	from failure_wait2
		wait [0,0];
		on (
			(btnode[start_drone_btn3].caller = None) and
			(btnode[start_camera_btn4].caller = None) and
			true);
		if (
			(btnode[start_drone_btn3].rstatus = running) or
			(btnode[start_camera_btn4].rstatus = running) or
			false) then
				to failure_wait
			else
				to failure
		end

	from success
		wait [0,0];
		btnode[ParallelAll5_btn2].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[ParallelAll5_btn2].rstatus := failure;
		to done

	from halted
		wait [0,0];
		if (halt_called_by_me) then
			if (force_success) then
				btnode[ParallelAll5_btn2].rstatus := success
			else
				btnode[ParallelAll5_btn2].rstatus := failure
			end
		else
			btnode[ParallelAll5_btn2].rstatus := failure
		end;
		halt_called_by_me := false;
		force_success := false;
		to done

	from running
		wait [0,0];
		btnode[ParallelAll5_btn2].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[ParallelAll5_btn2].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_measure_battery_btn9 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[measure_battery_btn9].caller = None));
		if (btnode[measure_battery_btn9].rstatus = halt_me) then to halt end;
		btnode[measure_battery_btn9].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		select
			battery := Good
		[]
			battery := Low
		[]
			battery := Critical
		end;
		to success

	from success
		wait [0,0];
		btnode[measure_battery_btn9].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[measure_battery_btn9].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[measure_battery_btn9].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[measure_battery_btn9].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_fail_btn8 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		measure_battery_btn9, measure_battery_btn9_done,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[fail_btn8].caller = None));
		if (btnode[fail_btn8].rstatus = halt_me) then to halt end;
		btnode[fail_btn8].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[measure_battery_btn9].rstatus = running) then
			btnode[measure_battery_btn9].rstatus := halt_me;
			btnode[measure_battery_btn9].caller := caller_fail_btn8;
		to halt_wait
		end;
		to halted

	from halt_wait
			on (btnode[measure_battery_btn9].caller = None);

	to halted

	from tick_node
		wait [0,0];
	to measure_battery_btn9

	from measure_battery_btn9
		wait [0,0];
		btnode[measure_battery_btn9].caller := caller_fail_btn8;
		to measure_battery_btn9_done

	from measure_battery_btn9_done
		wait [0,0];
		on (btnode[measure_battery_btn9].caller = None);
		if (btnode[measure_battery_btn9].rstatus = success) then
			to failure
		elsif (btnode[measure_battery_btn9].rstatus = failure) then
			to failure
		elsif (btnode[measure_battery_btn9].rstatus = running) then
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[fail_btn8].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[fail_btn8].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[fail_btn8].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[fail_btn8].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[fail_btn8].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Eval21_btn10 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[Eval21_btn10].caller = None));
		if (btnode[Eval21_btn10].rstatus = halt_me) then to halt end;
		btnode[Eval21_btn10].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		if (not (battery = Critical)) then
			to success
		else
			to failure
		end

	from success
		wait [0,0];
		btnode[Eval21_btn10].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Eval21_btn10].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Eval21_btn10].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[Eval21_btn10].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_land_btn11 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[land_btn11].caller = None));
		if (btnode[land_btn11].rstatus = halt_me) then to halt end;
		btnode[land_btn11].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[land_btn11].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[land_btn11].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[land_btn11].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[land_btn11].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[land_btn11].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Fallback15_btn7 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		fail_btn8, fail_btn8_done,
		Eval21_btn10, Eval21_btn10_done,
		land_btn11, land_btn11_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_fb:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Fallback15_btn7].caller = None));
		if (btnode[Fallback15_btn7].rstatus = halt_me) then to halt end;
		btnode[Fallback15_btn7].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[fail_btn8].rstatus = running) then
			btnode[fail_btn8].rstatus := halt_me;
			btnode[fail_btn8].caller := caller_Fallback15_btn7;
			to halt_wait
		end;
		if (btnode[Eval21_btn10].rstatus = running) then
			btnode[Eval21_btn10].rstatus := halt_me;
			btnode[Eval21_btn10].caller := caller_Fallback15_btn7;
			to halt_wait
		end;
		if (btnode[land_btn11].rstatus = running) then
			btnode[land_btn11].rstatus := halt_me;
			btnode[land_btn11].caller := caller_Fallback15_btn7;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[fail_btn8].caller = None) and
			(btnode[Eval21_btn10].caller = None) and
			(btnode[land_btn11].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_fb = 0) then to fail_btn8 end;
		if (next_fb = 1) then to Eval21_btn10 end;
		if (next_fb = 2) then to land_btn11 end;
		to error

	from fail_btn8
		wait [0,0];
		btnode[fail_btn8].caller := caller_Fallback15_btn7;
		to fail_btn8_done

	from fail_btn8_done
		wait [0,0];
		on (btnode[fail_btn8].caller = None);
		if (btnode[fail_btn8].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[fail_btn8].rstatus = failure) then
			to Eval21_btn10
		elsif (btnode[fail_btn8].rstatus = running) then
			next_fb := 0;
			to running
		else
			to error
		end

	from Eval21_btn10
		wait [0,0];
		btnode[Eval21_btn10].caller := caller_Fallback15_btn7;
		to Eval21_btn10_done

	from Eval21_btn10_done
		wait [0,0];
		on (btnode[Eval21_btn10].caller = None);
		if (btnode[Eval21_btn10].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[Eval21_btn10].rstatus = failure) then
			to land_btn11
		elsif (btnode[Eval21_btn10].rstatus = running) then
			next_fb := 1;
			to running
		else
			to error
		end

	from land_btn11
		wait [0,0];
		btnode[land_btn11].caller := caller_Fallback15_btn7;
		to land_btn11_done

	from land_btn11_done
		wait [0,0];
		on (btnode[land_btn11].caller = None);
		if (btnode[land_btn11].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[land_btn11].rstatus = failure) then
			next_fb := 0;
			to failure
		elsif (btnode[land_btn11].rstatus = running) then
			next_fb := 2;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Fallback15_btn7].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Fallback15_btn7].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Fallback15_btn7].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Fallback15_btn7].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Fallback15_btn7].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Eval25_btn12 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (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 (not (battery = Critical)) 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];
		btnode[Eval25_btn12].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[Eval25_btn12].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Eval29_btn14 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[Eval29_btn14].caller = None));
		if (btnode[Eval29_btn14].rstatus = halt_me) then to halt end;
		btnode[Eval29_btn14].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		if (battery = Good) then
			to success
		else
			to failure
		end

	from success
		wait [0,0];
		btnode[Eval29_btn14].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Eval29_btn14].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Eval29_btn14].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[Eval29_btn14].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn15 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn15].caller = None));
		if (btnode[goto_waypoint_btn15].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn15].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn15].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn15].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn15].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn15].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn15].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Fallback27_btn13 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Eval29_btn14, Eval29_btn14_done,
		goto_waypoint_btn15, goto_waypoint_btn15_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_fb:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Fallback27_btn13].caller = None));
		if (btnode[Fallback27_btn13].rstatus = halt_me) then to halt end;
		btnode[Fallback27_btn13].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[Eval29_btn14].rstatus = running) then
			btnode[Eval29_btn14].rstatus := halt_me;
			btnode[Eval29_btn14].caller := caller_Fallback27_btn13;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn15].rstatus = running) then
			btnode[goto_waypoint_btn15].rstatus := halt_me;
			btnode[goto_waypoint_btn15].caller := caller_Fallback27_btn13;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[Eval29_btn14].caller = None) and
			(btnode[goto_waypoint_btn15].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_fb = 0) then to Eval29_btn14 end;
		if (next_fb = 1) then to goto_waypoint_btn15 end;
		to error

	from Eval29_btn14
		wait [0,0];
		btnode[Eval29_btn14].caller := caller_Fallback27_btn13;
		to Eval29_btn14_done

	from Eval29_btn14_done
		wait [0,0];
		on (btnode[Eval29_btn14].caller = None);
		if (btnode[Eval29_btn14].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[Eval29_btn14].rstatus = failure) then
			to goto_waypoint_btn15
		elsif (btnode[Eval29_btn14].rstatus = running) then
			next_fb := 0;
			to running
		else
			to error
		end

	from goto_waypoint_btn15
		wait [0,0];
		btnode[goto_waypoint_btn15].caller := caller_Fallback27_btn13;
		to goto_waypoint_btn15_done

	from goto_waypoint_btn15_done
		wait [0,0];
		on (btnode[goto_waypoint_btn15].caller = None);
		if (btnode[goto_waypoint_btn15].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[goto_waypoint_btn15].rstatus = failure) then
			next_fb := 0;
			to failure
		elsif (btnode[goto_waypoint_btn15].rstatus = running) then
			next_fb := 1;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Fallback27_btn13].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Fallback27_btn13].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Fallback27_btn13].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Fallback27_btn13].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Fallback27_btn13].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Sequence13_btn6 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Fallback15_btn7, Fallback15_btn7_done,
		Eval25_btn12, Eval25_btn12_done,
		Fallback27_btn13, Fallback27_btn13_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Sequence13_btn6].caller = None));
		if (btnode[Sequence13_btn6].rstatus = halt_me) then to halt end;
		btnode[Sequence13_btn6].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[Fallback15_btn7].rstatus = running) then
			btnode[Fallback15_btn7].rstatus := halt_me;
			btnode[Fallback15_btn7].caller := caller_Sequence13_btn6;
			to halt_wait
		end;
		if (btnode[Eval25_btn12].rstatus = running) then
			btnode[Eval25_btn12].rstatus := halt_me;
			btnode[Eval25_btn12].caller := caller_Sequence13_btn6;
			to halt_wait
		end;
		if (btnode[Fallback27_btn13].rstatus = running) then
			btnode[Fallback27_btn13].rstatus := halt_me;
			btnode[Fallback27_btn13].caller := caller_Sequence13_btn6;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[Fallback15_btn7].caller = None) and
			(btnode[Eval25_btn12].caller = None) and
			(btnode[Fallback27_btn13].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_seq = 0) then to Fallback15_btn7 end;
		if (next_seq = 1) then to Eval25_btn12 end;
		if (next_seq = 2) then to Fallback27_btn13 end;
		to error

	from Fallback15_btn7
		wait [0,0];
		btnode[Fallback15_btn7].caller := caller_Sequence13_btn6;
		to Fallback15_btn7_done

	from Fallback15_btn7_done
		wait [0,0];
		on (btnode[Fallback15_btn7].caller = None);
		if (btnode[Fallback15_btn7].rstatus = success) then
			to Eval25_btn12
		elsif (btnode[Fallback15_btn7].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Fallback15_btn7].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from Eval25_btn12
		wait [0,0];
		btnode[Eval25_btn12].caller := caller_Sequence13_btn6;
		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 Fallback27_btn13
		elsif (btnode[Eval25_btn12].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Eval25_btn12].rstatus = running) then
			next_seq := 1;
			to running
		else
			to error
		end

	from Fallback27_btn13
		wait [0,0];
		btnode[Fallback27_btn13].caller := caller_Sequence13_btn6;
		to Fallback27_btn13_done

	from Fallback27_btn13_done
		wait [0,0];
		on (btnode[Fallback27_btn13].caller = None);
		if (btnode[Fallback27_btn13].rstatus = success) then
			next_seq := 0;
			to success
		elsif (btnode[Fallback27_btn13].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Fallback27_btn13].rstatus = running) then
			next_seq := 2;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Sequence13_btn6].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Sequence13_btn6].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Sequence13_btn6].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Sequence13_btn6].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Sequence13_btn6].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_localization_ok_btn17 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[localization_ok_btn17].caller = None));
		if (btnode[localization_ok_btn17].rstatus = halt_me) then to halt end;
		btnode[localization_ok_btn17].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		end

	from success
		wait [0,0];
		btnode[localization_ok_btn17].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[localization_ok_btn17].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[localization_ok_btn17].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[localization_ok_btn17].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_land_btn19 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[land_btn19].caller = None));
		if (btnode[land_btn19].rstatus = halt_me) then to halt end;
		btnode[land_btn19].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[land_btn19].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[land_btn19].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[land_btn19].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[land_btn19].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[land_btn19].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_fail_btn18 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		land_btn19, land_btn19_done,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[fail_btn18].caller = None));
		if (btnode[fail_btn18].rstatus = halt_me) then to halt end;
		btnode[fail_btn18].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[land_btn19].rstatus = running) then
			btnode[land_btn19].rstatus := halt_me;
			btnode[land_btn19].caller := caller_fail_btn18;
		to halt_wait
		end;
		to halted

	from halt_wait
			on (btnode[land_btn19].caller = None);

	to halted

	from tick_node
		wait [0,0];
	to land_btn19

	from land_btn19
		wait [0,0];
		btnode[land_btn19].caller := caller_fail_btn18;
		to land_btn19_done

	from land_btn19_done
		wait [0,0];
		on (btnode[land_btn19].caller = None);
		if (btnode[land_btn19].rstatus = success) then
			to failure
		elsif (btnode[land_btn19].rstatus = failure) then
			to failure
		elsif (btnode[land_btn19].rstatus = running) then
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[fail_btn18].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[fail_btn18].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[fail_btn18].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[fail_btn18].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[fail_btn18].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Fallback33_btn16 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		localization_ok_btn17, localization_ok_btn17_done,
		fail_btn18, fail_btn18_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_fb:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Fallback33_btn16].caller = None));
		if (btnode[Fallback33_btn16].rstatus = halt_me) then to halt end;
		btnode[Fallback33_btn16].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[localization_ok_btn17].rstatus = running) then
			btnode[localization_ok_btn17].rstatus := halt_me;
			btnode[localization_ok_btn17].caller := caller_Fallback33_btn16;
			to halt_wait
		end;
		if (btnode[fail_btn18].rstatus = running) then
			btnode[fail_btn18].rstatus := halt_me;
			btnode[fail_btn18].caller := caller_Fallback33_btn16;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[localization_ok_btn17].caller = None) and
			(btnode[fail_btn18].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_fb = 0) then to localization_ok_btn17 end;
		if (next_fb = 1) then to fail_btn18 end;
		to error

	from localization_ok_btn17
		wait [0,0];
		btnode[localization_ok_btn17].caller := caller_Fallback33_btn16;
		to localization_ok_btn17_done

	from localization_ok_btn17_done
		wait [0,0];
		on (btnode[localization_ok_btn17].caller = None);
		if (btnode[localization_ok_btn17].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[localization_ok_btn17].rstatus = failure) then
			to fail_btn18
		elsif (btnode[localization_ok_btn17].rstatus = running) then
			next_fb := 0;
			to running
		else
			to error
		end

	from fail_btn18
		wait [0,0];
		btnode[fail_btn18].caller := caller_Fallback33_btn16;
		to fail_btn18_done

	from fail_btn18_done
		wait [0,0];
		on (btnode[fail_btn18].caller = None);
		if (btnode[fail_btn18].rstatus = success) then
			next_fb := 0;
			to success
		elsif (btnode[fail_btn18].rstatus = failure) then
			next_fb := 0;
			to failure
		elsif (btnode[fail_btn18].rstatus = running) then
			next_fb := 1;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Fallback33_btn16].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Fallback33_btn16].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Fallback33_btn16].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Fallback33_btn16].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Fallback33_btn16].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_takeoff_btn21 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[takeoff_btn21].caller = None));
		if (btnode[takeoff_btn21].rstatus = halt_me) then to halt end;
		btnode[takeoff_btn21].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[takeoff_btn21].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[takeoff_btn21].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[takeoff_btn21].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[takeoff_btn21].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[takeoff_btn21].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_camera_tracking_camera_track (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[camera_tracking_camera_track].caller = None));
		if (btnode[camera_tracking_camera_track].rstatus = halt_me) then to halt end;
		btnode[camera_tracking_camera_track].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[camera_tracking_camera_track].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[camera_tracking_camera_track].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[camera_tracking_camera_track].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[camera_tracking_camera_track].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[camera_tracking_camera_track].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Eval53_btn26 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[Eval53_btn26].caller = None));
		if (btnode[Eval53_btn26].rstatus = halt_me) then to halt end;
		btnode[Eval53_btn26].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		// will assign: fls := (1 + fls)
		fls := (1 + fls);
		to success

	from success
		wait [0,0];
		btnode[Eval53_btn26].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Eval53_btn26].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Eval53_btn26].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[Eval53_btn26].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn27 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn27].caller = None));
		if (btnode[goto_waypoint_btn27].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn27].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn27].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn27].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn27].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn27].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn27].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn28 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn28].caller = None));
		if (btnode[goto_waypoint_btn28].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn28].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn28].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn28].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn28].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn28].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn28].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn29 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn29].caller = None));
		if (btnode[goto_waypoint_btn29].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn29].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn29].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn29].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn29].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn29].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn29].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn30 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn30].caller = None));
		if (btnode[goto_waypoint_btn30].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn30].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn30].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn30].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn30].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn30].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn30].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn31 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn31].caller = None));
		if (btnode[goto_waypoint_btn31].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn31].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn31].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn31].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn31].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn31].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn31].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn32 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn32].caller = None));
		if (btnode[goto_waypoint_btn32].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn32].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn32].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn32].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn32].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn32].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn32].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Sequence51_btn25 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Eval53_btn26, Eval53_btn26_done,
		goto_waypoint_btn27, goto_waypoint_btn27_done,
		goto_waypoint_btn28, goto_waypoint_btn28_done,
		goto_waypoint_btn29, goto_waypoint_btn29_done,
		goto_waypoint_btn30, goto_waypoint_btn30_done,
		goto_waypoint_btn31, goto_waypoint_btn31_done,
		goto_waypoint_btn32, goto_waypoint_btn32_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Sequence51_btn25].caller = None));
		if (btnode[Sequence51_btn25].rstatus = halt_me) then to halt end;
		btnode[Sequence51_btn25].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[Eval53_btn26].rstatus = running) then
			btnode[Eval53_btn26].rstatus := halt_me;
			btnode[Eval53_btn26].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn27].rstatus = running) then
			btnode[goto_waypoint_btn27].rstatus := halt_me;
			btnode[goto_waypoint_btn27].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn28].rstatus = running) then
			btnode[goto_waypoint_btn28].rstatus := halt_me;
			btnode[goto_waypoint_btn28].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn29].rstatus = running) then
			btnode[goto_waypoint_btn29].rstatus := halt_me;
			btnode[goto_waypoint_btn29].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn30].rstatus = running) then
			btnode[goto_waypoint_btn30].rstatus := halt_me;
			btnode[goto_waypoint_btn30].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn31].rstatus = running) then
			btnode[goto_waypoint_btn31].rstatus := halt_me;
			btnode[goto_waypoint_btn31].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn32].rstatus = running) then
			btnode[goto_waypoint_btn32].rstatus := halt_me;
			btnode[goto_waypoint_btn32].caller := caller_Sequence51_btn25;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[Eval53_btn26].caller = None) and
			(btnode[goto_waypoint_btn27].caller = None) and
			(btnode[goto_waypoint_btn28].caller = None) and
			(btnode[goto_waypoint_btn29].caller = None) and
			(btnode[goto_waypoint_btn30].caller = None) and
			(btnode[goto_waypoint_btn31].caller = None) and
			(btnode[goto_waypoint_btn32].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_seq = 0) then to Eval53_btn26 end;
		if (next_seq = 1) then to goto_waypoint_btn27 end;
		if (next_seq = 2) then to goto_waypoint_btn28 end;
		if (next_seq = 3) then to goto_waypoint_btn29 end;
		if (next_seq = 4) then to goto_waypoint_btn30 end;
		if (next_seq = 5) then to goto_waypoint_btn31 end;
		if (next_seq = 6) then to goto_waypoint_btn32 end;
		to error

	from Eval53_btn26
		wait [0,0];
		btnode[Eval53_btn26].caller := caller_Sequence51_btn25;
		to Eval53_btn26_done

	from Eval53_btn26_done
		wait [0,0];
		on (btnode[Eval53_btn26].caller = None);
		if (btnode[Eval53_btn26].rstatus = success) then
			to goto_waypoint_btn27
		elsif (btnode[Eval53_btn26].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Eval53_btn26].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from goto_waypoint_btn27
		wait [0,0];
		btnode[goto_waypoint_btn27].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn27_done

	from goto_waypoint_btn27_done
		wait [0,0];
		on (btnode[goto_waypoint_btn27].caller = None);
		if (btnode[goto_waypoint_btn27].rstatus = success) then
			to goto_waypoint_btn28
		elsif (btnode[goto_waypoint_btn27].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn27].rstatus = running) then
			next_seq := 1;
			to running
		else
			to error
		end

	from goto_waypoint_btn28
		wait [0,0];
		btnode[goto_waypoint_btn28].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn28_done

	from goto_waypoint_btn28_done
		wait [0,0];
		on (btnode[goto_waypoint_btn28].caller = None);
		if (btnode[goto_waypoint_btn28].rstatus = success) then
			to goto_waypoint_btn29
		elsif (btnode[goto_waypoint_btn28].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn28].rstatus = running) then
			next_seq := 2;
			to running
		else
			to error
		end

	from goto_waypoint_btn29
		wait [0,0];
		btnode[goto_waypoint_btn29].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn29_done

	from goto_waypoint_btn29_done
		wait [0,0];
		on (btnode[goto_waypoint_btn29].caller = None);
		if (btnode[goto_waypoint_btn29].rstatus = success) then
			to goto_waypoint_btn30
		elsif (btnode[goto_waypoint_btn29].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn29].rstatus = running) then
			next_seq := 3;
			to running
		else
			to error
		end

	from goto_waypoint_btn30
		wait [0,0];
		btnode[goto_waypoint_btn30].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn30_done

	from goto_waypoint_btn30_done
		wait [0,0];
		on (btnode[goto_waypoint_btn30].caller = None);
		if (btnode[goto_waypoint_btn30].rstatus = success) then
			to goto_waypoint_btn31
		elsif (btnode[goto_waypoint_btn30].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn30].rstatus = running) then
			next_seq := 4;
			to running
		else
			to error
		end

	from goto_waypoint_btn31
		wait [0,0];
		btnode[goto_waypoint_btn31].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn31_done

	from goto_waypoint_btn31_done
		wait [0,0];
		on (btnode[goto_waypoint_btn31].caller = None);
		if (btnode[goto_waypoint_btn31].rstatus = success) then
			to goto_waypoint_btn32
		elsif (btnode[goto_waypoint_btn31].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn31].rstatus = running) then
			next_seq := 5;
			to running
		else
			to error
		end

	from goto_waypoint_btn32
		wait [0,0];
		btnode[goto_waypoint_btn32].caller := caller_Sequence51_btn25;
		to goto_waypoint_btn32_done

	from goto_waypoint_btn32_done
		wait [0,0];
		on (btnode[goto_waypoint_btn32].caller = None);
		if (btnode[goto_waypoint_btn32].rstatus = success) then
			next_seq := 0;
			to success
		elsif (btnode[goto_waypoint_btn32].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn32].rstatus = running) then
			next_seq := 6;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Sequence51_btn25].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Sequence51_btn25].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Sequence51_btn25].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Sequence51_btn25].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Sequence51_btn25].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Repeat49_btn24 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Sequence51_btn25, Sequence51_btn25_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		rep:nat := 0, repeat: nat := 3

	from start_
		wait [0,0];
		on (not (btnode[Repeat49_btn24].caller = None));
		if (btnode[Repeat49_btn24].rstatus = halt_me) then to halt end;
		btnode[Repeat49_btn24].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[Sequence51_btn25].rstatus = running) then
			btnode[Sequence51_btn25].rstatus := halt_me;
			btnode[Sequence51_btn25].caller := caller_Repeat49_btn24;
		to halt_wait
		end;
		to halted

	from halt_wait
			on (btnode[Sequence51_btn25].caller = None);

	to halted

	from tick_node
		wait [0,0];
	to Sequence51_btn25

	from Sequence51_btn25
		wait [0,0];
		btnode[Sequence51_btn25].caller := caller_Repeat49_btn24;
		to Sequence51_btn25_done

	from Sequence51_btn25_done
		wait [0,0];
		on (btnode[Sequence51_btn25].caller = None);
		if (btnode[Sequence51_btn25].rstatus = success) then
			rep := rep + 1 ;
			if (rep = repeat) then
				rep := 0;
				to success
			end;
			to tick_node
		elsif (btnode[Sequence51_btn25].rstatus = failure) then
			rep := 0;
			to failure
		elsif (btnode[Sequence51_btn25].rstatus = running) then
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Repeat49_btn24].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Repeat49_btn24].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Repeat49_btn24].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Repeat49_btn24].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Repeat49_btn24].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Parallel45_btn22 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait,
		running, Parallel45_btn22_par, Parallel45_btn22_par_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		success_so_far:nat := 0, failed_so_far:nat := 0,
		runningb:bool := false,
		halt_called_by_me:bool := false,
		force_success:bool := false

	from start_
		wait [0,0];
		on (not (btnode[Parallel45_btn22].caller = None));
		if (btnode[Parallel45_btn22].rstatus = halt_me) then to halt end;
		btnode[Parallel45_btn22].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[camera_tracking_camera_track].rstatus = running) then
			btnode[camera_tracking_camera_track].rstatus := halt_me;
			btnode[camera_tracking_camera_track].caller := caller_Parallel45_btn22
		end;
		if (btnode[Repeat49_btn24].rstatus = running) then
			btnode[Repeat49_btn24].rstatus := halt_me;
			btnode[Repeat49_btn24].caller := caller_Parallel45_btn22
		end;
		to halt_wait

	from halt_wait
		on (
			(btnode[camera_tracking_camera_track].caller = None) and
			(btnode[Repeat49_btn24].caller = None) and
			true);

	to halted

	from tick_node
		wait [0,0];
	to Parallel45_btn22_par

	from Parallel45_btn22_par
		wait [0,0];
		if (runningb) then
			if (btnode[camera_tracking_camera_track].rstatus = running) then
				btnode[camera_tracking_camera_track].caller := caller_Parallel45_btn22
			end;
			if (btnode[Repeat49_btn24].rstatus = running) then
				btnode[Repeat49_btn24].caller := caller_Parallel45_btn22
			end;
			null
		else
			btnode[camera_tracking_camera_track].caller := caller_Parallel45_btn22;
			btnode[Repeat49_btn24].caller := caller_Parallel45_btn22;
			null
		end;
		to Parallel45_btn22_par_done

	from Parallel45_btn22_par_done
		wait [0,0];
		on (
			(btnode[camera_tracking_camera_track].caller = None) and
			(btnode[Repeat49_btn24].caller = None) and
			true);
		success_so_far := 0; failed_so_far := 0;
		if (btnode[camera_tracking_camera_track].rstatus = success) then success_so_far := success_so_far + 1
		elsif (btnode[camera_tracking_camera_track].rstatus = failure) then failed_so_far := failed_so_far + 1 end; 
		if (btnode[Repeat49_btn24].rstatus = success) then success_so_far := success_so_far + 1
		elsif (btnode[Repeat49_btn24].rstatus = failure) then failed_so_far := failed_so_far + 1 end; 
		if (success_so_far >= 1) then
			halt_called_by_me := true;
			force_success := true;
			to halt
		elsif (failed_so_far > 1) then
			to failure
		else
				runningb := true;
			to running
		end

	from success
		wait [0,0];
		btnode[Parallel45_btn22].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Parallel45_btn22].rstatus := failure;
		to done

	from halted
		wait [0,0];
		if (halt_called_by_me) then
			if (force_success) then
				btnode[Parallel45_btn22].rstatus := success
			else
				btnode[Parallel45_btn22].rstatus := failure
			end
		else
			btnode[Parallel45_btn22].rstatus := failure
		end;
		halt_called_by_me := false;
		force_success := false;
		to done

	from running
		wait [0,0];
		btnode[Parallel45_btn22].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Parallel45_btn22].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn33 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[goto_waypoint_btn33].caller = None));
		if (btnode[goto_waypoint_btn33].rstatus = halt_me) then to halt end;
		btnode[goto_waypoint_btn33].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[goto_waypoint_btn33].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[goto_waypoint_btn33].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[goto_waypoint_btn33].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[goto_waypoint_btn33].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[goto_waypoint_btn33].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_land_btn34 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[land_btn34].caller = None));
		if (btnode[land_btn34].rstatus = halt_me) then to halt end;
		btnode[land_btn34].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[land_btn34].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[land_btn34].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[land_btn34].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[land_btn34].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[land_btn34].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_shutdown_drone_btn35 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, running,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[shutdown_drone_btn35].caller = None));
		if (btnode[shutdown_drone_btn35].rstatus = halt_me) then to halt end;
		btnode[shutdown_drone_btn35].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		select
			to success
		[]
			to failure
		[]
			to running
		end

	from success
		wait [0,0];
		btnode[shutdown_drone_btn35].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[shutdown_drone_btn35].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[shutdown_drone_btn35].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[shutdown_drone_btn35].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[shutdown_drone_btn35].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Eval73_btn36 (&btnode: btnode_array, &fls: sv_fls, &localization_status: sv_localization_status, &battery: sv_battery) is

	states start_, tick_node, success, failure, halt, halted, error,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[Eval73_btn36].caller = None));
		if (btnode[Eval73_btn36].rstatus = halt_me) then to halt end;
		btnode[Eval73_btn36].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
		if (btnode[camera_tracking_camera_track].rstatus = success) then
			to success
		else
			to failure
		end

	from success
		wait [0,0];
		btnode[Eval73_btn36].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Eval73_btn36].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Eval73_btn36].rstatus := failure;
		to done

	from done
		wait [0,0];
		btnode[Eval73_btn36].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Sequence41_btn20 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		takeoff_btn21, takeoff_btn21_done,
		Parallel45_btn22, Parallel45_btn22_done,
		goto_waypoint_btn33, goto_waypoint_btn33_done,
		land_btn34, land_btn34_done,
		shutdown_drone_btn35, shutdown_drone_btn35_done,
		Eval73_btn36, Eval73_btn36_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Sequence41_btn20].caller = None));
		if (btnode[Sequence41_btn20].rstatus = halt_me) then to halt end;
		btnode[Sequence41_btn20].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[takeoff_btn21].rstatus = running) then
			btnode[takeoff_btn21].rstatus := halt_me;
			btnode[takeoff_btn21].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		if (btnode[Parallel45_btn22].rstatus = running) then
			btnode[Parallel45_btn22].rstatus := halt_me;
			btnode[Parallel45_btn22].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn33].rstatus = running) then
			btnode[goto_waypoint_btn33].rstatus := halt_me;
			btnode[goto_waypoint_btn33].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		if (btnode[land_btn34].rstatus = running) then
			btnode[land_btn34].rstatus := halt_me;
			btnode[land_btn34].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		if (btnode[shutdown_drone_btn35].rstatus = running) then
			btnode[shutdown_drone_btn35].rstatus := halt_me;
			btnode[shutdown_drone_btn35].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		if (btnode[Eval73_btn36].rstatus = running) then
			btnode[Eval73_btn36].rstatus := halt_me;
			btnode[Eval73_btn36].caller := caller_Sequence41_btn20;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[takeoff_btn21].caller = None) and
			(btnode[Parallel45_btn22].caller = None) and
			(btnode[goto_waypoint_btn33].caller = None) and
			(btnode[land_btn34].caller = None) and
			(btnode[shutdown_drone_btn35].caller = None) and
			(btnode[Eval73_btn36].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_seq = 0) then to takeoff_btn21 end;
		if (next_seq = 1) then to Parallel45_btn22 end;
		if (next_seq = 2) then to goto_waypoint_btn33 end;
		if (next_seq = 3) then to land_btn34 end;
		if (next_seq = 4) then to shutdown_drone_btn35 end;
		if (next_seq = 5) then to Eval73_btn36 end;
		to error

	from takeoff_btn21
		wait [0,0];
		btnode[takeoff_btn21].caller := caller_Sequence41_btn20;
		to takeoff_btn21_done

	from takeoff_btn21_done
		wait [0,0];
		on (btnode[takeoff_btn21].caller = None);
		if (btnode[takeoff_btn21].rstatus = success) then
			to Parallel45_btn22
		elsif (btnode[takeoff_btn21].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[takeoff_btn21].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from Parallel45_btn22
		wait [0,0];
		btnode[Parallel45_btn22].caller := caller_Sequence41_btn20;
		to Parallel45_btn22_done

	from Parallel45_btn22_done
		wait [0,0];
		on (btnode[Parallel45_btn22].caller = None);
		if (btnode[Parallel45_btn22].rstatus = success) then
			to goto_waypoint_btn33
		elsif (btnode[Parallel45_btn22].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Parallel45_btn22].rstatus = running) then
			next_seq := 1;
			to running
		else
			to error
		end

	from goto_waypoint_btn33
		wait [0,0];
		btnode[goto_waypoint_btn33].caller := caller_Sequence41_btn20;
		to goto_waypoint_btn33_done

	from goto_waypoint_btn33_done
		wait [0,0];
		on (btnode[goto_waypoint_btn33].caller = None);
		if (btnode[goto_waypoint_btn33].rstatus = success) then
			to land_btn34
		elsif (btnode[goto_waypoint_btn33].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[goto_waypoint_btn33].rstatus = running) then
			next_seq := 2;
			to running
		else
			to error
		end

	from land_btn34
		wait [0,0];
		btnode[land_btn34].caller := caller_Sequence41_btn20;
		to land_btn34_done

	from land_btn34_done
		wait [0,0];
		on (btnode[land_btn34].caller = None);
		if (btnode[land_btn34].rstatus = success) then
			to shutdown_drone_btn35
		elsif (btnode[land_btn34].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[land_btn34].rstatus = running) then
			next_seq := 3;
			to running
		else
			to error
		end

	from shutdown_drone_btn35
		wait [0,0];
		btnode[shutdown_drone_btn35].caller := caller_Sequence41_btn20;
		to shutdown_drone_btn35_done

	from shutdown_drone_btn35_done
		wait [0,0];
		on (btnode[shutdown_drone_btn35].caller = None);
		if (btnode[shutdown_drone_btn35].rstatus = success) then
			to Eval73_btn36
		elsif (btnode[shutdown_drone_btn35].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[shutdown_drone_btn35].rstatus = running) then
			next_seq := 4;
			to running
		else
			to error
		end

	from Eval73_btn36
		wait [0,0];
		btnode[Eval73_btn36].caller := caller_Sequence41_btn20;
		to Eval73_btn36_done

	from Eval73_btn36_done
		wait [0,0];
		on (btnode[Eval73_btn36].caller = None);
		if (btnode[Eval73_btn36].rstatus = success) then
			next_seq := 0;
			to success
		elsif (btnode[Eval73_btn36].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[Eval73_btn36].rstatus = running) then
			next_seq := 5;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Sequence41_btn20].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Sequence41_btn20].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Sequence41_btn20].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Sequence41_btn20].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Sequence41_btn20].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_ReactiveSequence11_btn5 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Sequence13_btn6, Sequence13_btn6_done,
		Fallback33_btn16, Fallback33_btn16_done,
		Sequence41_btn20, Sequence41_btn20_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		runningb:bool := false,
		halt_called_by_me:bool := false,
		force_success:bool := false,
		next_seq:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[ReactiveSequence11_btn5].caller = None));
		if (btnode[ReactiveSequence11_btn5].rstatus = halt_me) then to halt end;
		btnode[ReactiveSequence11_btn5].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[Sequence13_btn6].rstatus = running) then
			btnode[Sequence13_btn6].rstatus := halt_me;
			btnode[Sequence13_btn6].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		if (btnode[Fallback33_btn16].rstatus = running) then
			btnode[Fallback33_btn16].rstatus := halt_me;
			btnode[Fallback33_btn16].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		if (btnode[Sequence41_btn20].rstatus = running) then
			btnode[Sequence41_btn20].rstatus := halt_me;
			btnode[Sequence41_btn20].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[Sequence13_btn6].caller = None) and
			(btnode[Fallback33_btn16].caller = None) and
			(btnode[Sequence41_btn20].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_seq = 0) then to Sequence13_btn6 end;
		if (next_seq = 1) then to Fallback33_btn16 end;
		if (next_seq = 2) then to Sequence41_btn20 end;
		to error

	from Sequence13_btn6
		wait [0,0];
		btnode[Sequence13_btn6].caller := caller_ReactiveSequence11_btn5;
		to Sequence13_btn6_done

	from Sequence13_btn6_done
		wait [0,0];
		on (btnode[Sequence13_btn6].caller = None);
		if (btnode[Sequence13_btn6].rstatus = success) then
			to Fallback33_btn16
		elsif (btnode[Sequence13_btn6].rstatus = failure) then
			next_seq := 0;
			halt_called_by_me := true;
			to halt
		elsif (btnode[Sequence13_btn6].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from Fallback33_btn16
		wait [0,0];
		btnode[Fallback33_btn16].caller := caller_ReactiveSequence11_btn5;
		to Fallback33_btn16_done

	from Fallback33_btn16_done
		wait [0,0];
		on (btnode[Fallback33_btn16].caller = None);
		if (btnode[Fallback33_btn16].rstatus = success) then
			to Sequence41_btn20
		elsif (btnode[Fallback33_btn16].rstatus = failure) then
			next_seq := 0;
			halt_called_by_me := true;
			to halt
		elsif (btnode[Fallback33_btn16].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from Sequence41_btn20
		wait [0,0];
		btnode[Sequence41_btn20].caller := caller_ReactiveSequence11_btn5;
		to Sequence41_btn20_done

	from Sequence41_btn20_done
		wait [0,0];
		on (btnode[Sequence41_btn20].caller = None);
		if (btnode[Sequence41_btn20].rstatus = success) then
			next_seq := 0;
			to success
		elsif (btnode[Sequence41_btn20].rstatus = failure) then
			next_seq := 0;
			halt_called_by_me := true;
			to halt
		elsif (btnode[Sequence41_btn20].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[ReactiveSequence11_btn5].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[ReactiveSequence11_btn5].rstatus := failure;
		to done

	from halted
		wait [0,0];
		if (halt_called_by_me) then
			if (force_success) then
				btnode[ReactiveSequence11_btn5].rstatus := success
			else
				btnode[ReactiveSequence11_btn5].rstatus := failure
			end
		else
			btnode[ReactiveSequence11_btn5].rstatus := failure
		end;
		halt_called_by_me := false;
		force_success := false;
		to done

	from running
		wait [0,0];
		btnode[ReactiveSequence11_btn5].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[ReactiveSequence11_btn5].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_Sequence3_btn1 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		ParallelAll5_btn2, ParallelAll5_btn2_done,
		ReactiveSequence11_btn5, ReactiveSequence11_btn5_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq:nat := 0

	from start_
		wait [0,0];
		on (not (btnode[Sequence3_btn1].caller = None));
		if (btnode[Sequence3_btn1].rstatus = halt_me) then to halt end;
		btnode[Sequence3_btn1].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];
		if (btnode[ParallelAll5_btn2].rstatus = running) then
			btnode[ParallelAll5_btn2].rstatus := halt_me;
			btnode[ParallelAll5_btn2].caller := caller_Sequence3_btn1;
			to halt_wait
		end;
		if (btnode[ReactiveSequence11_btn5].rstatus = running) then
			btnode[ReactiveSequence11_btn5].rstatus := halt_me;
			btnode[ReactiveSequence11_btn5].caller := caller_Sequence3_btn1;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[ParallelAll5_btn2].caller = None) and
			(btnode[ReactiveSequence11_btn5].caller = None) and
			true);
		to halted

	from tick_node
		wait [0,0];
		if (next_seq = 0) then to ParallelAll5_btn2 end;
		if (next_seq = 1) then to ReactiveSequence11_btn5 end;
		to error

	from ParallelAll5_btn2
		wait [0,0];
		btnode[ParallelAll5_btn2].caller := caller_Sequence3_btn1;
		to ParallelAll5_btn2_done

	from ParallelAll5_btn2_done
		wait [0,0];
		on (btnode[ParallelAll5_btn2].caller = None);
		if (btnode[ParallelAll5_btn2].rstatus = success) then
			to ReactiveSequence11_btn5
		elsif (btnode[ParallelAll5_btn2].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[ParallelAll5_btn2].rstatus = running) then
			next_seq := 0;
			to running
		else
			to error
		end

	from ReactiveSequence11_btn5
		wait [0,0];
		btnode[ReactiveSequence11_btn5].caller := caller_Sequence3_btn1;
		to ReactiveSequence11_btn5_done

	from ReactiveSequence11_btn5_done
		wait [0,0];
		on (btnode[ReactiveSequence11_btn5].caller = None);
		if (btnode[ReactiveSequence11_btn5].rstatus = success) then
			next_seq := 0;
			to success
		elsif (btnode[ReactiveSequence11_btn5].rstatus = failure) then
			next_seq := 0;
			to failure
		elsif (btnode[ReactiveSequence11_btn5].rstatus = running) then
			next_seq := 1;
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[Sequence3_btn1].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[Sequence3_btn1].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[Sequence3_btn1].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[Sequence3_btn1].rstatus := running;
		to done

	from done
		wait [0,0];
		btnode[Sequence3_btn1].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_BehaviorTree1_drone (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, running, error,
		Sequence3_btn1, Sequence3_btn1_done,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (not (btnode[BehaviorTree1_drone].caller = None));
		if (btnode[BehaviorTree1_drone].rstatus = halt_me) then to halt end;
		btnode[BehaviorTree1_drone].rstatus := no_ret_status;
	to tick_node

	from halt
		wait [0,0];

	to halted

	from tick_node
		wait [1,1];
	to Sequence3_btn1

	from Sequence3_btn1
		wait [0,0];
		btnode[Sequence3_btn1].caller := caller_BehaviorTree1_drone;
		to Sequence3_btn1_done

	from Sequence3_btn1_done
		wait [0,0];
		on (btnode[Sequence3_btn1].caller = None);
		if (btnode[Sequence3_btn1].rstatus = success) then
			to success
		elsif (btnode[Sequence3_btn1].rstatus = failure) then
			to failure
		elsif (btnode[Sequence3_btn1].rstatus = running) then
			to running
		else
			to error
		end

	from success
		wait [0,0];
		btnode[BehaviorTree1_drone].rstatus := success;
		to done

	from failure
		wait [0,0];
		btnode[BehaviorTree1_drone].rstatus := failure;
		to done

	from halted
		wait [0,0];
		btnode[BehaviorTree1_drone].rstatus := failure;
		to done

	from running
		wait [0,0];
		btnode[BehaviorTree1_drone].rstatus := running;
		to tick_node

	from done
		wait [0,0];
		btnode[BehaviorTree1_drone].caller := None;
	to ether

component drone 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 = 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 = 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_BehaviorTree1_drone, ArgIndex = 0, rstatus = no_ret_status}],
		// **** state variables ****,
		fls: sv_fls := 0,
		localization_status: sv_localization_status := Invalid,
		battery: sv_battery := Good

par * in
// **** state variables processes ****
   sv_localization_status_automata(&localization_status)
|| sv_battery_automata(&battery)
// **** btnode processes ****
|| btnode_start_drone_btn3(&btnode, &fls, &localization_status, &battery)
|| btnode_start_camera_btn4(&btnode, &fls, &localization_status, &battery)
|| btnode_ParallelAll5_btn2(&btnode)
|| btnode_measure_battery_btn9(&btnode, &fls, &localization_status, &battery)
|| btnode_fail_btn8(&btnode)
|| btnode_Eval21_btn10(&btnode, &fls, &localization_status, &battery)
|| btnode_land_btn11(&btnode, &fls, &localization_status, &battery)
|| btnode_Fallback15_btn7(&btnode)
|| btnode_Eval25_btn12(&btnode, &fls, &localization_status, &battery)
|| btnode_Eval29_btn14(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn15(&btnode, &fls, &localization_status, &battery)
|| btnode_Fallback27_btn13(&btnode)
|| btnode_Sequence13_btn6(&btnode)
|| btnode_localization_ok_btn17(&btnode, &fls, &localization_status, &battery)
|| btnode_land_btn19(&btnode, &fls, &localization_status, &battery)
|| btnode_fail_btn18(&btnode)
|| btnode_Fallback33_btn16(&btnode)
|| btnode_takeoff_btn21(&btnode, &fls, &localization_status, &battery)
|| btnode_camera_tracking_camera_track(&btnode, &fls, &localization_status, &battery)
|| btnode_Eval53_btn26(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn27(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn28(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn29(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn30(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn31(&btnode, &fls, &localization_status, &battery)
|| btnode_goto_waypoint_btn32(&btnode, &fls, &localization_status, &battery)
|| btnode_Sequence51_btn25(&btnode)
|| btnode_Repeat49_btn24(&btnode)
|| btnode_Parallel45_btn22(&btnode)
|| btnode_goto_waypoint_btn33(&btnode, &fls, &localization_status, &battery)
|| btnode_land_btn34(&btnode, &fls, &localization_status, &battery)
|| btnode_shutdown_drone_btn35(&btnode, &fls, &localization_status, &battery)
|| btnode_Eval73_btn36(&btnode, &fls, &localization_status, &battery)
|| btnode_Sequence41_btn20(&btnode)
|| btnode_ReactiveSequence11_btn5(&btnode)
|| btnode_Sequence3_btn1(&btnode)
|| btnode_BehaviorTree1_drone(&btnode)
// **** end of the component ****

end


drone

/* Some properties to model check */

/* Can the btn3 btnode properly execute? */
property Action_start_drone_btn3_undoable is absent drone/3/state ether
assert Action_start_drone_btn3_undoable

/* Can the btn3 btnode success? */
property Action_start_drone_btn3_cannot_succeed is absent drone/3/state success
assert Action_start_drone_btn3_cannot_succeed

/* Can the btn3 btnode return failure? */
property Action_start_drone_btn3_cannot_fail is absent drone/3/state failure
assert Action_start_drone_btn3_cannot_fail

/* Can the btn3 btnode be halted? */
property Action_start_drone_btn3_cannot_be_halted is absent drone/3/state halted
assert Action_start_drone_btn3_cannot_be_halted

/* Can the btn3 btnode return running? */
property Action_start_drone_btn3_cannot_return_running is absent drone/3/state running
assert Action_start_drone_btn3_cannot_return_running

/* Can the btn4 btnode properly execute? */
property Action_start_camera_btn4_undoable is absent drone/4/state ether
assert Action_start_camera_btn4_undoable

/* Can the btn4 btnode success? */
property Action_start_camera_btn4_cannot_succeed is absent drone/4/state success
assert Action_start_camera_btn4_cannot_succeed

/* Can the btn4 btnode return failure? */
property Action_start_camera_btn4_cannot_fail is absent drone/4/state failure
assert Action_start_camera_btn4_cannot_fail

/* Can the btn4 btnode be halted? */
property Action_start_camera_btn4_cannot_be_halted is absent drone/4/state halted
assert Action_start_camera_btn4_cannot_be_halted

/* Can the btn4 btnode return running? */
property Action_start_camera_btn4_cannot_return_running is absent drone/4/state running
assert Action_start_camera_btn4_cannot_return_running

/* Can the btn2 btnode properly execute? */
property ParallelAll_ParallelAll5_btn2_undoable is absent drone/5/state ether
assert ParallelAll_ParallelAll5_btn2_undoable

/* Can the btn2 btnode success? */
property ParallelAll_ParallelAll5_btn2_cannot_succeed is absent drone/5/state success
assert ParallelAll_ParallelAll5_btn2_cannot_succeed

/* Can the btn2 btnode return failure? */
property ParallelAll_ParallelAll5_btn2_cannot_fail is absent drone/5/state failure
assert ParallelAll_ParallelAll5_btn2_cannot_fail

/* Can the btn2 btnode be halted? */
property ParallelAll_ParallelAll5_btn2_cannot_be_halted is absent drone/5/state halted
assert ParallelAll_ParallelAll5_btn2_cannot_be_halted

/* Can the btn9 btnode properly execute? */
property SetSV_measure_battery_btn9_undoable is absent drone/6/state ether
assert SetSV_measure_battery_btn9_undoable

/* Can the btn9 btnode success? */
property SetSV_measure_battery_btn9_cannot_succeed is absent drone/6/state success
assert SetSV_measure_battery_btn9_cannot_succeed

/* Can the btn9 btnode return failure? */
property SetSV_measure_battery_btn9_cannot_fail is absent drone/6/state failure
assert SetSV_measure_battery_btn9_cannot_fail

/* Can the btn9 btnode be halted? */
property SetSV_measure_battery_btn9_cannot_be_halted is absent drone/6/state halted
assert SetSV_measure_battery_btn9_cannot_be_halted

/* Can the btn9 btnode return running? */
property SetSV_measure_battery_btn9_cannot_return_running is absent drone/6/state running
assert SetSV_measure_battery_btn9_cannot_return_running

/* Can the btn9 btnode go in error? */
property SetSV_measure_battery_btn9_cannot_error is absent drone/6/state error
assert SetSV_measure_battery_btn9_cannot_error

/* Can the btn8 btnode properly execute? */
property ForceFailure_fail_btn8_undoable is absent drone/7/state ether
assert ForceFailure_fail_btn8_undoable

/* Can the btn8 btnode success? */
property ForceFailure_fail_btn8_cannot_succeed is absent drone/7/state success
assert ForceFailure_fail_btn8_cannot_succeed

/* Can the btn8 btnode return failure? */
property ForceFailure_fail_btn8_cannot_fail is absent drone/7/state failure
assert ForceFailure_fail_btn8_cannot_fail

/* Can the btn8 btnode be halted? */
property ForceFailure_fail_btn8_cannot_be_halted is absent drone/7/state halted
assert ForceFailure_fail_btn8_cannot_be_halted

/* Can the btn8 btnode return running? */
property ForceFailure_fail_btn8_cannot_return_running is absent drone/7/state running
assert ForceFailure_fail_btn8_cannot_return_running

/* Can the btn8 btnode go in error? */
property ForceFailure_fail_btn8_cannot_error is absent drone/7/state error
assert ForceFailure_fail_btn8_cannot_error

/* Can the btn10 btnode properly execute? */
property Eval_Eval21_btn10_undoable is absent drone/8/state ether
assert Eval_Eval21_btn10_undoable

/* Can the btn10 btnode success? */
property Eval_Eval21_btn10_cannot_succeed is absent drone/8/state success
assert Eval_Eval21_btn10_cannot_succeed

/* Can the btn10 btnode return failure? */
property Eval_Eval21_btn10_cannot_fail is absent drone/8/state failure
assert Eval_Eval21_btn10_cannot_fail

/* Can the btn10 btnode be halted? */
property Eval_Eval21_btn10_cannot_be_halted is absent drone/8/state halted
assert Eval_Eval21_btn10_cannot_be_halted

/* Can the btn11 btnode properly execute? */
property Action_land_btn11_undoable is absent drone/9/state ether
assert Action_land_btn11_undoable

/* Can the btn11 btnode success? */
property Action_land_btn11_cannot_succeed is absent drone/9/state success
assert Action_land_btn11_cannot_succeed

/* Can the btn11 btnode return failure? */
property Action_land_btn11_cannot_fail is absent drone/9/state failure
assert Action_land_btn11_cannot_fail

/* Can the btn11 btnode be halted? */
property Action_land_btn11_cannot_be_halted is absent drone/9/state halted
assert Action_land_btn11_cannot_be_halted

/* Can the btn11 btnode return running? */
property Action_land_btn11_cannot_return_running is absent drone/9/state running
assert Action_land_btn11_cannot_return_running

/* Can the btn7 btnode properly execute? */
property Fallback_Fallback15_btn7_undoable is absent drone/10/state ether
assert Fallback_Fallback15_btn7_undoable

/* Can the btn7 btnode success? */
property Fallback_Fallback15_btn7_cannot_succeed is absent drone/10/state success
assert Fallback_Fallback15_btn7_cannot_succeed

/* Can the btn7 btnode return failure? */
property Fallback_Fallback15_btn7_cannot_fail is absent drone/10/state failure
assert Fallback_Fallback15_btn7_cannot_fail

/* Can the btn7 btnode be halted? */
property Fallback_Fallback15_btn7_cannot_be_halted is absent drone/10/state halted
assert Fallback_Fallback15_btn7_cannot_be_halted

/* Can the btn7 btnode return running? */
property Fallback_Fallback15_btn7_cannot_return_running is absent drone/10/state running
assert Fallback_Fallback15_btn7_cannot_return_running

/* Can the btn7 btnode go in error? */
property Fallback_Fallback15_btn7_cannot_error is absent drone/10/state error
assert Fallback_Fallback15_btn7_cannot_error

/* Can the btn12 btnode properly execute? */
property Eval_Eval25_btn12_undoable is absent drone/11/state ether
assert Eval_Eval25_btn12_undoable

/* Can the btn12 btnode success? */
property Eval_Eval25_btn12_cannot_succeed is absent drone/11/state success
assert Eval_Eval25_btn12_cannot_succeed

/* Can the btn12 btnode return failure? */
property Eval_Eval25_btn12_cannot_fail is absent drone/11/state failure
assert Eval_Eval25_btn12_cannot_fail

/* Can the btn12 btnode be halted? */
property Eval_Eval25_btn12_cannot_be_halted is absent drone/11/state halted
assert Eval_Eval25_btn12_cannot_be_halted

/* Can the btn14 btnode properly execute? */
property Eval_Eval29_btn14_undoable is absent drone/12/state ether
assert Eval_Eval29_btn14_undoable

/* Can the btn14 btnode success? */
property Eval_Eval29_btn14_cannot_succeed is absent drone/12/state success
assert Eval_Eval29_btn14_cannot_succeed

/* Can the btn14 btnode return failure? */
property Eval_Eval29_btn14_cannot_fail is absent drone/12/state failure
assert Eval_Eval29_btn14_cannot_fail

/* Can the btn14 btnode be halted? */
property Eval_Eval29_btn14_cannot_be_halted is absent drone/12/state halted
assert Eval_Eval29_btn14_cannot_be_halted

/* Can the btn15 btnode properly execute? */
property Action_goto_waypoint_btn15_undoable is absent drone/13/state ether
assert Action_goto_waypoint_btn15_undoable

/* Can the btn15 btnode success? */
property Action_goto_waypoint_btn15_cannot_succeed is absent drone/13/state success
assert Action_goto_waypoint_btn15_cannot_succeed

/* Can the btn15 btnode return failure? */
property Action_goto_waypoint_btn15_cannot_fail is absent drone/13/state failure
assert Action_goto_waypoint_btn15_cannot_fail

/* Can the btn15 btnode be halted? */
property Action_goto_waypoint_btn15_cannot_be_halted is absent drone/13/state halted
assert Action_goto_waypoint_btn15_cannot_be_halted

/* Can the btn15 btnode return running? */
property Action_goto_waypoint_btn15_cannot_return_running is absent drone/13/state running
assert Action_goto_waypoint_btn15_cannot_return_running

/* Can the btn13 btnode properly execute? */
property Fallback_Fallback27_btn13_undoable is absent drone/14/state ether
assert Fallback_Fallback27_btn13_undoable

/* Can the btn13 btnode success? */
property Fallback_Fallback27_btn13_cannot_succeed is absent drone/14/state success
assert Fallback_Fallback27_btn13_cannot_succeed

/* Can the btn13 btnode return failure? */
property Fallback_Fallback27_btn13_cannot_fail is absent drone/14/state failure
assert Fallback_Fallback27_btn13_cannot_fail

/* Can the btn13 btnode be halted? */
property Fallback_Fallback27_btn13_cannot_be_halted is absent drone/14/state halted
assert Fallback_Fallback27_btn13_cannot_be_halted

/* Can the btn13 btnode return running? */
property Fallback_Fallback27_btn13_cannot_return_running is absent drone/14/state running
assert Fallback_Fallback27_btn13_cannot_return_running

/* Can the btn13 btnode go in error? */
property Fallback_Fallback27_btn13_cannot_error is absent drone/14/state error
assert Fallback_Fallback27_btn13_cannot_error

/* Can the btn6 btnode properly execute? */
property Sequence_Sequence13_btn6_undoable is absent drone/15/state ether
assert Sequence_Sequence13_btn6_undoable

/* Can the btn6 btnode success? */
property Sequence_Sequence13_btn6_cannot_succeed is absent drone/15/state success
assert Sequence_Sequence13_btn6_cannot_succeed

/* Can the btn6 btnode return failure? */
property Sequence_Sequence13_btn6_cannot_fail is absent drone/15/state failure
assert Sequence_Sequence13_btn6_cannot_fail

/* Can the btn6 btnode be halted? */
property Sequence_Sequence13_btn6_cannot_be_halted is absent drone/15/state halted
assert Sequence_Sequence13_btn6_cannot_be_halted

/* Can the btn6 btnode return running? */
property Sequence_Sequence13_btn6_cannot_return_running is absent drone/15/state running
assert Sequence_Sequence13_btn6_cannot_return_running

/* Can the btn6 btnode go in error? */
property Sequence_Sequence13_btn6_cannot_error is absent drone/15/state error
assert Sequence_Sequence13_btn6_cannot_error

/* Can the btn17 btnode properly execute? */
property Condition_localization_ok_btn17_undoable is absent drone/16/state ether
assert Condition_localization_ok_btn17_undoable

/* Can the btn17 btnode success? */
property Condition_localization_ok_btn17_cannot_succeed is absent drone/16/state success
assert Condition_localization_ok_btn17_cannot_succeed

/* Can the btn17 btnode return failure? */
property Condition_localization_ok_btn17_cannot_fail is absent drone/16/state failure
assert Condition_localization_ok_btn17_cannot_fail

/* Can the btn17 btnode be halted? */
property Condition_localization_ok_btn17_cannot_be_halted is absent drone/16/state halted
assert Condition_localization_ok_btn17_cannot_be_halted

/* Can the btn19 btnode properly execute? */
property Action_land_btn19_undoable is absent drone/17/state ether
assert Action_land_btn19_undoable

/* Can the btn19 btnode success? */
property Action_land_btn19_cannot_succeed is absent drone/17/state success
assert Action_land_btn19_cannot_succeed

/* Can the btn19 btnode return failure? */
property Action_land_btn19_cannot_fail is absent drone/17/state failure
assert Action_land_btn19_cannot_fail

/* Can the btn19 btnode be halted? */
property Action_land_btn19_cannot_be_halted is absent drone/17/state halted
assert Action_land_btn19_cannot_be_halted

/* Can the btn19 btnode return running? */
property Action_land_btn19_cannot_return_running is absent drone/17/state running
assert Action_land_btn19_cannot_return_running

/* Can the btn18 btnode properly execute? */
property ForceFailure_fail_btn18_undoable is absent drone/18/state ether
assert ForceFailure_fail_btn18_undoable

/* Can the btn18 btnode success? */
property ForceFailure_fail_btn18_cannot_succeed is absent drone/18/state success
assert ForceFailure_fail_btn18_cannot_succeed

/* Can the btn18 btnode return failure? */
property ForceFailure_fail_btn18_cannot_fail is absent drone/18/state failure
assert ForceFailure_fail_btn18_cannot_fail

/* Can the btn18 btnode be halted? */
property ForceFailure_fail_btn18_cannot_be_halted is absent drone/18/state halted
assert ForceFailure_fail_btn18_cannot_be_halted

/* Can the btn18 btnode return running? */
property ForceFailure_fail_btn18_cannot_return_running is absent drone/18/state running
assert ForceFailure_fail_btn18_cannot_return_running

/* Can the btn18 btnode go in error? */
property ForceFailure_fail_btn18_cannot_error is absent drone/18/state error
assert ForceFailure_fail_btn18_cannot_error

/* Can the btn16 btnode properly execute? */
property Fallback_Fallback33_btn16_undoable is absent drone/19/state ether
assert Fallback_Fallback33_btn16_undoable

/* Can the btn16 btnode success? */
property Fallback_Fallback33_btn16_cannot_succeed is absent drone/19/state success
assert Fallback_Fallback33_btn16_cannot_succeed

/* Can the btn16 btnode return failure? */
property Fallback_Fallback33_btn16_cannot_fail is absent drone/19/state failure
assert Fallback_Fallback33_btn16_cannot_fail

/* Can the btn16 btnode be halted? */
property Fallback_Fallback33_btn16_cannot_be_halted is absent drone/19/state halted
assert Fallback_Fallback33_btn16_cannot_be_halted

/* Can the btn16 btnode return running? */
property Fallback_Fallback33_btn16_cannot_return_running is absent drone/19/state running
assert Fallback_Fallback33_btn16_cannot_return_running

/* Can the btn16 btnode go in error? */
property Fallback_Fallback33_btn16_cannot_error is absent drone/19/state error
assert Fallback_Fallback33_btn16_cannot_error

/* Can the btn21 btnode properly execute? */
property Action_takeoff_btn21_undoable is absent drone/20/state ether
assert Action_takeoff_btn21_undoable

/* Can the btn21 btnode success? */
property Action_takeoff_btn21_cannot_succeed is absent drone/20/state success
assert Action_takeoff_btn21_cannot_succeed

/* Can the btn21 btnode return failure? */
property Action_takeoff_btn21_cannot_fail is absent drone/20/state failure
assert Action_takeoff_btn21_cannot_fail

/* Can the btn21 btnode be halted? */
property Action_takeoff_btn21_cannot_be_halted is absent drone/20/state halted
assert Action_takeoff_btn21_cannot_be_halted

/* Can the btn21 btnode return running? */
property Action_takeoff_btn21_cannot_return_running is absent drone/20/state running
assert Action_takeoff_btn21_cannot_return_running

/* Can the camera_track btnode properly execute? */
property Action_camera_tracking_camera_track_undoable is absent drone/21/state ether
assert Action_camera_tracking_camera_track_undoable

/* Can the camera_track btnode success? */
property Action_camera_tracking_camera_track_cannot_succeed is absent drone/21/state success
assert Action_camera_tracking_camera_track_cannot_succeed

/* Can the camera_track btnode return failure? */
property Action_camera_tracking_camera_track_cannot_fail is absent drone/21/state failure
assert Action_camera_tracking_camera_track_cannot_fail

/* Can the camera_track btnode be halted? */
property Action_camera_tracking_camera_track_cannot_be_halted is absent drone/21/state halted
assert Action_camera_tracking_camera_track_cannot_be_halted

/* Can the camera_track btnode return running? */
property Action_camera_tracking_camera_track_cannot_return_running is absent drone/21/state running
assert Action_camera_tracking_camera_track_cannot_return_running

/* Can the btn26 btnode properly execute? */
property Eval_Eval53_btn26_undoable is absent drone/22/state ether
assert Eval_Eval53_btn26_undoable

/* Can the btn26 btnode success? */
property Eval_Eval53_btn26_cannot_succeed is absent drone/22/state success
assert Eval_Eval53_btn26_cannot_succeed

/* Can the btn26 btnode return failure? */
property Eval_Eval53_btn26_cannot_fail is absent drone/22/state failure
assert Eval_Eval53_btn26_cannot_fail

/* Can the btn26 btnode be halted? */
property Eval_Eval53_btn26_cannot_be_halted is absent drone/22/state halted
assert Eval_Eval53_btn26_cannot_be_halted

/* Can the btn27 btnode properly execute? */
property Action_goto_waypoint_btn27_undoable is absent drone/23/state ether
assert Action_goto_waypoint_btn27_undoable

/* Can the btn27 btnode success? */
property Action_goto_waypoint_btn27_cannot_succeed is absent drone/23/state success
assert Action_goto_waypoint_btn27_cannot_succeed

/* Can the btn27 btnode return failure? */
property Action_goto_waypoint_btn27_cannot_fail is absent drone/23/state failure
assert Action_goto_waypoint_btn27_cannot_fail

/* Can the btn27 btnode be halted? */
property Action_goto_waypoint_btn27_cannot_be_halted is absent drone/23/state halted
assert Action_goto_waypoint_btn27_cannot_be_halted

/* Can the btn27 btnode return running? */
property Action_goto_waypoint_btn27_cannot_return_running is absent drone/23/state running
assert Action_goto_waypoint_btn27_cannot_return_running

/* Can the btn28 btnode properly execute? */
property Action_goto_waypoint_btn28_undoable is absent drone/24/state ether
assert Action_goto_waypoint_btn28_undoable

/* Can the btn28 btnode success? */
property Action_goto_waypoint_btn28_cannot_succeed is absent drone/24/state success
assert Action_goto_waypoint_btn28_cannot_succeed

/* Can the btn28 btnode return failure? */
property Action_goto_waypoint_btn28_cannot_fail is absent drone/24/state failure
assert Action_goto_waypoint_btn28_cannot_fail

/* Can the btn28 btnode be halted? */
property Action_goto_waypoint_btn28_cannot_be_halted is absent drone/24/state halted
assert Action_goto_waypoint_btn28_cannot_be_halted

/* Can the btn28 btnode return running? */
property Action_goto_waypoint_btn28_cannot_return_running is absent drone/24/state running
assert Action_goto_waypoint_btn28_cannot_return_running

/* Can the btn29 btnode properly execute? */
property Action_goto_waypoint_btn29_undoable is absent drone/25/state ether
assert Action_goto_waypoint_btn29_undoable

/* Can the btn29 btnode success? */
property Action_goto_waypoint_btn29_cannot_succeed is absent drone/25/state success
assert Action_goto_waypoint_btn29_cannot_succeed

/* Can the btn29 btnode return failure? */
property Action_goto_waypoint_btn29_cannot_fail is absent drone/25/state failure
assert Action_goto_waypoint_btn29_cannot_fail

/* Can the btn29 btnode be halted? */
property Action_goto_waypoint_btn29_cannot_be_halted is absent drone/25/state halted
assert Action_goto_waypoint_btn29_cannot_be_halted

/* Can the btn29 btnode return running? */
property Action_goto_waypoint_btn29_cannot_return_running is absent drone/25/state running
assert Action_goto_waypoint_btn29_cannot_return_running

/* Can the btn30 btnode properly execute? */
property Action_goto_waypoint_btn30_undoable is absent drone/26/state ether
assert Action_goto_waypoint_btn30_undoable

/* Can the btn30 btnode success? */
property Action_goto_waypoint_btn30_cannot_succeed is absent drone/26/state success
assert Action_goto_waypoint_btn30_cannot_succeed

/* Can the btn30 btnode return failure? */
property Action_goto_waypoint_btn30_cannot_fail is absent drone/26/state failure
assert Action_goto_waypoint_btn30_cannot_fail

/* Can the btn30 btnode be halted? */
property Action_goto_waypoint_btn30_cannot_be_halted is absent drone/26/state halted
assert Action_goto_waypoint_btn30_cannot_be_halted

/* Can the btn30 btnode return running? */
property Action_goto_waypoint_btn30_cannot_return_running is absent drone/26/state running
assert Action_goto_waypoint_btn30_cannot_return_running

/* Can the btn31 btnode properly execute? */
property Action_goto_waypoint_btn31_undoable is absent drone/27/state ether
assert Action_goto_waypoint_btn31_undoable

/* Can the btn31 btnode success? */
property Action_goto_waypoint_btn31_cannot_succeed is absent drone/27/state success
assert Action_goto_waypoint_btn31_cannot_succeed

/* Can the btn31 btnode return failure? */
property Action_goto_waypoint_btn31_cannot_fail is absent drone/27/state failure
assert Action_goto_waypoint_btn31_cannot_fail

/* Can the btn31 btnode be halted? */
property Action_goto_waypoint_btn31_cannot_be_halted is absent drone/27/state halted
assert Action_goto_waypoint_btn31_cannot_be_halted

/* Can the btn31 btnode return running? */
property Action_goto_waypoint_btn31_cannot_return_running is absent drone/27/state running
assert Action_goto_waypoint_btn31_cannot_return_running

/* Can the btn32 btnode properly execute? */
property Action_goto_waypoint_btn32_undoable is absent drone/28/state ether
assert Action_goto_waypoint_btn32_undoable

/* Can the btn32 btnode success? */
property Action_goto_waypoint_btn32_cannot_succeed is absent drone/28/state success
assert Action_goto_waypoint_btn32_cannot_succeed

/* Can the btn32 btnode return failure? */
property Action_goto_waypoint_btn32_cannot_fail is absent drone/28/state failure
assert Action_goto_waypoint_btn32_cannot_fail

/* Can the btn32 btnode be halted? */
property Action_goto_waypoint_btn32_cannot_be_halted is absent drone/28/state halted
assert Action_goto_waypoint_btn32_cannot_be_halted

/* Can the btn32 btnode return running? */
property Action_goto_waypoint_btn32_cannot_return_running is absent drone/28/state running
assert Action_goto_waypoint_btn32_cannot_return_running

/* Can the btn25 btnode properly execute? */
property Sequence_Sequence51_btn25_undoable is absent drone/29/state ether
assert Sequence_Sequence51_btn25_undoable

/* Can the btn25 btnode success? */
property Sequence_Sequence51_btn25_cannot_succeed is absent drone/29/state success
assert Sequence_Sequence51_btn25_cannot_succeed

/* Can the btn25 btnode return failure? */
property Sequence_Sequence51_btn25_cannot_fail is absent drone/29/state failure
assert Sequence_Sequence51_btn25_cannot_fail

/* Can the btn25 btnode be halted? */
property Sequence_Sequence51_btn25_cannot_be_halted is absent drone/29/state halted
assert Sequence_Sequence51_btn25_cannot_be_halted

/* Can the btn25 btnode return running? */
property Sequence_Sequence51_btn25_cannot_return_running is absent drone/29/state running
assert Sequence_Sequence51_btn25_cannot_return_running

/* Can the btn25 btnode go in error? */
property Sequence_Sequence51_btn25_cannot_error is absent drone/29/state error
assert Sequence_Sequence51_btn25_cannot_error

/* Can the btn24 btnode properly execute? */
property Repeat_Repeat49_btn24_undoable is absent drone/30/state ether
assert Repeat_Repeat49_btn24_undoable

/* Can the btn24 btnode success? */
property Repeat_Repeat49_btn24_cannot_succeed is absent drone/30/state success
assert Repeat_Repeat49_btn24_cannot_succeed

/* Can the btn24 btnode return failure? */
property Repeat_Repeat49_btn24_cannot_fail is absent drone/30/state failure
assert Repeat_Repeat49_btn24_cannot_fail

/* Can the btn24 btnode be halted? */
property Repeat_Repeat49_btn24_cannot_be_halted is absent drone/30/state halted
assert Repeat_Repeat49_btn24_cannot_be_halted

/* Can the btn24 btnode return running? */
property Repeat_Repeat49_btn24_cannot_return_running is absent drone/30/state running
assert Repeat_Repeat49_btn24_cannot_return_running

/* Can the btn24 btnode go in error? */
property Repeat_Repeat49_btn24_cannot_error is absent drone/30/state error
assert Repeat_Repeat49_btn24_cannot_error

/* Can the btn22 btnode properly execute? */
property Parallel_Parallel45_btn22_undoable is absent drone/31/state ether
assert Parallel_Parallel45_btn22_undoable

/* Can the btn22 btnode success? */
property Parallel_Parallel45_btn22_cannot_succeed is absent drone/31/state success
assert Parallel_Parallel45_btn22_cannot_succeed

/* Can the btn22 btnode return failure? */
property Parallel_Parallel45_btn22_cannot_fail is absent drone/31/state failure
assert Parallel_Parallel45_btn22_cannot_fail

/* Can the btn22 btnode be halted? */
property Parallel_Parallel45_btn22_cannot_be_halted is absent drone/31/state halted
assert Parallel_Parallel45_btn22_cannot_be_halted

/* Can the btn33 btnode properly execute? */
property Action_goto_waypoint_btn33_undoable is absent drone/32/state ether
assert Action_goto_waypoint_btn33_undoable

/* Can the btn33 btnode success? */
property Action_goto_waypoint_btn33_cannot_succeed is absent drone/32/state success
assert Action_goto_waypoint_btn33_cannot_succeed

/* Can the btn33 btnode return failure? */
property Action_goto_waypoint_btn33_cannot_fail is absent drone/32/state failure
assert Action_goto_waypoint_btn33_cannot_fail

/* Can the btn33 btnode be halted? */
property Action_goto_waypoint_btn33_cannot_be_halted is absent drone/32/state halted
assert Action_goto_waypoint_btn33_cannot_be_halted

/* Can the btn33 btnode return running? */
property Action_goto_waypoint_btn33_cannot_return_running is absent drone/32/state running
assert Action_goto_waypoint_btn33_cannot_return_running

/* Can the btn34 btnode properly execute? */
property Action_land_btn34_undoable is absent drone/33/state ether
assert Action_land_btn34_undoable

/* Can the btn34 btnode success? */
property Action_land_btn34_cannot_succeed is absent drone/33/state success
assert Action_land_btn34_cannot_succeed

/* Can the btn34 btnode return failure? */
property Action_land_btn34_cannot_fail is absent drone/33/state failure
assert Action_land_btn34_cannot_fail

/* Can the btn34 btnode be halted? */
property Action_land_btn34_cannot_be_halted is absent drone/33/state halted
assert Action_land_btn34_cannot_be_halted

/* Can the btn34 btnode return running? */
property Action_land_btn34_cannot_return_running is absent drone/33/state running
assert Action_land_btn34_cannot_return_running

/* Can the btn35 btnode properly execute? */
property Action_shutdown_drone_btn35_undoable is absent drone/34/state ether
assert Action_shutdown_drone_btn35_undoable

/* Can the btn35 btnode success? */
property Action_shutdown_drone_btn35_cannot_succeed is absent drone/34/state success
assert Action_shutdown_drone_btn35_cannot_succeed

/* Can the btn35 btnode return failure? */
property Action_shutdown_drone_btn35_cannot_fail is absent drone/34/state failure
assert Action_shutdown_drone_btn35_cannot_fail

/* Can the btn35 btnode be halted? */
property Action_shutdown_drone_btn35_cannot_be_halted is absent drone/34/state halted
assert Action_shutdown_drone_btn35_cannot_be_halted

/* Can the btn35 btnode return running? */
property Action_shutdown_drone_btn35_cannot_return_running is absent drone/34/state running
assert Action_shutdown_drone_btn35_cannot_return_running

/* Can the btn36 btnode properly execute? */
property Eval_Eval73_btn36_undoable is absent drone/35/state ether
assert Eval_Eval73_btn36_undoable

/* Can the btn36 btnode success? */
property Eval_Eval73_btn36_cannot_succeed is absent drone/35/state success
assert Eval_Eval73_btn36_cannot_succeed

/* Can the btn36 btnode return failure? */
property Eval_Eval73_btn36_cannot_fail is absent drone/35/state failure
assert Eval_Eval73_btn36_cannot_fail

/* Can the btn36 btnode be halted? */
property Eval_Eval73_btn36_cannot_be_halted is absent drone/35/state halted
assert Eval_Eval73_btn36_cannot_be_halted

/* Can the btn20 btnode properly execute? */
property Sequence_Sequence41_btn20_undoable is absent drone/36/state ether
assert Sequence_Sequence41_btn20_undoable

/* Can the btn20 btnode success? */
property Sequence_Sequence41_btn20_cannot_succeed is absent drone/36/state success
assert Sequence_Sequence41_btn20_cannot_succeed

/* Can the btn20 btnode return failure? */
property Sequence_Sequence41_btn20_cannot_fail is absent drone/36/state failure
assert Sequence_Sequence41_btn20_cannot_fail

/* Can the btn20 btnode be halted? */
property Sequence_Sequence41_btn20_cannot_be_halted is absent drone/36/state halted
assert Sequence_Sequence41_btn20_cannot_be_halted

/* Can the btn20 btnode return running? */
property Sequence_Sequence41_btn20_cannot_return_running is absent drone/36/state running
assert Sequence_Sequence41_btn20_cannot_return_running

/* Can the btn20 btnode go in error? */
property Sequence_Sequence41_btn20_cannot_error is absent drone/36/state error
assert Sequence_Sequence41_btn20_cannot_error

/* Can the btn5 btnode properly execute? */
property ReactiveSequence_ReactiveSequence11_btn5_undoable is absent drone/37/state ether
assert ReactiveSequence_ReactiveSequence11_btn5_undoable

/* Can the btn5 btnode success? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_succeed is absent drone/37/state success
assert ReactiveSequence_ReactiveSequence11_btn5_cannot_succeed

/* Can the btn5 btnode return failure? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_fail is absent drone/37/state failure
assert ReactiveSequence_ReactiveSequence11_btn5_cannot_fail

/* Can the btn5 btnode be halted? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_be_halted is absent drone/37/state halted
assert ReactiveSequence_ReactiveSequence11_btn5_cannot_be_halted

/* Can the btn5 btnode return running? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_return_running is absent drone/37/state running
assert ReactiveSequence_ReactiveSequence11_btn5_cannot_return_running

/* Can the btn5 btnode go in error? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_error is absent drone/37/state error
assert ReactiveSequence_ReactiveSequence11_btn5_cannot_error

/* Can the btn1 btnode properly execute? */
property Sequence_Sequence3_btn1_undoable is absent drone/38/state ether
assert Sequence_Sequence3_btn1_undoable

/* Can the btn1 btnode success? */
property Sequence_Sequence3_btn1_cannot_succeed is absent drone/38/state success
assert Sequence_Sequence3_btn1_cannot_succeed

/* Can the btn1 btnode return failure? */
property Sequence_Sequence3_btn1_cannot_fail is absent drone/38/state failure
assert Sequence_Sequence3_btn1_cannot_fail

/* Can the btn1 btnode be halted? */
property Sequence_Sequence3_btn1_cannot_be_halted is absent drone/38/state halted
assert Sequence_Sequence3_btn1_cannot_be_halted

/* Can the btn1 btnode return running? */
property Sequence_Sequence3_btn1_cannot_return_running is absent drone/38/state running
assert Sequence_Sequence3_btn1_cannot_return_running

/* Can the btn1 btnode go in error? */
property Sequence_Sequence3_btn1_cannot_error is absent drone/38/state error
assert Sequence_Sequence3_btn1_cannot_error

/* Can the drone btnode properly execute? */
property BehaviorTree_BehaviorTree1_drone_undoable is absent drone/39/state ether
assert BehaviorTree_BehaviorTree1_drone_undoable

/* Can the drone btnode success? */
property BehaviorTree_BehaviorTree1_drone_cannot_succeed is absent drone/39/state success
assert BehaviorTree_BehaviorTree1_drone_cannot_succeed

/* Can the drone btnode return failure? */
property BehaviorTree_BehaviorTree1_drone_cannot_fail is absent drone/39/state failure
assert BehaviorTree_BehaviorTree1_drone_cannot_fail

/* Can the drone btnode be halted? */
property BehaviorTree_BehaviorTree1_drone_cannot_be_halted is absent drone/39/state halted
assert BehaviorTree_BehaviorTree1_drone_cannot_be_halted

/* Can the drone btnode return running? */
property BehaviorTree_BehaviorTree1_drone_cannot_return_running is absent drone/39/state running
assert BehaviorTree_BehaviorTree1_drone_cannot_return_running

/* Can the drone btnode go in error? */
property BehaviorTree_BehaviorTree1_drone_cannot_error is absent drone/39/state error
assert BehaviorTree_BehaviorTree1_drone_cannot_error
/*End of File */