Hello,
first I just want to say, thanks for creating Spot, it is immensely useful! And I think that I might have found a bug (or two).
My inputs are classic state-based NBAs. I rely on Spot to compare and verify my determinized automata, i.e. I compare the automaton that my tool produces with the one I get from Spot using autfilt -D -S -p (to get a deterministic parity automaton). I use autfilt --equivalent-to=... for the equivalence test.
Yesterday I noticed something strange. When I compare the original NBA and my DPA, it reports that they are equivalent. Same for the original NBA and the DPA I get from Spot. But when I compare my automaton with the one from Spot, it says that the languages are different! So the first thought was - something must be broken in the equivalence test.
Apparently, at least one of the three answers I got is wrong. So I used a little Python script using the Spot API to get a word where two of the automata do not agree on. Let's call the original NBA A, my DPA B and the one from Spot C.
There were no words found in A׬B, ¬A×B, A׬C, ¬A×C and also B׬C.
But there IS a word in ¬B×C.
I used this word with autfilt --accept-word=... to check A, B and C. And it turned out that in fact A and B do not accept the word, but C does, i.e. C is incorrect.
So, to conclude, there seems to be a bug in the determinization and the problem is not detected by the equivalence test between A and C.
I don't know about Spot internals, but if the equivalence test is using the same determinization procedure to complement A for the required products, then the bug in the equivalence test is a consequence of the problem in the determinization (i.e., the equiv. test compares the wrong DPA with basically itself), so the issues might be related.
It might be useful to know that I found the problem using Spot 2.4.4 and it is still present in the current version 2.5.1. I also attach the smallest automata A, B and C that illustrate the issue and the script I used to search for the counterexample.
You can check that:
cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0
and
autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 1.
I hope this helps.
Thanks and best regards,
Anton Pirogov
Hi Anton,
Sorry for the delay.
On Fri, Mar 16, 2018 at 3:10 PM, Anton Pirogov pirogov@cs.rwth-aachen.de wrote:
You can check that:
cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0
and
autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns
Thank you for the report. This bug might be entirely elsewhere.
% cat aut_a.hoa HOA: v1 name: "Evil(1)" States: 2 Start: 0 AP: 1 "p" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc stutter-invariant --BODY-- State: 0 [t] 0 [0] 1 State: 1 {0} [0] 0 --END--
aut_a rejects cycle{!p;p}, but accepts cycle{!p;p;p}. It is therefore not a stutter-invariant language. Yet it pretends to be so with "properties: stutter-invarriant". This is therefore triggering tgba_determinize()'s optimization for stutter-invariant languages, which is wrong to apply here.
If you load aut_a.hoa with "--trust-hoa=no" to ignore all properties, you should get a correct output:
% autfilt --trust-hoa=no -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c 0
Now the question is where is this "properties: stutter-invariant" coming from? I notice that if I run `autfilt --trust-hoa=no --check=stutter aut_a.hoa" the property is added back, which means that Spot itself incorrectly thinks this is a stutter-invariant property... ouch!
In fact from all the 8 implementation of stutter-invariant checks Spot has (see the spot-x man page), only the last one (and the default one!) returns the wrong result.
% for i in 1 2 3 4 5 6 7 8; do SPOT_STUTTER_CHECK=$i autfilt --trust-hoa=no --check=stutter aut_a.hoa | grep properties: done properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-sensitive properties: trans-labels explicit-labels state-acc stutter-invariant
so something is definitely wrong. I'll look into this. Those stutter checks all involve a complementation via determinization, but since only one of them is failing, I hope the issue is not in the determinization.
-
Alexandre Duret-Lutz -
Anton Pirogov