Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add predicate filtering to compatibility graph comp
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 24 Feb 2023 14:40:39 +0000 (15:40 +0100)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Mon, 27 Feb 2023 08:24:17 +0000 (09:24 +0100)
commit9819fd4f244a981bf28f677cb7bd05fbcc8f6bcc
treeb270a3284bb7c0ed7477f17919b71ff0118788ab
parentf456852dd160e1f60f58e2a3ef37a0e688993fe0
Add predicate filtering to compatibility graph comp

Computing the compatibility graph should attempt to
disqualify as many events as possible from the configuration
to minimize the size of the resulting compatibility graph.
This is _esepcially_ important because we will enumerate
all cliques of the graph and subsequently all possible
events contains within each node. This means that removing
even one or two nodes could reduce the time spent in
enumeration dramatically.

For now, the UdporChecker can only prune based on
dependency. Perhaps, though, there are more clever
ways to prune based on whether `a` is enabled e.g.
in knowing some properties about the event structure.
This will be investigated later, but is a secondary
concern to getting an implementation of the algorithm
up-and-running.
src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/CompatibilityGraph.hpp
src/mc/explo/udpor/CompatibilityGraphNode.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/Configuration.hpp