Implement BDDbased 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 underapproximations, 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 underapproximation, 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 overapproximation.
 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 guardx = 5
will lead to a dependency, while there is none. Also, for updatedo x := x + 1
and guardx = 0
(assumingx
has lowerbound0
) a relation is assumed, while there is none. Not considering variable values leads to a significant overapproximation, 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 overapproximation:
 For each edge
e
, computeR(e)
, by applying the edge forward to thetrue
predicate.  For each combination of edges
e1
ande2
, computeP = R(e1) and guard(e2)
. IfP = false
then there is no forward dependency frome1
toe2
. Otherwise, there is a potential dependency and we adde2
to the forward dependency set ofe1
.  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 fromtrue
by taking this edge. Some examples: For an update
do x := 5
we know that inR(e)
for surex = 5
.  For a
goto loc1
we know that inR(e)
for sureLP = loc1
.  For an update
do x := x + 1
for a variable with lowerbound0
we know that inR(e)
for surex != 0
.  For a guard
x > 3
and updatedo x := x + 1
we know that inR(e)
for surex > 4
.
 For an update
 The ideas of
P
is that if the states reached bye1
don't enable the guard ofe2
, thene2
for sure can't follow one1
. In all other cases, it depends on the state beforee1
is applied, which we don't know statically, so we assume a dependency, to ensure an overapproximation 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 beingfalse
.  We may still overapproximate, but hopefully not as much.
 Performancewise, the complexity of the combinations of
e1
ande2
is O(n^2), which is not ideal. However, since we apply edges totrue
, hopefully this will not lead to large BDDs, and can thus be computed rather quickly.