/*
 * Copyright (c) 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 btnode_caller is union
	  None
	| caller_ParallelAll5_btn2
	| caller_fail_btn8
	| caller_Fallback13_btn6
	| caller_fail_btn12
	| caller_Fallback21_btn10
	| caller_Sequence37_btn18
	| caller_Parallel33_btn16
	| caller_Sequence29_btn14
	| 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 battery_ok_btn7: 3..3 is 3
const land_btn9: 4..4 is 4
const fail_btn8: 5..5 is 5
const Fallback13_btn6: 6..6 is 6
const localization_ok_btn11: 7..7 is 7
const land_btn13: 8..8 is 8
const fail_btn12: 9..9 is 9
const Fallback21_btn10: 10..10 is 10
const takeoff_btn15: 11..11 is 11
const camera_tracking_btn17: 12..12 is 12
const goto_waypoint_btn19: 13..13 is 13
const goto_waypoint_btn20: 14..14 is 14
const goto_waypoint_btn21: 15..15 is 15
const goto_waypoint_btn22: 16..16 is 16
const goto_waypoint_btn23: 17..17 is 17
const goto_waypoint_btn24: 18..18 is 18
const Sequence37_btn18: 19..19 is 19
const Parallel33_btn16: 20..20 is 20
const goto_waypoint_btn25: 21..21 is 21
const land_btn26: 22..22 is 22
const shutdown_drone_btn27: 23..23 is 23
const Sequence29_btn14: 24..24 is 24
const ReactiveSequence11_btn5: 25..25 is 25
const Sequence3_btn1: 26..26 is 26
const BehaviorTree1_drone: 27..27 is 27

type btnode_array is array 28 of btnode_record


/* state variable integer types*/

/* state variable FSM types*/

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

process btnode_start_drone_btn3 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (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];
		to failure

	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) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (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];
		to failure

	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,
		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 (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 [1,1];
	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 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
				to success
			else
				to failure
			end
		else
			to failure
		end

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

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

	from ether
		wait [0,0];
	to start_

process btnode_battery_ok_btn7 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[battery_ok_btn7].caller <> None);
		btnode[battery_ok_btn7].rstatus := no_ret_status;
	to tick_node

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_land_btn9 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[land_btn9].caller <> None);
		if (btnode[land_btn9].rstatus = halt_me) then
			to halt
		end;
		btnode[land_btn9].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_btn9].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_fail_btn8 (&btnode: btnode_array) is

	states start_, tick_node, failure, halt, halted, halt_wait, running, error,
		land_btn9, land_btn9_done,
		done, ether

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (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[land_btn9].rstatus = running) then
			btnode[land_btn9].rstatus := halt_me;
			btnode[land_btn9].caller := caller_fail_btn8;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (btnode[land_btn9].caller = None);
	to halted

	from tick_node
		wait [1,1];
	to land_btn9

	from land_btn9
		wait [0,0];
		btnode[land_btn9].caller := caller_fail_btn8;
		to land_btn9_done

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

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

	from halted
		wait [0,0];
		to failure

	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_Fallback13_btn6 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		battery_ok_btn7, battery_ok_btn7_done,
		fail_btn8, fail_btn8_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_fb: 1..2 := 1

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

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

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

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

	from battery_ok_btn7
		wait [0,0];
		btnode[battery_ok_btn7].caller := caller_Fallback13_btn6;
		to battery_ok_btn7_done

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

	from fail_btn8
		wait [0,0];
		btnode[fail_btn8].caller := caller_Fallback13_btn6;
		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 := 1;
			to success
		elsif (btnode[fail_btn8].rstatus = failure) then
			next_fb := 1;
			to failure
		elsif (btnode[fail_btn8].rstatus = running) then
			next_fb := 2;
			to running
		else
			to error
		end

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

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

	from halted
		wait [0,0];
		next_fb := 1;
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_localization_ok_btn11 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[localization_ok_btn11].caller <> None);
		btnode[localization_ok_btn11].rstatus := no_ret_status;
	to tick_node

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_land_btn13 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[land_btn13].caller <> None);
		if (btnode[land_btn13].rstatus = halt_me) then
			to halt
		end;
		btnode[land_btn13].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_btn13].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_fail_btn12 (&btnode: btnode_array) is

	states start_, tick_node, failure, halt, halted, halt_wait, running, error,
		land_btn13, land_btn13_done,
		done, ether

	var ignorep: nat, ignoreb: bool

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

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

	from halt_wait
		on (btnode[land_btn13].caller = None);
	to halted

	from tick_node
		wait [1,1];
	to land_btn13

	from land_btn13
		wait [0,0];
		btnode[land_btn13].caller := caller_fail_btn12;
		to land_btn13_done

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

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Fallback21_btn10 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		localization_ok_btn11, localization_ok_btn11_done,
		fail_btn12, fail_btn12_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_fb: 1..2 := 1

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

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

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

	from tick_node
		wait [1,1];
		if (next_fb = 1) then to localization_ok_btn11 end;
		if (next_fb = 2) then to fail_btn12 end;
		to error

	from localization_ok_btn11
		wait [0,0];
		btnode[localization_ok_btn11].caller := caller_Fallback21_btn10;
		to localization_ok_btn11_done

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

	from fail_btn12
		wait [0,0];
		btnode[fail_btn12].caller := caller_Fallback21_btn10;
		to fail_btn12_done

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

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

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

	from halted
		wait [0,0];
		next_fb := 1;
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_takeoff_btn15 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[takeoff_btn15].caller <> None);
		if (btnode[takeoff_btn15].rstatus = halt_me) then
			to halt
		end;
		btnode[takeoff_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[takeoff_btn15].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_camera_tracking_btn17 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[camera_tracking_btn17].caller <> None);
		if (btnode[camera_tracking_btn17].rstatus = halt_me) then
			to halt
		end;
		btnode[camera_tracking_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
		[]
			to running
		end

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

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn19 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn19].caller <> None);
		if (btnode[goto_waypoint_btn19].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_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[goto_waypoint_btn19].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn20 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn20].caller <> None);
		if (btnode[goto_waypoint_btn20].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_btn20].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_btn20].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn21 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn21].caller <> None);
		if (btnode[goto_waypoint_btn21].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_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[goto_waypoint_btn21].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn22 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn22].caller <> None);
		if (btnode[goto_waypoint_btn22].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_btn22].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_btn22].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn23 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn23].caller <> None);
		if (btnode[goto_waypoint_btn23].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_btn23].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_btn23].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn24 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn24].caller <> None);
		if (btnode[goto_waypoint_btn24].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_btn24].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_btn24].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Sequence37_btn18 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		goto_waypoint_btn19, goto_waypoint_btn19_done,
		goto_waypoint_btn20, goto_waypoint_btn20_done,
		goto_waypoint_btn21, goto_waypoint_btn21_done,
		goto_waypoint_btn22, goto_waypoint_btn22_done,
		goto_waypoint_btn23, goto_waypoint_btn23_done,
		goto_waypoint_btn24, goto_waypoint_btn24_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq: 1..7 := 1

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

	from halt
		wait [0,0];
		if (btnode[goto_waypoint_btn19].rstatus = running) then
			btnode[goto_waypoint_btn19].rstatus := halt_me;
			btnode[goto_waypoint_btn19].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn20].rstatus = running) then
			btnode[goto_waypoint_btn20].rstatus := halt_me;
			btnode[goto_waypoint_btn20].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn21].rstatus = running) then
			btnode[goto_waypoint_btn21].rstatus := halt_me;
			btnode[goto_waypoint_btn21].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn22].rstatus = running) then
			btnode[goto_waypoint_btn22].rstatus := halt_me;
			btnode[goto_waypoint_btn22].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn23].rstatus = running) then
			btnode[goto_waypoint_btn23].rstatus := halt_me;
			btnode[goto_waypoint_btn23].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn24].rstatus = running) then
			btnode[goto_waypoint_btn24].rstatus := halt_me;
			btnode[goto_waypoint_btn24].caller := caller_Sequence37_btn18;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[goto_waypoint_btn19].caller = None) and
			(btnode[goto_waypoint_btn20].caller = None) and
			(btnode[goto_waypoint_btn21].caller = None) and
			(btnode[goto_waypoint_btn22].caller = None) and
			(btnode[goto_waypoint_btn23].caller = None) and
			(btnode[goto_waypoint_btn24].caller = None) and
			true);
		to halted

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to goto_waypoint_btn19 end;
		if (next_seq = 2) then to goto_waypoint_btn20 end;
		if (next_seq = 3) then to goto_waypoint_btn21 end;
		if (next_seq = 4) then to goto_waypoint_btn22 end;
		if (next_seq = 5) then to goto_waypoint_btn23 end;
		if (next_seq = 6) then to goto_waypoint_btn24 end;
		to error

	from goto_waypoint_btn19
		wait [0,0];
		btnode[goto_waypoint_btn19].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn19_done

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

	from goto_waypoint_btn20
		wait [0,0];
		btnode[goto_waypoint_btn20].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn20_done

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

	from goto_waypoint_btn21
		wait [0,0];
		btnode[goto_waypoint_btn21].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn21_done

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

	from goto_waypoint_btn22
		wait [0,0];
		btnode[goto_waypoint_btn22].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn22_done

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

	from goto_waypoint_btn23
		wait [0,0];
		btnode[goto_waypoint_btn23].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn23_done

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

	from goto_waypoint_btn24
		wait [0,0];
		btnode[goto_waypoint_btn24].caller := caller_Sequence37_btn18;
		to goto_waypoint_btn24_done

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

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

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

	from halted
		wait [0,0];
		next_seq := 1;
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Parallel33_btn16 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait,
		running, Parallel33_btn16_par, Parallel33_btn16_par_done,
		done, ether

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

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

	from halt
		wait [0,0];
		if (btnode[camera_tracking_btn17].rstatus = running) then
			btnode[camera_tracking_btn17].rstatus := halt_me;
			btnode[camera_tracking_btn17].caller := caller_Parallel33_btn16
		end;
		if (btnode[Sequence37_btn18].rstatus = running) then
			btnode[Sequence37_btn18].rstatus := halt_me;
			btnode[Sequence37_btn18].caller := caller_Parallel33_btn16
		end;
		to halt_wait

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

	from tick_node
		wait [1,1];
	to Parallel33_btn16_par

	from Parallel33_btn16_par
		wait [0,0];
		if (runningb) then
			if (btnode[camera_tracking_btn17].rstatus = running) then
				btnode[camera_tracking_btn17].caller := caller_Parallel33_btn16
			end;
			if (btnode[Sequence37_btn18].rstatus = running) then
				btnode[Sequence37_btn18].caller := caller_Parallel33_btn16
			end;
			null
		else
			btnode[camera_tracking_btn17].caller := caller_Parallel33_btn16;
			btnode[Sequence37_btn18].caller := caller_Parallel33_btn16;
			null
		end;
		to Parallel33_btn16_par_done

	from Parallel33_btn16_par_done
		wait [0,0];
		on (
			(btnode[camera_tracking_btn17].caller = None) and
			(btnode[Sequence37_btn18].caller = None) and
			true);
		success_so_far := 0; failed_so_far := 0;
		if (btnode[camera_tracking_btn17].rstatus = success) then success_so_far := success_so_far + 1
		elsif (btnode[camera_tracking_btn17].rstatus = failure) then failed_so_far := failed_so_far + 1 end; 
		if (btnode[Sequence37_btn18].rstatus = success) then success_so_far := success_so_far + 1
		elsif (btnode[Sequence37_btn18].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[Parallel33_btn16].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		if (halt_called_by_me) then
			if (force_success) then
				to success
			else
				to failure
			end
		else
			to failure
		end

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

	from done
		wait [0,0];
		halt_called_by_me := false;
		force_success := false;
		btnode[Parallel33_btn16].caller := None;
	to ether

	from ether
		wait [0,0];
	to start_

process btnode_goto_waypoint_btn25 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[goto_waypoint_btn25].caller <> None);
		if (btnode[goto_waypoint_btn25].rstatus = halt_me) then
			to halt
		end;
		btnode[goto_waypoint_btn25].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_btn25].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_land_btn26 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[land_btn26].caller <> None);
		if (btnode[land_btn26].rstatus = halt_me) then
			to halt
		end;
		btnode[land_btn26].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_btn26].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_shutdown_drone_btn27 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (btnode[shutdown_drone_btn27].caller <> None);
		if (btnode[shutdown_drone_btn27].rstatus = halt_me) then
			to halt
		end;
		btnode[shutdown_drone_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[shutdown_drone_btn27].rstatus := success;
		to done

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Sequence29_btn14 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		takeoff_btn15, takeoff_btn15_done,
		Parallel33_btn16, Parallel33_btn16_done,
		goto_waypoint_btn25, goto_waypoint_btn25_done,
		land_btn26, land_btn26_done,
		shutdown_drone_btn27, shutdown_drone_btn27_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		next_seq: 1..6 := 1

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

	from halt
		wait [0,0];
		if (btnode[takeoff_btn15].rstatus = running) then
			btnode[takeoff_btn15].rstatus := halt_me;
			btnode[takeoff_btn15].caller := caller_Sequence29_btn14;
			to halt_wait
		end;
		if (btnode[Parallel33_btn16].rstatus = running) then
			btnode[Parallel33_btn16].rstatus := halt_me;
			btnode[Parallel33_btn16].caller := caller_Sequence29_btn14;
			to halt_wait
		end;
		if (btnode[goto_waypoint_btn25].rstatus = running) then
			btnode[goto_waypoint_btn25].rstatus := halt_me;
			btnode[goto_waypoint_btn25].caller := caller_Sequence29_btn14;
			to halt_wait
		end;
		if (btnode[land_btn26].rstatus = running) then
			btnode[land_btn26].rstatus := halt_me;
			btnode[land_btn26].caller := caller_Sequence29_btn14;
			to halt_wait
		end;
		if (btnode[shutdown_drone_btn27].rstatus = running) then
			btnode[shutdown_drone_btn27].rstatus := halt_me;
			btnode[shutdown_drone_btn27].caller := caller_Sequence29_btn14;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[takeoff_btn15].caller = None) and
			(btnode[Parallel33_btn16].caller = None) and
			(btnode[goto_waypoint_btn25].caller = None) and
			(btnode[land_btn26].caller = None) and
			(btnode[shutdown_drone_btn27].caller = None) and
			true);
		to halted

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to takeoff_btn15 end;
		if (next_seq = 2) then to Parallel33_btn16 end;
		if (next_seq = 3) then to goto_waypoint_btn25 end;
		if (next_seq = 4) then to land_btn26 end;
		if (next_seq = 5) then to shutdown_drone_btn27 end;
		to error

	from takeoff_btn15
		wait [0,0];
		btnode[takeoff_btn15].caller := caller_Sequence29_btn14;
		to takeoff_btn15_done

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

	from Parallel33_btn16
		wait [0,0];
		btnode[Parallel33_btn16].caller := caller_Sequence29_btn14;
		to Parallel33_btn16_done

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

	from goto_waypoint_btn25
		wait [0,0];
		btnode[goto_waypoint_btn25].caller := caller_Sequence29_btn14;
		to goto_waypoint_btn25_done

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

	from land_btn26
		wait [0,0];
		btnode[land_btn26].caller := caller_Sequence29_btn14;
		to land_btn26_done

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

	from shutdown_drone_btn27
		wait [0,0];
		btnode[shutdown_drone_btn27].caller := caller_Sequence29_btn14;
		to shutdown_drone_btn27_done

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

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

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

	from halted
		wait [0,0];
		next_seq := 1;
		to failure

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

	from done
		wait [0,0];
		btnode[Sequence29_btn14].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,
		Fallback13_btn6, Fallback13_btn6_done,
		Fallback21_btn10, Fallback21_btn10_done,
		Sequence29_btn14, Sequence29_btn14_done,
		done, ether

	var ignorep: nat, ignoreb: bool,
		runningb:bool := false,
		halt_called_by_me:bool := false,
		force_success:bool := false,
		next_seq: 1..4 := 1

	from start_
		wait [0,0];
		on (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[Fallback13_btn6].rstatus = running) then
			btnode[Fallback13_btn6].rstatus := halt_me;
			btnode[Fallback13_btn6].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		if (btnode[Fallback21_btn10].rstatus = running) then
			btnode[Fallback21_btn10].rstatus := halt_me;
			btnode[Fallback21_btn10].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		if (btnode[Sequence29_btn14].rstatus = running) then
			btnode[Sequence29_btn14].rstatus := halt_me;
			btnode[Sequence29_btn14].caller := caller_ReactiveSequence11_btn5;
			to halt_wait
		end;
		to halted

	from halt_wait
		on (
			(btnode[Fallback13_btn6].caller = None) and
			(btnode[Fallback21_btn10].caller = None) and
			(btnode[Sequence29_btn14].caller = None) and
			true);
		to halted

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to Fallback13_btn6 end;
		if (next_seq = 2) then to Fallback21_btn10 end;
		if (next_seq = 3) then to Sequence29_btn14 end;
		to error

	from Fallback13_btn6
		wait [0,0];
		btnode[Fallback13_btn6].caller := caller_ReactiveSequence11_btn5;
		to Fallback13_btn6_done

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

	from Fallback21_btn10
		wait [0,0];
		btnode[Fallback21_btn10].caller := caller_ReactiveSequence11_btn5;
		to Fallback21_btn10_done

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

	from Sequence29_btn14
		wait [0,0];
		btnode[Sequence29_btn14].caller := caller_ReactiveSequence11_btn5;
		to Sequence29_btn14_done

	from Sequence29_btn14_done
		wait [0,0];
		on (btnode[Sequence29_btn14].caller = None);
		if (btnode[Sequence29_btn14].rstatus = success) then
			next_seq := 1;
			to success
		elsif (btnode[Sequence29_btn14].rstatus = failure) then
			next_seq := 1;
			to failure
		elsif (btnode[Sequence29_btn14].rstatus = running) then
			next_seq := 1;
			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];
		next_seq := 1;
		if (halt_called_by_me) then
			if (force_success) then
				to success
			else
				to failure
			end
		else
			to failure
		end

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

	from done
		wait [0,0];
		halt_called_by_me := false;
		force_success := false;
		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: 1..3 := 1

	from start_
		wait [0,0];
		on (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 [1,1];
		if (next_seq = 1) then to ParallelAll5_btn2 end;
		if (next_seq = 2) 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 := 1;
			to failure
		elsif (btnode[ParallelAll5_btn2].rstatus = running) then
			next_seq := 1;
			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 := 1;
			to success
		elsif (btnode[ReactiveSequence11_btn5].rstatus = failure) then
			next_seq := 1;
			to failure
		elsif (btnode[ReactiveSequence11_btn5].rstatus = running) then
			next_seq := 2;
			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];
		next_seq := 1;
		to failure

	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 (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];
		to failure

	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 = caller_BehaviorTree1_drone, ArgIndex = 0, rstatus = no_ret_status}]

par * in
// **** state variables processes ****
// **** btnode processes ****
   btnode_start_drone_btn3(&btnode)
|| btnode_start_camera_btn4(&btnode)
|| btnode_ParallelAll5_btn2(&btnode)
|| btnode_battery_ok_btn7(&btnode)
|| btnode_land_btn9(&btnode)
|| btnode_fail_btn8(&btnode)
|| btnode_Fallback13_btn6(&btnode)
|| btnode_localization_ok_btn11(&btnode)
|| btnode_land_btn13(&btnode)
|| btnode_fail_btn12(&btnode)
|| btnode_Fallback21_btn10(&btnode)
|| btnode_takeoff_btn15(&btnode)
|| btnode_camera_tracking_btn17(&btnode)
|| btnode_goto_waypoint_btn19(&btnode)
|| btnode_goto_waypoint_btn20(&btnode)
|| btnode_goto_waypoint_btn21(&btnode)
|| btnode_goto_waypoint_btn22(&btnode)
|| btnode_goto_waypoint_btn23(&btnode)
|| btnode_goto_waypoint_btn24(&btnode)
|| btnode_Sequence37_btn18(&btnode)
|| btnode_Parallel33_btn16(&btnode)
|| btnode_goto_waypoint_btn25(&btnode)
|| btnode_land_btn26(&btnode)
|| btnode_shutdown_drone_btn27(&btnode)
|| btnode_Sequence29_btn14(&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/1/state ether
prove Action_start_drone_btn3_undoable

/* Can the btn3 btnode success? */
property Action_start_drone_btn3_cannot_succeed is absent drone/1/value (btnode[start_drone_btn3].rstatus=success)
prove Action_start_drone_btn3_cannot_succeed

/* Can the btn3 btnode return failure? */
property Action_start_drone_btn3_cannot_fail is absent  drone/1/value (btnode[start_drone_btn3].rstatus=failure)
prove Action_start_drone_btn3_cannot_fail

/* Can the btn3 btnode be halted? */
property Action_start_drone_btn3_cannot_be_halted is absent drone/1/state halted
prove Action_start_drone_btn3_cannot_be_halted

/* Can the btn3 btnode return running? */
property Action_start_drone_btn3_cannot_return_running is absent drone/1/state running
prove Action_start_drone_btn3_cannot_return_running

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

/* Can the btn4 btnode success? */
property Action_start_camera_btn4_cannot_succeed is absent drone/2/value (btnode[start_camera_btn4].rstatus=success)
prove Action_start_camera_btn4_cannot_succeed

/* Can the btn4 btnode return failure? */
property Action_start_camera_btn4_cannot_fail is absent  drone/2/value (btnode[start_camera_btn4].rstatus=failure)
prove Action_start_camera_btn4_cannot_fail

/* Can the btn4 btnode be halted? */
property Action_start_camera_btn4_cannot_be_halted is absent drone/2/state halted
prove Action_start_camera_btn4_cannot_be_halted

/* Can the btn4 btnode return running? */
property Action_start_camera_btn4_cannot_return_running is absent drone/2/state running
prove Action_start_camera_btn4_cannot_return_running

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

/* Can the btn2 btnode success? */
property ParallelAll_ParallelAll5_btn2_cannot_succeed is absent drone/3/value (btnode[ParallelAll5_btn2].rstatus=success)
prove ParallelAll_ParallelAll5_btn2_cannot_succeed

/* Can the btn2 btnode return failure? */
property ParallelAll_ParallelAll5_btn2_cannot_fail is absent  drone/3/value (btnode[ParallelAll5_btn2].rstatus=failure)
prove ParallelAll_ParallelAll5_btn2_cannot_fail

/* Can the btn2 btnode be halted? */
property ParallelAll_ParallelAll5_btn2_cannot_be_halted is absent drone/3/state halted
prove ParallelAll_ParallelAll5_btn2_cannot_be_halted

/* Can the btn7 btnode properly execute? */
property Condition_battery_ok_btn7_undoable is absent drone/4/state ether
prove Condition_battery_ok_btn7_undoable

/* Can the btn7 btnode success? */
property Condition_battery_ok_btn7_cannot_succeed is absent drone/4/value (btnode[battery_ok_btn7].rstatus=success)
prove Condition_battery_ok_btn7_cannot_succeed

/* Can the btn7 btnode return failure? */
property Condition_battery_ok_btn7_cannot_fail is absent  drone/4/value (btnode[battery_ok_btn7].rstatus=failure)
prove Condition_battery_ok_btn7_cannot_fail

/* Can the btn9 btnode properly execute? */
property Action_land_btn9_undoable is absent drone/5/state ether
prove Action_land_btn9_undoable

/* Can the btn9 btnode success? */
property Action_land_btn9_cannot_succeed is absent drone/5/value (btnode[land_btn9].rstatus=success)
prove Action_land_btn9_cannot_succeed

/* Can the btn9 btnode return failure? */
property Action_land_btn9_cannot_fail is absent  drone/5/value (btnode[land_btn9].rstatus=failure)
prove Action_land_btn9_cannot_fail

/* Can the btn9 btnode be halted? */
property Action_land_btn9_cannot_be_halted is absent drone/5/state halted
prove Action_land_btn9_cannot_be_halted

/* Can the btn9 btnode return running? */
property Action_land_btn9_cannot_return_running is absent drone/5/state running
prove Action_land_btn9_cannot_return_running

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

/* Can the btn8 btnode success? */
property ForceFailure_fail_btn8_cannot_succeed is absent drone/6/value (btnode[fail_btn8].rstatus=success)
prove ForceFailure_fail_btn8_cannot_succeed

/* Can the btn8 btnode return failure? */
property ForceFailure_fail_btn8_cannot_fail is absent  drone/6/value (btnode[fail_btn8].rstatus=failure)
prove ForceFailure_fail_btn8_cannot_fail

/* Can the btn8 btnode be halted? */
property ForceFailure_fail_btn8_cannot_be_halted is absent drone/6/state halted
prove ForceFailure_fail_btn8_cannot_be_halted

/* Can the btn8 btnode return running? */
property ForceFailure_fail_btn8_cannot_return_running is absent drone/6/state running
prove ForceFailure_fail_btn8_cannot_return_running

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

/* Can the btn6 btnode properly execute? */
property Fallback_Fallback13_btn6_undoable is absent drone/7/state ether
prove Fallback_Fallback13_btn6_undoable

/* Can the btn6 btnode success? */
property Fallback_Fallback13_btn6_cannot_succeed is absent drone/7/value (btnode[Fallback13_btn6].rstatus=success)
prove Fallback_Fallback13_btn6_cannot_succeed

/* Can the btn6 btnode return failure? */
property Fallback_Fallback13_btn6_cannot_fail is absent  drone/7/value (btnode[Fallback13_btn6].rstatus=failure)
prove Fallback_Fallback13_btn6_cannot_fail

/* Can the btn6 btnode be halted? */
property Fallback_Fallback13_btn6_cannot_be_halted is absent drone/7/state halted
prove Fallback_Fallback13_btn6_cannot_be_halted

/* Can the btn6 btnode return running? */
property Fallback_Fallback13_btn6_cannot_return_running is absent drone/7/state running
prove Fallback_Fallback13_btn6_cannot_return_running

/* Can the btn6 btnode go in error? */
property Fallback_Fallback13_btn6_cannot_error is absent drone/7/state error
prove Fallback_Fallback13_btn6_cannot_error

/* Can the btn11 btnode properly execute? */
property Condition_localization_ok_btn11_undoable is absent drone/8/state ether
prove Condition_localization_ok_btn11_undoable

/* Can the btn11 btnode success? */
property Condition_localization_ok_btn11_cannot_succeed is absent drone/8/value (btnode[localization_ok_btn11].rstatus=success)
prove Condition_localization_ok_btn11_cannot_succeed

/* Can the btn11 btnode return failure? */
property Condition_localization_ok_btn11_cannot_fail is absent  drone/8/value (btnode[localization_ok_btn11].rstatus=failure)
prove Condition_localization_ok_btn11_cannot_fail

/* Can the btn13 btnode properly execute? */
property Action_land_btn13_undoable is absent drone/9/state ether
prove Action_land_btn13_undoable

/* Can the btn13 btnode success? */
property Action_land_btn13_cannot_succeed is absent drone/9/value (btnode[land_btn13].rstatus=success)
prove Action_land_btn13_cannot_succeed

/* Can the btn13 btnode return failure? */
property Action_land_btn13_cannot_fail is absent  drone/9/value (btnode[land_btn13].rstatus=failure)
prove Action_land_btn13_cannot_fail

/* Can the btn13 btnode be halted? */
property Action_land_btn13_cannot_be_halted is absent drone/9/state halted
prove Action_land_btn13_cannot_be_halted

/* Can the btn13 btnode return running? */
property Action_land_btn13_cannot_return_running is absent drone/9/state running
prove Action_land_btn13_cannot_return_running

/* Can the btn12 btnode properly execute? */
property ForceFailure_fail_btn12_undoable is absent drone/10/state ether
prove ForceFailure_fail_btn12_undoable

/* Can the btn12 btnode success? */
property ForceFailure_fail_btn12_cannot_succeed is absent drone/10/value (btnode[fail_btn12].rstatus=success)
prove ForceFailure_fail_btn12_cannot_succeed

/* Can the btn12 btnode return failure? */
property ForceFailure_fail_btn12_cannot_fail is absent  drone/10/value (btnode[fail_btn12].rstatus=failure)
prove ForceFailure_fail_btn12_cannot_fail

/* Can the btn12 btnode be halted? */
property ForceFailure_fail_btn12_cannot_be_halted is absent drone/10/state halted
prove ForceFailure_fail_btn12_cannot_be_halted

/* Can the btn12 btnode return running? */
property ForceFailure_fail_btn12_cannot_return_running is absent drone/10/state running
prove ForceFailure_fail_btn12_cannot_return_running

/* Can the btn12 btnode go in error? */
property ForceFailure_fail_btn12_cannot_error is absent drone/10/state error
prove ForceFailure_fail_btn12_cannot_error

/* Can the btn10 btnode properly execute? */
property Fallback_Fallback21_btn10_undoable is absent drone/11/state ether
prove Fallback_Fallback21_btn10_undoable

/* Can the btn10 btnode success? */
property Fallback_Fallback21_btn10_cannot_succeed is absent drone/11/value (btnode[Fallback21_btn10].rstatus=success)
prove Fallback_Fallback21_btn10_cannot_succeed

/* Can the btn10 btnode return failure? */
property Fallback_Fallback21_btn10_cannot_fail is absent  drone/11/value (btnode[Fallback21_btn10].rstatus=failure)
prove Fallback_Fallback21_btn10_cannot_fail

/* Can the btn10 btnode be halted? */
property Fallback_Fallback21_btn10_cannot_be_halted is absent drone/11/state halted
prove Fallback_Fallback21_btn10_cannot_be_halted

/* Can the btn10 btnode return running? */
property Fallback_Fallback21_btn10_cannot_return_running is absent drone/11/state running
prove Fallback_Fallback21_btn10_cannot_return_running

/* Can the btn10 btnode go in error? */
property Fallback_Fallback21_btn10_cannot_error is absent drone/11/state error
prove Fallback_Fallback21_btn10_cannot_error

/* Can the btn15 btnode properly execute? */
property Action_takeoff_btn15_undoable is absent drone/12/state ether
prove Action_takeoff_btn15_undoable

/* Can the btn15 btnode success? */
property Action_takeoff_btn15_cannot_succeed is absent drone/12/value (btnode[takeoff_btn15].rstatus=success)
prove Action_takeoff_btn15_cannot_succeed

/* Can the btn15 btnode return failure? */
property Action_takeoff_btn15_cannot_fail is absent  drone/12/value (btnode[takeoff_btn15].rstatus=failure)
prove Action_takeoff_btn15_cannot_fail

/* Can the btn15 btnode be halted? */
property Action_takeoff_btn15_cannot_be_halted is absent drone/12/state halted
prove Action_takeoff_btn15_cannot_be_halted

/* Can the btn15 btnode return running? */
property Action_takeoff_btn15_cannot_return_running is absent drone/12/state running
prove Action_takeoff_btn15_cannot_return_running

/* Can the btn17 btnode properly execute? */
property Action_camera_tracking_btn17_undoable is absent drone/13/state ether
prove Action_camera_tracking_btn17_undoable

/* Can the btn17 btnode success? */
property Action_camera_tracking_btn17_cannot_succeed is absent drone/13/value (btnode[camera_tracking_btn17].rstatus=success)
prove Action_camera_tracking_btn17_cannot_succeed

/* Can the btn17 btnode return failure? */
property Action_camera_tracking_btn17_cannot_fail is absent  drone/13/value (btnode[camera_tracking_btn17].rstatus=failure)
prove Action_camera_tracking_btn17_cannot_fail

/* Can the btn17 btnode be halted? */
property Action_camera_tracking_btn17_cannot_be_halted is absent drone/13/state halted
prove Action_camera_tracking_btn17_cannot_be_halted

/* Can the btn17 btnode return running? */
property Action_camera_tracking_btn17_cannot_return_running is absent drone/13/state running
prove Action_camera_tracking_btn17_cannot_return_running

/* Can the btn19 btnode properly execute? */
property Action_goto_waypoint_btn19_undoable is absent drone/14/state ether
prove Action_goto_waypoint_btn19_undoable

/* Can the btn19 btnode success? */
property Action_goto_waypoint_btn19_cannot_succeed is absent drone/14/value (btnode[goto_waypoint_btn19].rstatus=success)
prove Action_goto_waypoint_btn19_cannot_succeed

/* Can the btn19 btnode return failure? */
property Action_goto_waypoint_btn19_cannot_fail is absent  drone/14/value (btnode[goto_waypoint_btn19].rstatus=failure)
prove Action_goto_waypoint_btn19_cannot_fail

/* Can the btn19 btnode be halted? */
property Action_goto_waypoint_btn19_cannot_be_halted is absent drone/14/state halted
prove Action_goto_waypoint_btn19_cannot_be_halted

/* Can the btn19 btnode return running? */
property Action_goto_waypoint_btn19_cannot_return_running is absent drone/14/state running
prove Action_goto_waypoint_btn19_cannot_return_running

/* Can the btn20 btnode properly execute? */
property Action_goto_waypoint_btn20_undoable is absent drone/15/state ether
prove Action_goto_waypoint_btn20_undoable

/* Can the btn20 btnode success? */
property Action_goto_waypoint_btn20_cannot_succeed is absent drone/15/value (btnode[goto_waypoint_btn20].rstatus=success)
prove Action_goto_waypoint_btn20_cannot_succeed

/* Can the btn20 btnode return failure? */
property Action_goto_waypoint_btn20_cannot_fail is absent  drone/15/value (btnode[goto_waypoint_btn20].rstatus=failure)
prove Action_goto_waypoint_btn20_cannot_fail

/* Can the btn20 btnode be halted? */
property Action_goto_waypoint_btn20_cannot_be_halted is absent drone/15/state halted
prove Action_goto_waypoint_btn20_cannot_be_halted

/* Can the btn20 btnode return running? */
property Action_goto_waypoint_btn20_cannot_return_running is absent drone/15/state running
prove Action_goto_waypoint_btn20_cannot_return_running

/* Can the btn21 btnode properly execute? */
property Action_goto_waypoint_btn21_undoable is absent drone/16/state ether
prove Action_goto_waypoint_btn21_undoable

/* Can the btn21 btnode success? */
property Action_goto_waypoint_btn21_cannot_succeed is absent drone/16/value (btnode[goto_waypoint_btn21].rstatus=success)
prove Action_goto_waypoint_btn21_cannot_succeed

/* Can the btn21 btnode return failure? */
property Action_goto_waypoint_btn21_cannot_fail is absent  drone/16/value (btnode[goto_waypoint_btn21].rstatus=failure)
prove Action_goto_waypoint_btn21_cannot_fail

/* Can the btn21 btnode be halted? */
property Action_goto_waypoint_btn21_cannot_be_halted is absent drone/16/state halted
prove Action_goto_waypoint_btn21_cannot_be_halted

/* Can the btn21 btnode return running? */
property Action_goto_waypoint_btn21_cannot_return_running is absent drone/16/state running
prove Action_goto_waypoint_btn21_cannot_return_running

/* Can the btn22 btnode properly execute? */
property Action_goto_waypoint_btn22_undoable is absent drone/17/state ether
prove Action_goto_waypoint_btn22_undoable

/* Can the btn22 btnode success? */
property Action_goto_waypoint_btn22_cannot_succeed is absent drone/17/value (btnode[goto_waypoint_btn22].rstatus=success)
prove Action_goto_waypoint_btn22_cannot_succeed

/* Can the btn22 btnode return failure? */
property Action_goto_waypoint_btn22_cannot_fail is absent  drone/17/value (btnode[goto_waypoint_btn22].rstatus=failure)
prove Action_goto_waypoint_btn22_cannot_fail

/* Can the btn22 btnode be halted? */
property Action_goto_waypoint_btn22_cannot_be_halted is absent drone/17/state halted
prove Action_goto_waypoint_btn22_cannot_be_halted

/* Can the btn22 btnode return running? */
property Action_goto_waypoint_btn22_cannot_return_running is absent drone/17/state running
prove Action_goto_waypoint_btn22_cannot_return_running

/* Can the btn23 btnode properly execute? */
property Action_goto_waypoint_btn23_undoable is absent drone/18/state ether
prove Action_goto_waypoint_btn23_undoable

/* Can the btn23 btnode success? */
property Action_goto_waypoint_btn23_cannot_succeed is absent drone/18/value (btnode[goto_waypoint_btn23].rstatus=success)
prove Action_goto_waypoint_btn23_cannot_succeed

/* Can the btn23 btnode return failure? */
property Action_goto_waypoint_btn23_cannot_fail is absent  drone/18/value (btnode[goto_waypoint_btn23].rstatus=failure)
prove Action_goto_waypoint_btn23_cannot_fail

/* Can the btn23 btnode be halted? */
property Action_goto_waypoint_btn23_cannot_be_halted is absent drone/18/state halted
prove Action_goto_waypoint_btn23_cannot_be_halted

/* Can the btn23 btnode return running? */
property Action_goto_waypoint_btn23_cannot_return_running is absent drone/18/state running
prove Action_goto_waypoint_btn23_cannot_return_running

/* Can the btn24 btnode properly execute? */
property Action_goto_waypoint_btn24_undoable is absent drone/19/state ether
prove Action_goto_waypoint_btn24_undoable

/* Can the btn24 btnode success? */
property Action_goto_waypoint_btn24_cannot_succeed is absent drone/19/value (btnode[goto_waypoint_btn24].rstatus=success)
prove Action_goto_waypoint_btn24_cannot_succeed

/* Can the btn24 btnode return failure? */
property Action_goto_waypoint_btn24_cannot_fail is absent  drone/19/value (btnode[goto_waypoint_btn24].rstatus=failure)
prove Action_goto_waypoint_btn24_cannot_fail

/* Can the btn24 btnode be halted? */
property Action_goto_waypoint_btn24_cannot_be_halted is absent drone/19/state halted
prove Action_goto_waypoint_btn24_cannot_be_halted

/* Can the btn24 btnode return running? */
property Action_goto_waypoint_btn24_cannot_return_running is absent drone/19/state running
prove Action_goto_waypoint_btn24_cannot_return_running

/* Can the btn18 btnode properly execute? */
property Sequence_Sequence37_btn18_undoable is absent drone/20/state ether
prove Sequence_Sequence37_btn18_undoable

/* Can the btn18 btnode success? */
property Sequence_Sequence37_btn18_cannot_succeed is absent drone/20/value (btnode[Sequence37_btn18].rstatus=success)
prove Sequence_Sequence37_btn18_cannot_succeed

/* Can the btn18 btnode return failure? */
property Sequence_Sequence37_btn18_cannot_fail is absent  drone/20/value (btnode[Sequence37_btn18].rstatus=failure)
prove Sequence_Sequence37_btn18_cannot_fail

/* Can the btn18 btnode be halted? */
property Sequence_Sequence37_btn18_cannot_be_halted is absent drone/20/state halted
prove Sequence_Sequence37_btn18_cannot_be_halted

/* Can the btn18 btnode return running? */
property Sequence_Sequence37_btn18_cannot_return_running is absent drone/20/state running
prove Sequence_Sequence37_btn18_cannot_return_running

/* Can the btn18 btnode go in error? */
property Sequence_Sequence37_btn18_cannot_error is absent drone/20/state error
prove Sequence_Sequence37_btn18_cannot_error

/* Can the btn16 btnode properly execute? */
property Parallel_Parallel33_btn16_undoable is absent drone/21/state ether
prove Parallel_Parallel33_btn16_undoable

/* Can the btn16 btnode success? */
property Parallel_Parallel33_btn16_cannot_succeed is absent drone/21/value (btnode[Parallel33_btn16].rstatus=success)
prove Parallel_Parallel33_btn16_cannot_succeed

/* Can the btn16 btnode return failure? */
property Parallel_Parallel33_btn16_cannot_fail is absent  drone/21/value (btnode[Parallel33_btn16].rstatus=failure)
prove Parallel_Parallel33_btn16_cannot_fail

/* Can the btn16 btnode be halted? */
property Parallel_Parallel33_btn16_cannot_be_halted is absent drone/21/state halted
prove Parallel_Parallel33_btn16_cannot_be_halted

/* Can the btn25 btnode properly execute? */
property Action_goto_waypoint_btn25_undoable is absent drone/22/state ether
prove Action_goto_waypoint_btn25_undoable

/* Can the btn25 btnode success? */
property Action_goto_waypoint_btn25_cannot_succeed is absent drone/22/value (btnode[goto_waypoint_btn25].rstatus=success)
prove Action_goto_waypoint_btn25_cannot_succeed

/* Can the btn25 btnode return failure? */
property Action_goto_waypoint_btn25_cannot_fail is absent  drone/22/value (btnode[goto_waypoint_btn25].rstatus=failure)
prove Action_goto_waypoint_btn25_cannot_fail

/* Can the btn25 btnode be halted? */
property Action_goto_waypoint_btn25_cannot_be_halted is absent drone/22/state halted
prove Action_goto_waypoint_btn25_cannot_be_halted

/* Can the btn25 btnode return running? */
property Action_goto_waypoint_btn25_cannot_return_running is absent drone/22/state running
prove Action_goto_waypoint_btn25_cannot_return_running

/* Can the btn26 btnode properly execute? */
property Action_land_btn26_undoable is absent drone/23/state ether
prove Action_land_btn26_undoable

/* Can the btn26 btnode success? */
property Action_land_btn26_cannot_succeed is absent drone/23/value (btnode[land_btn26].rstatus=success)
prove Action_land_btn26_cannot_succeed

/* Can the btn26 btnode return failure? */
property Action_land_btn26_cannot_fail is absent  drone/23/value (btnode[land_btn26].rstatus=failure)
prove Action_land_btn26_cannot_fail

/* Can the btn26 btnode be halted? */
property Action_land_btn26_cannot_be_halted is absent drone/23/state halted
prove Action_land_btn26_cannot_be_halted

/* Can the btn26 btnode return running? */
property Action_land_btn26_cannot_return_running is absent drone/23/state running
prove Action_land_btn26_cannot_return_running

/* Can the btn27 btnode properly execute? */
property Action_shutdown_drone_btn27_undoable is absent drone/24/state ether
prove Action_shutdown_drone_btn27_undoable

/* Can the btn27 btnode success? */
property Action_shutdown_drone_btn27_cannot_succeed is absent drone/24/value (btnode[shutdown_drone_btn27].rstatus=success)
prove Action_shutdown_drone_btn27_cannot_succeed

/* Can the btn27 btnode return failure? */
property Action_shutdown_drone_btn27_cannot_fail is absent  drone/24/value (btnode[shutdown_drone_btn27].rstatus=failure)
prove Action_shutdown_drone_btn27_cannot_fail

/* Can the btn27 btnode be halted? */
property Action_shutdown_drone_btn27_cannot_be_halted is absent drone/24/state halted
prove Action_shutdown_drone_btn27_cannot_be_halted

/* Can the btn27 btnode return running? */
property Action_shutdown_drone_btn27_cannot_return_running is absent drone/24/state running
prove Action_shutdown_drone_btn27_cannot_return_running

/* Can the btn14 btnode properly execute? */
property Sequence_Sequence29_btn14_undoable is absent drone/25/state ether
prove Sequence_Sequence29_btn14_undoable

/* Can the btn14 btnode success? */
property Sequence_Sequence29_btn14_cannot_succeed is absent drone/25/value (btnode[Sequence29_btn14].rstatus=success)
prove Sequence_Sequence29_btn14_cannot_succeed

/* Can the btn14 btnode return failure? */
property Sequence_Sequence29_btn14_cannot_fail is absent  drone/25/value (btnode[Sequence29_btn14].rstatus=failure)
prove Sequence_Sequence29_btn14_cannot_fail

/* Can the btn14 btnode be halted? */
property Sequence_Sequence29_btn14_cannot_be_halted is absent drone/25/state halted
prove Sequence_Sequence29_btn14_cannot_be_halted

/* Can the btn14 btnode return running? */
property Sequence_Sequence29_btn14_cannot_return_running is absent drone/25/state running
prove Sequence_Sequence29_btn14_cannot_return_running

/* Can the btn14 btnode go in error? */
property Sequence_Sequence29_btn14_cannot_error is absent drone/25/state error
prove Sequence_Sequence29_btn14_cannot_error

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

/* Can the btn5 btnode success? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_succeed is absent drone/26/value (btnode[ReactiveSequence11_btn5].rstatus=success)
prove ReactiveSequence_ReactiveSequence11_btn5_cannot_succeed

/* Can the btn5 btnode return failure? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_fail is absent  drone/26/value (btnode[ReactiveSequence11_btn5].rstatus=failure)
prove ReactiveSequence_ReactiveSequence11_btn5_cannot_fail

/* Can the btn5 btnode be halted? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_be_halted is absent drone/26/state halted
prove ReactiveSequence_ReactiveSequence11_btn5_cannot_be_halted

/* Can the btn5 btnode return running? */
property ReactiveSequence_ReactiveSequence11_btn5_cannot_return_running is absent drone/26/state running
prove ReactiveSequence_ReactiveSequence11_btn5_cannot_return_running

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

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

/* Can the btn1 btnode success? */
property Sequence_Sequence3_btn1_cannot_succeed is absent drone/27/value (btnode[Sequence3_btn1].rstatus=success)
prove Sequence_Sequence3_btn1_cannot_succeed

/* Can the btn1 btnode return failure? */
property Sequence_Sequence3_btn1_cannot_fail is absent  drone/27/value (btnode[Sequence3_btn1].rstatus=failure)
prove Sequence_Sequence3_btn1_cannot_fail

/* Can the btn1 btnode be halted? */
property Sequence_Sequence3_btn1_cannot_be_halted is absent drone/27/state halted
prove Sequence_Sequence3_btn1_cannot_be_halted

/* Can the btn1 btnode return running? */
property Sequence_Sequence3_btn1_cannot_return_running is absent drone/27/state running
prove Sequence_Sequence3_btn1_cannot_return_running

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

/* Can the drone btnode properly execute? */
property BehaviorTree_BehaviorTree1_drone_undoable is absent drone/28/state ether
prove BehaviorTree_BehaviorTree1_drone_undoable

/* Can the drone btnode success? */
property BehaviorTree_BehaviorTree1_drone_cannot_succeed is absent drone/28/value (btnode[BehaviorTree1_drone].rstatus=success)
prove BehaviorTree_BehaviorTree1_drone_cannot_succeed

/* Can the drone btnode return failure? */
property BehaviorTree_BehaviorTree1_drone_cannot_fail is absent  drone/28/value (btnode[BehaviorTree1_drone].rstatus=failure)
prove BehaviorTree_BehaviorTree1_drone_cannot_fail

/* Can the drone btnode be halted? */
property BehaviorTree_BehaviorTree1_drone_cannot_be_halted is absent drone/28/state halted
prove BehaviorTree_BehaviorTree1_drone_cannot_be_halted

/* Can the drone btnode return running? */
property BehaviorTree_BehaviorTree1_drone_cannot_return_running is absent drone/28/state running
prove BehaviorTree_BehaviorTree1_drone_cannot_return_running

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