Commit 78def4f8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin: add the --output to tools that output formulas

* src/bin/common_output.cc, src/bin/common_output.hh: Add option
--output.
* src/ltltest/ltlfilt.test, src/ltltest/rand.test: Add tests.
* NEWS, doc/org/ioltl.org: Document it.
parent e22a800f
......@@ -44,6 +44,12 @@ New in spot 1.99a (not yet released)
- ltlfilt has a new --count option to count the number of matching
automata.
- all tools that produce formulas or automata now have an --output
(a.k.a. -o) option to redirect that output to a file instead of
standard output. The name of this file can be constructed using
the same %-escape sequences that are available for --stats or
--format.
- ltlcross (and ltldo) have a list of hard-coded shorthands
for some existing tools. So for instance running
'ltlcross spin ...' is the same as running
......
......@@ -150,6 +150,7 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
-c, --count print only a count of matched formulas
-n, --max-count=NUM output at most NUM formulas
-q, --quiet suppress all normal output
-8, --utf8 output using UTF-8 characters
......@@ -158,14 +159,15 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
"%f")
-l, --lbt output in LBT's syntax
--latex output using LaTeX macros
-o, --output=FORMAT send output to a file named FORMAT instead of
standard output. The first formula sent to a file
truncates it unless FORMAT starts with '>>'.
-p, --full-parentheses output fully-parenthesized formulas
-s, --spin output in Spin's syntax
--spot output in Spot's syntax (default)
--wring output in Wring's syntax
#+end_example
# LocalWords: syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME
The =--spot=, =--utf-8=, =--spin=, =--wring= options select different
output syntaxes as seen in [[tab:formula-syntaxes][the above table]].
......@@ -203,5 +205,33 @@ from tool to tool:
| [[file:genltl.org][=genltl=]] | output formula | pattern name | pattern parameter | (empty) | (empty) |
| [[file:randltl.org][=randltl=]] | output formula | (empty) | formula number | (empty) | (empty) |
By default everything is output to standard output, so that you can
redirect the output to a file, and pipe it to another tool. The the
=--output= (or =-o=) allows you to construct a filename using some of
the above =%=-sequences.
For instance the following invocation of [[file:randltl.org][=randltl=]] will create 5
random formulas, but in 5 different files:
#+BEGIN_SRC sh :results verbatim :exports both
randltl -n5 a b -o example-%L.ltl
wc -l example-*.ltl
#+END_SRC
#+RESULTS:
: 1 example-1.ltl
: 1 example-2.ltl
: 1 example-3.ltl
: 1 example-4.ltl
: 1 example-5.ltl
: 5 total
#+BEGIN_SRC sh :results verbatim :exports none
rm -f example-*.ltl
#+END_SRC
#+RESULTS:
# LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck
# LocalWords: utf associativity
# LocalWords: syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME
......@@ -52,6 +52,10 @@ static const argp_option options[] =
-20 },
{ "format", OPT_FORMAT, "FORMAT", 0,
"specify how each line should be output (default: \"%f\")", -20 },
{ "output", 'o', "FORMAT", 0,
"send output to a file named FORMAT instead of standard output. The"
" first formula sent to a file truncates it unless FORMAT starts"
" with '>>'.", 0 },
{ 0, 0, 0, 0, 0, 0 }
};
......@@ -195,6 +199,9 @@ namespace
}
static formula_printer* format = 0;
static std::ostringstream outputname;
static formula_printer* outputnamer = 0;
static std::map<std::string, std::unique_ptr<output_file>> outputfiles;
int
parse_opt_output(int key, char* arg, struct argp_state*)
......@@ -208,6 +215,9 @@ parse_opt_output(int key, char* arg, struct argp_state*)
case 'l':
output_format = lbt_output;
break;
case 'o':
outputnamer = new formula_printer(outputname, arg);
break;
case 'p':
full_parenth = true;
break;
......@@ -237,10 +247,11 @@ parse_opt_output(int key, char* arg, struct argp_state*)
}
void
static void
output_formula(std::ostream& out,
const spot::ltl::formula* f, const char* filename, int linenum,
const char* prefix, const char* suffix)
const spot::ltl::formula* f,
const char* filename = nullptr, int linenum = 0,
const char* prefix = nullptr, const char* suffix = nullptr)
{
if (!format)
{
......@@ -257,15 +268,40 @@ output_formula(std::ostream& out,
}
}
void
::printable_formula::print(std::ostream& os, const char*) const
{
output_formula(os, val_);
}
void
output_formula_checked(const spot::ltl::formula* f,
const char* filename, int linenum,
const char* prefix, const char* suffix)
{
if (output_format == quiet_output || output_format == count_output)
if (output_format == count_output)
{
if (outputnamer)
throw std::runtime_error
("options --output and --count are incompatible");
return;
}
if (output_format == quiet_output)
return;
output_formula(std::cout, f, filename, linenum, prefix, suffix);
std::cout << '\n';
std::ostream* out = &std::cout;
if (outputnamer)
{
outputname.str("");
formula_with_location fl = { f, filename, linenum, prefix, suffix };
outputnamer->print(fl);
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_formula(*out, f, filename, linenum, prefix, suffix);
*out << '\n';
// Make sure we abort if we can't write to std::cout anymore
// (like disk full or broken pipe with SIGPIPE ignored).
check_cout();
......
......@@ -23,9 +23,12 @@
#include "common_sys.hh"
#include <argp.h>
#include <map>
#include <memory>
#include "ltlast/formula.hh"
#include "tgbaalgos/stats.hh"
#include "common_output.hh"
#include "common_file.hh"
enum output_format_t { spot_output, spin_output, utf8_output,
lbt_output, wring_output, latex_output,
......@@ -38,9 +41,6 @@ extern const struct argp output_argp;
int parse_opt_output(int key, char* arg, struct argp_state* state);
void output_formula(std::ostream& os, const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0,
const char* prefix = 0, const char* suffix = 0);
void output_formula_checked(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0,
const char* prefix = 0, const char* suffix = 0);
......@@ -58,10 +58,7 @@ public:
}
virtual void
print(std::ostream& os, const char*) const
{
output_formula(os, val_);
}
print(std::ostream& os, const char*) const;
};
class aut_stat_printer: protected spot::stat_printer
......@@ -73,6 +70,8 @@ public:
declare('f', &formula_); // Override the formula printer.
}
using spot::formater::set_output;
std::ostream&
print(const spot::const_tgba_digraph_ptr& aut,
const spot::ltl::formula* f = 0,
......
......@@ -188,4 +188,8 @@ SPOT_STUTTER_CHECK=5 \
# bug in the bitvectors.
../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
../../bin/ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
grep 'ltlfilt: options --output and --count are incompatible' stderr
true
......@@ -130,3 +130,9 @@ run 2 $randltl -n3 0
run 0 $randltl -n1000 0 1 > out
grep -q '"0"' out
grep -q '"1"' out
run 0 $randltl -n5 2 -o test-all.ltl
run 0 $randltl -n5 2 -o test-%L.ltl
cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl
diff test-cmp.ltl test-all.ltl
Supports Markdown
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