Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add first round of execution independence tests
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Tue, 23 May 2023 08:18:24 +0000 (10:18 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Tue, 23 May 2023 08:18:34 +0000 (10:18 +0200)
commit26501dd7026096ebf4d7a8e4ca5d16cea63e2a87
tree5597939b53df0541d6135d83706bc77759e08791
parenteee65f15473cbf3c3892ac1a87d677d935edc6c8
Add first round of execution independence tests

This commit adds the first set of tests for
checking whether a particular transition `t` is
independent with an extension `w` of an execution
sequence `E`. This is needed to determine whether
the transition `t` satisfies condition (2) of the
procedure outlined in the ODPOR paper for testing
whether `v ~_[E] w` holds between two sequences
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/Execution.hpp
src/mc/explo/odpor/Execution_test.cpp
src/mc/explo/odpor/WakeupTree_test.cpp