merge

Signed-off-by: Michaela Klauck <[email protected]>

.github/workflows/test.yml

@@ -0,0 +1,68 @@
+name: Test
+# Test the python packages that are part of the toolchain
+
+on:
+    push:
+        branches: [ "main" ]
+    pull_request:
+        branches: [ "main" ]
+
+jobs:
+    test:
+        runs-on: ubuntu-latest
+        strategy:
+            matrix:
+                ros-distro: [ "humble" ]
+        steps:
+            # Checkout the repository
+            - name: Checkout repository
+              uses: actions/checkout@v2
+            # Set up ROS
+            - name: Set up ROS
+              uses: ros-tooling/[email protected]
+              with:
+                required-ros-distributions: ${{ matrix.ros-distro }}
+            # Get bt_tools TODO: remove after the release of bt_tools
+            - name: Checkout bt_tools
+              uses: actions/checkout@v2
+              with:
+                repository: boschresearch/bt_tools
+                ref: feature/fsm_conversion
+                path: colcon_ws/src/bt_tools
+            # Compile bt_tools TODO: remove after the release of bt_tools
+            - name: Compile bt_tools
+              run: |
+                source /opt/ros/${{ matrix.ros-distro }}/setup.bash
+                # Install dependencies
+                cd colcon_ws
+                rosdep update && rosdep install --from-paths src --ignore-src -y
+                # Build and install bt_tools
+                colcon build --symlink-install
+            # Get smc_storm for testing
+            - name: Get smc_storm
+              id: get_smc_storm
+              run: |
+                wget https://github.com/convince-project/smc_storm/releases/download/0.0.1/smc_storm_executable.tar.gz
+                tar -xzf smc_storm_executable.tar.gz
+                ./install.sh --install-dependencies
+                # Save the path to the smc_storm executable
+                echo SMC_STORM_PATH=$PWD/bin/ >> $GITHUB_OUTPUT
+            # Update pip
+            - name: Update pip
+              run: python -m pip install --upgrade pip
+            # install the packages
+            - name: Install packages
+              run: | 
+                source colcon_ws/install/setup.bash  # TODO: remove after the release of bt_tools
+                pip install jani_generator/.[dev]
+                pip install mc_toolchain_jani_common/.[dev]
+                pip install scxml_converter/.[dev]
+            # lint packages
+            # TODO: add linting    
+            # 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 colcon_ws/install/setup.bash  # TODO: remove after the release of bt_tools
+                pytest-3 -vs mc_toolchain_jani_common jani_generator scxml_converter

README.md

@@ -15,4 +15,4 @@ Feedback is highly appreciated. Please open issues on new ideas, bugs, etc. here
 
 ### License
 
-as2fm comes under the Apache-2.0 license, see [LICENSE](./LICENSE).
+as2fm comes under the Apache-2.0 license, see [LICENSE](./LICENSE).

docs/source/index.rst

@@ -25,4 +25,5 @@ Contents
    :maxdepth: 2
 
    tutorials
+   scxml-jani-conversion
    api

docs/source/scxml-jani-conversion.rst

@@ -0,0 +1,81 @@
+SCXML to Jani Conversion
+========================
+
+SCXML and Jani
+----------------
+
+In CONVINCE, we expect developers to use Behavior Trees and SCXML to model the different parts of a robotic systems.
+
+SCXML (Scope XML) is an high level format that describes a single state machine, and allows it to exchange information with other state machines using events. Each SCXML file defines its variables (datamodel), states and transitions.
+
+With SCXML, the system consists of a set of state machines, each one represented by a SCXML file, that are synchronized together using events. Operations are carried out when a state machine receives an event, enters a state, or exits a state.
+
+With Jani, the whole system is contained in a single JSON file, consisting of a set of global variables, automata (equivalent to state machines) with their edges (equivalent to transitions), and a composition description, describing how Automata should be synchronized by the mean of advancing specific edges at the same time.
+
+The main difference between SCXML and Jani is that in Jani there is no concept of events, so synchronization must be achieved using the global variables and composition description.
+
+High-Level (ROS) SCXML Implementation
+---------------------------------------
+
+In CONVINCE, we extended the standard SCXML format defined `here <https://www.w3.org/TR/scxml/>`_ with ROS specific features, to make it easier for ROS developers to model ROS-based systems.
+
+In this guide we will refer to the extended SCXML format as High-Level SCXML and the standard SCXML format as Low-Level SCXML.
+
+Currently, the supported ROS-features are:
+- ROS Topics
+- ROS Timers (Rate-callbacks)
+
+TODO: Example of Topic and Timer declaration + usage.
+
+Low-Level SCXML Conversion
+----------------------------
+
+Low-Level SCXML is the standard SCXML format defined `here <https://www.w3.org/TR/scxml/>`_.
+
+Our converter is able to convert High-Level SCXML to Low-Level SCXML by translating the ROS specific features to standard SCXML features.
+In case of timers, we need additional information that cannot be encoded in SCXML, so that information is generated at runtime.
+
+The conversion between the two SCXML formats is implemented in ScxmlRoot.as_plain_scxml(). TODO: Link to API.
+
+TODO: Describe how we translate the High-Level SCXML to the Low-Level SCXML.
+
+Jani Conversion
+----------------
+
+Once the Low-Level SCXML is obtained, we can use it together with the timers information in the conversion to a Jani model.
+
+Simple Overview
+________________
+
+The following picture gives a simple overview of how our conversion works:
+
+.. image:: graphics/scxml_to_jani.drawio.svg
+    :alt: Conversion process
+    :align: center
+
+The core of the conversion lies in the translation of the SCXML state machines to Jani automata and the handling of the synchronization between them.
+In the example above, we have two SCXML state machines, BatteryDrainer and BatteryManager, that are synchronized using the event "level".
+
+At start, the BatteryDrainer state machine sends a "level" event out, containing the current battery level in the "data" field.
+In Jani, this translates to an edge, i.e. "level_on_send", that advances the BatteryDrainer automaton to a next state where the sending action is carried out and, at the same time, assigns a global variable corresponding to the event parameter, i.e. "level.data", and another edge with the same name that advances an additional automaton "level_sync" from the "wait" to the "received" state, signaling that an event "level" was sent out and needs to be processed.
+
+The BatteryManager automaton has an edge "level_on_receive", that can now be triggered since the "level_sync" automaton is in the "received" state. When executing the edge, the BatteryManager automaton assigns the global variable "battery_alarm" based on the data contained in the "level.data" variable and goes back to the same state, waiting for the next "level" event. Similarly, the "level_sync" automaton transitions back to the "wait" state using the edge "level_on_receive".
+
+The BatteryDrainer can execute the edge "battery_drainer_act_0" and transition back to the initial state either before or after the "level_on_receive" action, as there is no constraint enforcing a specific order of execution.
+
+Similarly, since the automaton "level_sync" has an outgoing edge "level_on_send" that stays in the "received" state, the BatteryManager can send a "level" event before the BatteryDrainer has processed the previous one.
+This has been introduced to make the synchronization more similar to how it works in ROS, where messages can be overridden before being processed.
+
+Handling onentry, onexit and conditions
+________________________________________
+
+TODO
+
+.. image:: graphics/scxml_to_jani_entry_exit_if.drawio.svg
+    :alt: How execution blocks and conditions are translated
+    :align: center
+
+Handling of (ROS) Timers
+__________________________
+
+TODO

graphics

@@ -0,0 +1 @@
+docs/source/graphics/

jani_generator/src/jani_generator/jani_entries/jani_automaton.py

@@ -76,6 +76,10 @@ def add_edge(self, edge: JaniEdge):
     def get_edges(self) -> List[JaniEdge]:
         return self._edges
 
+    def remove_edges_with_action_name(self, action_name: str):
+        assert isinstance(action_name, str), "Action name must be a string"
+        self._edges = [edge for edge in self._edges if edge.get_action() != action_name]
+
     def _generate_locations(self, location_list: List[str], initial_locations: List[str]):
         for location in location_list:
             self._locations.add(location["name"])

jani_generator/src/jani_generator/jani_entries/jani_composition.py

@@ -33,7 +33,8 @@ def __init__(self, composition_dict: Optional[Dict[str, Any]] = None):
 
     def add_element(self, element: str):
         """Append a new automaton name in the composition."""
-        assert element not in self._elements, f"Element {element} already exists in the composition"
+        assert element not in self._elements, \
+            f"Element {element} already exists in the composition"
         self._elements.append(element)
         self._element_to_id[element] = len(self._elements) - 1
 
@@ -49,7 +50,8 @@ def add_sync(self, sync_name: str, syncs: Dict[str, str]):
         }
         # Generate the synchronize list
         for automata, action in syncs.items():
-            assert automata in self._element_to_id, f"Automaton {automata} does not exist in the composition"
+            assert automata in self._element_to_id, \
+                f"Automaton {automata} does not exist in the composition"
             new_sync["synchronise"][self._element_to_id[automata]] = action
         self._syncs.append(new_sync)
 
@@ -92,6 +94,8 @@ def _generate_syncs(self, syncs_list):
         return generated_syncs
 
     def as_dict(self):
+        # Sort the syncs before return
+        self._syncs = sorted(self._syncs, key=lambda x: x["result"])
         return {
             "elements": [{"automaton": element} for element in self._elements],
             "syncs": self._syncs

jani_generator/src/jani_generator/jani_entries/jani_constant.py

@@ -36,7 +36,7 @@ def name(self) -> str:
     def value(self) -> JaniValue:
         assert self._value is not None, "Value not set"
         jani_value = self._value.value
-        assert jani_value is not None and jani_value.is_valid(), "The expression cannot be evaluated to a constant value"
+        assert jani_value is not None and jani_value.is_valid(), "The expression can't be evaluated to a constant value"
         return jani_value.value()
 
     def jani_type_from_string(str_type: str) -> ValidTypes:
@@ -52,6 +52,7 @@ def jani_type_from_string(str_type: str) -> ValidTypes:
         else:
             raise ValueError(f"Type {str_type} not supported by Jani")
 
+    # TODO: Move this to a util function file
     def jani_type_to_string(c_type: ValidTypes) -> str:
         """
         Translate a Python type to the name of the type in Jani.
@@ -68,14 +69,14 @@ def jani_type_to_string(c_type: ValidTypes) -> str:
         src https://docs.google.com/document/d/\
             1BDQIzPBtscxJFFlDUEPIo8ivKHgXT8_X6hz5quq7jK0/edit
         """
+        assert isinstance(c_type, type), f"Type {c_type} is not a type"
         if c_type == bool:
             return "bool"
-        elif c_type == int:
+        if c_type == int:
             return "int"
-        elif c_type == float:
+        if c_type == float:
             return "real"
-        else:
-            raise ValueError(f"Type {c_type} not supported by Jani")
+        raise ValueError(f"Type {c_type} not supported by Jani")
 
     def as_dict(self):
         return {

jani_generator/src/jani_generator/jani_entries/jani_expression.py

@@ -17,18 +17,18 @@
 Expressions in Jani
 """
 
-from typing import Union
+from typing import Dict, Union
 from jani_generator.jani_entries import JaniValue
 
 SupportedExp = Union[str, int, float, bool, dict]
 
 
 class JaniExpression:
-    def __init__(self, expression):
+    def __init__(self, expression: Union[SupportedExp, 'JaniExpression', JaniValue]):
         self.identifier: str = None
         self.value: JaniValue = None
         self.op = None
-        self.operands = None
+        self.operands: Dict[str, Union[JaniExpression, JaniValue]] = None
         if isinstance(expression, JaniExpression):
             self.identifier = expression.identifier
             self.value = expression.value
@@ -46,7 +46,8 @@ def __init__(self, expression):
                 # If it is a value, then we don't need to expand further
                 self.value = JaniValue(expression)
             else:
-                # If it isn't a value or an identifier, it must be a dictionary providing op and related operands
+                # If it isn't a value or an identifier, it must be a dictionary providing op and
+                # related operands
                 # Operands need to be expanded further, until we encounter a value expression
                 assert isinstance(expression, dict), "Expected a dictionary"
                 assert "op" in expression, "Expected either a value or an operator"
@@ -55,9 +56,11 @@ def __init__(self, expression):
 
     def _get_operands(self, expression_dict: dict):
         if (self.op in ("intersect", "distance")):
-            # intersect: returns a value in [0.0, 1.0], indicating where on the robot trajectory the intersection occurs.
-            #            0.0 means no intersection occurs (destination reached), 1.0 means the intersection occurs at the start
-            # distance: returns the distance between the robot and the barrier
+            # intersect: returns a value in [0.0, 1.0], indicating where on the robot trajectory
+            # the intersection occurs.
+            #            0.0 means no intersection occurs (destination reached), 1.0 means the
+            # intersection occurs at the start distance: returns the distance between the robot and
+            # the barrier.
             return {
                 "robot": JaniExpression(expression_dict["robot"]),
                 "barrier": JaniExpression(expression_dict["barrier"])}
@@ -75,7 +78,8 @@ def _get_operands(self, expression_dict: dict):
             return {
                 "left": JaniExpression(expression_dict["left"]),
                 "right": JaniExpression(expression_dict["right"])}
-        if (self.op in ("!", "¬", "sin", "cos", "floor", "ceil", "abs", "to_cm", "to_m", "to_deg", "to_rad")):
+        if (self.op in ("!", "¬", "sin", "cos", "floor", "ceil",
+                        "abs", "to_cm", "to_m", "to_deg", "to_rad")):
             return {
                 "exp": JaniExpression(expression_dict["exp"])}
         if (self.op in ("ite")):
@@ -96,13 +100,27 @@ def _get_operands(self, expression_dict: dict):
         assert False, f"Unknown operator \"{self.op}\" found."
 
     def replace_event(self, replacement):
+        """Replace `_event` with `replacement`.
+
+        Within a transitions, scxml can access data of events from the `_event` variable. We
+        have to replace this by the global variable where we stored the data from the received
+        event.
+
+        :param replacement: The string to replace `_event` with.
+        :return self: for the convenience of chain-ability
+        """
+        if replacement is None:
+            # No replacement needed!
+            return self
         if self.identifier is not None:
             self.identifier = self.identifier.replace("_event", replacement)
-            return
+            return self
         if self.value is not None:
-            return
+            return self
         for operand in self.operands.values():
-            operand.replace_event(replacement)
+            if isinstance(operand, JaniExpression):
+                operand.replace_event(replacement)
+        return self
 
     def is_valid(self) -> bool:
         return self.identifier is not None or self.value is not None or self.op is not None
@@ -117,7 +135,8 @@ def as_dict(self) -> Union[str, int, float, bool, dict]:
             "op": self.op,
         }
         for op_key, op_value in self.operands.items():
-            assert isinstance(op_value, JaniExpression), f"Expected an expression, found {type(op_value)} for {op_key}"
+            assert isinstance(op_value, JaniExpression), \
+                f"Expected an expression, found {type(op_value)} for {op_key}"
             assert hasattr(op_value, "identifier"), f"Identifier not set for {op_key}"
             op_dict.update({op_key: op_value.as_dict()})
         return op_dict

jani_generator/src/jani_generator/jani_entries/jani_expression_generator.py

@@ -96,6 +96,10 @@ def not_equal_operator(left, right) -> JaniExpression:
 
 
 # Logic operators
+def not_operator(exp) -> JaniExpression:
+    return JaniExpression({"op": "¬", "exp": exp})
+
+
 def and_operator(left, right) -> JaniExpression:
     return JaniExpression({"op": "∧", "left": left, "right": right})
 

jani_generator/src/jani_generator/jani_entries/jani_guard.py

@@ -22,6 +22,7 @@
 
 from jani_generator.jani_entries.jani_expression import JaniExpression
 
+
 class JaniGuard:
     def __init__(self, expression: Optional[JaniExpression]):
         self.expression = expression
@@ -30,9 +31,8 @@ def as_dict(self, constants: Optional[dict] = None):
         d = {}
         if self.expression:
             exp = self.expression.as_dict()
-            if (isinstance(exp, dict) and 
-                list(exp.keys()) == ['exp']):
+            if (isinstance(exp, dict) and list(exp.keys()) == ['exp']):
                 d['exp'] = exp['exp']
             else:
                 d['exp'] = exp
-        return d
+        return d