From cc5fcbced3a4e6a1dec69c5810e6765a1c80da8a Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 26 May 2015 16:33:28 +0200 Subject: [PATCH] [mc][doc] Document the model-check/visited option --- doc/doxygen/options.doc | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc index f71aa4d72f..f80bd32e03 100644 --- a/doc/doxygen/options.doc +++ b/doc/doxygen/options.doc @@ -371,7 +371,20 @@ Of course, specifying a reduction technique enables the model-checking so that you don't have to give --cfg=model-check:1 in addition. -\subsection options_modelchecking_max_depth model-checker/max_depth, Depth limit +\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, +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. + +By default, no state is snapshotted and cycles cannot be detected. + +\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 -- 2.20.1