minimize_wdba() seems too slow than reasonable
The following file has 5 states, 13 edges (or 85 transitions if we split those), and 21 atomic propositions. It is extracted from an intermediate construction from Pecan, in a test case that was sent to me by @pierreganty.
The job is to run minimize_wdba()
efficiently, despite the fact that we do not have the formula. Unfortunately, dualize()
, remove_alternation()
, and tgba_powerset()
, three functions that are called by minimize_wdba()
, are all slow because of the number of atomic propositions.
Running autfilt --dualize 21.hoa
takes 34 seconds, because the code has to iterate over all possible 2^21 valuations. I'm pretty sure we can do better.