From e92c7d4ea8c5e6100ef764ff000f4cf5654b8438 Mon Sep 17 00:00:00 2001 From: Marco Lampacrescia <65171491+MarcoLm993@users.noreply.github.com> Date: Fri, 11 Oct 2024 14:00:58 +0200 Subject: [PATCH] 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 --- docs/source/api.rst | 4 +- docs/source/howto.rst | 2 +- docs/source/installation.rst | 33 +++++++++++---- docs/source/tutorials.rst | 18 ++++---- .../scxml_helpers/scxml_tags.py | 16 +++---- .../scxml_entries/scxml_transition.py | 2 +- .../conditional_transitions/counter.scxml | 23 ++++++++++ .../conditional_transitions/main.xml | 14 +++++++ .../conditional_transitions/properties.jani | 42 +++++++++++++++++++ .../conditional_transitions/receiver.scxml | 17 ++++++++ .../test_systemtest_scxml_to_jani.py | 30 +++++++++---- test/jani_generator/utils.py | 32 ++++++++++++++ 12 files changed, 196 insertions(+), 37 deletions(-) create mode 100644 test/jani_generator/_test_data/conditional_transitions/counter.scxml create mode 100644 test/jani_generator/_test_data/conditional_transitions/main.xml create mode 100644 test/jani_generator/_test_data/conditional_transitions/properties.jani create mode 100644 test/jani_generator/_test_data/conditional_transitions/receiver.scxml create mode 100644 test/jani_generator/utils.py diff --git a/docs/source/api.rst b/docs/source/api.rst index 82160589..52689baf 100644 --- 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 index c26e80b5..431bd4f0 100644 --- 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 index 9c0c739b..82617edb 100644 --- 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 /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 index f5c51954..377197b5 100644 --- 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 `_. -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 `_. +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,10 +46,10 @@ 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 `_ defines the property of interest to be model-checked. +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 concept can be found in the :ref:`related 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. @@ -57,7 +57,7 @@ In addition, in this main file, all the components of the example are put togeth Structure of Inputs ````````````````````` -The `scxml_to_jani` tool takes a main XML file, e.g., `main.xml `_ with the following content: +The `as2fm_scxml_to_jani` tool takes a main XML file, e.g., `main.xml `_ 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 -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 `_. 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 `_. 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 index c4cf19b4..9d1ec412 100644 --- 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 index 198612bd..7bb65c89 100644 --- 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 new file mode 100644 index 00000000..9805e1ef --- /dev/null +++ b/test/jani_generator/_test_data/conditional_transitions/counter.scxml @@ -0,0 +1,23 @@ + + + + + + + + + + + + + + + + + + diff --git a/test/jani_generator/_test_data/conditional_transitions/main.xml b/test/jani_generator/_test_data/conditional_transitions/main.xml new file mode 100644 index 00000000..0337de7b --- /dev/null +++ b/test/jani_generator/_test_data/conditional_transitions/main.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + + diff --git a/test/jani_generator/_test_data/conditional_transitions/properties.jani b/test/jani_generator/_test_data/conditional_transitions/properties.jani new file mode 100644 index 00000000..70741999 --- /dev/null +++ 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 new file mode 100644 index 00000000..a9cb4bc3 --- /dev/null +++ b/test/jani_generator/_test_data/conditional_transitions/receiver.scxml @@ -0,0 +1,17 @@ + + + + + + + + + + + + diff --git a/test/jani_generator/test_systemtest_scxml_to_jani.py b/test/jani_generator/test_systemtest_scxml_to_jani.py index ee63ae59..d7b7f581 100644 --- 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 new file mode 100644 index 00000000..2e8cbd84 --- /dev/null +++ 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