diff --git a/NEWS b/NEWS index a3080a561..973d96574 100644 --- a/NEWS +++ b/NEWS @@ -90,6 +90,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) diff --git a/bin/common_post.cc b/bin/common_post.cc index 5679f542c..b6796f1b8 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -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 }; diff --git a/bin/common_post.hh b/bin/common_post.hh index faaa1fa61..483114a81 100644 --- a/bin/common_post.hh +++ b/bin/common_post.hh @@ -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 #include -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; diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index bc7f07349..7b73e0668 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -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 } };