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.
This commit is contained in:
Alexandre Duret-Lutz
parent
9d6727da5c
commit
d0b38156f3
21 changed files with 327 additions and 250 deletions
9
NEWS
9
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.
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@
|
|||
#include <spot/twaalgos/isunamb.hh>
|
||||
#include <spot/twaalgos/strength.hh>
|
||||
|
||||
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, "
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
|
|
@ -53,6 +54,7 @@ SPOT_DOTEXTRA= autfilt example.hoa --dot=
|
|||
#+RESULTS:
|
||||
: digraph G {
|
||||
: rankdir=LR
|
||||
: node [shape="circle"]
|
||||
: I [label="", style=invis, width=0]
|
||||
: I -> 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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
autfilt <<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
|
|
@ -499,7 +499,7 @@ actually spot the terms that have been grouped together internally by
|
|||
looking at the spacing around operators =&= and =|=. For instance:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
||||
randaut -A"Fin(0)|Fin(1)|Fin(2)&Fin(3)&Inf(4)&Inf(5)" -H 0 | grep Acceptance:
|
||||
randaut -A"Fin(0)|Fin(1)|Fin(2)&Fin(3)&Inf(4)&Inf(5)" 0 | grep Acceptance:
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
@ -708,7 +708,7 @@ State: 2 "so am I"
|
|||
[0] 2 {0 1}
|
||||
--END--
|
||||
EOF
|
||||
autfilt -H hw.hoa
|
||||
autfilt hw.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: hello-world
|
||||
|
|
@ -747,7 +747,7 @@ Here is for instance the result when =autfilt= is instructed to
|
|||
simplify the automaton:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
||||
autfilt -H --small hw.hoa
|
||||
autfilt --small hw.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
@ -780,7 +780,7 @@ construct the new name by simply copying the one of the original
|
|||
automaton.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
||||
autfilt -H --small hw.hoa --name=%M
|
||||
autfilt --small hw.hoa --name=%M
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
@ -825,7 +825,7 @@ randomize the order of their transitions and states before printing
|
|||
them in HOA format.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
||||
genltl --and-gf=1..3 | ltl2tgba -B -F- -H | autfilt --randomize -H
|
||||
genltl --and-gf=1..3 | ltl2tgba -B -F- | autfilt --randomize
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
|
|||
|
|
@ -14,25 +14,29 @@ option.
|
|||
Formulas to translate may be specified using [[file:ioltl.org][common input options for
|
||||
LTL/PSL formulas]].
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltl2tgba -f 'Fa & GFb'
|
||||
#+END_SRC
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
SPOT_DOTEXTRA= ltl2tgba -f 'Fa & GFb' --dot=
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 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"]
|
||||
|
|
|
|||
|
|
@ -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}"]
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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 '>>'.)
|
||||
|
|
|
|||
|
|
@ -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=<!a & !b>]
|
||||
0 -> 3 [label=<!a & !b>]
|
||||
0 -> 4 [label=<!a & !b>]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label=<a & !b>]
|
||||
1 -> 7 [label=<!a & !b>]
|
||||
1 -> 4 [label=<!a & b>]
|
||||
2 [label="2"]
|
||||
2 -> 2 [label=<!a & !b>]
|
||||
1 [label=<1>]
|
||||
1 -> 7 [label=<a & b>]
|
||||
1 -> 0 [label=<a & b>]
|
||||
1 -> 6 [label=<a & !b>]
|
||||
2 [label=<2>]
|
||||
2 -> 4 [label=<!a & !b>]
|
||||
2 -> 0 [label=<a & !b>]
|
||||
2 -> 5 [label=<a & !b>]
|
||||
3 [label="3"]
|
||||
3 -> 6 [label=<!a & b>]
|
||||
4 [label="4"]
|
||||
4 -> 8 [label=<a & !b>]
|
||||
4 -> 2 [label=<!a & b>]
|
||||
4 -> 3 [label=<a & b>]
|
||||
2 -> 9 [label=<!a & b>]
|
||||
3 [label=<3>]
|
||||
3 -> 2 [label=<a & b>]
|
||||
3 -> 9 [label=<a & !b>]
|
||||
3 -> 3 [label=<a & !b>]
|
||||
4 [label=<4>]
|
||||
4 -> 0 [label=<!a & !b>]
|
||||
4 -> 7 [label=<!a & b>]
|
||||
5 [label="5"]
|
||||
5 -> 9 [label=<!a & !b>]
|
||||
5 [label=<5>]
|
||||
5 -> 3 [label=<a & !b>]
|
||||
5 -> 1 [label=<!a & b>]
|
||||
5 -> 7 [label=<!a & !b>]
|
||||
6 [label="6"]
|
||||
6 -> 7 [label=<!a & !b>]
|
||||
6 -> 1 [label=<!a & b>]
|
||||
7 [label="7"]
|
||||
7 -> 3 [label=<!a & !b>]
|
||||
8 [label="8"]
|
||||
8 -> 8 [label=<!a & b>]
|
||||
9 [label="9"]
|
||||
9 -> 0 [label=<!a & b>]
|
||||
9 -> 6 [label=<!a & b>]
|
||||
5 -> 9 [label=<!a & b>]
|
||||
5 -> 5 [label=<!a & !b>]
|
||||
6 [label=<6>]
|
||||
6 -> 8 [label=<a & b>]
|
||||
6 -> 5 [label=<a & !b>]
|
||||
6 -> 2 [label=<a & !b>]
|
||||
7 [label=<7>]
|
||||
7 -> 8 [label=<!a & !b>]
|
||||
7 -> 9 [label=<a & b>]
|
||||
7 -> 0 [label=<!a & b>]
|
||||
7 -> 1 [label=<!a & !b>]
|
||||
7 -> 4 [label=<a & b>]
|
||||
8 [label=<8>]
|
||||
8 -> 1 [label=<a & b>]
|
||||
8 -> 3 [label=<!a & b>]
|
||||
9 [label=<9>]
|
||||
9 -> 1 [label=<!a & b>]
|
||||
9 -> 3 [label=<a & !b>]
|
||||
}
|
||||
#+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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -170,7 +170,6 @@ The Python equivalent is similar:
|
|||
: GFb is not F
|
||||
: GFc is G
|
||||
|
||||
|
||||
* Transforming formulas
|
||||
|
||||
** C++
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
digraph G {
|
||||
|
|
@ -78,7 +78,7 @@ EOF
|
|||
diff expected stdout
|
||||
|
||||
|
||||
run 0 ../ikwiad -XDB -R3 dra.dstar | tee stdout
|
||||
run 0 ../ikwiad -d -XDB -R3 dra.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -123,7 +123,7 @@ Acc-Sig:
|
|||
2
|
||||
EOF
|
||||
|
||||
run 0 ../ikwiad -XDB dsa.dstar | tee stdout
|
||||
run 0 ../ikwiad -d -XDB dsa.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -212,7 +212,7 @@ State: 3 "str\n\"ing" Acc-Sig: -0 +1 3 3 3 3
|
|||
State: 4 "more\"string\"" Acc-Sig: +0 +1 3 4 3 4
|
||||
EOF
|
||||
|
||||
run 0 autfilt -B dra.dstar | tee stdout
|
||||
run 0 autfilt -d -B dra.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2015 Laboratoire de Recherche et
|
||||
# Copyright (C) 2015, 2016 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -27,5 +27,5 @@ genltl=genltl
|
|||
test -n "$LTL2BA" || exit 77
|
||||
|
||||
$genltl --or-g=1..2 |
|
||||
run 0 $ltldo "$LTL2BA -f %s>%H" '{foo}ltl2ba' >output
|
||||
run 0 $ltldo -d "$LTL2BA -f %s>%H" '{foo}ltl2ba' >output
|
||||
test 4 = `grep -c digraph output`
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
expect ltl2tgba -d --monitor a <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@
|
|||
"version": "3.4.3+"
|
||||
},
|
||||
"name": "",
|
||||
"signature": "sha256:471d70bbd30f4ffde7ebceb35a8f4a1ca66baba3ad959b99d4bb72ef81e4d5cf"
|
||||
"signature": "sha256:8de782e4035d4a93101b749825f0975f5f8cee034332d048014ba13dfa232983"
|
||||
},
|
||||
"nbformat": 3,
|
||||
"nbformat_minor": 0,
|
||||
|
|
@ -111,7 +111,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1084090540> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fad7cc5f330> >"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -162,7 +162,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1084090600> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fad7cc5f4e0> >"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -208,7 +208,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1084090540> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fad7cc5f270> >"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -265,7 +265,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1084090600> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fad7cc5f330> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -342,7 +342,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f10840a0570> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' 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<ipython-input-4-765c7cc6937f>\u001b[0m in \u001b[0;36m<module>\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: \"<built-in function\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
|
||||
"\u001b[0;31mCalledProcessError\u001b[0m: Command 'non-existing-command' returned non-zero exit status 127"
|
||||
]
|
||||
}
|
||||
|
|
@ -385,7 +385,7 @@
|
|||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"for a in spot.automata(\"ltl2tgba -H 'a U b'|\", 'ltl2tgba -f \"syntax U U error\"|'):\n",
|
||||
"for a in spot.automata(\"ltl2tgba 'a U b'|\", 'ltl2tgba \"syntax U U error\"|'):\n",
|
||||
" display(a)"
|
||||
],
|
||||
"language": "python",
|
||||
|
|
@ -445,18 +445,18 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f10840a00c0> >"
|
||||
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' 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<ipython-input-5-21a24ff75c32>\u001b[0m in \u001b[0;36m<module>\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<ipython-input-5-1163f8abbaad>\u001b[0m in \u001b[0;36m<module>\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: \"<built-in function\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
|
||||
"\u001b[0;31mCalledProcessError\u001b[0m: Command 'ltl2tgba \"syntax U U error\"' returned non-zero exit status 2"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -485,12 +485,20 @@
|
|||
"traceback": [
|
||||
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)",
|
||||
"\u001b[0;32m<ipython-input-6-f4e056a50029>\u001b[0m in \u001b[0;36m<module>\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": {}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue