Implement BDD-based workset edge dependency set computation

In #520 (closed) the idea is to add the workset algorithm of Fei et al. (2014). One of the steps is to compute sensible edge dependency sets. Ideally, they are as small as possible, to get the best performance. But, they may not be under-approximations, as then not all states are reached that should be reached, and the workset algorithm breaks, as does synthesis.

The dependency sets as defined by Fei et al. (2014) are broken. I tried to fix that in !595 (closed). However, we end up with complex code, for which I'm not sure it is now correct, and it seems in all practical cases all edges are then dependencies.

Some things I noted while implementing the edge dependency set computation proposed by Fei et al. (2014):

• They compute follow relations by computing two separate relations, and taking their union. They have a bug that leads to under-approximation, so more things should be unioned with it. In the end, how do you know you unioned enough things into it? It seems better to compute what definitely can't follow, and then everything else can potentially follow. That way, we have a guaranteed over-approximation.
• Computing the dependencies on the original CIF specification is challenging. We have several more concepts in CIF than in plain EFAs, that we handle in the conversion to BDDs. These all need to be taken into account, in the proper way, and in the proper order, when analyzing the original CIF specification. It may be easier to compute the dependencies on the BDD level. Then we do the analysis on the BDD edges that the workset algorithm also operates on, meaning we analyze the dependencies and use the dependencies based on the same representation. This makes reasoning about the completeness of the dependencies much easier.
• Fei et al. (2014) consider for edge dependencies within automata the source and target locations. Essentially, they thus consider the values of the location pointer variables there. However, for all other variables, they only consider which variables are assigned in updates, and which variables are used in guards. There they do not consider the values of the variables. For instance, update do x := 5 and guard x = 5 will lead to a dependency, while there is none. Also, for update do x := x + 1 and guard x = 0 (assuming x has lower-bound 0) a relation is assumed, while there is none. Not considering variable values leads to a significant over-approximation, reducing the performance of the workset algorithm. Also, considering it for location pointers and not for other variables is conceptually not so clean. It would lead to people preferring DFAs over EFAs, as that would lead to better performance for the workset algorithm.

I've come up with an alternative approach that I think will be correct and has less over-approximation:

• For each edge e, compute R(e), by applying the edge forward to the true predicate.
• For each combination of edges e1 and e2, compute P = R(e1) and guard(e2). If P = false then there is no forward dependency from e1 to e2. Otherwise, there is a potential dependency and we add e2 to the forward dependency set of e1.
• The backward dependencies are the inverse of the forward dependencies.

Some notes on the steps of the proposed approach:

• R(e) indicates which states can be reached from true by taking this edge. Some examples:
  • For an update do x := 5 we know that in R(e) for sure x = 5.
  • For a goto loc1 we know that in R(e) for sure LP = loc1.
  • For an update do x := x + 1 for a variable with lower-bound 0 we know that in R(e) for sure x != 0.
  • For a guard x > 3 and update do x := x + 1 we know that in R(e) for sure x > 4.
• The ideas of P is that if the states reached by e1 don't enable the guard of e2, then e2 for sure can't follow on e1. In all other cases, it depends on the state before e1 is applied, which we don't know statically, so we assume a dependency, to ensure an over-approximation and thus correctness of the dependency sets.

Some notes on the proposed approach in general:

• This should lead to very simple code to compute the dependency sets: we already have code to apply edges, and computing a single and is easy, as is checking the result from being false.
• We may still over-approximate, but hopefully not as much.
• Performance-wise, the complexity of the combinations of e1 and e2 is O(n^2), which is not ideal. However, since we apply edges to true, hopefully this will not lead to large BDDs, and can thus be computed rather quickly.