======================================
SimGrid can not only predict the performance of your application, but also assess its correctness through formal methods. Mc SimGrid is
-a full-featured model-checker that is embedded in the SimGrid framework. It can be used to formally verify safety and liveness
+a full-featured model-checker that is embedded in the SimGrid framework. It can be used to formally verify safety
properties on codes running on top of SimGrid, be it :ref:`simple algorithms <usecase_simalgo>` or :ref:`full MPI applications
<usecase_smpi>`.
multithreaded programs. It can however be used to detect misuses of the synchronization functions, such as the ones resulting in
deadlocks.
-Mc SimGrid can be used to verify classical `safety and liveness properties <https://en.wikipedia.org/wiki/Linear_time_property>`_, but
+Mc SimGrid can be used to verify classical `safety properties <https://en.wikipedia.org/wiki/Linear_time_property>`_, but
also `communication determinism <https://hal.inria.fr/hal-01953167/document>`_, a property that allows more efficient solutions toward
fault-tolerance. It can alleviate the state space explosion problem through `Dynamic Partial Ordering Reduction (DPOR)
<https://en.wikipedia.org/wiki/Partial_order_reduction>`_ and `state equality <https://hal.inria.fr/hal-01900120/document>`_. Note that
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
------------------
-------------
This tutorial is not complete yet, as there is nothing on reduction
-techniques nor on liveness properties. For now, the best source of
+techniques. For now, the best source of
information on these topics is `this old tutorial
<https://simgrid.org/tutorials/simgrid-mc-101.pdf>`_ and `that old
presentation
-<http://people.irisa.fr/Martin.Quinson/blog/2018/0123/McSimGrid-Boston.pdf>`_.
+<http://people.irisa.fr/Martin.Quinson/blog/2018/0123/McSimGrid-Boston.pdf>`_. But be warned that these source of
+information are very old: the liveness verification was removed in v3.35, even if these docs still mention it.
.. |br| raw:: html
