spot
2.2.1
|
Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More...
#include <spot/twaalgos/postproc.hh>
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... | |
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().
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.
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.
|
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
.
|
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
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
.
|
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
.