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 !.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information