-.. _cfg=model-check/property:
-
-Specifying a liveness property
-..............................
-
-**Option** ``model-check/property`` **Default:** unset
-
-If you want to specify liveness properties, you have to pass them on
-the command line, specifying the name of the file containing the
-property, as formatted by the `ltl2ba <https://github.com/utwente-fmt/ltl2ba>`_ program.
-Note that ltl2ba is not part of SimGrid and must be installed separately.
-
-.. code-block:: console
-
- $ simgrid-mc ./my_program --cfg=model-check/property:<filename>
-
-.. _cfg=model-check/checkpoint:
-
-Going for Stateful Verification
-...............................
-
-By default, the system is backtracked to its initial state to explore
-another path, instead of backtracking to the exact step before the fork
-that we want to explore (this is called stateless verification). This
-is done this way because saving intermediate states can rapidly
-exhaust the available memory. If you want, you can change the value of
-the ``model-check/checkpoint`` item. For example,
-``--cfg=model-check/checkpoint:1`` asks to take a checkpoint every
-step. Beware, this will certainly explode your memory. Larger values
-are probably better, make sure to experiment a bit to find the right
-setting for your specific system.
-