cb9867b7d4
* doc/org/oaut.org: Adjust the parameters of randaut so that we get a mix of deterministic and nondeterministic automata.
1040 lines
28 KiB
Org Mode
1040 lines
28 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[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters for (a)
|
|
acceptance display, (c) circular nodes, (h)
|
|
horizontal layout, (v) vertical layout, (n) with
|
|
name, (N) without name, (s) with SCCs, (t) force
|
|
transition-based acceptance.
|
|
-H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters
|
|
to select (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.
|
|
|
|
* 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 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,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]] 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 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, =n= causes the
|
|
name (see below) of the automaton to be displayed, and =a= causes the
|
|
acceptance condition to be shown as well.
|
|
|
|
#+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"]
|
|
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
|
|
ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
|
|
#+END_SRC
|
|
|
|
#+RESULTS: oaut-dot2
|
|
#+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=orange
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=orange
|
|
label=""
|
|
9 [label="9"]
|
|
10 [label="10"]
|
|
}
|
|
subgraph cluster_3 {
|
|
color=green
|
|
label=""
|
|
8 [label="8"]
|
|
}
|
|
subgraph cluster_4 {
|
|
color=green
|
|
label=""
|
|
7 [label="7"]
|
|
}
|
|
subgraph cluster_5 {
|
|
color=black
|
|
label=""
|
|
2 [label="2"]
|
|
}
|
|
subgraph cluster_6 {
|
|
color=red
|
|
label=""
|
|
4 [label="4"]
|
|
}
|
|
subgraph cluster_7 {
|
|
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"]
|
|
6 -> 5 [label="1"]
|
|
7 -> 7 [label="!a & b\\n{0,1}"]
|
|
7 -> 7 [label="a & b\\n{0,2}"]
|
|
7 -> 8 [label="1"]
|
|
8 -> 8 [label="!a & b\\n{0,2}"]
|
|
8 -> 8 [label="a & b\\n{0,1}"]
|
|
8 -> 9 [label="1"]
|
|
9 -> 9 [label="!a & b\\n{0,2}"]
|
|
9 -> 10 [label="a & b\\n{0,1}"]
|
|
10 -> 9 [label="!a & b\\n{0,1}"]
|
|
10 -> 10 [label="a & b\\n{0,2}"]
|
|
}
|
|
#+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
|
|
- *orange* components may or may not contain an accepting cycle. Such an indecision occur only when using =Fin= acceptance primitive, deciding that would require a better algorithm than what the output routine is using.
|
|
- *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
|
|
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=orange
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=orange
|
|
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]]
|
|
|
|
* 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)
|
|
|
|
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 -S2 -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 -S2 -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 -S2 1 -H -o '>>out-det%d.hoa'
|
|
|
|
(You need the quotes so that the shell does not interpret '>>'.)
|