this automaton is reportedly not equivalent to itself...
This is a non-deterministic 20-state parity 17 automaton that @frenkin generated using randaut. Inclusion checks require more that 32 acceptance sets, so Spot needs to be compiled accordingly.
% ./configure --enable-max-accsets=64
[...]
% make -j16
[...]
% bin/autfilt --equivalent-to bug.hoa bug.hoa -c
0
% bin/autfilt --included-in bug.hoa bug.hoa -c
0
% bin/autfilt -D bug.hoa > bugdet.hoa
% bin/autfilt --included-in bugdet.hoa bug.hoa -c
0
% bin/autfilt --included-in bug.hoa bugdet.hoa -c
1
% bin/autfilt --complement bugdet.hoa > bugdetneg.hoa
% bin/autfilt --product bugdetneg.hoa bug.hoa > prod.hoa
% bin/autfilt --is-empty prod.hoa -c
0
% word=`bin/autfilt --stats='%w' prod.hoa`
% bin/autfilt --accept-word="$word" bug.hoa -c
1
% bin/autfilt --accept-word="$word" bugdet.hoa -c
0
% bin/autfilt --accept-word="$word" bugdetneg.hoa -c
1
All the 0
s above are unexpected, and so is the last 1
. What went wrong? Is it the determinization? Is it the emptiness check?