search

tulip-control / dd

Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
https://pypi.org/project/dd
Other
178 stars 39 forks source link

Returning BDDs from function #43

Closed MichalKnapik closed 4 years ago

MichalKnapik commented 5 years ago

Hi, I'd like to use dd in an experimental model checker, but I keep having an issue with memory management in Python. Namely, such method of 'bigClass':

def next(self):
    setBDDencoding = self.manager.true
    #... compute stuff
    return setBDDencoding

used like this:

niceBDD = oldBDD | bigClass.next()

throws:

Exception ignored in: <bound method BDD.__del__ of <dd.bdd.BDD object at 0x7f14e009d7f0>>
Traceback (most recent call last):
  File "/home/me/.local/lib/python3.6/site-packages/dd/bdd.py", line 183, in __del__
AssertionError: {1: 7, 10: 2, 16: 1, 17: 1, 24: 1, 25: 1, 28: 1, 29: 1}

I'd appreciate some suggestions how to deal with it.

A note: the error is not reproduced under dd.cudd.

johnyf commented 4 years ago

This issue seems to relate to nodes with nonzero reference counts when the manager is garbage collected by Python. The AssertionError is raised by the assert statement below.

https://github.com/tulip-control/dd/blob/a77dc26d7d08d45504bcb59c39eb6107e11bec26/dd/bdd.py#L179-L183

johnyf commented 4 years ago

This AssertionError seems (above) to be caused by using the class dd.bdd.BDD as a BDD manager within a class instance, and returning a BDD reference (an integer in this case) from a method of the class. If the class instance is not used further in the code, it is garbage collected, and so is the BDD manager. There are nodes with nonzero reference counts (calling dd.bdd.BDD.incref can achieve this result), and those cause the AssertionError.

This could be avoided by defining the BDD manager instance outside the class, and passing the BDD manager instance as an argument to the class upon instantiation (for example to __init__, to set the attribute self.manager).

Without this approach, returning a BDD reference from a method and applying an operation (|) with another integer would yield a result that is not in the context of any BDD manager.

This situation is avoided by using dd.autoref or dd.cudd. In those cases it is checked that operators are applied between BDD references from the same BDD manager. Another AssertionError would be raised then. This check is made possible by using dd.autoref.Function or dd.cudd.Function instances to represent BDD references.

https://github.com/tulip-control/dd/blob/15804acb6c17c2c5c2d005306e5b7277ae51ea2c/dd/autoref.py#L337

Moreover, reference counting is in that case automated within the Function instances, and the manager cannot be garbage collected before all references to it have been garbage collected. So an AssertionError as that in the OP could not occur when using dd.autoref.BDD or dd.cudd.BDD.

https://github.com/tulip-control/dd/blob/15804acb6c17c2c5c2d005306e5b7277ae51ea2c/dd/autoref.py#L275 https://github.com/tulip-control/dd/blob/15804acb6c17c2c5c2d005306e5b7277ae51ea2c/dd/autoref.py#L296