Big bang in MC: app's observers are serialized, to become transitions in checker
Instead of interacting with the observers over the network, we now
transfer over the wire (a simplified copy of) the observer to the
checker.
This was necessary because the lifetime of the Observer (or of its
components) was sometimes too short: it happened that the Actor
refered to by the Observer was not existing anymore at the end of the
simulation when the depend relation was evaluated. Or something like
that, I'm not sure.
Another argument for this change was that UDPOR reduction sometimes
need to evaluate the dependency between transitions that are not in
the same history (in the same run of the application), so we really
need to carry the transition over to let them live in the checker.
Note that we are not copying every information of the observer over,
only the ones that are relevant to the model-checker.
Finally, this change is still ongoing:
- not all observers are serialized over the wire yet
- the depends() are not implemented in the Transition yet
- the network protocol is utterly inefficient, and we probably need
to move to FlatBuffer or something like that.
- a lot of dead code remains
Sorry for the mess, it's progressing rather slowly...
16 files changed:
