Tutorials

We provide an example for using MoVe4BT.

Run MoVe4BT

./Groot

Using the above command to run MoVe4BT, then click the Editor button. After this, you will see the following interface.

The PickUp Example

This example describes a robot that needs to pick up a cube at location A.

Now, we will illustrate the usage of MoVe4BT with this simple PickUp example. We have divided it into five steps：

--1. Nodes registration and Constructing BehaviorTree
--2. Variables  declaration 
--3. Nodes semantics embedding 
--4. Input properties 
--5. Start verifying

(1) Nodes registration and Constructing Behavior Trees

The control node has been declared on the left interface earlier. Please note that currently only Sequence, Fallback, and Parallel are available. You can register Action nodes and Condition nodes as needed according to your own requirements.

In this example, we need to register four nodes:

--  Condition nodes
-----  Picked      Used to check whether the cube has been picked up
-----  AtA         Used to check  whether the robot is already at location A.

--  Action nodes
-----  GotoA       Robot moves to location A.
-----  PickUp      Robot picks up the cube.

First, click on the button indicated by the arrow to add a custom node, enter the node name and select the node type.


After registering all the necessary action and condition nodes, you can construct a BehaviorTree by combining the already registered control nodes. Just drag and drop them onto the right interface and connect them!



(2) Variables declaration

MoVe4BT only supports integer, Boolean and integer arrays, declared as follows: var x = Int32 for integers, var x = true/false for booleans and var x = [integer1,integer2,…,integern] for integer arrays. In our tool, the integer variable is a 32-bit signed integer, which means it can store values ranging from -2147483648 to 2147483647.

We can use variables to model environmental factors, and use constants to define nodes execution time.

--  Variables
-----  r_p     robot position,  r_p==0 means robot isn't at A, r_p==1 means robot is at A. Default: r_p=0
-----  c_p     cube position,   r_p==0 means cube is at A, c_p==1 means cube is in the robot arm. Default: c_p=0
Your GIF

Please note that var is a keyword. Variables need to be assigned using the = sign. Also, a semicolon ; needs to be added after each declaration.

The complete input in this example is:

var r_p=0; var c_p=0;

(3) Nodes semantics embedding

We designed guard port for condition nodes, while action nodes have guard, program, time, and success threshold port.

The guard specifies the condition the variables should satisfy to produce the event. In the absence of a guard or when multiple guards simultaneously fulfill the conditions, the model randomly selects from the feasible events. Additionally, a guard evaluating to false indicates that the corresponding event can never occur, whereas a guard evaluating to true signifies that the associated event may occur.

the program gives the data operations when the event happens.

The time specifies the action execution period.

Tnd the success threshold specifies the action will return success at least once after N times executions.

--  Guard port
-----  success_guard   if success_guard is satisfied, then executing this node will return success.
-----  failure_guard   if failure_guard is satisfied, then executing this node will return failure.
-----  running_guard   if running_guard is satisfied, then executing this node will return running.   (only Action nodes has this guard port)

--  Program port
-----  success_program   the effect after the execution of the action node returns success
-----  failure_program   the effect after the execution of the action node returns failure
-----  runnning_program  the effect after the execution of the action node returns running

--  Time port
-----  Execuiton time    the execution time of the action node.

--  Success threshold port
-----  Success threshold  the action execution N times can return success at least once.

The guard is a quantifier-free first-order logic formula on the data variables like:

c_p==0 && r_p==0

The program is a program that manipulates the data variables and can be specified in any programming language. In our implementation, the program is required to be given in C# language like:

c_p=1;r_p=1

The time and success threshold is required to be given in positive integers.


To add ports to the node, simply right-click on it as shown in the left figure below. The complete diagram is shown in the right figure below.

Your GIF
Your GIF

For example, the failure_guard of Picked is c_p==0, and the success_guard is c_p==1. This means that Picked will only return success if c_p==1 is satisfied, and if c_p==0 is met, the execution of Picked will return failure, c_p==1 means that the cube has already been picked up; the success_program of PickUP means that after the execution of PickUP node returns success, it will set c_p as 1.

(4) Input properties

(a) LTL properties

Some LTL’s temporal logic operators and their semantics as shown below (Image from PAT User Manual):

In this example, if we want to verify that if the robot finds itself not at A, then it will try move to A, the input LTL formula is:

#assert BehaviorTree |= G (AtA_f -> X (GoToA_s || GoToA_f || GoToA_r));

Here #assert BehaviorTree |= are keywords.

(b) Timed behavior properties

Our tool supports reachability property verification to verify timed behavior-related properties. Reachability verification verifies the reachability properties (i.e., a fragment of LTL) of the model. A reachability property specifies that a state is reachable from the initial state.

We now limit the robot to run for only 12 units time in the following way:

GIF 1

We can check whether the robot is able to eventually pick up the cube like

#define goal c_p==1;                        //c_p==1 means the cube is in the robot's hand.
#assert DeadlineProcess reaches goal;

So, we first define a target state. Here #define is a keyword, goal is the name of the target state, you can name whatever you want. The #assert DeadlineProcess reaches are keywords too.


Totally, the input properties of this example are:

#assert BehaviorTree |= G( AtA_f -> X( GoToA_s || GoToA_f || GoToA_r ));
#define goal c_p==1;     
#assert DeadlineProcess reaches goal;

(5) Start verifying

You can now click the Verification button and wait for the verification results to pop up!

Your GIF

Contacts

Please feel free to contact us if you have any questions about MoVe4BT.