Improve tutorials #21

MarcoLm993 · 2024-08-13T09:48:30Z

No description provided.

Signed-off-by: Marco Lampacrescia <[email protected]>

ct2034 · 2024-08-14T07:41:16Z

docs/source/howto.rst

+        </state>
+    </scxml>
+
+In this example, the SCXML model consists of three states, `s0`, `s1`, and `s2`, and three transitions, `e1`, `e2` and `e3`, that transition each state to the next one.


Suggested change

In this example, the SCXML model consists of three states, `s0`, `s1`, and `s2`, and three transitions, `e1`, `e2` and `e3`, that transition each state to the next one.

In this example, the SCXML model consists of three states, `s0`, `s1`, and `s2`, and three transitions, these transitions are triggered by the event `e1`, `e2` and `e3` respectively.

ct2034 · 2024-08-14T07:43:07Z

docs/source/howto.rst

+
+The events are expected to be sent by another scxml model, similarly to how it is done in the `s2` state.
+
+In order to make it more appealing to robotics developers, we have extended the default SCXML language with some ROS and BT specific features.


Suggested change

In order to make it more appealing to robotics developers, we have extended the default SCXML language with some ROS and BT specific features.

In order to fit the techstack of typical robotics developers, we have extended the default SCXML language to support ROS specific features and behavior trees.

ct2034 · 2024-08-14T07:43:39Z

docs/source/howto.rst

+
+In AS2FM, we extended the SCXML language with some additional functionalities, to support the following ROS specific features:
+
+* :ref:`ROS Timers <ros_timers>`: to schedule events at a specific rate


Suggested change

* :ref:`ROS Timers <ros_timers>`: to schedule events at a specific rate

* :ref:`ROS Timers <ros_timers>`: to trigger transitions at a specific rate

Generally, this would be fine. But since events are a concept in SCXML already, this could be misleading.

True, but transitions are an SCXML concept, too! Will rework it a little

ct2034 · 2024-08-14T07:45:00Z

docs/source/howto.rst

+* :ref:`ROS Services <ros_services>`: to call a ROS service and implement service servers
+* :ref:`ROS Actions <ros_actions>`: to call a ROS action and implement action servers (under development)
+
+All functionalities require the interface to be declared before being used, similarly to variables in the SCXML datamodel.


Suggested change

All functionalities require the interface to be declared before being used, similarly to variables in the SCXML datamodel.

All functionalities require the interface to be declared before being used, similarly to variables in the SCXML datamodel.

And similar to how ROS requires these interfaces to be declared in a node.

ct2034 · 2024-08-14T07:45:23Z

docs/source/howto.rst

+ROS Timers
+___________
+
+ROS Timers are used to schedule events at a specific rate. They can be declared as follows:


Suggested change

ROS Timers are used to schedule events at a specific rate. They can be declared as follows:

ROS Timers are used to trigger transitions at a specific rate. They can be declared as follows:

ct2034 · 2024-08-14T08:07:39Z

docs/source/graphics/scxml_tutorial_ros_example_w_bt.drawio.svg

Both are called Drainer ..

ct2034 · 2024-08-14T08:08:41Z

docs/source/tutorials.rst

+* a **battery_drainer**, that at each time step drains the battery by 1%, and each time the charge trigger is received, it recharges the battery to 100%.
+* a **battery_manager**, that at each time the battery level is received checks if it is below 30% and, if so, triggers the alarm.

+The **behavior tree** continuously checks the alarm topic and, once it is triggered, sends a charge trigger to the battery_drainer.


Suggested change

* a **battery_drainer**, that at each time step drains the battery by 1%, and each time the charge trigger is received, it recharges the battery to 100%.

* a **battery_manager**, that at each time the battery level is received checks if it is below 30% and, if so, triggers the alarm.

The **behavior tree** continuously checks the alarm topic and, once it is triggered, sends a charge trigger to the battery_drainer.

* a **Battery Drainer**, that at each time step drains the battery by 1%, and each time the charge trigger is received, it recharges the battery to 100%.

* a **Battery Manager**, that at each time the battery level is received checks if it is below 30% and, if so, triggers the alarm.

The **Behavior Tree** continuously checks the alarm topic and, once it is triggered, sends a charge trigger to the battery_drainer.

ct2034 · 2024-08-14T08:10:28Z

docs/source/tutorials.rst


+The JANI property given in `battery_depleted.jani <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example/battery_depleted.jani>`_ defines the property of interest to be model checked. In this case, it calculates the minimal probability that the battery level is below or equal to zero eventually, i.e., all we verify here is that the battery is empty at some point.


Given that we also provide a bt, it would make more sense to use the version where the battery is also charged and verify that it never runs out. I think this would make a bit more sense. Otherwise, people could get hung up on the point that the bt is useless.

Right, but we do not have that property implemented yet. We only have the emtpy, belowe 20% and alarm on.
I can implement one more property for the battery to get charged after a minimum amount of time

ct2034 · 2024-08-14T08:11:55Z

docs/source/tutorials.rst

-.. code-block:: bash
-
-    scxml_to_jani path_to_main.xml
+In the `main.xml file <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example/main.xml>`_ introduced earlier, the maximum run time of the system is specified with ``max_time`` and shared across the components. To make sure that the model checked property makes sense, the allowed runtime needs to be high enough to have enough time to deplete the battery, i.e., in this example the maximal time needs to be at least 100s because the battery is depleted by 1% per second.


This is maybe an aspect that goes a little too deep for a first tutorial. I mean we probably need a how-to for properties at some point anyway. Maybe we can mention this there? But just an idea. We can also keep it here for now.

Maybe we can keep it as is, and point to some other reference in the how to for further info?

ct2034 · 2024-08-14T08:15:19Z

docs/source/tutorials.rst

+
+.. _jani_conversion:
+
+How to convert from CONVINCE robotic JANI to plain JANI?


yeah .. maybe we can add a note that this is not really needed right now and completely independent of the ROS stuff

Signed-off-by: Marco Lampacrescia <[email protected]>

Signed-off-by: Marco Lampacrescia <[email protected]> Signed-off-by: Christian Henkel <[email protected]>

MarcoLm993 added 2 commits August 13, 2024 10:56

Split installation instructions from tutorials

91865ca

Signed-off-by: Marco Lampacrescia <[email protected]>

Refine scxml tutorial

9da3f85

Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993 requested a review from ct2034 August 13, 2024 09:48

MarcoLm993 added 5 commits August 13, 2024 11:57

Prepare the howto page for more content

129f132

Signed-off-by: Marco Lampacrescia <[email protected]>

Continue howto section and add diagram of example in tutorial

2ac45f4

Signed-off-by: Marco Lampacrescia <[email protected]>

Continuation of how-to for ros scxml

4cf8852

Signed-off-by: Marco Lampacrescia <[email protected]>

Topics docu

06262eb

Signed-off-by: Marco Lampacrescia <[email protected]>

Add services examples in the howto

31aa693

Signed-off-by: Marco Lampacrescia <[email protected]>

ct2034 requested changes Aug 14, 2024

View reviewed changes

Addressing review comments, and beyond!

008840c

Signed-off-by: Marco Lampacrescia <[email protected]>

ct2034 approved these changes Aug 14, 2024

View reviewed changes

Fix link

e17eb05

Signed-off-by: Marco Lampacrescia <[email protected]>

ct2034 merged commit bec6b2e into main Aug 14, 2024
8 checks passed

ct2034 deleted the improve-tutorials branch August 14, 2024 12:56

ct2034 pushed a commit that referenced this pull request Sep 25, 2024

Improve tutorials (#21)

9085a75

Signed-off-by: Marco Lampacrescia <[email protected]> Signed-off-by: Christian Henkel <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve tutorials #21

Improve tutorials #21

MarcoLm993 commented Aug 13, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

MarcoLm993 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

ct2034 Aug 14, 2024

MarcoLm993 Aug 14, 2024

ct2034 Aug 14, 2024

MarcoLm993 Aug 14, 2024

ct2034 Aug 14, 2024

	In this example, the SCXML model consists of three states, `s0`, `s1`, and `s2`, and three transitions, `e1`, `e2` and `e3`, that transition each state to the next one.
	In this example, the SCXML model consists of three states, `s0`, `s1`, and `s2`, and three transitions, these transitions are triggered by the event `e1`, `e2` and `e3` respectively.


		The events are expected to be sent by another scxml model, similarly to how it is done in the `s2` state.

		In order to make it more appealing to robotics developers, we have extended the default SCXML language with some ROS and BT specific features.

	In order to make it more appealing to robotics developers, we have extended the default SCXML language with some ROS and BT specific features.
	In order to fit the techstack of typical robotics developers, we have extended the default SCXML language to support ROS specific features and behavior trees.


		In AS2FM, we extended the SCXML language with some additional functionalities, to support the following ROS specific features:

		* :ref:`ROS Timers <ros_timers>`: to schedule events at a specific rate

	* :ref:`ROS Timers <ros_timers>`: to schedule events at a specific rate
	* :ref:`ROS Timers <ros_timers>`: to trigger transitions at a specific rate

	All functionalities require the interface to be declared before being used, similarly to variables in the SCXML datamodel.
	All functionalities require the interface to be declared before being used, similarly to variables in the SCXML datamodel.
	And similar to how ROS requires these interfaces to be declared in a node.

	ROS Timers are used to schedule events at a specific rate. They can be declared as follows:
	ROS Timers are used to trigger transitions at a specific rate. They can be declared as follows:


		The JANI property given in `battery_depleted.jani <https://github.com/convince-project/as2fm/tree/main/jani_generator/test/_test_data/ros_example/battery_depleted.jani>`_ defines the property of interest to be model checked. In this case, it calculates the minimal probability that the battery level is below or equal to zero eventually, i.e., all we verify here is that the battery is empty at some point.


		.. _jani_conversion:

		How to convert from CONVINCE robotic JANI to plain JANI?

Improve tutorials #21

Improve tutorials #21

Conversation

MarcoLm993 commented Aug 13, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment