From 0671d628069955483b9a3a845c78405e3459a3d7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Oct 2015 17:08:08 +0200 Subject: [PATCH] ltlgrind: fix handling of FILENAME/COL This additionally fixes #107. * src/bin/ltlgrind.cc: Fix handling for FILEANAME/COL. Document FORMAT in --help. Assume -F for arguments given without options. * src/tests/ltlgrind.test: Add two tests. * NEWS: Mention this. --- NEWS | 5 +++ src/bin/ltlgrind.cc | 92 +++++++++++++++++++++++++---------------- src/tests/ltlgrind.test | 20 ++++++++- 3 files changed, 79 insertions(+), 38 deletions(-) diff --git a/NEWS b/NEWS index 2711f5dc5..6072b1f93 100644 --- a/NEWS +++ b/NEWS @@ -13,6 +13,9 @@ New in spot 1.99.4a (not yet released) --high is given, thn the translation intent defaults to --small (unless specified otherwise). + * ltlgrind FILENAME[/COL] is now the same as + ltlgrind -F FILENAME[/COL] for consistency with ltlfilt. + Library: * Rename dtgba_complement() as dtwa_complement(), rename the header @@ -48,6 +51,8 @@ New in spot 1.99.4a (not yet released) * Handle saturation of formula reference counts. * Fix typo in the Python code for the CGI server. * "randaut -Q0 1" used to segfault. + * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. + * "ltlgrind --help" did not document FORMAT. New in spot 1.99.4 (2015-10-01) diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index 4415b63f6..de2becf04 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -51,43 +51,59 @@ static const char * argp_program_doc = "List formulas that are similar to but simpler than a given formula."; static const argp_option options[] = { - {nullptr, 0, nullptr, 0, - "Mutation rules (all enabled unless those options are used):", 15}, - {"ap-to-const", OPT_AP2CONST, nullptr, 0, - "atomic propositions are replaced with true/false", 15}, - {"remove-one-ap", OPT_REMOVE_ONE_AP, nullptr, 0, - "all occurrences of an atomic proposition are replaced with another " \ - "atomic proposition used in the formula", 15}, - {"remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, nullptr, 0, - "remove one operand from multops", 15}, - {"remove-ops", OPT_REMOVE_OPS, nullptr, 0, - "replace unary/binary operators with one of their operands", - 15}, - {"split-ops", OPT_SPLIT_OPS, nullptr, 0, - "when an operator can be expressed as a conjunction/disjunction using " \ - "simpler operators, each term of the conjunction/disjunction is a " \ - "mutation. e.g. a <-> b can be written as ((a & b) | (!a & !b)) or as " \ - "((a -> b) & (b -> a)) so those four terms can be a mutation of a <-> b", 0}, - {"rewrite-ops", OPT_REWRITE_OPS, nullptr, 0, - "rewrite operators that have a semantically simpler form: a U b becomes " \ - "a W b, etc.", 0}, - {"simplify-bounds", OPT_SIMPLIFY_BOUNDS, nullptr, 0, - "on a bounded unary operator, decrement one of the bounds, or set min to " \ - "0 or max to unbounded", 15}, - {nullptr, 0, nullptr, 0, "Output options:", 20}, - {"max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20}, - {"mutations", 'm', "NUM", 0, "number of mutations to apply to the " \ - "formulae (default: 1)", 0}, - {"sort", OPT_SORT, nullptr, 0, "sort the result by formula size", 0}, + { nullptr, 0, nullptr, 0, + "Mutation rules (all enabled unless those options are used):", 15}, + { "ap-to-const", OPT_AP2CONST, nullptr, 0, + "atomic propositions are replaced with true/false", 15 }, + { "remove-one-ap", OPT_REMOVE_ONE_AP, nullptr, 0, + "all occurrences of an atomic proposition are replaced with another " \ + "atomic proposition used in the formula", 15 }, + { "remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, nullptr, 0, + "remove one operand from multops", 15 }, + { "remove-ops", OPT_REMOVE_OPS, nullptr, 0, + "replace unary/binary operators with one of their operands", 15 }, + { "split-ops", OPT_SPLIT_OPS, nullptr, 0, + "when an operator can be expressed as a conjunction/disjunction using " + "simpler operators, each term of the conjunction/disjunction is a " + "mutation. e.g. a <-> b can be written as ((a & b) | (!a & !b)) or as " + "((a -> b) & (b -> a)) so those four terms can be a mutation of a <-> b", + 0 }, + { "rewrite-ops", OPT_REWRITE_OPS, nullptr, 0, + "rewrite operators that have a semantically simpler form: a U b becomes " + "a W b, etc.", 0 }, + { "simplify-bounds", OPT_SIMPLIFY_BOUNDS, nullptr, 0, + "on a bounded unary operator, decrement one of the bounds, or set min to " + "0 or max to unbounded", 15 }, + { nullptr, 0, nullptr, 0, "Output options:", 20 }, + { "max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20 }, + { "mutations", 'm', "NUM", 0, "number of mutations to apply to the " + "formulae (default: 1)", 0 }, + { "sort", OPT_SORT, nullptr, 0, "sort the result by formula size", 0 }, + { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use " + "the following interpreted sequences:", 21 }, + { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the formula (in the selected syntax)", 0 }, + { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the name of the input file", 0 }, + { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the original line number in the input file", 0 }, + { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the part of the line before the formula if it " + "comes from a column extracted from a CSV file", 0 }, + { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the part of the line after the formula if it " + "comes from a column extracted from a CSV file", 0 }, + { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, {nullptr, 0, nullptr, 0, "Miscellaneous options:", -1}, {nullptr, 0, nullptr, 0, nullptr, 0} }; static const argp_child children[] = { - {&finput_argp, 0, nullptr, 10}, - {&output_argp, 0, nullptr, 20}, - {&misc_argp, 0, nullptr, -1}, - {nullptr, 0, nullptr, 0} + { &finput_argp, 0, nullptr, 10 }, + { &output_argp, 0, nullptr, 20 }, + { &misc_argp, 0, nullptr, -1 }, + { nullptr, 0, nullptr, 0 } }; namespace @@ -102,7 +118,7 @@ namespace auto mutations = spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort); for (auto g: mutations) - output_formula_checked(g, filename, linenum); + output_formula_checked(g, filename, linenum, prefix, suffix); return 0; } }; @@ -119,6 +135,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'n': max_output = to_int(arg); break; + case ARGP_KEY_ARG: + // FIXME: use stat() to distinguish filename from string? + jobs.emplace_back(arg, true); + break; case OPT_AP2CONST: opt_all = 0; mut_opts |= spot::Mut_Ap2Const; @@ -161,8 +181,8 @@ main(int argc, char* argv[]) { setup(argv); - const argp ap = { options, parse_opt, nullptr, argp_program_doc, children, - nullptr, nullptr }; + const argp ap = { options, parse_opt, "[FILENAME[/COL]...]", argp_program_doc, + children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); @@ -170,7 +190,7 @@ main(int argc, char* argv[]) mut_opts |= opt_all; if (jobs.empty()) - jobs.push_back(job("-", 1)); + jobs.push_back(job("-", true)); mutate_processor processor; if (processor.run()) diff --git a/src/tests/ltlgrind.test b/src/tests/ltlgrind.test index 25890a903..8fda8e8f7 100755 --- a/src/tests/ltlgrind.test +++ b/src/tests/ltlgrind.test @@ -22,13 +22,18 @@ set -e -checkopt() +checkopt_noparse() { cat >exp run 0 ../../bin/ltlgrind --sort "$@" > out + diff exp out +} + +checkopt() +{ + checkopt_noparse "$@" # The result must be parsable ../../bin/ltlfilt out - diff exp out } checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' < Xp2) F({{1;p0}[:*]}[]-> Xp0) F({{p2;1}[:*]}[]-> Xp0) EOF + +echo '1,a,3' > input +checkopt_noparse input/2 <,%F,%L' <