X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a33903f0993a2bd3e7a426314de93fb20b0a6172..c17e2d0a40dd44817f3c8d5da7d72f4ef8f1e3c8:/examples/s4u/README.rst

diff --git a/examples/s4u/README.rst b/examples/s4u/README.rst
index 350d07361c..5adf1d329c 100644
--- a/examples/s4u/README.rst
+++ b/examples/s4u/README.rst
@@ -80,6 +80,10 @@ Starting and Stoping Actors
 Inter-Actors Interactions
 -------------------------
 
+See also the examples on :ref:`inter-actors communications
+<s4u_ex_communication>` and the ones on :ref:`classical
+synchronization objects <s4u_ex_IPC>`.
+
   - **Suspend and Resume actors:**    
     Actors can be suspended and resumed during their executions.
     
@@ -149,6 +153,8 @@ also the tesh files in the example directories for details.
 Activities: what Actors do
 ==========================
 
+.. _s4u_ex_communication:
+
 Communications on the Network
 -----------------------------
 
@@ -216,14 +222,18 @@ Executions on the CPU
     These objects are convenient abstractions of parallel
     computational kernels that span over several machines, such as a
     PDGEM and the other ScaLAPACK routines. Note that this only works
-    with the "ptask_L07" host model (`--cfg=host/model:ptask_L07`).
+    with the "ptask_L07" host model (``--cfg=host/model:ptask_L07``).
     |br| `examples/s4u/exec-ptask/s4u-exec-ptask.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/exec-ptask/s4u-exec-ptask.cpp>`_
     
   - **Using Pstates on a host:**
-    Shows how define a set of pstatesfor a host in the XML, and how the current
-    pstate can be accessed/changed with :cpp:func:`simgrid::s4u::Host::get_pstate_speed` and :cpp:func:`simgrid::s4u::Host::set_pstate`.
-    |br| `examples/s4u/exec-dvfs/s4u-exec-dvfs.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/exec-dvfs/s4u-exec-dvfs.cpp>`_
-    |br| `examples/platforms/energy_platform.xml <https://framagit.org/simgrid/simgrid/tree/master/examples/platforms/energy_platform.xml>`_
+    `examples/platforms/energy_platform.xml <https://framagit.org/simgrid/simgrid/tree/master/examples/platforms/energy_platform.xml>`_
+    shows how define a set of pstates in the XML. The current pstate
+    of an host can then be accessed and changed from the program.
+
+    - |cpp| `examples/s4u/exec-dvfs/s4u-exec-dvfs.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/exec-dvfs/s4u-exec-dvfs.cpp>`_
+      :cpp:func:`simgrid::s4u::Host::get_pstate_speed` and :cpp:func:`simgrid::s4u::Host::set_pstate`.
+    - |py|  `examples/python/exec-dvfs/exec-dvfs.py <https://framagit.org/simgrid/simgrid/tree/master/examples/python/exec-dvfs/exec-dvfs.py>`_
+      :py:func:`Host.get_pstate_speed` and :py:func:`Host.set_pstate`.
 
 I/O on Disks and Files
 ----------------------
@@ -252,6 +262,8 @@ result in short reads and short write, as in reality.
     i.e. when the accessed disk is not mounted on the caller's host.
     |br| `examples/s4u/io-file-remote/s4u-io-file-remote.cpp  <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/io-file-remote/s4u-io-file-remote.cpp>`_
 
+.. _s4u_ex_IPC:
+
 Classical synchronization objects
 ---------------------------------
 
@@ -396,6 +408,23 @@ Distributed Hash Tables (DHT)
 
 .. TODO:: document here the examples about plugins
 
+=======================
+Model-Checking Examples
+=======================
+
+The model-checker can be used to exhaustively search for issues in the
+tested application. It must be activated at compile time, but this
+mode is rather experimental in SimGrid (as of v3.22). You should not
+enable it unless you really want to formally verify your applications:
+SimGrid is slower and maybe less robust when MC is enabled.
+
+  - **Failing assert**
+    In this example, two actors send some data to a central server,
+    which asserts that the messages are always received in the same order.
+    This is obviously wrong, and the model-checker correctly finds a
+    counter-example to that assertion.
+    |br| `examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp>`_
+
 .. |br| raw:: html
 
    <br />