spot/doc/org/oaut.org

#+TITLE: Common output options for automata
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html

Spot supports different output syntaxes for automata.  This page
documents the options, common to all tools where it makes sense, that
are used to specify how to output of automata.

* Common output options

All tools that can output automata implement the following options:

#+BEGIN_SRC sh :results verbatim :exports results
ltl2tgba --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)
      --dot[=c|h|n|N|s|t|v]  GraphViz's format (default).  Add letters to chose
                             (c) circular nodes, (h) horizontal layout, (v)
                             vertical layout, (n) with name, (N) without name,
                             (s) with SCCs, (t) always transition-based
                             acceptance.
  -H, --hoaf[=s|t|m|l]       Output the automaton in HOA format.  Add letters
                             to select (s) state-based acceptance, (t)
                             transition-based acceptance, (m) mixed acceptance,
                             (l) single-line output
      --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
  -q, --quiet                suppress all normal output
  -s, --spin                 Spin neverclaim (implies --ba)
      --spot                 SPOT's format
      --stats=FORMAT         output statistics about the automaton
#+end_example

The main three output formats (that can also been used as input to
some of the tools) are [[http://adl.github.io/hoaf/][HOAF]] (activated by =-H= or =--hoaf=), [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]]
(activated by =--lbtt=), or spin [[http://spinroot.com/spin/Man/never.html][never claims]] (activated by =-s= or
=--spin=).  These three formats also support *streaming*, i.e., you
can concatenate multiple automata (and even mix these three formats in
the same stream), and the tools will be able to read and process them
in sequence.

The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=--dot=), Spot's
historical by deprecated format (=--spot=), various statistics
(=--stats=), or nothing at all (=--quiet=).  Of course it may seem
strange to ask a tool to not output anything, but it can make sense if
only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check
whether an input automaton has some property) or if we are only doing
some timing.


* HOAF output

The [[http://adl.github.io/hoaf/][HOAF]] output should be the preferred format to use if you want to
pass automata between different tools.  This format can be requested
using the =-H= option.

Here is an example where [[file:ltl2tgba.org][=ltl2tgba=]] is used to construct two automata:
one for =a U b= and one for =(Ga -> Gb) W c=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -H 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "a U b"
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
#+end_example

The above output contains to automata, named after the formulas they
represent.  Here is a picture of these two automata:

#+NAME: hoafex
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba --dot=cn '(Ga -> Gb) W c' 'a U b' | dot | gvpack |
perl -pe 's/\\\n//g;s/\\/\\\\/g;s/graph G/graph cluster/g'
#+END_SRC
#+RESULTS: hoafex
#+begin_example
digraph root {
	graph [bb="0,0,425,231.06",
		labelloc=t,
		lheight=0.21,
		rankdir=LR
	];
	node [label="\\N",
		shape=circle
	];
	subgraph cluster {
		graph [bb="",
			label="(Gb | F!a) W c",
			labelloc=t,
			lheight=0.21,
			lp="196.5,196.66",
			lwidth=1.14,
			rankdir=LR
		];
		node [height="",
			label="\\N",
			pos="",
			shape=circle,
			style="",
			width=""
		];
		edge [label="",
			lp="",
			pos=""
		];
		I		 [height=0.013889,
			label="",
			pos="1,49.162",
			style=invis,
			width=0.013889];
		1		 [height=0.5,
			label=1,
			pos="56,49.162",
			width=0.5];
		I -> 1		 [pos="e,37.942,49.324 1.1549,49.324 2.6725,49.324 15.097,49.324 27.628,49.324"];
		1 -> 1		 [label="!a & !c\\n{0}",
			lp="56,100.32",
			pos="e,62.379,66.361 49.621,66.361 48.319,76.181 50.445,85.324 56,85.324 59.472,85.324 61.604,81.752 62.398,76.677"];
		0		 [height=0.5,
			label=0,
			pos="189,121.16",
			width=0.5];
		1 -> 0		 [label="a & b & !c",
			lp="122.5,113.82",
			pos="e,171.82,115.02 70.135,60.558 76.501,65.71 84.4,71.688 92,76.324 114.85,90.263 142.72,102.89 162.53,111.19"];
		2		 [height=0.5,
			label=2,
			pos="189,34.162",
			width=0.5];
		1 -> 2		 [label="a & !c",
			lp="122.5,64.823",
			pos="e,174.09,44.491 73.626,53.241 93.026,57.118 125.9,61.52 153,54.324 157.19,53.213 161.39,51.47 165.37,49.466"];
		3		 [height=0.5,
			label=3,
			pos="375,34.162",
			width=0.5];
		1 -> 3		 [label=c,
			lp="240.5,9.8235",
			pos="e,359.03,25.984 66.028,34.328 72.163,25.634 81.128,15.425 92,10.324 114,0 275.42,0.3271 310,7.3235 323.76,10.107 338.24,15.942 349.94,21.478"];
		0 -> 0		 [label="b\\n{0}",
			lp="189,172.32",
			pos="e,197.63,137.24 180.37,137.24 178.11,147.47 180.99,157.32 189,157.32 194.26,157.32 197.3,153.08 198.14,147.27"];
		2 -> 1		 [label="!a & !c\\n{0}",
			lp="122.5,35.324",
			pos="e,68.596,36.184 172.36,26.591 166.44,24.064 159.55,21.586 153,20.324 126.38,15.197 117.5,11.13 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"];
		2 -> 2		 [label="a & !c",
			lp="189,77.824",
			pos="e,197.63,50.24 180.37,50.24 178.11,60.474 180.99,70.324 189,70.324 194.26,70.324 197.3,66.082 198.14,60.273"];
		2 -> 3		 [label="!a & c",
			lp="292,105.82",
			pos="e,363.94,48.712 202.25,46.94 217.46,61.618 244.99,85.026 274,94.324 289.24,99.207 295.12,100.21 310,94.324 329.12,86.764 345.87,70.495 357.43,56.803"];
		4		 [height=0.5,
			label=4,
			pos="292,34.162",
			width=0.5];
		2 -> 4		 [label="a & c",
			lp="240.5,41.824",
			pos="e,273.78,34.324 207.13,34.324 222.59,34.324 245.58,34.324 263.59,34.324"];
		3 -> 3		 [label="1\\n{0}",
			lp="375,85.324",
			pos="e,382.03,50.988 367.97,50.988 366.41,60.949 368.75,70.324 375,70.324 379,70.324 381.4,66.475 382.2,61.092"];
		4 -> 3		 [label="!a",
			lp="333.5,41.824",
			pos="e,356.85,34.324 310.18,34.324 320.81,34.324 334.69,34.324 346.8,34.324"];
		4 -> 4		 [label=a,
			lp="292,77.824",
			pos="e,299.03,50.988 284.97,50.988 283.41,60.949 285.75,70.324 292,70.324 296,70.324 298.4,66.475 299.2,61.092"];
	}
	subgraph cluster_gv1 {
		graph [bb="",
			label="a U b",
			labelloc=t,
			lheight=0.21,
			lp="80.5,88.5",
			lwidth=0.43,
			rankdir=LR
		];
		node [height="",
			label="\\N",
			peripheries="",
			pos="",
			shape=circle,
			style="",
			width=""
		];
		edge [label="",
			lp="",
			pos=""
		];
		I_gv1		 [height=0.013889,
			label="",
			pos="261,156.16",
			style=invis,
			width=0.013889];
		"1_gv1"		 [height=0.5,
			label=1,
			pos="316,156.16",
			width=0.5];
		I_gv1 -> "1_gv1"		 [pos="e,297.94,156.16 261.15,156.16 262.67,156.16 275.1,156.16 287.63,156.16"];
		"1_gv1" -> "1_gv1"		 [label="a & !b",
			lp="316,199.66",
			pos="e,322.38,173.2 309.62,173.2 308.32,183.02 310.44,192.16 316,192.16 319.47,192.16 321.6,188.59 322.4,183.51"];
		"0_gv1"		 [height=0.72222,
			label=0,
			peripheries=2,
			pos="399,156.16",
			width=0.72222];
		"1_gv1" -> "0_gv1"		 [label=b,
			lp="355.5,163.66",
			pos="e,376.81,156.16 334.18,156.16 343.61,156.16 355.6,156.16 366.64,156.16"];
		"0_gv1" -> "0_gv1"		 [label=1,
			lp="399,203.66",
			pos="e,406.68,177.15 391.32,177.15 390.37,187.25 392.93,196.16 399,196.16 402.89,196.16 405.34,192.5 406.35,187.22"];
	}
}
#+end_example

#+BEGIN_SRC dot :file hoafex.png :cmdline -Tpng :var txt=hoafex :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:hoafex.png]]

The [[http://adl.github.io/hoaf/][HOA format]] support both state and transition-based acceptance.
Although Spot works only with transition-based acceptance, its output
routines default to state-based acceptance whenever possible (this is
the case in the first of these two automata) and use transition-based
acceptance otherwise.  You can change this behavior using =-Hs= (or
=--hoaf=s=), =-Ht=, or =-Hm=.  Option =s= corresponds to the default
to use state-based acceptance whenever possible.  Option =t= forces
transition-based acceptance.  For instance compare this output to the
previous one:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Ht 'a U b'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "a U b"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1
[t] 1 {0}
--END--
#+end_example

Option =m= uses mixed acceptance, i.e, some states might use
state-based acceptance while other will not:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Hm '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels
--BODY--
State: 0 {0}
[0] 0
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3 {0}
[t] 3
State: 4
[!1] 3
[1] 4
--END--
#+end_example


It is also possible to output each automaton on a single line, in case
the result should be used with line-based tools or embedded into a CSV
file...  Here is an example using both transition-based acceptance,
and single-line output:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Htl 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
: HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [t] 0 {0} State: 1 [1] 0 [0&!1] 1 --END--
: HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--

* LBTT output

The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based (which is used to output
Büchi automata or monitors) or transition-based (for TGBA).

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt 'p0 U p1'
#+END_SRC
#+RESULTS:
: 2 1
: 0 1 -1
: 1 p1
: 0 & p0 ! p1
: -1
: 1 0 0 -1
: 1 t
: -1

If you want to request transition-based output even for Büchi automata,
use =--lbtt=t=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt=t 'p0 U p1'
#+END_SRC

#+RESULTS:
: 2 1t
: 0 1
: 1 -1 p1
: 0 -1 & p0 ! p1
: -1
: 1 0
: 1 0 -1 t
: -1

Note that the [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output generalizes the format output by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]] with
support for transition-based acceptance.  Both formats however are
restricted to atomic propositions of the form =p0=, =p1=, etc...  In
case other atomic propositions are used, Spot output them in double
quotes.  This other extension of the format is also supported by
[[http://www.ltl2dstar.de/][ltl2dstar]].

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt 'a U b'
#+END_SRC

#+RESULTS:
: 2 1
: 0 1 -1
: 1 "b"
: 0 & "a" ! "b"
: -1
: 1 0 0 -1
: 1 t
: -1

* Spin output

Spin [[http://spinroot.com/spin/Man/never.html][never claims]] can be requested using =-s= or =--spin=.  They can only
represent Büchi automata, so these options imply =--ba=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -s 'a U b'
#+END_SRC

#+RESULTS:
: never {
: T0_init:
:   if
:   :: ((b)) -> goto accept_all
:   :: ((a) && (!(b))) -> goto T0_init
:   fi;
: accept_all:
:   skip
: }

* Dot output

The =--dot= option (which usually is the default) causes automata to be
output in GraphViz's format.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba '(Ga -> Gb) W c'
#+END_SRC

#+RESULTS:
#+begin_example
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0"]
  0 -> 0 [label="b\n{0}"]
  1 [label="1"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 [label="2"]
  2 -> 1 [label="!a & !c\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 [label="3"]
  3 -> 3 [label="1\n{0}"]
  4 [label="4"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

This output should be processed with =dot= to be converted into a
picture.  For instance use =dot -Tpng= or =dot -Tpdf=.

#+NAME: oaut-dot1
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
#+END_SRC

#+RESULTS: oaut-dot1
#+begin_example
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0"]
  0 -> 0 [label="b\\n{0}"]
  1 [label="1"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 [label="2"]
  2 -> 1 [label="!a & !c\\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 [label="3"]
  3 -> 3 [label="1\\n{0}"]
  4 [label="4"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

#+BEGIN_SRC dot :file oaut-dot1.png :cmdline -Tpng :var txt=oaut-dot1 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:oaut-dot1.png]]

This output can be customized by passing optional characters to the
=--dot= option.  For instance =v= requests a vertical layout (instead
of the default horizontal layout), =c= requests circle states, =s=
causes strongly-connected components to be displayed, and =n= causes
the name (see below) of the automaton to be displayed.

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba --dot=vcsn '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
  label="(Gb | F!a) W c"
  labelloc="t"
  node [shape="circle"]
  I [label="", style=invis, height=0]
  I -> 1
  subgraph cluster_0 {
  0 [label="0"]
  }
  subgraph cluster_1 {
  3 [label="3"]
  }
  subgraph cluster_2 {
  4 [label="4"]
  }
  subgraph cluster_3 {
  1 [label="1"]
  2 [label="2"]
  }
  0 -> 0 [label="b\n{0}"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 -> 1 [label="!a & !c\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 -> 3 [label="1\n{0}"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

#+NAME: oaut-dot2
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba --dot=vcsn '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
#+END_SRC

#+RESULTS: oaut-dot2
#+begin_example
digraph G {
  label="(Gb | F!a) W c"
  labelloc="t"
  node [shape="circle"]
  I [label="", style=invis, height=0]
  I -> 1
  subgraph cluster_0 {
  label=""
  0 [label="0"]
  }
  subgraph cluster_1 {
  label=""
  3 [label="3"]
  }
  subgraph cluster_2 {
  label=""
  4 [label="4"]
  }
  subgraph cluster_3 {
  label=""
  1 [label="1"]
  2 [label="2"]
  }
  0 -> 0 [label="b\\n{0}"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 -> 1 [label="!a & !c\\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 -> 3 [label="1\\n{0}"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

#+BEGIN_SRC dot :file oaut-dot2.png :cmdline -Tpng :var txt=oaut-dot2 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:oaut-dot2.png]]

* Statistics

The =--stats= option takes format string parameter to specify what and
how statistics should be output.

Most tool support a common set of statistics about the output
automaton (like =%s= for the number of states, =%t= for transitions,
=%e= for edges, etc.)  Additional statistics might be available
depending on what the tool does (for instance [[file:autfilt.org][=autfilt=]] also has =%S=,
=%T=, and =%E= to display the same statistics about the input
automaton).  All the available statistics are displayed when a tool is
run with =--help=.

For instance here are the statistics available in [[file:randaut.org][=randaut=]]:

#+BEGIN_SRC sh :results verbatim :exports results
randaut --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
  %%                         a single %
  %a                         number of acceptance sets
  %c                         number of SCCs
  %d                         1 if the output is deterministic, 0 otherwise
  %e                         number of edges
  %F                         seed number
  %L                         automaton number
  %m                         name of the automaton
  %n                         number of nondeterministic states in output
  %p                         1 if the output is complete, 0 otherwise
  %r                         processing time (excluding parsing) in seconds
  %s                         number of states
  %t                         number of transitions
  %w                         one word accepted by the output automaton
#+end_example

In most tools =%F= and =%L= are the input filename and line number,
but as this makes no sense in =randaut=, these two sequences emit
numbers related to the generation of automata.

For instance let's generate 100 random automata with 10 states and
density 0.2, and just count the number of edges in each automaton. Then
use =R= to summarize the distribution of these values:

#+BEGIN_SRC sh :results verbatim :exports both
randaut -d 0.2 -S 10 -n 1000 a --stats %e > size.csv
R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))"
#+END_SRC

#+RESULTS:
:      edges
:  Min.   :17.00
:  1st Qu.:25.00
:  Median :28.00
:  Mean   :27.96
:  3rd Qu.:30.00
:  Max.   :42.00


For $S=10$ states and density $D=0.2$ the expected degree of each
state $1+(S-1)D = 1+9\times 0.2 = 2.8$ so the expected number of edges
should be 10 times that.


* Naming automata

Automata can be given names.  This name can be output in GraphViz
output when =--dot=n= is given, and is also part of the HOA format (as
activated by =-H=).

By default, =ltl2tgba= will use the input format as name.  Other tools
have no default name.  This name can be changed using the =--name= option,
that takes a format string similar to the one of =--stats=.

#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba --name='TGBA for %f' --dot=n 'a U b'
#+END_SRC

#+RESULTS:
#+begin_example
digraph G {
  rankdir=LR
  label="TGBA for a U b"
  labelloc="t"
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label="1"]
  1 [label="1"]
  1 -> 0 [label="b"]
  1 -> 1 [label="a & !b"]
}
#+end_example

#+NAME: oaut-name
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba --name='TGBA for %f' --dot=n 'a U b' | sed 's/\\/\\\\/'
#+END_SRC

#+RESULTS: oaut-name
#+begin_example
digraph G {
  rankdir=LR
  label="TGBA for a U b"
  labelloc="t"
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label="1"]
  1 [label="1"]
  1 -> 0 [label="b"]
  1 -> 1 [label="a & !b"]
}
#+end_example

#+BEGIN_SRC dot :file oaut-name.png :cmdline -Tpng :var txt=oaut-name :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:oaut-name.png]]

If you have an automaton saved in the HOA format, you can extract its
name using =autfilt --stats=%M input.hoa=. The =%M= escape sequence is
replaced by the name of the input automaton.

Here is a pipeline of commands that generates five LTL formulas
$\varphi$ such that both $\varphi$ and $\lnot\varphi$ are translated
into a 3-state TGBA by [[file:ltl2tgba.org][=ltl2tgba=]].  It starts by generating an
infinite stream of random LTL formulas using =a= and =b= as atomic
propositions, then it converts these formulas as TGBA (in the HOA
format, therefore carrying the formula as name), filtering only the
TGBA with 3 states and outputting =!(%M)= (that is the negation of the
associated formula), translating the resulting formulas as TGBA, again
retaining only the names (i.e. formulas) of the automata with 3
states, and finally restricting the output to the first 5 matches
using =autfilt -n5=.

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 a b |
ltl2tgba -H -F- |
autfilt --states=3 --stats='!(%M)' |
ltl2tgba -H -F- |
autfilt --states=3 --stats=%M -n5
#+END_SRC

#+RESULTS:
: G(F!a & XF(a | G!b))
: GFb | G(!b & FG!b)
: !a & F((a | b) & (!a | !b))
: !a | (b R a)
: !b & X(!b U a)

#  LocalWords:  num toc html syntaxes ltl tgba sed utf UTF lbtt SCCs
#  LocalWords:  GraphViz's hoaf HOA LBTT's neverclaim ba SPOT's Gb cn
#  LocalWords:  GraphViz autfilt acc Buchi hoafex gvpack perl pe bb
#  LocalWords:  labelloc rankdir subgraph lp pos invis gv png cmdline
#  LocalWords:  Tpng txt Hs Hm CSV Htl LBT dstar init goto fi Tpdf XF
#  LocalWords:  oaut vcsn randaut nondeterministic filename csv hoa
#  LocalWords:  varphi lnot GFb FG