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

/*
								 * This Behavior Tree FIACRE model is for verification with the TINA tools.
	 */


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

type btnode_caller is union
	  None
	| caller_Eval9_btn4
	| caller_Eval13_btn6
	| caller_Sequence7_btn3
	| caller_Eval17_btn8
	| caller_Eval21_btn10
	| caller_Sequence15_btn7
	| caller_Sequence23_btn11
	| caller_Fallback5_btn2
	| caller_KeepRunningUntilFailure3_btn1
	| caller_BehaviorTree1_mars_rover2
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 Eval9_btn4: 0..0 is 0
const UnfoldPanels_unfold_panels: 1..1 is 1
const Eval13_btn6: 2..2 is 2
const Sequence7_btn3: 3..3 is 3
const Eval17_btn8: 4..4 is 4
const Hibernate_hibernate: 5..5 is 5
const Eval21_btn10: 6..6 is 6
const Sequence15_btn7: 7..7 is 7
const DataReady_dataready: 8..8 is 8
const Send_send: 9..9 is 9
const Sequence23_btn11: 10..10 is 10
const Fallback5_btn2: 11..11 is 11
const KeepRunningUntilFailure3_btn1: 12..12 is 12
const BehaviorTree1_mars_rover2: 13..13 is 13

type btnode_array is array 14 of btnode_record


/* state variable integer types*/

/* state variable FSM types*/
type sv_meteo is union
	  MInit
	| Normal
	| Storm
end

type sv_battery is union
	  BInit
	| Good
	| Low
end

type sv_panel is union
	  PInit
	| Folded
	| Unfolded
end


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

process sv_meteo_automata (&meteo:sv_meteo) is

	states MInit, error, Normal , Storm 

	from MInit
		wait [0,0];
		select
			on (meteo = Normal);
			to Normal
		[]
			on (meteo = Storm);
			to Storm
		end

	from Normal
		wait [0,0];
		select
			on (meteo = MInit);
			to error
		[]
			on (meteo = Storm);
			to Storm
		end

	from Storm
		wait [0,0];
		select
			on (meteo = MInit);
			to error
		[]
			on (meteo = Normal);
			to Normal
		end

process sv_battery_automata (&battery:sv_battery) is

	states BInit, error, Good , Low 

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

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

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

process sv_panel_automata (&panel:sv_panel) is

	states PInit, error, Folded , Unfolded 

	from PInit
		wait [0,0];
		select
			on (panel = Folded);
			to Folded
		[]
			on (panel = Unfolded);
			to Unfolded
		end

	from Folded
		wait [0,0];
		select
			on (panel = PInit);
			to error
		[]
			on (panel = Unfolded);
			to Unfolded
		end

	from Unfolded
		wait [0,0];
		select
			on (panel = PInit);
			to error
		[]
			on (panel = Folded);
			to Folded
		end

process btnode_Eval9_btn4 (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

	from halt
		wait [0,0];
	to halted

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

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_UnfoldPanels_unfold_panels (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_Eval13_btn6 (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
		// will assign: panel := Unfolded
		panel := Unfolded;
		to success

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Sequence7_btn3 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Eval9_btn4, Eval9_btn4_done,
		UnfoldPanels_unfold_panels, UnfoldPanels_unfold_panels_done,
		Eval13_btn6, Eval13_btn6_done,
		done, ether

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

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

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

	from halt_wait
		on (
			(btnode[Eval9_btn4].caller = None) and
			(btnode[UnfoldPanels_unfold_panels].caller = None) and
			(btnode[Eval13_btn6].caller = None) and
			true);
		to halted

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to Eval9_btn4 end;
		if (next_seq = 2) then to UnfoldPanels_unfold_panels end;
		if (next_seq = 3) then to Eval13_btn6 end;
		to error

	from Eval9_btn4
		wait [0,0];
		btnode[Eval9_btn4].caller := caller_Sequence7_btn3;
		to Eval9_btn4_done

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

	from UnfoldPanels_unfold_panels
		wait [0,0];
		btnode[UnfoldPanels_unfold_panels].caller := caller_Sequence7_btn3;
		to UnfoldPanels_unfold_panels_done

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

	from Eval13_btn6
		wait [0,0];
		btnode[Eval13_btn6].caller := caller_Sequence7_btn3;
		to Eval13_btn6_done

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

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

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Eval17_btn8 (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

	from halt
		wait [0,0];
	to halted

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

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_Hibernate_hibernate (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_Eval21_btn10 (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

	from start_
		wait [0,0];
		on (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];
		// will assign: panel := Folded
		panel := Folded;
		to success

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Sequence15_btn7 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Eval17_btn8, Eval17_btn8_done,
		Hibernate_hibernate, Hibernate_hibernate_done,
		Eval21_btn10, Eval21_btn10_done,
		done, ether

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

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

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

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

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to Eval17_btn8 end;
		if (next_seq = 2) then to Hibernate_hibernate end;
		if (next_seq = 3) then to Eval21_btn10 end;
		to error

	from Eval17_btn8
		wait [0,0];
		btnode[Eval17_btn8].caller := caller_Sequence15_btn7;
		to Eval17_btn8_done

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

	from Hibernate_hibernate
		wait [0,0];
		btnode[Hibernate_hibernate].caller := caller_Sequence15_btn7;
		to Hibernate_hibernate_done

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

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

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

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_DataReady_dataready (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_Send_send (&btnode: btnode_array, &meteo: sv_meteo, &battery: sv_battery, &panel: sv_panel) is

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

	var ignorep: nat, ignoreb: bool

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

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

	from halted
		wait [0,0];
		to failure

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

	from ether
		wait [0,0];
	to start_

process btnode_Sequence23_btn11 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		DataReady_dataready, DataReady_dataready_done,
		Send_send, Send_send_done,
		done, ether

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

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

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

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

	from tick_node
		wait [1,1];
		if (next_seq = 1) then to DataReady_dataready end;
		if (next_seq = 2) then to Send_send end;
		to error

	from DataReady_dataready
		wait [0,0];
		btnode[DataReady_dataready].caller := caller_Sequence23_btn11;
		to DataReady_dataready_done

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

	from Send_send
		wait [0,0];
		btnode[Send_send].caller := caller_Sequence23_btn11;
		to Send_send_done

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

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

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_Fallback5_btn2 (&btnode: btnode_array) is

	states start_, tick_node, success, failure, halt, halted, halt_wait, running, error,
		Sequence7_btn3, Sequence7_btn3_done,
		Sequence15_btn7, Sequence15_btn7_done,
		Sequence23_btn11, Sequence23_btn11_done,
		done, ether

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

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

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

	from halt_wait
		on (
			(btnode[Sequence7_btn3].caller = None) and
			(btnode[Sequence15_btn7].caller = None) and
			(btnode[Sequence23_btn11].caller = None) and
			true);
		to halted

	from tick_node
		wait [1,1];
		if (next_fb = 1) then to Sequence7_btn3 end;
		if (next_fb = 2) then to Sequence15_btn7 end;
		if (next_fb = 3) then to Sequence23_btn11 end;
		to error

	from Sequence7_btn3
		wait [0,0];
		btnode[Sequence7_btn3].caller := caller_Fallback5_btn2;
		to Sequence7_btn3_done

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

	from Sequence15_btn7
		wait [0,0];
		btnode[Sequence15_btn7].caller := caller_Fallback5_btn2;
		to Sequence15_btn7_done

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

	from Sequence23_btn11
		wait [0,0];
		btnode[Sequence23_btn11].caller := caller_Fallback5_btn2;
		to Sequence23_btn11_done

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

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

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

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

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

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

	from ether
		wait [0,0];
	to start_

process btnode_KeepRunningUntilFailure3_btn1 (&btnode: btnode_array) is

	states start_, tick_node, failure, halt, halted, halt_wait, running, error,
		Fallback5_btn2, Fallback5_btn2_done,
		done, ether

	var ignorep: nat, ignoreb: bool

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

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

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

	from tick_node
		wait [1,1];
	to Fallback5_btn2

	from Fallback5_btn2
		wait [0,0];
		btnode[Fallback5_btn2].caller := caller_KeepRunningUntilFailure3_btn1;
		to Fallback5_btn2_done

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

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

	from halted
		wait [0,0];
		to failure

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

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

	from ether
		wait [0,0];
	to start_

process btnode_BehaviorTree1_mars_rover2 (&btnode: btnode_array) is

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

	var ignorep: nat, ignoreb: bool

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

	from halt
		wait [0,0];
	to halted

	from tick_node
		wait [1,1];
	to KeepRunningUntilFailure3_btn1

	from KeepRunningUntilFailure3_btn1
		wait [0,0];
		btnode[KeepRunningUntilFailure3_btn1].caller := caller_BehaviorTree1_mars_rover2;
		to KeepRunningUntilFailure3_btn1_done

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

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

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

	from halted
		wait [0,0];
		to failure

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

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

component mars_rover2 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 = caller_BehaviorTree1_mars_rover2, ArgIndex = 0, rstatus = no_ret_status}],
		// **** state variables ****,
		meteo: sv_meteo := MInit,
		battery: sv_battery := BInit,
		panel: sv_panel := PInit

par * in
// **** state variables processes ****
   sv_meteo_automata(&meteo)
|| sv_battery_automata(&battery)
|| sv_panel_automata(&panel)
// **** btnode processes ****
|| btnode_Eval9_btn4(&btnode, &meteo, &battery, &panel)
|| btnode_UnfoldPanels_unfold_panels(&btnode, &meteo, &battery, &panel)
|| btnode_Eval13_btn6(&btnode, &meteo, &battery, &panel)
|| btnode_Sequence7_btn3(&btnode)
|| btnode_Eval17_btn8(&btnode, &meteo, &battery, &panel)
|| btnode_Hibernate_hibernate(&btnode, &meteo, &battery, &panel)
|| btnode_Eval21_btn10(&btnode, &meteo, &battery, &panel)
|| btnode_Sequence15_btn7(&btnode)
|| btnode_DataReady_dataready(&btnode, &meteo, &battery, &panel)
|| btnode_Send_send(&btnode, &meteo, &battery, &panel)
|| btnode_Sequence23_btn11(&btnode)
|| btnode_Fallback5_btn2(&btnode)
|| btnode_KeepRunningUntilFailure3_btn1(&btnode)
|| btnode_BehaviorTree1_mars_rover2(&btnode)
// **** end of the component ****

end


mars_rover2

/* Some properties to model check */

/* Can the btn4 btnode properly execute? */
property Eval_Eval9_btn4_undoable is absent mars_rover2/4/state ether
prove Eval_Eval9_btn4_undoable

/* Can the btn4 btnode success? */
property Eval_Eval9_btn4_cannot_succeed is absent mars_rover2/4/value (btnode[Eval9_btn4].rstatus=success)
prove Eval_Eval9_btn4_cannot_succeed

/* Can the btn4 btnode return failure? */
property Eval_Eval9_btn4_cannot_fail is absent  mars_rover2/4/value (btnode[Eval9_btn4].rstatus=failure)
prove Eval_Eval9_btn4_cannot_fail

/* Can the btn4 btnode be halted? */
property Eval_Eval9_btn4_cannot_be_halted is absent mars_rover2/4/state halted
prove Eval_Eval9_btn4_cannot_be_halted

/* Can the unfold_panels btnode properly execute? */
property Action_UnfoldPanels_unfold_panels_undoable is absent mars_rover2/5/state ether
prove Action_UnfoldPanels_unfold_panels_undoable

/* Can the unfold_panels btnode success? */
property Action_UnfoldPanels_unfold_panels_cannot_succeed is absent mars_rover2/5/value (btnode[UnfoldPanels_unfold_panels].rstatus=success)
prove Action_UnfoldPanels_unfold_panels_cannot_succeed

/* Can the unfold_panels btnode return failure? */
property Action_UnfoldPanels_unfold_panels_cannot_fail is absent  mars_rover2/5/value (btnode[UnfoldPanels_unfold_panels].rstatus=failure)
prove Action_UnfoldPanels_unfold_panels_cannot_fail

/* Can the unfold_panels btnode be halted? */
property Action_UnfoldPanels_unfold_panels_cannot_be_halted is absent mars_rover2/5/state halted
prove Action_UnfoldPanels_unfold_panels_cannot_be_halted

/* Can the btn6 btnode properly execute? */
property Eval_Eval13_btn6_undoable is absent mars_rover2/6/state ether
prove Eval_Eval13_btn6_undoable

/* Can the btn6 btnode success? */
property Eval_Eval13_btn6_cannot_succeed is absent mars_rover2/6/value (btnode[Eval13_btn6].rstatus=success)
prove Eval_Eval13_btn6_cannot_succeed

/* Can the btn6 btnode return failure? */
property Eval_Eval13_btn6_cannot_fail is absent  mars_rover2/6/value (btnode[Eval13_btn6].rstatus=failure)
prove Eval_Eval13_btn6_cannot_fail

/* Can the btn6 btnode be halted? */
property Eval_Eval13_btn6_cannot_be_halted is absent mars_rover2/6/state halted
prove Eval_Eval13_btn6_cannot_be_halted

/* Can the btn3 btnode properly execute? */
property Sequence_Sequence7_btn3_undoable is absent mars_rover2/7/state ether
prove Sequence_Sequence7_btn3_undoable

/* Can the btn3 btnode success? */
property Sequence_Sequence7_btn3_cannot_succeed is absent mars_rover2/7/value (btnode[Sequence7_btn3].rstatus=success)
prove Sequence_Sequence7_btn3_cannot_succeed

/* Can the btn3 btnode return failure? */
property Sequence_Sequence7_btn3_cannot_fail is absent  mars_rover2/7/value (btnode[Sequence7_btn3].rstatus=failure)
prove Sequence_Sequence7_btn3_cannot_fail

/* Can the btn3 btnode be halted? */
property Sequence_Sequence7_btn3_cannot_be_halted is absent mars_rover2/7/state halted
prove Sequence_Sequence7_btn3_cannot_be_halted

/* Can the btn3 btnode return running? */
property Sequence_Sequence7_btn3_cannot_return_running is absent mars_rover2/7/state running
prove Sequence_Sequence7_btn3_cannot_return_running

/* Can the btn3 btnode go in error? */
property Sequence_Sequence7_btn3_cannot_error is absent mars_rover2/7/state error
prove Sequence_Sequence7_btn3_cannot_error

/* Can the btn8 btnode properly execute? */
property Eval_Eval17_btn8_undoable is absent mars_rover2/8/state ether
prove Eval_Eval17_btn8_undoable

/* Can the btn8 btnode success? */
property Eval_Eval17_btn8_cannot_succeed is absent mars_rover2/8/value (btnode[Eval17_btn8].rstatus=success)
prove Eval_Eval17_btn8_cannot_succeed

/* Can the btn8 btnode return failure? */
property Eval_Eval17_btn8_cannot_fail is absent  mars_rover2/8/value (btnode[Eval17_btn8].rstatus=failure)
prove Eval_Eval17_btn8_cannot_fail

/* Can the btn8 btnode be halted? */
property Eval_Eval17_btn8_cannot_be_halted is absent mars_rover2/8/state halted
prove Eval_Eval17_btn8_cannot_be_halted

/* Can the hibernate btnode properly execute? */
property Action_Hibernate_hibernate_undoable is absent mars_rover2/9/state ether
prove Action_Hibernate_hibernate_undoable

/* Can the hibernate btnode success? */
property Action_Hibernate_hibernate_cannot_succeed is absent mars_rover2/9/value (btnode[Hibernate_hibernate].rstatus=success)
prove Action_Hibernate_hibernate_cannot_succeed

/* Can the hibernate btnode return failure? */
property Action_Hibernate_hibernate_cannot_fail is absent  mars_rover2/9/value (btnode[Hibernate_hibernate].rstatus=failure)
prove Action_Hibernate_hibernate_cannot_fail

/* Can the hibernate btnode be halted? */
property Action_Hibernate_hibernate_cannot_be_halted is absent mars_rover2/9/state halted
prove Action_Hibernate_hibernate_cannot_be_halted

/* Can the btn10 btnode properly execute? */
property Eval_Eval21_btn10_undoable is absent mars_rover2/10/state ether
prove Eval_Eval21_btn10_undoable

/* Can the btn10 btnode success? */
property Eval_Eval21_btn10_cannot_succeed is absent mars_rover2/10/value (btnode[Eval21_btn10].rstatus=success)
prove Eval_Eval21_btn10_cannot_succeed

/* Can the btn10 btnode return failure? */
property Eval_Eval21_btn10_cannot_fail is absent  mars_rover2/10/value (btnode[Eval21_btn10].rstatus=failure)
prove Eval_Eval21_btn10_cannot_fail

/* Can the btn10 btnode be halted? */
property Eval_Eval21_btn10_cannot_be_halted is absent mars_rover2/10/state halted
prove Eval_Eval21_btn10_cannot_be_halted

/* Can the btn7 btnode properly execute? */
property Sequence_Sequence15_btn7_undoable is absent mars_rover2/11/state ether
prove Sequence_Sequence15_btn7_undoable

/* Can the btn7 btnode success? */
property Sequence_Sequence15_btn7_cannot_succeed is absent mars_rover2/11/value (btnode[Sequence15_btn7].rstatus=success)
prove Sequence_Sequence15_btn7_cannot_succeed

/* Can the btn7 btnode return failure? */
property Sequence_Sequence15_btn7_cannot_fail is absent  mars_rover2/11/value (btnode[Sequence15_btn7].rstatus=failure)
prove Sequence_Sequence15_btn7_cannot_fail

/* Can the btn7 btnode be halted? */
property Sequence_Sequence15_btn7_cannot_be_halted is absent mars_rover2/11/state halted
prove Sequence_Sequence15_btn7_cannot_be_halted

/* Can the btn7 btnode return running? */
property Sequence_Sequence15_btn7_cannot_return_running is absent mars_rover2/11/state running
prove Sequence_Sequence15_btn7_cannot_return_running

/* Can the btn7 btnode go in error? */
property Sequence_Sequence15_btn7_cannot_error is absent mars_rover2/11/state error
prove Sequence_Sequence15_btn7_cannot_error

/* Can the dataready btnode properly execute? */
property Action_DataReady_dataready_undoable is absent mars_rover2/12/state ether
prove Action_DataReady_dataready_undoable

/* Can the dataready btnode success? */
property Action_DataReady_dataready_cannot_succeed is absent mars_rover2/12/value (btnode[DataReady_dataready].rstatus=success)
prove Action_DataReady_dataready_cannot_succeed

/* Can the dataready btnode return failure? */
property Action_DataReady_dataready_cannot_fail is absent  mars_rover2/12/value (btnode[DataReady_dataready].rstatus=failure)
prove Action_DataReady_dataready_cannot_fail

/* Can the dataready btnode be halted? */
property Action_DataReady_dataready_cannot_be_halted is absent mars_rover2/12/state halted
prove Action_DataReady_dataready_cannot_be_halted

/* Can the send btnode properly execute? */
property Action_Send_send_undoable is absent mars_rover2/13/state ether
prove Action_Send_send_undoable

/* Can the send btnode success? */
property Action_Send_send_cannot_succeed is absent mars_rover2/13/value (btnode[Send_send].rstatus=success)
prove Action_Send_send_cannot_succeed

/* Can the send btnode return failure? */
property Action_Send_send_cannot_fail is absent  mars_rover2/13/value (btnode[Send_send].rstatus=failure)
prove Action_Send_send_cannot_fail

/* Can the send btnode be halted? */
property Action_Send_send_cannot_be_halted is absent mars_rover2/13/state halted
prove Action_Send_send_cannot_be_halted

/* Can the btn11 btnode properly execute? */
property Sequence_Sequence23_btn11_undoable is absent mars_rover2/14/state ether
prove Sequence_Sequence23_btn11_undoable

/* Can the btn11 btnode success? */
property Sequence_Sequence23_btn11_cannot_succeed is absent mars_rover2/14/value (btnode[Sequence23_btn11].rstatus=success)
prove Sequence_Sequence23_btn11_cannot_succeed

/* Can the btn11 btnode return failure? */
property Sequence_Sequence23_btn11_cannot_fail is absent  mars_rover2/14/value (btnode[Sequence23_btn11].rstatus=failure)
prove Sequence_Sequence23_btn11_cannot_fail

/* Can the btn11 btnode be halted? */
property Sequence_Sequence23_btn11_cannot_be_halted is absent mars_rover2/14/state halted
prove Sequence_Sequence23_btn11_cannot_be_halted

/* Can the btn11 btnode return running? */
property Sequence_Sequence23_btn11_cannot_return_running is absent mars_rover2/14/state running
prove Sequence_Sequence23_btn11_cannot_return_running

/* Can the btn11 btnode go in error? */
property Sequence_Sequence23_btn11_cannot_error is absent mars_rover2/14/state error
prove Sequence_Sequence23_btn11_cannot_error

/* Can the btn2 btnode properly execute? */
property Fallback_Fallback5_btn2_undoable is absent mars_rover2/15/state ether
prove Fallback_Fallback5_btn2_undoable

/* Can the btn2 btnode success? */
property Fallback_Fallback5_btn2_cannot_succeed is absent mars_rover2/15/value (btnode[Fallback5_btn2].rstatus=success)
prove Fallback_Fallback5_btn2_cannot_succeed

/* Can the btn2 btnode return failure? */
property Fallback_Fallback5_btn2_cannot_fail is absent  mars_rover2/15/value (btnode[Fallback5_btn2].rstatus=failure)
prove Fallback_Fallback5_btn2_cannot_fail

/* Can the btn2 btnode be halted? */
property Fallback_Fallback5_btn2_cannot_be_halted is absent mars_rover2/15/state halted
prove Fallback_Fallback5_btn2_cannot_be_halted

/* Can the btn2 btnode return running? */
property Fallback_Fallback5_btn2_cannot_return_running is absent mars_rover2/15/state running
prove Fallback_Fallback5_btn2_cannot_return_running

/* Can the btn2 btnode go in error? */
property Fallback_Fallback5_btn2_cannot_error is absent mars_rover2/15/state error
prove Fallback_Fallback5_btn2_cannot_error

/* Can the btn1 btnode properly execute? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_undoable is absent mars_rover2/16/state ether
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_undoable

/* Can the btn1 btnode success? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_succeed is absent mars_rover2/16/value (btnode[KeepRunningUntilFailure3_btn1].rstatus=success)
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_succeed

/* Can the btn1 btnode return failure? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_fail is absent  mars_rover2/16/value (btnode[KeepRunningUntilFailure3_btn1].rstatus=failure)
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_fail

/* Can the btn1 btnode be halted? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_be_halted is absent mars_rover2/16/state halted
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_be_halted

/* Can the btn1 btnode return running? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_return_running is absent mars_rover2/16/state running
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_return_running

/* Can the btn1 btnode go in error? */
property KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_error is absent mars_rover2/16/state error
prove KeepRunningUntilFailure_KeepRunningUntilFailure3_btn1_cannot_error

/* Can the mars_rover2 btnode properly execute? */
property BehaviorTree_BehaviorTree1_mars_rover2_undoable is absent mars_rover2/17/state ether
prove BehaviorTree_BehaviorTree1_mars_rover2_undoable

/* Can the mars_rover2 btnode success? */
property BehaviorTree_BehaviorTree1_mars_rover2_cannot_succeed is absent mars_rover2/17/value (btnode[BehaviorTree1_mars_rover2].rstatus=success)
prove BehaviorTree_BehaviorTree1_mars_rover2_cannot_succeed

/* Can the mars_rover2 btnode return failure? */
property BehaviorTree_BehaviorTree1_mars_rover2_cannot_fail is absent  mars_rover2/17/value (btnode[BehaviorTree1_mars_rover2].rstatus=failure)
prove BehaviorTree_BehaviorTree1_mars_rover2_cannot_fail

/* Can the mars_rover2 btnode be halted? */
property BehaviorTree_BehaviorTree1_mars_rover2_cannot_be_halted is absent mars_rover2/17/state halted
prove BehaviorTree_BehaviorTree1_mars_rover2_cannot_be_halted

/* Can the mars_rover2 btnode return running? */
property BehaviorTree_BehaviorTree1_mars_rover2_cannot_return_running is absent mars_rover2/17/state running
prove BehaviorTree_BehaviorTree1_mars_rover2_cannot_return_running

/* Can the mars_rover2 btnode go in error? */
property BehaviorTree_BehaviorTree1_mars_rover2_cannot_error is absent mars_rover2/17/state error
prove BehaviorTree_BehaviorTree1_mars_rover2_cannot_error
/*End of File */