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

ltlfilt: add a --max-count/-n option

This fixes #44.

* src/bin/ltlfilt.cc: Implement -n/--max-count.
* doc/org/ltlfilt.org, src/tgbatest/randpsl.test: Use it
* NEWS: Document it.
parent ae234d2e
......@@ -29,6 +29,10 @@ New in spot 1.99a (not yet released)
same as in grep (and also autfilt): disable all normal
input, for situtations where only the exit status matters.
- ltlfilt's old -n/--negate option can only be used as --negate
now. The short '-n NUM' option is now the same as the new
--max-count=N option, for consistency with other tools.
- There is a parser for the HOA format
(http://adl.github.io/hoaf/) available as a
spot::hoa_stream_parser object or spot::hoa_parse() function.
......
......@@ -234,30 +234,29 @@ formulas that respect certain constraints. For instance let us
generate 10 formulas that are equivalent to =a U b=:
#+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' | head -n 10
randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' -n 10
#+END_SRC
#+RESULTS:
#+begin_example
!(!a R !b)
(!Gb -> a) U b
a U b
Fb & (a W b)
((a <-> !(a | b)) W a) U ((!b M b) U b)
(b <-> (Xb M a)) -> b
(b W Fb) & ((Fb xor (a W b)) -> (a U b))
(b U (a W b)) U b
!(!b W (!a & !b))
(a M (a <-> (a xor !a))) U b
(a U b) | ((a & Xa) M Gb)
(a | b) U b
((!b U b) -> (a W b)) U b
(a xor b) U b
b R (Fb & (a U (a W b)))
(b xor !b) -> ((b W a) U b)
(!a -> ((a W b) W (a & b))) U b
(a U b) | (Ga U b)
#+end_example
The =-n -1= option to =randltl= will cause it to output an infinite
stream of random formulas. =ltlfilt=, which reads its standard input
by default, will select only those equivalent to =a U b=. The output
of =ltlfilt= would still be an infinite stream of random formulas, so
we display only the first 10 using the standard =head= utility. Less
trivial formulas could be obtained by adding the =-r= option to
=randltl= (or equivalently adding the =-r= and =-u= option to
=ltlfilt=).
of =ltlfilt= is limited to 10 formulas using =-n 10=. (As would using
=| head -n 10=.) Less trivial formulas could be obtained by adding
the =-r= option to =randltl= (or equivalently adding the =-r= and =-u=
option to =ltlfilt=).
Another similar example, that requires two calls to =ltlfilt=, is the
......@@ -268,20 +267,20 @@ then ignoring all syntactic safety formulas, and keeping only the
safety formulas in the remaining list.
#+BEGIN_SRC sh :results verbatim :exports both
randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety | head -n 10
randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety -n 10
#+END_SRC
#+RESULTS:
#+begin_example
(!a & Fa) R Xa
!a | (a & b) | (((!a & b) | (a & !b)) M (!a M X!a))
G(!a M Xa)
G((G!b & !a) | (a & Fb)) R a
G!a M !a
G(!a M ((!b & XGb) | (b & XF!b)))
F(b | G!b)
F(Xa | G!a)
G(XXa | (b & F!a))
G((!a & (!a M !b)) | (a & (a W b)))
G(!b | Gb | X(b & Fa))
((!a | X(!a R (!b U !a))) & X((!a & !b) | (a & b))) | (a & X(((!a & b) | (a & !b)) & (b R a)))
(F!a & (a | G!a)) R Xa
(b M XGb) W XXa
G(Xa & (!a U G!b))
(a & F!a) R X(a | b)
!a | (a & (a M !b))
b U XGb
(!a | (a R (!a | Xa))) M X!a
Ga | (!b U !a)
#+end_example
......
......@@ -166,6 +166,7 @@ static const argp_option options[] =
/**************************************************/
{ 0, 0, 0, 0, "Output options:", -20 },
{ "quiet", 'q', 0, 0, "suppress all normal output", 0 },
{ "max-count", 'n', "NUM", 0, "output at most NUM formulas", 0 },
{ 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,
......@@ -230,6 +231,7 @@ static bool remove_x = false;
static bool stutter_insensitive = false;
static bool ap = false;
static unsigned ap_n = 0;
static int opt_max_count = -1;
static const spot::ltl::formula* implied_by = 0;
static const spot::ltl::formula* imply = 0;
......@@ -245,6 +247,14 @@ to_int(const char* s)
return res;
}
static int
to_pos_int(const char* s)
{
int res = to_int(s);
if (res < 0)
error(2, 0, "%d is not positive", res);
return res;
}
static const spot::ltl::formula*
parse_formula_arg(const std::string& input)
......@@ -264,6 +274,9 @@ parse_opt(int key, char* arg, struct argp_state*)
// This switch is alphabetically-ordered.
switch (key)
{
case 'n':
opt_max_count = to_pos_int(arg);
break;
case 'q':
output_format = quiet_output;
break;
......@@ -475,6 +488,13 @@ namespace
process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0)
{
if (opt_max_count == 0)
{
abort_run = true;
f->destroy();
return 0;
}
if (negate)
f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
......@@ -603,6 +623,8 @@ namespace
{
one_match = true;
output_formula_checked(f, filename, linenum, prefix, suffix);
if (opt_max_count > 0)
--opt_max_count;
}
f->destroy();
return 0;
......
......@@ -27,6 +27,8 @@ set -e
# formulae, and that have a size of at lease 12.
../../bin/randltl -n -1 --tree-size 30 --seed 0 --psl a b c |
../../bin/ltlfilt -r --size-min 12 --unique |
../../bin/ltlfilt -v --ltl | head -n 50 |
../../bin/ltlfilt -v --ltl -n 50 | tee formulas |
../../bin/ltlcross '../ltl2tgba -R3 -t %f >%T' '../ltl2tgba -x -R3 -t %f >%T' \
-F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}'
test `wc -l < formulas` = 50
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