document -U
* doc/org/.dir-locals.el, doc/org/init.el.in: Use 'B' instead of 'b' for default Dot output. * doc/org/oaut.org: Adjust. * NEWS, doc/org/ltl2tgba.org: Document -U. * src/bin/common_post.cc, src/bin/ltl2tgba.cc: Fix location of help text for -U.
This commit is contained in:
Alexandre Duret-Lutz
parent
5d76b9127b
commit
332694a485
7 changed files with 185 additions and 59 deletions
16
NEWS
16
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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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]")
|
||||
|
||||
|
|
|
|||
|
|
@ -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<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 [label="0", peripheries=2]
|
||||
0 -> 0 [label=<a & b>]
|
||||
0 -> 1 [label=<!b>]
|
||||
0 -> 2 [label=<!a & b>]
|
||||
1 [label=<1>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<a & b>]
|
||||
1 -> 1 [label=<!b>]
|
||||
1 -> 2 [label=<!a & b>]
|
||||
2 [label=<2>]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label=<a>]
|
||||
2 -> 2 [label=<!a>]
|
||||
}
|
||||
|
|
@ -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<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 [label="0", peripheries=2]
|
||||
0 -> 0 [label=<c>]
|
||||
1 [label=<1<br/><font color="#5DA5DA">⓿</font>>]
|
||||
1 [label="1", peripheries=2]
|
||||
1 -> 0 [label=<!b & c>]
|
||||
1 -> 1 [label=<b & c>]
|
||||
1 -> 2 [label=<b & !c>]
|
||||
2 [label=<2<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 [label="2", peripheries=2]
|
||||
2 -> 2 [label=<b>]
|
||||
3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 [label="3", peripheries=2]
|
||||
3 -> 2 [label=<!a & b>]
|
||||
3 -> 3 [label=<a & b>]
|
||||
3 -> 5 [label=<a & !b>]
|
||||
4 [label=<4<br/><font color="#5DA5DA">⓿</font>>]
|
||||
4 [label="4", peripheries=2]
|
||||
4 -> 0 [label=<!a & c>]
|
||||
4 -> 4 [label=<a & c>]
|
||||
4 -> 5 [label=<a & !c>]
|
||||
5 [label=<5<br/><font color="#5DA5DA">⓿</font>>]
|
||||
5 [label="5", peripheries=2]
|
||||
5 -> 5 [label=<a>]
|
||||
6 [label=<6<br/><font color="#5DA5DA">⓿</font>>]
|
||||
6 [label="6", peripheries=2]
|
||||
6 -> 0 [label=<!a & !b & c>]
|
||||
6 -> 1 [label=<!a & b & c>]
|
||||
6 -> 2 [label=<!a & b & !c>]
|
||||
|
|
@ -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=<!a>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<!a>]
|
||||
1 -> 1 [label=<1>]
|
||||
1 -> 2 [label=<b>]
|
||||
2 [label="2", peripheries=2]
|
||||
2 -> 2 [label=<b>]
|
||||
2 -> 3 [label=<!b>]
|
||||
3 [label="3"]
|
||||
3 -> 2 [label=<b>]
|
||||
3 -> 3 [label=<!b>]
|
||||
}
|
||||
#+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=<!a & !b>]
|
||||
0 -> 2 [label=<1>]
|
||||
0 -> 3 [label=<a | b>]
|
||||
0 -> 4 [label=<!a & !b>]
|
||||
1 [label="1", peripheries=2]
|
||||
1 -> 1 [label=<!a & !b>]
|
||||
2 [label="2", peripheries=2]
|
||||
2 -> 2 [label=<b>]
|
||||
2 -> 5 [label=<!b>]
|
||||
3 [label="3"]
|
||||
3 -> 1 [label=<!a & !b>]
|
||||
3 -> 3 [label=<a | b>]
|
||||
3 -> 4 [label=<!a & !b>]
|
||||
4 [label="4"]
|
||||
4 -> 3 [label=<a | b>]
|
||||
4 -> 4 [label=<!a & !b>]
|
||||
5 [label="5"]
|
||||
5 -> 2 [label=<b>]
|
||||
5 -> 5 [label=<!b>]
|
||||
}
|
||||
#+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=),
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 },
|
||||
/**************************************************/
|
||||
|
|
|
|||
|
|
@ -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 }
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue