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

diff --git a/examples/s4u/README.rst b/examples/s4u/README.rst
index 1fab295d2f..e332ab6783 100644
--- a/examples/s4u/README.rst
+++ b/examples/s4u/README.rst
@@ -31,6 +31,7 @@ to simulate.
 Actors: the Active Entities
 ===========================
 
+.. _s4u_ex_actors:
 
 Starting and Stoping Actors
 ---------------------------
@@ -307,7 +308,7 @@ Interacting with the Platform
    resources must be turned off and on again, and how to react to such
    failures in your code.
    
-   |br| `examples/platforms/small_platform_with_failure.xml <https://framagit.org/simgrid/simgrid/tree/master/examples/platforms/small_platform_with_failure.xml>`_
+   |br| `examples/platforms/small_platform_failures.xml <https://framagit.org/simgrid/simgrid/tree/master/examples/platforms/small_platform_failures.xml>`_
    |br| The state profiles in `examples/platforms/profiles <https://framagit.org/simgrid/simgrid/tree/master/examples/platforms/profiles>`_
 
  - **Specifying speed profiles:** shows how to specify an external
@@ -406,7 +407,34 @@ Distributed Hash Tables (DHT)
     One of the most famous DHT protocol.
     |br| `examples/s4u/dht-chord/s4u-dht-chord.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/dht-chord/s4u-dht-chord.cpp>`_
 
-.. TODO:: document here the examples about plugins
+.. _s4u_ex_clouds:
+
+Simulating Clouds
+-----------------
+
+  - **Cloud basics**
+    This example starts some computations both on PMs and VMs, and
+    migrates some VMs around.
+    |br| `examples/s4u/cloud-simple/s4u-cloud-simple.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/cloud-simple/s4u-cloud-simple.cpp>`_
+
+.. TODO:: document here the examples about clouds and 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