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

* src/tgbatest/ltl2tgba.cc (-rs): New option for reduce_size_striclty.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-05-02 20:23:58 +02:00
parent 42963b99c8
commit 2c3df109e1
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tgbatest/ltl2tgba.cc
View file

@ -178,7 +178,8 @@ syntax(char* prog)
<< " -r6 reduce formula using tau03+" << std::endl << " -r6 reduce formula using tau03+" << std::endl
<< " -r7 reduce formula using tau03+ and -r4" << std::endl << " -r7 reduce formula using tau03+ and -r4" << std::endl
<< " -rd display the reduced formula" << std::endl << " -rd display the reduced formula" << std::endl
<< std::endl << " -rL disable basic rewritings producing larger formulas"
<< std::endl << std::endl
<< "Automaton degeneralization (after translation):" << "Automaton degeneralization (after translation):"
<< std::endl << std::endl
@ -303,7 +304,8 @@ main(int argc, char** argv)
bool read_neverclaim = false; bool read_neverclaim = false;
bool scc_filter = false; bool scc_filter = false;
bool simpltl = false; bool simpltl = false;
spot::ltl::ltl_simplifier_options redopt(false, false, false, false, false); spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
false, false, false);
bool scc_filter_all = false; bool scc_filter_all = false;
bool symbolic_scc_pruning = false; bool symbolic_scc_pruning = false;
bool display_reduced_form = false; bool display_reduced_form = false;
@ -626,6 +628,12 @@ main(int argc, char** argv)
{ {
opt_minimize = true; opt_minimize = true;
} }
else if (!strcmp(argv[formula_index], "-rs"))
{
simpltl = true;
redopt.reduce_basics = true;
redopt.reduce_size_strictly = true;
}
else if (!strcmp(argv[formula_index], "-M")) else if (!strcmp(argv[formula_index], "-M"))
{ {
opt_monitor = true; opt_monitor = true;