diff --git a/docs/source/index.rst b/docs/source/index.rst index 1433bd7..7e71b29 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -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 `_. -The toolbox, which can be found `here `_, 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 `_, into `plain JANI `_ 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 `_, into `plain JANI `_ 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 ---------- @@ -114,7 +114,7 @@ smc-storm --------- `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 `_. The tool and its documentation can be found in this `repository `_. +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 `_. The tool and its documentation can be found in this `repository `_. .. toctree:: diff --git a/docs/source/overview.plantuml b/docs/source/overview.plantuml index 8455678..722db2a 100644 --- a/docs/source/overview.plantuml +++ b/docs/source/overview.plantuml @@ -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 ] @@ -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