trivial acceptance simplifications missing
The following is done by the spot::cleanup_acceptance()
function:
- remove sets number from the automaton that do not appear in the acceptance
- 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()
:
- find set numbers that always appear together and replace them by the smallest one
- If sets #i and #j are the complement of each other, then
-
Fin(i) & Inf(j)
is replaced byFin(i)
-
Fin(i) & Fin(j)
is replaced byf
-
Fin(i) | Inf(j)
is replaced byInf(j)
-
Inf(i) | Inf(j)
is replaced byt
-
Writing this, I realize that there are a couple of easy simplifications that are still missing, namely
- replace
Fin(i) & Inf(i)
byf
- replace
Fin(i) | Inf(i)
byt
I suggest that we add these two simplifications to simplify_acceptance()
.