Skip to content

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.

21.hoa

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.

Edited by Alexandre Duret-Lutz