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.
This commit is contained in:
parent
e3682a2301
commit
0671d62806
3 changed files with 79 additions and 38 deletions
5
NEWS
5
NEWS
|
|
@ -13,6 +13,9 @@ New in spot 1.99.4a (not yet released)
|
||||||
--high is given, thn the translation intent defaults to --small
|
--high is given, thn the translation intent defaults to --small
|
||||||
(unless specified otherwise).
|
(unless specified otherwise).
|
||||||
|
|
||||||
|
* ltlgrind FILENAME[/COL] is now the same as
|
||||||
|
ltlgrind -F FILENAME[/COL] for consistency with ltlfilt.
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
* Rename dtgba_complement() as dtwa_complement(), rename the header
|
* 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.
|
* Handle saturation of formula reference counts.
|
||||||
* Fix typo in the Python code for the CGI server.
|
* Fix typo in the Python code for the CGI server.
|
||||||
* "randaut -Q0 1" used to segfault.
|
* "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)
|
New in spot 1.99.4 (2015-10-01)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -51,43 +51,59 @@ static const char * argp_program_doc =
|
||||||
"List formulas that are similar to but simpler than a given formula.";
|
"List formulas that are similar to but simpler than a given formula.";
|
||||||
|
|
||||||
static const argp_option options[] = {
|
static const argp_option options[] = {
|
||||||
{nullptr, 0, nullptr, 0,
|
{ nullptr, 0, nullptr, 0,
|
||||||
"Mutation rules (all enabled unless those options are used):", 15},
|
"Mutation rules (all enabled unless those options are used):", 15},
|
||||||
{"ap-to-const", OPT_AP2CONST, nullptr, 0,
|
{ "ap-to-const", OPT_AP2CONST, nullptr, 0,
|
||||||
"atomic propositions are replaced with true/false", 15},
|
"atomic propositions are replaced with true/false", 15 },
|
||||||
{"remove-one-ap", OPT_REMOVE_ONE_AP, nullptr, 0,
|
{ "remove-one-ap", OPT_REMOVE_ONE_AP, nullptr, 0,
|
||||||
"all occurrences of an atomic proposition are replaced with another " \
|
"all occurrences of an atomic proposition are replaced with another " \
|
||||||
"atomic proposition used in the formula", 15},
|
"atomic proposition used in the formula", 15 },
|
||||||
{"remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, nullptr, 0,
|
{ "remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, nullptr, 0,
|
||||||
"remove one operand from multops", 15},
|
"remove one operand from multops", 15 },
|
||||||
{"remove-ops", OPT_REMOVE_OPS, nullptr, 0,
|
{ "remove-ops", OPT_REMOVE_OPS, nullptr, 0,
|
||||||
"replace unary/binary operators with one of their operands",
|
"replace unary/binary operators with one of their operands", 15 },
|
||||||
15},
|
{ "split-ops", OPT_SPLIT_OPS, nullptr, 0,
|
||||||
{"split-ops", OPT_SPLIT_OPS, nullptr, 0,
|
"when an operator can be expressed as a conjunction/disjunction using "
|
||||||
"when an operator can be expressed as a conjunction/disjunction using " \
|
"simpler operators, each term of the conjunction/disjunction is a "
|
||||||
"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 "
|
||||||
"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",
|
||||||
"((a -> b) & (b -> a)) so those four terms can be a mutation of a <-> b", 0},
|
0 },
|
||||||
{"rewrite-ops", OPT_REWRITE_OPS, nullptr, 0,
|
{ "rewrite-ops", OPT_REWRITE_OPS, nullptr, 0,
|
||||||
"rewrite operators that have a semantically simpler form: a U b becomes " \
|
"rewrite operators that have a semantically simpler form: a U b becomes "
|
||||||
"a W b, etc.", 0},
|
"a W b, etc.", 0 },
|
||||||
{"simplify-bounds", OPT_SIMPLIFY_BOUNDS, nullptr, 0,
|
{ "simplify-bounds", OPT_SIMPLIFY_BOUNDS, nullptr, 0,
|
||||||
"on a bounded unary operator, decrement one of the bounds, or set min to " \
|
"on a bounded unary operator, decrement one of the bounds, or set min to "
|
||||||
"0 or max to unbounded", 15},
|
"0 or max to unbounded", 15 },
|
||||||
{nullptr, 0, nullptr, 0, "Output options:", 20},
|
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
|
||||||
{"max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20},
|
{ "max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20 },
|
||||||
{"mutations", 'm', "NUM", 0, "number of mutations to apply to the " \
|
{ "mutations", 'm', "NUM", 0, "number of mutations to apply to the "
|
||||||
"formulae (default: 1)", 0},
|
"formulae (default: 1)", 0 },
|
||||||
{"sort", OPT_SORT, nullptr, 0, "sort the result by formula size", 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, "Miscellaneous options:", -1},
|
||||||
{nullptr, 0, nullptr, 0, nullptr, 0}
|
{nullptr, 0, nullptr, 0, nullptr, 0}
|
||||||
};
|
};
|
||||||
|
|
||||||
static const argp_child children[] = {
|
static const argp_child children[] = {
|
||||||
{&finput_argp, 0, nullptr, 10},
|
{ &finput_argp, 0, nullptr, 10 },
|
||||||
{&output_argp, 0, nullptr, 20},
|
{ &output_argp, 0, nullptr, 20 },
|
||||||
{&misc_argp, 0, nullptr, -1},
|
{ &misc_argp, 0, nullptr, -1 },
|
||||||
{nullptr, 0, nullptr, 0}
|
{ nullptr, 0, nullptr, 0 }
|
||||||
};
|
};
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
|
|
@ -102,7 +118,7 @@ namespace
|
||||||
auto mutations =
|
auto mutations =
|
||||||
spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort);
|
spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort);
|
||||||
for (auto g: mutations)
|
for (auto g: mutations)
|
||||||
output_formula_checked(g, filename, linenum);
|
output_formula_checked(g, filename, linenum, prefix, suffix);
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
@ -119,6 +135,10 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
case 'n':
|
case 'n':
|
||||||
max_output = to_int(arg);
|
max_output = to_int(arg);
|
||||||
break;
|
break;
|
||||||
|
case ARGP_KEY_ARG:
|
||||||
|
// FIXME: use stat() to distinguish filename from string?
|
||||||
|
jobs.emplace_back(arg, true);
|
||||||
|
break;
|
||||||
case OPT_AP2CONST:
|
case OPT_AP2CONST:
|
||||||
opt_all = 0;
|
opt_all = 0;
|
||||||
mut_opts |= spot::Mut_Ap2Const;
|
mut_opts |= spot::Mut_Ap2Const;
|
||||||
|
|
@ -161,8 +181,8 @@ main(int argc, char* argv[])
|
||||||
{
|
{
|
||||||
setup(argv);
|
setup(argv);
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, nullptr, argp_program_doc, children,
|
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]", argp_program_doc,
|
||||||
nullptr, nullptr };
|
children, nullptr, nullptr };
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
exit(err);
|
exit(err);
|
||||||
|
|
@ -170,7 +190,7 @@ main(int argc, char* argv[])
|
||||||
mut_opts |= opt_all;
|
mut_opts |= opt_all;
|
||||||
|
|
||||||
if (jobs.empty())
|
if (jobs.empty())
|
||||||
jobs.push_back(job("-", 1));
|
jobs.push_back(job("-", true));
|
||||||
|
|
||||||
mutate_processor processor;
|
mutate_processor processor;
|
||||||
if (processor.run())
|
if (processor.run())
|
||||||
|
|
|
||||||
|
|
@ -22,13 +22,18 @@
|
||||||
|
|
||||||
set -e
|
set -e
|
||||||
|
|
||||||
checkopt()
|
checkopt_noparse()
|
||||||
{
|
{
|
||||||
cat >exp
|
cat >exp
|
||||||
run 0 ../../bin/ltlgrind --sort "$@" > out
|
run 0 ../../bin/ltlgrind --sort "$@" > out
|
||||||
|
diff exp out
|
||||||
|
}
|
||||||
|
|
||||||
|
checkopt()
|
||||||
|
{
|
||||||
|
checkopt_noparse "$@"
|
||||||
# The result must be parsable
|
# The result must be parsable
|
||||||
../../bin/ltlfilt out
|
../../bin/ltlfilt out
|
||||||
diff exp out
|
|
||||||
}
|
}
|
||||||
|
|
||||||
checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <<EOF
|
checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <<EOF
|
||||||
|
|
@ -181,3 +186,14 @@ F({p2[*2][:*]}[]-> Xp2)
|
||||||
F({{1;p0}[:*]}[]-> Xp0)
|
F({{1;p0}[:*]}[]-> Xp0)
|
||||||
F({{p2;1}[:*]}[]-> Xp0)
|
F({{p2;1}[:*]}[]-> Xp0)
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
echo '1,a,3' > input
|
||||||
|
checkopt_noparse input/2 <<EOF
|
||||||
|
1,0,3
|
||||||
|
1,1,3
|
||||||
|
EOF
|
||||||
|
|
||||||
|
checkopt_noparse -F input/2 --format '%<,%f,%>,%F,%L' <<EOF
|
||||||
|
1,0,3,input,1
|
||||||
|
1,1,3,input,1
|
||||||
|
EOF
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue