Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add complicated computation of v ~_E w to Execution
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Wed, 10 May 2023 09:38:07 +0000 (11:38 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Tue, 16 May 2023 07:50:34 +0000 (09:50 +0200)
commit714db2034b160bdacbbacd76693209ec412463d8
tree96328213214b59f7ca640e5feeb1451749e7a06b
parenta9a21312483780dd659eba21102f79f207984f7c
Add complicated computation of v ~_E w to Execution

The relation `v ~_E w` is used when traversing
a WakeupTree to determine is an "equivalent"
execution is already noted in the tree. This commit
adds the first "working" implementation of
several components to this process, viz.

1. Assuming that iteration has been implemented
(which is to come in future commits), the WakeupTree
now implements the `insert_E(v, B)` operation, where
`B` refers to the tree instance itself.

2. The `Execution` class can now determine what
is needed to complete the `insert()` operation,
specifically determining first if a) two sequences
`v` and `w` are related by `v ~_E w` and b)
what the smallest sequence `w'` is such that
`w [= v.w'`. The latter computation uses the neat
observation that (w / v) is the smallest such
sequence (viz. removing anything in `w` that's in
`v` "one at a time") and computes this value as
it is in the process of determining whether the
`~_E` relation noted holds
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/Execution.hpp
src/mc/explo/odpor/WakeupTree.cpp
src/mc/explo/odpor/WakeupTree.hpp
src/mc/explo/odpor/odpor_forward.hpp