From 1b12df46fe17510164d5c4052cac5da59ab84784 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Feb 2016 13:44:51 +0100 Subject: [PATCH] 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. --- NEWS | 5 +++ bin/ltlfilt.cc | 52 +++++++++++++++++++---------- doc/org/ltlfilt.org | 67 +++++++++++++++++++++++++++++++++++--- tests/core/ltl2dstar2.test | 8 ++--- tests/core/randpsl.test | 8 ++--- 5 files changed, 108 insertions(+), 32 deletions(-) diff --git a/NEWS b/NEWS index 871325fad..26fa1f5fe 100644 --- a/NEWS +++ b/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 diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index d832d9411..c278cb62c 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -33,6 +33,7 @@ #include "common_cout.hh" #include "common_conv.hh" #include "common_r.hh" +#include "common_range.hh" #include #include @@ -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::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::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); diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 83d22bc09..7f48010f7 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -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 diff --git a/tests/core/ltl2dstar2.test b/tests/core/ltl2dstar2.test index 1d1525bda..ff66d3918 100755 --- a/tests/core/ltl2dstar2.test +++ b/tests/core/ltl2dstar2.test @@ -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 diff --git a/tests/core/randpsl.test b/tests/core/randpsl.test index 1bcf69845..f06a75cc9 100755 --- a/tests/core/randpsl.test +++ b/tests/core/randpsl.test @@ -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)}}}}'