alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

remove options -! and -" from genltl

Browse source 
Fixes #237.

* bin/genltl.cc: Fix the numbering of options.
* NEWS: Mention the bugs.
This commit is contained in:
Alexandre Duret-Lutz 2017-03-01 16:17:05 +01:00
parent 18283d6907
commit 22a3d1c393
2 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -16,6 +16,9 @@ New in spot 2.3.1.dev (not yet released)
- Because of a typo, the output of --stats='...%P...' was correct
only if %p was used as well.
- genltl was never meant to have (randomly attributed) short
options for --postive and --negative.
Deprecation notices:
- Using --format=%a to print the number of atomic propositions in

9
bin/genltl.cc
View file

@ -167,7 +167,8 @@ const char argp_program_doc[] ="\
Generate temporal logic formulas from predefined patterns.";
enum {
OPT_AND_F = 1,
FIRST_CLASS = 256,
OPT_AND_F = FIRST_CLASS,
OPT_AND_FG,
OPT_AND_GF,
OPT_CCJ_ALPHA,
@ -203,7 +204,7 @@ enum {
OPT_NEGATIVE,
};
const char* const class_name[LAST_CLASS] =
const char* const class_name[LAST_CLASS - FIRST_CLASS] =
{
"and-f",
"and-fg",
@ -1445,12 +1446,12 @@ output_pattern(int pattern, int n)
if (opt_positive || !opt_negative)
{
output_formula_checked(f, class_name[pattern - 1], n);
output_formula_checked(f, class_name[pattern - FIRST_CLASS], n);
}
if (opt_negative)
{
std::string tmp = "!";
tmp += class_name[pattern - 1];
tmp += class_name[pattern - FIRST_CLASS];
output_formula_checked(spot::formula::Not(f), tmp.c_str(), n);
}
}