out-of-date example on satmin.html
On https://spot.lrde.epita.fr/satmin.html#sec-2 there the following example:
There are cases where ltl2tgba's tba-det algorithm fails to produce a deterministic automaton. In that case, SAT-based minimization is simply skipped. For instance:
ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d' states=5, det=1
outputting a determinitic automaton contradicts the text.
This is a case where tba-det works. I'm not sure what changed and when it started to work, but we need to find another example of syntactic-recurrence that tba-det cannot determinize.
PS: while we are at it, we should try to favor single-quotes over double-quotes in examples so that users do not get any surprise with interactive shells interpreting !
.