Skip to content

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
Edited by Alexandre Duret-Lutz