Add a workset-based algorithm for CIF data-based synthesis reachability computations
Reachability is at the core of the data-based synthesis algorithm. Any improvements there could help greatly. @sthuijsman suggested a workset-based algorithm at #493 (comment 1068705):
Just seeing this issue. Just want to make a note that there are methods to recognize fixpoint even sooner (and avoids unnecessary evaluations of edges) by using a Workset based algorithm as used in:
In short, the idea is use the knowledge of which edges relate to the same variables. A workset list is kept that includes edges that might potentially find new states during the search. Let's say we find new states when searching over event a, and event b relates to the same variables, it might be worthwhile to search over b. However, if we previously searched over c and didn't find any states, even after finding new states by a, if a and c do not relate to the same variables, we know it is not necessary to look over c again.
Not sure if it is really worth the work, so I did not make an issue for it. But maybe it is interesting to investigate in the future.
Steps to add it, as defined in the Fei et al 2014 paper, that refers to Fei et al 2013 for some of the details (see also #520 (comment 1114569)):
-
Add per-event edge granularity. (#586 (closed)) -
Add workset algorithm. (!587 (merged)) -
Add edge dependency sets/relation from Fei et al (2014). (!595 (closed)) -
Add edge dependency sets/relation based on BDD compuations. (#602 (closed), !599 (merged)) -
Add heuristics for edge selection from Fei et al (2013). (#605 (closed), !636 (merged))
In !587 (merged), in commit 3228efc3, we also improved synthesis performance a bit by only performing pre/post apply of edges that we perform reachability on, rather than all edges.