NeVerTools · lorenzo0507 · Dec 18, 2025 · Dec 16, 2025 · Dec 16, 2025 · Dec 16, 2025
diff --git a/NOTICE b/NOTICE
@@ -31,3 +31,6 @@ Robert Bosch GmbH
 
 List, CEA, Université Paris-Saclay
     Matteo Morelli <matteo.morelli@cea.fr>
+
+Università degli Studi di Genova
+    Enrico Ghiorzi <enrico.ghiorzi@edu.unige.it>
diff --git a/docker-compose.yml b/docker-compose.yml
@@ -1,7 +1,7 @@
 
 services:
   base:
-    image: ghcr.io/nevertools/moco:latest # TODO fix link once release is up
+    image: ghcr.io/nevertools/moco:latest
     build:
       context: .
       dockerfile: .docker/Dockerfile

diff --git a/docs/README.md b/docs/README.md
@@ -1,6 +1,6 @@
 # Build documentation
 
-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.
+Before you can build the documentation, you need to install the required packages as described, since the code API documentation of those packages is also built.
 
 ```
 pip install ../moco_common

diff --git a/docs/source/conf.py b/docs/source/conf.py
@@ -33,7 +33,7 @@
 # -- Options for HTML output
 
 html_theme = "sphinx_rtd_theme"
-html_logo = "convince_logo_horizontal_200p.png"
+html_logo = "moco_logo.png"
 html_theme_options = {
     # 'analytics_id': 'G-XXXXXXXXXX',  #  Provided by Google in your dashboard
     # 'analytics_anonymize_ip': False,

diff --git a/docs/source/convince_logo_horizontal_200p.png b/docs/source/convince_logo_horizontal_200p.png
diff --git a/docs/source/graphics/ros_service_to_scxml.drawio.svg b/docs/source/graphics/ros_service_to_scxml.drawio.svg
diff --git a/docs/source/graphics/scxml_tutorial_ros_fetch_and_carry_bt_pick.drawio.png b/docs/source/graphics/scxml_tutorial_ros_fetch_and_carry_bt_pick.drawio.png
diff --git a/docs/source/graphics/scxml_tutorial_ros_fetch_and_carry_world.drawio.png b/docs/source/graphics/scxml_tutorial_ros_fetch_and_carry_world.drawio.png
diff --git a/...urce/graphics/scxml_tutorial_ros_fetch_and_carry_world_probabilistic.drawio.png b/...urce/graphics/scxml_tutorial_ros_fetch_and_carry_world_probabilistic.drawio.png
diff --git a/docs/source/graphics/uc2_bt_block_fell.drawio.png b/docs/source/graphics/uc2_bt_block_fell.drawio.png
diff --git a/docs/source/graphics/uc2_bt_move_block.drawio.png b/docs/source/graphics/uc2_bt_move_block.drawio.png
diff --git a/docs/source/graphics/uc2_bt_recover_block.drawio.png b/docs/source/graphics/uc2_bt_recover_block.drawio.png
diff --git a/docs/source/graphics/uc2_move_block.drawio.png b/docs/source/graphics/uc2_move_block.drawio.png
diff --git a/docs/source/graphics/uc2_recover_block.drawio.png b/docs/source/graphics/uc2_recover_block.drawio.png
diff --git a/docs/source/index.rst b/docs/source/index.rst
@@ -1,24 +1,24 @@
-Autonomous Systems to Formal Models (AS2FM)
+MOdel COmpiler (MOCO)
 ===============================================
 
-This is the documentation of the AS2FM tools from the `CONVINCE project's <https://convince-project.eu/>`_ toolbox. Besides illustrative :doc:`tutorials <../tutorials>` on how to use the provided scripts, their :doc:`API <../api>` is documented to foster contributions from users outside of the core project's team.
+This is the documentation of MOCO, a mantainability fork of AS2FM, originally developed from the `CONVINCE project <https://convince-project.eu/>`_.
+Besides illustrative :doc:`tutorials <../tutorials>` on how to use the provided scripts, the :doc:`API <../api>` is documented to foster contributions from users outside of the core project's team.
 
 Overview
 --------
 
-The purpose of the provided components is to convert all specifications of components of the robotic system under investigation into a format which can be given as input to model checkers for verifying the robustness of the system functionalities.
+The purpose of the provided program is to convert all specifications of components of the given robotic system into a format which can be given as input to model checkers for verifying the robustness of the system functionalities.
+It is intended for use with `GRAPE <https://github.com/NeVerTools/GRAPE>`_ and `SCAN <https://github.com/convince-project/SCAN>`_, respectively a development tool and a model checker.
 
-AS2FM focuses on converting the model of the system, provided as a combination of `Behavior Tree (BT) XML <https://www.behaviortree.dev/docs/learn-the-basics/xml_format>`_ and :ref:`High-Level (HL)-SCXML<hl_scxml>` into a format that can be used by model checking tools (i.e. JANI or plain SCXML).
+MOCO focuses on converting the RoaML model of the system into a plain `SCXML format <https://www.w3.org/TR/scxml/>`_ that can be used by model checking tools such as SCAN.
 A full robotic system and the information needed for model checking consists of:
 
-* one or multiple ROS nodes in SCXML,
-* the environment model in SCXML,
+* one or multiple ROS nodes in (A)SCXML,
+* the environment model in (A)SCXML,
 * the Behavior Tree in XML,
-* the plugins of the Behavior Tree leaf nodes in SCXML,
-* the property to check in temporal logic, currently given in JANI, later support for XML will be added.
+* the plugins of the Behavior Tree leaf nodes in (A)SCXML
 
-We offer a push-button solution for the full bundle conversion of all of those input files into one model-checkable format.
-We suggest using `smc_storm <https://github.com/convince-project/smc_storm>`_ for verifying JANI models and `SCAN <https://github.com/convince-project/SCAN>`_ to verify plain SCXML models..
+The full bundle of files is converted to an equivalent model in plain SCXML, which can be directly verified using model checkers such as `SCAN <https://github.com/convince-project/SCAN>`_.
 
 .. image:: graphics/as2fm_overview.drawio.svg
     :alt: How AS2FM works
@@ -33,9 +33,7 @@ Contents
    :maxdepth: 2
 
    installation
-   quick-guide
    tutorials
-   howto
-   scxml-jani-conversion
+   roaml-scxml-conversion
    api
    contacts
diff --git a/docs/source/installation.rst b/docs/source/installation.rst
@@ -15,14 +15,13 @@ In the root folder of the repository, pull the necessary docker image:
     $ docker compose pull
     ...
 
-Then verify that the correct versions are installed
+Then run it with:
 
 .. code-block:: bash
 
-    $ docker compose run --remove-orphans base smc_storm --version
+    $ docker compose run --remove-orphans base
     [+] Creating 1/1
     ...
-    0.1.4
 
 Local installation
 ^^^^^^^^^^^^^^^^^^
@@ -32,86 +31,24 @@ Requirements
 
 The scripts have been tested with Python 3.10 and pip version 24.0.
 
-You need to install ROS. We currently support the following distributions:
+You will need to install ROS. We currently support the following distributions:
 
 * `Humble <https://docs.ros.org/en/humble/index.html>`_
 * `Jazzy <https://docs.ros.org/en/jazzy/index.html>`_
 
-Don't forget to source ROS, e.g.:
+Once installed, be sure to source it (ie. via ``$ source /opt/ros/humble/setup.bash``)
 
-.. sybil-new-environment: IGNORE
-.. TODO: this needs actual bash instead of sh
-
-.. code-block:: bash
-
-    $ source /opt/ros/humble/setup.bash
-
-Install SMC Storm by downloading the `latest release <https://github.com/convince-project/smc_storm/releases>`_ and executing the installation script.
-Verify your installation:
-
-.. sybil-new-environment: smc_storm
-
-.. code-block:: bash
-
-    $ smc_storm --version
-    0.1.4
-
-AS2FM Python Package
-````````````````````
-
-.. warning::
-
-    Before proceeding with the installation, make sure that pip's version is at least 24.0.
-
-    - To check pip's version: `python3 -m pip --version`
-    - To upgrade pip: `python3 -m pip install --upgrade pip`
-
-.. note::
-
-    Since we switched from a multi-package to a mono-package setup, make sure to uninstall the previous version of the AS2FM tools.
-    It can be done using the following instructions:
-
-    .. sybil-new-environment: IGNORE
-
-    .. code-block:: bash
-
-        python3 -m pip uninstall moco_common
-        python3 -m pip uninstall roaml_generator
-        python3 -m pip uninstall roaml_converter
-        python3 -m pip uninstall jani_visualizer
-        python3 -m pip uninstall trace_visualizer
-
-AS2FM can be installed using pip:
+ Then run the following command to build the workspace:
 
 .. code-block:: bash
 
-    # Non-editable mode
-    python3 -m pip install AS2FM/
-    # Editable mode
-    python3 -m pip install -e AS2FM/
-
-Verify your installation by **sourcing your ROS distribution** (i.e. running `source /opt/ros/<ros-distro>/setup.bash`) and then running:
+    $ docker compose build base
+    ...
 
-.. sybil-new-environment: pip
-    :cwd: /
+And you can now run it with:
 
 .. code-block:: bash
 
-    $ as2fm_scxml_to_jani --help
-
-    usage: as2fm_scxml_to_jani [-h] [--generated-scxml-dir GENERATED_SCXML_DIR]
-                            [--jani-out-file JANI_OUT_FILE]
-                            main_xml
-
-    Convert SCXML robot system models to JANI model.
-
-    positional arguments:
-    main_xml              The path to the main XML file to interpret.
-
-    options:
-    -h, --help            show this help message and exit
-    --generated-scxml-dir GENERATED_SCXML_DIR
-                            Path to the folder containing the generated plain-
-                            SCXML files.
-    --jani-out-file JANI_OUT_FILE
-                            Path to the generated jani file.
+    $ docker compose run --remove-orphans base
+    [+] Creating 1/1
+    ...
diff --git a/docs/source/moco_logo.png b/docs/source/moco_logo.png
diff --git a/docs/source/quick-guide.rst b/docs/source/quick-guide.rst