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.