Re: [Spot] A bug in determinization procedure of Spot?

Hi Anton, Sorry for the delay. On Fri, Mar 16, 2018 at 3:10 PM, Anton Pirogov <pirogov(a)cs.rwth-aachen.de> wrote: 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