Add ODPOR extension computation (lines 4-6)

Add ODPOR extension computation (lines 4-6)

ODPOR asks us to compute, for each reversible
race in the current maximal execution `E`,
whether some subsequence `v` of events
extending a prefix `E'` of `E` should be
inserted into a wakeup tree.

There's a few subtle details that should
be noted in this computation. ODPOR asks
us to compute `notdep(e, E)`, which means
possibly looking at events that occur
*after* `e'` and THEN adding `proc(e')`.
The subtlety lies in the fact that the
actual transition associated with `e'`
must be added AFTER all of the others.
We got lucky with SDPOR since next_E_p
was already in the last position and
thus required no special treatment. With
ODPOR, we have to be more careful.

Even more subtle is the observation that
any events in `notdep(e, E)` can neither
affect the enabledness of `e'` nor can
`e'` affect the enabledness of any of
those events, or else if they do
affect the enabledness of `e'` they
will necessarily be contained "between"
`e` and `e'`