GitLab

Jeroen Meijer reports that if we do many products with autfilt, as in:

autfilt -B 1.hoa --product 2.hoa --product 3.hoa ... --product 40.hoa

you can run out of acceptance sets, despite the fact that we are building a Büchi automaton (-B). This is because autfilt builds a GBA for the whole product sequence before degeneralizing it.

We should probably degeneralize as we progress (or whenever we detect that a product will fail) when option -B is given. BTW, I suspect it's better to use transition-based BA as intermediate automata even if the final result will be state-based.