Skip to content

#602 Implemented BDD-based workset edge dependency set computation

  • See #602 (closed) for a description of the algorithm, and the reason for doing it this way.
  • Best to review per commit.
  • For now, the merge request is draft, until !587 (merged) is merged.
  • This algorithm to compute the dependencies is indeed much simpler than the one based on Fei et al. (2014), see !595 (closed).
  • I tested the algorithm in 3 ways:
    • I added unit tests (see one of the commits).
    • I ran all the integration tests, forcing it to use the workset algorithm.
    • I compared the number of states with/without workset algorithm (and with/without forward reachability) for all benchmark models.
  • I updated, and improved the edge order documentation.
  • I added debug output for the workset dependencies, which can help to understand the performance of the workset algorithm.

Closes #602 (closed)

Merge request reports