+\subsection options_recordreplay Record/replay
+
+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
+under the model-checker. Event the output of the program is difficult to
+interpret. Moreover, the model-checker does not behave nicely with advanced
+debugging tools such as valgrind. For those reason, to identify a trajectory
+in the execution graph with the model-checker and replay this trajcetory and
+without the model-checker black-magic but with more standard tools
+(such as a debugger, valgrind, etc.). For this reason, Simgrid implements an
+experimental record/replay functionnality in order to record a trajectory with
+the model-checker and replay it without the model-checker.
+
+When the model-checker finds an interesting path in the application execution
+graph (where a safety or liveness property is violated), it can generate an
+identifier for this path. In order to enable this behavious the
+\b model-check/record must be set to \b yes. By default, this behaviour is not
+enabled.
+
+This is an example of output:
+
+<pre>
+[ 0.000000] (0:@) Check a safety property
+[ 0.000000] (0:@) **************************
+[ 0.000000] (0:@) *** PROPERTY NOT VALID ***
+[ 0.000000] (0:@) **************************
+[ 0.000000] (0:@) Counter-example execution trace:
+[ 0.000000] (0:@) Path = 1/3;1/4
+[ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(3)
+[ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(4)
+[ 0.000000] (0:@) Expanded states = 27
+[ 0.000000] (0:@) Visited states = 68
+[ 0.000000] (0:@) Executed transitions = 46
+</pre>
+
+This path can then be replayed outside of the model-checker (and even in
+non-MC build of simgrid) by setting the \b model-check/replay item to the given
+path. The other options should be the same (but the model-checker should
+be disabled).
+
+The format and meaning of the path may change between different releases so
+the same release of Simgrid should be used for the record phase and the replay
+phase.
+