****************************************************************************** * Rabinizer 3 by Jan Kretinsky and Zuzana Komarkova * ****************************************************************************** Arguments: -batch -batch ../benchmarks.txt Transition-based Generalized Rabin Automaton, output in form: Input formula Number of states Size of AC __________________________________________________________________________ G (a | F b) 2 1 ((F G a | F G b) | G F c) 1 4 F (a | b) 2 1 G F (a | b) 1 1 G ((a | b) | c) 2 1 G (a | F (b | c)) 2 1 (F a | G b) 3 2 G (a | F (b & c)) 2 1 (F G a | G F b) 1 2 (G F (a | b) & G F (b | c)) 1 1 ((F F a & G ! a) | (G G ! a & F a)) 2 0 (G F a & F G b) 1 1 ((G F a & F G b) | (F G ! a & G F ! b)) 1 2 (F G a & G F a) 1 1 G (F a & F b) 3 1 (F a & F ! a) 4 1 (((G (b | G F a) & G (c | G F ! a)) | G b) | G c) 4 6 (((G (b | F G a) & G (c | F G ! a)) | G b) | G c) 4 7 (((F (b & F G a) | F (c & F G ! a)) & F b) & F c) 4 2 (((F (b & G F a) | F (c & G F ! a)) & F b) & F c) 4 2 (F G a | G F b) 1 2 ((F G a | G F b) & (F G c | G F d)) 1 4 (((F G a | G F b) & (F G c | G F d)) & (F G h | G F k)) 1 8 (((((F G a | F G b) | F G c) | F G d) | F G h) | G F k) 1 32 G F ((F a | G F b) | F G (a | b)) 1 1 F G ((F a | G F b) | F G (a | b)) 1 1 F G (((F a | G F b) | F G (a | b)) | F G b) 1 1 (F p U G q) 2 1 (G p U q) 5 2 (((p | q) U p) | G q) 3 2 (G (! p | F q) & ((X p U q) | X (((! p | ! q) U ! p) | G (! p | ! q)))) 5 2 (G (q | X G p) & G (r | X G ! p)) 5 3 ((G F (a & X X b) | F G b) & F G (c | (X a & X X b))) 12 2 ((G F (X X X a & X X X X b) & G F (b | X c)) & G F (c & X X a)) 16 1 ((G F a | F G b) & (G F c | F G (d | X e))) 2 5 ((G F (a & X X c) | F G b) & (G F c | F G (d | (X a & X X b)))) 12 4 ((((a U b) & (G F a | F G b)) & (G F c | F G d)) | (((a U c) & (G F a | F G d)) & (G F c | F G b))) 7 6 (G F a | F G b) 1 2 ((G F a | F G b) & (G F b | F G c)) 1 4 (((G F a | F G b) & (G F b | F G c)) & (G F c | F G d)) 1 8 ((((G F a | F G b) & (G F b | F G c)) & (G F c | F G d)) & (G F d | F G h)) 1 16 (((((G F a | F G b) & (G F b | F G c)) & (G F c | F G d)) & (G F d | F G h)) & (G F h | F G k)) 1 32 (X (G r | (r U (r & (s U p)))) U (G r | (r U (r & s)))) 8 2 (p U (q & X (r & F (s & X F (t & X F (u & X F v)))))) 13 1 G (! q | (G p | (! p U (r | ((s & ! p) & X (! p U t)))))) 6 2 G (! q | ((((! s | r) | X (G (! t | r) | (! r U (r & (! t | r))))) U (r | p)) | G (! s | X G ! t))) 16 4 G (! p1 & (p2 U (! p2 U (! p3 | p4)))) 4 1 G ((p1 & X ! p1) | X (p1 U ((! p2 & p1) & X ((p2 & p1) & (p1 U ((! p2 & p1) & X (p2 & p1))))))) 8 1 G (! q | ((! p | (! r U ((s & ! r) & X (! r U t)))) U (r | G (! p | (s & X F t))))) 21 2 G (! q | ((! p | (! r U (((s & ! r) & ! z) & X ((! r & ! z) U t)))) U (r | G (! p | ((s & ! z) & X (! z U t)))))) 21 2 F G (((a & X X b) & G F b) U G (X X ! c | X X (a & b))) 3 1 (G ((F ! a & F (b & X ! c)) & G F (a U d)) & G F (X d U (b | G c))) 7 1