Tutorials

This section provides two tutorials on how to use the MOCO tools to convert an autonomous robotic system into a model compatible with existing model checker tools (MOON and SCAn). The RoaML models generated in the tutorials can be given to any model checker accepting SCXML as input format, but we recommend SCAn.

Prerequisites

You don’t need to install MOCO locally on your machine. You can use the docker container, provided as a package on the MOCO Github page

Either pull the container with the following command:

$ docker pull ghcr.io/nevertools/moco:latest
...

or clone the repository and pull the image with docker compose: .. code-block:: bash

$ docker compose pull …

Then, run the container with: .. code-block:: bash

$ docker compose run –remove-orphans base

Should you wish to install MOCO locally, follow the description in the installation guide.

What you will learn

In this tutorial you will learn in about one hour how a robotic example can be expressed in RoaML with ROS and BT tools. Then, you will use MOCO to translate the model into plain SCXML. The example models a robot with a simple symbolic fetch and carry task. You will use linear temporal logic (LTL) properties to verify it is working correctly. Then, you will translate the model of the robot and its environment with AS2FM into JANI to run it with SMC Storm, our statistical model checking (SMC) tool. With the results from SMC Storm, you will observe that some properties are fulfilled and some are violated. By updating the model with more complexity in terms of probabilistic behavior and additional features in the behavior tree (BT), you make sure that the required properties hold in the end. This verifies, that your BT controls the example correctly.

The output is a folder (./output, unless otherwise specified) containing the plain SCXML files for the model.

Tutorial 2: Fetch & Carry Robot

For this tutorial we use the model defined here: tutorial_fetch_and_carry. A classical fetch and carry task is implemented there. A robot should drive to the pantry where food is stored, pick up snacks, drive to the table and place the snacks there. The robot should be done with this task after at most 100 seconds.

The model consists of a main.xml file, referencing the BT bt_tree.xml running in the system and the SCXML files modeling the BT plugins for navigating bt_navigate_action.scxml, picking bt_pick_action.scxml, and placing bt_place_action.scxml, as well as the world model world.scxml.

All of those components are summarized and collected in the main.xml file.

For the rest of the tutorial it is assumed the container is running and you have navigated to the model’s folder - mounted from the cloned repository:

$ cd examples/tutorial_fetch_and_carry

  • First, some parameters configuring generic properties of the system are defined. In this example we bound the maximum execution time to 100 seconds, and configure unbounded arrays to contain at most 10 elements.

    <parameters>
    <max_time value="100" unit="s" />
    <max_array_size value="10" />
</parameters>

  • Afterwards the Behavior Tree is fully specified in terms of the BT in the BT.cpp XML format and the used BT plugins in ASCXML for navigating, picking, and placing. We will go into the details of the individual files later.

    <behavior_tree>
    <input type="bt.cpp-xml" src="./bt_tree.xml" />
    <input type="bt-plugin-ascxml" src="./bt_navigate_action.scxml" />
    <input type="bt-plugin-ascxml" src="./bt_pick_action.scxml" />
    <input type="bt-plugin-ascxml" src="./bt_place_action.scxml" />
</behavior_tree>

  • In addition, the model of the environment, also known as world, is given in SCXML. We will go into the details of the environment model later.

    <node_models>
    <input type="node-ascxml" src="./world.scxml" />
</node_models>

The behavior tree specified in bt_tree.xml looks as depicted in the image below. The SequenceWithMemory node ticks each child in order until all of them have returned Success. Those who already returned Success are not ticked in the next cycle again. The location is encoded as 0 = in the pantry and 1 = at the table. The snack object has id 0.

An image of the behavior tree of the fetch and carry example.

The next image depicts the behavior of the BT plugin bt_navigate_action.scxml. It is used to navigate to a certain location given by the id, either 0 or 1 in this example, stored in data. When the BT is ticked it assigns loc_id = data. When the BT is halted or the action is aborted tmp_result is set to false, otherwise it is set to true. Based on that the return status of the tree is then published.

An image of the BT navigate action plugin.

The next image depicts the behavior of the BT plugin bt_pick_action.scxml in a very similar fashion. The action is used to pick a certain item with a given id, stored in data. When the BT is ticked it assigns object_id = data. When the BT is halted or the action is aborted tmp_result is set to false, otherwise it is set to true. Based on that the return status of the tree is then published.

An image of the BT pick action plugin.

The next image depicts the behavior of the BT plugin bt_place_action.scxml. When called, the action just immediately tries to successfully execute, no matter if there is an object in the gripper or not, when the BT is ticked. When the BT is halted or the action is aborted tmp_result is set to false, otherwise it is set to true. Based on that the return status of the tree is then published.

An image of the BT place action plugin.

As a last step, we take a closer look at the environment model in world.scxml.

  • First, it is indicated that the model makes use of the interfaces from the fetch_and_carry_msgs package, where custom ROS actions are defined. In line 21 the ROS topic publisher for the snack type is declared.

    <ros_action_server name="act_nav" action_name="/go_to_goal" type="fetch_and_carry_msgs/Navigate" />
<ros_action_server name="act_pick" action_name="/pick_object" type="fetch_and_carry_msgs/Pick" />
<ros_action_server name="act_place" action_name="/place_object" type="fetch_and_carry_msgs/Place" />
<ros_topic_publisher name="pub_snacks0" topic="/snacks0_loc" type="std_msgs/Int32" />

  • The next block defines and initializes the variables used: An array of integers for the objects’ locations, an integer for the robot’s location, a flag indicating if the robot is holding something (-1 = no, otherwise the object’s id), a variable saying where the object should be brought to, i.e., the goal_id, and two helper variables req_obj_idx and req_loc_idx for the id of the object which is requested to be picked up and the location to which the robot is requested to navigate to.

    <datamodel>
    <data id="obj_locs" type="int32[1]" expr="[0]" />
    <data id="robot_loc" type="int32" expr="1" />
    <data id="robot_holding" type="int32" expr="-1" />
    <!-- Additional support variable for the goal_id -->
    <data id="goal_id" type="int32" expr="0" />
    <data id="req_obj_idx" type="int32" expr="0" />
    <data id="req_loc_idx" type="int32" expr="0" />
</datamodel>

  • The actual functionality of the world model is depicted in the graph below. When trying to navigate to a goal the location is first stored in the helper variable and from there the robot location is set to the goal location id. For the moment, in this file it is assumed that this operation always succeeds. When trying to pick an object, the requested object’s id is again stored in a helper variable. Afterwards, it is checked if the object’s location is the same as the robot’s location. It is recorded in the robot_holding variable that the robot now holds the object with a certain id. The location of the object is reset to -1 indicating that it is in the robot’s gripper. This procedure can succeed or be aborted. In case an object should be placed, it is checked if the robot is holding an object (by robot_holding != -1). In this case the location of the object is replaced with the robot’s location and robot_holding is set to -1 again because the gripper is empty now. This procedure can also be aborted if it does not succeed.

    An image of the world behavior of the fetch and carry example.

Model Translation with MOCO

You can translate this RoaML model in SCXML just as easily as the first one. Assuming you are in the examples/tutorial_fetch_and_carry folder:

$ moco_roaml_to_scxml main.xml

MOCO - RoAML to SCXML.

Loading model from main.xml.
...

This produces an equivalent model in the plain SCXML format and saves it to the ./output folder. You may specify a different output folder with the –generated-scxml-dir argument.

Should you wish to learn more about RoaML, its’ tags and their handling, check the RoaML to SCXML conversion.