Commit 05e59a9e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

postproc: Add an option_map parameter

* src/tgbaalgos/postproc.cc: Add an option_map parameter, and use to get
extra options to pass to the degeneralization algorithm.
* src/tgbaalgos/postproc.hh: Adjust prototype, and store Boolean
variables for degeneralize() options.
* src/bin/ltl2tgba.cc: Add a -x option to fill the option map, and pass
it to the postprocessor.
* src/bin/man/ltl2tgba.x: Document the three degeneralization options.
parent 1b2f9fe5
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de // Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -39,6 +39,7 @@ ...@@ -39,6 +39,7 @@
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "misc/optionmap.hh"
const char argp_program_doc[] ="\ const char argp_program_doc[] ="\
Translate linear-time formulas (LTL/PSL) into Büchi automata.\n\n\ Translate linear-time formulas (LTL/PSL) into Büchi automata.\n\n\
...@@ -91,6 +92,8 @@ static const argp_option options[] = ...@@ -91,6 +92,8 @@ static const argp_option options[] =
"a single %", 0 }, "a single %", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 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 } { 0, 0, 0, 0, 0, 0 }
}; };
...@@ -105,6 +108,7 @@ const struct argp_child children[] = ...@@ -105,6 +108,7 @@ const struct argp_child children[] =
enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot; enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot;
bool utf8 = false; bool utf8 = false;
const char* stats = ""; const char* stats = "";
spot::option_map extra_options;
static int static int
parse_opt(int key, char* arg, struct argp_state*) parse_opt(int key, char* arg, struct argp_state*)
...@@ -126,6 +130,13 @@ 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) if (type != spot::postprocessor::Monitor)
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
break; 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: case OPT_DOT:
format = Dot; format = Dot;
break; break;
...@@ -258,7 +269,7 @@ main(int argc, char** argv) ...@@ -258,7 +269,7 @@ main(int argc, char** argv)
spot::ltl::ltl_simplifier simpl(simplifier_options()); spot::ltl::ltl_simplifier simpl(simplifier_options());
spot::postprocessor postproc; spot::postprocessor postproc(&extra_options);
postproc.set_pref(pref); postproc.set_pref(pref);
postproc.set_type(type); postproc.set_type(type);
postproc.set_level(level); postproc.set_level(level);
......
...@@ -2,3 +2,27 @@ ...@@ -2,3 +2,27 @@
ltl2tgba \- translate LTL/PSL formulas into Büchi automata ltl2tgba \- translate LTL/PSL formulas into Büchi automata
[DESCRIPTION] [DESCRIPTION]
.\" Add any additional description here .\" 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.
...@@ -24,6 +24,8 @@ ...@@ -24,6 +24,8 @@
#include "degen.hh" #include "degen.hh"
#include "stats.hh" #include "stats.hh"
#include "stripacc.hh" #include "stripacc.hh"
#include <cstdlib>
#include "misc/optionmap.hh"
namespace spot namespace spot
{ {
...@@ -41,6 +43,18 @@ namespace spot ...@@ -41,6 +43,18 @@ namespace spot
return st.states; 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) const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
{ {
if (type_ == TGBA && pref_ == Any && level_ == Low) if (type_ == TGBA && pref_ == Any && level_ == Low)
...@@ -100,7 +114,10 @@ namespace spot ...@@ -100,7 +114,10 @@ namespace spot
{ {
if (type_ == BA) if (type_ == BA)
{ {
const tgba* d = degeneralize(a); const tgba* d = degeneralize(a,
degen_reset,
degen_order,
degen_cache);
delete a; delete a;
a = d; a = d;
} }
...@@ -133,7 +150,10 @@ namespace spot ...@@ -133,7 +150,10 @@ namespace spot
// Degeneralize the result of the simulation if needed. // Degeneralize the result of the simulation if needed.
if (type_ == BA) if (type_ == BA)
{ {
const tgba* d = degeneralize(sim); const tgba* d = degeneralize(sim,
degen_reset,
degen_order,
degen_cache);
delete sim; delete sim;
sim = d; sim = d;
} }
......
...@@ -24,6 +24,8 @@ ...@@ -24,6 +24,8 @@
namespace spot namespace spot
{ {
class option_map;
/// \addtogroup tgba_reduction /// \addtogroup tgba_reduction
/// @{ /// @{
...@@ -45,9 +47,9 @@ namespace spot ...@@ -45,9 +47,9 @@ namespace spot
/// deterministic automata or small automata. If you don't care, /// deterministic automata or small automata. If you don't care,
/// less post processing will be done. /// less post processing will be done.
/// ///
/// The set_level() method let you set the optimization level. /// The set_level() method lets you set the optimization level.
/// Higher level enable more costly postprocessign. For instance /// A higher level enables more costly post-processings. For instance
/// pref=Small,level=High will try two different postprocessings /// pref=Small,level=High will try two different post-processings
/// (one with minimize_obligation(), and one with /// (one with minimize_obligation(), and one with
/// iterated_simulations()) an keep the smallest result. /// iterated_simulations()) an keep the smallest result.
/// pref=Small,level=Medium will only try the iterated_simulations() /// pref=Small,level=Medium will only try the iterated_simulations()
...@@ -57,10 +59,11 @@ namespace spot ...@@ -57,10 +59,11 @@ namespace spot
class postprocessor class postprocessor
{ {
public: public:
postprocessor() /// \brief Construct a postprocessor.
: type_(TGBA), pref_(Small), level_(High) ///
{ /// 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 }; enum output_type { TGBA, BA, Monitor };
void void
...@@ -76,7 +79,6 @@ namespace spot ...@@ -76,7 +79,6 @@ namespace spot
pref_ = pref; pref_ = pref;
} }
enum optimization_level { Low, Medium, High }; enum optimization_level { Low, Medium, High };
void void
set_level(optimization_level level) set_level(optimization_level level)
...@@ -91,6 +93,10 @@ namespace spot ...@@ -91,6 +93,10 @@ namespace spot
output_type type_; output_type type_;
output_pref pref_; output_pref pref_;
optimization_level level_; optimization_level level_;
// Fine-tuning degeneralization options.
bool degen_reset;
bool degen_order;
bool degen_cache;
}; };
/// @} /// @}
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment