+.. _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>`_
