Skip to content

#1200 #1201 CIF/BDD and CIF data-based synthesis: allow keeping certain BDDs rather than freeing them.

Dennis Hendriks requested to merge 1200-cif-datasynth-free-settings into develop
  • Best to review per commit.
  • No end-user visible changes.
  • Notes:
    • This solves the issues mentioned in #1200 (closed) and #1201 (closed). That is, the changes allow certain parts of the CIF/BDD specification and data-based synthesis result to be kept rather than freed, so that they remain available after synthesis. This is useful when embedding the synthesis algorithm into a larger computation, where these BDDs are still needed after synthesis. For instance, the controlled behavior can be kept, so that it doesn't need to be recomputed with expensive reachability computations, and edges can still be applied.
    • I opted to add only some BDDs that can be kept, rather than being complete, as being complete would mean adding dozens more of these. Since it doesn't exactly make the code nicer, I opted to keep it conservative to what we need right now, and what is reasonable to expect in the near future. It can always be extended.
    • I opted to have 'keep' enum constants, as I felt it best to explicitly request exceptions, from a user's perspective. This does lead to some double negations in some places where the enum constants are used though (but not in all places).
  • Other changes:
    • I've adopted BddUtils.free in a few places where a BDD was freed and set to null. I did this in places where I was making changes anyway, and in similar places within the same methods as where I made changes.
    • EnumSet -> Set in cif.bdd and cif.datasynth plugins where relevant.

Closes #1200 (closed), #1201 (closed)

Edited by Dennis Hendriks

Merge request reports

Loading