autfilt -B --product should not run out of acceptance sets
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.