From 17a18f2890776e221b2274036fa9c5fe6dfea09c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Sep 2015 22:46:39 +0200 Subject: [PATCH] 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. --- NEWS | 10 ++ doc/org/autfilt.org | 9 +- doc/org/dstar2tgba.org | 369 ++++++++++++++++++++++++++------------- doc/org/ltlcross.org | 45 +++-- doc/org/tools.org | 4 +- doc/org/tut20.org | 8 +- src/bin/common_trans.cc | 6 +- src/bin/man/dstar2tgba.x | 59 ++++++- src/bin/man/ltlcross.x | 20 +-- 9 files changed, 357 insertions(+), 173 deletions(-) diff --git a/NEWS b/NEWS index 0b5888c0f..fff597b6b 100644 --- a/NEWS +++ b/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 diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 49276067d..f4c77cef4 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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=...). diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 3af817c71..e4a0f5cfb 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -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=⓿) & Inf(❶)> + 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
❶>] + 0 -> 0 [label=] + 0 -> 3 [label=] + 1 [label=<1
⓿>] + 1 -> 1 [label=<1>] + 2 [label=<2>] + 2 -> 0 [label=] + 2 -> 1 [label=] + 2 -> 2 [label=] + 3 [label=<3>] + 3 -> 0 [label=] + 3 -> 3 [label=] +} +#+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
⓿>] + 0 [label="0", peripheries=2] 0 -> 0 [label=] 0 -> 2 [label=] - 1 [label=<1>] - 1 -> 0 [label=] - 1 -> 1 [label=] - 2 [label=<2>] + 1 [label="1"] + 1 -> 0 [label=] + 1 -> 1 [label=] + 2 [label="2"] 2 -> 0 [label=] 2 -> 2 [label=] } @@ -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(⓿) | Inf(❶)) & (Fin(❷) | Inf(❸))> + 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
❶❸>] + 0 -> 0 [label=] + 0 -> 1 [label=] + 0 -> 2 [label=] + 0 -> 3 [label=] + 1 [label=<1
⓿❸>] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] + 1 -> 3 [label=] + 2 [label=<2
❶❷>] + 2 -> 0 [label=] + 2 -> 1 [label=] + 2 -> 2 [label=] + 2 -> 3 [label=] + 3 [label=<3
⓿❷>] + 3 -> 0 [label=] + 3 -> 1 [label=] + 3 -> 2 [label=] + 3 -> 3 [label=] +} #+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=⓿❶>] + 0 -> 1 [label=⓿❶>] + 0 -> 2 [label=⓿❶>] + 0 -> 3 [label=⓿❶>] 1 [label="1"] - 1 -> 1 [label=] - 1 -> 1 [label=⓿>] + 1 -> 0 [label=❶>] 1 -> 1 [label=❶>] - 1 -> 1 [label=⓿❶>] + 1 -> 2 [label=❶>] + 1 -> 3 [label=❶>] + 2 [label="2"] + 2 -> 0 [label=⓿>] + 2 -> 1 [label=⓿>] + 2 -> 2 [label=⓿>] + 2 -> 3 [label=⓿>] + 3 [label="3"] + 3 -> 0 [label=] + 3 -> 1 [label=] + 3 -> 2 [label=] + 3 -> 3 [label=] } #+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. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index eae60005a..6cc13c175 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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). diff --git a/doc/org/tools.org b/doc/org/tools.org index 0e7a67b48..f36d69968 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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. diff --git a/doc/org/tut20.org b/doc/org/tut20.org index c90a82e01..905b0f31d 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -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 diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 2d01fea90..447a8553d 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -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 " diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x index e1dbce322..8caa0596d 100644 --- a/src/bin/man/dstar2tgba.x +++ b/src/bin/man/dstar2tgba.x @@ -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. diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 750533373..30b8b5e81 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -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),