GitLab

The following is done by the spot::cleanup_acceptance() function:

1. remove sets number from the automaton that do not appear in the acceptance
2. remove sets from the acceptance that do not appear in the automaton (simplifying the acceptance this way might in turn make some set number unused so start the process again in that case.)

The following is additionally done by spot::simplify_acceptance():

3. find set numbers that always appear together and replace them by the smallest one
4. If sets #i and #j are the complement of each other, then
   • Fin(i) & Inf(j) is replaced by Fin(i)
   • Fin(i) & Fin(j) is replaced by f
   • Fin(i) | Inf(j) is replaced by Inf(j)
   • Inf(i) | Inf(j) is replaced by t

Writing this, I realize that there are a couple of easy simplifications that are still missing, namely

• replace Fin(i) & Inf(i) by f
• replace Fin(i) | Inf(i) by t

I suggest that we add these two simplifications to simplify_acceptance().