By default, no state is snapshotted and cycles cannot be detected.
+\subsection options_modelchecking_termination, model-check/termination, Non termination detection
+
+The \b model-check/termination configuration item can be used to report if a
+non-termination execution path has been found. This is a path with a cycle
+which means that the program might never terminate.
+
+This only works in safety mode.
+
+This options is disabled by default.
+
+\subsection options_modelchecking_dot_output model-check/dot_output, Dot output
+
+If set, the \b model-check/dot_output configuration item is the name of a file
+in which to write a dot file of the path leading the found property (safety or
+liveness violation) as well as the cycle for liveness properties. This dot file
+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
The \b model-checker/max_depth can set the maximum depth of the exploration
implementation was found to be buggy and this options is not as useful as
it could be. For this reason, it is currently disabled by default.
-\subsection options_recordreplay Record/replay (experimental)
+\subsection options_modelchecking_recordreplay Record/replay (experimental)
As the model-checker keeps jumping at different places in the execution graph,
it is difficult to understand what happens when trying to debug an application
- \c model-check: \ref options_modelchecking
- \c model-check/checkpoint: \ref options_modelchecking_steps
- \c model-check/communications_determinism: \ref options_modelchecking_comm_determinism
-- \c model-check/communications_determinism: \ref options_modelchecking_send_determinism
+- \c model-check/send_determinism: \ref options_modelchecking_comm_determinism
- \c model-check/dot_output: \ref options_modelchecking_dot_output
- \c model-check/hash: \ref options_modelchecking_hash
- \c model-check/property: \ref options_modelchecking_liveness
