From d0b38156f3eff528b94dc02cce6347dd74603bd0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 8 Jan 2016 12:07:30 +0100 Subject: [PATCH] bin: make HOA the default output * bin/common_aoutput.cc: Make HOA the default output. * NEWS: Mention this. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org, tests/core/dstar.test, tests/core/ltldo2.test, tests/core/monitor.test, tests/python/piperead.ipynb: Adjust. --- NEWS | 9 ++++ bin/common_aoutput.cc | 6 +-- doc/org/autfilt.org | 34 ++++++++---- doc/org/dstar2tgba.org | 71 ++++++++++++++----------- doc/org/hoa.org | 16 +++--- doc/org/ltl2tgba.org | 102 ++++++++++++++++++++---------------- doc/org/ltl2tgta.org | 27 ++++++---- doc/org/ltlcross.org | 8 +-- doc/org/ltldo.org | 53 +++++++++++-------- doc/org/oaut.org | 66 ++++++++++++----------- doc/org/randaut.org | 82 ++++++++++++++++------------- doc/org/satmin.org | 11 ++-- doc/org/tut02.org | 3 -- doc/org/tut03.org | 1 - doc/org/tut20.org | 5 +- doc/org/tut21.org | 6 ++- doc/org/tut30.org | 19 ++++--- tests/core/dstar.test | 10 ++-- tests/core/ltldo2.test | 4 +- tests/core/monitor.test | 6 +-- tests/python/piperead.ipynb | 38 ++++++++------ 21 files changed, 327 insertions(+), 250 deletions(-) diff --git a/NEWS b/NEWS index 7540371b2..f291cd94e 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,15 @@ New in spot 1.99.6a (not yet released) Command-line tools: + * BACKWARD INCOMPATIBILE CHANGE: All tools that output automata now + use the HOA format by default instead of the GraphViz output. + This makes it easier to pipe several commands. + + If you have an old script that relies on GraphViz being the default + output and that you do not want to update it, use + export SPOT_DEFAULT_FORMAT=dot + to get the old behavior back. + * Tools that output automata now accept -d as a shorthand for --dot. randaut's short option for specifying edge-density used to be -d: it has been renamed to -e. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 9ade197f9..482126d40 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -35,7 +35,7 @@ #include #include -automaton_format_t automaton_format = Dot; +automaton_format_t automaton_format = Hoa; static const char* automaton_format_opt = nullptr; const char* opt_name = nullptr; static const char* opt_output = nullptr; @@ -82,7 +82,7 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, "Output format:", 3 }, { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT", OPTION_ARG_OPTIONAL, - "GraphViz's format (default). Add letters for " + "GraphViz's format. 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, " @@ -95,7 +95,7 @@ static const argp_option options[] = "(t) force transition-based acceptance, " "(+INT) add INT to all set numbers", 0 }, { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL, - "Output the automaton in HOA format. Add letters to select " + "Output the automaton in HOA format (default). Add letters to select " "(i) use implicit labels for complete deterministic automata, " "(s) prefer state-based acceptance when possible [default], " "(t) force transition-based acceptance, " diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 13dff0990..46e4270a5 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -27,8 +27,9 @@ process them in batch. (The only restriction is that inside a file an automaton in LBTT's format may not follow an automaton in =ltl2dstar='s format.) -The output format can be controlled using [[file:oaut.org][the common output options]] -(like =--spin=, =--lbtt=, =--dot=, =--hoaf=...). +By default the output uses the HOA format. This can be changed using +[[file:oaut.org][the common output options]] like =--spin=, =--lbtt=, =--dot=, +=--hoaf=... #+BEGIN_SRC sh :results silent :exports both cat >example.hoa < 0 : 0 [label="0"] @@ -102,7 +104,7 @@ statistics. #+BEGIN_SRC sh :results verbatim :exports both -randaut --hoa -n 10 -A0..2 -Q10..20 -e0.05 2 | +randaut -n 10 -A0..2 -Q10..20 -e0.05 2 | autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d' #+END_SRC @@ -127,17 +129,20 @@ autfilt --help | sed -n '/^ %%/,/^$/p' | sed '$d' #+RESULTS: #+begin_example %% a single % - %A, %a number of acceptance pairs or sets + %A, %a number of acceptance sets %C, %c number of SCCs %d 1 if the output is deterministic, 0 otherwise %E, %e number of edges %F name of the input file + %G, %g acceptance condition (in HOA syntax) + %L location in the input file + %M, %m name of the automaton %n number of nondeterministic states in output %p 1 if the output is complete, 0 otherwise - %r conversion time (including post-processings, but - not parsing) in seconds + %r processing time (excluding parsing) in seconds %S, %s number of states %T, %t number of transitions + %w one word accepted by the output automaton #+end_example When a letter is available both as uppercase and lowercase, the @@ -166,6 +171,10 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d' --is-complete keep complete automata --is-deterministic keep deterministic automata --is-empty keep automata with an empty language + --is-inherently-weak keep only inherently weak automata + --is-terminal keep only terminal automata + --is-unambiguous keep only unambiguous automata + --is-weak keep only weak automata --states=RANGE keep automata whose number of states are in RANGE -u, --unique do not output the same automaton twice (same in the sense that they are isomorphic) @@ -193,14 +202,14 @@ This set of options controls the desired type of output automaton: autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -B, --ba Büchi Automaton (with state-based acceptance) +: -B, --ba Büchi Automaton (with state-based acceptance) : -C, --complete output a complete automaton -: --generic Any acceptance is allowed (default) +: --generic any acceptance is allowed (default) : -M, --monitor Monitor (accepts all finite prefixes of the given : property) : -S, --state-based-acceptance, --sbacc : define the acceptance using states -: --tgba Transition-based Generalized Büchi Automaton +: --tgba Transition-based Generalized Büchi Automaton These options specify any simplification goal: @@ -251,6 +260,9 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' deterministic automata) --complement-acceptance complement the acceptance condition (without touching the automaton) + --decompose-strength=t|w|s extract the (t) terminal, (w) weak, or (s) + strong part of an automaton (letters may be + combined to combine more strengths in the output) --destut allow less stuttering --dnf-acceptance put the acceptance condition in Disjunctive Normal Form @@ -279,8 +291,8 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' quantification, or by assigning them 0 or 1 --remove-dead-states remove states that are unreachable, or that cannot belong to an infinite path - --remove-fin rewrite the automaton without using Fin acceptance - + --remove-fin rewrite the automaton without using Fin + acceptance --remove-unreachable-states remove states that are unreachable from the initial state diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index e69ac7438..70122ed3e 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -4,16 +4,21 @@ #+HTML_LINK_UP: tools.html This tool converts automata into transition-based generalized Büchi -automata, a.k.a., TGBA. +automata, a.k.a., TGBA. It can also produce Büchi automata on request +(=-B=). It's usage is almost similar to [[file:ltl2tgba.org][=ltl2tgba=]] except that +instead of supplying a formula to translate, you should specify a +filename containing the automaton to convert. In earlier version (before Spot 1.99.4) =dstar2tgba= was only able to -read automata written in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]], hence its -name. However nowadays it can read automata in any of the supported -formats ([[file:hoa.org][HOA]], LBTT's format, ltl2dstar's format, and never claims). +read automata written in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]]. However +nowadays it can read automata in any of the supported formats ([[file:hoa.org][HOA]], +LBTT's format, ltl2dstar's format, and never claims). Also +=dstar2tgba= used to be the only tool being able to read ltl2dstar's +format, but today this format can also be read by any of the tool that +read automata. So in practice, running =dstar2tgba some files...= +produces the same result as running =autfilt --tgba --high --small +some files...=. -It's usage is almost similar to [[file:ltl2tgba.org][=ltl2tgba=]] except that instead of -supplying a formula to translate, you should specify a filename -containing the automaton to convert. * Two quick examples @@ -127,7 +132,7 @@ For instance here is the conversion to a Büchi automaton (=-B=): #+NAME: fagfb2ba #+BEGIN_SRC sh :results verbatim :exports code -dstar2tgba -B fagfb +dstar2tgba -B fagfb -d #+END_SRC #+RESULTS: fagfb2ba #+begin_example @@ -172,18 +177,18 @@ dstar2tgba -s fagfb never { T0_init: if - :: ((b)) -> goto accept_S0 + :: (b) -> goto accept_S0 :: ((a) && (!(b))) -> goto T0_init fi; accept_S0: if - :: ((b)) -> goto accept_S0 - :: ((!(b))) -> goto T0_S2 + :: (b) -> goto accept_S0 + :: (!(b)) -> goto T0_S2 fi; T0_S2: if - :: ((b)) -> goto accept_S0 - :: ((!(b))) -> goto T0_S2 + :: (b) -> goto accept_S0 + :: (!(b)) -> goto T0_S2 fi; } #+end_example @@ -252,7 +257,7 @@ the default: #+NAME: gfagfb2ba #+BEGIN_SRC sh :results verbatim :exports code -dstar2tgba gfagfb +dstar2tgba gfagfb -d #+END_SRC #+RESULTS: gfagfb2ba #+begin_example @@ -309,9 +314,10 @@ The =dstar2tgba= tool implements a 4-step process: 3. postprocess the resulting TGBA (simplifying the automaton, a degeneralizing it into a BA or Monitor if requested) 4. output the resulting automaton -BTW, the above scenario is also exactly what you can with [[file:autfilt.org][=autfilt=]] if -you run it as =autfilt --tgba --high --small=. (This is true only since version -1.99.4, since both tools can now read the same file formats.) +BTW, the above scenario is also exactly what you get with [[file:autfilt.org][=autfilt=]] if +you run it as =autfilt --tgba --high --small=. (This is true only +since version 1.99.4, since both tools can now read the same file +formats.) ** Controlling output @@ -324,13 +330,13 @@ dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -B, --ba Büchi Automaton (implies -S) +: -B, --ba Büchi Automaton (implies -S) : -C, --complete output a complete automaton : -M, --monitor Monitor (accepts all finite prefixes of the given : property) : -S, --state-based-acceptance, --sbacc : define the acceptance using states -: --tgba Transition-based Generalized Büchi Automaton +: --tgba Transition-based Generalized Büchi Automaton : (default) And these may be refined by a simplification goal, should the @@ -370,10 +376,11 @@ dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' --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) + 'unambiguous', 'stutter-invariant', or 'strength'. + + -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] + GraphViz's format. 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 @@ -381,14 +388,16 @@ dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' (n) with name, (N) without name, (o) ordered transitions, (r) rainbow colors for acceptance sets, (R) color acceptance sets by Inf/Fin, (s) - with SCCs, (t) force transition-based acceptance. - -H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. Add letters - to select (i) use implicit labels for complete - deterministic automata, (s) prefer state-based - acceptance when possible [default], (t) force - transition-based acceptance, (m) mix state and - transition-based acceptance, (l) single-line - output + with SCCs, (t) force transition-based acceptance, + (+INT) add INT to all set numbers + -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format (default). Add + letters to select (i) use implicit labels for + complete deterministic automata, (s) prefer + state-based acceptance when possible [default], + (t) force transition-based acceptance, (m) mix + state and transition-based acceptance, (k) use + state labels when possible, (l) single-line + output, (v) verbose properties --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 95e2c5005..aa441c730 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -33,7 +33,7 @@ When an HOA file is loaded by Spot, it is stored into the data-structure used by Spot to represent ω-Automata. This structure is called Transition-based ω-Automaton, henceforth abbreviated TωA. Such a TωA can be saved back as an HOA file. If you run a command -such as =autfilt -H input.hoa >output.hoa= this is exactly what +such as =autfilt input.hoa >output.hoa= this is exactly what happens: the file =input.hoa= is parsed to create a TωA, and this TωA is then printed in the HOA format into =output.hoa=. @@ -221,7 +221,7 @@ State: 2 [0] 2 {0 1} --END-- EOF_HOA -autfilt -H sba.hoa +autfilt sba.hoa #+END_SRC so the HOA output of =autfilt= automatically uses state-based acceptance: @@ -432,7 +432,7 @@ Rabin pair, and reordering the remaining pair to fit the syntax corresponding to =Rabin 1=. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -autfilt -H < 1 - 0 [label="0"] - 0 -> 0 [label="b\n{0}"] - 0 -> 0 [label="!b"] - 1 [label="1"] - 1 -> 0 [label="a"] - 1 -> 1 [label="!a"] -} +HOA: v1 +name: "Fa & GFb" +States: 2 +Start: 1 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 +[1] 0 {0} +[!1] 0 +State: 1 +[0] 0 +[!0] 1 +--END-- #+end_example Actually, because =ltl2tgba= is often used with a single formula @@ -42,11 +46,14 @@ assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltl where such parameters are assumed to be filenames). =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]]. -The default output format, as shown above, is [[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 +The default output format, as shown above, is the [[file:hoa.org][HOA]] format, as this +can easily be piped to other tools. + +To convert the automaton into a picture, or into vectorial format, use +=--dot= or =-d= to request [[http://www.graphviz.org/][GraphViz output]] and process the result with +=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 +ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf #+END_SRC #+RESULTS: @@ -55,12 +62,13 @@ we use some [[file:oaut.org][environment variables]] to produce a more colorful output by default) #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba "Fa & GFb" +ltl2tgba "Fa & GFb" -d #+END_SRC #+RESULTS: dotex #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] @@ -99,7 +107,7 @@ Here is a TGBA with multiple acceptance sets (we omit the call to #+NAME: dotex2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" +ltl2tgba "GFa & GFb" -d #+END_SRC #+RESULTS: dotex2 #+begin_example @@ -134,7 +142,7 @@ A Büchi automaton for the previous formula can be obtained with the #+NAME: dotex2ba #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -B 'GFa & GFb' +ltl2tgba -B 'GFa & GFb' -d #+END_SRC #+RESULTS: dotex2ba #+begin_example @@ -220,7 +228,7 @@ as above, for comparison. #+NAME: dotex2gba #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -S 'GFa & GFb' +ltl2tgba -S 'GFa & GFb' -d #+END_SRC #+RESULTS: dotex2gba @@ -282,27 +290,30 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' --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) + 'unambiguous', 'stutter-invariant', or + 'strength'. + -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] + GraphViz's format. 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 + Büchi/co-Büchi automata, (c) force circular nodes, (e) force elliptic nodes, (f(FONT)) use FONT, (h) horizontal layout, (v) vertical layout, (n) with name, (N) without name, (o) ordered transitions, (r) rainbow colors for acceptance sets, (R) color acceptance sets by Inf/Fin, (s) - with SCCs, (t) force transition-based acceptance. - -H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. Add letters - to select (i) use implicit labels for complete - deterministic automata, (s) prefer state-based - acceptance when possible [default], (t) force - transition-based acceptance, (m) mix state and - transition-based acceptance, (l) single-line - output + with SCCs, (t) force transition-based acceptance, + (+INT) add INT to all set numbers + -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format (default). Add + letters to select (i) use implicit labels for + complete deterministic automata, (s) prefer + state-based acceptance when possible [default], + (t) force transition-based acceptance, (m) mix + state and transition-based acceptance, (k) use + state labels when possible, (l) single-line + output, (v) verbose properties --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 @@ -319,7 +330,7 @@ if your system can display UTF-8 correctly. #+NAME: dotex2ba8 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -B8 "GFa & GFb" +ltl2tgba -B8 "GFa & GFb" -d #+END_SRC #+RESULTS: dotex2ba8 #+begin_example @@ -442,7 +453,7 @@ flagrant is =Ga|Gb|Gc=: #+NAME: gagbgc1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba 'Ga|Gb|Gc' +ltl2tgba 'Ga|Gb|Gc' -d #+END_SRC #+RESULTS: gagbgc1 #+begin_example @@ -476,7 +487,7 @@ $txt #+NAME: gagbgc2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -D 'Ga|Gb|Gc' +ltl2tgba -D 'Ga|Gb|Gc' -d #+END_SRC #+RESULTS: gagbgc2 #+begin_example @@ -544,7 +555,7 @@ $\bar ab$. #+NAME: ambig1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -B 'GFa -> GFb' +ltl2tgba -B 'GFa -> GFb' -d #+END_SRC #+RESULTS: ambig1 #+begin_example @@ -583,7 +594,7 @@ is only one run that recognizes this example word: #+NAME: ambig2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -B -U 'GFa -> GFb' +ltl2tgba -B -U 'GFa -> GFb' -d #+END_SRC #+RESULTS: ambig2 @@ -713,6 +724,7 @@ ltl2tgba --help | sed -n '/^ *%/p' %e number of edges %f the formula, in Spot's syntax %F name of the input file + %g acceptance condition (in HOA syntax) %L location in the input file %m name of the automaton %n number of nondeterministic states in output @@ -771,13 +783,14 @@ deterministic monitor for the given formula. #+NAME: monitor1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -M '(Xa & Fb) | Gc' +ltl2tgba -M '(Xa & Fb) | Gc' -d #+END_SRC #+RESULTS: monitor1 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] @@ -805,13 +818,14 @@ $txt #+NAME: monitor2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -MD '(Xa & Fb) | Gc' +ltl2tgba -MD '(Xa & Fb) | Gc' -d #+END_SRC #+RESULTS: monitor2 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index f850de106..ff290d87f 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -22,21 +22,26 @@ ltl2tgta --ta --multiple-init 'a U Gb' #+RESULTS: #+begin_example digraph G { + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] -1 [label="", style=invis, height=0] - -1 -> 1 [label="!a & b"] + -1 -> 1 [label="a & b"] -2 [label="", style=invis, height=0] - -2 -> 2 [label="a & b"] + -2 -> 2 [label="a & !b"] -3 [label="", style=invis, height=0] - -3 -> 3 [label="a & !b"] - 1 [label="2\n!a & b",shape=box] + -3 -> 3 [label="!a & b"] + 1 [label="2\na & b",shape=box] 1 -> 4 [label="{a}\n"] - 2 [label="1\na & b",shape=box] - 2 -> 4 [label="{a}\n"] - 2 -> 1 [label="{a}\n"] - 2 -> 3 [label="{b}\n"] - 3 [label="0\na & !b"] - 3 -> 2 [label="{b}\n"] - 3 -> 1 [label="{a, b}\n"] + 1 -> 3 [label="{a}\n"] + 1 -> 2 [label="{b}\n"] + 2 [label="1\na & !b"] + 2 -> 1 [label="{b}\n"] + 2 -> 3 [label="{a, b}\n"] + 3 [label="0\n!a & b",shape=box] + 3 -> 4 [label="{a}\n"] 4 [label="3",peripheries=2,shape=box] 4 -> 4 [label="{a}\n{0}"] } diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 6cc13c175..887b77c47 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -128,10 +128,10 @@ tools: - '=modella -r12 -g -e %L %O=' - '=/path/to/script4lbtt.py %L %O=' (script supplied by [[http://web.archive.org/web/20070214050826/http://estragon.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for its interface with LBTT) - - '=ltl2tgba -s %s >%O=' (smaller output, Büchi automaton) - - '=ltl2tgba -s -D %s >%O=' (more deterministic output, Büchi automaton) - - '=ltl2tgba -H %s >%O=' (smaller output, TGBA) - - '=ltl2tgba -H -D %s >%O=' (more deterministic output, TGBA) + - '=ltl2tgba -s %f >%O=' (smaller output, Büchi automaton) + - '=ltl2tgba -s -D %f >%O=' (more deterministic output, Büchi automaton) + - '=ltl2tgba -H %f >%O=' (smaller output, TGBA) + - '=ltl2tgba -H -D %f >%O=' (more deterministic output, TGBA) - '=lbt <%L >%O=' - '~ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD --output-format=hoa %L %O~' deterministic Rabin output in HOA, as diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 1b09b0335..c83ad891b 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -129,7 +129,7 @@ the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, bu converts the never claim produced by =spin= into this format. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -ltldo -f a -f GFa 'spin -f %s>%O' -H +ltldo -f a -f GFa 'spin -f %s>%O' #+END_SRC #+RESULTS: @@ -167,9 +167,9 @@ State: 1 {0} Again, using the shorthands defined below, the previous command can be simplified to just this: -#+BEGIN_SRC sh :results verbatim :exports code -ltldo spin -f a -f GFa -H -#+END_SRC +#+BEGIN_EXAMPLE sh + ltldo spin -f a -f GFa +#+END_EXAMPLE * Syntax for specifying tools to call @@ -303,36 +303,45 @@ the following words, then the string on the right is appended. lbt <%L>%O ltl2ba -f %s>%O - ltl2dstar %L %D + ltl2dstar --output-format=hoa %L %O ltl2tgba -H %f>%O ltl3ba -f %s>%O - ltl3dra -f %f>%O + ltl3dra -f %s>%O modella %L %O spin -f %s>%O + +Any {name} and directory component is skipped for the purpose of +matching those prefixes. So for instance + '{DRA} ~/mytools/ltl2dstar-0.5.2' +will changed into + '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O' #+end_example -So for instance you can type just +Therefore you can type just #+BEGIN_SRC sh :results verbatim :exports code -ltldo ltl2ba -f a +ltldo ltl2ba -f a -d #+END_SRC -to obtain a Dot output (this is the default output format for =ltldo=) -for the neverclaim produced by =ltl2ba -f a=. +to obtain a Dot output (as requested with =-d=) for the neverclaim +produced by =ltl2ba -f a=. #+BEGIN_SRC sh :results verbatim :exports results SPOT_DOTEXTRA= ltldo ltl2ba -f a --dot= #+END_SRC #+RESULTS: -: digraph G { -: rankdir=LR -: I [label="", style=invis, width=0] -: I -> 0 -: 0 [label="0", peripheries=2] -: 0 -> 1 [label="a"] -: 1 [label="1", peripheries=2] -: 1 -> 1 [label="1"] -: } +#+begin_example +digraph G { + rankdir=LR + node [shape="circle"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0", peripheries=2] + 0 -> 1 [label="a"] + 1 [label="1", peripheries=2] + 1 -> 1 [label="1"] +} +#+end_example The =ltl2ba= argument passed to =ltldo= was interpreted as if you had typed ={ltl2ba}ltl2ba -f %s>%O=. @@ -385,7 +394,7 @@ ltldo spin -f '[]!Error' -s : } (We need the =-s= option to obtain a never claim, instead of the -default GraphViz output.) +default HOA output.) What happened is that =ltldo= renamed the atomic propositions in the formula before calling =spin=. So =spin= actually received the @@ -407,7 +416,7 @@ automaton uses the atomic proposition =Error=, but its name contains a reference to =p0=. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -ltldo 'ltl3ba -H' -f '[]!Error' -H +ltldo 'ltl3ba -H' -f '[]!Error' #+END_SRC #+RESULTS: #+BEGIN_SRC hoa @@ -430,7 +439,7 @@ If this is a problem, you can always force a new name with the =--name= option: #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -ltldo 'ltl3ba -H' -f '[]!Error' -H --name='BA for %f' +ltldo 'ltl3ba -H' -f '[]!Error' --name='BA for %f' #+END_SRC #+RESULTS: diff --git a/doc/org/oaut.org b/doc/org/oaut.org index f5ae81405..72628d920 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -24,8 +24,8 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' 'unambiguous', 'stutter-invariant', or 'strength'. -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] - GraphViz's format (default). Add letters for (1) - force numbered states, (a) acceptance display, (b) + GraphViz's format. 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 @@ -35,14 +35,14 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' sets, (R) color acceptance sets by Inf/Fin, (s) with SCCs, (t) force transition-based acceptance, (+INT) add INT to all set numbers - -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format. Add letters - to select (i) use implicit labels for complete - deterministic automata, (s) prefer state-based - acceptance when possible [default], (t) force - transition-based acceptance, (m) mix state and - transition-based acceptance, (k) use state labels - when possible, (l) single-line output, (v) verbose - properties + -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format (default). Add + letters to select (i) use implicit labels for + complete deterministic automata, (s) prefer + state-based acceptance when possible [default], + (t) force transition-based acceptance, (m) mix + state and transition-based acceptance, (k) use + state labels when possible, (l) single-line + output, (v) verbose properties --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton @@ -57,12 +57,12 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+end_example The main three output formats (that can also been used as input to -some of the tools) are [[http://adl.github.io/hoaf/][HOAF]] (activated by =-H= or =--hoaf=), [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] -(activated by =--lbtt=), or Spin [[http://spinroot.com/spin/Man/never.html][never claims]] (activated by =-s= or -=--spin=). These three formats also support *streaming*, i.e., you -can concatenate multiple automata (and even mix these three formats in -the same stream), and the tools will be able to read and process them -in sequence. +some of the tools) are [[http://adl.github.io/hoaf/][HOA]] (used by default, or with =-H= or +=--hoaf=), [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] (activated by =--lbtt=), or Spin [[http://spinroot.com/spin/Man/never.html][never claims]] +(activated by =-s= or =--spin=). These three formats also support +*streaming*, i.e., you can concatenate multiple automata (and even mix +these three formats in the same stream), and the tools will be able to +read and process them in sequence. The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=-d= or =--dot=), various statistics (=--stats=), or nothing at all (=--quiet=). It may @@ -73,16 +73,20 @@ purposes. * HOA output +Details about supported features of the HOA format can be found on a +[[file:hoa.org][separate page]]. + The [[http://adl.github.io/hoaf/][HOA]] output should be the preferred format to use if you want to -pass automata between different tools. This format can be requested -using the =-H= option. (Details about supported features of the HOA -format can be found on a [[file:hoa.org][separate page]].) +pass automata between different tools. Since Spot 1.99.7, it is the +default output format, but you can explicitely request it using the +=-H= parameter and this allows passing additional options to the HOA +printer. Here is an example where [[file:ltl2tgba.org][=ltl2tgba=]] is used to construct two automata: one for =a U b= and one for =(Ga -> Gb) W c=. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -ltl2tgba -H 'a U b' '(Ga -> Gb) W c' +ltl2tgba 'a U b' '(Ga -> Gb) W c' #+END_SRC #+RESULTS: #+BEGIN_SRC hoa @@ -904,13 +908,13 @@ edges should be $20.8\times100=2080$. * Naming automata -Automata can be given names. This name can be output in GraphViz -output when =--dot=n= is given, and is also part of the HOA format (as -activated by =-H=). +Automata can be given names. This name can be output in the +HOA format, but also in GraphViz output when =--dot=n= is given. -By default, =ltl2tgba= will use the input format as name. Other tools -have no default name. This name can be changed using the =--name= option, -that takes a format string similar to the one of =--stats=. +By default, =ltl2tgba= will use the input formula as name. Other +tools have no default name. This name can be changed using the +=--name= option, that takes a format string similar to the one of +=--stats=. #+NAME: oaut-name #+BEGIN_SRC sh :results verbatim :exports code @@ -959,9 +963,9 @@ using =autfilt -n5=. #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 a b | -ltl2tgba -H -F- | +ltl2tgba -F- | autfilt --states=3 --stats='!(%M)' | -ltl2tgba -H -F- | +ltl2tgba -F- | autfilt --states=3 --stats=%M -n5 #+END_SRC @@ -1018,7 +1022,7 @@ automaton is deterministic. We can generate 20 random automata, and output them in two files depending on their determinism: #+BEGIN_SRC sh :results verbatim :exports both -randaut -n 20 -Q2 -d1 1 -H -o out-det%d.hoa +randaut -n 20 -Q2 -e1 1 -o out-det%d.hoa autfilt -c out-det0.hoa # Count of non-deterministic automata autfilt -c out-det1.hoa # Count of deterministic automata #+END_SRC @@ -1036,7 +1040,7 @@ deterministic automata, it may look like we produced more than 20 automata: #+BEGIN_SRC sh :results verbatim :exports both -randaut -D -n 20 -Q2 -d1 1 -H -o out-det%d.hoa +randaut -D -n 20 -Q2 -e1 1 -o out-det%d.hoa autfilt -c out-det0.hoa # Count of non-deterministic automata autfilt -c out-det1.hoa # Count of deterministic automata #+END_SRC @@ -1051,6 +1055,6 @@ previous execution, while =out-det1.hoa= has been overwritten. In the case where you want to append to a file instead of overwriting it, prefix the output filename with =>>= as in -: randaut -D -n 20 -Q2 1 -H -o '>>out-det%d.hoa' +: randaut -D -n 20 -Q2 1 -o '>>out-det%d.hoa' (You need the quotes so that the shell does not interpret '>>'.) diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 9d3d186b0..e2064a432 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -11,50 +11,61 @@ supply. #+NAME: randaut1 #+BEGIN_SRC sh :results verbatim :exports code -randaut a b +randaut a b --dot #+END_SRC #+RESULTS: randaut1 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 - 0 [label="0"] + 0 [label=<0>] 0 -> 8 [label=] + 0 -> 3 [label=] 0 -> 4 [label=] - 1 [label="1"] - 1 -> 2 [label=] - 1 -> 7 [label=] - 1 -> 4 [label=] - 2 [label="2"] - 2 -> 2 [label=] + 1 [label=<1>] + 1 -> 7 [label=] + 1 -> 0 [label=] + 1 -> 6 [label=] + 2 [label=<2>] + 2 -> 4 [label=] 2 -> 0 [label=] 2 -> 5 [label=] - 3 [label="3"] - 3 -> 6 [label=] - 4 [label="4"] - 4 -> 8 [label=] - 4 -> 2 [label=] - 4 -> 3 [label=] + 2 -> 9 [label=] + 3 [label=<3>] + 3 -> 2 [label=] + 3 -> 9 [label=] + 3 -> 3 [label=] + 4 [label=<4>] + 4 -> 0 [label=] 4 -> 7 [label=] - 5 [label="5"] - 5 -> 9 [label=] + 5 [label=<5>] 5 -> 3 [label=] + 5 -> 1 [label=] 5 -> 7 [label=] - 6 [label="6"] - 6 -> 7 [label=] - 6 -> 1 [label=] - 7 [label="7"] - 7 -> 3 [label=] - 8 [label="8"] - 8 -> 8 [label=] - 9 [label="9"] - 9 -> 0 [label=] - 9 -> 6 [label=] + 5 -> 9 [label=] + 5 -> 5 [label=] + 6 [label=<6>] + 6 -> 8 [label=] + 6 -> 5 [label=] + 6 -> 2 [label=] + 7 [label=<7>] + 7 -> 8 [label=] + 7 -> 9 [label=] + 7 -> 0 [label=] + 7 -> 1 [label=] + 7 -> 4 [label=] + 8 [label=<8>] + 8 -> 1 [label=] + 8 -> 3 [label=] + 9 [label=<9>] + 9 -> 1 [label=] + 9 -> 3 [label=] } #+end_example @@ -84,7 +95,7 @@ In particular =-e0= will cause all states to have 1 successors, and #+NAME: randaut2 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -e0 2 +randaut -Q3 -e0 2 --dot #+END_SRC #+RESULTS: randaut2 @@ -115,7 +126,7 @@ $txt #+NAME: randaut3 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -e1 2 +randaut -Q3 -e1 2 --dot #+END_SRC #+RESULTS: randaut3 @@ -168,7 +179,7 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p' RANGE may have one of the following forms: 'INT', 'INT..INT', or '..INT'. In the latter case, the missing number is assumed to be 1. - ACCEPTANCE may be either a RANGE (in which case generalized Büchi is + ACCEPTANCE may be either a RANGE (in which case generalized Büchi is assumed), or an arbitrary acceptance formula such as 'Fin(0)|Inf(1)&Fin(2)' in the same syntax as in the HOA format, or one of the following patterns: none @@ -211,7 +222,7 @@ ans =-s= (or =--spin=) implies =-B=. #+NAME: randaut4 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -e0.5 -A3 -a0.5 2 +randaut -Q3 -e0.5 -A3 -a0.5 2 --dot #+END_SRC #+RESULTS: randaut4 @@ -247,7 +258,7 @@ $txt #+NAME: randaut5 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -e0.4 -B -a0.7 2 +randaut -Q3 -e0.4 -B -a0.7 2 --dot #+END_SRC #+RESULTS: randaut5 @@ -411,7 +422,7 @@ therefore deterministic and complete. #+NAME: randaut6 #+BEGIN_SRC sh :results verbatim :exports code -randaut -D -Q3 -e0.6 -A2 -a0.5 2 +randaut -D -Q3 -e0.6 -A2 -a0.5 2 --dot #+END_SRC #+RESULTS: randaut6 @@ -463,6 +474,5 @@ automatically implies =--ba=. Use option =-n= to specify a number of automata to build. A negative value will cause an infinite number of automata to be produced. This -generation of multiple automata is probably useful only with =--hoaf=, -when piped to another tool that can read this format and process -automata in batches. +generation of multiple automata is useful when piped to another tool +that can process automata in batches. diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 3d2ae919f..92586c76f 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -105,7 +105,7 @@ We can draw it: #+NAME: gfaexxb3 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" +ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" -d #+END_SRC #+RESULTS: gfaexxb3 #+begin_example @@ -154,16 +154,17 @@ result will of course be slightly bigger. #+NAME: gfaexxb4 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" +ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -d #+END_SRC #+RESULTS: gfaexxb4 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -208,7 +209,7 @@ In that case, SAT-based minimization is simply skipped. For instance: ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d' #+END_SRC #+RESULTS: -: states=4, det=0 +: states=5, det=1 The question, of course, is whether there exist a deterministic automaton for this formula, in other words: is this a recurrence @@ -573,7 +574,7 @@ smaller than the output. Let's take this small TGBA as input: #+NAME: autfiltsm6 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba 'GFa & GFb' -H > output2.hoa +ltl2tgba 'GFa & GFb' >output2.hoa autfilt output2.hoa --dot=.a #+END_SRC diff --git a/doc/org/tut02.org b/doc/org/tut02.org index d1a9db045..a75dd988b 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -7,7 +7,6 @@ The task is to read an LTL formula, relabel all (possibly complex) atomic propositions, and provide =#define= statements for each of these renamings, writing everything in Spin's syntax. - * Shell #+BEGIN_SRC sh :results verbatim :exports both @@ -49,7 +48,6 @@ accept_all: } #+end_example - * Python The =spot.relabel= function takes an optional third parameter that @@ -109,7 +107,6 @@ destructor. : #define p2 (var > 10) : (p0) U ((p1) || (p2)) - * Additional comments ** Two ways to name atomic propositions diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 837542c93..7240243fb 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -170,7 +170,6 @@ The Python equivalent is similar: : GFb is not F : GFc is G - * Transforming formulas ** C++ diff --git a/doc/org/tut20.org b/doc/org/tut20.org index 2de1477c0..1bd63c058 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -49,11 +49,10 @@ write will work with any of those formats. * Shell This is very simple: [[file:autfilt.org][=autfilt=]] can read automata in any of the -supported formats, so all we have to do is to request the HOA output -with =-H=: +supported formats, and outputs it in the HOA format by default: #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -autfilt -H tut20.never +autfilt tut20.never #+END_SRC #+RESULTS: diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 6bb55b0f5..a35fd155b 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -21,10 +21,12 @@ different kind of interface (not demonstrated here) to iterate over automata that are constructed on-the-fly and where such a loop would be impossible. -First let's create an example automaton in HOA format. +First let's create an example automaton in HOA format. We use =-U= to +request unambiguous automata, as this allows us to demonstrate how +property bits are used. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -ltl2tgba -U -H 'Fa | G(Fb&Fc)' | tee tut21.hoa +ltl2tgba -U 'Fa | G(Fb&Fc)' | tee tut21.hoa #+END_SRC #+RESULTS: #+BEGIN_SRC hoa diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 8f24f64cc..bd82228cb 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -6,7 +6,7 @@ Consider the following Rabin automaton, generated by =ltl2dstar=: #+BEGIN_SRC sh :results silent :exports both -ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' -H > tut30.hoa +ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' > tut30.hoa #+END_SRC #+RESULTS: @@ -68,16 +68,15 @@ any acceptance to Büchi acceptance. * Shell We use =autfilt= with option =-B= to request Büchi acceptance and -state-based output, =-D= to express a preference for deterministic -output, and =-H= for output in the HOA format. Using option -=-D/--deterministic= (or =--small=) actually activates the -"postprocessing" routines of Spot: the acceptance will not only be -changed to Büchi, but simplification routines (useless SCCs removal, -simulation-based reductions, acceptance sets simplifications, -WDBA-minimization, ...) will also be applied. +state-based output and =-D= to express a preference for deterministic +output. Using option =-D/--deterministic= (or =--small=) actually +activates the "postprocessing" routines of Spot: the acceptance will +not only be changed to Büchi, but simplification routines (useless +SCCs removal, simulation-based reductions, acceptance sets +simplifications, WDBA-minimization, ...) will also be applied. #+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa -autfilt -B -D -H tut30.hoa +autfilt -B -D tut30.hoa #+END_SRC #+RESULTS: #+BEGIN_SRC hoa @@ -108,7 +107,7 @@ State: 4 #+NAME: tut30out #+BEGIN_SRC sh :results verbatim :exports none -autfilt -B -D tut30.hoa +autfilt -B -D -d tut30.hoa #+END_SRC #+RESULTS: tut30out diff --git a/tests/core/dstar.test b/tests/core/dstar.test index 0cfd5f2e7..585c70374 100755 --- a/tests/core/dstar.test +++ b/tests/core/dstar.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -56,7 +56,7 @@ Acc-Sig: +0 2 EOF -run 0 ../ikwiad -XD dra.dstar | tee stdout +run 0 ../ikwiad -d -XD dra.dstar | tee stdout cat >expected <expected <expected <expected <%H" '{foo}ltl2ba' >output + run 0 $ltldo -d "$LTL2BA -f %s>%H" '{foo}ltl2ba' >output test 4 = `grep -c digraph output` diff --git a/tests/core/monitor.test b/tests/core/monitor.test index d484ac598..504721c28 100755 --- a/tests/core/monitor.test +++ b/tests/core/monitor.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -31,7 +31,7 @@ expect() diff output.out output.exp } -expect ltl2tgba --monitor a <\n" ], "text": [ - " *' at 0x7f1084090540> >" + " *' at 0x7fad7cc5f330> >" ] }, { @@ -162,7 +162,7 @@ "\n" ], "text": [ - " *' at 0x7f1084090600> >" + " *' at 0x7fad7cc5f4e0> >" ] }, { @@ -208,7 +208,7 @@ "\n" ], "text": [ - " *' at 0x7f1084090540> >" + " *' at 0x7fad7cc5f270> >" ] }, { @@ -265,7 +265,7 @@ "\n" ], "text": [ - " *' at 0x7f1084090600> >" + " *' at 0x7fad7cc5f330> >" ] } ], @@ -342,7 +342,7 @@ "\n" ], "text": [ - " *' at 0x7f10840a0570> >" + " *' at 0x7fad7cc5f4e0> >" ] } ], @@ -373,8 +373,8 @@ "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'non-existing-command|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 404\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 405\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 406\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 407\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 408\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, *sources)\u001b[0m\n\u001b[1;32m 395\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 396\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 397\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 398\u001b[0m \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 399\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 457\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 458\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 459\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 461\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \"\n" ], "text": [ - " *' at 0x7f10840a00c0> >" + " *' at 0x7fad7cc5f780> >" ] }, { "ename": "CalledProcessError", - "evalue": "Command 'ltl2tgba -f \"syntax U U error\"' returned non-zero exit status 2", + "evalue": "Command 'ltl2tgba \"syntax U U error\"' returned non-zero exit status 2", "output_type": "pyerr", "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", - "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"ltl2tgba -H 'a U b'|\"\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'ltl2tgba -f \"syntax U U error\"|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, *sources)\u001b[0m\n\u001b[1;32m 395\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 396\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 397\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 398\u001b[0m \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 399\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;31mCalledProcessError\u001b[0m: Command 'ltl2tgba -f \"syntax U U error\"' returned non-zero exit status 2" + "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"ltl2tgba 'a U b'|\"\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'ltl2tgba \"syntax U U error\"|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \"\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'true|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 406\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 407\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 408\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 409\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 410\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 459\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 461\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 462\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 463\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: Failed to read automaton from true|" ] } ], "prompt_number": 6 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [] } ], "metadata": {}