Draft: #520 Add algorithm by Fei et al. (2014) to compute edge dependency sets
- This merge quest is based on a somewhat outdated version of !587 (merged), and includes the changes of that older version of !587 (merged) as well. The relevant commits are f6612fc3 and later. If we want to keep this merge request and merge it, I'll recreate it based on the latest version, and then I'll also clean up the history. However, I propose not to ever merge it, see below.
- Getting a working solution:
- I tried to implement the algorithm from Fei et al. (2014) that I summarized here.
- I found that it has a bug that I fixed, at the cost of significantly larger dependency sets, which will reduce the performance of the workset algorithm. But, correctness is more important than performance.
- The
FeiEdgeDependencySetCreator
now includes various additions compared to the orginal algorithm of Fei et al. (2014), to fix the bug, but also to account for various features of the CIF language that we support in data-based synthesis, but that were not in the EFAs as defined by Fei et al. - This modified algorithm works for our entire regression test set, where I temporarily enabled the workset algorithm for all tests. Thus, I'm not aware of any issues in this implementation.
- But it has become complex:
- The
FeiEdgeDependencySetCreator
has 576 lines. - Several parts of the algorithm now have long sections with comments that explain why certain modifications of the algorithm are needed. It is not exactly simple anymore.
- The order in which various concepts are considered needs to be exactly right, or things go wrong. I made mistakes several times while working on it. I can't be sure there are more issues in it.
- Getting the dependencies right, such that they work for our regression tests required quite some trial and error. I can't be sure it works for all models, only that it works for the ones in the current regression test set.
- Fundamentally, what I don't like about the algorithm is that it tries to compute when things can follow. However, as the bug showed, this is both difficult to determine statically. It requires that sufficient dependencies are found and unioned together. But how do we now that we didn't miss some dependency that only in some rare situations is needed. Guaranteeing that we don't have an under-approximation seems practically impossible.
- The
- It seems the whole algorithm is now useless:
- The unit tests were adapted in a separate commit after the fix, to show how much the depencies increase. In fact, all unit tests now have the full/maximal dependency set.
- Similarly, for all integration tests, the dependency sets are full/maximal dependency sets.
- Thus, we could just as well use
AllEdgesEdgeDependencySetCreator
, which gives the same dependency sets, which much simpler code.
- I created a merge request for two reasons:
- I've come up with an alternative, see #602 (closed).
Addresses #520 (closed)
Edited by Dennis Hendriks