- **model-check/checkpoint:** :ref:`cfg=model-check/checkpoint`
- **model-check/communications-determinism:** :ref:`cfg=model-check/communications-determinism`
- **model-check/dot-output:** :ref:`cfg=model-check/dot-output`
-- **model-check/hash:** :ref:`cfg=model-checker/hash`
- **model-check/max-depth:** :ref:`cfg=model-check/max-depth`
- **model-check/property:** :ref:`cfg=model-check/property`
- **model-check/reduction:** :ref:`cfg=model-check/reduction`
application, the stack will silently overflow on other parts of the
memory (see :ref:`contexts/guard-size <cfg=contexts/guard-size>`).
-.. _cfg=model-checker/hash:
-
-State Hashing
-.............
-
-Usually most of the time of the model-checker is spent comparing states. This
-process is complicated and consumes a lot of bandwidth and cache.
-In order to speedup the state comparison, the experimental ``model-checker/hash``
-configuration item enables the computation of a hash summarizing as much
-information of the state as possible into a single value. This hash can be used
-to avoid most of the comparisons: the costly comparison is then only used when
-the hashes are identical.
-
-Currently most of the state is not included in the hash because the
-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.
-
.. _cfg=model-check/replay:
Replaying buggy execution paths out of the model-checker
[ 0.000000] (0:@) Executed transitions = 46
The interesting line is ``Path = 1/3;1/4``, which means that you should use
-`--cfg=model-check/replay:1/3;1/4`` to replay your application on the buggy
-execution path. The other options should be the same (but the model-checker
-should be disabled). Note that format and meaning of the path may change between
-different releases.
+``--cfg=model-check/replay:1/3;1/4`` to replay your application on the buggy
+execution path. All options (but the model-checker related ones) must
+remain the same. In particular, if you ran your application with
+``smpirun -wrapper simgrid-mc``, then do it again. Remove all
+MC-related options, keep the other ones and add
+``--cfg=model-check/replay``.
+
+Currently, if the path is of the form ``X;Y;Z``, each number denotes
+the actor's pid that is selected at each indecision point. If it's of
+the form ``X/a;Y/b``, the X and Y are the selected pids while the a
+and b are the return values of their simcalls. In the previouse
+example, ``1/3;1/4``, you can see from the full output that the actor
+1 is doing MC_RANDOM simcalls, so the 3 and 4 simply denote the values
+that these simcall return.
Configuring the User Code Virtualization
----------------------------------------
