bogus co-Büchi generation by nsa_to_nca
Consider the following dnf.hoa automaton with DNF acceptance:
It recognizes the persistence formula (FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)
:
% ltl2tgba -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)' > ref.hoa
% autfilt -c --equivalent-to ref.hoa dnf.hoa
1
% ltlfilt --format='%[v]h' -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)'
persistence
and it does not accept the following word:
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' dnf.hoa ref.hoa
0
(All runs for this word, starting with 0->1->3... or 0->2->6... ultimately cycle between states 6 and 8.)
Now let's build a (supposedly) equivalent NCA automaton:
python3 -c 'import spot; print(spot.dnf_to_nca(spot.automaton("dnf.hoa")).to_str())' > nca.hoa
That automaton is too big to be displayed, but it does accept the above word, which isn't expected.
% autfilt --stats=%s nca.hoa
69
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' nca.hoa
1
% autfilt -c --equivalent-to ref.hoa nca.hoa
0
The DCA version is bogus as well (but that isn't surprising given that dnf_to_dca()
calls dnf_to_nca()
first), but it has the advantage of being simplifiable to some automaton small enough to be displayed. This allows us to double-check that the given word is really accepted; i.e., this is probably not a bug of remove_fin()
(used by --accept-word
and --equivalent-to
).
% python3 -c 'import spot; print(spot.dnf_to_dca(spot.automaton("dnf.hoa")).to_str())' | autfilt --small > dca.hoa
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' dca.hoa
1
The accepting run is 0->1->6->13->4->7->4->7->4->...
.
I have also tested that the output of dnf_to_streett
is equivalent to the reference, so the problem comes after that.
% python3 -c 'import spot; print(spot.dnf_to_streett(spot.automaton("dnf.hoa")).to_str())' > streett.hoa
% autfilt -c --equivalent-to streett.hoa ref.hoa
1