spot 2.13.0.dev
|
Translate an LTL formula into an optimized spot::tgba. More...
#include <spot/twaalgos/translate.hh>
Public Types | |
enum | output_type |
typedef int | output_pref |
enum | optimization_level |
Public Member Functions | |
translator (tl_simplifier *simpl, const option_map *opt=nullptr) | |
translator (const bdd_dict_ptr &dict, const option_map *opt=nullptr) | |
translator (const option_map *opt=nullptr) | |
void | set_type (output_type type) |
void | set_pref (output_pref pref) |
void | set_level (optimization_level level) |
twa_graph_ptr | run (formula f) |
Convert f into an automaton. | |
twa_graph_ptr | run (formula *f) |
Convert f into an automaton, and update f. | |
void | clear_caches () |
Clear the LTL simplification caches. | |
Protected Types | |
enum | { Any = 0 , Small = 1 , Deterministic = 2 , Complete = 4 , SBAcc = 8 , Unambiguous = 16 , Colored = 32 } |
Protected Member Functions | |
void | setup_opt (const option_map *opt) |
void | build_simplifier (const bdd_dict_ptr &dict) |
twa_graph_ptr | run_aux (formula f) |
void | set_type (output_type type) |
Select the desired output type. | |
void | set_level (optimization_level level) |
Set the optimization level. | |
twa_graph_ptr | run (twa_graph_ptr input, formula f=nullptr) |
Optimize an automaton. | |
twa_graph_ptr | do_simul (const twa_graph_ptr &input, int opt) const |
twa_graph_ptr | do_sba_simul (const twa_graph_ptr &input, int opt) const |
twa_graph_ptr | choose_degen (const twa_graph_ptr &input) const |
twa_graph_ptr | do_degen (const twa_graph_ptr &input) const |
twa_graph_ptr | do_degen_tba (const twa_graph_ptr &input) const |
twa_graph_ptr | do_scc_filter (const twa_graph_ptr &a, bool arg) const |
twa_graph_ptr | do_scc_filter (const twa_graph_ptr &a) const |
twa_graph_ptr | finalize (twa_graph_ptr tmp) const |
Translate an LTL formula into an optimized spot::tgba.
This class implements a three-step translation:
Method set_type() may be used to specify the type of automaton produced (TGBA, BA, Monitor). The default is TGBA.
Method set_pref() may be used to specify whether small automata should be preferred over deterministic automata.
Method set_level() may be used to specify the optimization level.
The semantic of these three methods is inherited from the spot::postprocessor class, but the optimization level is additionally used to select which LTL simplifications to enable.
Most of the techniques used to produce TGBA or BA are described in "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).
Unambiguous automata are produced using a trick described in "LTL Model Checking of Interval Markov Chains" (Michael Benedikt and Rastislav Lenhardt and James Worrell, Proceedings of TACAS'13, pp. 32–46, LNCS 7795).
For reference about formula simplifications, see https://spot.lrde.epita.fr/tl.pdf (a copy of this file should be in the doc/tl/ subdirectory of the Spot sources).
For reference and documentation about the post-processing step, see the documentation of the spot::postprocessor class.
void spot::translator::clear_caches | ( | ) |
Clear the LTL simplification caches.
twa_graph_ptr spot::translator::run | ( | formula * | f | ) |
Convert f into an automaton, and update f.
The formula *f
is replaced by the simplified version.
twa_graph_ptr spot::translator::run | ( | formula | f | ) |
Convert f into an automaton.
The formula f is simplified internally.
|
inherited |
Optimize an automaton.
The returned automaton might be a new automaton, or an in-place modification of the input automaton.
|
inlineinherited |
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
.
|
inlineinherited |
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 recognize a larger language otherwise.
BA
is a historical type that means Buchi and additionally set state-based acceptance (this should normally be set with set_pref(SBAcc)
).
If set_type() is not called, the default output_type
is GeneralizedBuchi
.