spot/doc/org/oaut.org

Common output options for automata

• Common output options
• HOAF output
• LBTT output
• Spin output
• Dot output
• Statistics
• Naming automata

#+EMAIL spot@lrde.epita.fr

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:

  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
      --dot[=c|h|n|N|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

The main three output formats (that can also been used as input to some of the tools) are HOAF (activated by -H or --hoaf), LBTT (activated by --lbtt), or spin 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 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 autfilt to check whether an input automaton has some property) or if we are only doing some timing.

HOAF output

The 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 ltl2tgba is used to construct two automata: one for a U b and one for (Ga -> Gb) W c.

ltl2tgba -H 'a U b' '(Ga -> Gb) W c'

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 state-acc deterministic
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
[2] 3
State: 1
[0] 1 {0}
State: 2
[!1&!2] 0 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--

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

The 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:

ltl2tgba -Ht 'a U b'

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--

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

ltl2tgba -Hm '(Ga -> Gb) W c'

HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
[2] 3
State: 1 {0}
[0] 1
State: 2
[!1&!2] 0 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3 {0}
[t] 3
State: 4
[!1] 3
[1] 4
--END--

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:

ltl2tgba -Htl 'a U b' '(Ga -> Gb) W c'

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--
HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 0 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0&1&!2] 1 [!1&!2] 0 {0} [1&!2] 2 [2] 3 State: 1 [0] 1 {0} State: 2 [!1&!2] 0 {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 LBTT output has two flavors: state-based (which is used to output Büchi automata or monitors) or transition-based (for TGBA).

ltl2tgba --ba --lbtt 'p0 U p1'

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.

ltl2tgba --ba --lbtt=t 'p0 U p1'

2 1t
0 1
1 -1 p1
0 -1 & p0 ! p1
-1
1 0
1 0 -1 t
-1

Note that the LBTT output generalizes the format output by 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 ltl2dstar.

ltl2tgba --ba --lbtt 'a U b'

2 1
0 1 -1
1 "b"
0 & "a" ! "b"
-1
1 0 0 -1
1 t
-1

Spin output

Spin never claims can be requested using -s or --spin. They can only represent Büchi automata, so these options imply --ba.

ltl2tgba -s 'a U b'

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.

ltl2tgba '(Ga -> Gb) W c'

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"]
}

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

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.

ltl2tgba --dot=vcsn '(Ga -> Gb) W c'

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 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 randaut:

  %%                         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

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:

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'))"

     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.

ltl2tgba --name='TGBA for %f' --dot=n 'a U b'

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 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.

randltl -n -1 a b |
ltl2tgba -H -F- |
autfilt --states=3 --stats='!(%M)' |
ltl2tgba -H -F- |
autfilt --states=3 --stats=%M -n5

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)