From 9d6727da5cd12cd469259a79b09ed676507228ee Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Jan 2016 18:17:06 +0100 Subject: [PATCH] bin: add support for SPOT_DEFAULT_FORMAT * bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_setup.cc: Implement it. * NEWS, bin/man/spot-x.x: Document it. * tests/core/readsave.test: Test it. --- NEWS | 4 ++++ bin/common_aoutput.cc | 47 ++++++++++++++++++++++++++++------------ bin/common_aoutput.hh | 6 +++-- bin/common_setup.cc | 4 ++++ bin/man/spot-x.x | 39 ++++++++++++++++++++++++++++----- tests/core/readsave.test | 12 ++++++---- 6 files changed, 86 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index 553add972..7540371b2 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,10 @@ New in spot 1.99.6a (not yet released) randaut's short option for specifying edge-density used to be -d: it has been renamed to -e. + * The SPOT_DEFAULT_FORMAT environment variable can be set to 'dot' + or 'hoa' to force a default output format for automata. Options + may also be added, as in SPOT_DEFAULT_FORMAT='hoa=iv'. + * autfilt has a new option: --is-inherently-weak. Library: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index fa0eb9c50..9ade197f9 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -36,10 +36,7 @@ #include automaton_format_t automaton_format = Dot; -static const char* opt_dot = nullptr; -static const char* opt_never = nullptr; -static const char* hoa_opt = nullptr; -static const char* opt_lbtt = nullptr; +static const char* automaton_format_opt = nullptr; const char* opt_name = nullptr; static const char* opt_output = nullptr; static const char* stats = ""; @@ -230,11 +227,11 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) break; case 'd': automaton_format = Dot; - opt_dot = arg; + automaton_format_opt = arg; break; case 'H': automaton_format = Hoa; - hoa_opt = arg; + automaton_format_opt = arg; break; case 'o': opt_output = arg; @@ -246,8 +243,7 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) automaton_format = Spin; if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; - if (arg) - opt_never = arg; + automaton_format_opt = arg; break; case OPT_CHECK: automaton_format = Hoa; @@ -258,7 +254,7 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) break; case OPT_LBTT: automaton_format = Lbtt; - opt_lbtt = arg; + automaton_format_opt = arg; // This test could be removed when more options are added, // because print_lbtt will raise an exception anyway. The // error message is slightly better in the current way. @@ -280,7 +276,30 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) return 0; } - +void setup_default_output_format() +{ + if (auto val = getenv("SPOT_DEFAULT_FORMAT")) + { + static char const *const args[] = + { + "dot", "hoa", "hoaf", nullptr + }; + static automaton_format_t const format[] = + { + Dot, Hoa, Hoa + }; + auto eq = strchr(val, '='); + if (eq) + { + val = strndup(val, eq - val); + automaton_format_opt = eq + 1; + } + ARGMATCH_VERIFY(args, format); + automaton_format = XARGMATCH("SPOT_DEFAULT_FORMAT", val, args, format); + if (eq) + free(val); + } +} automaton_printer::automaton_printer(stat_style input) : statistics(std::cout, stats, input), @@ -340,16 +359,16 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, // Do not output anything. break; case Dot: - spot::print_dot(*out, aut, opt_dot); + spot::print_dot(*out, aut, automaton_format_opt); break; case Lbtt: - spot::print_lbtt(*out, aut, opt_lbtt); + spot::print_lbtt(*out, aut, automaton_format_opt); break; case Hoa: - spot::print_hoa(*out, aut, hoa_opt) << '\n'; + spot::print_hoa(*out, aut, automaton_format_opt) << '\n'; break; case Spin: - spot::print_never_claim(*out, aut, opt_never); + spot::print_never_claim(*out, aut, automaton_format_opt); break; case Stats: statistics.set_output(*out); diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 593ae4fd7..d9df1fb45 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- 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. // @@ -233,3 +233,5 @@ public: void add_stat(char c, const spot::printable* p); }; + +void setup_default_output_format(); diff --git a/bin/common_setup.cc b/bin/common_setup.cc index c05313753..6eb0d34a0 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -18,6 +18,8 @@ // along with this program. If not, see . #include "common_setup.hh" +#include "common_aoutput.hh" + #include "argp.h" #include #include @@ -40,6 +42,7 @@ This is free software: you are free to change and redistribute it.\n\ There is NO WARRANTY, to the extent permitted by law.\n", stream); } + #ifdef HAVE_SIGACTION static void sig_handler(int sig) { @@ -81,6 +84,7 @@ setup(char** argv) std::ios_base::sync_with_stdio(false); + setup_default_output_format(); setup_sig_handler(); } diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index 972397e5c..6197d7d33 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -1,5 +1,5 @@ [NAME] -spot-x \- Common fine-tuning options. +spot-x \- Common fine-tuning options and environment variables. [SYNOPSIS] .B \-\-extra-options STRING @@ -11,14 +11,41 @@ spot-x \- Common fine-tuning options. [ENVIRONMENT VARIABLES] +.TP +\fBSPOT_DEFAULT_FORMAT\fR +Set to a value of \fBdot\fR or \fBhoa\fR to override the default +format used to output automata. Up to Spot 1.9.6 the default output +format for automata used to be \fBdot\fR. Starting with Spot 1.9.7, +the default output format switched to \fBhoa\fR as it is more +convenient when chaining tools in a pipe. Set this variable to +\fBdot\fR to get the old behavior. Additional options may be +passed to the printer by suffixing the output format with +\fB=\fR and the options. For instance running +.in +4n +.nf +.ft C +% SPOT_DEFAULT_OUTPUT=dot=bar autfilt ... +.fi +.in -4n +is the same as running +.in +4n +.nf +.ft C +% autfilt --dot=bar ... +.fi +.in -4n +but the use of the environment variable makes more sense if you set +it up once for many commands. + .TP \fBSPOT_DOTDEFAULT\fR Whenever the \f(CW--dot\fR option is used without argument (even -implicitely), the contents of this variable is used as default -argument. If you have some default setting in \fBSPOT_DOTDEFAULT\fR -but want to alter them temporarily for one call, use -\f(CW--dot=.yyy\fR: the dot character will be replaced by the contents -of the \f(CWSPOT_DOTDEFAULT\fR environment variable. +implicitely via \fBSPOT_DEFAULT_FORMAT\fR), the contents of this +variable is used as default argument. If you have some default +setting in \fBSPOT_DOTDEFAULT\fR but want to alter them temporarily +for one call, use \f(CW--dot=.yyy\fR: the dot character will be +replaced by the contents of the \f(CWSPOT_DOTDEFAULT\fR environment +variable. .TP \fBSPOT_DOTEXTRA\fR diff --git a/tests/core/readsave.test b/tests/core/readsave.test index bc3643481..a3e0ee506 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -306,7 +306,10 @@ State: 3 "s3" EOF autfilt -H input | - SPOT_DOTDEFAULT=vcsn SPOT_DOTEXTRA='/* hello world */' autfilt >output + SPOT_DEFAULT_FORMAT=dot \ + SPOT_DOTDEFAULT=vcsn \ + SPOT_DOTEXTRA='/* hello world */' \ + autfilt >output cat >expected <output +# The SPOT_DEFAULT_FORMAT envvar should be ignored if --dot is given. +SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=a 'GFa & GFb' >output cat output cat >expected <output2 && exit 1 +SPOT_DEFAULT_FORMAT=hoa autfilt --remove-dead input >output2 && exit 1 cat >expect2 <output2b +SPOT_DEFAULT_FORMAT=hoa=k autfilt expect2 >output2b cat >expect2b <