Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix two minor bugs in the ODPOR implementation
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 25 May 2023 08:25:07 +0000 (10:25 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 25 May 2023 08:39:21 +0000 (10:39 +0200)
commit9513f2fee2b19db92ef287098fa7707d30cdce84
tree2a8cea3a35a76ddfe1c7e04fb8aa5ed2d57c6328
parente2760543e66cfe14a7f11bd0b398d17b100f6ec9
Fix two minor bugs in the ODPOR implementation

This commit fixes the following two bugs:

1. When seeding a wakeup tree for the first
time, we forgot to add a `break` statement
to ensure that only one such enabled thread
were placed into the wakeup tree. Before
all such enabled threads were inserted which
amounted to what would have been a brute-force
search :(.

2. When determining whether a sequence is a
candidate for insertion into a wakeup tree,
we may need to check, for all enabled actors
in a given state, whether those actors'
next steps are independent with the sequence
theretofore constructed. This additional
step peforms the work needed to check whether
those actors are contained in the set of
*weak* initials. The method corresponds
to line 6 of the pseudocode of the ODPOR algorithm
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp