spot  2.2.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members

Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More...

#include <spot/twaalgos/postproc.hh>

Inheritance diagram for spot::postprocessor:
Inheritance graph
Collaboration diagram for spot::postprocessor:
Collaboration graph

Public Types

enum  output_type { TGBA, BA, Monitor, Generic }
 
enum  {
  Any = 0, Small = 1, Deterministic = 2, Complete = 4,
  SBAcc = 8, Unambiguous = 16
}
 
enum  optimization_level { Low, Medium, High }
 
typedef int output_pref
 

Public Member Functions

 postprocessor (const option_map *opt=nullptr)
 Construct a postprocessor. More...
 
void set_type (output_type type)
 Select the desired output type. More...
 
void set_pref (output_pref pref)
 Select the desired characteristics of the output automaton. More...
 
void set_level (optimization_level level)
 Set the optimization level. More...
 
twa_graph_ptr run (twa_graph_ptr input, formula f=nullptr)
 Optimize an automaton. More...
 

Protected Member Functions

twa_graph_ptr do_simul (const twa_graph_ptr &input, int opt)
 
twa_graph_ptr do_sba_simul (const twa_graph_ptr &input, int opt)
 
twa_graph_ptr do_degen (const twa_graph_ptr &input)
 
twa_graph_ptr do_scc_filter (const twa_graph_ptr &a, bool arg)
 
twa_graph_ptr do_scc_filter (const twa_graph_ptr &a)
 

Protected Attributes

output_type type_ = TGBA
 
int pref_ = Small
 
optimization_level level_ = High
 
bool degen_reset_ = true
 
bool degen_order_ = false
 
int degen_cache_ = 1
 
bool degen_lskip_ = true
 
bool degen_lowinit_ = false
 
bool det_scc_ = true
 
bool det_simul_ = true
 
bool det_stutter_ = true
 
int simul_ = -1
 
int scc_filter_ = -1
 
int ba_simul_ = -1
 
bool tba_determinisation_ = false
 
int sat_minimize_ = 0
 
int sat_acc_ = 0
 
int sat_states_ = 0
 
bool state_based_ = false
 
bool wdba_minimize_ = true
 

Detailed Description

Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface.

This class is a shell around scc_filter(), minimize_obligation(), simulation(), iterated_simulations(), degeneralize(), to_generalized_buchi() and tgba_determinize(). These different algorithms will be combined depending on the various options set with set_type(), set_pref(), and set_level().

This helps hiding some of the logic required to combine these simplifications efficiently (e.g., there is no point calling degeneralize() or any simulation when minimize_obligation() succeeded.)

Use set_type() to select desired output type.

Use the set_pref() method to specify whether you favor deterministic automata or small automata. If you don't care, less post processing will be done.

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() when minimized_obligation failed to produce an automaton smaller than its input. pref=Small,level=Low will only run simulation().

Constructor & Destructor Documentation

spot::postprocessor::postprocessor ( const option_map opt = nullptr)

Construct a postprocessor.

The opt argument can be used to pass extra fine-tuning options used for debugging or benchmarking.

Member Function Documentation

twa_graph_ptr spot::postprocessor::run ( twa_graph_ptr  input,
formula  f = nullptr 
)

Optimize an automaton.

The returned automaton might be a new automaton, or an in-place modification of the input automaton.

void spot::postprocessor::set_level ( optimization_level  level)
inline

Set the optimization level.

At Low level, very few simplifications are performed on the automaton. Use this level if you need a result that matches the other constraints, but want it fast.

At High level, several simplifications are chained, but also the result of different algorithms may be compared to pick the best result. This might be slow.

At Medium level, several simplifications are chained, but only one such "pipeline" is used.

If set_level() is not called, the default output_type is High.

void spot::postprocessor::set_pref ( output_pref  pref)
inline

Select the desired characteristics of the output automaton.

Use Any if you do not care about any feature of the output automaton: less processing will be done.

Small and Deterministic are exclusive choices and indicate whether a smaller non-deterministic automaton should be preferred over a deterministic automaton. These are preferences. The Small option does not guarantee that the resulting automaton will be minimal. The Deterministic option may not manage to produce a deterministic automaton if the target acceptance set with set_type() is TGBA or BA (and even if such automaton exists).

Use

set_type(postprocessor::Generic);
set_pref(postprocessor::Deterministic);

if you absolutely want a deterministic automaton.

The above options can be combined with Complete and SBAcc, to request a complete automaton, and an automaton with state-based acceptance.

Note: the postprocessor::Unambiguous option is not actually supported by spot::postprocessor; it is only honored by spot::translator.

If set_pref() is not called, the default output_type is Small.

void spot::postprocessor::set_type ( output_type  type)
inline

Select the desired output type.

TGBA requires transition-based generalized Büchi acceptance while BA requests state-based Büchi acceptance. In both cases, automata with more complex acceptance conditions will be converted into these simpler acceptance. Monitor requests an automaton with the "all paths are accepting condition": this is less expressive, and may output automata that recognize a larger language than the input. Finally Generic remove all constraints about the acceptance condition. Using Generic can be needed to force the determinization of some automata (e.g., not all TGBA can be degeneralized, using Generic will allow parity acceptance to be used instead).

If set_type() is not called, the default output_type is TGBA.


The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Nov 21 2016 08:26:37 for spot by doxygen 1.8.8