|
| enum | output_type {
TGBA = 0
, GeneralizedBuchi = 0
, BA = 1
, Monitor = 2
,
Generic = 3
, Parity = 4
, ParityMin = Parity | 8
, ParityMax = Parity | 16
,
ParityOdd = Parity | 32
, ParityEven = Parity | 64
, ParityMinOdd = ParityMin | ParityOdd
, ParityMaxOdd = ParityMax | ParityOdd
,
ParityMinEven = ParityMin | ParityEven
, ParityMaxEven = ParityMax | ParityEven
, CoBuchi = 128
, Buchi = 256
,
Finite = 512
} |
| | Output type selection. More...
|
| |
| enum | {
Any = 0
, Small = 1
, Deterministic = 2
, Complete = 4
,
SBAcc = 8
, Unambiguous = 16
, Colored = 32
, Obligation = 64
} |
| |
| enum | optimization_level { Low
, Medium
, High
} |
| | Optimization level selection. More...
|
| |
| typedef int | output_pref |
| | Output preferences bitmask.
|
| |
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(), tgba_determinize(), and other algorithms. 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()) and 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().
The handling of alternating automata should change in the future, but currently Generic, Low, Any is the only configuration where alternation is preserved. In any other configuration, remove_alternation() will be called.
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.
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
void set_pref(output_pref pref)
Select the desired characteristics of the output automaton.
Definition postproc.hh:207
void set_type(output_type type)
Select the desired output type.
Definition postproc.hh:140
if you absolutely want a deterministic automaton. The resulting deterministic automaton may have generalized Büchi acceptance or parity acceptance.
The above options can be combined with Complete and SBAcc, to request a complete automaton, and an automaton with state-based acceptance. Automata with parity acceptance may also be required to be Colored, ensuring that each transition (or state) belongs to exactly one acceptance set.
Note 1: the Unambiguous option is not actually supported by spot::postprocessor; it is only honored by spot::translator.
Note 2: for historical reasons, option SBAcc is implied when the output type is set to BA.
Note 3: while setting the output type to Monitor requests automata with t as acceptance condition, combining Monitor with Complete may produce Büchi automata in case a sink state (which should be rejecting) is added.
Note 4: Obligation is not really an output preference, but rather an indication that the input can be assumed to be an Obligation, bypassing some unnecessary checks. This is set automatically by the translator when translating LTLf formulas, so it is probably best considered as an implementation detail.
If set_pref() is not called, the default output_type is Small.
Select the desired output type.
GeneralizedBuchi requires generalized Büchi acceptance while Buchi requests Büchi acceptance. In both cases, automata with more complex acceptance conditions will be converted into these simpler acceptance. For references about the algorithms used behind these options, see section 5 of "LTL translation improvements in Spot 1.0" (Alexandre Duret-Lutz. Int. J. on Critical Computer-Based Systems, 5(1/2), pp. 31–54, March 2014).
Monitor requests an automaton where all paths are accepting: this is less expressive than Büchi automata, and may output automata that recognize a larger language than the input (the output recognizes the smallest safety property containing the input). The algorithm used to obtain monitors comes from "Efficient monitoring of ω-languages" (Marcelo d’Amorim and Grigoire Roşu, Proceedings of CAV’05, LNCS 3576) but is better described in "Optimized Temporal Monitors for
SystemC" (Deian Tabakov and Moshe Y. Vardi, Proceedings of RV’10, LNCS 6418).
Generic removes all constraints about the acceptance condition. Using Generic (or Parity below) 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).
Parity and its variants request the acceptance condition to be of some parity type. Note that the determinization algorithm used by Spot produces "parity min odd" acceptance, but other parity types can be obtained from there by minor adjustments.
CoBuchi requests a Co-Büchi automaton equivalent to the input, when possible, or a Co-Büchi automaton that recognizes a larger language otherwise.
BA is a historical type that means Buchi and additionally sets state-based acceptance (this should normally be set with set_pref(SBAcc)).
If set_type() is not called, the default output_type is GeneralizedBuchi.
