diff --git a/NEWS b/NEWS index c4e2d019f..553add972 100644 --- a/NEWS +++ b/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. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index cc16f7618..fa0eb9c50 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -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; diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 99eebcec5..f5ae81405 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 diff --git a/tests/core/readsave.test b/tests/core/readsave.test index ffb656999..bc3643481 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -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 <