Commit 1e7c1e5c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

bin: implement --output for automata

Fixes #56.

* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/dstar2tgba.cc: Implement it.
* src/bin/autfilt.cc, src/bin/ltl2tgba.cc, src/bin/ltldo.cc,
src/bin/randaut.cc: Fix main() to catch exceptions from the
constructor of the automaton printer as well.
* src/tgbatest/randaut.test: Add a test case.
* doc/org/oaut.org: Document it.
parent d17d7469
......@@ -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 '>>'.)
......@@ -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;
}
......
......@@ -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);
}
......@@ -23,6 +23,7 @@
#include "common_sys.hh"
#include <argp.h>
#include <memory>
#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<std::string, std::unique_ptr<output_file>> outputfiles;
public:
......
......@@ -21,6 +21,7 @@
#include <string>
#include <iostream>
#include <memory>
#include <argp.h>
#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<std::string, std::unique_ptr<output_file>> 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;
}
......@@ -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;
}
......
......@@ -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;
}
......@@ -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();
try
{
spot::srand(opt_seed);
auto d = spot::make_bdd_dict();
automaton_printer printer;
automaton_printer printer;
constexpr unsigned max_trials = 10000;
unsigned trials = max_trials;
constexpr unsigned max_trials = 10000;
unsigned trials = max_trials;
int automaton_num = 0;
int automaton_num = 0;
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<tr_t> trans(tmp->transition_vector().begin() + 1,
tmp->transition_vector().end());
if (!opt_uniq->emplace(trans).second)
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)
{
--trials;
if (trials == 0)
error(2, 0, "failed to generate a new unique automaton"
" after %d trials", max_trials);
continue;
auto tmp = spot::canonicalize
(make_tgba_digraph(aut, spot::tgba::prop_set::all()));
std::vector<tr_t> 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;
}
trials = max_trials;
}
auto runtime = sw.stop();
auto runtime = sw.stop();
try
{
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);
}
......@@ -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
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