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