#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 setassignedVariables
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 setCifBddEdge#assignedVariables
. - The calls to
relnext
andrelprev
inCifBddEdge#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 performingrelnext
/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?)