adjust documentation for the merge of the dstar parser
* NEWS: Mention the changes. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltlcross.org, doc/org/tools.org, doc/org/tut20.org, src/bin/man/dstar2tgba.x, src/bin/man/ltlcross.x: Adjust documentation. * src/bin/common_trans.cc: Use %O instead of %D, but keep %D hidden for backward compatibility.
This commit is contained in:
Alexandre Duret-Lutz
parent
c59e994a2c
commit
17a18f2890
9 changed files with 357 additions and 173 deletions
10
NEWS
10
NEWS
|
|
@ -5,6 +5,16 @@ New in spot 1.99.3a (not yet released)
|
|||
exactly one acceptance sets. This is useful when targeting parity
|
||||
acceptance.
|
||||
|
||||
* the parser for ltl2dstar's format has been merged with the parser
|
||||
for the other automata formats. This implies two things:
|
||||
- autfilt and dstar2tgba (despite its name) can now both read
|
||||
automata written in any of the four supported syntaxes
|
||||
(ltl2dstar's, lbtt's, HOA, never claim).
|
||||
- "dstar2tgba some files..." now behaves exactly like
|
||||
"autfilt --tgba --high --small some files...".
|
||||
(But dstar2tgba does not offer all the filtering and
|
||||
transformations options of autfilt.)
|
||||
|
||||
New in spot 1.99.3 (2015-08-26)
|
||||
|
||||
* The CGI script for LTL translation offers a HOA download link
|
||||
|
|
|
|||
|
|
@ -20,9 +20,12 @@ filtering.
|
|||
* Conversion between formats
|
||||
|
||||
=autfilt= can read automata written in the [[http://adl.github.io/hoaf/][Hanoi Omega Automata
|
||||
Format]], as [[http://spinroot.com/spin/Man/never.html][Spin never claims]], or using [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]]. Automata in
|
||||
those formats (even a mix of those formats) can be concatenated in the
|
||||
same stream, =autfilt= will process them in batch.
|
||||
Format]], as [[http://spinroot.com/spin/Man/never.html][Spin never claims]], using [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], or using
|
||||
[[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dstar='s format]]. Automata in those formats (even a mix of those
|
||||
formats) can be concatenated in the same stream, =autfilt= will
|
||||
process them in batch. (The only restriction is that inside a file an
|
||||
automaton in LBTT's format may not follow an automaton in
|
||||
=ltl2dstar='s format.)
|
||||
|
||||
The output format can be controlled using [[file:oaut.org][the common output options]]
|
||||
(like =--spin=, =--lbtt=, =--dot=, =--hoaf=...).
|
||||
|
|
|
|||
|
|
@ -3,12 +3,17 @@
|
|||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
|
||||
This tool converts deterministic Rabin and Streett automata, presented
|
||||
in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]], into Büchi automata.
|
||||
This tool converts automata into transition-based generalized Büchi
|
||||
automata, a.k.a., TGBA.
|
||||
|
||||
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=]], hence its
|
||||
name. 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).
|
||||
|
||||
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 deterministic Rabin or Streett automaton to convert.
|
||||
containing the automaton to convert.
|
||||
|
||||
* Two quick examples
|
||||
|
||||
|
|
@ -18,18 +23,18 @@ Here are some brief examples before we discuss the behavior of
|
|||
** From Rabin to Büchi
|
||||
|
||||
The following command instructs =ltl2dstar= to:
|
||||
1. run =ltl2tgba -sD= to build a Büchi automaton for =Fa & GFb=, and then
|
||||
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 'Fa & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - fagfb
|
||||
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 3-state DRA:
|
||||
produced a 4-state DRA:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
cat fagfb
|
||||
|
|
@ -38,64 +43,87 @@ cat fagfb
|
|||
#+begin_example
|
||||
DRA v2 explicit
|
||||
Comment: "Safra[NBA=3]"
|
||||
States: 3
|
||||
States: 4
|
||||
Acceptance-Pairs: 1
|
||||
Start: 1
|
||||
Start: 2
|
||||
AP: 2 "a" "b"
|
||||
---
|
||||
State: 0
|
||||
Acc-Sig: +0
|
||||
2
|
||||
2
|
||||
3
|
||||
3
|
||||
0
|
||||
0
|
||||
State: 1
|
||||
Acc-Sig:
|
||||
Acc-Sig: -0
|
||||
1
|
||||
1
|
||||
1
|
||||
0
|
||||
1
|
||||
0
|
||||
State: 2
|
||||
Acc-Sig:
|
||||
1
|
||||
2
|
||||
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=) in [[http://www.graphviz.org/][GraphViz]]'s format:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
dstar2tgba -B fagfb
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
SPOT_DOTEXTRA= dstar2tgba -B fagfb --dot=
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
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="a"]
|
||||
1 -> 1 [label="!a"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="b"]
|
||||
2 -> 2 [label="!b"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
Which can be rendered as (note that in this documentation
|
||||
we use some [[file:oaut.org][environment variables]] to produce a more colorful
|
||||
output by default):
|
||||
For instance here is the conversion to a Büchi automaton (=-B=):
|
||||
|
||||
#+NAME: fagfb2ba
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
|
|
@ -105,19 +133,20 @@ dstar2tgba -B fagfb
|
|||
#+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<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 [label="0", peripheries=2]
|
||||
0 -> 0 [label=<b>]
|
||||
0 -> 2 [label=<!b>]
|
||||
1 [label=<1>]
|
||||
1 -> 0 [label=<a>]
|
||||
1 -> 1 [label=<!a>]
|
||||
2 [label=<2>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<b>]
|
||||
1 -> 1 [label=<a & !b>]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label=<b>]
|
||||
2 -> 2 [label=<!b>]
|
||||
}
|
||||
|
|
@ -129,7 +158,11 @@ $txt
|
|||
#+RESULTS:
|
||||
[[file:fagfb2ba.png]]
|
||||
|
||||
But we could as well require the output to be output as a never claim for Spin (option =-s=):
|
||||
|
||||
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
|
||||
|
|
@ -139,18 +172,18 @@ dstar2tgba -s fagfb
|
|||
never {
|
||||
T0_init:
|
||||
if
|
||||
:: ((!(a))) -> goto T0_init
|
||||
:: ((a)) -> goto accept_S2
|
||||
:: ((b)) -> goto accept_S0
|
||||
:: ((a) && (!(b))) -> goto T0_init
|
||||
fi;
|
||||
accept_S2:
|
||||
accept_S0:
|
||||
if
|
||||
:: ((b)) -> goto accept_S2
|
||||
:: ((!(b))) -> goto T0_S3
|
||||
:: ((b)) -> goto accept_S0
|
||||
:: ((!(b))) -> goto T0_S2
|
||||
fi;
|
||||
T0_S3:
|
||||
T0_S2:
|
||||
if
|
||||
:: ((b)) -> goto accept_S2
|
||||
:: ((!(b))) -> goto T0_S3
|
||||
:: ((b)) -> goto accept_S0
|
||||
:: ((!(b))) -> goto T0_S2
|
||||
fi;
|
||||
}
|
||||
#+end_example
|
||||
|
|
@ -160,50 +193,62 @@ T0_S3:
|
|||
:CUSTOM_ID: streett_to_tgba_example
|
||||
:END:
|
||||
|
||||
Here is the translation of =GFa & GFb= to a 4-state Streett automaton:
|
||||
Here is the translation of =GFa | GFb= to a 4-state Streett automaton:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+NAME: gfafgb
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
|
||||
cat gfagfb
|
||||
autfilt --dot=.a gfagfb
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
|
||||
#+RESULTS: gfafgb
|
||||
#+begin_example
|
||||
DSA v2 explicit
|
||||
Comment: "Streett{Union{Safra[NBA=2],Safra[NBA=2]}}"
|
||||
States: 4
|
||||
Acceptance-Pairs: 2
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
---
|
||||
State: 0
|
||||
Acc-Sig: -0 -1
|
||||
3
|
||||
2
|
||||
1
|
||||
0
|
||||
State: 1
|
||||
Acc-Sig: +0 -1
|
||||
3
|
||||
2
|
||||
1
|
||||
0
|
||||
State: 2
|
||||
Acc-Sig: -0 +1
|
||||
3
|
||||
2
|
||||
1
|
||||
0
|
||||
State: 3
|
||||
Acc-Sig: +0 +1
|
||||
3
|
||||
2
|
||||
1
|
||||
0
|
||||
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
|
||||
|
||||
And now its conversion by =dstar2tgba= to a 2-state Büchi automaton.
|
||||
We don't pass any option to =dstar2tgba= because converting to TGBA in
|
||||
GraphViz's format is the default:
|
||||
#+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
|
||||
|
|
@ -213,6 +258,7 @@ dstar2tgba gfagfb
|
|||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
|
|
@ -220,12 +266,25 @@ digraph G {
|
|||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 1 [label=<1>]
|
||||
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 -> 1 [label=<!a & !b>]
|
||||
1 -> 1 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
1 -> 0 [label=<a & b<br/><font color="#F17CB0">❶</font>>]
|
||||
1 -> 1 [label=<!a & b<br/><font color="#F17CB0">❶</font>>]
|
||||
1 -> 1 [label=<a & b<br/><font color="#5DA5DA">⓿</font><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
|
||||
|
||||
|
|
@ -235,20 +294,25 @@ $txt
|
|||
#+RESULTS:
|
||||
[[file:gfagfb2ba.png]]
|
||||
|
||||
(Obviously the resulting automaton could be simplified further, by
|
||||
starting with the second state right away.)
|
||||
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 implement a 4-step process:
|
||||
The =dstar2tgba= tool implements a 4-step process:
|
||||
|
||||
1. read the DRA/DSA
|
||||
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 can 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.
|
||||
|
|
@ -301,18 +365,35 @@ dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
|
|||
#+begin_example
|
||||
-8, --utf8 enable UTF-8 characters in output (ignored with
|
||||
--lbtt or --spin)
|
||||
--dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose
|
||||
(c) circular nodes, (h) horizontal layout, (v)
|
||||
vertical layout, (n) with name, (N) without name,
|
||||
(s) with SCCs, (t) always transition-based
|
||||
acceptance.
|
||||
-H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters
|
||||
to select (s) state-based acceptance, (t)
|
||||
transition-based acceptance, (m) mixed acceptance,
|
||||
(l) single-line output
|
||||
--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', or 'stutter-invariant'.
|
||||
--dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v]
|
||||
GraphViz's format (default). 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.
|
||||
-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
|
||||
|
|
@ -358,7 +439,7 @@ done
|
|||
#+RESULTS:
|
||||
#+begin_example
|
||||
(b | Fa) R Fc
|
||||
DRA: 9st.; BA: 6st.; det.? 1; complete? 1
|
||||
DRA: 9st.; BA: 9st.; det.? 1; complete? 1
|
||||
Ga U (Gc R (!a | Gc))
|
||||
DRA: 7st.; BA: 7st.; det.? 0; complete? 0
|
||||
GFc
|
||||
|
|
@ -368,7 +449,7 @@ GFc
|
|||
Xc R (G!c R (b | G!c))
|
||||
DRA: 4st.; BA: 2st.; det.? 1; complete? 0
|
||||
c & G(b | F(a & c))
|
||||
DRA: 5st.; BA: 3st.; det.? 1; complete? 0
|
||||
DRA: 4st.; BA: 3st.; det.? 1; complete? 0
|
||||
XXFc
|
||||
DRA: 4st.; BA: 4st.; det.? 1; complete? 1
|
||||
XFc | Gb
|
||||
|
|
@ -388,11 +469,46 @@ 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 from Rabin and Streett to TGBA
|
||||
** Conversion of various acceptance conditions to TGBA and BA
|
||||
|
||||
The algorithms used to convert Rabin and Streett into TGBA/BA are different.
|
||||
Spot implements several acceptance conversion algorithms.
|
||||
There is one generic cases, with some specialized variants.
|
||||
|
||||
*** Rabin to BA
|
||||
*** 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"
|
||||
|
|
@ -402,14 +518,21 @@ 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: any DRA
|
||||
will be converted into a BA, and the determinism will be conserved
|
||||
only in strongly connected components where determinism can be
|
||||
conserved.
|
||||
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 automata are converted into non-deterministic 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.
|
||||
|
|
|
|||
|
|
@ -55,12 +55,13 @@ following character sequences:
|
|||
ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: %% a single %
|
||||
: %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin,
|
||||
: LBT, or Wring's syntax
|
||||
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
|
||||
: Wring's syntax
|
||||
: %O,%D the automaton is output as either (%O) HOA/never
|
||||
: claim/LBTT, or (%D) in LTL2DSTAR's format
|
||||
: %O the automaton is output in HOA, never claim, LBTT,
|
||||
: or ltl2dstar's format
|
||||
|
||||
For instance here is how we could cross-compare the never claims
|
||||
output by =spin= and =ltl2tgba= for the formulas =GFa= and =X(a U b)=.
|
||||
|
|
@ -100,27 +101,21 @@ No problem detected.
|
|||
=ltlcross= can only read four kinds of output:
|
||||
- Never claims (only if they are restricted to representing an
|
||||
automaton using =if=, =goto=, and =skip= statements) such as those
|
||||
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. These
|
||||
should be indicated using =%O=. The newer syntax introduced by
|
||||
Spin 6.24, using =do= instead of =if=, is also supported.
|
||||
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. The
|
||||
newer syntax introduced by Spin 6.24, using =do= instead of =if=,
|
||||
is also supported.
|
||||
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with
|
||||
either state-based acceptance or transition-based acceptance.
|
||||
This output is used for instance by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][=lbt=]], [[http://web.archive.org/web/20080607170403/http://www.science.unitn.it/~stonetta/modella.html][=modella=]], or =ltl2tgba
|
||||
--lbtt=. These should also be indicated using =%O=.
|
||||
--lbtt=.
|
||||
- Non-alternating automata in [[file:http://adl.github.io/hoaf/][the HOA format]] with an acceptance
|
||||
condition that is is generalized-Büchi or inferior. These
|
||||
should also be indicated using =%O=.
|
||||
condition that is is generalized-Büchi or inferior.
|
||||
- [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dstar='s format]], which supports deterministic Rabin or Streett
|
||||
automata. After =ltlcross= reads such input, it immediately
|
||||
converts it into a Büchi automaton. Rabin automata are converted
|
||||
to (degeneralized) Büchi automata and the conversion will preserve
|
||||
the determinism anytime a deterministic Büchi automaton exists for
|
||||
that property (this determinism is good for the complemented
|
||||
intersection check discussed below). Streett automata are
|
||||
converted to non-deterministic TGBA, where generalized acceptance
|
||||
conditions are used to reduce the size of the automaton you would
|
||||
get by the classical conversion from Streett to Büchi.
|
||||
This kind of output (Rabin or Streett) should be indicated with =%D=.
|
||||
automata.
|
||||
|
||||
Files in any of these format should be indicated with =%O=. (Past
|
||||
versions of =ltlcross= used different letters for each format, but the
|
||||
four parsers have been merged into a single one.)
|
||||
|
||||
Of course all configured tools need not use the same =%= sequences.
|
||||
The following list shows some typical configurations for some existing
|
||||
|
|
@ -144,18 +139,18 @@ tools:
|
|||
- '~ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD --automata=streett
|
||||
--output-format=hoa %L %O~' deterministic Streett output in HOA,
|
||||
as supported since version 0.5.2 of =ltl2dstar=.
|
||||
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D=' (Rabin
|
||||
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %O=' (Rabin
|
||||
output in DSTAR format, as supported in older versions of
|
||||
=ltl2dstar=.
|
||||
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba
|
||||
-s >%O=' (external conversion from Rabin to Büchi done by
|
||||
=dstar2tgba= for more reduction of the Büchi automaton than what
|
||||
=ltlcross= would provide)
|
||||
- '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer
|
||||
uses the last =%D= argument as a prefix to which it always append =.dst=,
|
||||
so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file)
|
||||
- '=java -jar Rabinizer3.jar -hoa -formula %f; mv output.hoa %O=' (Rabinizer *3*
|
||||
always output in =output.hoa= when the formula comes from the command line.)
|
||||
- '=java -jar Rabinizer.jar -ltl2dstar %F %O; mv %O.dst %O=' (Rabinizer
|
||||
uses the last =%O= argument as a prefix to which it always append =.dst=,
|
||||
so we have to rename =%O.dst= as =%O= so that =ltlcross= can find the file)
|
||||
- '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %f >%O~'
|
||||
(rabinizer 3.1 can output automata in the HOA format)
|
||||
- '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl2dra=.)
|
||||
|
||||
To simplify the use of some of the above tools, a set of predefined
|
||||
|
|
@ -631,7 +626,7 @@ positive and negative formulas by the ith translator).
|
|||
coverage. Using '=ltl2tgba -lD %f >%O=' will produce
|
||||
deterministic automata for all obligation properties and many
|
||||
recurrence properties. Using '=ltl2dstar
|
||||
--ltl2nba=spin:pathto/ltl2tgba@-Ds %L %D=' will systematically
|
||||
--ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will systematically
|
||||
produce a deterministic Rabin automaton (that =ltlcross= can
|
||||
complement easily).
|
||||
|
||||
|
|
|
|||
|
|
@ -46,10 +46,10 @@ corresponding commands are hidden.
|
|||
- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-Büchi translators.
|
||||
- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL
|
||||
formula
|
||||
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert deterministic Rabin or Streett automata into
|
||||
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert automata with any acceptance into variants of
|
||||
Büchi automata.
|
||||
- [[file:randaut.org][=randaut=]] Generate random automata.
|
||||
- [[file:autfilt.org][=autfilt=]] Filter and convert automata.
|
||||
- [[file:autfilt.org][=autfilt=]] Filter and transform automata.
|
||||
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
|
||||
and [[file:oaut.org][output]] interfaces.
|
||||
|
||||
|
|
|
|||
|
|
@ -41,10 +41,10 @@ accept_all:
|
|||
and convert this into an automaton in [[file:hoa.org][the HOA format]].
|
||||
|
||||
Note that the automaton parser of Spot can read automata written
|
||||
either as never claims, in LBTT's format or in the HOA format, and
|
||||
there is no need to specify which format you expect. Even if our
|
||||
example use a never claim as input, the code we write will work with
|
||||
any of those formats.
|
||||
either as never claims, in LBTT's format, in ltl2dstar's format or in
|
||||
the HOA format, and there is no need to specify which format you
|
||||
expect. Even if our example uses a never claim as input, the code we
|
||||
write will work with any of those formats.
|
||||
|
||||
* Shell
|
||||
|
||||
|
|
|
|||
|
|
@ -427,9 +427,9 @@ static const argp_option options[] =
|
|||
0 },
|
||||
{ "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
|
||||
{ "%O,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"the automaton is output as either (%O) HOA/never claim/LBTT, or (%D) "
|
||||
"in LTL2DSTAR's format", 0 },
|
||||
{ "%O", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"the automaton is output in HOA, never claim, LBTT, or ltl2dstar's "
|
||||
"format", 0 },
|
||||
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
|
||||
{ 0, 0, 0, 0,
|
||||
"If either %l, %L, or %T are used, any input formula that does "
|
||||
|
|
|
|||
|
|
@ -1,5 +1,62 @@
|
|||
[NAME]
|
||||
dstar2tgba \- convert Rabin or Streett automata into Büchi automata
|
||||
dstar2tgba \- convert automata into Büchi automata
|
||||
[HISTORY]
|
||||
.B dstar2tgba
|
||||
was introduced in Spot 1.2 as a command that reads automata
|
||||
in
|
||||
.BR ltl2dstar 's
|
||||
format, and converts them into TGBA. At this time it was
|
||||
the only command-line tool being able to read automata.
|
||||
.PP
|
||||
In Spot 1.99.1 the
|
||||
.B autfilt
|
||||
command was introduced, but could only read automata
|
||||
in the HOA format, or in
|
||||
.BR lbtt 's
|
||||
format, or as never claims. So
|
||||
.B dstar2tgba
|
||||
was still the only way to process automata
|
||||
in
|
||||
.BR ltl2dstar 's
|
||||
format.
|
||||
.PP
|
||||
In Spot 1.99.4 the parser for
|
||||
.BR ltl2dstar 's
|
||||
format was finally merged with the parser
|
||||
used by
|
||||
.B autfilt
|
||||
for reading the other format. This implies not only
|
||||
that
|
||||
.B autfilt
|
||||
can now read
|
||||
.BR ltl2dstar's
|
||||
format, but also that
|
||||
.B dstar2tgba
|
||||
can read the other formats as well.
|
||||
|
||||
Nowadays, the command
|
||||
.PP
|
||||
.in +4n
|
||||
.nf
|
||||
.ft C
|
||||
% dstar2tgba some files
|
||||
.fi
|
||||
.PP
|
||||
can be used as a shorthand for
|
||||
.PP
|
||||
.in +4n
|
||||
.nf
|
||||
.ft C
|
||||
% autfilt \-\-tgba \-\-high \-\-small some files
|
||||
.fi
|
||||
.PP
|
||||
The name
|
||||
.B dstar2tgba
|
||||
is kept for backward compatibility and because it is used
|
||||
in at least one published paper, but naming this tool
|
||||
.B aut2tgba
|
||||
would make more sense.
|
||||
|
||||
[BIBLIOGRAPHY]
|
||||
.TP
|
||||
1.
|
||||
|
|
|
|||
|
|
@ -204,22 +204,18 @@ Some development versions leading to 1.99.1 also featured
|
|||
An output file in the HOA format.
|
||||
.PP
|
||||
Different specifiers were needed because Spot implemented
|
||||
different parsers for these formats. Nowadays, the parsers
|
||||
for never claims, lbtt's format, and HOA format have been merged into
|
||||
a single parser that is able to distinguish these three formats
|
||||
automatically.
|
||||
different parsers for these formats. Nowadays, these parsers
|
||||
have been merged into a single parser that is able to
|
||||
distinguish these four formats automatically.
|
||||
.B ltlcross
|
||||
officially supports only two output specifiers
|
||||
officially supports only one output specifier:
|
||||
.TP
|
||||
%O
|
||||
An output file in either \fBlbtt\fR's format, as a never claim,
|
||||
or in the HOA format
|
||||
.TP
|
||||
%D
|
||||
An output file in \fBltl2dstar\fR's format.
|
||||
An output file in either \fBlbtt\fR's format, \fBltl2dstar\fR's format,
|
||||
as a never claim, or in the HOA format
|
||||
.P
|
||||
For backward compatibility, the sequences %N, %T, and %H are still
|
||||
supported (as aliases for %O), but are deprecated.
|
||||
For backward compatibility, the sequences %D, %H, %N, and %T, are
|
||||
still supported (as aliases for %O), but are deprecated.
|
||||
|
||||
[SEE ALSO]
|
||||
.BR randltl (1),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue