1# Formulas from Gasier et al., "Rabinizer: Small deterministic 2# automata for LTL(F,G)" (ATVA'12) 3G(a | Fb) 4FGa | FGb | GFc 5F(a | b) 6GF(a | b) 7G(a | Fa) 8G(a | b | c) 9G(a | F(b | c)) 10Fa | Gb 11G(a | F(b & c)) 12FGa | GFb 13GF(a | b) & GF(b | c) 14 15FF(a & G!a) | (GG!a & Fa) 16GFa & FGb 17(GFa & FGb) | (FG!a & GF!b) 18FGa & GFa 19G(Fa & Fb) 20Fa & F!a 21G(b | GFa) & G(c | GF!a) | Gb | Gc 22G(b | FGa) & G(c | FG!a) | Gb | Gc 23F(b & FGa) | F(c & FG!a) & Fb & Fc 24F(b & GFa) | F(c & GF!a) & Fb & Fc 25 26GFa -> GFb 27(GFa -> GFb) & (GFc -> GFd) 28 29GF(Fa | GFb | FG(a | b)) 30FG(Fa | GFb | FG(a | b)) 31FG(Fa | GFb | FG(a | b) | FGb) 32 33# formulas from DBA minimizer 34XXa 35GF(a -> XXXb) 36F(p & XF(q & XF(r & XFs))) 37F(q & X(p U r)) 38F(p & X(q & XFr)) 39p U (q & X(r U s)) 40G(a -> Fb) & G(c -> Fd) 41GFa & GFb 42GFa | GFb | GFc 43GFa 44a U b U c U d 45G(a -> Fb) & Gc 46(Ga -> Fb) & (G!a -> F!b) 47p U (q & X(r & F(s & XF(u & XF(v & XFw))))) 48G(a -> Fb) & G(b -> Fc) 49G(a -> Fb) & G(!a -> F!b) 50GFp && GFq && GF r && GF u 51GF(a <-> XXXb) 52G(p -> q U r) 53GF(a <-> XXb) 54G!c & G(a -> Fb) & G(b -> Fc) 55G(a -> XXXb) 56G(a -> Fb) 57G(a U b U !a U !b) 58(p U q U r) || (q U r U p) || (r U p U q) 59 60# Some random formulas that are determinizable with tba-det 61X((a M F((!c & !b) | (c & b))) W (G!c U b)) 62X(((a & b) R (!a U !c)) R b) 63XXG(Fa U Xb) 64(!a M !b) W F!c 65(b & Fa & GFc) R a 66(a R (b W a)) W G(!a M (c | b)) 67(Fa W b) R (Fc | !a) 68X(G(!a M !b) | G(a | G!a)) 69Fa W Gb 70Ga | GFb 71a M G(F!b | X!a) 72G!a R XFb 73XF(!a | GFb) 74G(F!a U !a) U Xa 75(a | G(a M !b)) W Fc 76Fa W Xb 77X(a R ((!b & F!c) M X!a)) 78XG!a R Fb 79GFc | (a & Fb) 80X(a R (Fb R F!b)) 81G(Xa M Fa) 82X(Gb | GFa) 83X(Gc | XG((b & Ga) | (!b & F!a))) 84Ga R Fb 85G(a U (b | X((!c & !a) | (a & c)))) 86XG((G!a & F!b) | (Fa & (a | Gb))) 87(a U X!a) | XG(!b & XFc) 88X(G!a | GFa) 89G(G!a | F!c | G!b) 90 91# Some random formulas that should only be determinizable via dstar2tgba 92# Generated with 93# randltl -n -1 a b c | 94# ltlfilt --remove-wm -r -u --size-min=3 --size-max=15 --syntactic-recurrence | 95# ltlfilt -v --obligation | ltl2tgba -F - -x tba-det -D --stats='%d,%f' | 96# grep 0, | head -n 30 97 98X(Fc W b) R Fa 99!b & ((Fa U b) W Xc) 100G(F!c | (Fb U a)) 101(c R (b R Fa)) W XGb 102X((Fb & XFa) R XFc) 103(Ga R (F!c U b)) W b 104X(!b | G(b & !a)) R F(c & Fa) 105G(Fc | Ga | XXF!b) 106G(F(!a & Fa) U (b U Xc)) 107G(F!c U X(Xb & F!b)) 108G(XXFa U (b | a | Fc)) 109G(c | F!a | (b U Xb)) 110G(a U X(a | (F!b U Xc))) 111XF!a R F(b | (!a & F!c)) 112(c & Xc) R ((!b | XFc) U a) 113G(Gb | (b & c) | F(!a & XXa)) 114G(X(Fc & Xa) M Fb) 115X(!c & Fc) R (c M Fa) 116G(Ga | X(Fc U (b | X!b))) 117G(XXFb U (c | (!c & F!a))) 118((Fc U b) R Fa) W X!a 119G(a | X(a R (GFb | (Fc U a)))) 120(F!c R F!b) W G!a 121(Fb & !b) R (!a R XFc) 122F(Fb & c) W Xa 123G(G!c | ((Fb U a) U c)) 124(Fa & XXb) R Fc 125Gc R (F!a & (b U a)) 126(c R Fa) U X!b 127GF(b & XXXFc) 128 129# Extra ones 130G(F(a & F(b & Fc))) 131(GFa & GFb) | (GFc & GFd) 132