Merge pull request #10 from convince-project/address-todos-from-clean…

…up-cp

Address todos from cleanup

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

jani_generator/src/jani_generator/scxml_helpers/scxml_tags.py

@@ -19,7 +19,7 @@
 
 import xml.etree.ElementTree as ET
 from hashlib import sha256
-from typing import List, Optional, Tuple, Union
+from typing import Dict, List, Optional, Tuple, Union
 
 from jani_generator.jani_entries import (JaniAssignment, JaniAutomaton,
                                          JaniEdge, JaniExpression, JaniGuard,
@@ -194,18 +194,19 @@ def _append_scxml_body_to_jani_automaton(jani_automaton: JaniAutomaton, events_h
                 new_edges.extend(sub_edges)
                 new_locations.extend(sub_locs)
                 previous_conditions.append(current_cond)
-            # Add else branch:
-            if ec.get_else_execution() is not None:
-                print(f"Else: {ec.get_else_execution()}")
-                jani_cond = _merge_conditions(
-                    previous_conditions).replace_event(trigger_event)
-                sub_edges, sub_locs = _append_scxml_body_to_jani_automaton(
-                    jani_automaton, events_holder, ec.get_else_execution(), interm_loc_before,
-                    interm_loc_after, '-'.join([hash_str, _hash_element(ec), 'else']),
-                    JaniGuard(jani_cond), None)
-                new_edges.extend(sub_edges)
-                new_locations.extend(sub_locs)
-            # TODO: If no else branch, we probably need to add an branch with empty body!
+            # Add else branch: if no else is provided, we assume an empty else body!
+            else_execution_body = ec.get_else_execution()
+            else_execution_body = [] if else_execution_body is None else else_execution_body
+            print(f"Else: {ec.get_else_execution()}")
+            jani_cond = _merge_conditions(
+                previous_conditions).replace_event(trigger_event)
+            sub_edges, sub_locs = _append_scxml_body_to_jani_automaton(
+                jani_automaton, events_holder, ec.get_else_execution(), interm_loc_before,
+                interm_loc_after, '-'.join([hash_str, _hash_element(ec), 'else']),
+                JaniGuard(jani_cond), None)
+            new_edges.extend(sub_edges)
+            new_locations.extend(sub_locs)
+            # Prepare the edge from the end of the if-else block
             new_edges.append(JaniEdge({
                 "location": interm_loc_after,
                 "action": edge_action_name,
@@ -309,11 +310,26 @@ def write_model(self):
         self.automaton.set_name(self.element.get_name())
         super().write_model()
         # Note: we don't support the initial tag (as state) https://www.w3.org/TR/scxml/#initial
-        # initial_state = self.element.get_state_by_id(self.element.get_initial_state_id())
-        # if initial_state.get_onentry() is not None:
-        #     raise NotImplementedError("Initial state with onentry not supported.")
-        # else:
-        self.automaton.make_initial(self.element.get_initial_state_id())
+        initial_state_id = self.element.get_initial_state_id()
+        initial_state = self.element.get_state_by_id(initial_state_id)
+        # Make sure we execute the onentry block of the initial state at the start
+        if initial_state.get_onentry() is not None:
+            source_state = f"{initial_state_id}-first-exec"
+            target_state = initial_state_id
+            onentry_body = initial_state.get_onentry()
+            hash_str = _hash_element([source_state, target_state, "onentry"])
+            new_edges, new_locations = _append_scxml_body_to_jani_automaton(
+                self.automaton, self.events_holder, onentry_body, source_state,
+                target_state, hash_str, None, None)
+            # Add the initial state and start sequence to the automaton
+            self.automaton.add_location(source_state)
+            self.automaton.make_initial(source_state)
+            for edge in new_edges:
+                self.automaton.add_edge(edge)
+            for loc in new_locations:
+                self.automaton.add_location(loc)
+        else:
+            self.automaton.make_initial(initial_state_id)
 
 
 class StateTag(BaseTag):
@@ -325,15 +341,35 @@ class StateTag(BaseTag):
     def get_children(self) -> List[ScxmlTransition]:
         # Here we care only about the transitions.
         # onentry and onexit are handled in the TransitionTag
-        # TODO: If multiple conditional transitions, we need to track and negate the previous cond.
         state_transitions = self.element.get_body()
         return [] if state_transitions is None else state_transitions
 
     def write_model(self):
         state_name = self.element.get_id()
         self.automaton.add_location(state_name)
-        # TODO: Make sure initial states that have onentry execute the onentry block at start
-        super().write_model()
+        # Dictionary tracking the conditional trigger-based transitions
+        self._event_to_conditions: Dict[str, List[str]] = {}
+        # List of events that trigger transitions without conditions
+        self._events_no_condition: List[str] = []
+        for child in self.children:
+            transition_events = child.element.get_events()
+            transition_event = "" if transition_events is None else transition_events[0]
+            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, []))
+            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."
+                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):
@@ -345,12 +381,18 @@ class TransitionTag(BaseTag):
     def get_children(self) -> List[ScxmlBase]:
         return []
 
+    def set_previous_siblings_conditions(self, conditions_scripts: List[str]):
+        """Add conditions from previous transitions with same event trigger."""
+        self._previous_conditions = conditions_scripts
+
     def write_model(self):
-        scxml_root = self.call_trace[0]
-        current_state = self.call_trace[-1]
-        current_state_id = current_state.get_id()
-        target_state_id = self.element.get_target_state_id()
-        target_state = scxml_root.get_state_by_id(target_state_id)
+        assert hasattr(self, "_previous_conditions"), \
+            "Make sure 'set_previous_siblings_conditions' was called before."
+        scxml_root: ScxmlRoot = self.call_trace[0]
+        current_state: ScxmlState = self.call_trace[-1]
+        current_state_id: str = current_state.get_id()
+        target_state_id: str = self.element.get_target_state_id()
+        target_state: ScxmlState = scxml_root.get_state_by_id(target_state_id)
         assert target_state is not None, f"Transition's target state {target_state_id} not found."
         event_name = self.element.get_events()
         # TODO: Need to extend this to support multiple events
@@ -370,14 +412,25 @@ def write_model(self):
             existing_event = self.events_holder.get_event(transition_trigger_event)
             existing_event.add_receiver(
                 self.automaton.get_name(), current_state_id, action_name)
+        # Prepare the previous expressions for the transition guard
+        previous_expressions = [
+            parse_ecmascript_to_jani_expression(cond) for cond in self._previous_conditions]
+        if event_name is not None:
+            for expr in previous_expressions:
+                expr.replace_event(transition_trigger_event)
         transition_condition = self.element.get_condition()
         if transition_condition is not None:
-            expression = parse_ecmascript_to_jani_expression(transition_condition)
+            current_expression = parse_ecmascript_to_jani_expression(transition_condition)
             if event_name is not None:
-                expression.replace_event(transition_trigger_event)
-            guard = JaniGuard(expression)
+                current_expression.replace_event(transition_trigger_event)
+            # If there are multiple transitions for an event, consider the previous conditions
+            merged_expression = _merge_conditions(previous_expressions, current_expression)
+            guard = JaniGuard(merged_expression)
         else:
-            guard = None
+            if len(previous_expressions) > 0:
+                guard = JaniGuard(_merge_conditions(previous_expressions))
+            else:
+                guard = None
 
         original_transition_body = self.element.get_executable_body()
 

jani_generator/test/_test_data/battery_example/output_GROUND_TRUTH.jani

@@ -27,6 +27,9 @@
         {
             "name": "level_on_send"
         },
+        {
+            "name": "use_battery-first-exec-use_battery-766fa6e4"
+        },
         {
             "name": "use_battery-use_battery-1b935c10"
         }
@@ -40,10 +43,16 @@
                 },
                 {
                     "name": "use_battery-1-1b935c10"
+                },
+                {
+                    "name": "use_battery-first-exec"
+                },
+                {
+                    "name": "use_battery-first-exec-0-766fa6e4"
                 }
             ],
             "initial-locations": [
-                "use_battery"
+                "use_battery-first-exec"
             ],
             "edges": [
                 {
@@ -86,6 +95,37 @@
                         }
                     ],
                     "action": "level_on_send"
+                },
+                {
+                    "location": "use_battery-first-exec",
+                    "destinations": [
+                        {
+                            "location": "use_battery-first-exec-0-766fa6e4",
+                            "assignments": []
+                        }
+                    ],
+                    "action": "use_battery-first-exec-use_battery-766fa6e4"
+                },
+                {
+                    "location": "use_battery-first-exec-0-766fa6e4",
+                    "destinations": [
+                        {
+                            "location": "use_battery",
+                            "assignments": [
+                                {
+                                    "ref": "level.data",
+                                    "value": "battery_percent",
+                                    "index": 0
+                                },
+                                {
+                                    "ref": "level.valid",
+                                    "value": true,
+                                    "index": 0
+                                }
+                            ]
+                        }
+                    ],
+                    "action": "level_on_send"
                 }
             ],
             "variables": [
@@ -223,6 +263,14 @@
                     "level_on_send"
                 ]
             },
+            {
+                "result": "use_battery-first-exec-use_battery-766fa6e4",
+                "synchronise": [
+                    "use_battery-first-exec-use_battery-766fa6e4",
+                    null,
+                    null
+                ]
+            },
             {
                 "result": "use_battery-use_battery-1b935c10",
                 "synchronise": [

jani_generator/test/test_systemtest_scxml_to_jani.py

@@ -53,10 +53,10 @@ def test_basic_example(self):
         convert_scxml_root_to_jani_automaton(scxml_root, jani_a, eh)
 
         automaton = jani_a.as_dict(constant={})
-        self.assertEqual(len(automaton["locations"]), 1)
-        init_location = automaton["locations"][0]
-        self.assertIn("Initial", init_location["name"])
-        self.assertIn("Initial", automaton["initial-locations"])
+        self.assertEqual(len(automaton["locations"]), 2)
+        locations = [loc['name'] for loc in automaton["locations"]]
+        self.assertIn("Initial-first-exec", locations)
+        self.assertIn("Initial-first-exec", automaton["initial-locations"])
 
     def test_battery_drainer(self):
         """
@@ -73,12 +73,11 @@ def test_battery_drainer(self):
 
         automaton = jani_a.as_dict(constant={})
         self.assertEqual(automaton["name"], "BatteryDrainer")
-        self.assertEqual(len(automaton["locations"]), 2)
+        self.assertEqual(len(automaton["locations"]), 4)
         self.assertEqual(len(automaton["initial-locations"]), 1)
-        init_location = automaton["locations"][0]
-        self.assertEqual(init_location['name'],
-                         automaton.get("initial-locations")[0])
-        self.assertEqual(len(automaton["edges"]), 2)
+        locations = [loc['name'] for loc in automaton["locations"]]
+        self.assertIn(automaton.get("initial-locations")[0], locations)
+        self.assertEqual(len(automaton["edges"]), 4)
 
         # Variables
         self.assertEqual(len(automaton["variables"]), 1)
@@ -154,7 +153,7 @@ def test_example_with_sync(self):
         self.assertIn({"automaton": "BatteryManager"}, elements)
         self.assertIn({"automaton": "level"}, elements)
         syncs = jani_dict["system"]["syncs"]
-        self.assertEqual(len(syncs), 3)
+        self.assertEqual(len(syncs), 4)
         self.assertIn({'result': 'level_on_send',
                        'synchronise': [
                            'level_on_send', None, 'level_on_send']},