ltlfilt: replace --[b]size-max/min by --[b]size
* bin/ltlfilt.cc: Implement the new option, and hide the old ones. * doc/org/ltlfilt.org, NEWS: Document these options. * tests/core/ltl2dstar2.test, tests/core/randpsl.test: Adjust tests to the new syntax.
This commit is contained in:
Alexandre Duret-Lutz
parent
a3e0c8624e
commit
1b12df46fe
5 changed files with 108 additions and 32 deletions
5
NEWS
5
NEWS
|
|
@ -43,6 +43,11 @@ New in spot 1.99.7a (not yet released)
|
|||
* autfilt has a new option, --equivalent-to, to filter automata
|
||||
that are equivalent (language-wise) to a given automaton.
|
||||
|
||||
* ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and
|
||||
--bsize-max=N have been reimplemented as --size=RANGE and
|
||||
--bsize=RANGE. The old names are still supported for backward
|
||||
compatibility, but they are not documented anymore.
|
||||
|
||||
Library:
|
||||
|
||||
* Building products with different dictionaries now raise an
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@
|
|||
#include "common_cout.hh"
|
||||
#include "common_conv.hh"
|
||||
#include "common_r.hh"
|
||||
#include "common_range.hh"
|
||||
|
||||
#include <spot/misc/hash.hh>
|
||||
#include <spot/tl/simplify.hh>
|
||||
|
|
@ -59,6 +60,7 @@ enum {
|
|||
OPT_AP_N = 256,
|
||||
OPT_BOOLEAN,
|
||||
OPT_BOOLEAN_TO_ISOP,
|
||||
OPT_BSIZE,
|
||||
OPT_BSIZE_MAX,
|
||||
OPT_BSIZE_MIN,
|
||||
OPT_DEFINE,
|
||||
|
|
@ -79,6 +81,7 @@ enum {
|
|||
OPT_REMOVE_WM,
|
||||
OPT_REMOVE_X,
|
||||
OPT_SAFETY,
|
||||
OPT_SIZE,
|
||||
OPT_SIZE_MAX,
|
||||
OPT_SIZE_MIN,
|
||||
OPT_SKIP_ERRORS,
|
||||
|
|
@ -166,13 +169,21 @@ static const argp_option options[] =
|
|||
"match guarantee formulas (even pathological)", 0 },
|
||||
{ "obligation", OPT_OBLIGATION, nullptr, 0,
|
||||
"match obligation formulas (even pathological)", 0 },
|
||||
{ "size-max", OPT_SIZE_MAX, "INT", 0,
|
||||
{ "size", OPT_SIZE, "RANGE", 0,
|
||||
"match formulas with size in RANGE", 0},
|
||||
// backward compatibility
|
||||
{ "size-max", OPT_SIZE_MAX, "INT", OPTION_HIDDEN,
|
||||
"match formulas with size <= INT", 0 },
|
||||
{ "size-min", OPT_SIZE_MIN, "INT", 0,
|
||||
// backward compatibility
|
||||
{ "size-min", OPT_SIZE_MIN, "INT", OPTION_HIDDEN,
|
||||
"match formulas with size >= INT", 0 },
|
||||
{ "bsize-max", OPT_BSIZE_MAX, "INT", 0,
|
||||
{ "bsize", OPT_BSIZE, "RANGE", 0,
|
||||
"match formulas with Boolean size in RANGE", 0 },
|
||||
// backward compatibility
|
||||
{ "bsize-max", OPT_BSIZE_MAX, "INT", OPTION_HIDDEN,
|
||||
"match formulas with Boolean size <= INT", 0 },
|
||||
{ "bsize-min", OPT_BSIZE_MIN, "INT", 0,
|
||||
// backward compatibility
|
||||
{ "bsize-min", OPT_BSIZE_MIN, "INT", OPTION_HIDDEN,
|
||||
"match formulas with Boolean size >= INT", 0 },
|
||||
{ "implied-by", OPT_IMPLIED_BY, "FORMULA", 0,
|
||||
"match formulas implied by FORMULA", 0 },
|
||||
|
|
@ -188,6 +199,7 @@ static const argp_option options[] =
|
|||
{ "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
|
||||
{ "unique", 'u', nullptr, 0,
|
||||
"drop formulas that have already been output (not affected by -v)", 0 },
|
||||
RANGE_DOC_FULL,
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", -20 },
|
||||
{ "count", 'c', nullptr, 0, "print only a count of matched formulas", 0 },
|
||||
|
|
@ -245,10 +257,8 @@ static bool syntactic_si = false;
|
|||
static bool safety = false;
|
||||
static bool guarantee = false;
|
||||
static bool obligation = false;
|
||||
static int size_min = -1;
|
||||
static int size_max = -1;
|
||||
static int bsize_min = -1;
|
||||
static int bsize_max = -1;
|
||||
static range size = { -1, -1 };
|
||||
static range bsize = { -1, -1 };
|
||||
enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling };
|
||||
static relabeling_mode relabeling = NoRelabeling;
|
||||
static spot::relabeling_style style = spot::Abc;
|
||||
|
|
@ -320,11 +330,14 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
case OPT_BOOLEAN_TO_ISOP:
|
||||
boolean_to_isop = true;
|
||||
break;
|
||||
case OPT_BSIZE:
|
||||
bsize = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||
break;
|
||||
case OPT_BSIZE_MIN:
|
||||
bsize_min = to_int(arg);
|
||||
bsize.min = to_int(arg);
|
||||
break;
|
||||
case OPT_BSIZE_MAX:
|
||||
bsize_max = to_int(arg);
|
||||
bsize.max = to_int(arg);
|
||||
break;
|
||||
case OPT_DEFINE:
|
||||
opt->output_define.reset(new output_file(arg ? arg : "-"));
|
||||
|
|
@ -398,11 +411,14 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
case OPT_SAFETY:
|
||||
safety = obligation = true;
|
||||
break;
|
||||
case OPT_SIZE:
|
||||
size = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||
break;
|
||||
case OPT_SIZE_MIN:
|
||||
size_min = to_int(arg);
|
||||
size.min = to_int(arg);
|
||||
break;
|
||||
case OPT_SIZE_MAX:
|
||||
size_max = to_int(arg);
|
||||
size.max = to_int(arg);
|
||||
break;
|
||||
case OPT_SKIP_ERRORS:
|
||||
error_style = skip_errors;
|
||||
|
|
@ -564,18 +580,18 @@ namespace
|
|||
matched &= !syntactic_si || f.is_syntactic_stutter_invariant();
|
||||
matched &= !ap || atomic_prop_collect(f)->size() == ap_n;
|
||||
|
||||
if (matched && (size_min > 0 || size_max >= 0))
|
||||
if (matched && (size.min > 0 || size.max >= 0))
|
||||
{
|
||||
int l = spot::length(f);
|
||||
matched &= (size_min <= 0) || (l >= size_min);
|
||||
matched &= (size_max < 0) || (l <= size_max);
|
||||
matched &= (size.min <= 0) || (l >= size.min);
|
||||
matched &= (size.max < 0) || (l <= size.max);
|
||||
}
|
||||
|
||||
if (matched && (bsize_min > 0 || bsize_max >= 0))
|
||||
if (matched && (bsize.min > 0 || bsize.max >= 0))
|
||||
{
|
||||
int l = spot::length_boolone(f);
|
||||
matched &= (bsize_min <= 0) || (l >= bsize_min);
|
||||
matched &= (bsize_max < 0) || (l <= bsize_max);
|
||||
matched &= (bsize.min <= 0) || (l >= bsize.min);
|
||||
matched &= (bsize.max < 0) || (l <= bsize.max);
|
||||
}
|
||||
|
||||
matched &= !opt->implied_by || simpl.implication(opt->implied_by, f);
|
||||
|
|
|
|||
|
|
@ -253,20 +253,19 @@ ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
--ap=N match formulas which use exactly N atomic
|
||||
propositions
|
||||
--boolean match Boolean formulas
|
||||
--bsize-max=INT match formulas with Boolean size <= INT
|
||||
--bsize-min=INT match formulas with Boolean size >= INT
|
||||
--bsize=RANGE match formulas with Boolean size in RANGE
|
||||
--equivalent-to=FORMULA match formulas equivalent to FORMULA
|
||||
--eventual match pure eventualities
|
||||
--guarantee match guarantee formulas (even pathological)
|
||||
--implied-by=FORMULA match formulas implied by FORMULA
|
||||
--imply=FORMULA match formulas implying FORMULA
|
||||
--ltl match only LTL formulas (no PSL operator)
|
||||
--nox match X-free formulas
|
||||
--obligation match obligation formulas (even pathological)
|
||||
--safety match safety formulas (even pathological)
|
||||
--size-max=INT match formulas with size <= INT
|
||||
--size-min=INT match formulas with size >= INT
|
||||
--size=RANGE match formulas with size in RANGE
|
||||
--stutter-insensitive, --stutter-invariant
|
||||
match stutter-insensitive LTL formulas
|
||||
--syntactic-guarantee match syntactic-guarantee formulas
|
||||
|
|
@ -274,6 +273,9 @@ ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|||
--syntactic-persistence match syntactic-persistence formulas
|
||||
--syntactic-recurrence match syntactic-recurrence formulas
|
||||
--syntactic-safety match syntactic-safety formulas
|
||||
--syntactic-stutter-invariant, --nox
|
||||
match stutter-invariant formulas syntactically
|
||||
(LTL-X or siPSL)
|
||||
--universal match purely universal formulas
|
||||
-u, --unique drop formulas that have already been output (not
|
||||
affected by -v)
|
||||
|
|
@ -389,6 +391,61 @@ ltlfilt -f 'F(a & X(!a & Gb))' --remove-x | ltlfilt --equivalent-to 'F(a & X(!a
|
|||
|
||||
It is therefore equivalent (otherwise the output would have been empty).
|
||||
|
||||
|
||||
The difference between =--size= and =--bsize= lies in the way Boolean
|
||||
subformula are counted. With =--size= the size of the formula is
|
||||
exactly the number of atomic propositions and operators used. For
|
||||
instance the following command generates 10 random formulas with size
|
||||
5 (the reason [[file:randltl.org][=randltl=]] uses =--tree-size=8= is because the "tree" of
|
||||
the formula generated randomly can be reduced by trivial
|
||||
simplifications such as =!!f= being rewritten to =f=, yielding
|
||||
formulas of smaller sizes).
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randltl -n -1 --tree-size=8 a b | ltlfilt --size=5 -n 10
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
!F!Ga
|
||||
X!(a U b)
|
||||
!G(a & b)
|
||||
(b W a) W 0
|
||||
b R X!b
|
||||
GF!Xa
|
||||
Xb & Ga
|
||||
a xor !Fb
|
||||
a xor FXb
|
||||
!(0 R Fb)
|
||||
#+end_example
|
||||
|
||||
With =--bsize=, any Boolean subformula is counted as "1" in the total
|
||||
size. So =F(a & b & c)= would have Boolean-size 2. This type of size
|
||||
is probably a better way to classify formulas that are going to be
|
||||
translated as automata, since transitions are labeled by Boolean
|
||||
formulas: the complexity of the Boolean subformulas has little
|
||||
influence on the overall translation. Here are 10 random formula with
|
||||
Boolean-size 5:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randltl -n -1 --tree-size=12 a b | ltlfilt --bsize=5 -n 10
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
Gb xor Fa
|
||||
FX!Fa
|
||||
!(Fb U b)
|
||||
(a -> !b) & XFb
|
||||
X(b & Xb)
|
||||
0 R (a U !b)
|
||||
XXa R !b
|
||||
(!a & !(!a xor b)) xor (0 R b)
|
||||
GF(1 U b)
|
||||
(a U b) R b
|
||||
#+end_example
|
||||
|
||||
|
||||
* Using =--format=
|
||||
|
||||
The =--format= option can be used the alter the way formulas are output (for instance use
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2015 Laboratoire de Recherche et
|
||||
# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -47,8 +47,7 @@ head -n 20 > formulas
|
|||
|
||||
$randltl -n -1 a b --tree-size=5..15 |
|
||||
$ltlfilt -v --obligation |
|
||||
$ltlfilt --syntactic-recurrence --remove-wm -r -u \
|
||||
--size-min=4 --size-max=15 --relabel=abc |
|
||||
$ltlfilt --syntactic-recurrence --remove-wm -r -u --size=4..15 --relabel=abc |
|
||||
head -n 20 >> formulas
|
||||
|
||||
while read f; do
|
||||
|
|
@ -64,8 +63,7 @@ echo ==========================
|
|||
# For obligation formulas, the output of dstar2tgba should
|
||||
# have the same size as the input when option -D is used.
|
||||
$randltl -n -1 a b --tree-size=5..15 |
|
||||
$ltlfilt --obligation --size-min=4 --size-max=15 --relabel=abc \
|
||||
--remove-wm -r -u |
|
||||
$ltlfilt --obligation --size=4..15 --relabel=abc --remove-wm -r -u |
|
||||
head -n 20 > formulas
|
||||
|
||||
while read f; do
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
|
|
@ -24,9 +24,9 @@
|
|||
set -e
|
||||
|
||||
# Generate 50 random unique PSL formula that do not simplify to LTL
|
||||
# formulae, and that have a size of at lease 12.
|
||||
# formulae, and that have a size of at least 12.
|
||||
randltl -n -1 --tree-size 30 --seed 12 --psl a b c |
|
||||
ltlfilt -r --size-min 12 --unique |
|
||||
ltlfilt -r --size 12.. --unique |
|
||||
ltlfilt -v --ltl -n 50 | tee formulas |
|
||||
ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' \
|
||||
-F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue