search

sybila / biodivine-hctl-model-checker

Symbolic HCTL model checker for Boolean networks
MIT License
0 stars 0 forks source link

Sanitization/desanitization of BDD #5

Closed daemontus closed 1 year ago

daemontus commented 1 year ago

Right now, the BDDs resulting from the model checking process (or BDDs entering the model checking methods) need to admit the symbolic variables that encode additional HCTL state variables. However, this means the BDDs are incompatible with BDDs produced by a "standard" SymbolicAsyncGraph. This means the HCTL model checker generally cannot "share" results with other tools in the biodivine tool-chain (either importing or exporting).

However, it is possible to "sanitize" these BDDs as demonstrated here such that they are compatible with the default SymbolicAsyncGraph representation.

It would thus be good to include this functionality in the model checker library as well.

ondrej33 commented 1 year ago

This should be resolved through #6 and #7. The standard model-checking procedure now automatically applies this "sanitization" to the resulting BDDs. Versions of the model-checking functions without sanitizing are also provided, as they are useful for some contexts.