McNet : Saturation-like `forward` and `backward`

[ssoelvsten]

Currently, we use a simple(ish) forward and backward algorithm.

• Prior to BDD Construction: The list of transitions can be sorted based on the model; for example, one can try to derive the 'distance' of the edge from the initial state. Here, one can use the pre and post support of each transition.
• During forward/backward: By use of the (symbolic) support (or something even smarter), we know whether the transition touches anything that has changed since last time. Yet, at this point in time, we've already lost the 'pre' and 'post' information.