Commit 40fb80ea authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin: use common_aoutput in ltl2tgba

* src/bin/common_aoutput.hh, src/bin/common_aoutput.cc: Adjust to
support three kind of statistics printer, depending on whether the
tool input formulas, automata, or nothing.
* src/bin/randaut.cc, src/bin/autfilt.cc: Adjust.
* src/bin/ltl2tgba.cc: Use the common_aoutput printers.  The
--csv-escape option disappeared along the way, but it was not honored
anyway...
parent 72737dfe
......@@ -320,7 +320,7 @@ namespace
public:
hoa_processor(spot::postprocessor& post)
: post(post), printer(true)
: post(post), printer(aut_input)
{
}
......@@ -398,7 +398,7 @@ namespace
return 0;
}
printer.print(aut, filename, -1, conversion_time, haut);
printer.print(aut, nullptr, filename, -1, conversion_time, haut);
if (opt_max_count >= 0 && match_count >= opt_max_count)
abort_run = true;
......
......@@ -59,8 +59,8 @@ static const argp_option options[] =
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
"LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)", 0 },
{ "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL,
"set the name of the output automaton (default: %M)", 0 },
{ "name", OPT_NAME, "FORMAT", 0,
"set the name of the output automaton", 0 },
{ "quiet", 'q', 0, 0, "suppress all normal output", 0 },
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
......@@ -105,7 +105,7 @@ static const argp_option io_options[] =
{ "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"1 if the output is complete, 0 otherwise", 0 },
{ "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"processing time (excluding any parsing) in seconds", 0 },
"processing time (excluding parsing) in seconds", 0 },
{ "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the output automaton", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
......@@ -137,7 +137,7 @@ static const argp_option o_options[] =
{ "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"1 if the output is complete, 0 otherwise", 0 },
{ "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"processing time (excluding any parsing) in seconds", 0 },
"processing time (excluding parsing) in seconds", 0 },
{ "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the output automaton", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
......@@ -185,10 +185,7 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
}
break;
case OPT_NAME:
if (arg)
opt_name = arg;
else
opt_name = "%M";
opt_name = arg;
break;
case OPT_SPOT:
automaton_format = Spot;
......@@ -207,14 +204,15 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
automaton_printer::automaton_printer(bool has_input)
: statistics(std::cout, stats, has_input),
namer(name, opt_name, has_input)
automaton_printer::automaton_printer(stat_style input)
: statistics(std::cout, stats, input),
namer(name, opt_name, input)
{
}
void
automaton_printer::print(const spot::tgba_digraph_ptr& aut,
const spot::ltl::formula* f,
// Input location for errors and statistics.
const char* filename,
int loc,
......@@ -226,7 +224,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut,
if (opt_name)
{
name.str("");
namer.print(haut, aut, filename, loc, time);
namer.print(haut, aut, f, filename, loc, time);
aut->set_named_prop("automaton-name", new std::string(name.str()));
}
......@@ -259,7 +257,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut,
spot::never_claim_reachable(std::cout, aut);
break;
case Stats:
statistics.print(haut, aut, filename, loc, time) << '\n';
statistics.print(haut, aut, f, filename, loc, time) << '\n';
break;
}
flush_cout();
......
......@@ -65,6 +65,9 @@ extern const struct argp aoutput_o_format_argp;
// Parse output options
int parse_opt_aoutput(int key, char* arg, struct argp_state* state);
enum stat_style { no_input, aut_input, ltl_input };
/// \brief prints various statistics about a TGBA
///
/// This object can be configured to display various statistics
......@@ -74,10 +77,10 @@ class hoa_stat_printer: protected spot::stat_printer
{
public:
hoa_stat_printer(std::ostream& os, const char* format,
bool has_input = false)
stat_style input = no_input)
: spot::stat_printer(os, format)
{
if (has_input)
if (input == aut_input)
{
declare('A', &haut_acc_);
declare('C', &haut_scc_);
......@@ -88,7 +91,8 @@ public:
}
declare('F', &filename_);
declare('L', &location_);
declare('f', &filename_); // Override the formula printer.
if (input != ltl_input)
declare('f', &filename_); // Override the formula printer.
declare('m', &aut_name_);
declare('w', &aut_word_);
}
......@@ -100,6 +104,7 @@ public:
std::ostream&
print(const spot::const_hoa_aut_ptr& haut,
const spot::const_tgba_digraph_ptr& aut,
const spot::ltl::formula* f,
const char* filename, int loc, double run_time)
{
filename_ = filename;
......@@ -177,7 +182,7 @@ public:
}
}
return this->spot::stat_printer::print(aut, 0, run_time);
return this->spot::stat_printer::print(aut, f, run_time);
}
private:
......@@ -202,10 +207,11 @@ class automaton_printer
public:
automaton_printer(bool has_input = false);
automaton_printer(stat_style input = no_input);
void
print(const spot::tgba_digraph_ptr& aut,
const spot::ltl::formula* f = nullptr,
// Input location for errors and statistics.
const char* filename = nullptr,
int loc = -1,
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -30,22 +30,16 @@
#include "common_cout.hh"
#include "common_finput.hh"
#include "common_output.hh"
#include "common_aoutput.hh"
#include "common_post.hh"
#include "ltlast/formula.hh"
#include "ltlvisit/tostring.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh"
#include "tgbaalgos/hoa.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/translate.hh"
#include "tgba/bddprint.hh"
#include "misc/optionmap.hh"
#include "misc/timer.hh"
const char argp_program_doc[] ="\
static const char argp_program_doc[] ="\
Translate linear-time formulas (LTL/PSL) into Büchi automata.\n\n\
By default it will apply all available optimizations to output \
the smallest Transition-based Generalized Büchi Automata, \
......@@ -53,11 +47,6 @@ in GraphViz's format.\n\
If multiple formulas are supplied, several automata will be output.";
#define OPT_TGBA 1
#define OPT_DOT 2
#define OPT_LBTT 3
#define OPT_SPOT 4
#define OPT_STATS 5
#define OPT_CSV 6
static const argp_option options[] =
{
......@@ -69,48 +58,8 @@ static const argp_option options[] =
{ "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
"of the given formula)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output format:", 3 },
{ "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format "
"for use in CSV file", 0 },
{ "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL,
"GraphViz's format (default). Add letters to chose (c) circular nodes, "
"(h) horizontal layout, (v) vertical layout, (n) with name, "
"(N) without name, (t) always transition-based acceptance.", 0 },
{ "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format. Add letters to select "
"(s) state-based acceptance, (t) transition-based acceptance, "
"(m) mixed acceptance, (l) single-line output", 0 },
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
"LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)", 0 },
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
{ "utf8", '8', 0, 0, "enable UTF-8 characters in output "
"(ignored with --lbtt or --spin)", 0 },
{ "stats", OPT_STATS, "FORMAT", 0,
"output statistics about the automaton", 0 },
/**************************************************/
{ 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
"the following interpreted sequences:", 4 },
{ "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula, in Spot's syntax", 0 },
{ "%s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of states", 0 },
{ "%e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of edges", 0 },
{ "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 },
{ "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 },
{ "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of nondeterministic states", 0 },
{ "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"1 if the automaton is deterministic, 0 otherwise", 0 },
{ "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"1 if the automaton is complete, 0 otherwise", 0 },
{ "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"translation time (including pre- and post-processings, but not parsing)"
" in seconds", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
"the formula, in Spot's syntax", 4 },
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0,
......@@ -121,16 +70,14 @@ static const argp_option options[] =
const struct argp_child children[] =
{
{ &finput_argp, 0, 0, 1 },
{ &aoutput_argp, 0, 0, 0 },
{ &aoutput_o_format_argp, 0, 0, 0 },
{ &post_argp, 0, 0, 20 },
{ &misc_argp, 0, 0, -1 },
{ 0, 0, 0, 0 }
};
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
const char* opt_dot = nullptr;
const char* stats = "";
const char* hoa_opt = 0;
spot::option_map extra_options;
static spot::option_map extra_options;
static int
parse_opt(int key, char* arg, struct argp_state*)
......@@ -138,25 +85,12 @@ parse_opt(int key, char* arg, struct argp_state*)
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
spot::enable_utf8();
output_format = utf8_output;
break;
case 'B':
type = spot::postprocessor::BA;
break;
case 'H':
format = Hoa;
hoa_opt = arg;
break;
case 'M':
type = spot::postprocessor::Monitor;
break;
case 's':
format = Spin;
if (type != spot::postprocessor::Monitor)
type = spot::postprocessor::BA;
break;
case 'x':
{
const char* opt = extra_options.parse_options(arg);
......@@ -164,37 +98,8 @@ parse_opt(int key, char* arg, struct argp_state*)
error(2, 0, "failed to parse --options near '%s'", opt);
}
break;
case OPT_CSV:
escape_csv = true;
break;
case OPT_DOT:
format = Dot;
opt_dot = arg;
break;
case OPT_LBTT:
if (arg)
{
if (arg[0] == 't' && arg[1] == 0)
format = Lbtt_t;
else
error(2, 0, "unknown argument for --lbtt: '%s'", arg);
}
else
{
format = Lbtt;
}
break;
case OPT_SPOT:
format = Spot;
break;
case OPT_STATS:
if (!*arg)
error(2, 0, "empty format string for --stats");
stats = arg;
format = Stats;
break;
case OPT_TGBA:
if (format == Spin)
if (automaton_format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
break;
......@@ -216,10 +121,10 @@ namespace
{
public:
spot::translator& trans;
aut_stat_printer statistics;
automaton_printer printer;
trans_processor(spot::translator& trans)
: trans(trans), statistics(std::cout, stats)
: trans(trans), printer(ltl_input)
{
}
......@@ -227,11 +132,6 @@ namespace
process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0)
{
spot::stopwatch sw;
sw.start();
auto aut = trans.run(&f);
const double translation_time = sw.stop();
// This should not happen, because the parser we use can only
// read PSL/LTL formula, but since our ltl::formula* type can
// represent more than PSL formula, let's make this
......@@ -244,35 +144,13 @@ namespace
s.c_str());
}
switch (format)
{
case Dot:
spot::dotty_reachable(std::cout, aut,
(type == spot::postprocessor::BA)
|| (type == spot::postprocessor::Monitor),
opt_dot);
break;
case Lbtt:
spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
break;
case Lbtt_t:
spot::lbtt_reachable(std::cout, aut, false);
break;
case Hoa:
spot::hoa_reachable(std::cout, aut, hoa_opt, f) << '\n';
break;
case Spot:
spot::tgba_save_reachable(std::cout, aut);
break;
case Spin:
spot::never_claim_reachable(std::cout, aut, f);
break;
case Stats:
statistics.print(aut, f, translation_time) << '\n';
break;
}
spot::stopwatch sw;
sw.start();
auto aut = trans.run(&f);
const double translation_time = sw.stop();
printer.print(aut, f, filename, linenum, translation_time, nullptr);
f->destroy();
flush_cout();
return 0;
}
};
......@@ -281,6 +159,9 @@ namespace
int
main(int argc, char** argv)
{
// By default we name automata using the formula.
opt_name = "%f";
setup(argv);
const argp ap = { options, parse_opt, "[FORMULA...]",
......
......@@ -298,7 +298,8 @@ main(int argc, char** argv)
auto runtime = sw.stop();
printer.print(aut, opt_seed_str, automaton_num, runtime, nullptr);
printer.print(aut, nullptr,
opt_seed_str, automaton_num, runtime, nullptr);
++automaton_num;
if (opt_automata > 0 && automaton_num >= opt_automata)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment