Add flag to enable tick of non-running BT + UC2 in tests (#68)

Signed-off-by: Marco Lampacrescia <[email protected]>
Co-authored-by: Matteo MORELLI <[email protected]>

.github/workflows/test.yml

@@ -55,9 +55,17 @@ jobs:
               if: ${{ matrix.os == 'ubuntu-22.04' }}
             # lint packages
             # TODO: add linting
+            # Prepare ROS WS for the tests
+            - name: Install ROS support pkgs
+              run: |
+                source /opt/ros/${{ matrix.ros-distro }}/setup.bash
+                mkdir ros_interfaces_ws
+                cd ros_interfaces_ws
+                ln -s ../ros_support_interfaces src
+                colcon build --cmake-args -DCMAKE_BUILD_TYPE=Release
             # run the tests
             - name: Run tests
               run: |
                 export PATH=$PATH:${{ steps.get_smc_storm.outputs.SMC_STORM_PATH }}
-                source /opt/ros/${{ matrix.ros-distro }}/setup.bash
+                source ros_interfaces_ws/install/setup.bash
                 pytest-3 -vs test/

docs/source/howto.rst

@@ -341,15 +341,80 @@ Or we can use `start_value` to define the initial value of a variable.
 BT ports can also be linked to variables in the `BT Blackboard` by wrapping the variable name in curly braces in the BT XML file. However, this feature is not yet supported.
 
 
-.. _additional_params_howto:
+.. _main_xml_howto:
 
-Additional Parameters for the Main XML file
--------------------------------------------
+The System Description (High Level XML file)
+---------------------------------------------
 
+This file references all the components defining the system, including the Behavior Tree, its plugins and the additional nodes that might be running on the side.
+Additionally, it contains additional configuration for the model, e.g. the maximum time the clock can reach or the tick rate of a Behavior Tree.
 
-.. _max_time_tag:
+An exemplary system description is the following:
+
+.. code-block:: xml
+
+    <convince_mc_tc>
+        <mc_parameters>
+            <max_time value="100" unit="s" />
+            <bt_tick_rate value="1.0" />
+            <bt_tick_if_not_running value="true" />
+        </mc_parameters>
+
+        <behavior_tree>
+            <input type="bt.cpp-xml" src="./bt.xml" />
+            <input type="bt-plugin-ros-scxml" src="./bt_topic_condition.scxml" />
+            <input type="bt-plugin-ros-scxml" src="./bt_topic_action.scxml" />
+        </behavior_tree>
+
+        <node_models>
+            <input type="ros-scxml" src="./battery_drainer.scxml" />
+            <input type="ros-scxml" src="./battery_manager.scxml" />
+        </node_models>
+
+        <properties>
+            <input type="jani" src="./battery_properties.jani" />
+        </properties>
+    </convince_mc_tc>
+
+.. _mc_parameters:
+
+Available Parameters
+~~~~~~~~~~~~~~~~~~~~~
+
+AS2FM provides a number of parameters to control the generation of the formal model. They are all contained in the tag `<mc_parameters>`.
 
 Max Time
-~~~~~~~~
+____________
 
-TODO
+The maximum time the global clock is allowed to reach.
+
+The tag is called `max_time`. The `value` argument is the max time, and the argument `unit` specifies the time unit of the provided value. Supported units are `s`, `ms`, `us`, `ns`.
+
+For example `<max_time value="100" unit="s" />` would allow the model to run for 100 seconds.
+
+Max Array Size
+_________________
+
+The maximum size assigned to a dynamic array.
+
+The tag is called `max_array_size`. The `value` argument defines the max size the dynamic array can reach, and is 100 by default.
+
+For example `<max_array_size value="100" />` would allow dynamic arrays to contain up tp 100 entries.
+
+BT Tick Rate
+_________________
+
+The tick rate of the Behavior Tree (in Hz).
+
+The tag is called `bt_tick_rate`. The `value` argument defines the tick rate in Hz, and is 1.0 by default.
+
+For example `<bt_tick_rate value="10.0">` would tick the behavior tree with a frequency of _10Hz_.
+
+BT Tick If Not Running
+_________________________
+
+Whether we shall keep ticking a Behavior Tree after it returns something different from `RUNNING` (i.e. `SUCCESS` or `FAILURE`).
+
+The tag is called `bt_tick_if_not_running`. The `value` argument enables or disables the ticking of non-running Behavior Trees, and is set to `false` by default. After the tree is stopped, the model execution will stop as well.
+
+For example `<bt_tick_if_not_running value="false" />` would stop ticking the tree after it returned either _SUCCESS_ or _FAILURE_.

docs/source/tutorials.rst

@@ -49,7 +49,7 @@ The **Behavior Tree** continuously checks the alarm topic and, once it is trigge
 The JANI property `battery_charged` given in `battery_properties.jani <https://github.com/convince-project/AS2FM/blob/main/test/jani_generator/_test_data/ros_example_w_bt/battery_properties.jani>`_ defines the property of interest to be model-checked.
 In this case, it calculates the minimal probability that the battery level will eventually be 100%, after an initial depletion time, i.e., all we verify here is that the battery is charged at some point.
 
-In the `main.xml file <https://github.com/convince-project/AS2FM/blob/main/test/jani_generator/_test_data/ros_example_w_bt/main.xml>`_ introduced earlier, the maximum run time of the system is specified with ``max_time`` and shared across the components. To make sure that the model-checked property makes sense, the allowed runtime needs to be high enough to have enough time to deplete the battery, i.e., in this example the maximal time needs to be at least 100s because the battery is depleted by 1% per second. Further information about this concept can be found in the :ref:`related section <max_time_tag>` of the :ref:`How-To page <howto>`.
+In the `main.xml file <https://github.com/convince-project/AS2FM/blob/main/test/jani_generator/_test_data/ros_example_w_bt/main.xml>`_ introduced earlier, the maximum run time of the system is specified with ``max_time`` and shared across the components. To make sure that the model-checked property makes sense, the allowed runtime needs to be high enough to have enough time to deplete the battery, i.e., in this example the maximal time needs to be at least 100s because the battery is depleted by 1% per second. Further information about this and other configuration parameters can be found in the :ref:`Available Parameters section <mc_parameters>` of the :ref:`How-To page <howto>`.
 
 In addition, in this main file, all the components of the example are put together, and the property to use is indicated.
 

ros_support_interfaces/uc2_interfaces/CMakeLists.txt

@@ -0,0 +1,49 @@
+cmake_minimum_required(VERSION 3.5)
+project(uc2_interfaces)
+
+# Default to C99
+if(NOT CMAKE_C_STANDARD)
+  set(CMAKE_C_STANDARD 99)
+endif()
+
+# Default to C++14
+if(NOT CMAKE_CXX_STANDARD)
+  set(CMAKE_CXX_STANDARD 14)
+endif()
+
+if(CMAKE_COMPILER_IS_GNUCXX OR CMAKE_CXX_COMPILER_ID MATCHES "Clang")
+  add_compile_options(-Wall -Wextra -Wpedantic)
+endif()
+
+# find dependencies
+find_package(ament_cmake REQUIRED)
+# uncomment the following section in order to fill in
+# further dependencies manually.
+find_package(std_msgs REQUIRED)
+
+find_package(rosidl_default_generators REQUIRED)
+
+rosidl_generate_interfaces(${PROJECT_NAME}
+  "msg/BlockStatus.msg"
+  "srv/GetBlockStatus.srv"
+  "action/MoveBlock.action"
+  "action/MoveBlockImplem.action"
+  "action/RecoverBlock.action"
+  "action/RecoverBlockImplem.action"
+  "action/InspectBlock.action"
+  "action/InspectBlockImplem.action"
+  DEPENDENCIES std_msgs
+ )
+
+if(BUILD_TESTING)
+  find_package(ament_lint_auto REQUIRED)
+  # the following line skips the linter which checks for copyrights
+  # uncomment the line when a copyright and license is not present in all source files
+  #set(ament_cmake_copyright_FOUND TRUE)
+  # the following line skips cpplint (only works in a git repo)
+  # uncomment the line when this package is not in a git repo
+  #set(ament_cmake_cpplint_FOUND TRUE)
+  ament_lint_auto_find_test_dependencies()
+endif()
+
+ament_package()

ros_support_interfaces/uc2_interfaces/README.md

@@ -0,0 +1,7 @@
+# Current status
+This repository stores message, service, action definitions for all the moonshot runs prepared until 31/07/2023, namely `RUN 2` and `RUN 3`.
+
+In the current version, interface definitions from all runs are mixed together. Some of them, though, have become obsolete; others need to undergo a complete re-examination and/or refactoring.
+
+# Future versions
+Next versions of the repository will re-organize the interface definitions to be compatible with the developments from `RUN 3` on.

ros_support_interfaces/uc2_interfaces/action/InspectBlock.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/action/InspectBlockImplem.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/action/MoveBlock.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/action/MoveBlockImplem.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/action/RecoverBlock.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/action/RecoverBlockImplem.action

@@ -0,0 +1,7 @@
+# action pattern
+# attributes of goal
+int32 block_id
+---
+# attributes of result
+---
+# attributes of feedback

ros_support_interfaces/uc2_interfaces/msg/BlockStatus.msg

@@ -0,0 +1 @@
+int32 block_down

ros_support_interfaces/uc2_interfaces/package.xml

@@ -0,0 +1,22 @@
+<?xml version="1.0"?>
+<?xml-model href="http://download.ros.org/schema/package_format3.xsd" schematypens="http://www.w3.org/2001/XMLSchema"?>
+<package format="3">
+  <name>uc2_interfaces</name>
+  <version>0.0.0</version>
+  <description>TODO: Package description</description>
+  <maintainer email="[email protected]">root</maintainer>
+  <license>TODO: License declaration</license>
+
+  <buildtool_depend>ament_cmake</buildtool_depend>
+  <depend>std_msgs</depend>
+  <test_depend>ament_lint_auto</test_depend>
+  <test_depend>ament_lint_common</test_depend>
+
+  <build_depend>rosidl_default_generators</build_depend>
+  <exec_depend>rosidl_default_runtime</exec_depend>
+  <member_of_group>rosidl_interface_packages</member_of_group>
+
+  <export>
+    <build_type>ament_cmake</build_type>
+  </export>
+</package>

ros_support_interfaces/uc2_interfaces/srv/GetBlockStatus.srv

@@ -0,0 +1,2 @@
+---
+int32 block_down

src/as2fm/jani_generator/scxml_helpers/top_level_interpreter.py

@@ -42,13 +42,23 @@
 
 @dataclass()
 class FullModel:
+    # The maximum time the model is allowed to run, in nanoseconds
     max_time: Optional[int] = None
+    # Max size of "dynamic" arrays defined in the SCXML models
     max_array_size: int = field(default=100)
+    # Tick rate for the loaded BT in Hz
     bt_tick_rate: float = field(default=1.0)
+    # Whether to keep ticking the BT after it returns SUCCESS / FAILURE
+    bt_tick_when_not_running: bool = field(default=False)
+    # Path to the behavior tree loaded in the model
     bt: Optional[str] = None
+    # Paths to the SCXML models of the BT nodes used in the model
     plugins: List[str] = field(default_factory=list)
+    # Paths to the SCXML models of the non-BT nodes in the model
     skills: List[str] = field(default_factory=list)
+    # Similar to the skills, currently unused
     components: List[str] = field(default_factory=list)
+    # Path to the properties definition, currently in JANI
     properties: List[str] = field(default_factory=list)
 
 
@@ -67,15 +77,7 @@ def _parse_time_element(time_element: ET.Element) -> int:
 
 def parse_main_xml(xml_path: str) -> FullModel:
     """
-    Interpret the top-level XML file as a dictionary.
-
-    The returned dictionary contains the following keys:
-    - max_time: The maximum time in nanoseconds.
-    - bt: The path to the Behavior Tree definition.
-    - plugins: A list of paths to the Behavior Tree plugins.
-    - skills: A list of paths to SCXML files encoding an FSM.
-    - components: Similar to skills, but representing abstract models of existing skills
-    - properties: A list of paths to Jani properties.
+    Interpret the top-level XML file and return it as a FullModel object.
     """
     # Used to generate absolute paths of scxml models
     folder_of_xml = os.path.dirname(xml_path)
@@ -98,6 +100,8 @@ def parse_main_xml(xml_path: str) -> FullModel:
                     model.max_array_size = int(mc_parameter.attrib["value"])
                 elif remove_namespace(mc_parameter.tag) == "bt_tick_rate":
                     model.bt_tick_rate = float(mc_parameter.attrib["value"])
+                elif remove_namespace(mc_parameter.tag) == "bt_tick_if_not_running":
+                    model.bt_tick_when_not_running = bool(mc_parameter.attrib["value"])
                 else:
                     raise ValueError(
                         error(mc_parameter, f"Invalid mc_parameter tag: {mc_parameter.tag}")
@@ -160,7 +164,11 @@ def generate_plain_scxml_models_and_timers(
         ros_scxmls.append(ScxmlRoot.from_scxml_file(fname))
     # Convert behavior tree and plugins to ROS-SCXML
     if model.bt is not None:
-        ros_scxmls.extend(bt_converter(model.bt, model.plugins, model.bt_tick_rate))
+        ros_scxmls.extend(
+            bt_converter(
+                model.bt, model.plugins, model.bt_tick_rate, model.bt_tick_when_not_running
+            )
+        )
     # Convert the loaded entries to plain SCXML
     plain_scxml_models = []
     all_timers: List[RosTimer] = []