Fix bugs converting conditional transitions to jani (#60)

* Solve bug causing conditional transition guards to be always false in some cases * Add test for correct import of properties in jani * Update installation instructions --------- Signed-off-by: Marco Lampacrescia <[email protected]>
convince-project · Oct 11, 2024 · e92c7d4 · e92c7d4
1 parent f8cc7d2
commit e92c7d4
Show file tree

Hide file tree

Showing 12 changed files with 196 additions and 37 deletions.
diff --git a/docs/source/api.rst b/docs/source/api.rst
@@ -6,6 +6,4 @@ API
    :template: custom-module-template.rst
    :recursive:
 
-   as2fm_common
-   jani_generator
-   scxml_converter
+   as2fm
diff --git a/docs/source/howto.rst b/docs/source/howto.rst
@@ -55,7 +55,7 @@ The following sections guide you through the process of :ref:`creating a SCXML m
 .. _ros_node_scxml:
 
 Creating an SCXML model of a ROS node
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 In AS2FM, we extended the SCXML language with some additional functionalities, to support the following ROS specific features:
 

diff --git a/docs/source/installation.rst b/docs/source/installation.rst
@@ -17,18 +17,37 @@ Additionally, the following dependencies are required to be installed:
 AS2FM Package Installations
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-Before installing the AS2FM packages, make sure to source the ROS workspace containing the `bt_tools` package by executing ``source <path_to_ws>/install/setup.bash``.
+.. warning::
 
-Afterwards, install the AS2FM packages with the following commands:
+    Before proceeding with the installation, make sure that pip's version is at least 24.0.
+
+    - To check pip's version: `python3 -m pip --version -m pip --version`
+    - To upgrade pip: `python3 -m pip install --upgrade pip`
+
+.. note::
+
+    Since we switched from a multi-package to a mono-package setup, make sure to uninstall the previous version of the AS2FM tools.
+    It can be done using the following instructions:
+
+    .. code-block:: bash
+
+        python3 -m pip uninstall as2fm_common
+        python3 -m pip uninstall jani_generator
+        python3 -m pip uninstall scxml_converter
+        python3 -m pip uninstall jani_visualizer
+        python3 -m pip uninstall trace_visualizer
+
+AS2FM can be installed using pip:
 
 .. code-block:: bash
 
-    python3 -m pip install as2fm_common/
-    python3 -m pip install jani_generator/
-    python3 -m pip install scxml_converter/
+    # Non-editable mode
+    python3 -m pip install AS2FM/
+    # Editable mode
+    python3 -m pip install -e AS2FM/
 
-Verify your installation by running:
+Verify your installation by **sourcing the ROS workspace containing btlib** and then running:
 
 .. code-block:: bash
 
-    scxml_to_jani --help
+    as2fm_scxml_to_jani --help
diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst
@@ -27,8 +27,8 @@ For this tutorial, we assume the system specification is already available. Furt
 Reference Model
 ```````````````
 
-For this tutorial, we use the model defined here: `ros_example_w_bt <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example_w_bt>`_.
-The model consists of a main.xml file, referencing to the BT files running in the system and the SCXML files modeling the BT plugins, as well as the environment and the ROS nodes.
+For this tutorial, we use the model defined here: `ros_example_w_bt <https://github.com/convince-project/AS2FM/tree/main/test/jani_generator/_test_data/ros_example_w_bt>`_.
+The model consists of a `main.xml` file, referencing to the BT files running in the system and the SCXML files modeling the BT plugins, as well as the environment and the ROS nodes.
 
 This example models a simple system with a battery that is continuously drained and, once it reaches a certain level, an alarm is triggered.
 A behavior tree continuously monitors the alarm topic and, once it is triggered, recharges the battery to its full level before starting the draining process again.
@@ -46,18 +46,18 @@ In this example, the system is composed by the following components modeled in S
 
 The **Behavior Tree** continuously checks the alarm topic and, once it is triggered, sends a charge trigger to the battery drainer.
 
-The JANI property `battery_charged` given in `battery_properties.jani <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example/battery_properties.jani>`_ defines the property of interest to be model-checked.
+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/tree/main/jani_generator/test/_test_data/ros_example/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 concept can be found in the :ref:`related section <max_time_tag>` 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.
 
 
 Structure of Inputs
 `````````````````````
 
-The `scxml_to_jani` tool takes a main XML file, e.g., `main.xml <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example/main.xml>`_ with the following content:
+The `as2fm_scxml_to_jani` tool takes a main XML file, e.g., `main.xml <https://github.com/convince-project/AS2FM/blob/main/test/jani_generator/_test_data/ros_example_w_bt/main.xmll>`_ with the following content:
 
 * one or multiple ROS nodes in SCXML:
 
@@ -89,7 +89,7 @@ The `scxml_to_jani` tool takes a main XML file, e.g., `main.xml <https://github.
             <max_time value="100" unit="s" />
         </mc_parameters>
 
-All of those components are converted into one JANI DTMC model by the ``scxml_to_jani`` tool.
+All of those components are converted into one JANI DTMC model by the ``as2fm_scxml_to_jani`` tool.
 
 
 Running the Script
@@ -100,7 +100,7 @@ After installing the AS2FM packages as described in the :ref:`installation secti
 .. code-block:: bash
 
     cd AS2FM/jani_generator/test/_test_data/ros_example_w_bt/
-    scxml_to_jani main.xml
+    as2fm_scxml_to_jani main.xml
 
 The output is a JANI file called `main.jani` that will be located in the same folder.
 
@@ -123,13 +123,13 @@ After it has been installed, the script can be run on a CONVINCE robotics JANI m
 
 .. code-block:: bash
 
-    convince_to_plain_jani --convince_jani path_to_convince_robotic_file.jani --output output_plain_file.jani
+    as2fm_convince_to_plain_jani --convince_jani path_to_convince_robotic_file.jani --output output_plain_file.jani
 
 
 Example
 `````````
 
-Let's convert a first simple robotic JANI model. An example can be found in `here <https://github.com/convince-project/as2fm/blob/main/jani_generator/test/_test_data/convince_jani/first-model-mc-version.jani>`_. The environment model describes a room with three straight edges and one edge with a small corner in the middle. The room describing the environment in which the robot operates looks like this:
+Let's convert a first simple robotic JANI model. An example can be found in `here <https://github.com/convince-project/AS2FM/blob/main/test/jani_generator/_test_data/convince_jani/first-model-mc-version.jani>`_. The environment model describes a room with three straight edges and one edge with a small corner in the middle. The room describing the environment in which the robot operates looks like this:
 
 .. image:: graphics/room.PNG
     :width: 200

diff --git a/src/as2fm/jani_generator/scxml_helpers/scxml_tags.py b/src/as2fm/jani_generator/scxml_helpers/scxml_tags.py
@@ -619,25 +619,27 @@ def write_model(self):
         self._events_no_condition: List[str] = []
         for child in self.children:
             transition_events = child.element.get_events()
-            transition_event = "" if len(transition_events) == 0 else transition_events[0]
+            assert len(transition_events) <= 1, "Multiple events in a transition not supported."
+            transition_event: str = "" if len(transition_events) == 0 else transition_events[0]
+            assert transition_event not in self._events_no_condition, (
+                f"Event {transition_event} in state {self.element.get_id()} has already a base"
+                "exit condition."
+            )
             transition_condition = child.element.get_condition()
             # Add previous conditions matching the same event trigger to the current child state
             child.set_previous_siblings_conditions(
                 self._event_to_conditions.get(transition_event, [])
             )
+            # Write the model BEFORE appending the new condition to the events' conditions list
+            child.write_model()
             if transition_condition is None:
-                # Make sure we do not have multiple transitions with no condition and same event
-                assert transition_event not in self._events_no_condition, (
-                    f"Event {transition_event} in state {self.element.get_id()} already has a"
-                    "transition without condition."
-                )
+                # Base condition for transitioning, when all previous aren't verified
                 self._events_no_condition.append(transition_event)
             else:
                 # Update the list of conditions related to a transition trigger
                 if transition_event not in self._event_to_conditions:
                     self._event_to_conditions[transition_event] = []
                 self._event_to_conditions[transition_event].append(transition_condition)
-            child.write_model()
 
 
 class TransitionTag(BaseTag):

diff --git a/src/as2fm/scxml_converter/scxml_entries/scxml_transition.py b/src/as2fm/scxml_converter/scxml_entries/scxml_transition.py
@@ -104,7 +104,7 @@ def get_target_state_id(self) -> str:
         """Return the ID of the target state of this transition."""
         return self._target
 
-    def get_events(self) -> Optional[List[str]]:
+    def get_events(self) -> List[str]:
         """Return the events that trigger this transition (if any)."""
         return self._events
 

diff --git a/test/jani_generator/_test_data/conditional_transitions/counter.scxml b/test/jani_generator/_test_data/conditional_transitions/counter.scxml
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<scxml
+    initial="increase"
+    version="1.0"
+    name="Counter"
+    model_src=""
+    xmlns="http://www.w3.org/2005/07/scxml">
+
+    <datamodel>
+        <data id="counter" expr="0" type="int16" />
+    </datamodel>
+
+    <state id="increase">
+        <onentry>
+            <send event="counter">
+                <param name="data" expr="counter" />
+            </send>
+        </onentry>
+        <transition target="increase">
+            <assign location="counter" expr="counter + 1" />
+        </transition>
+    </state>
+</scxml>
diff --git a/test/jani_generator/_test_data/conditional_transitions/main.xml b/test/jani_generator/_test_data/conditional_transitions/main.xml
@@ -0,0 +1,14 @@
+<convince_mc_tc>
+    <mc_parameters>
+        <max_time value="100" unit="s" />
+    </mc_parameters>
+
+    <node_models>
+        <input type="ros-scxml" src="./counter.scxml" />
+        <input type="ros-scxml" src="./receiver.scxml" />
+    </node_models>
+
+    <properties>
+        <input type="jani" src="./properties.jani" />
+    </properties>
+</convince_mc_tc>
diff --git a/test/jani_generator/_test_data/conditional_transitions/properties.jani b/test/jani_generator/_test_data/conditional_transitions/properties.jani
@@ -0,0 +1,42 @@
+{
+    "properties": [
+    {
+      "name": "destination_reached",
+      "expression": {
+        "op": "filter",
+        "fun": "values",
+        "values": {
+          "op": "Pmin",
+          "exp": {
+            "op": "U",
+            "left": {
+              "op": "⇒",
+              "left": {
+                  "op": ">",
+                  "left": 0,
+                  "right": 0
+              },
+              "right": {
+                "op": ">",
+                "left": 0,
+                "right": 0
+              }
+            },
+            "right": {
+              "op": "∧",
+              "left": {
+                "op": ">",
+                "left": "counter.data",
+                "right": 9
+              },
+              "right": "success.valid"
+            }
+          }
+        },
+        "states": {
+          "op": "initial"
+        }
+      }
+    }
+  ]
+}
diff --git a/test/jani_generator/_test_data/conditional_transitions/receiver.scxml b/test/jani_generator/_test_data/conditional_transitions/receiver.scxml
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<scxml
+    initial="check_counter"
+    version="1.0"
+    name="Receiver"
+    model_src=""
+    xmlns="http://www.w3.org/2005/07/scxml">
+
+    <state id="check_counter">
+        <transition event="counter" target="check_counter" cond="_event.data &lt; 10" />
+        <transition event="counter" target="done" cond="_event.data >= 10">
+            <send event="success" />
+        </transition>
+    </state>
+
+    <state id="done" />
+</scxml>
diff --git a/test/jani_generator/test_systemtest_scxml_to_jani.py b/test/jani_generator/test_systemtest_scxml_to_jani.py
@@ -30,10 +30,14 @@
     convert_multiple_scxmls_to_jani,
     convert_scxml_root_to_jani_automaton,
 )
-from as2fm.jani_generator.scxml_helpers.top_level_interpreter import interpret_top_level_xml
+from as2fm.jani_generator.scxml_helpers.top_level_interpreter import (
+    interpret_top_level_xml,
+    parse_main_xml,
+)
 from as2fm.scxml_converter.scxml_entries import ScxmlRoot
 
 from ..as2fm_common.test_utilities_smc_storm import run_smc_storm_with_output
+from .utils import json_jani_properties_match
 
 
 # pylint: disable=too-many-public-methods
@@ -219,23 +223,27 @@ def _test_with_main(
         """
         test_data_dir = os.path.join(os.path.dirname(__file__), "_test_data", folder)
         xml_main_path = os.path.join(test_data_dir, "main.xml")
-        ouput_path = os.path.join(test_data_dir, "main.jani")
-        if os.path.exists(ouput_path):
-            os.remove(ouput_path)
+        output_path = os.path.join(test_data_dir, "main.jani")
+        if os.path.exists(output_path):
+            os.remove(output_path)
         generated_scxml_path = "generated_plain_scxml" if store_generated_scxmls else None
         interpret_top_level_xml(xml_main_path, "main.jani", generated_scxml_path)
-        self.assertTrue(os.path.exists(ouput_path))
+        self.assertTrue(os.path.exists(output_path))
+        properties_file = os.path.join(test_data_dir, parse_main_xml(xml_main_path).properties[0])
+        assert json_jani_properties_match(
+            properties_file, output_path
+        ), "Properties from input json and generated jani file do not match."
         if not skip_smc:
             assert len(property_name) > 0, "Property name must be provided for SMC."
             pos_res = "Result: 1" if success else "Result: 0"
             neg_res = "Result: 0" if success else "Result: 1"
             run_smc_storm_with_output(
-                f"--model {ouput_path} --properties-names {property_name}",
-                [property_name, ouput_path, pos_res],
+                f"--model {output_path} --properties-names {property_name}",
+                [property_name, output_path, pos_res],
                 [neg_res],
             )
-        # if os.path.exists(ouput_path):
-        #     os.remove(ouput_path)
+        if os.path.exists(output_path):
+            os.remove(output_path)
 
     def test_battery_ros_example_depleted_success(self):
         """Test the battery_depleted property is satisfied."""
@@ -279,6 +287,10 @@ def test_multiple_senders_same_event(self):
         being sent in different orders without deadlocks."""
         self._test_with_main("multiple_senders_same_event", False, "seq_check", True)
 
+    def test_conditional_transitions(self):
+        """Test transitions upon same event with multiple conditions."""
+        self._test_with_main("conditional_transitions", False, "destination_reached", True)
+
     def test_array_model_basic(self):
         """Test the array model."""
         self._test_with_main("array_model_basic", False, "array_check", True)

diff --git a/test/jani_generator/utils.py b/test/jani_generator/utils.py
@@ -0,0 +1,32 @@
+# Copyright (c) 2024 - for information on the respective copyright owner
+# see the NOTICE file
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     http://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""
+Some test utils
+"""
+
+import json
+import os
+
+
+def json_jani_properties_match(path1: str, path2: str) -> bool:
+    """Compare the property definition from 2 json files. Return true if they match."""
+    assert os.path.exists(path1), f"Error: Path {path1} does not exist."
+    assert os.path.exists(path2), f"Error: Path {path2} does not exist."
+    with open(path1, "r", encoding="utf-8") as file:
+        property1 = json.load(file)["properties"]
+    with open(path2, "r", encoding="utf-8") as file:
+        property2 = json.load(file)["properties"]
+    return property1 == property2