diff --git a/src/as2fm/jani_generator/main.py b/src/as2fm/jani_generator/main.py
index 0f9b5b73..ac6c2053 100644
--- a/src/as2fm/jani_generator/main.py
+++ b/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__":
diff --git a/src/as2fm/jani_generator/scxml_helpers/full_model_type.py b/src/as2fm/jani_generator/scxml_helpers/full_model_type.py
new file mode 100644
index 00000000..39212a00
--- /dev/null
+++ b/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)
diff --git a/src/as2fm/jani_generator/scxml_helpers/string_replacer.py b/src/as2fm/jani_generator/scxml_helpers/string_replacer.py
new file mode 100644
index 00000000..10bf0c65
--- /dev/null
+++ b/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)
+```
+
+```
+turns into ...
+```
+
+```
+and
+(in scxml)
+```
+
+```
+turns into ...
+```
+
+```
+"""
+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:
+
+ """
+ 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
diff --git a/src/as2fm/jani_generator/scxml_helpers/top_level_interpreter.py b/src/as2fm/jani_generator/scxml_helpers/top_level_interpreter.py
index 066a6aa9..1427ee19 100644
--- a/src/as2fm/jani_generator/scxml_helpers/top_level_interpreter.py
+++ b/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)
diff --git a/support_pkgs/delib_ws_24_interfaces/CMakeLists.txt b/support_pkgs/delib_ws_24_interfaces/CMakeLists.txt
index 917f549f..14164928 100644
--- a/support_pkgs/delib_ws_24_interfaces/CMakeLists.txt
+++ b/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"
)
diff --git a/support_pkgs/delib_ws_24_interfaces/action/Navigate.action b/support_pkgs/delib_ws_24_interfaces/action/NavigateInt.action
similarity index 100%
rename from support_pkgs/delib_ws_24_interfaces/action/Navigate.action
rename to support_pkgs/delib_ws_24_interfaces/action/NavigateInt.action
diff --git a/support_pkgs/delib_ws_24_interfaces/action/NavigateStr.action b/support_pkgs/delib_ws_24_interfaces/action/NavigateStr.action
new file mode 100644
index 00000000..9c94a394
--- /dev/null
+++ b/support_pkgs/delib_ws_24_interfaces/action/NavigateStr.action
@@ -0,0 +1,6 @@
+# Goal
+str goal_loc
+---
+# Result
+---
+# Feedback
diff --git a/support_pkgs/delib_ws_24_interfaces/action/Pick.action b/support_pkgs/delib_ws_24_interfaces/action/PickInt.action
similarity index 100%
rename from support_pkgs/delib_ws_24_interfaces/action/Pick.action
rename to support_pkgs/delib_ws_24_interfaces/action/PickInt.action
diff --git a/support_pkgs/delib_ws_24_interfaces/action/PickStr.action b/support_pkgs/delib_ws_24_interfaces/action/PickStr.action
new file mode 100644
index 00000000..9af7434c
--- /dev/null
+++ b/support_pkgs/delib_ws_24_interfaces/action/PickStr.action
@@ -0,0 +1,6 @@
+# Goal
+str object_id
+---
+# Result
+---
+# Feedback
diff --git a/test/jani_generator/_test_data/delibws24_p1/bt.xml b/test/jani_generator/_test_data/delibws24_p1_int/bt.xml
similarity index 100%
rename from test/jani_generator/_test_data/delibws24_p1/bt.xml
rename to test/jani_generator/_test_data/delibws24_p1_int/bt.xml
diff --git a/test/jani_generator/_test_data/delibws24_p1/bt_navigate_action.scxml b/test/jani_generator/_test_data/delibws24_p1_int/bt_navigate_action.scxml
similarity index 97%
rename from test/jani_generator/_test_data/delibws24_p1/bt_navigate_action.scxml
rename to test/jani_generator/_test_data/delibws24_p1_int/bt_navigate_action.scxml
index 87dd9fad..6707cf9a 100644
--- a/test/jani_generator/_test_data/delibws24_p1/bt_navigate_action.scxml
+++ b/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">
-
+
diff --git a/test/jani_generator/_test_data/delibws24_p1/bt_original.xml b/test/jani_generator/_test_data/delibws24_p1_int/bt_original.xml
similarity index 100%
rename from test/jani_generator/_test_data/delibws24_p1/bt_original.xml
rename to test/jani_generator/_test_data/delibws24_p1_int/bt_original.xml
diff --git a/test/jani_generator/_test_data/delibws24_p1/bt_pick_action.scxml b/test/jani_generator/_test_data/delibws24_p1_int/bt_pick_action.scxml
similarity index 98%
rename from test/jani_generator/_test_data/delibws24_p1/bt_pick_action.scxml
rename to test/jani_generator/_test_data/delibws24_p1_int/bt_pick_action.scxml
index 22a4fee0..3c8703ac 100644
--- a/test/jani_generator/_test_data/delibws24_p1/bt_pick_action.scxml
+++ b/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">
-
+
diff --git a/test/jani_generator/_test_data/delibws24_p1/bt_place_action.scxml b/test/jani_generator/_test_data/delibws24_p1_int/bt_place_action.scxml
similarity index 100%
rename from test/jani_generator/_test_data/delibws24_p1/bt_place_action.scxml
rename to test/jani_generator/_test_data/delibws24_p1_int/bt_place_action.scxml
diff --git a/test/jani_generator/_test_data/delibws24_p1/main.xml b/test/jani_generator/_test_data/delibws24_p1_int/main.xml
similarity index 100%
rename from test/jani_generator/_test_data/delibws24_p1/main.xml
rename to test/jani_generator/_test_data/delibws24_p1_int/main.xml
diff --git a/test/jani_generator/_test_data/delibws24_p1/properties.jani b/test/jani_generator/_test_data/delibws24_p1_int/properties.jani
similarity index 100%
rename from test/jani_generator/_test_data/delibws24_p1/properties.jani
rename to test/jani_generator/_test_data/delibws24_p1_int/properties.jani
diff --git a/test/jani_generator/_test_data/delibws24_p1/world.scxml b/test/jani_generator/_test_data/delibws24_p1_int/world.scxml
similarity index 96%
rename from test/jani_generator/_test_data/delibws24_p1/world.scxml
rename to test/jani_generator/_test_data/delibws24_p1_int/world.scxml
index 9ef6df8c..0c27ddc1 100644
--- a/test/jani_generator/_test_data/delibws24_p1/world.scxml
+++ b/test/jani_generator/_test_data/delibws24_p1_int/world.scxml
@@ -15,8 +15,8 @@
0 .. snacks0
-->
-
-
+
+
diff --git a/test/jani_generator/test_systemtest_scxml_to_jani.py b/test/jani_generator/test_systemtest_scxml_to_jani.py
index ee63ae59..e0312a2a 100644
--- a/test/jani_generator/test_systemtest_scxml_to_jani.py
+++ b/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."""
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/bt.xml b/test/scxml_converter/_test_data/delibws24_p1_str/bt.xml
new file mode 100644
index 00000000..0946bd66
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/bt.xml
@@ -0,0 +1,11 @@
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/bt_navigate_action.scxml b/test/scxml_converter/_test_data/delibws24_p1_str/bt_navigate_action.scxml
new file mode 100644
index 00000000..4b1da499
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/bt_navigate_action.scxml
@@ -0,0 +1,57 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/bt_pick_action.scxml b/test/scxml_converter/_test_data/delibws24_p1_str/bt_pick_action.scxml
new file mode 100644
index 00000000..427ec0b5
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/bt_pick_action.scxml
@@ -0,0 +1,56 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/bt_place_action.scxml b/test/scxml_converter/_test_data/delibws24_p1_str/bt_place_action.scxml
new file mode 100644
index 00000000..fbfebb8d
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/bt_place_action.scxml
@@ -0,0 +1,48 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/main.xml b/test/scxml_converter/_test_data/delibws24_p1_str/main.xml
new file mode 100644
index 00000000..f4a7890a
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/main.xml
@@ -0,0 +1,21 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/properties.jani b/test/scxml_converter/_test_data/delibws24_p1_str/properties.jani
new file mode 100644
index 00000000..4a3090cb
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/properties.jani
@@ -0,0 +1,29 @@
+{
+ "properties": [
+ {
+ "name": "snack_at_table",
+ "expression": {
+ "op": "filter",
+ "fun": "values",
+ "values": {
+ "op": "Pmin",
+ "exp": {
+ "op": "F",
+ "exp": {
+ "op": "∧",
+ "left": {
+ "op": "=",
+ "left": "topic_snacks0_loc_msg.ros_fields__data",
+ "right": 1
+ },
+ "right": "topic_snacks0_loc_msg.valid"
+ }
+ }
+ },
+ "states": {
+ "op": "initial"
+ }
+ }
+ }
+ ]
+}
diff --git a/test/scxml_converter/_test_data/delibws24_p1_str/world.scxml b/test/scxml_converter/_test_data/delibws24_p1_str/world.scxml
new file mode 100644
index 00000000..b95b9657
--- /dev/null
+++ b/test/scxml_converter/_test_data/delibws24_p1_str/world.scxml
@@ -0,0 +1,80 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+