Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add workaround for subtlety with state regeneration
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 4 May 2023 12:29:44 +0000 (14:29 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 12 May 2023 13:58:22 +0000 (15:58 +0200)
commit8f063c752da6a7adf2f8c36f94269bc63807dd18
tree6bf1ce65cf95000b48684cf4c2b05619fb19dd5b
parent7375674952af9a3836b0d7692a1a0894f758baab
Add workaround for subtlety with state regeneration

Regeneration of the Execution inside DFSExplorer
should be as simple as choosing the prefix relative
to the appropriate backtracking point. However,
it did not appear to function so simple. After
a good amount of debugging, it appears that
the stack contents can change unexpectedly so
(e.g. a transition "in the middle" of the stack
seemingly switches arbitrarily). Until we can
pinpoint the true cause here, we simple resort
to rebuilding the execution based off the new
stack each time we decide to backtrack. The
downside is that all clock vectors have to be
recomputed after each backtrack. For now,
this is something that's OK to live with,
especially considering that this certainly
won't be a bottle neck in performance
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/Execution.hpp
src/mc/explo/odpor/Execution_test.cpp