diff --git a/doc/org/oaut.org b/doc/org/oaut.org index a8c4b84dd..774d434ac 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -28,8 +28,11 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' transition-based acceptance, (m) mixed acceptance, (l) single-line output --lbtt[=t] LBTT's format (add =t to force transition-based - acceptance even on Büchi automata) + acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton + -o, --output=FORMAT send output to a file named FORMAT instead of + standard output. The first automaton sent to a + file truncates it unless FORMAT starts with '>>'. -q, --quiet suppress all normal output -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to select (6) Spin's 6.2.4 style, (c) comments on @@ -39,7 +42,7 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' The main three output formats (that can also been used as input to some of the tools) are [[http://adl.github.io/hoaf/][HOAF]] (activated by =-H= or =--hoaf=), [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] -(activated by =--lbtt=), or spin [[http://spinroot.com/spin/Man/never.html][never claims]] (activated by =-s= or +(activated by =--lbtt=), or Spin [[http://spinroot.com/spin/Man/never.html][never claims]] (activated by =-s= or =--spin=). These three formats also support *streaming*, i.e., you 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 @@ -806,3 +809,53 @@ head -n5 | cut -d, -f2 # return the five first formulas # LocalWords: Tpng txt Hs Hm CSV Htl LBT dstar init goto fi Tpdf XF # LocalWords: oaut vcsn randaut nondeterministic filename csv hoa # LocalWords: varphi lnot GFb FG +* Naming output + +By default, all output is sent to standard output, so you can either +redirect it to a file, or pipe it to another program. +You can also use the =--output= (a.k.a. =-o=) option to specify a +filename where automata should be written. The advantage over +a shell redirection, is that you may build a name using the same +escape sequences as used by =--stats= and =--name=. + +For instance =%d= is replaced by 0 or 1 depending on whether the +automaton is deterministic. We can generate 20 random automata, and +output them in two files depending on their determinism: + +#+BEGIN_SRC sh :results verbatim :exports both +randaut -n 20 -S2 1 -H -o out-det%d.hoa +autfilt -c out-det0.hoa # Count of non-deterministic automata +autfilt -c out-det1.hoa # Count of deterministic automata +#+END_SRC + +#+RESULTS: +: 4 +: 16 + +If you use this feature, beware that the output filename +is only truncated by the first file that is output to it: so +if no automaton generate some filename, the existing file +will be left untouched. For instance we we run the above +commands, again, but forcing [[file:randaut.org][=randaut=]] to output 20 +deterministic automata, it may look like we produced more +than 20 automata: + +#+BEGIN_SRC sh :results verbatim :exports both +randaut -D -n 20 -S2 1 -H -o out-det%d.hoa +autfilt -c out-det0.hoa # Count of non-deterministic automata +autfilt -c out-det1.hoa # Count of deterministic automata +#+END_SRC + +#+RESULTS: +: 4 +: 20 + +This is because the =out-det0.hoa= file hasn't changed from the +previous execution, while =out-det1.hoa= has been overwritten. + +In the case where you want to append to a file instead of overwriting +it, prefix the output filename with =>>= as in + +: randaut -D -n 20 -S2 1 -H -o '>>out-det%d.hoa' + +(You need the quotes so that the shell does not interpret '>>'.) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 8ab7b6822..65297e239 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -515,9 +515,9 @@ main(int argc, char** argv) post.set_type(type); post.set_level(level); - hoa_processor processor(post); try { + hoa_processor processor(post); if (processor.run()) return 2; } diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 73b82f38e..63724d287 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -37,6 +37,7 @@ static const char* opt_dot = nullptr; static const char* opt_never = nullptr; static const char* hoa_opt = nullptr; const char* opt_name = nullptr; +static const char* opt_output = nullptr; static const char* stats = ""; #define OPT_DOT 1 @@ -62,6 +63,10 @@ static const argp_option options[] = " on Büchi automata)", 0 }, { "name", OPT_NAME, "FORMAT", 0, "set the name of the output automaton", 0 }, + { "output", 'o', "FORMAT", 0, + "send output to a file named FORMAT instead of standard output. The" + " first automaton sent to a file truncates it unless FORMAT starts" + " with '>>'.", 0 }, { "quiet", 'q', 0, 0, "suppress all normal output", 0 }, { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", @@ -83,7 +88,7 @@ char L_doc[32] = "location in the input file"; static const argp_option io_options[] = { /**************************************************/ - { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\ + { 0, 0, 0, 0, "Any FORMAT string may use "\ "the following interpreted sequences (capitals for input," " minuscules for output):", 4 }, { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, @@ -116,7 +121,7 @@ const struct argp aoutput_io_format_argp = { io_options, 0, 0, 0, 0, 0, 0 }; static const argp_option o_options[] = { /**************************************************/ - { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\ + { 0, 0, 0, 0, "Any FORMAT string may use "\ "the following interpreted sequences:", 4 }, { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 }, { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 }, @@ -165,6 +170,9 @@ 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_DOT: automaton_format = Dot; opt_dot = arg; @@ -201,8 +209,12 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) automaton_printer::automaton_printer(stat_style input) : statistics(std::cout, stats, input), - namer(name, opt_name, input) + namer(name, opt_name, input), + outputnamer(outputname, opt_output, input) { + if (automaton_format == Count && opt_output) + throw std::runtime_error + ("options --output and --count are incompatible"); } void @@ -223,6 +235,18 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, aut->set_named_prop("automaton-name", new std::string(name.str())); } + std::ostream* out = &std::cout; + if (opt_output) + { + outputname.str(""); + outputnamer.print(haut, aut, f, filename, loc, time); + std::string fname = outputname.str(); + auto p = outputfiles.emplace(fname, nullptr); + if (p.second) + p.first->second.reset(new output_file(fname.c_str())); + out = &p.first->second->ostream(); + } + // Output it. switch (automaton_format) { @@ -231,21 +255,22 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, // Do not output anything. break; case Dot: - spot::dotty_reachable(std::cout, aut, opt_dot); + spot::dotty_reachable(*out, aut, opt_dot); break; case Lbtt: - spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); + spot::lbtt_reachable(*out, aut, type == spot::postprocessor::BA); break; case Lbtt_t: - spot::lbtt_reachable(std::cout, aut, false); + spot::lbtt_reachable(*out, aut, false); break; case Hoa: - spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; + spot::hoa_reachable(*out, aut, hoa_opt) << '\n'; break; case Spin: - spot::never_claim_reachable(std::cout, aut, opt_never); + spot::never_claim_reachable(*out, aut, opt_never); break; case Stats: + statistics.set_output(*out); statistics.print(haut, aut, f, filename, loc, time) << '\n'; break; } @@ -256,4 +281,5 @@ void automaton_printer::add_stat(char c, const spot::printable* p) { namer.declare(c, p); statistics.declare(c, p); + outputnamer.declare(c, p); } diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index b3f357ba1..281ba868e 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -23,6 +23,7 @@ #include "common_sys.hh" #include +#include #include "hoaparse/public.hh" @@ -32,6 +33,7 @@ #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/word.hh" #include "tgbaalgos/isdet.hh" +#include "common_file.hh" // Format for automaton output @@ -97,6 +99,7 @@ public: } using spot::formater::declare; + using spot::formater::set_output; /// \brief print the configured statistics. /// @@ -205,6 +208,9 @@ class automaton_printer hoa_stat_printer statistics; std::ostringstream name; hoa_stat_printer namer; + std::ostringstream outputname; + hoa_stat_printer outputnamer; + std::map> outputfiles; public: diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 5a4d5fb3b..2550727b8 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -21,6 +21,7 @@ #include #include +#include #include #include "error.h" @@ -29,6 +30,7 @@ #include "common_finput.hh" #include "common_cout.hh" #include "common_post.hh" +#include "common_file.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" @@ -83,6 +85,10 @@ static const argp_option options[] = " on Büchi automata)", 0 }, { "name", OPT_NAME, "FORMAT", 0, "set the name of the output automaton", 0 }, + { "output", 'o', "FORMAT", 0, + "send output to a file named FORMAT instead of standard output. The" + " first automaton sent to a file truncates it unless FORMAT starts" + " with '>>'.", 0 }, { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", 0 }, @@ -138,6 +144,7 @@ static const char* stats = ""; static const char* hoa_opt = nullptr; static const char* opt_never = nullptr; static const char* opt_name = nullptr; +static const char* opt_output = nullptr; static spot::option_map extra_options; static int @@ -162,6 +169,9 @@ parse_opt(int key, char* arg, struct argp_state*) case 'M': type = spot::postprocessor::Monitor; break; + case 'o': + opt_output = arg; + break; case 's': format = Spin; if (type != spot::postprocessor::Monitor) @@ -241,6 +251,8 @@ namespace declare('m', &aut_name_); } + using spot::formater::set_output; + /// \brief print the configured statistics. /// /// The \a f argument is not needed if the Formula does not need @@ -306,10 +318,14 @@ namespace dstar_stat_printer statistics; std::ostringstream name; dstar_stat_printer namer; + std::ostringstream outputname; + dstar_stat_printer outputnamer; + std::map> outputfiles; dstar_processor(spot::postprocessor& post) : post(post), statistics(std::cout, stats), - namer(name, opt_name) + namer(name, opt_name), + outputnamer(outputname, opt_output) { } @@ -344,24 +360,37 @@ namespace aut->set_named_prop("automaton-name", new std::string(name.str())); } + std::ostream* out = &std::cout; + if (opt_output) + { + outputname.str(""); + outputnamer.print(daut, aut, filename, conversion_time); + std::string fname = outputname.str(); + auto p = outputfiles.emplace(fname, nullptr); + if (p.second) + p.first->second.reset(new output_file(fname.c_str())); + out = &p.first->second->ostream(); + } + switch (format) { case Dot: - spot::dotty_reachable(std::cout, aut, opt_dot); + spot::dotty_reachable(*out, aut, opt_dot); break; case Lbtt: - spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); + spot::lbtt_reachable(*out, aut, type == spot::postprocessor::BA); break; case Lbtt_t: - spot::lbtt_reachable(std::cout, aut, false); + spot::lbtt_reachable(*out, aut, false); break; case Hoa: - spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; + spot::hoa_reachable(*out, aut, hoa_opt) << '\n'; break; case Spin: - spot::never_claim_reachable(std::cout, aut, opt_never); + spot::never_claim_reachable(*out, aut, opt_never); break; case Stats: + statistics.set_output(*out); statistics.print(daut, aut, filename, conversion_time) << '\n'; break; } @@ -390,8 +419,15 @@ main(int argc, char** argv) post.set_type(type); post.set_level(level); - dstar_processor processor(post); - if (processor.run()) - return 2; + try + { + dstar_processor processor(post); + if (processor.run()) + return 2; + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } return 0; } diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 35b786aaf..5b460c6aa 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -181,9 +181,9 @@ main(int argc, char** argv) trans.set_type(type); trans.set_level(level); - trans_processor processor(trans); try { + trans_processor processor(trans); if (processor.run()) return 2; } diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 61d7f43a8..3f1d114ff 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -361,9 +361,15 @@ main(int argc, char** argv) post.set_type(type); post.set_level(level); - processor p(post); - if (p.run()) - return 2; - + try + { + processor p(post); + if (p.run()) + return 2; + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } return 0; } diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 0b08cfee5..009d48a5b 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -231,67 +231,66 @@ main(int argc, char** argv) error(2, 0, "--ba is incompatible with --acc-sets=%d..%d", opt_acc_sets.min, opt_acc_sets.max); - spot::srand(opt_seed); - auto d = spot::make_bdd_dict(); - - automaton_printer printer; - - constexpr unsigned max_trials = 10000; - unsigned trials = max_trials; - - int automaton_num = 0; - - for (;;) + try { - spot::stopwatch sw; - sw.start(); + spot::srand(opt_seed); + auto d = spot::make_bdd_dict(); - int size = opt_states.min; - if (size != opt_states.max) - size = spot::rrand(size, opt_states.max); + automaton_printer printer; - int accs = opt_acc_sets.min; - if (accs != opt_acc_sets.max) - accs = spot::rrand(accs, opt_acc_sets.max); + constexpr unsigned max_trials = 10000; + unsigned trials = max_trials; - auto aut = - spot::random_graph(size, opt_density, &aprops, d, - accs, opt_acc_prob, 0.5, - opt_deterministic, opt_state_acc); + int automaton_num = 0; - if (opt_uniq) - { - auto tmp = - spot::canonicalize(make_tgba_digraph(aut, - spot::tgba::prop_set::all())); - std::vector trans(tmp->transition_vector().begin() + 1, - tmp->transition_vector().end()); - if (!opt_uniq->emplace(trans).second) - { - --trials; - if (trials == 0) - error(2, 0, "failed to generate a new unique automaton" - " after %d trials", max_trials); - continue; - } - trials = max_trials; - } - - auto runtime = sw.stop(); - - try + for (;;) { + spot::stopwatch sw; + sw.start(); + + int size = opt_states.min; + if (size != opt_states.max) + size = spot::rrand(size, opt_states.max); + + int accs = opt_acc_sets.min; + if (accs != opt_acc_sets.max) + accs = spot::rrand(accs, opt_acc_sets.max); + + auto aut = + spot::random_graph(size, opt_density, &aprops, d, + accs, opt_acc_prob, 0.5, + opt_deterministic, opt_state_acc); + + if (opt_uniq) + { + auto tmp = spot::canonicalize + (make_tgba_digraph(aut, spot::tgba::prop_set::all())); + std::vector trans(tmp->transition_vector().begin() + 1, + tmp->transition_vector().end()); + if (!opt_uniq->emplace(trans).second) + { + --trials; + if (trials == 0) + error(2, 0, "failed to generate a new unique automaton" + " after %d trials", max_trials); + continue; + } + trials = max_trials; + } + + auto runtime = sw.stop(); + printer.print(aut, nullptr, opt_seed_str, automaton_num, runtime, nullptr); - } - catch (const std::runtime_error& e) - { - error(2, 0, "%s", e.what()); - } - ++automaton_num; - if (opt_automata > 0 && automaton_num >= opt_automata) - break; - } + ++automaton_num; + if (opt_automata > 0 && automaton_num >= opt_automata) + break; + } + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } spot::ltl::destroy_atomic_prop_set(aprops); } diff --git a/src/tgbatest/randaut.test b/src/tgbatest/randaut.test index 5f45cf498..20df91e44 100755 --- a/src/tgbatest/randaut.test +++ b/src/tgbatest/randaut.test @@ -71,3 +71,13 @@ diff out2 expected $randaut -n 5 --dot=@ a 2>stderr && exit 1 grep 'randaut: unknown option.*@' stderr + +$randaut -n -1 -S2 2 -H | $autfilt -H --is-deterministic -n 3 -o out.hoa +$randaut -n -1 -S2 2 -H | $autfilt -H -v --is-deterministic -n 4 -o '>>out.hoa' +$autfilt -H out.hoa -o 'out-det%d.hoa' +$autfilt -H out.hoa -o '>>out-det%d.hoa' +test 8 = `$autfilt -c out-det0.hoa` +test 6 = `$autfilt -c out-det1.hoa` + +$autfilt -H out.hoa -o foo -c 2>stderr && exit 1 +grep 'autfilt: options --output and --count are incompatible' stderr