Mc SimGrid is currently less mature than other parts of the framework, but it improves every month. Please report any question and
issue so that we can further improve it.
+Limits
+^^^^^^
+
+The main limit of Model Checking lies in the huge amount of scenarios to explore. SimGrid tries to explore only non-redundant
+scenarios thanks to classical reduction techniques (such as DPOR and stateful exploration) but the exploration may well never
+finish if you don't carefully adapt your application to this mode.
+
+A classical trap is that the Model Checker can only verify whether your application fits the properties provided, which is
+useless if you have a bug in your property. Remember also that one way for your application to never violate a given assertion
+is to not start at all, because of a stupid bug.
+
+Another limit of this mode is that it does not use the performance models of the simulation mode. Time becomes discrete: You can
+say for example that the application took 42 steps to run, but there is no way to know how much time it took or the number of
+watts that were dissipated.
+
+Finally, the model checker only explores the interleavings of computations and communications. Other factors such as thread
+execution interleaving are not considered by the SimGrid model checker.
+
+The model checker may well miss existing issues, as it computes the possible outcomes *from a given initial situation*. There is
+no way to prove the correctness of your application in full generality with this tool.
+
Getting Mc SimGrid
------------------
It is included in the SimGrid source code, but it is not compiled in by default as it induces a small performance overhead to the
-simulations. It is also not activated in the Debian package, nor in the Java or Python binary distributions. If you just plan to
+simulations. It is also not activated in the Debian package, nor in the Python binary distributions. If you just plan to
experiment with Mc SimGrid, the easiest is to get the corresponding docker image. On the long term, you probably want to install it on
your machine: it works out of the box on Linux, Windows (with WSL2) and FreeBSD. Simply request it from cmake (``cmake
-Denable_model-checking .``) and then compile SimGrid :ref:`as usual <install_src>`. Unfortunately, Mc SimGrid does not work natively
.. toggle-header::
:header: Code of ``ndet-receive-s4u.cpp``: click here to open
-
+
You can also `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-s4u.cpp>`_
.. literalinclude:: tuto_mc/ndet-receive-s4u.cpp
