using more acceptance sets than needed by the acceptance condition

[adl]

Tomáš and Fanda recently found that when autfilt is fed an automaton with Acceptance: 1 t, it interprets it as Acceptance: 1 Inf(0). This looks bogus to me. I think the original acceptance condition states "the automaton will use one acceptance set, but this set is not used to decide acceptance of runs: all runs are acceptings".

We could also imagine something like Acceptance: 3 Inf(0)&Fin(2) not using the acceptance set 1 for the purpose of acceptance. But maybe {1} can be used for another purpose that does not affect the semantics, e.g., as a state or transition marker for debugging an algorithm.

So far, there is no discussion about this kind of acceptance in the specification of the format. I think we should either explicitely allow it or explicitely disallow it. Something like

An acceptance condition declaring $m$ sets need not actually use all of these sets.  
In this case the unused sets can be ignored if they appear in the body of the automaton.

or

An acceptance condition declaring $m$ sets must use all of these sets.

What do you think? I have a slight preference for allowing unused sets, but I've no problem with the other (and simpler) solution.

[xblahoud]

I agree that this kind of sets can be usefull for debugging. Therefore I also prefer the first possibility. But the stricter one is also OK with me.

[adl]

I have fixed the HOA parser of Spot to ignore unused acceptance sets when reading an automaton. That means you can input something like Acceptance: 3 Fin(1) but the output will have Acceptance: 1 Fin(0).

[strejcek]

I also prefer the first possibility (thanks for implementing it).

[JanKretinsky]

yep, same opinion, thanks