Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix conflict detection between configs + history
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Wed, 5 Apr 2023 08:04:18 +0000 (10:04 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Wed, 5 Apr 2023 08:39:59 +0000 (10:39 +0200)
commit3529af6d632ac8a5f36352711acae57b10208c2c
tree5063a953f4e8cc54957ddd34e17f7cae1b6f687d
parent858298e81941473ad0ea981a85fa57a65da3491f
Fix conflict detection between configs + history

The computation of K-partial alternatives requires
that we can determine whether or not `[e] + C`
for some event `e` is a valid configuration. There
was a subtlety in the code prior to the this commit
that caused UDPOR to incorrectly compute whether
or not `[e] + C` was a valid configuration. Specifically,
it was not sufficient to look at the difference between
the event's history and the events in the configuration
and checking *dependency*. You have to check *conflicts*:
it's possible that two events are dependent in a configuration
but are related to each other causally (and thus would
not be in conflict with one another)
src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/Configuration.hpp
src/mc/explo/udpor/History.hpp
src/mc/explo/udpor/UnfoldingEvent.cpp
src/mc/explo/udpor/UnfoldingEvent.hpp
src/mc/explo/udpor/maximal_subsets_iterator.cpp