Skip to content

Commit

Permalink
Merge pull request #8 from convince-project/fix-links
Browse files Browse the repository at this point in the history
fix links
  • Loading branch information
MKlauck authored May 16, 2024
2 parents 75ef549 + 50c003d commit 2cfb85a
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 6 deletions.
6 changes: 3 additions & 3 deletions docs/source/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,8 @@ mc-toolchain-jani

This is a toolbox for converting all specifications of components of a 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 resulting format used for model checking is `JANI <https://jani-spec.org>`_.

The toolbox, which can be found `here <TODO>`_, consist of a script to convert models describing the system and its environment together, given in the CONVINCE robotics JANI flavor as specified in the `data model repository <https://github.com/convince-project/data-model>`_, into `plain JANI <https://jani-spec.org>`_ accepted as input by model checkers.
The second part of the provided toolchain components centers around system specifications given in ScXML and how to convert them into a plain Jani file for model checking. This comprises property specification in temporal logic, currently given in Jani, a behavior tree in XML, plugins and nodes in ScXML, and an environment specification in ScXML.
The toolbox consist of a script to convert models describing the system and its environment together, given in the CONVINCE robotics JANI flavor as specified in the `data model repository <https://github.com/convince-project/data-model>`_, into `plain JANI <https://jani-spec.org>`_ accepted as input by model checkers.
The second part of the toolbox centers around system specifications given in (SC)XML and how to convert them into a plain JANI file for model checking. This comprises property specification in temporal logic, currently given in JANI, a behavior tree in XML, ROS nodes and their pugins in SCXML, and an environment specification in SCXML.

model2code
----------
Expand All @@ -114,7 +114,7 @@ smc-storm
---------
`convince-project/smc_storm <https:///github.com/convince-project/smc_storm>`_

This is a statistical model checking engine for DTMC models given in Jani, which has been implemented as an extension to the famous `Storm model checker <https://stormchecker.org>`_. The tool and its documentation can be found in this `repository <https://github.com/convince-project/smc_storm>`_.
This is a statistical model checking engine for DTMC models given in JANI, which has been implemented as an extension to the famous `Storm model checker <https://stormchecker.org>`_. The tool and its documentation can be found in this `repository <https://github.com/convince-project/smc_storm>`_.


.. toctree::
Expand Down
6 changes: 3 additions & 3 deletions docs/source/overview.plantuml
Original file line number Diff line number Diff line change
Expand Up @@ -60,12 +60,12 @@ agent coverageplan #PaleGreen [
WP3 / UoB
]
agent activeplan #PaleGreen [
[[https://github.com/convince-project/active-plan ACTIVE-PLAN]]
[[https://convince-project.github.io/overview/#active-plan ACTIVE-PLAN]]
....
WP3 / UoB
]
agent simulateplan #PaleGreen [
[[https://github.com/convince-project/simulate-plan SIMULATE-PLAN]]
[[https://convince-project.github.io/overview/#simulate-plan SIMULATE-PLAN]]
....
WP3 / UoB
]
Expand All @@ -88,7 +88,7 @@ WP4 / UniGe
]
' ]
agent stormscan #TECHNOLOGY [
[[https://convince-project.github.io/overview/#smc_storm SMC-STORM]]
[[https://convince-project.github.io/overview/#smc-storm SMC-STORM]]
....
WP4 / Bosch

Expand Down

0 comments on commit 2cfb85a

Please sign in to comment.