Add documentation for additional parameters in the system description

Signed-off-by: Marco Lampacrescia <[email protected]>

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
+
+    <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 defining it is `<max_time value="100" unit="s" />`. 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 `<max_array_size value="100" />`. 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 `<bt_tick_rate value="1.0">`. 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 `<bt_tick_if_not_running value="false" />`. 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.

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.
 

test/jani_generator/_test_data/ros_example_w_bt/main.xml

@@ -1,6 +1,7 @@
 <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>