A last solution is to pass your configuration directly using the C
interface. If you happen to use the MSG interface, this is very easy
-with the MSG_config() function. If you do not use MSG, that's a bit
+with the simgrid::s4u::Engine::setConfig() or MSG_config() functions. If you do not use MSG, that's a bit
more complex, as you have to mess with the internal configuration set
directly as follows. Check the \ref XBT_config "relevant page" for
details on all the functions you can use in this context, \c
- \c contexts/factory: \ref options_virt_factory
- \c contexts/guard-size: \ref options_virt_guard_size
- \c contexts/nthreads: \ref options_virt_parallel
-- \c contexts/parallel_threshold: \ref options_virt_parallel
+- \c contexts/parallel-threshold: \ref options_virt_parallel
- \c contexts/stack-size: \ref options_virt_stacksize
- \c contexts/synchro: \ref options_virt_parallel
\subsection options_modelchecking_visited model-check/visited, Cycle detection
In order to detect cycles, the model-checker needs to check if a new explored
-state is in fact the same state than a previous one. In order to do this,
+state is in fact the same state than a previous one. For that,
the model-checker can take a snapshot of each visited state: this snapshot is
then used to compare it with subsequent states in the exploration graph.
-The \b model-check/visited is the maximum number of states which are stored in
-memory. If the maximum number of snapshotted state is reached some states will
-be removed from the memory and some cycles might be missed.
+The \b model-check/visited option is the maximum number of states which are stored in
+memory. If the maximum number of snapshotted state is reached, some states will
+be removed from the memory and some cycles might be missed. Small
+values can lead to incorrect verifications, but large value can
+exhaust your memory, so choose carefully.
By default, no state is snapshotted and cycles cannot be detected.
can then fed to the graphviz dot tool to generate an corresponding graphical
representation.
-\subsection options_modelchecking_max_depth model-check/max_depth, Depth limit
+\subsection options_modelchecking_max_depth model-check/max-depth, Depth limit
The \b model-checker/max-depth can set the maximum depth of the exploration
graph of the model-checker. If this limit is reached, a logging message is
