diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 266548e77..ac480cba6 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -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. // @@ -39,6 +39,7 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "tgba/bddprint.hh" +#include "misc/optionmap.hh" const char argp_program_doc[] ="\ Translate linear-time formulas (LTL/PSL) into Büchi automata.\n\n\ @@ -91,6 +92,8 @@ static const argp_option options[] = "a single %", 0 }, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { "extra-options", 'x', "OPTS", 0, + "fine-tuning options (see man page)", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -105,6 +108,7 @@ const struct argp_child children[] = enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot; bool utf8 = false; const char* stats = ""; +spot::option_map extra_options; static int parse_opt(int key, char* arg, struct argp_state*) @@ -126,6 +130,13 @@ parse_opt(int key, char* arg, struct argp_state*) if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; break; + case 'x': + { + const char* opt = extra_options.parse_options(arg); + if (opt) + error(2, 0, "failed to parse --options near '%s'", opt); + } + break; case OPT_DOT: format = Dot; break; @@ -258,7 +269,7 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier simpl(simplifier_options()); - spot::postprocessor postproc; + spot::postprocessor postproc(&extra_options); postproc.set_pref(pref); postproc.set_type(type); postproc.set_level(level); diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index f7f660e42..c99d70a4b 100644 --- a/src/bin/man/ltl2tgba.x +++ b/src/bin/man/ltl2tgba.x @@ -2,3 +2,27 @@ ltl2tgba \- translate LTL/PSL formulas into Büchi automata [DESCRIPTION] .\" Add any additional description here +[FINE-TUNING OPTIONS] + +The \fB\-\-extra\-options\fR argument is a comma-separated list of +\fIKEY\fR=\fIINT\fR assignments that are passed to the post-processing +routines (they may be passed to other algorithms in the future). +These options are mostly used for benchmarking and debugging +purpose. \fIKEY\fR (without any value) is a +shorthand for \fIKEY\fR=1, and !\fIKEY\fR is a shorthand for +\fIKEY\fR=0. + +Supported options are: +.TP +\fBdegen\-reset\fR +If non-zero (the default), the degeneralization algorithm will reset +its level any time it exits a non-accepting SCC. +.TP +\fBdegen\-lcache\fR +If non-zero (the default), whenever the degeneralization algorithm enters +an SCC on a state that has already been associated to a level elsewhere, +it should reuse that level. The "lcache" stands for "level cache". +.TP +\fBdegen\-order\fR +If non-zero, the degeneralization algorithm will compute one degeneralization +order for each SCC it processes. This is currently disabled by default. diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 7f99814f3..d1bacdc8e 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -24,6 +24,8 @@ #include "degen.hh" #include "stats.hh" #include "stripacc.hh" +#include +#include "misc/optionmap.hh" namespace spot { @@ -41,6 +43,18 @@ namespace spot return st.states; } + postprocessor::postprocessor(const option_map* opt) + : type_(TGBA), pref_(Small), level_(High), + degen_reset(true), degen_order(false), degen_cache(true) + { + if (opt) + { + degen_order = opt->get("degen-order", 0); + degen_reset = opt->get("degen-reset", 1); + degen_cache = opt->get("degen-lcache", 1); + } + } + const tgba* postprocessor::run(const tgba* a, const ltl::formula* f) { if (type_ == TGBA && pref_ == Any && level_ == Low) @@ -100,7 +114,10 @@ namespace spot { if (type_ == BA) { - const tgba* d = degeneralize(a); + const tgba* d = degeneralize(a, + degen_reset, + degen_order, + degen_cache); delete a; a = d; } @@ -133,7 +150,10 @@ namespace spot // Degeneralize the result of the simulation if needed. if (type_ == BA) { - const tgba* d = degeneralize(sim); + const tgba* d = degeneralize(sim, + degen_reset, + degen_order, + degen_cache); delete sim; sim = d; } diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index e7c55e022..bd8b7ac8a 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -24,6 +24,8 @@ namespace spot { + class option_map; + /// \addtogroup tgba_reduction /// @{ @@ -45,9 +47,9 @@ namespace spot /// deterministic automata or small automata. If you don't care, /// less post processing will be done. /// - /// The set_level() method let you set the optimization level. - /// Higher level enable more costly postprocessign. For instance - /// pref=Small,level=High will try two different postprocessings + /// The set_level() method lets you set the optimization level. + /// A higher level enables more costly post-processings. For instance + /// pref=Small,level=High will try two different post-processings /// (one with minimize_obligation(), and one with /// iterated_simulations()) an keep the smallest result. /// pref=Small,level=Medium will only try the iterated_simulations() @@ -57,10 +59,11 @@ namespace spot class postprocessor { public: - postprocessor() - : type_(TGBA), pref_(Small), level_(High) - { - } + /// \brief Construct a postprocessor. + /// + /// The \a opt argument can be used to pass extra fine-tuning + /// options used for debugging or benchmarking. + postprocessor(const option_map* opt = 0); enum output_type { TGBA, BA, Monitor }; void @@ -76,7 +79,6 @@ namespace spot pref_ = pref; } - enum optimization_level { Low, Medium, High }; void set_level(optimization_level level) @@ -91,6 +93,10 @@ namespace spot output_type type_; output_pref pref_; optimization_level level_; + // Fine-tuning degeneralization options. + bool degen_reset; + bool degen_order; + bool degen_cache; }; /// @} }