From afd04cc263840eb6b5b11abac7eaf7a34c264280 Mon Sep 17 00:00:00 2001 From: Marco Lampacrescia Date: Tue, 12 Nov 2024 16:22:43 +0100 Subject: [PATCH] Add documentation for additional parameters in the system description Signed-off-by: Marco Lampacrescia --- docs/source/howto.rst | 69 +++++++++++++++++-- docs/source/tutorials.rst | 2 +- .../_test_data/ros_example_w_bt/main.xml | 1 + 3 files changed, 65 insertions(+), 7 deletions(-) diff --git a/docs/source/howto.rst b/docs/source/howto.rst index e6604023..0029cfea 100644 --- a/docs/source/howto.rst +++ b/docs/source/howto.rst @@ -341,15 +341,72 @@ 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 + + + + + + + + + + + + + + + + + + + + + + + + +.. _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 ``. Max Time -~~~~~~~~ +____________ -TODO +The maximum time the global clock is allowed to reach. + +The tag defining it is ``. 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`. + +Max Array Size +_________________ + +The maximum size assigned to a dynamic array. + +The tag defining it is ``. The `value` argument defines the max size the dynamic array can reach, and is 100 by default. + +BT Tick Rate +_________________ + +The tick rate of the Behavior Tree (in Hz). + +The tag defining it is ``. The `value` argument defines the tick rate in Hz, and is 1.0 by default. + +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 defining it is ``. The `value` argument enables / 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. diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst index 891b0d20..25036ef0 100644 --- a/docs/source/tutorials.rst +++ b/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 `_ 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 `_ 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 ` of the :ref:`How-To page `. +In the `main.xml file `_ 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 ` of the :ref:`How-To page `. In addition, in this main file, all the components of the example are put together, and the property to use is indicated. diff --git a/test/jani_generator/_test_data/ros_example_w_bt/main.xml b/test/jani_generator/_test_data/ros_example_w_bt/main.xml index 0feda93c..c51fc0ba 100644 --- a/test/jani_generator/_test_data/ros_example_w_bt/main.xml +++ b/test/jani_generator/_test_data/ros_example_w_bt/main.xml @@ -1,6 +1,7 @@ +