\section options_modelchecking Configuring the Model-Checking
-To enable the experimental SimGrid model-checking support the program should
-be executed with the command line argument
+To enable the SimGrid model-checking support the program should
+be executed using the simgrid-mc wrapper:
\verbatim
---cfg=model-check:1
+simgrid-mc ./my_program
\endverbatim
Safety properties are expressed as assertions using the function
--cfg=model-check/property:<filename>
\endverbatim
-Of course, specifying a liveness property enables the model-checking
-so that you don't have to give <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_steps Going for stateful verification
By default, the system is backtracked to its initial state to explore
--cfg=model-check/checkpoint:1
\endverbatim
-Of course, specifying this option enables the model-checking so that
-you don't have to give <tt>--cfg=model-check:1</tt> in addition.
-
\subsection options_modelchecking_reduction Specifying the kind of reduction
The main issue when using the model-checking is the state space
* dpor: Apply Dynamic Partial Ordering Reduction. Only valid if you
verify local safety properties.
-Of course, specifying a reduction technique enables the model-checking
-so that you don't have to give <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_visited model-check/visited, Cycle detection
In order to detect cycles, the model-checker needs to check if a new explored
