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

ltl2tgta: remove options --ba, --tgba, and friends

Browse source 
* bin/common_post.cc, bin/common_post.hh: Add a "nooutput" variant of
the options.
* bin/ltl2tgta.cc: Use it.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-06 14:08:59 +02:00
parent d4a385e341
commit 70064d0b75
4 changed files with 27 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -12,6 +12,7 @@ New in spot 2.0.2a (Not yet released)
efficient at reducing automata (on the average).
* The generalized testing automata displayed by the on-line
translator were incorrect (those output by ltl2tgta were OK).
* ltl2tgta should not offer options --ba, --monitor, --tgba and such.
New in spot 2.0.2 (2016-06-17)

22
bin/common_post.cc
View file

@ -39,7 +39,7 @@ enum {
OPT_TGBA,
};
static const argp_option options[] =
static constexpr const argp_option options[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output automaton type:", 2 },
@ -72,6 +72,23 @@ static const argp_option options[] =
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
static constexpr const argp_option options_nooutput[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
{ "any", 'a', nullptr, 0, "no preference, do not bother making it small "
"or deterministic", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification level:", 21 },
{ "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
{ "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
{ "high", OPT_HIGH, nullptr, 0,
"all available optimizations (slow, default)", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
static const argp_option options_disabled[] =
{
/**************************************************/
@ -169,3 +186,6 @@ const struct argp post_argp = { options, parse_opt_post,
const struct argp post_argp_disabled = { options_disabled, parse_opt_post,
nullptr, nullptr, nullptr,
nullptr, nullptr };
const struct argp post_argp_nooutput = { options_nooutput, parse_opt_post,
nullptr, nullptr, nullptr,
nullptr, nullptr };

7
bin/common_post.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -23,8 +23,9 @@
#include <spot/twaalgos/postproc.hh>
#include <argp.h>
extern const struct argp post_argp; // postprocessing enabled
extern const struct argp post_argp; // postprocessing enabled
extern const struct argp post_argp_disabled; // postprocessing disabled
extern const struct argp post_argp_nooutput; // no output option
extern spot::postprocessor::output_type type;
extern spot::postprocessor::output_pref pref;

2
bin/ltl2tgta.cc
View file

@ -90,7 +90,7 @@ static const argp_option options[] =
const struct argp_child children[] =
{
{ &finput_argp, 0, nullptr, 1 },
{ &post_argp, 0, nullptr, 20 },
{ &post_argp_nooutput, 0, nullptr, 20 },
{ &misc_argp, 0, nullptr, -1 },
{ nullptr, 0, nullptr, 0 }
};