ltlfilt: implement -q/--quiet as in grep
the existing -q/--quiet option is renamed to --ignore-errors * src/bin/ltlfilt.cc: Adjust option. * src/bin/common_output.cc, src/bin/common_output.hh: Add a quiet_output. * bench/dtgbasat/prepare.sh: Rename -q to --ignore-errors.. * src/ltltest/remove_x.test: Use -q. * NEWS: Mention this change.
This commit is contained in:
parent
1e84bb1ee7
commit
ac225c0ee9
6 changed files with 30 additions and 14 deletions
5
NEWS
5
NEWS
|
|
@ -24,6 +24,11 @@ New in spot 1.99a (not yet released)
|
||||||
The implementation is actually much more efficient
|
The implementation is actually much more efficient
|
||||||
than the previous implementation that was only for LTL.
|
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
|
- There is a parser for the HOA format
|
||||||
(http://adl.github.io/hoaf/) available as a
|
(http://adl.github.io/hoaf/) available as a
|
||||||
spot::hoa_stream_parser object or spot::hoa_parse() function.
|
spot::hoa_stream_parser object or spot::hoa_parse() function.
|
||||||
|
|
|
||||||
|
|
@ -5,7 +5,7 @@ ltl2tgba=../../src/bin/ltl2tgba
|
||||||
dstar2tgba=../../src/bin/dstar2tgba
|
dstar2tgba=../../src/bin/dstar2tgba
|
||||||
|
|
||||||
# Rename all formulas using a b c... suppress duplicates.
|
# 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
|
while read f; do
|
||||||
acc=`$ltl2tgba "$f" --low -a --stats="%a"`
|
acc=`$ltl2tgba "$f" --low -a --stats="%a"`
|
||||||
|
|
|
||||||
|
|
@ -104,6 +104,8 @@ stream_formula(std::ostream& out,
|
||||||
case latex_output:
|
case latex_output:
|
||||||
spot::ltl::to_latex_string(f, out, full_parenth);
|
spot::ltl::to_latex_string(f, out, full_parenth);
|
||||||
break;
|
break;
|
||||||
|
case quiet_output:
|
||||||
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -259,6 +261,8 @@ output_formula_checked(const spot::ltl::formula* f,
|
||||||
const char* filename, int linenum,
|
const char* filename, int linenum,
|
||||||
const char* prefix, const char* suffix)
|
const char* prefix, const char* suffix)
|
||||||
{
|
{
|
||||||
|
if (output_format == quiet_output)
|
||||||
|
return;
|
||||||
output_formula(std::cout, f, filename, linenum, prefix, suffix);
|
output_formula(std::cout, f, filename, linenum, prefix, suffix);
|
||||||
std::cout << std::endl;
|
std::cout << std::endl;
|
||||||
// Make sure we abort if we can't write to std::cout anymore
|
// Make sure we abort if we can't write to std::cout anymore
|
||||||
|
|
|
||||||
|
|
@ -28,7 +28,8 @@
|
||||||
#include "common_output.hh"
|
#include "common_output.hh"
|
||||||
|
|
||||||
enum output_format_t { spot_output, spin_output, utf8_output,
|
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 output_format_t output_format;
|
||||||
extern bool full_parenth;
|
extern bool full_parenth;
|
||||||
extern bool escape_csv;
|
extern bool escape_csv;
|
||||||
|
|
|
||||||
|
|
@ -84,6 +84,7 @@ Exit status:\n\
|
||||||
#define OPT_REMOVE_X 28
|
#define OPT_REMOVE_X 28
|
||||||
#define OPT_STUTTER_INSENSITIVE 29
|
#define OPT_STUTTER_INSENSITIVE 29
|
||||||
#define OPT_AP_N 30
|
#define OPT_AP_N 30
|
||||||
|
#define OPT_IGNORE_ERRORS 31
|
||||||
|
|
||||||
static const argp_option options[] =
|
static const argp_option options[] =
|
||||||
{
|
{
|
||||||
|
|
@ -93,7 +94,8 @@ static const argp_option options[] =
|
||||||
"output erroneous lines as-is without processing", 0 },
|
"output erroneous lines as-is without processing", 0 },
|
||||||
{ "drop-errors", OPT_DROP_ERRORS, 0, 0,
|
{ "drop-errors", OPT_DROP_ERRORS, 0, 0,
|
||||||
"discard erroneous lines (default)", 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 },
|
{ 0, 0, 0, 0, "Transformation options:", 3 },
|
||||||
{ "negate", 'n', 0, 0, "negate each formula", 0 },
|
{ "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 },
|
"drop formulas that have already been output (not affected by -v)", 0 },
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
{ 0, 0, 0, 0, "Output options:", -20 },
|
{ 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 "\
|
{ 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
|
||||||
"the following interpreted sequences:", -19 },
|
"the following interpreted sequences:", -19 },
|
||||||
{ "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%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 };
|
enum error_style_t { drop_errors, skip_errors };
|
||||||
static error_style_t error_style = drop_errors;
|
static error_style_t error_style = drop_errors;
|
||||||
static bool quiet = false;
|
static bool ignore_errors = false;
|
||||||
static bool nnf = false;
|
static bool nnf = false;
|
||||||
static bool negate = false;
|
static bool negate = false;
|
||||||
static bool boolean_to_isop = false;
|
static bool boolean_to_isop = false;
|
||||||
|
|
@ -264,7 +267,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
negate = true;
|
negate = true;
|
||||||
break;
|
break;
|
||||||
case 'q':
|
case 'q':
|
||||||
quiet = true;
|
output_format = quiet_output;
|
||||||
break;
|
break;
|
||||||
case OPT_R:
|
case OPT_R:
|
||||||
parse_r(arg);
|
parse_r(arg);
|
||||||
|
|
@ -307,6 +310,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
case OPT_GUARANTEE:
|
case OPT_GUARANTEE:
|
||||||
guarantee = obligation = true;
|
guarantee = obligation = true;
|
||||||
break;
|
break;
|
||||||
|
case OPT_IGNORE_ERRORS:
|
||||||
|
ignore_errors = true;
|
||||||
|
break;
|
||||||
case OPT_IMPLIED_BY:
|
case OPT_IMPLIED_BY:
|
||||||
{
|
{
|
||||||
const spot::ltl::formula* i = parse_formula_arg(arg);
|
const spot::ltl::formula* i = parse_formula_arg(arg);
|
||||||
|
|
@ -436,7 +442,7 @@ namespace
|
||||||
|
|
||||||
if (!f || pel.size() > 0)
|
if (!f || pel.size() > 0)
|
||||||
{
|
{
|
||||||
if (!quiet)
|
if (!ignore_errors)
|
||||||
{
|
{
|
||||||
if (filename)
|
if (filename)
|
||||||
error_at_line(0, 0, filename, linenum, "parse error:");
|
error_at_line(0, 0, filename, linenum, "parse error:");
|
||||||
|
|
@ -451,7 +457,7 @@ namespace
|
||||||
else
|
else
|
||||||
assert(error_style == drop_errors);
|
assert(error_style == drop_errors);
|
||||||
check_cout();
|
check_cout();
|
||||||
return !quiet;
|
return !ignore_errors;
|
||||||
}
|
}
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -19,21 +19,21 @@
|
||||||
|
|
||||||
. ./defs
|
. ./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
|
run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xa & Xb)' > out
|
||||||
grep -v X 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
|
run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xb)' > out
|
||||||
grep -v X out
|
grep -v X out
|
||||||
# The output is stutter invariant, even if the input wasn't.
|
# 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'
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue