diff --git a/NEWS b/NEWS index 06a228272..d60777c02 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,11 @@ New in spot 1.99a (not yet released) The implementation is actually much more efficient than the previous implementation that was only for LTL. + - ltlfilt's old -q/--quiet option has been renamed to + --ignore-errors. The new -q/--quiet semantic is the + same as in grep (and also autfilt): disable all normal + input, for situtations where only the exit status matters. + - 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. diff --git a/bench/dtgbasat/prepare.sh b/bench/dtgbasat/prepare.sh index 37819ce95..94d3a206d 100755 --- a/bench/dtgbasat/prepare.sh +++ b/bench/dtgbasat/prepare.sh @@ -5,7 +5,7 @@ ltl2tgba=../../src/bin/ltl2tgba dstar2tgba=../../src/bin/dstar2tgba # Rename all formulas using a b c... suppress duplicates. -$ltlfilt -q --relabel=abc -u formulas > nodups.ltl +$ltlfilt --ignore-errors --relabel=abc -u formulas > nodups.ltl while read f; do acc=`$ltl2tgba "$f" --low -a --stats="%a"` diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index b07efa972..1cf5f926a 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -104,6 +104,8 @@ stream_formula(std::ostream& out, case latex_output: spot::ltl::to_latex_string(f, out, full_parenth); break; + case quiet_output: + break; } } @@ -259,6 +261,8 @@ output_formula_checked(const spot::ltl::formula* f, const char* filename, int linenum, const char* prefix, const char* suffix) { + if (output_format == quiet_output) + return; output_formula(std::cout, f, filename, linenum, prefix, suffix); std::cout << std::endl; // Make sure we abort if we can't write to std::cout anymore diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index ac2cd70fb..781d04b36 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -28,7 +28,8 @@ #include "common_output.hh" enum output_format_t { spot_output, spin_output, utf8_output, - lbt_output, wring_output, latex_output }; + lbt_output, wring_output, latex_output, + quiet_output }; extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 0eaf15281..54f6bdf47 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -84,6 +84,7 @@ Exit status:\n\ #define OPT_REMOVE_X 28 #define OPT_STUTTER_INSENSITIVE 29 #define OPT_AP_N 30 +#define OPT_IGNORE_ERRORS 31 static const argp_option options[] = { @@ -93,7 +94,8 @@ static const argp_option options[] = "output erroneous lines as-is without processing", 0 }, { "drop-errors", OPT_DROP_ERRORS, 0, 0, "discard erroneous lines (default)", 0 }, - { "quiet", 'q', 0, 0, "do not report syntax errors", 0 }, + { "ignore-errors", OPT_IGNORE_ERRORS, 0, 0, + "do not report syntax errors", 0 }, /**************************************************/ { 0, 0, 0, 0, "Transformation options:", 3 }, { "negate", 'n', 0, 0, "negate each formula", 0 }, @@ -162,6 +164,7 @@ static const argp_option options[] = "drop formulas that have already been output (not affected by -v)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, + { "quiet", 'q', 0, 0, "suppress all normal output", 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, @@ -194,7 +197,7 @@ static bool one_match = false; enum error_style_t { drop_errors, skip_errors }; static error_style_t error_style = drop_errors; -static bool quiet = false; +static bool ignore_errors = false; static bool nnf = false; static bool negate = false; static bool boolean_to_isop = false; @@ -264,7 +267,7 @@ parse_opt(int key, char* arg, struct argp_state*) negate = true; break; case 'q': - quiet = true; + output_format = quiet_output; break; case OPT_R: parse_r(arg); @@ -307,6 +310,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_GUARANTEE: guarantee = obligation = true; break; + case OPT_IGNORE_ERRORS: + ignore_errors = true; + break; case OPT_IMPLIED_BY: { const spot::ltl::formula* i = parse_formula_arg(arg); @@ -436,7 +442,7 @@ namespace if (!f || pel.size() > 0) { - if (!quiet) + if (!ignore_errors) { if (filename) error_at_line(0, 0, filename, linenum, "parse error:"); @@ -451,7 +457,7 @@ namespace else assert(error_style == drop_errors); check_cout(); - return !quiet; + return !ignore_errors; } try { diff --git a/src/ltltest/remove_x.test b/src/ltltest/remove_x.test index e81dca283..c4fb448a6 100755 --- a/src/ltltest/remove_x.test +++ b/src/ltltest/remove_x.test @@ -19,21 +19,21 @@ . ./defs -run 0 ../../bin/ltlfilt --remove-x -f 'Xa' --equivalent-to 'Ga | (!a & Fa)' +run 0 ../../bin/ltlfilt -q --remove-x -f 'Xa' --equivalent-to 'Ga | (!a & Fa)' -run 1 ../../bin/ltlfilt --stutter-invariant -f 'Xa' +run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'Xa' -run 0 ../../bin/ltlfilt --stutter-invariant -f 'F(!a & Xa & Xb)' +run 0 ../../bin/ltlfilt -q --stutter-invariant -f 'F(!a & Xa & Xb)' -run 1 ../../bin/ltlfilt --stutter-invariant -f 'F(Xa & Xb)' +run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'F(Xa & Xb)' run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xa & Xb)' > out grep -v X out -run 0 ../../bin/ltlfilt --stutter-invariant -F 'out' +run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out' -run 1 ../../bin/ltlfilt --stutter-invariant -f 'F(!a & Xb)' +run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'F(!a & Xb)' run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xb)' > out grep -v X out # The output is stutter invariant, even if the input wasn't. -run 0 ../../bin/ltlfilt --stutter-invariant -F 'out' +run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out'