From 345b8c5b144bc5afb2e3c64804730c15c62e3efa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Jan 2013 10:30:48 +0100 Subject: [PATCH] doc: add org-mode documentation for user tools * doc/org/.gitignore, doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org: New files. --- doc/org/.gitignore | 7 + doc/org/genltl.org | 84 +++++ doc/org/ioltl.org | 162 ++++++++++ doc/org/ltl2tgba.org | 716 +++++++++++++++++++++++++++++++++++++++++++ doc/org/ltl2tgta.org | 342 +++++++++++++++++++++ doc/org/ltlcross.org | 373 ++++++++++++++++++++++ doc/org/ltlfilt.org | 233 ++++++++++++++ doc/org/randltl.org | 327 ++++++++++++++++++++ doc/org/tools.org | 55 ++++ 9 files changed, 2299 insertions(+) create mode 100644 doc/org/.gitignore create mode 100644 doc/org/genltl.org create mode 100644 doc/org/ioltl.org create mode 100644 doc/org/ltl2tgba.org create mode 100644 doc/org/ltl2tgta.org create mode 100644 doc/org/ltlcross.org create mode 100644 doc/org/ltlfilt.org create mode 100644 doc/org/randltl.org create mode 100644 doc/org/tools.org diff --git a/doc/org/.gitignore b/doc/org/.gitignore new file mode 100644 index 000000000..32bc90c2f --- /dev/null +++ b/doc/org/.gitignore @@ -0,0 +1,7 @@ +*.png +err +*.html +*.csv +*.json +scheck.ltl +sum.py diff --git a/doc/org/genltl.org b/doc/org/genltl.org new file mode 100644 index 000000000..d5e995b36 --- /dev/null +++ b/doc/org/genltl.org @@ -0,0 +1,84 @@ +#+TITLE: =genltl= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This tool generates LTL formulas according to scalable patterns. +These pattern are usually taken from the literature (see the man page +for references). Sometimes the same pattern is given different names +in different papers, so we alias different option names to the same +pattern. + +#+BEGIN_SRC sh :results verbatim :exports results +genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +#+begin_example + --and-f=RANGE, --gh-e=RANGE + F(p1)&F(p2)&...&F(pn) + --and-fg=RANGE FG(p1)&FG(p2)&...&FG(pn) + --and-gf=RANGE, --ccj-phi=RANGE, --gh-c2=RANGE + GF(p1)&GF(p2)&...&GF(pn) + --ccj-alpha=RANGE F(p1&F(p2&F(p3&...F(pn)))) & + F(q1&F(q2&F(q3&...F(qn)))) + --ccj-beta=RANGE F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q)))) + --ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) & + F(q&(Xq)&(XXq)&...(X...X(q))) + --gh-q=RANGE (F(p1)|G(p2))&(F(p2)|G(p3))&... &(F(pn)|G(p{n+1})) + + --gh-r=RANGE (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... + &(GF(pn)|FG(p{n+1})) + --go-theta=RANGE !((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) + --or-fg=RANGE, --ccj-xi=RANGE + FG(p1)|FG(p2)|...|FG(pn) + --or-g=RANGE, --gh-s=RANGE G(p1)|G(p2)|...|G(pn) + --or-gf=RANGE, --gh-c1=RANGE + GF(p1)|GF(p2)|...|GF(pn) + --r-left=RANGE (((p1 R p2) R p3) ... R pn) + --r-right=RANGE (p1 R (p2 R (... R pn))) + --rv-counter=RANGE n-bit counter + --rv-counter-carry=RANGE n-bit counter w/ carry + --rv-counter-carry-linear=RANGE + n-bit counter w/ carry (linear size) + --rv-counter-linear=RANGE n-bit counter (linear size) + --u-left=RANGE, --gh-u=RANGE + (((p1 U p2) U p3) ... U pn) + --u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE + (p1 U (p2 U (... U pn))) +#+end_example + +An example is probably all it takes to explain how this tool works: + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --and-gf=1..5 --u-left=1..5 +#+END_SRC +#+RESULTS: +#+begin_example +GFp1 +GFp1 & GFp2 +GFp1 & GFp2 & GFp3 +GFp1 & GFp2 & GFp3 & GFp4 +GFp1 & GFp2 & GFp3 & GFp4 & GFp5 +p1 +p1 U p2 +(p1 U p2) U p3 +((p1 U p2) U p3) U p4 +(((p1 U p2) U p3) U p4) U p5 +#+end_example + +=genltl= supports the [[file:ioltl.org][common option for output of LTL formulas]], so you +may output these pattern for various tools. + +Note that for the =--lbt= output, each formula is relabeled using +=p0=, =p1=, ... before it is output, when the pattern (like +=--ccj-alpha=) use different names. + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: genltl num toc LTL scalable SRC sed gh pn fg FG gf qn +# LocalWords: ccj Xp XXp Xq XXq rv GFp lbt diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org new file mode 100644 index 000000000..df637739f --- /dev/null +++ b/doc/org/ioltl.org @@ -0,0 +1,162 @@ +#+TITLE: Common input and output options for LTL/PSL formulas +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +Spot supports different syntaxes for LTL/PSL formulas. This pages +document the options, common to all tools where it makes sense, that +are used to specify input and output of formula. + +* Common input options + +All tools that read LTL/PSL formulas implement the following options: + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --help | sed -n '/Input options:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: -f, --formula=STRING process the formula STRING +: -F, --file=FILENAME process each line of FILENAME as a formula +: --lbt-input read all formulas using LBT's prefix syntax +: --lenient parenthesized blocks that cannot be parsed as +: subformulas are considered as atomic properties + +=-f= is used to pass one formula one the command line, but this option can +be repeated to pass multiple formulas. + +=-F= is used to read formulas from a file (one formula per line). +This option can also be repeated to pass multiple files. If the +filename specified is =-= (as in =-F-=), then formulas are read from +standard input. + +** Default parser + +Spot's default LTL parser is able to parse the syntaxes of many tools, +such as [[http://spinroot.com][Spin]], [[http://vlsi.colorado.edu/~rbloem/wring.html][Wring]], [[http://goal.im.ntu.edu.tw][Goal]], etc. For instance here are the preferred ways +to express the same formula for different tools. + +# <> +| Tool | Formula | +|--------------+-------------------------| +| Spot | =G(a -> (b R !c))= | +| Spot (UTF-8) | =□(a → (b R c̅))= | +| Spin | =[](a -> (b V !c))= | +| Wring | =G(a=1 -> (b=1 R c=0))= | +| Goal | =G(a --> (b R ~c))= | + +Spot's default LTL parser will understand all of them. + +For a complete definition of the supported operators, including PSL +operators, please refer to the =doc/tl/tl.pdf= document inside the +Spot distribution. + +For Spot, an atomic proposition is any alphanumeric string that does +not start with the (upper case) characters =F=, =G=, or =X=. For +instance =gfa= is an atomic proposition, but =GFa= actually denotes +the LTL formula =G(F(a))=. Any double-quoted string is also +considered to be an atomic proposition, so if =GFa= had to be an +atomic proposition, it could be written +#+HTML: "GFa" +. + +These double-quote string also make it possible to embed arbitrarily +complex expressions that represent an atomic proposition that Spot +should not try to interpret. For instance: +: "a < b" U "process[2]@ok" + +** Lenient mode + +In version 6, Spin extended its syntax to support arbitrary atomic expression +in LTL formulas. The previous formula would be written simply: +: (a < b) U (process[2]@ok) + +While Spot cannot read the above syntax by default, it can do it if +you specify the =--lenient= option. (This global option affects all +formulas that are input.) + +The same parser is used, however its processing of parenthesis blocks +is different: every time a parenthesis block is scanned, the parser +first tries to recursively parse the block as an LTL/PSL formula, and +if this parsing failed, the block is considered to be an atomic +proposition. + + +For instance =(a U b) U c= will be successfully converted into an LTL +formula with two operators, while parsing =(a + b < 2) U c= will +consider =a + b < 2= as an atomic proposition. + +An unfortunate side-effect of =--lenient= parsing is that many syntax +errors will not be caught. Compare the following syntax error: + +#+BEGIN_SRC sh :results verbatim :exports code +ltlfilt -f '(a U b U) U c' +#+END_SRC +#+RESULTS: + +#+BEGIN_SRC sh :results verbatim :exports results +(ltlfilt -f '(a U b U) U c' 2>&1 | cat) | sed '/^$/d' +#+END_SRC +#+RESULTS: +: >>> (a U b U) U c +: ^ +: syntax error, unexpected closing parenthesis +: >>> (a U b U) U c +: ^ +: missing right operand for "until operator" + +With the same command in =--lenient= mode: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --lenient -f '(a U b U) U c' +#+END_SRC +#+RESULTS: +: "a U b U" U c + +Here =a U b U= was taken as an atomic proposition. + +** Prefix parser + +The prefix syntax used by tools such as [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]], [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], or [[http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/][scheck]], require +a different parser. For these tools, the above example formula has to +be written =G i p0 V p1 ! p2= (atomic propositions must start with =p= +and be followed by a number). Spot's =--lbt-input= option can be used +to activate the parser for this syntax. + +As an extension to LBT's syntax, atomic propositions may also be +double-quoted. In that case they do not have to follow the "=p= + +number" rule. + +=--lbt-input= is a global option that affects *all* formulas that are read. + +* Common output options + +All tools that output LTL/PSL formulas implement the following options: + +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: -8, --utf8 output using UTF-8 characters +: -l, --lbt output in LBT's syntax +: -p, --full-parentheses output fully-parenthesized formulas +: -s, --spin output in Spin's syntax +: --spot output in Spot's syntax (default) +: --wring output in Wring's syntax + +# LocalWords: syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME + +The =--spot=, =--utf-8=, =--spin=, =--wring= select different +output syntax as seen in [[tab:formula-syntaxes][the above table]]. The =-p= option can +be used to request that parenthesis be used at all levels. + +Note that by default Spot always output parentheses around operators +such as =U=, because not all tools agree on their associativity. For +instance =a U b U c= is read by Spot as =a U (b U c)= (because =U= is +right-associative in the PSL standard), while Spin (among other tools) +with read it as =(a U b) U c=. + +The =--lbt= option request an output in LBT's prefix format, and in +that case discussing associativity and parentheses makes no sense. + +# LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck +# LocalWords: utf associativity diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org new file mode 100644 index 000000000..60aeda52a --- /dev/null +++ b/doc/org/ltl2tgba.org @@ -0,0 +1,716 @@ +#+TITLE: =ltl2tgba= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This tool translates LTL or PSL formulas into two kinds of Büchi +automata. The default is to output Transition-based Generalized Büchi +Automata (hereinafter abbreviated TGBA), but more traditional Büchi +automata (BA) may be requested using the =-B= option. + +* TGBA and BA + +Formulas to translate may be specified using [[file:ioltl.org][common input options for +LTL/PSL formulas]]. + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -f 'Fa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 1 [label="!a\n"] + 1 -> 2 [label="a\n"] + 2 [label="2"] + 2 -> 2 [label="b\n{Acc[b]}"] + 2 -> 2 [label="!b\n"] +} +#+end_example + +Actually, because =ltl2tgba= is often used with a single formula +passed on the command line, the =-f= option can be omitted and any +command-line parameter that is not the argument of some option will be +assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltlfilt=]], +where such parameters are assumed to be filenames). + +The default output format, as shown above, is [[http://http://www.graphviz.org/][GraphViz]]'s format. This +can converted into a picture, or into vectorial format using =dot= or +=dotty=. Typically, you could get a =pdf= of this TGBA using +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "Fa & GFb" | dot -Tpdf > tgba.pdf +#+END_SRC +#+RESULTS: + +The result would look like this: +#+NAME: dotex +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba "Fa & GFb" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: dotex +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 2 [label="a\\n"] + 1 -> 1 [label="!a\\n"] + 2 [label="2"] + 2 -> 2 [label="b\\n{Acc[b]}"] + 2 -> 2 [label="!b\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file dotex.png :cmdline -Tpng :var txt=dotex :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:dotex.png]] + +The string between braces, =Acc[b]=, represents an acceptance set (its +actual name is not really important): any transition labeled by +=Acc[b]= belongs to the =Acc[b]= acceptance set. You may have many +transitions in the same acceptance set, and a transition may also +belong to multiple acceptance sets. An infinite path through this +automaton is accepting iff it visit each acceptance set infinitely +often. Therefore, in the above example, any accepted path will +/necessarily/ leave the initial state after a finite amount of steps, +and then it will verify the property =b= infinitely often. It is also +possible that an automaton do not use any acceptance set at all, in +which any run is accepting. + +Here is a TGBA with multiple acceptance sets (we omit the call to +=dot= to render the output of =ltl2tgba= from now on): + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba 'GFa & GFb' +#+END_SRC +#+RESULTS: +: digraph G { +: 0 [label="", style=invis, height=0] +: 0 -> 1 +: 1 [label="1"] +: 1 -> 1 [label="a & b\n{Acc[b], Acc[a]}"] +: 1 -> 1 [label="b & !a\n{Acc[b]}"] +: 1 -> 1 [label="a & !b\n{Acc[a]}"] +: 1 -> 1 [label="!b & !a\n"] +: } + +#+NAME: dotex2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba "GFa & GFb" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: dotex2 +: digraph G { +: 0 [label="", style=invis, height=0] +: 0 -> 1 +: 1 [label="1"] +: 1 -> 1 [label="a & b\\n{Acc[b], Acc[a]}"] +: 1 -> 1 [label="b & !a\\n{Acc[b]}"] +: 1 -> 1 [label="a & !b\\n{Acc[a]}"] +: 1 -> 1 [label="!b & !a\\n"] +: } + +#+BEGIN_SRC dot :file dotex2.png :cmdline -Tpng :var txt=dotex2 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:dotex2.png]] + +The above TGBA has two acceptance sets: =Acc[a]= and =Acc[b]=. +The position of these acceptance sets ensures that =a= and =b= atomic +proposition must be true infinitely often. + +A Büchi automaton for the previous formula can be obtained with the +=-B= option: + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -B 'GFa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 1 [label="a & b\n{Acc[1]}"] + 1 -> 2 [label="b & !a\n{Acc[1]}"] + 1 -> 3 [label="!b\n{Acc[1]}"] + 2 [label="1"] + 2 -> 1 [label="a\n"] + 2 -> 2 [label="!a\n"] + 3 [label="2"] + 3 -> 1 [label="a & b\n"] + 3 -> 2 [label="b & !a\n"] + 3 -> 3 [label="!b\n"] +} +#+end_example + +#+NAME: dotex2ba +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -B 'GFa & GFb' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: dotex2ba +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 1 [label="a & b\\n{Acc[1]}"] + 1 -> 2 [label="b & !a\\n{Acc[1]}"] + 1 -> 3 [label="!b\\n{Acc[1]}"] + 2 [label="1"] + 2 -> 1 [label="a\\n"] + 2 -> 2 [label="!a\\n"] + 3 [label="2"] + 3 -> 1 [label="a & b\\n"] + 3 -> 2 [label="b & !a\\n"] + 3 -> 3 [label="!b\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file dotex2ba.png :cmdline -Tpng :var txt=dotex2ba :exports results +$txt +#+END_SRC +#+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 =Acc[1]= such that the transitions +leaving the state are either all accepting, or all non-accepting. +This is the reason why the =Acc[1]= sets are still shown in the +output: it shows that a Büchi automaton is (a special case of) a TGBA. + +Various options controls the output format of =ltl2tgba=: + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: -8, --utf8 enable UTF-8 characters in output (ignored with +: --lbtt or --spin) +: --dot GraphViz's format (default) +: --lbtt LBTT's format +: -s, --spin Spin neverclaim (implies --ba) +: --spot SPOT's format +: --stats=FORMAT output statistics about the automaton + + +The =-8= option can be used to improve the readability of the output +if your system can display UTF-8 correctly. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -B8 'GFa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 1 [label="a∧b\n{Acc[1]}"] + 1 -> 2 [label="b∧a̅\n{Acc[1]}"] + 1 -> 3 [label="b̅\n{Acc[1]}"] + 2 [label="1"] + 2 -> 1 [label="a\n"] + 2 -> 2 [label="a̅\n"] + 3 [label="2"] + 3 -> 1 [label="a∧b\n"] + 3 -> 2 [label="b∧a̅\n"] + 3 -> 3 [label="b̅\n"] +} +#+end_example + +#+NAME: dotex2ba8 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -B8 "GFa & GFb" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: dotex2ba8 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0", peripheries=2] + 1 -> 1 [label="a∧b\\n{Acc[1]}"] + 1 -> 2 [label="b∧a̅\\n{Acc[1]}"] + 1 -> 3 [label="b̅\\n{Acc[1]}"] + 2 [label="1"] + 2 -> 1 [label="a\\n"] + 2 -> 2 [label="a̅\\n"] + 3 [label="2"] + 3 -> 1 [label="a∧b\\n"] + 3 -> 2 [label="b∧a̅\\n"] + 3 -> 3 [label="b̅\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file dotex2ba8.png :cmdline -Tpng :var txt=dotex2ba8 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:dotex2ba8.png]] + +* Spin output + +Using the =--spin= or =-s= option, =ltl2tgba= will produce a Büchi automaton +(the =-B= option is implied) as a never claim that can be fed to Spin. +=ltl2tgba -s= is therefore a drop-in replacement for =spin -f=. + + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -s 'GFa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +never { /* G(Fa & Fb) */ +accept_init: + if + :: ((a) && (b)) -> goto accept_init + :: ((b) && (!((a)))) -> goto T0_S2 + :: ((!((b)))) -> goto T0_S3 + fi; +T0_S2: + if + :: ((a)) -> goto accept_init + :: ((!((a)))) -> goto T0_S2 + fi; +T0_S3: + if + :: ((a) && (b)) -> goto accept_init + :: ((b) && (!((a)))) -> goto T0_S2 + :: ((!((b)))) -> goto T0_S3 + fi; +} +#+end_example + +Since Spin 6 extended its syntax to support arbitrary atomic +propositions, you may also need put the parser in =--lenient= mode to +support these: + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -s --lenient '(a < b) U (process[2]@ok)' +#+END_SRC +#+RESULTS: +: never { /* "a < b" U "process[2]@ok" */ +: T0_init: +: if +: :: ((process[2]@ok)) -> goto accept_all +: :: ((a < b) && (!(process[2]@ok))) -> goto T0_init +: fi; +: accept_all: +: 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? + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: -a, --any no preference +: -D, --deterministic prefer deterministic automata +: --small prefer small automata (default) + +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. + +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 =--small= option (the default), the translator will not +produce a deterministic automaton when it knows how to build smaller +automaton. + +An example formula where the difference between =-D= and =--small= is +flagrant is =Ga|Gb|Gc=: + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba 'Ga|Gb|Gc' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 2 [label="b\n"] + 1 -> 3 [label="c\n"] + 1 -> 4 [label="a\n"] + 2 [label="2"] + 2 -> 2 [label="b\n"] + 3 [label="3"] + 3 -> 3 [label="c\n"] + 4 [label="4"] + 4 -> 4 [label="a\n"] +} +#+end_example + +#+NAME: gagbgc1 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba "Ga|Gb|Gc" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gagbgc1 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 2 [label="c\\n"] + 1 -> 3 [label="b\\n"] + 1 -> 4 [label="a\\n"] + 2 [label="2"] + 2 -> 2 [label="c\\n"] + 3 [label="3"] + 3 -> 3 [label="b\\n"] + 4 [label="4"] + 4 -> 4 [label="a\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file gagbgc1.png :cmdline -Tpng :var txt=gagbgc1 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gagbgc1.png]] + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -D 'Ga|Gb|Gc' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="6"] + 1 -> 1 [label="a & b & c\n{Acc[1]}"] + 1 -> 2 [label="b & c & !a\n{Acc[1]}"] + 1 -> 3 [label="a & c & !b\n{Acc[1]}"] + 1 -> 4 [label="c & !a & !b\n{Acc[1]}"] + 1 -> 5 [label="a & b & !c\n{Acc[1]}"] + 1 -> 6 [label="b & !a & !c\n{Acc[1]}"] + 1 -> 7 [label="a & !b & !c\n{Acc[1]}"] + 2 [label="2"] + 2 -> 2 [label="b & c\n{Acc[1]}"] + 2 -> 4 [label="c & !b\n{Acc[1]}"] + 2 -> 6 [label="b & !c\n{Acc[1]}"] + 3 [label="4"] + 3 -> 3 [label="a & c\n{Acc[1]}"] + 3 -> 4 [label="c & !a\n{Acc[1]}"] + 3 -> 7 [label="a & !c\n{Acc[1]}"] + 4 [label="1"] + 4 -> 4 [label="c\n{Acc[1]}"] + 5 [label="5"] + 5 -> 5 [label="a & b\n{Acc[1]}"] + 5 -> 6 [label="b & !a\n{Acc[1]}"] + 5 -> 7 [label="a & !b\n{Acc[1]}"] + 6 [label="3"] + 6 -> 6 [label="b\n{Acc[1]}"] + 7 [label="0"] + 7 -> 7 [label="a\n{Acc[1]}"] +} +#+end_example + +#+NAME: gagbgc2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D 'Ga|Gb|Gc' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gagbgc2 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="6"] + 1 -> 1 [label="a & b & c\\n{Acc[1]}"] + 1 -> 2 [label="b & c & !a\\n{Acc[1]}"] + 1 -> 3 [label="a & c & !b\\n{Acc[1]}"] + 1 -> 4 [label="c & !a & !b\\n{Acc[1]}"] + 1 -> 5 [label="a & b & !c\\n{Acc[1]}"] + 1 -> 6 [label="b & !a & !c\\n{Acc[1]}"] + 1 -> 7 [label="a & !b & !c\\n{Acc[1]}"] + 2 [label="1"] + 2 -> 2 [label="b & c\\n{Acc[1]}"] + 2 -> 4 [label="c & !b\\n{Acc[1]}"] + 2 -> 6 [label="b & !c\\n{Acc[1]}"] + 3 [label="2"] + 3 -> 3 [label="a & c\\n{Acc[1]}"] + 3 -> 4 [label="c & !a\\n{Acc[1]}"] + 3 -> 7 [label="a & !c\\n{Acc[1]}"] + 4 [label="0"] + 4 -> 4 [label="c\\n{Acc[1]}"] + 5 [label="4"] + 5 -> 5 [label="a & b\\n{Acc[1]}"] + 5 -> 6 [label="b & !a\\n{Acc[1]}"] + 5 -> 7 [label="a & !b\\n{Acc[1]}"] + 6 [label="3"] + 6 -> 6 [label="b\\n{Acc[1]}"] + 7 [label="5"] + 7 -> 7 [label="a\\n{Acc[1]}"] +} +#+end_example + +#+BEGIN_SRC dot :file gagbgc2.png :cmdline -Tpng :var txt=gagbgc2 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gagbgc2.png]] + +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. + +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 +via a common set of switches: +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: --high all available optimizations (slow, default) +: --low minimal optimizations (fast) +: --medium moderate optimizations + +Pre-processings are rewritings done on the LTL formulas, usually to +reduce its size, but mainly to put it in a form that will help the +translator (for instance =F(a|b)= is easier to translate than +=F(a)|F(b)=). At =--low= level, only simple syntactic rewritings are +performed. At =--medium= level, additional simplifications based on +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 +- SCC filtering: removing useless strongly connected components, + and useless acceptance sets. +- direct simulation: merge states based on suffix inclusion. +- iterated simulations: merge states based on suffix inclusion, + or prefix inclusion, in a loop. +- WDBA minimization: determinize and minimize automata representing + obligation properties. +- degeneralization: convert a TGBA into a BA + +The chaining of these various algorithms depends on the selected +combination of optimization level (=--low=, =--medium=, =--high=), +translation intent (=--small=, =--deterministic=) and type of +automaton desired (=--tgba=, =--ba=). + +A notable configuration is =--any --low=, which will produce a TGBA as +fast as possible. In this case, post-processing is disabled, and only +syntactic rewritings are performed. This can be used for +satisfiability checking, although in this context even building an +automaton is overkill (you only need an accepted run). + +Finally, it should be noted that the default optimization options +(=--small --high=) are usually overkill. =--low= will produce good +automata most of the time. Most of pattern formulas of [[file:genltl.org][=genltl=]] will +be efficiently translated in this configuration (meaning that =--small +--high= will not produce a better automaton). If you are planning to +generate automata for large family of pattern formulas, it makes sense +to experiment with the different settings on a small version of the +pattern, and select the lowest setting that satisfies your +expectations. + +* Translating multiple formulas for statistics + +If multiple formulas are given to =ltl2tgba=, the corresponding +automata will be output one after the other. This is not very +convenient, since most of these output formats are not designed to +represent multiple automata, and tools like =dot= will only display +the first one. + +One situation where passing many formulas to =ltl2tgba= is useful is +in combination with the =--stats=FORMAT= option. This option will +output statistics about the translated automata instead of the +automata themselves. The =FORMAT= string should indicate which +statistics should be output, and how they should be output using the +following sequence of characters (other characters are output as-is): + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --help | sed -n '/^ *%/p' +#+END_SRC +#+RESULTS: +: %% a single % +: %a number of acceptance sets +: %d 1 if the automaton is deterministic, 0 otherwise +: %e number of edges +: %f the formula, in Spot's syntax +: %n number of nondeterministic states +: %s number of states +: %S number of SCCs +: %t number of transitions + +For instance we can study the size of the automata generated for the +right-nested =U= formulas as follows: + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"' +#+END_SRC +#+RESULTS: +: 2 states and 2 edges for "p1" +: 2 states and 3 edges for "p1 U p2" +: 3 states and 6 edges for "p1 U (p2 U p3)" +: 4 states and 10 edges for "p1 U (p2 U (p3 U p4))" +: 5 states and 15 edges for "p1 U (p2 U (p3 U (p4 U p5)))" +: 6 states and 21 edges for "p1 U (p2 U (p3 U (p4 U (p5 U p6))))" +: 7 states and 28 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U p7)))))" +: 8 states and 36 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U (p7 U p8))))))" + +Here =-F -= means that formulas should be read from the standard input. + +When computing the size of an automaton, we distinguish /transitions/ +and /edges/. An edge between two states is labeled by a Boolean +formula and may in fact represent several transitions labeled by +compatible Boolean assignment. + +For instance if the atomic propositions are =x= and =y=, an edge labeled +by the formula =!x= actually represents two transitions labeled respectively +with =!x&y= and =!x&!y=. + +Two automata with the same structures (states and edges) but differing +labels, may have a different count of transitions, e.g., if one has +more restricted labels. + +* Building Monitors + +In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the +=-M= option. These are finite automata that accept all prefixes of a +formula. The idea is that you can use these automata to monitor a +system as it is running, and report a violation as soon as no +compatible outgoing transition exist. + +=ltl2tgba -M= may output non-deterministic monitors while =ltl2tgba +-MD= (short for =--monitor --deterministic=) will output the minimal +deterministic monitor for the given formula. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -M '(Xa & Fb) | Gc' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 2 [label="1\n"] + 1 -> 3 [label="c\n"] + 2 [label="2", peripheries=2] + 2 -> 4 [label="a\n"] + 3 [label="3", peripheries=2] + 3 -> 3 [label="c\n"] + 4 [label="4", peripheries=2] + 4 -> 4 [label="1\n"] +} +#+end_example +#+NAME: monitor1 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -M '(Xa & Fb) | Gc' | sed 's/\\/\\\\/' +#+END_SRC + +#+RESULTS: monitor1 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 2 [label="1\\n"] + 1 -> 3 [label="c\\n"] + 2 [label="2", peripheries=2] + 2 -> 4 [label="a\\n"] + 3 [label="3", peripheries=2] + 3 -> 3 [label="c\\n"] + 4 [label="4", peripheries=2] + 4 -> 4 [label="1\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file monitor1.png :cmdline -Tpng :var txt=monitor1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:monitor1.png]] + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -M '(Xa & Fb) | Gc' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 2 [label="1\n"] + 1 -> 3 [label="c\n"] + 2 [label="2", peripheries=2] + 2 -> 4 [label="a\n"] + 3 [label="3", peripheries=2] + 3 -> 3 [label="c\n"] + 4 [label="4", peripheries=2] + 4 -> 4 [label="1\n"] +} +#+end_example +#+NAME: monitor2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -MD '(Xa & Fb) | Gc' | sed 's/\\/\\\\/' +#+END_SRC + +#+RESULTS: monitor2 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 2 [label="c\\n"] + 1 -> 3 [label="!c\\n"] + 2 [label="4", peripheries=2] + 2 -> 4 [label="a\\n"] + 2 -> 5 [label="c & !a\\n"] + 3 [label="3", peripheries=2] + 3 -> 4 [label="a\\n"] + 4 [label="2", peripheries=2] + 4 -> 4 [label="1\\n"] + 5 [label="0", peripheries=2] + 5 -> 5 [label="c\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:monitor2.png]] + +Because they accept all finite executions that could be extended to +match the formula, monitor cannot be used to check for eventualities +such as =F(a)=. Any finite execution can be extended to match =F(a)=. + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc +# LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex +# LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb +# LocalWords: GraphViz's LBTT's neverclaim SPOT's init goto fi Gb +# LocalWords: controled Gc gagbgc disjunction pre rewritings SCC Xa +# LocalWords: WDBA determinize degeneralization satisfiability SCCs +# LocalWords: genltl nondeterministic eval setenv concat getenv +# LocalWords: setq diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org new file mode 100644 index 000000000..1c4863070 --- /dev/null +++ b/doc/org/ltl2tgta.org @@ -0,0 +1,342 @@ +#+TITLE: =ltl2tgta= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This tool generates various form of Testing Automata, i.e., automata +that observe the /changes/ of atomic propositions, not their values. + +Three types of automata can be output. The only output format +supported currently is [[http://http://www.graphviz.org/][GraphViz]]'s format, with option =-8= to enable +UTF-8 characters as in other tools. + +The =--ta= option will translate a formula into Testing Automaton, as +described by [[http://spinroot.com/spin/Workshops/ws06/039.pdf][Geldenhuys and Hansen (Spin'06)]]. + +Here is the output on =a U Gb= (we omit the call to =dot=, as shown while +discussing [[file:ltl2tgba.org][=ltl2tgba=]]). + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgta --ta --multiple-init 'a U Gb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + -1 [label="", style=invis, height=0] + -1 -> 1 [label="a & b"] + -2 [label="", style=invis, height=0] + -2 -> 2 [label="a & !b"] + -3 [label="", style=invis, height=0] + -3 -> 3 [label="b & !a"] + 1 [label="0\na & b",shape=box] + 1 -> 3 [label="{a}\n"] + 1 -> 2 [label="{b}\n"] + 1 -> 4 [label="{a}\n"] + 2 [label="1\na & !b"] + 2 -> 1 [label="{b}\n"] + 2 -> 3 [label="{a, b}\n"] + 3 [label="2\nb & !a",shape=box] + 3 -> 4 [label="{a}\n"] + 4 [label="3",peripheries=2,shape=box] + 4 -> 4 [label="{a}\n{Acc[1]}"] +} +#+end_example + +#+NAME: augb-ta +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgta --ta --multiple-init 'a U Gb' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: augb-ta +#+begin_example +digraph G { + -1 [label="", style=invis, height=0] + -1 -> 1 [label="a & !b"] + -2 [label="", style=invis, height=0] + -2 -> 2 [label="b & !a"] + -3 [label="", style=invis, height=0] + -3 -> 3 [label="a & b"] + 1 [label="2\\na & !b"] + 1 -> 3 [label="{b}\\n"] + 1 -> 2 [label="{a, b}\\n"] + 2 [label="0\\nb & !a",shape=box] + 2 -> 4 [label="{a}\\n"] + 3 [label="1\\na & b",shape=box] + 3 -> 2 [label="{a}\\n"] + 3 -> 1 [label="{b}\\n"] + 3 -> 4 [label="{a}\\n"] + 4 [label="3",peripheries=2,shape=box] + 4 -> 4 [label="{a}\\n{Acc[1]}"] +} +#+end_example + +#+BEGIN_SRC dot :file augb-ta.png :cmdline -Tpng :var txt=augb-ta :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:augb-ta.png]] + +As always, the labels of the states have no influence on the language +recognized by the automaton. This automaton has three possible +initial states. The initial state should be chosen depending on the +initial valuation of =a= and =b= in the system to be synchronized with +this testing automaton. For instance if =a= is true and =b= false in +the initial state, the testing automaton should start in the state +pointed to by the initial arrow labeled =a & !b=. In the rest of the +testing automaton, the transitions are labeled by the sets of atomic +propositions that should change in the system for the testing +automaton to progress. States with a double enclosure are Büchi +accepting, meaning that any execution that visits one of these states +is accepting. All states have an implicit self-loop labeled by ={}=: +if the system progress without changing the value of =a= and =b=, the +testing automaton remains in the same state. Rectangle states are +livelock-accepting: any execution of the system that get stuck into +one of these state is accepting. + +Without the =--multiple-init= option, a fake initial state is added. +This is the default since it often makes the result more readable. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgta --ta 'a U Gb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="b & !a\n"] + 1 -> 3 [label="a & b\n"] + 1 -> 4 [label="a & !b\n"] + 2 [label="2",shape=box] + 2 -> 5 [label="{a}\n"] + 3 [label="3",shape=box] + 3 -> 5 [label="{a}\n"] + 3 -> 2 [label="{a}\n"] + 3 -> 4 [label="{b}\n"] + 4 [label="1"] + 4 -> 3 [label="{b}\n"] + 4 -> 2 [label="{a, b}\n"] + 5 [label="4",peripheries=2,shape=box] + 5 -> 5 [label="{a}\n{Acc[1]}"] +} +#+end_example + +#+NAME: augb-ta2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgta --ta 'a U Gb' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: augb-ta2 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="b & !a\\n"] + 1 -> 3 [label="a & b\\n"] + 1 -> 4 [label="a & !b\\n"] + 2 [label="2",shape=box] + 2 -> 5 [label="{a}\\n"] + 3 [label="3",shape=box] + 3 -> 2 [label="{a}\\n"] + 3 -> 4 [label="{b}\\n"] + 3 -> 5 [label="{a}\\n"] + 4 [label="1"] + 4 -> 3 [label="{b}\\n"] + 4 -> 2 [label="{a, b}\\n"] + 5 [label="4",peripheries=2,shape=box] + 5 -> 5 [label="{a}\\n{Acc[1]}"] +} +#+end_example + +#+BEGIN_SRC dot :file augb-ta2.png :cmdline -Tpng :var txt=augb-ta2 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:augb-ta2.png]] + +The =--gba= option can be used to request a Generalized Testing +Automaton, i.e., a Testing Automaton with Generalized Büchi +acceptance. In that case double-enclosures are not used anymore, and +Büchi accepting transitions are marked with the same ={Acc[x],Acc[y]}= +notation used in TGBA. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgta --gta 'GFa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="a & b\n"] + 1 -> 3 [label="b & !a\n"] + 1 -> 4 [label="a & !b\n"] + 1 -> 5 [label="!b & !a\n"] + 2 [label="1",shape=box] + 2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"] + 2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"] + 2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"] + 3 [label="4"] + 3 -> 2 [label="{a}\n{Acc[b]}"] + 3 -> 4 [label="{a, b}\n{Acc[b]}"] + 3 -> 5 [label="{b}\n{Acc[b]}"] + 4 [label="2"] + 4 -> 2 [label="{b}\n{Acc[a]}"] + 4 -> 3 [label="{a, b}\n{Acc[a]}"] + 4 -> 5 [label="{a}\n{Acc[a]}"] + 5 [label="3"] + 5 -> 2 [label="{a, b}\n"] + 5 -> 3 [label="{b}\n"] + 5 -> 4 [label="{a}\n"] +} +#+end_example + +#+NAME: gfagfb-gta +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgta --gta 'GFa & GFb' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gfagfb-gta +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="a & b\\n"] + 1 -> 3 [label="b & !a\\n"] + 1 -> 4 [label="a & !b\\n"] + 1 -> 5 [label="!b & !a\\n"] + 2 [label="1",shape=box] + 2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"] + 2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"] + 2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"] + 3 [label="4"] + 3 -> 2 [label="{a}\\n{Acc[b]}"] + 3 -> 4 [label="{a, b}\\n{Acc[b]}"] + 3 -> 5 [label="{b}\\n{Acc[b]}"] + 4 [label="2"] + 4 -> 2 [label="{b}\\n{Acc[a]}"] + 4 -> 3 [label="{a, b}\\n{Acc[a]}"] + 4 -> 5 [label="{a}\\n{Acc[a]}"] + 5 [label="3"] + 5 -> 2 [label="{a, b}\\n"] + 5 -> 3 [label="{b}\\n"] + 5 -> 4 [label="{a}\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file gfagfb-gta.png :cmdline -Tpng :var txt=gfagfb-gta :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gfagfb-gta.png]] + +The interpretation is similar to that of the TA. Execution that +stutter in a livelock-accepting (square) state are accepting as well +as execution that visit the =Acc[a]= and =Acc[b]= acceptance sets +infinitely often. Those acceptance sets are carried by transitions, +as in TGBAs. + +Finally, the default is to output a Transition-based Generalized +Testing Automaton [fn:topnoc]. In TGTAs, the stuttering states are +made explicit with ={}= self-loops. Since these self-loop can be in +acceptance sets, livelock acceptance states are no longer needed. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgta 'GFa & GFb' +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="a & b\n"] + 1 -> 3 [label="b & !a\n"] + 1 -> 4 [label="a & !b\n"] + 1 -> 5 [label="!b & !a\n"] + 2 [label="3"] + 2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"] + 2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"] + 2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"] + 2 -> 2 [label="{}\n{Acc[b], Acc[a]}"] + 3 [label="4"] + 3 -> 2 [label="{a}\n{Acc[b]}"] + 3 -> 4 [label="{a, b}\n{Acc[b]}"] + 3 -> 5 [label="{b}\n{Acc[b]}"] + 3 -> 3 [label="{}\n"] + 4 [label="2"] + 4 -> 2 [label="{b}\n{Acc[a]}"] + 4 -> 3 [label="{a, b}\n{Acc[a]}"] + 4 -> 5 [label="{a}\n{Acc[a]}"] + 4 -> 4 [label="{}\n"] + 5 [label="1"] + 5 -> 2 [label="{a, b}\n"] + 5 -> 3 [label="{b}\n"] + 5 -> 4 [label="{a}\n"] + 5 -> 5 [label="{}\n"] +} +#+end_example + +#+NAME: gfagfb-tgta +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgta 'GFa & GFb' | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gfagfb-tgta +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label=init] + 1 -> 2 [label="a & b\\n"] + 1 -> 3 [label="b & !a\\n"] + 1 -> 4 [label="a & !b\\n"] + 1 -> 5 [label="!b & !a\\n"] + 2 [label="1"] + 2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"] + 2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"] + 2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"] + 2 -> 2 [label="{}\\n{Acc[b], Acc[a]}"] + 3 [label="4"] + 3 -> 2 [label="{a}\\n{Acc[b]}"] + 3 -> 4 [label="{a, b}\\n{Acc[b]}"] + 3 -> 5 [label="{b}\\n{Acc[b]}"] + 3 -> 3 [label="{}\\n"] + 4 [label="3"] + 4 -> 2 [label="{b}\\n{Acc[a]}"] + 4 -> 3 [label="{a, b}\\n{Acc[a]}"] + 4 -> 5 [label="{a}\\n{Acc[a]}"] + 4 -> 4 [label="{}\\n"] + 5 [label="2"] + 5 -> 2 [label="{a, b}\\n"] + 5 -> 3 [label="{b}\\n"] + 5 -> 4 [label="{a}\\n"] + 5 -> 5 [label="{}\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file gfagfb-tgta.png :cmdline -Tpng :var txt=gfagfb-tgta :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gfagfb-tgta.png]] + + +[fn:topnoc]: This new class of automaton, as well as the +implementation of the previous testing automata classes, is part of +Ala Eddine BEN SALEM's PhD work, and should appear in a future edition +of ToPNoC (LNCS 7400). + + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: ltl tgta num toc Automata automata GraphViz UTF Gb na +# LocalWords: Geldenhuys tgba SRC init invis nb Acc augb sed png fn +# LocalWords: cmdline Tpng txt Büchi livelock gba gta GFa GFb TGTAs +# LocalWords: gfagfb topnoc Eddine SALEM's ToPNoC LNCS eval setenv +# LocalWords: concat getenv setq diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org new file mode 100644 index 000000000..c59efc054 --- /dev/null +++ b/doc/org/ltlcross.org @@ -0,0 +1,373 @@ +#+TITLE: =ltlcross= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +=ltlcross= is a tool for cross-comparing the output of LTL-to-Büchi +translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], the +/LTL-to-Büchi Translator Testbench/, that essentially performs the +same sanity checks. + +The main motivations for rewriting this tool were: + - support for PSL formulas in addition to LTL + - more statistics (like counting the number of logical transitions + represented by each physical edge), output in a format that + can be more easily be post-processed, + - more precise time measurement (LBTT was only precise to + 1/100 of a second, reporting most times as "0.00s"). + +Although =ltlcross= performs the same sanity checks as LBTT, it does +not implement any of the interactive features of LBTT. Essentially +=ltlcross= will report problems, but you will be on your own to +investigate and fix them. + +The core of =ltlcross= is a loop that does the following steps: + - Input a formula + - Translate the formula and its negation using each configured translator. + If there are 3 translators, the positive and negative translations + will be denoted =P0=, =N0=, =P1=, =N1=, =P2=, =N2=. + - Build the products of these automata with a random state-space (the same + state-space for all translations). + - Perform sanity checks between all these automata to detect any problem. + - Gather statistics if requested. + +* Formula selection + +Formulas to translate should be specified using the [[file:ioltl.org][common input options]]. +Standard input is read if no =-f= or =-F= option is given. + +* Configuring translators + +Each translator should be specified as a string that use some of the +following character sequences: + +#+BEGIN_SRC sh :results verbatim :exports results +ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: %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 +: %N,%T the output automaton as a Never claim, or in +: LBTT'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)=. + +#+BEGIN_SRC sh :results verbatim :exports code +ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N' +#+END_SRC +#+RESULTS: + +When =ltlcross= executes these commands, =%s= will be replaced +by the formula in Spin's syntax, and =%N= will be replaced by a +temporary file into which the output of the translator is redirected +before it is read back by =ltlcross=. + +#+BEGIN_SRC sh :results verbatim :exports results +ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N' 2>&1 +#+END_SRC +#+RESULTS: +#+begin_example +([](<>(a))) +Running [P0]: ltl2tgba -s '([](<>(a)))' >'lck-o0-iDGV6y' +Running [P1]: spin -f '([](<>(a)))' >'lck-o1-sA3FYp' +Running [N0]: ltl2tgba -s '(!([](<>(a))))' >'lck-o0-1ClVQg' +Running [N1]: spin -f '(!([](<>(a))))' >'lck-o1-wyErP7' +Performing sanity checks and gathering statistics... + +(X((a) U (b))) +Running [P0]: ltl2tgba -s '(X((a) U (b)))' >'lck-o0-ex1BYY' +Running [P1]: spin -f '(X((a) U (b)))' >'lck-o1-UNE8dQ' +Running [N0]: ltl2tgba -s '(!(X((a) U (b))))' >'lck-o0-coM8tH' +Running [N1]: spin -f '(!(X((a) U (b))))' >'lck-o1-eHPoQy' +Performing sanity checks and gathering statistics... + +no problem detected +#+end_example + +=ltlcross= can only read two 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 =%N=. + - [[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 be indicated using =%T=. + +Of course all configured tools need not the same =%= sequences. + +* Getting statistics + +Detailed statistics about the result of each translation, and the +product of that resulting automaton with the random state-space, can +be obtained using the =--csv=FILE= or =--json=FILE= option. + +The following compare =ltl2tgba=, =spin=, and =lbt= on three random +formula (where =W= and =M= operators have been removed because they +are not supported by =spin= and =lbt=). + +#+BEGIN_SRC sh :results verbatim :exports code +randltl -n 2 a b | +ltlfilt --remove-wm | +ltlcross --csv=results.csv \ + 'ltl2tgba -s %f >%N' \ + 'spin -f %s >%N' \ + 'lbt < %L >%T' +#+END_SRC +#+RESULTS: + +#+BEGIN_SRC sh :results verbatim :exports results +randltl -n 2 a b c | ltlfilt --remove-wm | +ltlcross --csv=results.csv --json=results.json \ + 'ltl2tgba -s %f >%N' \ + 'spin -f %s >%N' \ + 'lbt < %L >%T' --csv=results.csv 2>&1 +#+END_SRC +#+RESULTS: +#+begin_example +-:1: (G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))) +Running [P0]: ltl2tgba -s '(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))' >'lck-o0-eGEYaZ' +Running [P1]: spin -f '([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1)))))))' >'lck-o1-nYpFBX' +Running [P2]: lbt < 'lck-i0-fGdZQ0' >'lck-o2-CPs23V' +Running [N0]: ltl2tgba -s '(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))' >'lck-o0-kXiZZS' +Running [N1]: spin -f '(!([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1))))))))' >'lck-o1-7ILLzR' +Running [N2]: lbt < 'lck-i0-9KG0wU' >'lck-o2-CcMCaQ' +Performing sanity checks and gathering statistics... + +-:2: (!((G(F(p0))) -> (F(p1)))) +Running [P0]: ltl2tgba -s '(!((G(F(p0))) -> (F(p1))))' >'lck-o0-IOckzW' +Running [P1]: spin -f '(!((<>(p1)) || (!([](<>(p0))))))' >'lck-o1-tsT3RZ' +Running [P2]: lbt < 'lck-i1-5TJXmT' >'lck-o2-5E9jb3' +Running [N0]: ltl2tgba -s '(G(F(p0))) -> (F(p1))' >'lck-o0-M3XRO9' +Running [N1]: spin -f '(<>(p1)) || (!([](<>(p0))))' >'lck-o1-6nxqfd' +Running [N2]: lbt < 'lck-i1-4hS5u6' >'lck-o2-vNItGg' +Performing sanity checks and gathering statistics... + +no problem detected +#+end_example + +After this execution, the file =results.csv= contains the following: + +#+BEGIN_SRC sh :results verbatim :exports results +cat results.csv +#+END_SRC +#+RESULTS: +#+begin_example +"formula", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "time", "product_states", "product_transitions", "product_scc" +"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "ltl2tgba -s %f >%N", 3, 5, 9, 1, 3, 2, 1, 0.0453898, 401, 5136, 3 +"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "spin -f %s >%N", 6, 13, 18, 1, 3, 6, 1, 0.0108596, 995, 14384, 5 +"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "lbt < %L >%T", 8, 41, 51, 1, 3, 8, 1, 0.00343479, 1389, 42998, 5 +"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "ltl2tgba -s %f >%N", 4, 10, 16, 1, 3, 0, 0, 0.0437875, 797, 16340, 3 +"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "spin -f %s >%N", 7, 24, 63, 1, 4, 6, 1, 0.0061535, 1400, 64668, 4 +"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "lbt < %L >%T", 39, 286, 614, 3, 28, 33, 1, 0.00384434, 7592, 602204, 4400 +"(!((G(F(p0))) -> (F(p1))))", "ltl2tgba -s %f >%N", 2, 4, 4, 1, 1, 0, 0, 0.0416853, 398, 4198, 1 +"(!((G(F(p0))) -> (F(p1))))", "spin -f %s >%N", 2, 3, 5, 1, 1, 1, 1, 0.00325558, 398, 5227, 1 +"(!((G(F(p0))) -> (F(p1))))", "lbt < %L >%T", 5, 10, 15, 1, 4, 5, 1, 0.00299424, 409, 6401, 12 +"(G(F(p0))) -> (F(p1))", "ltl2tgba -s %f >%N", 3, 5, 11, 1, 3, 1, 1, 0.0422192, 600, 11663, 3 +"(G(F(p0))) -> (F(p1))", "spin -f %s >%N", 3, 5, 14, 1, 3, 1, 1, 0.00293655, 600, 14840, 3 +"(G(F(p0))) -> (F(p1))", "lbt < %L >%T", 11, 18, 54, 2, 11, 5, 1, 0.0030133, 1253, 26891, 457 +#+end_example + +This can be loaded in any spreadsheet application. Although we only +supplied 2 random generated formulas, the output contains 4 formulas because +=ltlcross= had to translate the positive and negative version of each. + +If we had used the option =--json=results.json= instead of +=--cvs=results.csv=, the file =results.json= would have contained the +following [[http://www.json.org/][JSON]] output. + +#+BEGIN_SRC sh :results verbatim :exports results +cat results.json +#+END_SRC +#+RESULTS: +#+begin_example +{ + "tools": [ + "ltl2tgba -s %f >%N", + "spin -f %s >%N", + "lbt < %L >%T" + ], + "inputs": [ + "(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", + "(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", + "(!((G(F(p0))) -> (F(p1))))", + "(G(F(p0))) -> (F(p1))" + ], + "fields": [ + "input", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "time", "product_states", "product_transitions", "product_scc" + ], + "results": [ + [ 0, 0, 3, 5, 9, 1, 3, 2, 1, 0.0431589, 401, 5136, 3 ], + [ 0, 1, 6, 13, 18, 1, 3, 6, 1, 0.0104812, 995, 14384, 5 ], + [ 0, 2, 8, 41, 51, 1, 3, 8, 1, 0.00321619, 1389, 42998, 5 ], + [ 1, 0, 4, 10, 16, 1, 3, 0, 0, 0.0443761, 797, 16340, 3 ], + [ 1, 1, 7, 24, 63, 1, 4, 6, 1, 0.00623927, 1400, 64668, 4 ], + [ 1, 2, 39, 286, 614, 3, 28, 33, 1, 0.00386306, 7592, 602204, 4400 ], + [ 2, 0, 2, 4, 4, 1, 1, 0, 0, 0.0414639, 398, 4198, 1 ], + [ 2, 1, 2, 3, 5, 1, 1, 1, 1, 0.00327304, 398, 5227, 1 ], + [ 2, 2, 5, 10, 15, 1, 4, 5, 1, 0.00322862, 409, 6401, 12 ], + [ 3, 0, 3, 5, 11, 1, 3, 1, 1, 0.0432979, 600, 11663, 3 ], + [ 3, 1, 3, 5, 14, 1, 3, 1, 1, 0.00296043, 600, 14840, 3 ], + [ 3, 2, 11, 18, 54, 2, 11, 5, 1, 0.00295457, 1253, 26891, 457 ] + ] +} +#+end_example + +Here the =fields= table describes the columns of the =results= table, +and the =input= and =tool= columns contains indices relative to the +=inputs= and =tools= table. This format is more compact when dealing +with lots of translators and formulas, because they don't have to be +repeated on each line as in the CSV version. + +JSON data can be easily processed in any language. For instance the +following Python3 script averages each column for each tool, +and presents the results in a form that can almost be copied into a +LaTeX table (the =%= in the tool names have to be taken care of). + +#+BEGIN_SRC python :results output :exports both +#!/usr/bin/python3 +import json +data = json.load(open('results.json')) +datacols = range(2, len(data["fields"])) +# Index results by tool +results = { t:[] for t in range(0, len(data["tools"])) } +for l in data["results"]: + results[l[1]].append(l) +# Average columns for each tools, and display them as a table +print("%-18s &" % "tool", "count &", + " & ".join(data["fields"][2:]), "\\\\") +for i in range(0, len(data["tools"])): + c = len(results[i]) + sums = ["%6.2f" % (sum([x[j] for x in results[i]])/c) + for j in datacols] + print("%-18s & %3d & " % (data["tools"][i], c), + " & ".join(sums), "\\\\") +#+END_SRC +#+RESULTS: +: tool & count & states & edges & transitions & acc & scc & nondetstates & nondeterministic & time & product_states & product_transitions & product_scc \\ +: ltl2tgba -s %f >%N & 4 & 3.00 & 6.00 & 10.00 & 1.00 & 2.50 & 0.75 & 0.50 & 0.04 & 549.00 & 9334.25 & 2.50 \\ +: spin -f %s >%N & 4 & 4.50 & 11.25 & 25.00 & 1.00 & 2.75 & 3.50 & 1.00 & 0.01 & 848.25 & 24779.75 & 3.25 \\ +: lbt < %L >%T & 4 & 15.75 & 88.75 & 183.50 & 1.75 & 11.50 & 12.75 & 1.00 & 0.00 & 2660.75 & 169623.50 & 1218.50 \\ + + +When computing such statistics, you should be aware that inputs for +which a tool failed to generate an automaton (e.g. it crashed, or it +was killed if you used =ltlcross='s =--timeout= option to limit run +time) are not represented in the CSV or JSON files. However data for +bogus automata are still included: as shown below =ltlcross= will +report inconsistencies between automata as errors, but it does not try +to guess who is incorrect. + +* Detecting problems + +If a translator exits with a non-zero status code, or fails to output +an automaton =ltlcross= can read, and error will be displayed and the +result of the translation will be discarded. + +Otherwise =ltlcross= performs the following checks on all translated +formulas ($P_i$ and $N_i$ designate respectively the translation of +positive and negative formulas by the ith translator). + + - Intersection check: $P_i\otimes N_j$ must be empty for all + pairs of $(i,j)$. + + A single failing translator might generate a lot of lines of + the form: + + : error: P0*N1 is nonempty + : error: P1*N0 is nonempty + : error: P1*N1 is nonempty + : error: P1*N2 is nonempty + : error: P1*N3 is nonempty + : error: P1*N4 is nonempty + : error: P1*N5 is nonempty + : error: P1*N6 is nonempty + : error: P1*N7 is nonempty + : error: P1*N8 is nonempty + : error: P1*N9 is nonempty + : error: P2*N1 is nonempty + : error: P3*N1 is nonempty + : error: P4*N1 is nonempty + : error: P5*N1 is nonempty + : error: P6*N1 is nonempty + : error: P7*N1 is nonempty + : error: P8*N1 is nonempty + : error: P9*N1 is nonempty + + In this example, translator number =1= looks clearly faulty + (at least the other 9 translators do not contradict each other). + + - Cross-comparison checks: for some state-space $S$, + all $P_i\otimes S$ are either all empty, or all non-empty. + Similarly all $N_i\otimes S$ are either all empty, or all non-empty. + + A cross-comparison failure could be displayed as: + + : error: {P0,P2,P3,P4,P5,P6,P7,P8,P9} disagree with {P1} when evaluating the state-space + + - Consistency check: + + For each $i$, the products $P_i\otimes S$ and $N_i\otimes S$ + actually cover all states of $S$. Because $S$ does not have any + deadlock, any of its infinite path must be accepted by $P_i$ or + $N_i$ (or both). + + An error in that case is displayed as + + : error: inconsistency between P1 and N1 + +The above checks are the same that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]]. + +If any problem was reported during the translation of one of the +formulas, =ltlcheck= will exit with an exit status of =1=. Statistics +(if requested) are output nonetheless, and include any faulty +automaton as well. + +* Miscellaneous options + +** =--stop-on-error= + +The =--stop-on-error= will cause =ltlcross= to abort on the first +detected error. This include failure to start some translator, read +its output, or failure to passe the sanity checks. Timeouts are +allowed. + +One use for this option is when =ltlcross= is used in combination with +=randltl= to check translators on an infinite stream of formulas. + +For instance the following will cross-compare =ltl2tgba= against +=ltl3ba= until it finds an error, or your interrupt the command, or it +runs out of memory (the hash tables used by =randltl= and =ltlcross= +to remove duplicate formulas will keep growing). + +#+BEGIN_SRC sh :export code :eval no +randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' +#+END_SRC + +** =--no-check= + +The =--no-check= option disables all sanity checks, and only use the supplied +formulas in their positive form. + +When checks are enabled, the negated formulas are intermixed with the +positives ones in the results. Therefore the =--no-check= option can +be used to gather statistics about a specific set of formulas. + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t) (python . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# eval: (setq org-babel-python-command "/usr/bin/python3") +# End: + +# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed +# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY +# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella +# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ +# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO +# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic +# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq +# LocalWords: setenv concat getenv diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org new file mode 100644 index 000000000..c642aa273 --- /dev/null +++ b/doc/org/ltlfilt.org @@ -0,0 +1,233 @@ +#+TITLE: =ltlfilt= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This tool is a filter for LTL formulas. (It will also work with PSL +formulas.) It can be used to perform a number of tasks. Essentially: +- converting formulas from one syntax to another, +- transforming formulas, +- selecting formulas matching some criterion. + +* Changing syntaxes + +Because it read and write formulas, =ltlfilt= accepts +all the [[file:ioltl.org][common input and output options]]. + +Additionally, if no =-f= or =-F= option is specified, =ltlfilt= +will read formulas from the standard input. + +For instance the following will convert two LTL formulas expressed +using infix notation (with different names supported for the same +operators) and convert it into LBT's syntax. + +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt -l -f 'p1 U (p2 & GFp3)' -f 'X<>[]p4' +#+END_SRC +#+RESULTS: +: U p1 & p2 G F p3 +: X F G p4 + +Conversely, here is how to rewrite formulas expressed using the +LBT's Polish notation. Let's take the following four formulas +taken from examples distributed with =scheck=: +#+BEGIN_SRC sh :results verbatim :exports both +cat >scheck.ltl<= INT + --equivalent-to=FORMULA match formulas equivalent to FORMULA + --eventual match pure eventualities + --guarantee match guarantee formulas (even pathological) + --implied-by=FORMULA match formulas implied by FORMULA + --imply=FORMULA match formulas implying FORMULA + --ltl match only LTL formulas (no PSL operator) + --nox match X-free formulas + --obligation match obligation formulas (even pathological) + --safety match safety formulas (even pathological) + --size-max=INT match formulas with size <= INT + --size-min=INT match formulas with size >= INT + --syntactic-guarantee match syntactic-guarantee formulas + --syntactic-obligation match syntactic-obligation formulas + --syntactic-persistence match syntactic-persistence formulas + --syntactic-recurrence match syntactic-recurrence formulas + --syntactic-safety match syntactic-safety formulas + --universal match purely universal formulas + -u, --unique drop formulas that have already been output (not + affected by -v) + -v, --invert-match select non-matching formulas +#+end_example + +Most of the above options should be self-explanatory. For instance +the following command will extract all formulas from =scheck.ltl= +which do not represent guarantee properties. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --lbt-input -F scheck.ltl -v --guarantee +#+END_SRC +#+RESULTS: +: !(Gp0 | (Gp1 & Fp3)) + +Combining =ltlfilt= with [[file:randltl.org][=randltl=]] makes it easier to generate random +formulas that respect certain constraints. For instance let us +generate 10 formulas that are equivalent to =a U b=: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' | head -n 10 +#+END_SRC +#+RESULTS: +#+begin_example +!(!a R !b) +(!Gb -> a) U b +a U b +Fb & (a W b) +((a <-> !(a | b)) W a) U ((!b M b) U b) +(b <-> (Xb M a)) -> b +(a | b) U b +((!b U b) -> (a W b)) U b +(a xor b) U b +b R (Fb & (a U (a W b))) +#+end_example + +The =-n -1= option to =randltl= will cause it to output an infinite +stream of random formulas. =ltlfilt=, which reads its standard input +by default, will select only those equivalent to =a U b=. The output +of =ltlfilt= would still be an infinite stream of random formulas, so +we display only the first 10 using the standard =head= utility. Less +trivial formulas could be obtained by adding the =-r= option to +=randltl= (or equivalently adding the =-r= and =-u= option to +=ltlfilt=). + + +Another similar example, that requires two calls to =ltlfilt=, is the +generation of random pathological safety formulas. Pathological +safety formulas are safety formulas that do not /look/ so +syntactically. We can generate some starting again with =randltl=, +then ignoring all syntactic safety formulas, and keeping only the +safety formulas in the remaining list. + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety | head -n 10 +#+END_SRC +#+RESULTS: +#+begin_example +(!a & Fa) R Xa +!a | (a & b) | (((!a & b) | (a & !b)) M (!a M X!a)) +G(!a M Xa) +G((G!b & !a) | (a & Fb)) R a +G!a M !a +G(!a M ((!b & XGb) | (b & XF!b))) +F(b | G!b) +F(Xa | G!a) +G(XXa | (b & F!a)) +G((!a & (!a M !b)) | (a & (a W b))) +#+end_example + + +=ltlfilt='s filtering ability can also be used to answer questions +about a single formula. For instance is =a U (b U a)= equivalent to +=b U a=? + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a' +#+END_SRC +#+RESULTS: +: a U (b U a) + +The commands prints the formula and returns an exit status of 0 if the +two formulas are equivalent. It would print nothing and set the exit +status to 1, were the two formulas not equivalent. + + + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck +# LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc +# LocalWords: pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb +# LocalWords: XF XXa diff --git a/doc/org/randltl.org b/doc/org/randltl.org new file mode 100644 index 000000000..b16fdaaed --- /dev/null +++ b/doc/org/randltl.org @@ -0,0 +1,327 @@ +#+TITLE: =randltl= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This tool generates random formulas. By default, it will generate one +random LTL formula using atomic propositions supplied on the +command-line. It can be instructed to generate random Boolean or PSL +formulas instead, but let us first focus on LTL generation. + +For instance to obtain one random LTL formula over the propositions +=a=, =b=, or =c=, use: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl a b c +#+END_SRC +#+RESULTS: +: G(Gb W (Gb M c)) + +Note that the result does not always use all atomic propositions. + +The syntax of the formula output can be changed using the +[[file:ioltl.org][common output options]]: + +#+BEGIN_SRC sh :results verbatim :exports results +randltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +: -8, --utf8 output using UTF-8 characters +: -l, --lbt output in LBT's syntax +: -p, --full-parentheses output fully-parenthesized formulas +: -s, --spin output in Spin's syntax +: --spot output in Spot's syntax (default) +: --wring output in Wring's syntax + +When you select Spin's or Wring's syntax, operators =W= and =M= are +automatically rewritten using =U= and =R= (written =V= for Spin). +When you select LBT's syntax, you should name you atomic propositions +like =p0=, =p1=, etc... (Atomic proposition named differently will be +output by Spot in double-quotes, but this is not supported by LBT.) + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -l p1 p2 p3 +randltl -8 p1 p2 p3 +randltl -s p1 p2 p3 +randltl --wring p1 p2 p3 +#+END_SRC +#+RESULTS: +: G W G p2 M G p2 p3 +: □(□p2 W (□p2 M p3)) +: []((p3 U (p3 && []p2)) V ([]p2 || (p3 U (p3 && []p2)))) +: (G(((p3=1) U ((p3=1) * (G(p2=1)))) R ((G(p2=1)) + ((p3=1) U ((p3=1) * (G(p2=1))))))) + +As you might guess from the above result, for a given set of atomic +propositions (and on the same computer) the generated formula will +always be the same. This is because each time =randltl= starts, it +initialize the seed of the random number generator to =0=. This seed +can be changed using the =--seed= option. For instance the following +three commands: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl a b c +randltl --seed=123 a b c +randltl --seed=0 a b c +#+END_SRC + +Will give three formulas in which the first and last are identical: + +#+RESULTS: +: G(Gb W (Gb M c)) +: X((c <-> F(a M Xc)) -> a) +: G(Gb W (Gb M c)) + +When generating random formulas, we usually want large quantity of +them. Rather than running =randltl= several times with different +seeds, we can use the =-n= option to specify a number of formulas to +produce. + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 5 a b c +#+END_SRC +#+RESULTS: +: G(Gb W (Gb M c)) +: !(GFb -> Fa) +: (((c xor Xc) R c) R Gc) & !c +: X(1 U Xb) M Fb +: !XFb U !(Xa W 0) + +By default =randltl= will never output the same formula twice (this +can be changed with the =--allow-dups= option), so it may generate +more formulas internally than it eventually prints. To ensure +termination, for each output formula the number of ignored (because +duplicated) random formulas that are generated is limited to 100000. +Therefore in some situations, most likely when generating small +formulas, with few atomic proposition, you may see =randltl= stop +before the requested number of formulas has been output with an error +message. + +If the integer passed to =-n= is negative, =randltl= will attempt to +generate as many formulas as it can. This is most useful when +=randltl= is piped to =ltlfilt= to select random formulas matching a +certain criterion, as we shall see later. + +Besides the list of atomic propositions (=a b c= in our example) and +the seed, several other parameters control the generation of the +random formulas. + +Initially, the random generator selects a tree size for the formula. +The default size is =15=, but it can be changed using the =--tree-size= +option. For instance in the following, for each formula the tree size +will be chosen randomly in the range =22..30=. +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 5 a b c --tree-size=22..30 +#+END_SRC +#+RESULTS: +: ((Fc W 0) M 1) & ((a | XXc) M (b W Fb)) +: (!(c | (a R Xb)) <-> (Xc R (a & c))) -> !a +: 0 +: X(Xc R GX(1 U Xb)) & GX(b M Xc) +: (!b -> ((c xor Fa) W b)) W (!Fb U a) + +The tree size is just the number of nodes in the syntax tree of the +formula during its construction. However because Spot automatically +applies some /trivial simplifications/ during the construction of its +formulas (e.g., =F(F(a)= is reduced to =F(a)=, =a&0= to =0=, etc.), +the actual size of the formula output may be smaller than the +tree size specified. + +It is pretty common to obtain the formulas =0= or =1= among the first +formulas output, since many random formulas trivially simplify to +these. However because duplicate formulas are suppressed by default, +they shall only occur once. + +Stronger simplifications may be requested using the =-r= option, that +implements many rewritings that helps Spot translators algorithms (so +beware that using =-r= reduces the randomness of the output). + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 5 a b c --tree-size=22..30 -r +#+END_SRC +#+RESULTS: +: GFc & ((a | XXc) M Fb) +: !a | (!c & (!a U X!b)) | (a & c & Xc) +: 0 +: XG(b M Xc) +: (((!c & Fa) | (c & G!a)) W b) W (G!b U a) + +The generator build the syntax tree recursively from its root, by +considering all operators that could be used for a given tree size (for +example a tree-size of 2 disables binary operators). A /priority/ is +associated to each operator, and the probability of this operator +being selected is this priority over the sum of the priorities of all +considered operators. The default priorities for each operator can +be seen with =--dump-priorities=: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl a b c --dump-priorities +#+END_SRC +#+RESULTS: +#+begin_example +Use --ltl-priorities to set the following LTL priorities: +ap 3 +false 1 +true 1 +not 1 +F 1 +G 1 +X 1 +equiv 1 +implies 1 +xor 1 +R 1 +U 1 +W 1 +M 1 +and 1 +or 1 +#+end_example + +Where =ap= stands for /atomic propositions/ (=a=, =b=, =c=). In this +example, when the generator builds a leaf of the syntax tree (i.e., a +subformula of tree-size 1), it must ignore all operators, and chose +between =ap=, =false=, or =true=, and the odds of choosing =ap= is +3/(3+1+1). + +As indicated at the top of the output, these priorities can be changed +using the =--ltl-priorities= options. The most common scenario is to +disable some of the operators by giving them a null priority. The +following example disables 6 operators, and augments the priority of +=U= to 3 to favor its occurrence. + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 5 a b c --ltl-priorities 'xor=0,implies=0,equiv=0,W=0,M=0,X=0,U=3' +#+END_SRC +#+RESULTS: +: F(Fb U (c & Gb)) +: !(Fb U Fa) +: ((Gc U c) U c) U Fc +: 0 +: 1 + +When using =-r= to simplify generated formulas, beware that these +rewritings may use operators that you disabled during the initial +random generation: you may obtain a formula that uses =W= even if =W= +has a null priority. (You can use =ltlfilt= to rewrite these +operators if that is a problem.) + +If the =--weak-fairness= option is used, for each random formula +generated, a weak-fairness formula of the form =GF(a) & GF(b) & GF(c)= +is generated for a subset of the atomic propositions and "ANDed" to +the random formula. The =--tree-size= option has no influence on the +weak-fairness formula appended. + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 5 a b c --weak-fairness +#+END_SRC +#+RESULTS: +: G(Gb W (Gb M c)) & GFb +: GFb & !(GFb -> Fa) & GFa +: GFb & (((c xor Xc) R c) R Gc) & !c +: GFb & GFa & (X(1 U Xb) M Fb) +: GFb & (!XFb U !(Xa W 0)) & GFc + + +Boolean formulas may be output with the =-B= option: +#+BEGIN_SRC sh :results verbatim :exports both +randltl -B -n 5 a b c +#+END_SRC +#+RESULTS: +: !a -> !b +: !(!(a -> (b xor c)) -> !a) +: !c | (!c xor (c xor (c xor !c))) +: !b +: a xor !(!b <-> (!a -> c)) + +In that case, priorities should be set with =--boolean-priorities=. + +Finally, PSL formulas may be output using the =-P= option. However +keep in mind that since LTL formulas are PSL formulas, generating +random PSL formula may produce many LTL formulas that do not use any +PSL operator (this is even more so the case when simplifications are +enabled with =-r=). + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -P -n 5 a b c +#+END_SRC +#+RESULTS: +: G(Gb M ((c & Xb) | (!a M 1))) +: !(Fa xor X({{c | {a xor !b}}[*]}[]-> Fb)) +: c & Gc +: 0 +: 1 + +As shown with the =--dump-priorities= output below, tweaking the +priorities used to generated PSL formulas requires three different +options: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -P a b c --dump-priorities +#+END_SRC +#+RESULTS: +#+begin_example +Use --ltl-priorities to set the following LTL priorities: +ap 3 +false 1 +true 1 +not 1 +F 1 +G 1 +X 1 +Closure 1 +equiv 1 +implies 1 +xor 1 +R 1 +U 1 +W 1 +M 1 +and 1 +or 1 +EConcat 1 +UConcat 1 +Use --sere-priorities to set the following SERE priorities: +eword 1 +boolform 1 +star 1 +star_b 1 +and 1 +andNLM 1 +or 1 +concat 1 +fusion 1 +Use --boolean-priorities to set the following Boolean formula priorities: +ap 3 +false 1 +true 1 +not 1 +equiv 1 +implies 1 +xor 1 +and 1 +or 1 +#+end_example + +The =--ltl-priorities= option we have seen previously now recognize +some new PSL-specific operators: =Closure= is the ={sere}= operator, +=EConcat= is the ={sere}<>->f= operator, and =UConcat= is the +={sere}[]->f= operator. When these operator are selected, they +require a SERE argument which is generated according to the priorities +set by =--sere-priorities=: =eword= is the empty word, =boolform= is a +Boolean formula (generated using the priorities set by +=--boolean-priorities=), =star= is the unbounded Kleen star, while +=star_b= is the bounded version, and =andNLM= is the +non-length-matching variant of the =and= operator. + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: randltl num toc LTL PSL SRC Gb sed utf UTF lbt LBT's +# LocalWords: Xc GFb Gc Xb Fb XFb Xa dups ltlfilt Fc XXc GX GFc XG +# LocalWords: rewritings ltl ap GF ANDed GFa boolean EConcat eword +# LocalWords: UConcat boolform andNLM concat Kleen eval setenv setq +# LocalWords: getenv diff --git a/doc/org/tools.org b/doc/org/tools.org new file mode 100644 index 000000000..41e51811b --- /dev/null +++ b/doc/org/tools.org @@ -0,0 +1,55 @@ +#+TITLE: Command-line tools installed by Spot 1.0 +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t + +This document introduces command-line tools that are installed with +the Spot library. We give some examples to highlight possible +use-cases but shall not attempt to cover all features exhaustively +(please check the man pages for further inspiration). + +* Conventions + +For technical reasons related to the way we generate these pages, we +use the following convention when rendering shell commands. The +commands issued to the shell are formatted like this with a green line +on the left: + +#+NAME: helloworld +#+BEGIN_SRC sh :results verbatim :exports both +echo Hello World +#+END_SRC + +And the output of such a command is formatted as follows, with a red +line on the left: + +#+RESULTS: helloworld +: Hello World + +Parts of these documents (e.g., lists of options) are actually the +results of shell commands and will be presented as above, even if the +corresponding commands are hidden. + +* Common options + +- [[file:ioltl.org][common input and output options for LTL/PSL formulas]] + +* Command-line tools + +- [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas. +- [[file:ltlfilt.org][=ltlfilt=]] Filter LTL/PSL formulas. +- [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns. +- [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into Büchi automata. +- [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata. +- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-Büchi translators. + + +# Local variables: +# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH"))) +# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t))) +# eval: (setq org-confirm-babel-evaluate nil) +# End: + + +# LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl +# LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval +# LocalWords: setenv concat getenv setq