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

Correctly handle ltl2tgba's option -rL.

Browse source 
* src/tgbatest/ltl2tgba.cc: Fix mismatch between the help text,
documenting -rL, and the handling code, expecting -rs.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-19 00:11:13 +02:00
parent 8c454f9ddf
commit babc024097
2 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -5,6 +5,7 @@ New in spot 0.9a:
for "and" and "or", mistaking And/Or with AndRat/OrRat. for "and" and "or", mistaking And/Or with AndRat/OrRat.
- The translation of !{r} was incorrect when this subformula - The translation of !{r} was incorrect when this subformula
was recurring (e.g. in G!{r}) and r had loops. was recurring (e.g. in G!{r}) and r had loops.
- Correctly recognize ltl2tgba's option -rL.
New in spot 0.9 (2012-05-09): New in spot 0.9 (2012-05-09):

10
src/tgbatest/ltl2tgba.cc
View file

@ -623,16 +623,16 @@ main(int argc, char** argv)
{ {
reduction_dir_sim = true; reduction_dir_sim = true;
} }
else if (!strcmp(argv[formula_index], "-Rm")) else if (!strcmp(argv[formula_index], "-rL"))
{
opt_minimize = true;
}
else if (!strcmp(argv[formula_index], "-rs"))
{ {
simpltl = true; simpltl = true;
redopt.reduce_basics = true; redopt.reduce_basics = true;
redopt.reduce_size_strictly = true; redopt.reduce_size_strictly = true;
} }
else if (!strcmp(argv[formula_index], "-Rm"))
{
opt_minimize = true;
}
else if (!strcmp(argv[formula_index], "-M")) else if (!strcmp(argv[formula_index], "-M"))
{ {
opt_monitor = true; opt_monitor = true;