Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix subtle bug in Execution regeneration in DFSExplorer
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 26 May 2023 08:07:57 +0000 (10:07 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 26 May 2023 08:16:21 +0000 (10:16 +0200)
commit0cc6b0eafa7e1eef267891d41c5d826eaad71d5f
tree0fe3830046c36873c52a1915cc81f70f5c782caf
parent16e87acf00914bbe8a17f80a352dda60a02894ad
Fix subtle bug in Execution regeneration in DFSExplorer

Prior to this commit, during state regeneration,
we had used the state's `get_transition_out()`
method to refill the `Execution` instance bound
to DFSExplorer (`execution_seq_`). The trouble
is that this is an **unstable** source of truth:
it should not be trusted to regenerate an execution.
Instead, the `get_transition_in()` method should
be used on the state which follows. Intuitively,
both methods should be equivalent, which is why
the bug was overlooked for so long. Now that the
execution is correct and that SDPOR/ODPOR are
based on the correct sources of truth, things
are moving along more nicely and the two algorithms
appear to behave more sanely.

In addition to the above bug fix, this commit adds
a return value to the `insert()` function of the
`WakeupTree` class. This extra information is used
in debug logs to get a better idea of what ODPOR
is doing during its insertion. Similar debug information
will be added to SDPOR in subsequent phases.
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/Execution.hpp
src/mc/explo/odpor/WakeupTree.cpp
src/mc/explo/odpor/WakeupTree.hpp