❶>] 0 -> 0 [label=

⓿>] 1 -> 1 [label=<1>] 2 [label=<2>] 2 -> 0 [label=

❶❸>] 0 -> 0 [label=

⓿❸>] 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] 1 -> 3 [label=] 2 [label=<2

❶❷>] 2 -> 0 [label=] 2 -> 1 [label=] 2 -> 2 [label=] 2 -> 3 [label=] 3 [label=<3

⓿❷>] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] 3 -> 3 [label=] } #+end_example #+BEGIN_SRC dot :file gfafgb.png :cmdline -Tpng :var txt=gfafgb :exports results $txt #+END_SRC #+RESULTS: [[file:gfafgb.png]] And now its conversion by =dstar2tgba= to a 4-state TGBA. We don't pass any option to =dstar2tgba= because converting to TGBA is the default: #+NAME: gfagfb2ba #+BEGIN_SRC sh :results verbatim :exports code dstar2tgba gfagfb -d #+END_SRC #+RESULTS: gfagfb2ba #+begin_example digraph G { rankdir=LR node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 0 [label=⓿❶>] 0 -> 1 [label=⓿❶>] 0 -> 2 [label=⓿❶>] 0 -> 3 [label=⓿❶>] 1 [label="1"] 1 -> 0 [label=❶>] 1 -> 1 [label=❶>] 1 -> 2 [label=❶>] 1 -> 3 [label=❶>] 2 [label="2"] 2 -> 0 [label=⓿>] 2 -> 1 [label=⓿>] 2 -> 2 [label=⓿>] 2 -> 3 [label=⓿>] 3 [label="3"] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] 3 -> 3 [label=] } #+end_example #+BEGIN_SRC dot :file gfagfb2ba.png :cmdline -Tpng :var txt=gfagfb2ba :exports results $txt #+END_SRC #+RESULTS: [[file:gfagfb2ba.png]] Obviously the resulting automaton could be simplified further, as the minimal TGBA for this formula has a single state. (Patches welcome...) * Details ** General behavior The =dstar2tgba= tool implements a 4-step process: 1. read the automaton 2. convert it into TGBA 3. postprocess the resulting TGBA (simplifying the automaton, a degeneralizing it into a BA or Monitor if requested) 4. output the resulting automaton BTW, the above scenario is also exactly what you get with [[file:autfilt.org][=autfilt=]] if you run it as =autfilt --tgba --high --small=. (This is true only since version 1.99.4, since both tools can now read the same file formats.) ** Controlling output The last two steps are shared with =ltl2tgba= and use the same options. The type of automaton to produce can be selected using the =-B= or =-M= switches: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -B, --ba Büchi Automaton (implies -S) : -C, --complete output a complete automaton : -M, --monitor Monitor (accepts all finite prefixes of the given : property) : -S, --state-based-acceptance, --sbacc : define the acceptance using states : --tgba Transition-based Generalized Büchi Automaton : (default) And these may be refined by a simplification goal, should the post-processor routine had a choice to make: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference, do not bother making it small or : deterministic : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) The effort put into post-processing can be limited with the =--low= or =--medium= options: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : --high all available optimizations (slow, default) : --low minimal optimizations (fast) : --medium moderate optimizations For instance using =-a --low= will skip any optional post-processing, should you find =dstar2tgba= too slow. Finally, the output format can be changed with the following [[file:oaut.org][common ouput options]]: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) --check[=PROP] test for the additional property PROP and output the result in the HOA format (implies -H). PROP may be any prefix of 'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'. -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] GraphViz's format. Add letters for (1) force numbered states, (a) acceptance display, (b) acceptance sets as bullets, (B) bullets except for Büchi/co-Büchi automata, (c) force circular nodes, (e) force elliptic nodes, (f(FONT)) use FONT, (h) horizontal layout, (v) vertical layout, (n) with name, (N) without name, (o) ordered transitions, (r) rainbow colors for acceptance sets, (R) color acceptance sets by Inf/Fin, (s) with SCCs, (t) force transition-based acceptance, (+INT) add INT to all set numbers -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format (default). Add letters to select (i) use implicit labels for complete deterministic automata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transition-based acceptance, (k) use state labels when possible, (l) single-line output, (v) verbose properties --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton -o, --output=FORMAT send output to a file named FORMAT instead of standard output. The first automaton sent to a file truncates it unless FORMAT starts with '>>'. -q, --quiet suppress all normal output -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to select (6) Spin's 6.2.4 style, (c) comments on states --stats=FORMAT output statistics about the automaton #+end_example The =--stats= options can output statistics about the input and the output automaton, so it can be useful to search for particular pattern. For instance here is a complex command that will 1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]], 2. use [[file:ltlfilt.org][=ltlfilt=]] to rewrite the W and M operators away (=--remove-wm=), simplify the formulas (=-r=), remove duplicates (=u=) as well as formulas that have a size less then 3 (=--size-min=3=), 3. use =head= to keep only 10 of such formula 4. loop to process each of these formula: - print it - then convert the formula into =ltl2dstar='s input format, process it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA transltor), and process the result with =dstar2tgba= to build a Büchi automaton (=-B=), favoring determinism if we can (=-D=), and finally displaying some statistics about this conversion. The statistics displayed in this case are: =%S=, the number of states of the input (Rabin) automaton, =%s=, the number of states of the output (Büchi) automaton, =%d=, whether the output automaton is deterministic, and =%p= whether the automaton is complete. #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 --tree-size=10..14 a b c | ltlfilt --remove-wm -r -u --size-min=3 | head -n 10 | while read f; do echo "$f" ltlfilt -l -f "$f" | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p' done #+END_SRC #+RESULTS: #+begin_example (b | Fa) R Fc DRA: 9st.; BA: 9st.; det.? 1; complete? 1 Ga U (Gc R (!a | Gc)) DRA: 7st.; BA: 7st.; det.? 0; complete? 0 GFc DRA: 3st.; BA: 3st.; det.? 1; complete? 1 !a | (a R b) DRA: 3st.; BA: 2st.; det.? 1; complete? 0 Xc R (G!c R (b | G!c)) DRA: 4st.; BA: 2st.; det.? 1; complete? 0 c & G(b | F(a & c)) DRA: 4st.; BA: 3st.; det.? 1; complete? 0 XXFc DRA: 4st.; BA: 4st.; det.? 1; complete? 1 XFc | Gb DRA: 5st.; BA: 4st.; det.? 1; complete? 1 G(((!a & Gc) | (a & F!c)) U (!a | Ga)) DRA: 6st.; BA: 5st.; det.? 1; complete? 1 a & !b DRA: 3st.; BA: 2st.; det.? 1; complete? 0 #+end_example An important point you should be aware of when comparing these numbers of states is that the deterministic automata produced by =ltl2dstar= are complete, while the automata produced by =dstar2tgba= (deterministic or not) are not complete by default. This can explain a difference of one state (the so called "sink" state). You can instruct =dstar2tgba= to output a complete automaton using the =--complete= option (or =-C= for short). ** Conversion of various acceptance conditions to TGBA and BA Spot implements several acceptance conversion algorithms. There is one generic cases, with some specialized variants. *** Generic case The most generic one, called =remove_fin()= in Spot, takes an automaton with any acceptance condition, and as its name suggests, it removes all the =Fin(x)= from the acceptance condition: the output is an automaton whose acceptance conditions is a Boolean combination of =Inf(x)= acceptance primitive. (Such automata with Fin-less acceptance can be easily tested for emptiness using SCC-based emptiness checks.) This algorithm works by fist converting the acceptance conditions into disjunctive normal form, and then removing any =Fin(x)= acceptance by adding non-deterministic jumps into clones of the SCCs that intersect set =x=. This is done with a few tricks that limits the numbers of clones, and that ensure that the resulting automaton uses /at most/ one extra acceptance sets. This algorithm is not readily available from =dstar2tgba=, but [[file:autfilt.org][=autfilt=]] has an option =--remove-fin= if you need it. From an automaton with Fin-less acceptance, one can obtain a TGBA without changing the transitions structure: take the Fin-less acceptance, transform it into conjunctive normal form (CNF), and create one new Fin-accepting set for each conjunct of the CNF. The combination of these two algorithms is implemented by the =to_generalized_buchi()= function in Spot. Finally a TGBA can easily be converted into a BA with classical degeneralization algorithms (our version of that includes several SCC-based optimizations described in our [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.13.spin.pdf][SPIN'13 paper]]). This generalized case is specialized for two types of acceptances that are common (Rabin and Streett). *** State-based Rabin to BA For state-based Rabin automata, and dedicated conversion to BA is used. The conversion implemented is a variation of Krishnan et al.'s "Deterministic ω-Automata vis-a-vis Deterministic Büchi Automata" (ISAAC'94) paper. They explain how to convert a deterministic Rabin automaton (DRA) into a deterministic Büchi automaton (DBA) when such an automaton exist. The surprising result is that when a DRA is DBA-realizable, a DBA can be obtained from the DRA without changing its transition structure. Spot implements a slight refinement to the above technique by doing it SCC-wise: any DRA will be converted into a BA, and the determinism will be conserved only for strongly connected components where determinism can be conserved. (If some SCC is not DBA-realizable, it will be cloned into several deterministic SCC, but the jumps between these SCCs will be nondeterministic.) This specialized conversion is built in the =remove_fin()= procedure described above. *** Streett to TGBA Streett acceptance have a specialized conversion into non-deterministic TGBA. This improved conversion is automatically used by =to_generalized_buchi()=. When a Streett automaton uses multiple acceptance pairs, we use generalized acceptance conditions in the TGBA to limit the combinatorial explosion. A straightforward translation from Streett to BA, as described for instance by [[http://www.automata.rwth-aachen.de/~loeding/diploma_loeding.pdf][Löding's diploma thesis]], will create a BA with $|Q|\cdot(4^n-3^n+2)$ states if the input Streett automaton has $|Q|$ states and $n$ acceptance pairs. Our translation to TGBA limits this to $|Q|\cdot(2^n+1)$ states. Sometimes, as in the [[#streett_to_tgba_example][example for =GFa & GFb=]] the output of this conversion happens to be deterministic. This is pure luck: Spot does not implement any algorithm to preserve the determinism of Streett automata.