Reachability is at the core of the data-based synthesis algorithm. Any improvements there could help greatly. @sthuijsman suggested a workset-based algorithm at https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/493#note_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: - https://doi.org/10.1016/j.conengprac.2006.02.013 - https://doi.org/10.1109/tcst.2014.2303134 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 https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/520#note_1114569): * [x] Add per-event edge granularity. (#586) * [x] Add workset algorithm. (!587) * [~] Add edge dependency sets/relation from Fei et al (2014). (!595) * [x] Add edge dependency sets/relation based on BDD compuations. (#602, !599) * [x] Add heuristics for edge selection from Fei et al (2013). (#605, !636) In !587, in commit 3228efc3de97b13f5971cfab3e5e85c7e865fe70, we also improved synthesis performance a bit by only performing pre/post apply of edges that we perform reachability on, rather than all edges.