diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index e405e5b2..7efbe73c 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -55,7 +55,7 @@ jobs: 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 as2fm_common/.[dev] pip install scxml_converter/.[dev] # lint packages # TODO: add linting @@ -65,4 +65,4 @@ jobs: 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 + pytest-3 -vs as2fm_common jani_generator scxml_converter diff --git a/README.md b/README.md index 2bfbf4d3..490f46f4 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Model Checking Toolchain Components # Autonomous Systems to Formal Models (AS2FM) -> Please access the documentation via [convince-project.github.io/as2fm](https://convince-project.github.io/as2fm) +> Please access the documentation via [convince-project.github.io/AS2FM](https://convince-project.github.io/AS2FM) ## Further Information diff --git a/mc_toolchain_jani_common/pyproject.toml b/as2fm_common/pyproject.toml similarity index 94% rename from mc_toolchain_jani_common/pyproject.toml rename to as2fm_common/pyproject.toml index 36d3b028..b69753d2 100644 --- a/mc_toolchain_jani_common/pyproject.toml +++ b/as2fm_common/pyproject.toml @@ -3,7 +3,7 @@ requires = ["setuptools>=61.0.0", "wheel"] build-backend = "setuptools.build_meta" [project] -name = "mc_toolchain_jani_common" +name = "as2fm_common" version = "0.0.1" description = "" readme = "README.md" diff --git a/mc_toolchain_jani_common/src/mc_toolchain_jani_common/common.py b/as2fm_common/src/as2fm_common/common.py similarity index 100% rename from mc_toolchain_jani_common/src/mc_toolchain_jani_common/common.py rename to as2fm_common/src/as2fm_common/common.py diff --git a/mc_toolchain_jani_common/src/mc_toolchain_jani_common/ecmascript_interpretation.py b/as2fm_common/src/as2fm_common/ecmascript_interpretation.py similarity index 95% rename from mc_toolchain_jani_common/src/mc_toolchain_jani_common/ecmascript_interpretation.py rename to as2fm_common/src/as2fm_common/ecmascript_interpretation.py index 66237403..95c70ab7 100644 --- a/mc_toolchain_jani_common/src/mc_toolchain_jani_common/ecmascript_interpretation.py +++ b/as2fm_common/src/as2fm_common/ecmascript_interpretation.py @@ -21,7 +21,7 @@ import js2py -from mc_toolchain_jani_common.common import ValidTypes +from as2fm_common.common import ValidTypes def interpret_ecma_script_expr( diff --git a/mc_toolchain_jani_common/test/test_utilities_smc_strom.py b/as2fm_common/test/test_utilities_smc_strom.py similarity index 100% rename from mc_toolchain_jani_common/test/test_utilities_smc_strom.py rename to as2fm_common/test/test_utilities_smc_strom.py diff --git a/docs/README.md b/docs/README.md index 736b3cd0..43096e61 100644 --- a/docs/README.md +++ b/docs/README.md @@ -3,7 +3,7 @@ Before you can build the documentation, you need to install the required packages as described above, since also the code API documentation of those packages is built. ``` -pip install ../mc_toolchain_jani_common +pip install ../as2fm_common pip install ../scxml_converter pip install ../jani_generator pip install -r requirements.txt diff --git a/docs/source/api.rst b/docs/source/api.rst index 8d12e04b..136ee6be 100644 --- a/docs/source/api.rst +++ b/docs/source/api.rst @@ -6,7 +6,7 @@ API :template: custom-module-template.rst :recursive: - mc_toolchain_jani_common + as2fm_common jani_generator scxml_converter diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst index d4f23df1..e8bd8360 100644 --- a/docs/source/tutorials.rst +++ b/docs/source/tutorials.rst @@ -9,7 +9,7 @@ To run the Python scripts install the required dependencies with the following c .. code-block:: bash - python3 -m pip install mc_toolchain_jani_common/ + python3 -m pip install as2fm_common/ python3 -m pip install jani_generator/ python3 -m pip install scxml_converter/ diff --git a/jani_generator/src/jani_generator/jani_entries/jani_variable.py b/jani_generator/src/jani_generator/jani_entries/jani_variable.py index d8434f10..851ca478 100644 --- a/jani_generator/src/jani_generator/jani_entries/jani_variable.py +++ b/jani_generator/src/jani_generator/jani_entries/jani_variable.py @@ -20,7 +20,7 @@ from typing import Optional, Union, get_args from jani_generator.jani_entries import JaniExpression, JaniValue -from mc_toolchain_jani_common.common import ValidTypes +from as2fm_common.common import ValidTypes class JaniVariable: diff --git a/jani_generator/src/jani_generator/scxml_helpers/scxml_data.py b/jani_generator/src/jani_generator/scxml_helpers/scxml_data.py index d846d899..e37c8572 100644 --- a/jani_generator/src/jani_generator/scxml_helpers/scxml_data.py +++ b/jani_generator/src/jani_generator/scxml_helpers/scxml_data.py @@ -21,8 +21,8 @@ import xml.etree.ElementTree as ET from typing import Dict, List, Optional, get_args -from mc_toolchain_jani_common.common import ros_type_name_to_python_type -from mc_toolchain_jani_common.ecmascript_interpretation import \ +from as2fm_common.common import ros_type_name_to_python_type +from as2fm_common.ecmascript_interpretation import \ interpret_ecma_script_expr from jani_generator.jani_entries.jani_expression import JaniExpression from jani_generator.jani_entries.jani_variable import JaniVariable, ValidTypes diff --git a/jani_generator/src/jani_generator/scxml_helpers/scxml_tags.py b/jani_generator/src/jani_generator/scxml_helpers/scxml_tags.py index 86361eaa..8442deb2 100644 --- a/jani_generator/src/jani_generator/scxml_helpers/scxml_tags.py +++ b/jani_generator/src/jani_generator/scxml_helpers/scxml_tags.py @@ -30,7 +30,7 @@ from jani_generator.scxml_helpers.scxml_event import Event, EventsHolder from jani_generator.scxml_helpers.scxml_expression import \ parse_ecmascript_to_jani_expression -from mc_toolchain_jani_common.ecmascript_interpretation import \ +from as2fm_common.ecmascript_interpretation import \ interpret_ecma_script_expr from scxml_converter.scxml_entries import (ScxmlAssign, ScxmlBase, ScxmlDataModel, ScxmlExecutionBody, diff --git a/jani_generator/src/jani_generator/scxml_helpers/top_level_interpreter.py b/jani_generator/src/jani_generator/scxml_helpers/top_level_interpreter.py index 2aa150b9..e2ad65ee 100644 --- a/jani_generator/src/jani_generator/scxml_helpers/top_level_interpreter.py +++ b/jani_generator/src/jani_generator/scxml_helpers/top_level_interpreter.py @@ -24,7 +24,7 @@ from xml.etree import ElementTree as ET -from mc_toolchain_jani_common.common import remove_namespace +from as2fm_common.common import remove_namespace from scxml_converter.bt_converter import bt_converter from scxml_converter.scxml_converter import ros_to_scxml_converter from jani_generator.jani_entries import JaniModel diff --git a/jani_generator/test/_test_data/ros_example/main-prepared.jani b/jani_generator/test/_test_data/ros_example/main-prepared.jani new file mode 100644 index 00000000..bb8f0703 --- /dev/null +++ b/jani_generator/test/_test_data/ros_example/main-prepared.jani @@ -0,0 +1,377 @@ +{ + "jani-version": 1, + "name": "", + "type": "mdp", + "metadata": { + "description": "Autogenerated with CONVINCE toolchain" + }, + "variables": [ + { + "name": "ros_topic.level.data", + "type": "int", + "transient": false, + "initial-value": 0 + }, + { + "name": "ros_topic.level.valid", + "type": "bool", + "transient": false, + "initial-value": false + } + ], + "constants": [], + "actions": [ + { + "name": "global_timer_action_0" + }, + { + "name": "ros_time_rate.my_timer_on_receive" + }, + { + "name": "ros_topic.level_on_receive" + }, + { + "name": "ros_topic.level_on_send" + } + ], + "automata": [ + { + "name": "BatteryDrainer", + "locations": [ + { + "name": "use_battery" + }, + { + "name": "use_battery_on_entry" + } + ], + "initial-locations": [ + "use_battery_on_entry" + ], + "edges": [ + { + "location": "use_battery", + "destinations": [ + { + "location": "use_battery_on_entry", + "assignments": [ + { + "ref": "battery_percent", + "value": { + "op": "-", + "left": "battery_percent", + "right": 1 + }, + "index": 0 + } + ] + } + ], + "action": "ros_time_rate.my_timer_on_receive", + "guard": { + "exp": { + "op": ">", + "left": "battery_percent", + "right": 0 + } + } + }, + { + "location": "use_battery_on_entry", + "destinations": [ + { + "location": "use_battery", + "probability": { + "exp": 1.0 + }, + "assignments": [ + { + "ref": "ros_topic.level.data", + "value": "battery_percent", + "index": 0 + }, + { + "ref": "ros_topic.level.valid", + "value": true, + "index": 1 + } + ] + } + ], + "action": "ros_topic.level_on_send" + } + ], + "variables": [ + { + "name": "battery_percent", + "type": "int", + "transient": false, + "initial-value": 100 + } + ] + }, + { + "name": "BatteryManager", + "locations": [ + { + "name": "check_battery" + } + ], + "initial-locations": [ + "check_battery" + ], + "edges": [ + { + "location": "check_battery", + "destinations": [ + { + "location": "check_battery", + "assignments": [ + { + "ref": "battery_alarm", + "value": { + "op": "<", + "left": "ros_topic.level.data", + "right": 30 + }, + "index": 0 + } + ] + } + ], + "action": "ros_topic.level_on_receive" + } + ], + "variables": [ + { + "name": "battery_alarm", + "type": "bool", + "transient": false, + "initial-value": false + } + ] + }, + { + "name": "global_timer", + "locations": [ + { + "name": "loc" + } + ], + "initial-locations": [ + "loc" + ], + "edges": [ + { + "location": "loc", + "destinations": [ + { + "location": "loc", + "assignments": [ + { + "ref": "t", + "value": { + "op": "+", + "left": "t", + "right": 1 + }, + "index": 0 + }, + { + "ref": "my_timer_needed", + "value": { + "op": "=", + "left": { + "op": "%", + "left": "t", + "right": 1 + }, + "right": 0 + }, + "index": 1 + } + ] + } + ], + "action": "global_timer_action_0", + "guard": { + "exp": { + "op": "¬", + "exp": "my_timer_needed" + } + } + }, + { + "location": "loc", + "destinations": [ + { + "location": "loc", + "assignments": [ + { + "ref": "my_timer_needed", + "value": false, + "index": 0 + } + ] + } + ], + "action": "ros_time_rate.my_timer_on_receive", + "guard": { + "exp": "my_timer_needed" + } + } + ], + "variables": [ + { + "name": "t", + "type": "int", + "transient": false, + "initial-value": 0 + }, + { + "name": "my_timer_needed", + "type": "bool", + "transient": false, + "initial-value": true + } + ] + }, + { + "name": "ros_topic.level", + "locations": [ + { + "name": "received" + }, + { + "name": "waiting" + } + ], + "initial-locations": [ + "waiting" + ], + "edges": [ + { + "location": "waiting", + "destinations": [ + { + "location": "received", + "probability": { + "exp": 1.0 + }, + "assignments": [] + } + ], + "action": "ros_topic.level_on_send" + }, + { + "location": "received", + "destinations": [ + { + "location": "received", + "probability": { + "exp": 1.0 + }, + "assignments": [] + } + ], + "action": "ros_topic.level_on_send" + }, + { + "location": "received", + "destinations": [ + { + "location": "waiting", + "probability": { + "exp": 1.0 + }, + "assignments": [] + } + ], + "action": "ros_topic.level_on_receive" + } + ] + } + ], + "system": { + "elements": [ + { + "automaton": "BatteryDrainer" + }, + { + "automaton": "BatteryManager" + }, + { + "automaton": "global_timer" + }, + { + "automaton": "ros_topic.level" + } + ], + "syncs": [ + { + "result": "ros_topic.level_on_send", + "synchronise": [ + "ros_topic.level_on_send", + null, + null, + "ros_topic.level_on_send" + ] + }, + { + "result": "ros_topic.level_on_receive", + "synchronise": [ + null, + "ros_topic.level_on_receive", + null, + "ros_topic.level_on_receive" + ] + }, + { + "result": "ros_time_rate.my_timer_on_receive", + "synchronise": [ + "ros_time_rate.my_timer_on_receive", + null, + "ros_time_rate.my_timer_on_receive", + null + ] + }, + { + "result": "global_timer_action_0", + "synchronise": [ + null, + null, + "global_timer_action_0", + null + ] + } + ] + }, + "properties": [ + { + "name": "battery_depleted", + "expression": { + "op": "filter", + "fun": "values", + "values": { + "op": "Pmin", + "exp": { + "left": true, + "op": "U", + "right": { + "left": { + "op": "≤", + "left": "ros_topic.level.data", + "right": 0 + }, + "op": "∧", + "right": "ros_topic.level.valid" + } + } + }, + "states": { + "op": "initial" + } + } + } + ] +} \ No newline at end of file diff --git a/scxml_converter/src/scxml_converter/scxml_converter.py b/scxml_converter/src/scxml_converter/scxml_converter.py index 5545037c..621108da 100644 --- a/scxml_converter/src/scxml_converter/scxml_converter.py +++ b/scxml_converter/src/scxml_converter/scxml_converter.py @@ -25,8 +25,8 @@ from scxml_converter.scxml_entries import ScxmlRoot -from mc_toolchain_jani_common.common import ros_type_name_to_python_type -from mc_toolchain_jani_common.ecmascript_interpretation import \ +from as2fm_common.common import ros_type_name_to_python_type +from as2fm_common.ecmascript_interpretation import \ interpret_ecma_script_expr BASIC_FIELD_TYPES = ['boolean', 'int32', 'int16', 'float', 'double']