a75a9c091c
This fixes #85. * src/misc/random.hh (barand): Use round() before casting. * doc/org/oaut.org: Recompute example. * src/tests/randaut.test, wrap/python/tests/randaut.ipynb: Adjust.
1042 lines
30 KiB
Org Mode
1042 lines
30 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: Common output options for automata
|
|
#+SETUPFILE: setup.org
|
|
#+HTML_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[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v]
|
|
GraphViz's format (default). Add letters for (a)
|
|
acceptance display, (b) acceptance sets as
|
|
bullets,(c) circular nodes, (f(FONT)) use FONT,
|
|
(h) horizontal layout, (v) vertical layout, (n)
|
|
with name, (N) without name, (r) rainbow colors
|
|
for acceptance set, (R) color acceptance set by
|
|
Inf/Fin, (s) with SCCs, (t) force transition-based
|
|
acceptance.
|
|
-H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. 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, (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
|
|
-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 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=), various
|
|
statistics (=--stats=), or nothing at all (=--quiet=). It may seem
|
|
strange to ask a tool to not output anything, but it makes sense when
|
|
only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check
|
|
whether an input automaton has some property) or for timing purposes.
|
|
|
|
* HOA output
|
|
|
|
The [[http://adl.github.io/hoaf/][HOA]] 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. (Details about supported features of the HOA
|
|
format can be found on a [[file:hoa.org][separate page]].)
|
|
|
|
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 two 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,427,231.07",
|
|
fontname=Lato,
|
|
labelloc=t,
|
|
lheight=0.21,
|
|
rankdir=LR
|
|
];
|
|
node [fillcolor="#ffffa0",
|
|
fontname=Lato,
|
|
label="\\N",
|
|
shape=circle,
|
|
style=filled
|
|
];
|
|
edge [fontname=Lato];
|
|
subgraph cluster {
|
|
graph [bb="",
|
|
fontname=Lato,
|
|
label=<(Gb | F!a) W c>,
|
|
labelloc=t,
|
|
lheight=0.21,
|
|
lp="197.5,196.66",
|
|
lwidth=1.19,
|
|
rankdir=LR
|
|
];
|
|
node [fillcolor="#ffffa0",
|
|
fontname=Lato,
|
|
height="",
|
|
label="\\N",
|
|
pos="",
|
|
shape=circle,
|
|
style=filled,
|
|
width=""
|
|
];
|
|
edge [fontname=Lato,
|
|
label="",
|
|
lp="",
|
|
pos=""
|
|
];
|
|
I [height=0.013889,
|
|
label="",
|
|
pos="1,49.168",
|
|
style=invis,
|
|
width=0.013889];
|
|
1 [height=0.5,
|
|
label=1,
|
|
pos="56,49.168",
|
|
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<br/><font color="#5DA5DA">⓿</font>>,
|
|
lp="56,100.32",
|
|
pos="e,62.379,66.362 49.621,66.362 48.319,76.182 50.445,85.324 56,85.324 59.472,85.324 61.604,81.753 62.398,76.677"];
|
|
0 [height=0.5,
|
|
label=0,
|
|
pos="190,121.17",
|
|
width=0.5];
|
|
1 -> 0 [label=<a & b & !c>,
|
|
lp="123,113.83",
|
|
pos="e,172.99,115.19 70.127,60.572 76.491,65.727 84.391,71.704 92,76.324 115.21,90.42 143.57,103.1 163.61,111.38"];
|
|
2 [height=0.5,
|
|
label=2,
|
|
pos="190,34.168",
|
|
width=0.5];
|
|
1 -> 2 [label=<a & !c>,
|
|
lp="123,64.824",
|
|
pos="e,175.09,44.492 73.8,53.268 93.402,57.17 126.62,61.596 154,54.324 158.19,53.213 162.39,51.47 166.37,49.467"];
|
|
3 [height=0.5,
|
|
label=3,
|
|
pos="377,34.168",
|
|
width=0.5];
|
|
1 -> 3 [label=<c>,
|
|
lp="242,9.8246",
|
|
pos="e,361.03,25.984 66.027,34.327 72.161,25.632 81.127,15.423 92,10.325 114.02,0 277.48,0.3418 312,7.3246 325.76,10.108 340.24,15.943 351.94,21.478"];
|
|
0 -> 0 [label=<b<br/><font color="#5DA5DA">⓿</font>>,
|
|
lp="190,172.33",
|
|
pos="e,198.98,137.24 181.02,137.24 178.68,147.48 181.67,157.33 190,157.33 195.47,157.33 198.63,153.08 199.5,147.28"];
|
|
2 -> 1 [label=<!a & !c<br/><font color="#5DA5DA">⓿</font>>,
|
|
lp="123,35.324",
|
|
pos="e,68.596,36.186 173.36,26.591 167.44,24.066 160.55,21.587 154,20.324 126.94,15.113 117.92,10.98 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"];
|
|
2 -> 2 [label=<a & !c>,
|
|
lp="190,77.824",
|
|
pos="e,198.98,50.24 181.02,50.24 178.68,60.475 181.67,70.324 190,70.324 195.47,70.324 198.63,66.083 199.5,60.274"];
|
|
2 -> 3 [label=<!a & c>,
|
|
lp="294,105.83",
|
|
pos="e,365.94,48.712 203.15,46.686 218.52,61.348 246.56,84.98 276,94.324 291.25,99.165 297.12,100.21 312,94.324 331.12,86.764 347.87,70.495 359.43,56.803"];
|
|
4 [height=0.5,
|
|
label=4,
|
|
pos="294,34.168",
|
|
width=0.5];
|
|
2 -> 4 [label=<a & c>,
|
|
lp="242,41.824",
|
|
pos="e,275.95,34.324 208.3,34.324 224.08,34.324 247.64,34.324 265.91,34.324"];
|
|
3 -> 3 [label=<1<br/><font color="#5DA5DA">⓿</font>>,
|
|
lp="377,85.324",
|
|
pos="e,384.03,50.989 369.97,50.989 368.41,60.949 370.75,70.324 377,70.324 381,70.324 383.4,66.477 384.2,61.093"];
|
|
4 -> 3 [label=<!a>,
|
|
lp="335.5,41.824",
|
|
pos="e,358.85,34.324 312.18,34.324 322.81,34.324 336.69,34.324 348.8,34.324"];
|
|
4 -> 4 [label=<a>,
|
|
lp="294,77.824",
|
|
pos="e,301.03,50.989 286.97,50.989 285.41,60.949 287.75,70.324 294,70.324 298,70.324 300.4,66.477 301.2,61.093"];
|
|
}
|
|
subgraph cluster_gv1 {
|
|
graph [bb="",
|
|
fontname=Lato,
|
|
label=<a U b>,
|
|
labelloc=t,
|
|
lheight=0.21,
|
|
lp="81.5,88.5",
|
|
lwidth=0.47,
|
|
rankdir=LR
|
|
];
|
|
node [fillcolor="#ffffa0",
|
|
fontname=Lato,
|
|
height="",
|
|
label="\\N",
|
|
peripheries="",
|
|
pos="",
|
|
shape=circle,
|
|
style=filled,
|
|
width=""
|
|
];
|
|
edge [fontname=Lato,
|
|
label="",
|
|
lp="",
|
|
pos=""
|
|
];
|
|
I_gv1 [height=0.013889,
|
|
label="",
|
|
pos="261,156.17",
|
|
style=invis,
|
|
width=0.013889];
|
|
"1_gv1" [height=0.5,
|
|
label=1,
|
|
pos="316,156.17",
|
|
width=0.5];
|
|
I_gv1 -> "1_gv1" [pos="e,297.94,156.17 261.15,156.17 262.67,156.17 275.1,156.17 287.63,156.17"];
|
|
"1_gv1" -> "1_gv1" [label=<a & !b>,
|
|
lp="316,199.67",
|
|
pos="e,322.38,173.21 309.62,173.21 308.32,183.03 310.44,192.17 316,192.17 319.47,192.17 321.6,188.6 322.4,183.52"];
|
|
"0_gv1" [height=0.72222,
|
|
label=0,
|
|
peripheries=2,
|
|
pos="401,156.17",
|
|
width=0.72222];
|
|
"1_gv1" -> "0_gv1" [label=<b>,
|
|
lp="356.5,163.67",
|
|
pos="e,379,156.17 334.2,156.17 344.16,156.17 357,156.17 368.7,156.17"];
|
|
"0_gv1" -> "0_gv1" [label=1,
|
|
lp="401,203.67",
|
|
pos="e,409.01,176.75 392.99,176.75 391.89,187.01 394.55,196.17 401,196.17 405.13,196.17 407.71,192.41 408.74,187.01"];
|
|
}
|
|
}
|
|
#+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]] supports 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 { /* a U b */
|
|
: T0_init:
|
|
: if
|
|
: :: ((b)) -> goto accept_all
|
|
: :: ((a) && (!(b))) -> goto T0_init
|
|
: fi;
|
|
: accept_all:
|
|
: skip
|
|
: }
|
|
|
|
Recent versions of Spin (starting with Spin 6.2.4) output never claims
|
|
in a slightly different style that can be requested using either
|
|
=-s6= or =--spin=6=:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltl2tgba -s6 'a U b'
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: never { /* a U b */
|
|
: T0_init:
|
|
: do
|
|
: :: atomic { ((b)) -> assert(!((b))) }
|
|
: :: ((a) && (!(b))) -> goto T0_init
|
|
: od;
|
|
: accept_all:
|
|
: skip
|
|
: }
|
|
|
|
(Note that while Spot is able to read never claims that follow any of
|
|
these two styles, it is not capable of interpreting an arbitrary piece
|
|
of Promela syntax.)
|
|
|
|
* 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 code
|
|
ltl2tgba '(Ga -> Gb) W c'
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot=
|
|
#+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
|
|
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot= | 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, =n= causes the
|
|
name (see below) of the automaton to be displayed, and =a= causes the
|
|
acceptance condition to be shown as well. Option =b= causes sets to
|
|
be ouput as bullets (e.g., ⓿ instead of ={0}=); option =r= (for
|
|
rainbow) causes sets to be displayed in different colors, while option
|
|
=R= also uses colors, but it chooses them depending on whether a set
|
|
is used with Fin-acceptance, Inf-acceptance, or both. Finally option
|
|
=f(FONT)= is used to select a fontname: it is often necessary when =b=
|
|
is used to ensure the characters ⓿, ❶, etc. are all selected from the
|
|
same font.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
digraph G {
|
|
label="(Gb | F!a) W c\nInf(0)"
|
|
labelloc="t"
|
|
node [shape="circle"]
|
|
node[style=filled, fillcolor="#ffffa0"]
|
|
I [label="", style=invis, height=0]
|
|
I -> 1
|
|
subgraph cluster_0 {
|
|
color=green
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_1 {
|
|
color=green
|
|
label=""
|
|
3 [label="3"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=red
|
|
label=""
|
|
4 [label="4"]
|
|
}
|
|
subgraph cluster_3 {
|
|
color=green
|
|
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
|
|
|
|
#+NAME: oaut-dot2
|
|
#+BEGIN_SRC sh :results verbatim :exports none
|
|
SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
|
|
#+END_SRC
|
|
|
|
#+RESULTS: oaut-dot2
|
|
#+begin_example
|
|
digraph G {
|
|
label="(Gb | F!a) W c\\nInf(0)"
|
|
labelloc="t"
|
|
node [shape="circle"]
|
|
I [label="", style=invis, height=0]
|
|
I -> 1
|
|
subgraph cluster_0 {
|
|
color=green
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_1 {
|
|
color=green
|
|
label=""
|
|
3 [label="3"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=red
|
|
label=""
|
|
4 [label="4"]
|
|
}
|
|
subgraph cluster_3 {
|
|
color=green
|
|
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]]
|
|
|
|
The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA
|
|
format]]. Here =Inf(0)= means that runs are accepting if and only if
|
|
they visit some the transitions in the set #0 infinitely often.
|
|
|
|
The strongly connected components are displayed using the following colors:
|
|
- *green* components contain an accepting cycle
|
|
- *red* components contain no accepting cycle
|
|
- *black* components are trivial (i.e., they contain no cycle)
|
|
- *gray* components are useless (i.e., they are non-accepting, and are only followed by non-accepting components)
|
|
|
|
Here is an example involving all colors:
|
|
|
|
#+NAME: oaut-dot3
|
|
#+BEGIN_SRC sh :results verbatim :exports none
|
|
SPOT_DOTEXTRA= autfilt --dot=cas <<EOF | sed 's/\\/\\\\/'
|
|
HOA: v1
|
|
States: 10
|
|
Start: 1
|
|
AP: 2 "a" "b"
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 3 Inf(0)&Inf(1)&Fin(2)
|
|
--BODY--
|
|
State: 0 {2}
|
|
[0&1] 0 {0 1}
|
|
[!0&!1] 0
|
|
[0] 5
|
|
State: 1
|
|
[1] 4
|
|
[0&!1] 3
|
|
State: 4
|
|
[!1] 4 {1 2}
|
|
[1] 2
|
|
State: 2
|
|
[0] 0
|
|
[1] 7
|
|
State: 3
|
|
[0&1] 1 {1 0}
|
|
State: 5
|
|
[t] 6 {1}
|
|
State: 6
|
|
[t] 5
|
|
State: 7
|
|
[!0&1] 7 {0 2}
|
|
[0&1] 7 {0 1}
|
|
[t] 8
|
|
State: 8
|
|
[!0&1] 8 {0 2}
|
|
[0&1] 9 {0 1}
|
|
State: 9
|
|
[!0&1] 8 {0 1}
|
|
[0&1] 9 {0 2}
|
|
--END--
|
|
EOF
|
|
#+END_SRC
|
|
|
|
#+RESULTS: oaut-dot3
|
|
#+begin_example
|
|
digraph G {
|
|
rankdir=LR
|
|
label="Fin(2) & (Inf(0)&Inf(1))"
|
|
labelloc="t"
|
|
node [shape="circle"]
|
|
I [label="", style=invis, width=0]
|
|
I -> 1
|
|
subgraph cluster_0 {
|
|
color=grey
|
|
label=""
|
|
5 [label="5"]
|
|
6 [label="6"]
|
|
}
|
|
subgraph cluster_1 {
|
|
color=grey
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=green
|
|
label=""
|
|
8 [label="8"]
|
|
9 [label="9"]
|
|
}
|
|
subgraph cluster_3 {
|
|
color=green
|
|
label=""
|
|
7 [label="7"]
|
|
}
|
|
subgraph cluster_4 {
|
|
color=black
|
|
label=""
|
|
2 [label="2"]
|
|
}
|
|
subgraph cluster_5 {
|
|
color=red
|
|
label=""
|
|
4 [label="4"]
|
|
}
|
|
subgraph cluster_6 {
|
|
color=green
|
|
label=""
|
|
1 [label="1"]
|
|
3 [label="3"]
|
|
}
|
|
0 -> 0 [label="a & b\\n{0,1,2}"]
|
|
0 -> 0 [label="!a & !b\\n{2}"]
|
|
0 -> 5 [label="a\\n{2}"]
|
|
1 -> 4 [label="b"]
|
|
1 -> 3 [label="a & !b"]
|
|
2 -> 0 [label="a"]
|
|
2 -> 7 [label="b"]
|
|
3 -> 1 [label="a & b\\n{0,1}"]
|
|
4 -> 4 [label="!b\\n{1,2}"]
|
|
4 -> 2 [label="b"]
|
|
5 -> 6 [label="1\\n{1}"]
|
|
6 -> 5 [label="1"]
|
|
7 -> 7 [label="!a & b\\n{0,2}"]
|
|
7 -> 7 [label="a & b\\n{0,1}"]
|
|
7 -> 8 [label="1"]
|
|
8 -> 8 [label="!a & b\\n{0,2}"]
|
|
8 -> 9 [label="a & b\\n{0,1}"]
|
|
9 -> 8 [label="!a & b\\n{0,1}"]
|
|
9 -> 9 [label="a & b\\n{0,2}"]
|
|
}
|
|
#+end_example
|
|
|
|
#+BEGIN_SRC dot :file oaut-dot3.png :cmdline -Tpng :var txt=oaut-dot3 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:oaut-dot3.png]]
|
|
|
|
<<default-dot>>
|
|
|
|
The dot output can also be customized via two environment variables:
|
|
- =SPOT_DOTDEFAULT= contains default arguments for the =--dot= option
|
|
(for when it is used implicitly, or used as just =--dot= without
|
|
argument). For instance after =export SPOT_DOTDEFAULT=vcsn=, using
|
|
=--dot= is equivalent to =--dot=vcsn=. However using =--dot=xyz=
|
|
(for any value of =xyz=, even empty) will ignore the
|
|
=SPOT_DOTDEFAULT= variable. If the argument of =--dot= contains
|
|
a dot character, then this dot is replaced by the contents of
|
|
=SPOT_DOTDEFAULT=. So ~--dot=.a~ would be equivalent to =--dot=vcsna=
|
|
with our example definition of =SPOT_DOTDEFAULT=.
|
|
- =SPOT_DOTEXTRA= may contains an arbitrary string that will be emitted
|
|
in the dot output before the first state. This can be used to modify
|
|
any attribute. For instance (except for this page, where we had
|
|
do demonstrate the various options of =--dot=, and a few pages where
|
|
we show the =--dot= output verbatim) all the automata displayed in
|
|
this documentation are generated with the following environment
|
|
variables set:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
export SPOT_DOTDEFAULT='Brf(Lato)'
|
|
export SPOT_DOTEXTRA='node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]'
|
|
#+END_SRC
|
|
|
|
* 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 1000 random automata with 100 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 -d0.2 -Q100 -n1000 a --stats %e > size.csv
|
|
R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))"
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: edges
|
|
: Min. :1939
|
|
: 1st Qu.:2056
|
|
: Median :2083
|
|
: Mean :2082
|
|
: 3rd Qu.:2107
|
|
: Max. :2233
|
|
|
|
For $Q=100$ states and density $D=0.2$ the expected degree of each
|
|
state is $1+(Q-1)D = 1+99\times 0.2 = 20.8$, so the expected number of
|
|
edges should be $20.8\times100=2080$.
|
|
|
|
* 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=.
|
|
|
|
#+NAME: oaut-name
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba --name='TGBA for %f' --dot=n 'a U b'
|
|
#+END_SRC
|
|
|
|
#+RESULTS: oaut-name
|
|
#+begin_example
|
|
digraph G {
|
|
rankdir=LR
|
|
label="TGBA for a U b"
|
|
labelloc="t"
|
|
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
|
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)
|
|
|
|
Note that the above result can also be obtained without using
|
|
=autfilt= and automata names. We can use the fact that =ltl2tgba
|
|
--stats= can output the automaton size, and that =ltl2tgba= is also
|
|
capable of [[file:csv.org][reading from a CSV file]] (=-F-/2= instructs =ltl2tgba= to
|
|
read the standard input as if it was a CSV file, and to process its
|
|
second column):
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
randltl -n -1 a b | # generate a stream of random LTL formulas
|
|
ltl2tgba -F- --stats='%s,!(%f)' | # for each formula output "states,negated formula"
|
|
grep '^3,' | # keep only formulas with 3 states
|
|
ltl2tgba -F-/2 --stats='%s,%f' | # for each negated formula output "states,formula"
|
|
grep '^3,' | # keep only negated formulas with 3 states
|
|
head -n5 | cut -d, -f2 # return the five first formulas
|
|
#+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
|
|
* Naming output
|
|
|
|
By default, all output is sent to standard output, so you can either
|
|
redirect it to a file, or pipe it to another program.
|
|
You can also use the =--output= (a.k.a. =-o=) option to specify a
|
|
filename where automata should be written. The advantage over
|
|
a shell redirection, is that you may build a name using the same
|
|
escape sequences as used by =--stats= and =--name=.
|
|
|
|
For instance =%d= is replaced by 0 or 1 depending on whether the
|
|
automaton is deterministic. We can generate 20 random automata, and
|
|
output them in two files depending on their determinism:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
randaut -n 20 -Q2 -d1 1 -H -o out-det%d.hoa
|
|
autfilt -c out-det0.hoa # Count of non-deterministic automata
|
|
autfilt -c out-det1.hoa # Count of deterministic automata
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: 14
|
|
: 6
|
|
|
|
If you use this feature, beware that the output filename
|
|
is only truncated by the first file that is output to it: so
|
|
if no automaton generate some filename, the existing file
|
|
will be left untouched. For instance we we run the above
|
|
commands, again, but forcing [[file:randaut.org][=randaut=]] to output 20
|
|
deterministic automata, it may look like we produced more
|
|
than 20 automata:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
randaut -D -n 20 -Q2 -d1 1 -H -o out-det%d.hoa
|
|
autfilt -c out-det0.hoa # Count of non-deterministic automata
|
|
autfilt -c out-det1.hoa # Count of deterministic automata
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: 14
|
|
: 20
|
|
|
|
This is because the =out-det0.hoa= file hasn't changed from the
|
|
previous execution, while =out-det1.hoa= has been overwritten.
|
|
|
|
In the case where you want to append to a file instead of overwriting
|
|
it, prefix the output filename with =>>= as in
|
|
|
|
: randaut -D -n 20 -Q2 1 -H -o '>>out-det%d.hoa'
|
|
|
|
(You need the quotes so that the shell does not interpret '>>'.)
|