Project

General

Profile

History

Documentation for BT2Fiacre

Félix Ingrand.

The BT2Fiacre tool takes a Behavior Tree (BT) as input and produces an equivalent Fiacre formal model, which can then be used with the Tina toolbox (to prove some formal properties using model checking), but also with the Hippo engine to execute the equivalent formal model of the BT.

To perform the translation from BT to Fiacre, a number of clarifications in the BT semantics had to be made. This is in fact one advantage of transforming the BT in a formal model, one needs to make explicit some of the unspecified behaviors of BT, and thus clarify what was often left to the implementer choice. For example, what should be done with running branches when a Parallel node has succeeded or failed. Should we wait for those running branches? halt them? Similarly, for ReactiveSequence node, if a branch fails, while there are other following branches still running.

Note Fiacre also offers nice features such as explicit time representation. For example, one could specify that the BT tick takes a particular time value, or that some BT Actions (presumably asynchronous ones) take some time to execute within a given time interval.

The current status of this work is best illustrated with some examples, both managing a drone surveying an area with its camera, while monitoring its battery energy level and localization accuracy. The drone simulation (and real execution) is presented and described here (drone application/simulation at LAAS)

Examples

Simple Example (drone1)

The following BT implements a mission for a drone which surveys an area in search of interesting object with its camera. It monitors its battery and its localization covariance in parallel and lands if either fails, and then fails the mission.

The corresponding BT is in the file the drone1.btf file in the examples sub directory. Even if we are using a lisp like syntax, the behavior tree uses and implements well known BT node types and most additional keywords and arguments are self explanatory. Condition and Action are implemented with Fiacre/Hippo externs and tasks. These externs and tasks are linked to the GenoM components (services and ports) used to fly the drone. The Action and Condition nodes have an :ID field which points to the name of the Hippo task which implements the Action/Condition and :args is the arguments list passed for this particular call (if any).

( ;;; drone1.btf
 (BehaviorTree
  :name drone
  (Sequence
   (ParallelAll :wait 1 ; if wait is 1, will wait the running branch if one fails
    (Action :ID start_drone)
    (Action :ID start_camera))
   (ReactiveSequence
    (Fallback
     (Condition :ID battery_ok) ; check if the battery is OK
     (ForceFailure :ID fail ; if not, just land and fail
      (Action :ID land)))
    (Fallback
     (Condition :ID localization_ok) ;same for localization
     (ForceFailure :ID fail
      (Action :ID land)))
    (Sequence
     (Action :ID takeoff :args (height 1.0 duration 0))
     (Parallel :success 1 :wait 0 ; If either the camera_tracking or the nav succeed... we are done.
      (Action :ID camera_tracking)
      (Sequence
       (Action :ID goto_waypoint :args (x -3 y -3 z 5 yaw 0 duration 0))
       (Action :ID goto_waypoint :args (x -1.5 y 3 z 5 yaw 0 duration 0))
       (Action :ID goto_waypoint :args (x 0 y -3 z 5 yaw 0 duration 0))
       (Action :ID goto_waypoint :args (x 1.5 y 3 z 5 yaw 0 duration 0))
       (Action :ID goto_waypoint :args (x 3 y -3 z 5 yaw 0 duration 0))
       (Action :ID goto_waypoint :args (x 3 y -3 z 5 yaw 0 duration 0))))
     (Action :ID goto_waypoint :args (x 0 y 0 z 5 yaw 1.4 duration 0))
     (Action :ID land)
     (Action :ID shutdown_drone)
     )))))

From this BT definition the bt2fiacre program automatically produces the following Fiacre (Hippo) model (assuming you have installed bt2fiacre, the Makefile in the examples directory will build it for you).

Drone1 Fiacre model

Drone1 Fiacre Hippo model

When being executed, you get a screen like this one (provided you started the proper Drone1 experiment). This assumes you have TCL/TK installed along graphiz (which provides the tcldot package, used for drawing the BT). The color animation is handled by the Hippo engine which sends the proper TCL commands to the graphical interface.

Screen

The color code of the BT node in the graphical interface is the following:

  • white, the node has not yet been visited.

  • dark blue, the tick is currently in this node.

  • light blue, the tick has been passed to child(ren) node(s) below, the node is waiting for the children to return (either success, failure or running).

  • yellow, the node has returned running

  • green, the node has returned success

  • red, the node has returned failure

The top leftmost white node indicates the hippo tick, which is set at 10 Hz in this experiment, and is also the BT tick.

Note

We have defined 3 semantics for BT tick progression (this can be selected at synthesis time):

  1. The tick is only advanced by the root of the BT (each time it gets it),

  2. The tick is advanced by each BT node ticked,

  3. The tick is advanced by the root and by Action or Condition nodes.

Click on the next image for a video of an execution of the Drone1 BT, Fiacre model with Hippo.

Logo

A more complex example (drone2)

The second example builds on the previous one and adds some new features to make BT more practical and the semantics cleaner, while keeping the mapping to Fiacre formal model. It is also a consequence of the mapping to formal model which requires to clarify what should be done in ambiguous situations.

So, we added some extra features (state variables, SetSV and Eval nodes, etc).

  1. State variables are variables which can hold an int or an enumeration. See the example below with fls (flight level status) which can take an int between 0 and 3, or battery which can take three values (Good, Low and Critical), and transitions from any of them to any other.

  2. SetSV nodes can be used to set a state variable passed with the :SV keyword, by calling the :ID function (defined in Fiacre). SetSV node can only return success.

  3. Eval nodes evaluate the condition they hold and return success or failure (like Condition, they never return running).

Another area where we clarify the BT is for asynchronous actions (those usually taking some time and returning running). In the example above and below, we have parallel nodes (ParallelAll, when we start the drone and then Parallel when we track objects with the camera, while flying around). For the first one, what should we do if one of the branches fails (i.e., the ParallelAll fails) while the other one is still running? Should we wait for it, halt it? Similarly, the Parallel node will succeed as soon as one branch succeeds (this is specified with the :succeed 1). What should we do then? This is what the :halt keyword specifies. If a Parallel (or a ParallelAll) is ready to return success or failure, the running branches, if any are halted, if :halt 1 has been specified, they are left on their own otherwise. Of course, the halt is propagated downward all the way to Action. A similar mechanism is also provided for ReactiveSequence which restarts from their first branch on every tick and may have left a running branch. For example, in the BT below, a ReactiveSequence checks the battery, then the localization, at every tick, before pursuing the mission to fly around while tracking objects (this is best seen running the video available at the end of this section).

( ;;; drone2.btf
  (defsv fls ; Flight level
    :init 0  ; Initial value
    :min 0
    :max 3)

  (defsv battery
    :states (Good Low Critical)		;Self explanatory
    :init Good
    :transitions :all)

(BehaviorTree
  :name drone
  (Sequence
   (ParallelAll :wait 1 :halt 0
    (Action :ID start_drone)
    (Action :ID start_camera))
   (ReactiveSequence :halt 1
    (Sequence
     (Fallback
      (ForceFailure
       (SetSV :ID measure_battery :SV battery)) ; will set the battery State Variable
      (Eval (~ (= battery Critical))) ; If critical
      (Action :ID land)) ; ermergency landing
     (Eval (~ (= battery Critical)))
     (Fallback
      (Eval (= battery Good)) ; if Good, (but not Critical)
      (Action :ID goto_waypoint :args (x -1 y -1 z 0.5 yaw 0 duration 0)))) ; goto charging station
    (Fallback
     (Condition :ID localization_ok)
     (ForceFailure ; if localisation is not OK
      (Action :ID land))) ; we land
    (Sequence
     (Action :ID takeoff :args (height 1.0 duration 0))
     (Parallel :success 1 :wait 0 :halt 1 ; If the tracking or the nav success... we are done.
      (Action :ID camera_tracking)
      (Repeat :repeat 3
       (Sequence
	(Eval (:= fls (+ 1 fls))) ; we increment the fls state variable to fly the same pattern at 2, 4, and 6 meters high
	(Action :ID goto_waypoint :args (x -3 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x -1.5 y 3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 0 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 1.5 y 3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 3 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 3 y -3 z (* 2 $fls) yaw 0 duration 0))
	)
       )
      )
     (Action :ID goto_waypoint :args (x 0 y 0 z 5 yaw 1.4 duration 0))
     (Action :ID land)
     (Action :ID shutdown_drone))))))

Again, from this BT definition we automatically produce the following Fiacre (Hippo) model (assuming you have installed bt2fiacre, the Makefile in the examples directory will build it for you)

Drone2 Fiacre model

Drone2 Fiacre Hippo model

When being executed, you get a screen like the ones below (provided you started the proper Drone experiment).

The new color code of BT nodes now includes the following new color:

  • purple, the node was running and has been halted by one of its parent nodes

  • pink, the node has been instructed to halt itself (and its running branches). This state is so transient that it is hardly seen when the demo runs.

Localization failed

In the screenshot above, localization has failed, and it is currently making an emergency landing. You can also see that the branch executing the mission has returned running (yellow).

Localization failed and mission branch was halted

This screenshot shows that after the emergency landing has completed, the Fallback fails, so does the ReactiveSequence which then halts the mission branch (which becomes purple).

The mission completed

The last screenshot shows a completed mission (the drone has flown the pattern three times at different altitudes), but the camera did not find anything, hence it has been halted.

Click on the next image for a video of an execution of this extended Drone BT, Fiacre model with Hippo. Three runs are shown in this video (with random errors generated by the simulation):

  • failure upon startup

  • the drone finds the target and land

  • localization fails, emergency landing and mission abort

Logo

Yet, another more complex example (drone3)

The third example builds on the previous ones and adds the possibility to consult the returned status of a BT node.

In the example below, note the last line: (Eval (= camera_track.rstatus success)). This will succeed if the camera_track node has returned success and fail otherwise. In this particular example, even if the sequence has been successful so far, it is useful to decide if the tracking has found an object or not, and then report the success or failure above.

(
  (defsv fls
    :init 0
    :min 0
    :max 3)

  (defsv localization_status
    :states (Invalid Coarse Valid)
    :init Invalid
    :transitions :all)

  (defsv battery
    :states (Good Low Critical)		;Self explanatory
    :init Good
    :transitions :all)

(BehaviorTree
  :name drone
  (Sequence
   (ParallelAll :wait 1 :halt 0
    (Action :ID start_drone)
    (Action :ID start_camera))
  (ReactiveSequence :halt 1
    (Sequence
     (Fallback
      (ForceFailure :ID fail
       (SetSV :ID measure_battery :SV battery))
      (Eval (~ (= battery Critical)))
      (Action :ID land))
     (Eval (~ (= battery Critical)))
     (Fallback
      (Eval (= battery Good))
      (Action :ID goto_waypoint :args (x -1 y -1 z 0.5 yaw 0 duration 0)))) ; goto charging station
    (Fallback
     (Condition :ID localization_ok)
     (ForceFailure :ID fail
      (Action :ID land)))
    (Sequence
     (Action :ID takeoff :args (height 1.0 duration 0))
     (Parallel :success 1 :wait 0 :halt 1 ; If the tracking or the nav success... we are done.
      (Action :ID camera_tracking :name camera_track)
      (Repeat :repeat 3
       (Sequence
	(Eval (:= fls (+ 1 fls)))
	(Action :ID goto_waypoint :args (x -3 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x -1.5 y 3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 0 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 1.5 y 3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 3 y -3 z (* 2 $fls) yaw 0 duration 0))
	(Action :ID goto_waypoint :args (x 3 y -3 z (* 2 $fls) yaw 0 duration 0)))))
     (Action :ID goto_waypoint :args (x 0 y 0 z 5 yaw 1.4 duration 0))
     (Action :ID land)
     (Action :ID shutdown_drone)
     (Eval (= camera_track.rstatus success)))))))

The synthesized Fiacre model for the Hippo version can be found here: Drone3 Fiacre model and Drone3 Fiacre Hippo model

Some screenshots from running this model:

Init BT

The screenshot above shows the BT before starting execution.

Mission completed no detection

The screenshot above shows the BT fully executed but without detecting anything. Note that, as expected by the Parallel node above them, the Camera_Track has been halted.

Failed Camera

In the screenshot above, camera tracking has failed and even if the flying mission complete, the overall BT fails.

Camera track success

In the screenshot above, camera tracking has found something, the flying has been halted and the drone is flying back to base.

Camera track success

Following the previous screenshot, the mission has finished and has succeeded.

Click on the next image for a long run of different executions of this Drone BT, Fiacre model with Hippo. Six runs are shown in this video (with random errors generated by the simulation):

  • Localization failure while flying the mission (0:10)

  • Camera tracking failure, the flying continues (because one success is enough in the parallel), but the whole mission fails later, because of a localization failure again (1:12)

  • Camera track success, and the whole mission is a success (3:17)

  • Localization failure again…​ (5:40)

  • Localization failure again…​ (Sorry) (6:38)

  • Camera tracking failure, the flying mission finish, but the last Eval fails and so does the mission (7:00).

Logo

Formal verification of the BT

As we have seen above, bt2fiacre can synthesize a formal model of the BT to be executed with Hippo, but as mentioned in the introduction, it can also synthesize an equivalent model for verification. In fact, when you call bt2fiacre you choose if you want a runtime executable model (to be used with Hippo), or a verification model which can be used offline before deploying the BT. Here is below the Fiacre model for the drone3 BT: Drone3 Fiacre model for Verification

The entire process is automated using the Makefile in the examples directory but after synthesizing the fiacre model, it is compiled using the frac compiler.

frac -j -tts drone3.fcr drone3.tts

The Tina toolbox is then used to build the reachable states space of the model (it takes almost 9 minutes on an Intel® Xeon® E-2146G CPU @ 3.50GHz with 32 Giga Bytes of memory).

sift -stats drone3.tts -rsd drone3.tts/drone3.ktz
10472992 classe(s), 10472936 marking(s), 71 domain(s), 45201339 transition(s)
475.166s

Then one can check some default propeties of the model.

./drone3.tts/drone3.rch drone3.tts/drone3.ktz
never Action_start_drone_btn3_undoable FALSE
never Action_start_drone_btn3_cannot_succeed FALSE
never Action_start_drone_btn3_cannot_fail FALSE
never Action_start_drone_btn3_cannot_be_halted TRUE
never Action_start_drone_btn3_cannot_return_running FALSE
...
never Sequence_Sequence41_btn20_undoable FALSE
never Sequence_Sequence41_btn20_cannot_succeed FALSE
never Sequence_Sequence41_btn20_cannot_fail FALSE
never Sequence_Sequence41_btn20_cannot_be_halted FALSE
never Sequence_Sequence41_btn20_cannot_return_running FALSE
never Sequence_Sequence41_btn20_cannot_error TRUE
never ReactiveSequence_ReactiveSequence11_btn5_undoable FALSE
never ReactiveSequence_ReactiveSequence11_btn5_cannot_succeed FALSE
never ReactiveSequence_ReactiveSequence11_btn5_cannot_fail FALSE
never ReactiveSequence_ReactiveSequence11_btn5_cannot_be_halted FALSE
never ReactiveSequence_ReactiveSequence11_btn5_cannot_return_running FALSE
never ReactiveSequence_ReactiveSequence11_btn5_cannot_error TRUE
never Sequence_Sequence3_btn1_undoable FALSE
never Sequence_Sequence3_btn1_cannot_succeed FALSE
never Sequence_Sequence3_btn1_cannot_fail FALSE
never Sequence_Sequence3_btn1_cannot_be_halted TRUE
never Sequence_Sequence3_btn1_cannot_return_running FALSE
never Sequence_Sequence3_btn1_cannot_error TRUE
never BehaviorTree_BehaviorTree1_drone_undoable FALSE
never BehaviorTree_BehaviorTree1_drone_cannot_succeed FALSE
never BehaviorTree_BehaviorTree1_drone_cannot_fail FALSE
never BehaviorTree_BehaviorTree1_drone_cannot_be_halted TRUE
never BehaviorTree_BehaviorTree1_drone_cannot_return_running FALSE
never BehaviorTree_BehaviorTree1_drone_cannot_error TRUE

The properties which are checked are at the end of the Fiacre file above. The full output of this model checking can be found here: Drone3 verification results

For each BT node, we check some properties (usually by checking if their negation is reachable):

  1. can the BT execute and complete

  2. can the BT succeed

  3. can the BT fail

  4. can the BT return running

  5. can the BT be halted

For each of these properties, selt will output if it is TRUE or FALSE and how long it took to determine the truth value (most of the time, it is instantaneous, but it may take 30-40 seconds for the longest ones).

Note In most cases, as we check for the absence of a particular state/condition, TRUE values take longer time to be proven, as one needs to cover the whole reachable space, while FALSE value just requires to find one counter example. In this output we just present the TRUE/FALSE values, but when the property is FALSE, selt can also output the counterexample it found and the trace leading to it, so as to allow the developer to better understand how it happened.

Playing with ROS2 Nav2 BT

In this section we show how we can use our framework to model, proove and run the BT developped for the ROS2 Nav2 project…​

Frome https://docs.nav2.org/behavior_trees/overview/detailed_behavior_tree_walkthrough.html , here is the BT in regular XML format:

<root main_tree_to_execute="MainTree">
    <BehaviorTree ID="MainTree">
        <RecoveryNode number_of_retries="6" name="NavigateRecovery">
            <PipelineSequence name="NavigateWithReplanning">
                <RateController hz="1.0">
                    <RecoveryNode number_of_retries="1" name="ComputePathToPose">
                        <ComputePathToPose goal="{goal}" path="{path}" planner_id="GridBased"/>
                        <ReactiveFallback name="ComputePathToPoseRecoveryFallback">
                            <GoalUpdated/>
                            <ClearEntireCostmap name="ClearGlobalCostmap-Context" service_name="global_costmap/clear_entirely_global_costmap"/>
                        </ReactiveFallback>
                    </RecoveryNode>
                </RateController>
                <RecoveryNode number_of_retries="1" name="FollowPath">
                    <FollowPath path="{path}" controller_id="FollowPath"/>
                    <ReactiveFallback name="FollowPathRecoveryFallback">
                        <GoalUpdated/>
                        <ClearEntireCostmap name="ClearLocalCostmap-Context" service_name="local_costmap/clear_entirely_local_costmap"/>
                    </ReactiveFallback>
                </RecoveryNode>
            </PipelineSequence>
            <ReactiveFallback name="RecoveryFallback">
                <GoalUpdated/>
                <RoundRobin name="RecoveryActions">
                    <Sequence name="ClearingActions">
                        <ClearEntireCostmap name="ClearLocalCostmap-Subtree" service_name="local_costmap/clear_entirely_local_costmap"/>
                        <ClearEntireCostmap name="ClearGlobalCostmap-Subtree" service_name="global_costmap/clear_entirely_global_costmap"/>
                    </Sequence>
                    <Spin spin_dist="1.57"/>
                    <Wait wait_duration="5"/>
                    <BackUp backup_dist="0.15" backup_speed="0.025"/>
                </RoundRobin>
            </ReactiveFallback>
        </RecoveryNode>
    </BehaviorTree>
</root>

and its graphical representation

Navigate To Pose With Replanning and Recovery

Here is the same BT in our btf format

((BehaviorTree :ID MainTree
        (Recovery :num_retries 6 :name NavigateRecovery
            (PipelineSequence :name NavigateWithReplanning
                (RateController :args (hz 1)
                    (Recovery :num_retries 1 :name ComputePathToPose
                        (Action :ID ComputePathToPose :args (goal $goal path $path planner_id GridBased))
                        (ReactiveFallback :name ComputePathToPoseRecoveryFallback
                            (Condition :ID GoalUpdated)
                            (Action :ID ClearEntireCostmap :name ClearGlobalCostmap_Context1
				    :args (service_name global_costmap/clear_entirely_global_costmap)))))
                (Recovery :num_retries 1 :name FollowPath
                    (Action :ID FollowPath :args (path $path controller_id FollowPath))
                    (ReactiveFallback :name FollowPathRecoveryFallback
                        (Condition :ID GoalUpdated)
                        (Action :ID ClearEntireCostmap :name ClearLocalCostmap_Context2 :args (service_name local_costmap/clear_entirely_local_costmap)))))
            (ReactiveFallback :name RecoveryFallback
                (Condition :ID GoalUpdated)
                (RoundRobin :name RecoveryActions
                    (Sequence :name ClearingActions
                        (Action :ID ClearEntireCostmap :name ClearLocalCostmap_Subtree3 :args ( service_name local_costmap/clear_entirely_local_costmap))
                        (Action :ID ClearEntireCostmap :name ClearGlobalCostmap_Subtree4 :args (service_name global_costmap/clear_entirely_global_costmap))
                    )
                    (Action :ID Spin :args (spin_dist 1.57))
                    (Action :ID Wait :args (wait_duration 5))
                    (Action :ID BackUp :args (backup_dist 0.15 backup_speed 0.025)))))))

and its graphical representation:

Navigate To Pose With Replanning and Recovery graphical representation of the BT2F version

Here is a run of our ROS2 Nav2 BT (see above for the color coding):

Logo

Other documentation pages to check on BT2Fiacre: