spot 2.13.0.dev
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members

Translate an LTL formula into an optimized spot::tgba. More...

#include <spot/twaalgos/translate.hh>

Inheritance diagram for spot::translator:
Collaboration diagram for spot::translator:

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
 

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 degen_remscc_ = true
 
bool det_scc_ = true
 
int det_simul_ = -1
 
bool det_stutter_ = true
 
int det_max_states_ = -1
 
int det_max_edges_ = -1
 
int simul_ = -1
 
int simul_method_ = -1
 
int simul_trans_pruning_ = 512
 
int dpa_simul_ = -1
 
int dba_simul_ = -1
 
int scc_filter_ = -1
 
int ba_simul_ = -1
 
bool tba_determinisation_ = false
 
int sat_minimize_ = 0
 
int sat_incr_steps_ = 0
 
bool sat_langmap_ = false
 
int sat_acc_ = 0
 
int sat_states_ = 0
 
int gen_reduce_parity_ = 1
 
bool state_based_ = false
 
int wdba_minimize_ = -1
 
int simul_max_ = 4096
 
int merge_states_min_ = 128
 
int wdba_det_max_ = 4096
 
bool acd_ = true
 
bool acd_was_used_
 
int rde_ = -1
 

Detailed Description

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.

Member Function Documentation

◆ clear_caches()

void spot::translator::clear_caches ( )

Clear the LTL simplification caches.

◆ run() [1/3]

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.

◆ run() [2/3]

twa_graph_ptr spot::translator::run ( formula  f)

Convert f into an automaton.

The formula f is simplified internally.

◆ run() [3/3]

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

Optimize an automaton.

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

◆ set_level()

void spot::postprocessor::set_level ( optimization_level  level)
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.

◆ set_type()

void spot::postprocessor::set_type ( output_type  type)
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.


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 Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.8