bin: --stats=%H --stats=%h

Part of #91.

* bin/common_aoutput.cc, bin/common_aoutput.hh: implement %H and %h.
* tests/core/readsave.test: Test them.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-08-08 10:48:06 +02:00
parent 0d753048ce
commit f423c424eb
4 changed files with 57 additions and 1 deletions

5
NEWS
View file

@ -107,6 +107,11 @@ New in spot 2.0.3a (not yet released)
is now deprecated. The option is still here, but hidden and is now deprecated. The option is still here, but hidden and
undocumented. undocumented.
* The --stats option of autfilt, dstar2tgba, ltl2tgba, ltldo,
randaut learned to display the output (or input if that makes
sense) automaton as a HOA one-liner using %H (or %h), helping to
create CSV files contained automata.
* Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba) * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
that are not used are now reported as they might be typos. that are not used are now reported as they might be typos.
This ocurred a couple of times in our test-suite. A similar This ocurred a couple of times in our test-suite. A similar

View file

@ -152,6 +152,9 @@ static const argp_option io_options[] =
" minuscules for output):", 4 }, " minuscules for output):", 4 },
{ "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
{ "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
{ "%H, %h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"the automaton in HOA format on a single line (use %[opt]H or %[opt]h "
"to specify additional options as in --hoa=opt)", 0 },
{ "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"name of the automaton", 0 }, "name of the automaton", 0 },
{ "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@ -192,6 +195,9 @@ static const argp_option o_options[] =
"the following interpreted sequences:", 4 }, "the following interpreted sequences:", 4 },
{ "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
{ "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
{ "%h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"the automaton in HOA format on a single line (use %[opt]h "
"to specify additional options as in --hoa=opt)", 0 },
{ "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"name of the automaton", 0 }, "name of the automaton", 0 },
{ "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@ -396,3 +402,17 @@ void automaton_printer::add_stat(char c, const spot::printable* p)
statistics.declare(c, p); statistics.declare(c, p);
outputnamer.declare(c, p); outputnamer.declare(c, p);
} }
void printable_automaton::print(std::ostream& os, const char* pos) const
{
std::string options = "l";
if (*pos == '[')
{
++pos;
auto end = strchr(pos, ']');
options = std::string(pos, end - pos);
options += 'l';
pos = end + 1;
}
print_hoa(os, val_, options.c_str());
}

View file

@ -66,6 +66,14 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state* state);
enum stat_style { no_input, aut_input, ltl_input }; enum stat_style { no_input, aut_input, ltl_input };
struct printable_automaton final:
public spot::printable_value<spot::const_twa_graph_ptr>
{
using spot::printable_value<spot::const_twa_graph_ptr>::operator=;
void print(std::ostream& os, const char* pos) const override;
};
/// \brief prints various statistics about a TGBA /// \brief prints various statistics about a TGBA
/// ///
/// This object can be configured to display various statistics /// This object can be configured to display various statistics
@ -84,6 +92,7 @@ public:
declare('C', &haut_scc_); declare('C', &haut_scc_);
declare('E', &haut_edges_); declare('E', &haut_edges_);
declare('G', &haut_gen_acc_); declare('G', &haut_gen_acc_);
declare('H', &input_aut_);
declare('M', &haut_name_); declare('M', &haut_name_);
declare('S', &haut_states_); declare('S', &haut_states_);
declare('T', &haut_trans_); declare('T', &haut_trans_);
@ -94,6 +103,7 @@ public:
declare('L', &location_); declare('L', &location_);
if (input != ltl_input) if (input != ltl_input)
declare('f', &filename_); // Override the formula printer. declare('f', &filename_); // Override the formula printer.
declare('h', &output_aut_);
declare('m', &aut_name_); declare('m', &aut_name_);
declare('w', &aut_word_); declare('w', &aut_word_);
} }
@ -121,8 +131,10 @@ public:
os << loc; os << loc;
location_ = os.str(); location_ = os.str();
} }
output_aut_ = aut;
if (haut) if (haut)
{ {
input_aut_ = haut->aut;
if (loc < 0 && has('L')) if (loc < 0 && has('L'))
{ {
std::ostringstream os; std::ostringstream os;
@ -190,7 +202,13 @@ public:
} }
} }
return this->spot::stat_printer::print(aut, f, run_time); auto& res = this->spot::stat_printer::print(aut, f, run_time);
// Make sure we do not store the automaton until the next one is
// printed, as the registered APs will affect how the next
// automata are built.
output_aut_ = nullptr;
input_aut_ = nullptr;
return res;
} }
private: private:
@ -207,6 +225,8 @@ private:
spot::printable_value<unsigned> haut_scc_; spot::printable_value<unsigned> haut_scc_;
spot::printable_value<const char*> csv_prefix_; spot::printable_value<const char*> csv_prefix_;
spot::printable_value<const char*> csv_suffix_; spot::printable_value<const char*> csv_suffix_;
printable_automaton input_aut_;
printable_automaton output_aut_;
}; };

View file

@ -971,6 +971,17 @@ EOF
test `autfilt -c --is-inherently-weak input8` = 0 test `autfilt -c --is-inherently-weak input8` = 0
test `autfilt -c --is-weak input8` = 0 test `autfilt -c --is-weak input8` = 0
autfilt input8 -Hl >oneline.hoa
autfilt input8 --stats='%h' >oneline2.hoa
autfilt input8 --stats='%H' >oneline3.hoa
autfilt input8 --randomize --stats='%h' >oneline4.hoa
autfilt input8 --randomize --stats='%H' >oneline5.hoa
diff oneline.hoa oneline2.hoa
diff oneline.hoa oneline3.hoa
diff oneline.hoa oneline4.hoa && exit 1
diff oneline.hoa oneline5.hoa
cat >input9 <<EOF cat >input9 <<EOF
HOA: v1 HOA: v1
name: "a U (b U c)" name: "a U (b U c)"