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.
This commit is contained in:
Alexandre Duret-Lutz
parent
cca2022e90
commit
9d6727da5c
6 changed files with 86 additions and 26 deletions
4
NEWS
4
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:
|
||||
|
|
|
|||
|
|
@ -36,10 +36,7 @@
|
|||
#include <spot/twaalgos/strength.hh>
|
||||
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -18,6 +18,8 @@
|
|||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "common_setup.hh"
|
||||
#include "common_aoutput.hh"
|
||||
|
||||
#include "argp.h"
|
||||
#include <cstdlib>
|
||||
#include <iostream>
|
||||
|
|
@ -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();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
digraph G {
|
||||
|
|
@ -340,7 +343,8 @@ diff output expected
|
|||
test 1 = `autfilt -H input --complete | autfilt --is-complete --count`
|
||||
|
||||
|
||||
ltl2tgba --dot=a 'GFa & GFb' >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 <<EOF
|
||||
digraph G {
|
||||
|
|
@ -607,7 +611,7 @@ diff output1 output1b
|
|||
# Here is the scenario where the undefined states are actually states
|
||||
# we wanted to remove. So we tell autfilt to fix the automaton using
|
||||
# --remove-dead-states
|
||||
autfilt -H --remove-dead input >output2 && exit 1
|
||||
SPOT_DEFAULT_FORMAT=hoa autfilt --remove-dead input >output2 && exit 1
|
||||
|
||||
cat >expect2 <<EOF
|
||||
HOA: v1
|
||||
|
|
@ -629,7 +633,7 @@ EOF
|
|||
|
||||
diff output2 expect2
|
||||
|
||||
autfilt -Hk expect2 >output2b
|
||||
SPOT_DEFAULT_FORMAT=hoa=k autfilt expect2 >output2b
|
||||
|
||||
cat >expect2b <<EOF
|
||||
HOA: v1
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue