Introduce ODPOR integration with multiple actions
Prior commits had missing integration with transitions
which could be executed multiple times in the form of
variants. This commit resolves those issues by making
two important modifications:
1. Determining the "current thing that actor X is
running" from a given state `s` has been modified
to reflect what we would expect if we asked the
question even after having exhausted all combinations;
the the case where all combinations have been executed,
the last variant is that which we would expect to be
considered the transition which were enabled at `s`.
This allows us to "fix" the spot in ODPOR where we
need to determine those actions enabled at a given
state `s`. We need to treat it as if only one variant
actually exists; for if there are differences in the
dependency structure for each variant, we wouldn't
want to erroneously deduce that an actor `X` were
a weak initial for some prefix `E'` of `E` and
for some extension `v` of `E'` based on what it
HAD run in the past.
2. In ODPOR, we now only insert members into the
sleep set when all variants of a transition have
been executed. This ensures that we are effectively
treating each variant in isolation from one another;
it is only when we reach the last variant that we
can finally go ahead and say "OK actor X you can
go into the sleep set now". Note that it's perfectly
possible for the actor to later end up in sleep sets
of states that occur *later on*; but for the sleep
set that is at *this* state, we'd want to be sure
only to add it after having explored the state space
with each variant. The reasoning is the same as in
point 1: we wouldn't want the sleep set to be based
on an action that the actor HAD run in the past as
the proxy representing what that actor is doing IN
THE PRESENT. If the dependencies were different among
the different variants, we'd have an issue if we
had previously added the other variants
