X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/40a6b57b33ba92df9a10600b8d6fa10fff80c9d2..1cd1baa02965994b011595fb05c8b3b575571f12:/doc/doxygen/options.doc

diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc
index 328e201d61..89af6768d3 100644
--- a/doc/doxygen/options.doc
+++ b/doc/doxygen/options.doc
@@ -316,10 +316,10 @@ in NS3. The only valid values (enforced on the SimGrid side) are
 
 \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
@@ -338,10 +338,6 @@ ltl2ba program.
 --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
@@ -359,9 +355,6 @@ setting for your specific system.
 --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
@@ -382,10 +375,6 @@ For now, this configuration variable can take 2 values:
  * 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