Skip to content

#866 Use partial transition relations for improving data based synthesis performance

Closes #866 (closed).

Short summary of changes:

  • I got rid of the CifBddSpec#varSetOldAndNew that was introduced in #865 (closed), as we don't need it any longer. Instead, CifBddEdge now maintains a set assignedVariables of CIF/BDD variables that are being assigned to on the edge.
  • CifToBddConverter#convertUpdates now no longer adds unchanged variable predicates 'x = x+', but instead populates the set CifBddEdge#assignedVariables.
  • The calls to relnext and relprev in CifBddEdge#apply now receive the (smaller) set of variables that are relevant for computing successor/predecessor states. These sets are precomputed for efficiency reasons. In essence, the set of variables that are relevant with respect to performing relnext/relprev with some update relation, are all BDD variables that are being assigned on that edge, union the edge support of the update relation.
  • Since we now have partial transition relation, we must be careful when merging edges. There we must add unchanged variable predicates for all BDD variables that are being assigned to on one edge, but not the other.

Results of running the CIF benchmark: benchmark_results.zip. The HTML report of the CIF benchmark results contains three configurations. For config 1, the develop branch was used before #865 (closed) got merged (commit 1fbb8818). For config 2, the develop branch was used after #865 (closed) got merged (commit 002f962b). Config 3 are the changes proposed in this PR, i.e., the use of partial transition relations instead of full ones. On average, performance improved slightly, and peak memory consumption quite a bit (for some models).

One thing to remark on is that 'mri_event' now seems to perform worse. However, the benchmark report actually reports on the number of cache misses. When instead looking at the number of actual BDD operations performed (in the *.out files, which are included in the ZIP file), then this number went down from 50664436 (config 2) to 37680573 (config 3). So it seems that, for some reason, config 3 was more unfortunate when it comes to caching. (Perhaps due to cache table resizing at an unlucky moment?)

Merge request reports