From: Gabriel Corona Date: Tue, 26 May 2015 14:53:49 +0000 (+0200) Subject: [mc][doc] Document the model-check/terminate option X-Git-Tag: v3_12~651 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fbf9fb3a0b1846167834bf842a3cb88ebfa46d30 [mc][doc] Document the model-check/terminate option --- diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc index f80bd32e03..b3d76a9312 100644 --- a/doc/doxygen/options.doc +++ b/doc/doxygen/options.doc @@ -384,6 +384,16 @@ be removed from the memory and some cycles might be missed. 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_max_depth model-check/max_depth, Depth limit The \b model-checker/max_depth can set the maximum depth of the exploration