diff --git a/NEWS b/NEWS index 298cecb14..1de5e6cee 100644 --- a/NEWS +++ b/NEWS @@ -75,6 +75,11 @@ New in spot 1.99b (not yet released) in a pipe, and it also takes care of some necessary format conversion. + - ltl2tgba has a new option, -U, to produce unambiguous automata. + In unambiguous automata any word this recognized by at most one + accepting run (but there might be several ways to reject a + word). This works for LTL and PSL formulas. + - ltlcross will work with translator producing automata with any acceptance condition, provided the output is in the HOA format. So it can effectively be used to validate tools producing Rabin @@ -131,7 +136,8 @@ New in spot 1.99b (not yet released) ltl2tgba --check 'formula' additional checks will be performed, and the automaton will be accurately marked as either 'stutter-invariant' - or 'stutter-sensitive'. + or 'stutter-sensitive'. Another check performed by + --check is testing whether the automaton is unambiguous. - ltlcross (and ltldo) have a list of hard-coded shorthands for some existing tools. So for instance running @@ -222,10 +228,10 @@ New in spot 1.99b (not yet released) --spin=6 (or -s6 for short). - Support for building unambiguous automata. ltl_to_tgba() has a - new options to produce unambiguous TGBA, i.e., TGBAs in which - every word is accepted by at most one path. The ltl2tgba - command line has a new option, --unambigous (or -U) to produce - these automata, and autfilt has a --is-unambiguous filter. + new options to produce unambiguous TGBA (used by ltl2tgba -U as + discussed above). The function is_unambiguous() will check + whether an automaton is unambigous, and this is used by + autfilt --is-unmabiguous. * Noteworthy code changes diff --git a/doc/org/.dir-locals.el b/doc/org/.dir-locals.el index 25978d85c..a5908c461 100644 --- a/doc/org/.dir-locals.el +++ b/doc/org/.dir-locals.el @@ -8,7 +8,7 @@ (setq org-babel-sh-command (concat "PATH=../../src/bin" path-separator "$PATH sh")) - (setenv "SPOT_DOTDEFAULT" "brf(Lato)") + (setenv "SPOT_DOTDEFAULT" "Brf(Lato)") (setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"] edge[arrowhead=vee, arrowsize=.7]") (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 83337b547..7056cd8c8 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -24,7 +24,7 @@ (setq org-babel-sh-command (concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh")) -(setenv "SPOT_DOTDEFAULT" "brf(Lato)") +(setenv "SPOT_DOTDEFAULT" "Brf(Lato)") (setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"] edge[arrowhead=vee, arrowsize=.7]") diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index d4d7f0c64..02591195d 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -51,7 +51,7 @@ ltl2tgba "Fa & GFb" | dot -Tpdf > tgba.pdf #+RESULTS: The result would look like this (note that in this documentation -we use some [[file:aout.org][environement variables]] to produce a more colorful +we use some [[file:aout.org][environment variables]] to produce a more colorful output by default) #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none @@ -140,21 +140,22 @@ ltl2tgba -B 'GFa & GFb' #+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 [label="0", peripheries=2] 0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=] - 1 [label=<1>] + 1 [label="1"] 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] - 2 [label=<2>] + 2 [label="2"] 2 -> 0 [label=] 2 -> 2 [label=] } @@ -166,13 +167,13 @@ $txt #+RESULTS: [[file:dotex2ba.png]] -Although accepting states in the Büchi automaton are pictured with -double-lines, internally this automaton is still handled as a TGBA -with a single acceptance set such that the transitions -leaving the state are either all accepting, or all non-accepting. -You can see this underlying TGBA if you pass the =--dot=t= option -(the =t= requests the use of transition-based acceptance at it -is done internally): +Although accepting states in the Büchi automaton are (traditionally) +pictured with double-lines, internally this automaton is still handled +as a TGBA with a single acceptance set such that the transitions +leaving the state are either all accepting, or all non-accepting. You +can see this underlying TGBA if you pass the =--dot=t= option (the =t= +requests the use of transition-based acceptance as it is done +internally): #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba --dot=t -B 'GFa & GFb' @@ -223,15 +224,21 @@ ltl2tgba --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[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v] - GraphViz's format (default). Add letters for (a) - acceptance display, (b) acceptance sets as - bullets,(c) circular nodes, (f(FONT)) use FONT, - (h) horizontal layout, (v) vertical layout, (n) - with name, (N) without name, (r) rainbow colors - for acceptance set, (R) color acceptance set by - Inf/Fin, (s) with SCCs, (t) force transition-based - acceptance. + --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 @@ -240,7 +247,7 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' transition-based acceptance, (l) single-line output --lbtt[=t] LBTT's format (add =t to force transition-based - acceptance even on Büchi automata) + 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 @@ -340,49 +347,57 @@ ltl2tgba -s --lenient '(a < b) U (process[2]@ok)' : skip : } - * Do you favor deterministic or small automata? The translation procedure can be controled by a few switches. A first set of options specifies the intent of the translation: whenever -possible, would you prefer a small automaton or a deterministic -automaton? +possible, would you prefer a small automaton (=--small=) or a +deterministic (=--deterministic=) automaton? #+BEGIN_SRC sh :results verbatim :exports results ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -a, --any no preference +: -a, --any no preference, do not bother making it small or +: deterministic : -C, --complete output a complete automaton (combine with other : intents) : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) +: -U, --unambiguous output unambiguous automata (combine with other +: intents) -The =--any= option tells the translator that it should not target any -particular form of result: any automaton denoting the given formula is -OK. This effectively disables post-processings and speeds up the -translation. +The =--any= option tells the translator that it should attempt to +reduce or produce a deterministic result result: any automaton +denoting the given formula is OK. This effectively disables +post-processings and speeds up the translation. -With the =-D= option, the translator will /attempt/ to produce a -deterministic automaton, even if this requires a lot of states. =ltl2tgba= -knows how to produce the minimal deterministic Büchi automaton for -any obligation property (this includes safety properties). +With the =-D= or =--deterministic= option, the translator will +/attempt/ to produce a deterministic automaton, even if this requires +a lot of states. =ltl2tgba= knows how to produce the minimal +deterministic Büchi automaton for any obligation property (this +includes safety properties). With the =--small= option (the default), the translator will not produce a deterministic automaton when it knows how to build smaller automaton. +Note that options =--deterministic= and =--small= express +/preferences/. They certainly do /not/ guarantee that the output will +be deterministic, or will be the smallest automaton possible. + An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: #+NAME: gagbgc1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "Ga|Gb|Gc" +ltl2tgba 'Ga|Gb|Gc' #+END_SRC #+RESULTS: gagbgc1 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] @@ -416,31 +431,32 @@ ltl2tgba -D 'Ga|Gb|Gc' #+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 -> 6 - 0 [label=<0
⓿>] + 0 [label="0", peripheries=2] 0 -> 0 [label=] - 1 [label=<1
⓿>] + 1 [label="1", peripheries=2] 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] - 2 [label=<2
⓿>] + 2 [label="2", peripheries=2] 2 -> 2 [label=] - 3 [label=<3
⓿>] + 3 [label="3", peripheries=2] 3 -> 2 [label=] 3 -> 3 [label=] 3 -> 5 [label=] - 4 [label=<4
⓿>] + 4 [label="4", peripheries=2] 4 -> 0 [label=] 4 -> 4 [label=] 4 -> 5 [label=] - 5 [label=<5
⓿>] + 5 [label="5", peripheries=2] 5 -> 5 [label=] - 6 [label=<6
⓿>] + 6 [label="6", peripheries=2] 6 -> 0 [label=] 6 -> 1 [label=] 6 -> 2 [label=] @@ -461,10 +477,110 @@ You can augment the number of terms in the disjunction to magnify the difference. For N terms, the =--small= automaton has N+1 states, while the =--deterministic= automaton needs 2^N-1 states. -Add the =--complete= option if you want to obtain a complete +Add the =-C= or =--complete= option if you want to obtain a complete automaton, with a sink state capturing that rejected words that would not otherwise have a run in the output automaton. +Add the =-U= or =--unambiguous= option if you want unambiguous +automata to be produced. An automaton is unambiguous if any word is +recognized by at most one accepting run of the automaton (however a +word can be rejected by multiple runs, so unambiguous automata can be +non-deterministic). + +The following example is an ambiguous Büchi automaton, because the are +two ways to accept a run that repeats continuously the configuration +$\bar ab$. + +#+NAME: ambig1 +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -B 'GFa -> GFb' +#+END_SRC +#+RESULTS: ambig1 +#+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=] + 1 [label="1"] + 1 -> 0 [label=] + 1 -> 1 [label=<1>] + 1 -> 2 [label=] + 2 [label="2", peripheries=2] + 2 -> 2 [label=] + 2 -> 3 [label=] + 3 [label="3"] + 3 -> 2 [label=] + 3 -> 3 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file ambig1.png :cmdline -Tpng :var txt=ambig1 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:ambig1.png]] + +Here is an unambiguous automaton for the same formula, in which there +is only one run that recognizes this example word: + +#+NAME: ambig2 +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -B -U 'GFa -> GFb' +#+END_SRC + +#+RESULTS: ambig2 +#+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 -> 1 [label=] + 0 -> 2 [label=<1>] + 0 -> 3 [label=] + 0 -> 4 [label=] + 1 [label="1", peripheries=2] + 1 -> 1 [label=] + 2 [label="2", peripheries=2] + 2 -> 2 [label=] + 2 -> 5 [label=] + 3 [label="3"] + 3 -> 1 [label=] + 3 -> 3 [label=] + 3 -> 4 [label=] + 4 [label="4"] + 4 -> 3 [label=] + 4 -> 4 [label=] + 5 [label="5"] + 5 -> 2 [label=] + 5 -> 5 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file ambig2.png :cmdline -Tpng :var txt=ambig2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:ambig2.png]] + + +Unlike =--small= and =--deterministic= that express preferences, +options =--complete= and =--unambiguous= do guarantee that the output +will be complete and unambiguous. + A last parameter that can be used to tune the translation is the amount of pre- and post-processing performed. These two steps can be adjusted @@ -486,8 +602,8 @@ syntactic implications are performed. At =--high= level, language containment is used instead of syntactic implications. Post-processings are cleanups and simplifications of the automaton -produced by the core translator. The algorithms used during post-processing -are +produced by the core translator. The algorithms used during +post-processing are - SCC filtering: removing useless strongly connected components, and useless acceptance sets. - direct simulation: merge states based on suffix inclusion. @@ -496,6 +612,7 @@ are - WDBA minimization: determinize and minimize automata representing obligation properties. - degeneralization: convert a TGBA into a BA +- BA simulation (again direct or iterated) The chaining of these various algorithms depends on the selected combination of optimization level (=--low=, =--medium=, =--high=), diff --git a/doc/org/oaut.org b/doc/org/oaut.org index ef0b21761..a056628e0 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -822,7 +822,7 @@ The dot output can also be customized via two environment variables: variables set: #+BEGIN_SRC sh :results verbatim :exports code -export SPOT_DOTDEFAULT='brf(Lato)' +export SPOT_DOTDEFAULT='Brf(Lato)' export SPOT_DOTEXTRA='node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]' #+END_SRC diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 737c6d16a..88145fdd3 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -37,11 +37,12 @@ static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Translation intent:", 20 }, - { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 20 }, - { "deterministic", 'D', 0, 0, "prefer deterministic automata", 20 }, - { "any", 'a', 0, 0, "no preference", 20 }, + { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, + { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, + { "any", 'a', 0, 0, "no preference, do not bother making it small " + "or deterministic", 0 }, { "complete", 'C', 0, 0, "output a complete automaton (combine " - "with other intents)", 20 }, + "with other intents)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Optimization level:", 21 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, @@ -57,7 +58,8 @@ static const argp_option options_disabled[] = { 0, 0, 0, 0, "Translation intent:", 20 }, { "small", OPT_SMALL, 0, 0, "prefer small automata", 0 }, { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, - { "any", 'a', 0, 0, "no preference (default)", 0 }, + { "any", 'a', 0, 0, "no preference, do not bother making it small " + "or deterministic (default)", 0 }, { "complete", 'C', 0, 0, "output a complete automaton (combine " "with other intents)", 0 }, /**************************************************/ diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 75c47be90..6c7d41a97 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -64,7 +64,8 @@ static const argp_option options[] = { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "the formula, in Spot's syntax", 4 }, /**************************************************/ - { "unambiguous", 'U', 0, 0, "produce unambiguous automata", 20 }, + { "unambiguous", 'U', 0, 0, "output unambiguous automata " + "(combine with other intents)", 20 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, @@ -76,7 +77,7 @@ const struct argp_child children[] = { &finput_argp, 0, 0, 1 }, { &aoutput_argp, 0, 0, 0 }, { &aoutput_o_format_argp, 0, 0, 0 }, - { &post_argp, 0, 0, 20 }, + { &post_argp, 0, 0, 0 }, { &misc_argp, 0, 0, -1 }, { 0, 0, 0, 0 } };