Closed m4lvin closed 1 year ago
The goal of this PR is to include the work by @dushiel done as part of the master thesis Zero-suppression Decision Diagrams versus Binary Decision Diagrams on Dynamic Epistemic Logic Model Checking into SMCDEL proper.
Note: the cli and web executables are not affected by this, they still only use CacBDD.
stack bench smcdel:bench:bench-muddychildren --benchmark-arguments "CUDD/3"
statesOf
allSat
The goal of this PR is to include the work by @dushiel done as part of the master thesis Zero-suppression Decision Diagrams versus Binary Decision Diagrams on Dynamic Epistemic Logic Model Checking into SMCDEL proper.
Note: the cli and web executables are not affected by this, they still only use CacBDD.
ToDo
stack bench smcdel:bench:bench-muddychildren --benchmark-arguments "CUDD/3"
failed, also with 4, but not with 15 or 20. All of them needed way too much RAM.statesOf
NotDo / later
allSat
etc for BDD flipped variants (or even for ZDDs)