26 May
2021
26 May
'21
10:14 p.m.
Ayrat Khalimov <ayrat.khalimov(a)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).