Convertings strings to constant nrs

src/as2fm/jani_generator/main.py

@@ -81,6 +81,12 @@ def main_scxml_to_jani(_args: Optional[Sequence[str]] = None) -> None:
     parser.add_argument(
         "--jani-out-file", type=str, default="main.jani", help="Path to the generated jani file."
     )
+    parser.add_argument(
+        "--replace-strings",
+        action="store_true",
+        help="Replace string constants with unique numbers. "
+        + "(Workaround Required by most model checkers)",
+    )
     parser.add_argument("main_xml", type=str, help="The path to the main XML file to interpret.")
     args = parser.parse_args(_args)
 
@@ -92,7 +98,7 @@ def main_scxml_to_jani(_args: Optional[Sequence[str]] = None) -> None:
     assert os.path.isfile(main_xml_file), f"File {main_xml_file} does not exist."
     assert len(jani_out_file) > 0, "Output file not provided."
 
-    interpret_top_level_xml(main_xml_file, jani_out_file, scxml_out_dir)
+    interpret_top_level_xml(main_xml_file, jani_out_file, scxml_out_dir, args.replace_strings)
 
 
 if __name__ == "__main__":

src/as2fm/jani_generator/scxml_helpers/full_model_type.py

@@ -0,0 +1,37 @@
+# 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.
+
+"""
+Container to store full model
+"""
+
+from dataclasses import dataclass, field
+from typing import List, Optional
+
+
+@dataclass()
+class FullModel:
+    """
+    A class to represent the full model.
+    """
+
+    max_time: Optional[int] = None
+    max_array_size: int = field(default=100)
+    bt_tick_rate: float = field(default=1.0)
+    bt: Optional[str] = None
+    plugins: List[str] = field(default_factory=list)
+    skills: List[str] = field(default_factory=list)
+    components: List[str] = field(default_factory=list)
+    properties: List[str] = field(default_factory=list)

src/as2fm/jani_generator/scxml_helpers/string_replacer.py

@@ -0,0 +1,93 @@
+# 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.
+
+"""
+Module to go through existing bt.xml and scxml files and replace strings with constant numbers,
+because model checkers usually don't like strings.
+
+- preprocessing step that looks through the bt.xml and all scxmls for string constants
+- fixed mapping between strings constants and unique integers (like a enum)
+- replace strings with corresponding numbers in bt.xml and scxmls
+
+e.g.
+(in bt.xml)
+```
+<DetectObject name="DetectSnack" object="snacks0"/>
+```
+turns into ...
+```
+<DetectObject name="DetectSnack" object="8"/>
+```
+and
+(in scxml)
+```
+<field name="data" expr="_msg.data == 'snacks0'" />
+```
+turns into ...
+```
+<field name="data" expr="_msg.data == 8" />
+```
+"""
+from typing import Set
+
+from lxml import etree as ET
+
+from as2fm.jani_generator.scxml_helpers.full_model_type import FullModel
+
+
+def replace_strings_in_model(model: FullModel) -> FullModel:
+    """
+    Replace all strings in the model with corresponding numbers.
+    """
+    # Find all strings in the model
+    # strings = _find_strings_in_model(model)
+    # TODO ...
+
+    return model
+
+
+def _find_strings_in_model(model: FullModel) -> Set[str]:
+    """
+    Find all strings in the model.
+    """
+    strings: Set[str] = set()
+    if model.bt is not None:
+        strings.update(_find_strings_in_bt_xml(model.bt))
+    # for scxml in model.scxmls:
+    #     strings.extend(_find_strings_in_scxml(scxml.xml))
+    return strings
+
+
+def _find_strings_in_bt_xml(bt_xml_fname: str) -> Set[str]:
+    """
+    Find all strings used in ports in the bt.xml file.
+
+    e.g. 'pantry' in the following line:
+    <Action ID="NavigateAction" name="navigate" data="pantry" />
+    """
+    ATTRS_THAT_CANT_BE_PORTS = ["name", "ID"]
+    strings = set()
+    with open(bt_xml_fname, "r", encoding="utf-8") as f:
+        et = ET.parse(f)
+        root = et.getroot()
+        for node in root.iter():
+            for key in node.keys():
+                if key in ATTRS_THAT_CANT_BE_PORTS:
+                    continue
+                port_value = node.get(key)
+                if not isinstance(port_value, str):
+                    continue
+                strings.add(port_value)
+    return strings

src/as2fm/jani_generator/scxml_helpers/top_level_interpreter.py

@@ -19,7 +19,6 @@
 
 import json
 import os
-from dataclasses import dataclass, field
 from typing import Dict, List, Optional, Tuple
 
 import lxml.etree as ET
@@ -34,23 +33,13 @@
 )
 from as2fm.jani_generator.ros_helpers.ros_service_handler import RosServiceHandler
 from as2fm.jani_generator.ros_helpers.ros_timer import RosTimer, make_global_timer_scxml
+from as2fm.jani_generator.scxml_helpers.full_model_type import FullModel
 from as2fm.jani_generator.scxml_helpers.scxml_to_jani import convert_multiple_scxmls_to_jani
+from as2fm.jani_generator.string_replacer import replace_strings_in_model
 from as2fm.scxml_converter.bt_converter import bt_converter
 from as2fm.scxml_converter.scxml_entries import ScxmlRoot
 
 
-@dataclass()
-class FullModel:
-    max_time: Optional[int] = None
-    max_array_size: int = field(default=100)
-    bt_tick_rate: float = field(default=1.0)
-    bt: Optional[str] = None
-    plugins: List[str] = field(default_factory=list)
-    skills: List[str] = field(default_factory=list)
-    components: List[str] = field(default_factory=list)
-    properties: List[str] = field(default_factory=list)
-
-
 def _parse_time_element(time_element: ET.Element) -> int:
     """
     Interpret a time element. Output is in nanoseconds.
@@ -195,7 +184,10 @@ def generate_plain_scxml_models_and_timers(
 
 
 def interpret_top_level_xml(
-    xml_path: str, jani_file: str, generated_scxmls_dir: Optional[str] = None
+    xml_path: str,
+    jani_file: str,
+    generated_scxmls_dir: Optional[str] = None,
+    replace_strings: bool = False,
 ):
     """
     Interpret the top-level XML file as a Jani model. And write it to a file.
@@ -211,6 +203,9 @@ def interpret_top_level_xml(
     assert model.max_time is not None, f"Max time must be defined in {xml_path}."
     plain_scxml_models, all_timers = generate_plain_scxml_models_and_timers(model)
 
+    if replace_strings:
+        model = replace_strings_in_model(model)
+
     if generated_scxmls_dir is not None:
         plain_scxml_dir = os.path.join(model_dir, generated_scxmls_dir)
         os.makedirs(plain_scxml_dir, exist_ok=True)

support_pkgs/delib_ws_24_interfaces/CMakeLists.txt

@@ -15,8 +15,10 @@ find_package(ament_cmake REQUIRED)
 find_package(rosidl_default_generators REQUIRED)
 
 rosidl_generate_interfaces(${PROJECT_NAME}
-  "action/Navigate.action"
-  "action/Pick.action"
+  "action/NavigateInt.action"
+  "action/NavigateStr.action"
+  "action/PickInt.action"
+  "action/PickStr.action"
   "action/Place.action"
 )
 

support_pkgs/delib_ws_24_interfaces/action/NavigateStr.action

@@ -0,0 +1,6 @@
+# Goal
+str goal_loc
+---
+# Result
+---
+# Feedback

support_pkgs/delib_ws_24_interfaces/action/PickStr.action

@@ -0,0 +1,6 @@
+# Goal
+str object_id
+---
+# Result
+---
+# Feedback

test/jani_generator/_test_data/delibws24_p1/bt_navigate_action.scxml → test/jani_generator/_test_data/delibws24_p1_int/bt_navigate_action.scxml

@@ -6,7 +6,7 @@
     model_src=""
     xmlns="http://www.w3.org/2005/07/scxml">
 
-    <ros_action_client name="act" action_name="/go_to_goal" type="delib_ws_24_interfaces/Navigate" />
+    <ros_action_client name="act" action_name="/go_to_goal" type="delib_ws_24_interfaces/NavigateInt" />
 
     <datamodel>
         <data id="tmp_result" type="bool" expr="false" />

test/jani_generator/_test_data/delibws24_p1/bt_pick_action.scxml → test/jani_generator/_test_data/delibws24_p1_int/bt_pick_action.scxml

@@ -6,7 +6,7 @@
     model_src=""
     xmlns="http://www.w3.org/2005/07/scxml">
 
-    <ros_action_client name="act" action_name="/pick_object" type="delib_ws_24_interfaces/Pick" />
+    <ros_action_client name="act" action_name="/pick_object" type="delib_ws_24_interfaces/PickInt" />
 
     <datamodel>
         <data id="tmp_result" type="bool" expr="false" />

test/jani_generator/_test_data/delibws24_p1/world.scxml → test/jani_generator/_test_data/delibws24_p1_int/world.scxml

@@ -15,8 +15,8 @@
     0 .. snacks0
     -->
 
-    <ros_action_server name="act_nav" action_name="/go_to_goal" type="delib_ws_24_interfaces/Navigate" />
-    <ros_action_server name="act_pick" action_name="/pick_object" type="delib_ws_24_interfaces/Pick" />
+    <ros_action_server name="act_nav" action_name="/go_to_goal" type="delib_ws_24_interfaces/NavigateInt" />
+    <ros_action_server name="act_pick" action_name="/pick_object" type="delib_ws_24_interfaces/PickInt" />
     <ros_action_server name="act_place" action_name="/place_object" type="delib_ws_24_interfaces/Place" />
     <ros_topic_publisher name="pub_snacks0" topic="/snacks0_loc" type="std_msgs/Int32" />
 

test/jani_generator/test_systemtest_scxml_to_jani.py

@@ -302,7 +302,7 @@ def test_ros_fibonacci_action_single_client_example(self):
     @pytest.mark.skip(reason="Not yet working. The BT ticking needs some revision.")
     def test_ros_delib_ws_2024_p1(self):
         """Test the ROS Deliberation Workshop example works."""
-        self._test_with_main("delibws24_p1", True, "snack_at_table", True)
+        self._test_with_main("delibws24_p1_int", True, "snack_at_table", True)
 
     def test_robot_navigation_demo(self):
         """Test the robot demo."""

test/scxml_converter/_test_data/delibws24_p1_str/bt.xml

@@ -0,0 +1,11 @@
+<root BTCPP_format="4">
+    <BehaviorTree>
+        <!-- For now use a normal sequence, since failures aren't expected yet -->
+        <Sequence>
+            <Action ID="NavigateAction" name="navigate" data="pantry" />
+            <Action ID="PickAction" name="pick" data="snacks0" />
+            <Action ID="NavigateAction" name="navigate" data="table" />
+            <Action ID="PlaceAction" name="place" />
+        </Sequence>
+    </BehaviorTree>
+</root>

test/scxml_converter/_test_data/delibws24_p1_str/bt_navigate_action.scxml

@@ -0,0 +1,57 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<scxml
+    initial="initial"
+    version="1.0"
+    name="NavigateAction"
+    model_src=""
+    xmlns="http://www.w3.org/2005/07/scxml">
+
+    <ros_action_client name="act" action_name="/go_to_goal" type="delib_ws_24_interfaces/NavigateStr" />
+
+    <datamodel>
+        <data id="tmp_result" type="bool" expr="false" />
+    </datamodel>
+
+    <bt_declare_port_in key="data" type="str" />
+
+    <!-- Assumption: We get an event when the node is ticked by the BT, named "bt_tick". -->
+    <!-- Assumption: We have to send an event to the BT, that is either "bt_success" or "bt_failure". -->
+
+    <state id="initial">
+        <transition event="bt_tick" target="wait_result">
+            <ros_action_send_goal name="act">
+                <field name="goal_loc">
+                    <expr>
+                        <bt_get_input key="data" />
+                    </expr>
+                </field>
+            </ros_action_send_goal>
+            <!-- Let's assume this is always successful. -->
+            <send event="bt_running" />
+        </transition>
+    </state>
+
+    <state id="wait_result">
+        <transition event="bt_tick" target="wait_result">
+            <send event="bt_running" />
+        </transition>
+        <ros_action_handle_success_result name="act" target="result_available">
+            <assign location="tmp_result" expr="true" />
+        </ros_action_handle_success_result>
+        <ros_action_handle_aborted_result name="act" target="result_available">
+            <assign location="tmp_result" expr="false" />
+        </ros_action_handle_aborted_result>
+
+    </state>
+
+    <state id="result_available">
+        <transition event="bt_tick" target="initial">
+            <if cond="tmp_result">
+                <send event="bt_success" />
+                <else/>
+                <send event="bt_failure" />
+            </if>
+        </transition>
+    </state>
+
+</scxml>