fin-removal conversion bug (probably in streett_to_generalized_buchi)
The following code prints BUG
instead of OK
. Removing --gsa
or setting SPOT_STREETT_CONV_MIN=0
avoid the issue, so I think this is yet another bug in streett_to_generalized_buchi()
called by remove_fin()
for --equivalent-to
.
f1='XF(b & Ga)'
f2='F(((c W Xb) & F(b R !c)) | ((!c M X!b) & G(!b U c)))'
ltl2tgba "($f1)&!($f2)" > 1.hoa
ltl2tgba "$f2" -D --parity | autfilt --dualize --gsa > nf2.hoa
ltl2tgba "$f1" > nf1.hoa
autfilt --product nf1.hoa nf2.hoa > 2.hoa
if autfilt -q --equivalent-to 1.hoa 2.hoa; then
echo OK
else
echo BUG
fi