bin: add -d as a shorthand for --dot
* bin/common_aoutput.cc: Here. * NEWS, doc/org/oaut.org: Mention it. * tests/core/readsave.test: Use it once.
This commit is contained in:
Alexandre Duret-Lutz
parent
ea5f52ddbb
commit
cca2022e90
4 changed files with 45 additions and 35 deletions
5
NEWS
5
NEWS
|
|
@ -2,8 +2,9 @@ New in spot 1.99.6a (not yet released)
|
|||
|
||||
Command-line tools:
|
||||
|
||||
* randaut's short option for --density used to be -d. It has been renamed
|
||||
to -e so that -d means --dot in all tools.
|
||||
* 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.
|
||||
|
||||
* autfilt has a new option: --is-inherently-weak.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -73,8 +73,7 @@ ARGMATCH_VERIFY(check_args, check_types);
|
|||
unsigned opt_check = 0U;
|
||||
|
||||
enum {
|
||||
OPT_DOT = 1,
|
||||
OPT_LBTT,
|
||||
OPT_LBTT = 1,
|
||||
OPT_NAME,
|
||||
OPT_STATS,
|
||||
OPT_CHECK,
|
||||
|
|
@ -84,7 +83,7 @@ static const argp_option options[] =
|
|||
{
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output format:", 3 },
|
||||
{ "dot", OPT_DOT, "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT",
|
||||
{ "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 "
|
||||
"(1) force numbered states, "
|
||||
|
|
@ -229,10 +228,17 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
|
|||
case '8':
|
||||
spot::enable_utf8();
|
||||
break;
|
||||
case 'd':
|
||||
automaton_format = Dot;
|
||||
opt_dot = arg;
|
||||
break;
|
||||
case 'H':
|
||||
automaton_format = Hoa;
|
||||
hoa_opt = arg;
|
||||
break;
|
||||
case 'o':
|
||||
opt_output = arg;
|
||||
break;
|
||||
case 'q':
|
||||
automaton_format = Quiet;
|
||||
break;
|
||||
|
|
@ -243,9 +249,6 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
|
|||
if (arg)
|
||||
opt_never = arg;
|
||||
break;
|
||||
case 'o':
|
||||
opt_output = arg;
|
||||
break;
|
||||
case OPT_CHECK:
|
||||
automaton_format = Hoa;
|
||||
if (arg)
|
||||
|
|
@ -253,10 +256,6 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
|
|||
else
|
||||
opt_check |= check_all;
|
||||
break;
|
||||
case OPT_DOT:
|
||||
automaton_format = Dot;
|
||||
opt_dot = arg;
|
||||
break;
|
||||
case OPT_LBTT:
|
||||
automaton_format = Lbtt;
|
||||
opt_lbtt = arg;
|
||||
|
|
|
|||
|
|
@ -18,22 +18,31 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
|
|||
#+begin_example
|
||||
-8, --utf8 enable UTF-8 characters in output (ignored with
|
||||
--lbtt or --spin)
|
||||
--dot[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v]
|
||||
GraphViz's format (default). Add letters for (a)
|
||||
acceptance display, (b) acceptance sets as
|
||||
bullets,(c) circular nodes, (f(FONT)) use FONT,
|
||||
(h) horizontal layout, (v) vertical layout, (n)
|
||||
with name, (N) without name, (r) rainbow colors
|
||||
for acceptance set, (R) color acceptance set by
|
||||
Inf/Fin, (s) with SCCs, (t) force transition-based
|
||||
acceptance.
|
||||
-H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. Add letters
|
||||
--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', '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)
|
||||
acceptance sets as bullets, (B) bullets except for
|
||||
Büchi/co-Büchi automata, (c) force circular
|
||||
nodes, (e) force elliptic nodes, (f(FONT)) use
|
||||
FONT, (h) horizontal layout, (v) vertical layout,
|
||||
(n) with name, (N) without name, (o) ordered
|
||||
transitions, (r) rainbow colors for acceptance
|
||||
sets, (R) color acceptance sets by Inf/Fin, (s)
|
||||
with SCCs, (t) force transition-based acceptance,
|
||||
(+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, (l) single-line
|
||||
output
|
||||
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
|
||||
|
|
@ -55,11 +64,12 @@ 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 (=--dot=), various
|
||||
statistics (=--stats=), or nothing at all (=--quiet=). It may seem
|
||||
strange to ask a tool to not output anything, but it makes sense when
|
||||
only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check
|
||||
whether an input automaton has some property) or for timing purposes.
|
||||
The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=-d= or =--dot=),
|
||||
various statistics (=--stats=), or nothing at all (=--quiet=). It may
|
||||
seem strange to ask a tool to not output anything, but it makes sense
|
||||
when only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to
|
||||
check whether an input automaton has some property) or for timing
|
||||
purposes.
|
||||
|
||||
* HOA output
|
||||
|
||||
|
|
@ -478,11 +488,11 @@ of Promela syntax.)
|
|||
|
||||
* Dot output
|
||||
|
||||
The =--dot= option (which usually is the default) causes automata to be
|
||||
output in GraphViz's format.
|
||||
The =-d= or =--dot= option causes automata to be output in GraphViz's
|
||||
format.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgba '(Ga -> Gb) W c'
|
||||
ltl2tgba '(Ga -> Gb) W c' -d
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
|
|
|
|||
|
|
@ -359,7 +359,7 @@ digraph G {
|
|||
EOF
|
||||
diff output expected
|
||||
|
||||
ltl2tgba --dot=ban 'GFa & GFb' >output
|
||||
ltl2tgba -dban 'GFa & GFb' >output
|
||||
cat output
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue