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

tools: Add a --format option

* src/bin/common_output.cc: Add option --format and implement
it.
* src/bin/ltlfilt.cc, src/bin/randltl.cc: Document the
supported %-sequences.
* src/bin/genltl.cc: Document the %-sequences, and supply
the name of the pattern to output_formula().
* doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltlfilt.org,
NEWS: Document it.
* src/ltltest/latex.test: Use it.
parent 983feb52
......@@ -76,6 +76,10 @@ New in spot 1.1.4a (not relased)
Each operator is output as a command such as \U, \F, etc.
doc/tl/spotltl.sty gives one possible definition for each macro.
- ltlfilt, genltl, and randltl have a new --format option to
indicate how to present the output formula, possibly with
information about the input.
* New functions and classes in the library:
- dtba_sat_synthetize(): Use a SAT-solver to build an equivalent
......
......@@ -47,7 +47,7 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
(p1 U (p2 U (... U pn)))
#+end_example
An example is probably all it takes to explain how this tool works:
An example is probably all it takes to understand how this tool works:
#+BEGIN_SRC sh :results verbatim :exports both
genltl --and-gf=1..5 --u-left=1..5
......@@ -69,9 +69,47 @@ p1 U p2
=genltl= supports the [[file:ioltl.org][common option for output of LTL formulas]], so you
may output these pattern for various tools.
Note that for the =--lbt= output, each formula is relabeled using
For instance here is the same formulas, but formatted in a way that is
suitable for being included in a LaTeX table.
#+BEGIN_SRC sh :results verbatim :exports both
genltl --and-gf=1..5 --u-left=1..5 --latex --format='%F & %L & $%f$ \\'
#+END_SRC
#+RESULTS:
#+begin_example
and-gf & 1 & $\G \F p_{1}$ \\
and-gf & 2 & $\G \F p_{1} \land \G \F p_{2}$ \\
and-gf & 3 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3}$ \\
and-gf & 4 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4}$ \\
and-gf & 5 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4} \land \G \F p_{5}$ \\
u-left & 1 & $p_{1}$ \\
u-left & 2 & $p_{1} \U p_{2}$ \\
u-left & 3 & $(p_{1} \U p_{2}) \U p_{3}$ \\
u-left & 4 & $((p_{1} \U p_{2}) \U p_{3}) \U p_{4}$ \\
u-left & 5 & $(((p_{1} \U p_{2}) \U p_{3}) \U p_{4}) \U p_{5}$ \\
#+end_example
Note that for the =--lbt= syntax, each formula is relabeled using
=p0=, =p1=, ... before it is output, when the pattern (like
=--ccj-alpha=) use different names.
=--ccj-alpha=) use different names. Compare:
#+BEGIN_SRC sh :results verbatim :exports both
genltl --ccj-alpha=3
#+END_SRC
#+RESULTS:
: F(F(Fq3 & q2) & q1) & F(F(Fp3 & p2) & p1)
with
#+BEGIN_SRC sh :results verbatim :exports both
genltl --ccj-alpha=3 --lbt
#+END_SRC
#+RESULTS:
: & F & p2 F & p1 F p0 F & F & F p3 p4 p5
This is because most tools using =lbt='s syntax require atomic
propositions to have the form =pNN=.
# LocalWords: genltl num toc LTL scalable SRC sed gh pn fg FG gf qn
# LocalWords: ccj Xp XXp Xq XXq rv GFp lbt
......@@ -141,7 +141,10 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: -8, --utf8 output using UTF-8 characters
: --format=FORMAT specify how each line should be output (default:
: "%f")
: -l, --lbt output in LBT's syntax
: --latex output using LaTeX macros
: -p, --full-parentheses output fully-parenthesized formulas
: -s, --spin output in Spin's syntax
: --spot output in Spot's syntax (default)
......@@ -150,8 +153,14 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
# 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]]. The =-p= option can
be used to request that parentheses be used at all levels.
output syntaxes as seen in [[tab:formula-syntaxes][the above table]].
Option =--latex= causes formulas to be output using LaTeX macros for
each operator. You may define these macros as you wish, and some
example definitions are in =doc/tl/spotltl.sty=.
The =-p= option can be used to request that parentheses be used at all
levels.
Note that by default Spot always outputs parentheses around operators
such as =U=, because not all tools agree on their associativity. For
......@@ -162,5 +171,16 @@ with read it as =(a U b) U c=.
The =--lbt= option requests an output in LBT's prefix format, and in
that case discussing associativity and parentheses makes no sense.
The =--format= option can be used to fine-tune the way the formula is
output. Not using the =--format= option is equivalent to using
=--format=%f=. The semantic of the available =%=-sequences differ
from tool to tool:
| | =%f= | =%F= | =%L= |
|-----------+----------------+----------------+-------------------|
| [[file:ltlfilt.org][=ltlfilt=]] | output formula | input filename | input line |
| [[file:genltl.org][=genltl=]] | output formula | pattern name | pattern parameter |
| [[file:randltl.org][=randltl=]] | output formula | (empty) | formula number |
# LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck
# LocalWords: utf associativity
......@@ -253,6 +253,23 @@ It is therefore equivalent, but that is not a surprise since the
[[http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps][this procedure]] (calling the =remove_x()= function, and building automata
to check the equivalence of the resulting formula with the original one).
* Using =--format=
The =--format= option can be used the alter the way formulas are output (for instance use
#+HTML: <code>--latex --format='$%f$'</code>
to enclose formula in LaTeX format with =$...$=). You may also find
=--format= useful in more complex scenarios. For instance you could
print the only the line numbers containing formulas matching some
criterion. In the following, we print only the numbers of the lines
of =scheck.ltl= that contain guarantee formulas:
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --lbt-input -F scheck.ltl --guarantee --format=%L
#+END_SRC
#+RESULTS:
: 2
: 3
: 4
# LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck
# LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc
......
......@@ -20,14 +20,17 @@
#include "common_sys.hh"
#include "common_output.hh"
#include <iostream>
#include <sstream>
#include "ltlvisit/tostring.hh"
#include "ltlvisit/lbt.hh"
#include "misc/formater.hh"
#include "common_cout.hh"
#include "error.h"
#define OPT_SPOT 1
#define OPT_WRING 2
#define OPT_LATEX 3
#define OPT_FORMAT 4
output_format_t output_format = spot_output;
bool full_parenth = false;
......@@ -42,44 +45,13 @@ static const argp_option options[] =
{ "wring", OPT_WRING, 0, 0, "output in Wring's syntax", -20 },
{ "utf8", '8', 0, 0, "output using UTF-8 characters", -20 },
{ "latex", OPT_LATEX, 0, 0, "output using LaTeX macros", -20 },
{ "format", OPT_FORMAT, "FORMAT", 0,
"specify how each line should be output (default: \"%f\")", -20 },
{ 0, 0, 0, 0, 0, 0 }
};
const struct argp output_argp = { options, parse_opt_output, 0, 0, 0, 0, 0 };
int
parse_opt_output(int key, char*, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
output_format = utf8_output;
break;
case 'l':
output_format = lbt_output;
break;
case 'p':
full_parenth = true;
break;
case 's':
output_format = spin_output;
break;
case OPT_LATEX:
output_format = latex_output;
break;
case OPT_SPOT:
output_format = spot_output;
break;
case OPT_WRING:
output_format = wring_output;
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
static
void
report_not_ltl(const spot::ltl::formula* f,
......@@ -94,40 +66,154 @@ report_not_ltl(const spot::ltl::formula* f,
error(2, 0, msg, s.c_str(), syn);
}
void
output_formula(const spot::ltl::formula* f, const char* filename, int linenum)
static void
stream_formula(std::ostream& out,
const spot::ltl::formula* f, const char* filename, int linenum)
{
switch (output_format)
{
case lbt_output:
if (f->is_ltl_formula())
spot::ltl::to_lbt_string(f, std::cout);
spot::ltl::to_lbt_string(f, out);
else
report_not_ltl(f, filename, linenum, "LBT");
break;
case spot_output:
spot::ltl::to_string(f, std::cout, full_parenth);
spot::ltl::to_string(f, out, full_parenth);
break;
case spin_output:
if (f->is_ltl_formula())
spot::ltl::to_spin_string(f, std::cout, full_parenth);
spot::ltl::to_spin_string(f, out, full_parenth);
else
report_not_ltl(f, filename, linenum, "Spin");
break;
case wring_output:
if (f->is_ltl_formula())
spot::ltl::to_wring_string(f, std::cout);
spot::ltl::to_wring_string(f, out);
else
report_not_ltl(f, filename, linenum, "Wring");
break;
case utf8_output:
spot::ltl::to_utf8_string(f, std::cout, full_parenth);
spot::ltl::to_utf8_string(f, out, full_parenth);
break;
case latex_output:
spot::ltl::to_latex_string(f, std::cout, full_parenth);
spot::ltl::to_latex_string(f, out, full_parenth);
break;
}
}
namespace
{
struct formula_with_location
{
const spot::ltl::formula* f;
const char* filename;
int line;
};
class printable_formula:
public spot::printable_value<const formula_with_location*>
{
public:
printable_formula&
operator=(const formula_with_location* new_val)
{
val_ = new_val;
return *this;
}
virtual void
print(std::ostream& os, const char*) const
{
stream_formula(os,
val_->f,
val_->filename,
val_->line);
}
};
class formula_printer: protected spot::formater
{
public:
formula_printer(std::ostream& os, const char* format)
: format_(format)
{
declare('f', &fl_);
declare('F', &filename_);
declare('L', &line_);
set_output(os);
}
std::ostream&
print(const formula_with_location& fl)
{
fl_ = &fl;
filename_ = fl.filename ? fl.filename : "";
line_ = fl.line;
return format(format_);
}
private:
const char* format_;
printable_formula fl_;
spot::printable_value<const char*> filename_;
spot::printable_value<int> line_;
};
}
static formula_printer* format = 0;
int
parse_opt_output(int key, char* arg, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
{
case '8':
output_format = utf8_output;
break;
case 'l':
output_format = lbt_output;
break;
case 'p':
full_parenth = true;
break;
case 's':
output_format = spin_output;
break;
case OPT_LATEX:
output_format = latex_output;
break;
case OPT_SPOT:
output_format = spot_output;
break;
case OPT_WRING:
output_format = wring_output;
break;
case OPT_FORMAT:
delete format;
format = new formula_printer(std::cout, arg);
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
void
output_formula(const spot::ltl::formula* f, const char* filename, int linenum)
{
if (!format)
{
stream_formula(std::cout, f, filename, linenum);
}
else
{
formula_with_location fl = { f, filename, linenum };
format->print(fl);
}
// Make sure we abort if we can't write to std::cout anymore
// (like disk full or broken pipe with SIGPIPE ignored).
std::cout << std::endl;
......
......@@ -96,26 +96,52 @@ using namespace spot::ltl;
const char argp_program_doc[] ="\
Generate temporal logic formulas from predefined scalable patterns.";
#define OPT_AND_F 2
#define OPT_AND_FG 3
#define OPT_AND_GF 4
#define OPT_CCJ_ALPHA 5
#define OPT_CCJ_BETA 6
#define OPT_CCJ_BETA_PRIME 7
#define OPT_GH_Q 8
#define OPT_GH_R 9
#define OPT_GO_THETA 10
#define OPT_OR_FG 11
#define OPT_OR_G 12
#define OPT_OR_GF 13
#define OPT_R_LEFT 14
#define OPT_R_RIGHT 15
#define OPT_RV_COUNTER 16
#define OPT_RV_COUNTER_CARRY 17
#define OPT_RV_COUNTER_CARRY_LINEAR 18
#define OPT_RV_COUNTER_LINEAR 19
#define OPT_U_LEFT 20
#define OPT_U_RIGHT 21
#define OPT_AND_F 1
#define OPT_AND_FG 2
#define OPT_AND_GF 3
#define OPT_CCJ_ALPHA 4
#define OPT_CCJ_BETA 5
#define OPT_CCJ_BETA_PRIME 6
#define OPT_GH_Q 7
#define OPT_GH_R 8
#define OPT_GO_THETA 9
#define OPT_OR_FG 10
#define OPT_OR_G 11
#define OPT_OR_GF 12
#define OPT_R_LEFT 13
#define OPT_R_RIGHT 14
#define OPT_RV_COUNTER 15
#define OPT_RV_COUNTER_CARRY 16
#define OPT_RV_COUNTER_CARRY_LINEAR 17
#define OPT_RV_COUNTER_LINEAR 18
#define OPT_U_LEFT 19
#define OPT_U_RIGHT 20
#define LAST_CLASS 20
const char* const class_name[LAST_CLASS] =
{
"and-f",
"and-fg",
"and-gf",
"ccj-alpha",
"ccj-beta",
"ccj-beta-prime",
"gh-q",
"gh-r",
"go-theta",
"or-fg",
"or-g",
"or-gf",
"or-r-left",
"or-r-right",
"rv-counter",
"rv-counter-carry",
"rv-counter-carry-linear",
"rv-counter-linear",
"u-left",
"u-right",
};
#define OPT_ALIAS(o) { #o, 0, 0, OPTION_ALIAS, 0, 0 }
......@@ -168,6 +194,16 @@ static const argp_option options[] =
RANGE_DOC,
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
"the following interpreted sequences:", -19 },
{ "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula (in the selected syntax)", 0 },
{ "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the name of the pattern", 0 },
{ "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the argument of the pattern", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
};
......@@ -810,7 +846,7 @@ output_pattern(int pattern, int n)
f = r;
}
output_formula(f);
output_formula(f, class_name[pattern - 1], n);
f->destroy();
}
......
......@@ -153,6 +153,16 @@ static const argp_option options[] =
"drop formulas that have already been output (not affected by -v)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
"the following interpreted sequences:", -19 },
{ "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula (in the selected syntax)", 0 },
{ "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the name of the input file", 0 },
{ "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the original line number in the input file", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
};
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -107,6 +107,14 @@ static const argp_option options[] =
"listed by --dump-priorities.", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
"the following interpreted sequences:", -19 },
{ "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula (in the selected syntax)", 0 },
{ "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the (serial) number of the formula", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ 0, 0, 0, 0, 0, 0 }
};
......@@ -387,7 +395,8 @@ main(int argc, char** argv)
if (trials == 0)
error(2, 0, "failed to generate a new unique formula after %d trials",
MAX_TRIALS);
output_formula(f);
static int count = 0;
output_formula(f, 0, ++count);
f->destroy();
};
......
......@@ -44,13 +44,13 @@ cat <<\EOF
\usepackage{amsmath}
\usepackage{spotltl}
\begin{document}
\begin{align}
\begin{tabular}{ll}
EOF
( ../../bin/ltlfilt --latex input;
../../bin/genltl --go-theta=1..3 --latex ) | sed 's/$/\\\\/'
( ../../bin/ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\';
../../bin/genltl --go-theta=1..3 --latex \
--format='\texttt{--%F:%L} & $%f$ \\')
cat <<\EOF
\text{done}
\end{align}
\end{tabular}
\end{document}
EOF
) > output.tex
......
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