bin: Fix handling of LTL simplification options.

Enable LTL simplifications by default for ltl2tgba & ltl2tgta, and make
sure the ltl_simplifier_options are all false initially.  Before this
patch --low/-r1 had the same effect as --medium/-r2 with respect to LTL
simplification.

* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc (simplification_level): Set
to 3 by default.
* src/bin/common_r.cc: Disable all ltl_simplifier options initially.
This commit is contained in:
Alexandre Duret-Lutz 2013-03-02 15:15:47 +01:00
parent 543de07737
commit b6b6582b05
3 changed files with 9 additions and 5 deletions

View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -42,7 +42,7 @@ parse_r(const char* arg)
spot::ltl::ltl_simplifier_options
simplifier_options()
{
spot::ltl::ltl_simplifier_options options;
spot::ltl::ltl_simplifier_options options(false, false, false);
switch (simplification_level)
{
case 3:

View file

@ -247,6 +247,8 @@ main(int argc, char** argv)
const argp ap = { options, parse_opt, "[FORMULA...]",
argp_program_doc, children, 0, 0 };
simplification_level = 3;
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
exit(err);

View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -244,6 +244,8 @@ main(int argc, char** argv)
const argp ap = { options, parse_opt, "[FORMULA...]",
argp_program_doc, children, 0, 0 };
simplification_level = 3;
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
exit(err);