Re: [Spot] Walking through BDD formula in python

Ayrat Khalimov <ayrat.khalimov@gmail.com> writes:

O, found the answer. According to the implementation of the function spot::bdd_to_formula, any formula of transition.cond is of the form of "sum of products", so a straightforward traversing of the formula bdd_to_formula(transition.cond) is sufficient.

Exactly. If the top-level if the result is not an Or operator, then the output is a single cube, otherwise is a disjunction of cubes. If you need the result as a BDD, it's faster to use minato_isop directly (bdd_to_formula uses this but additionally has to convert the BDD to a formula).