spot  2.11.2
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. More...
twa_graph_ptr run (formula *f)
 Convert f into an automaton, and update f. More...
void clear_caches ()
 Clear the LTL simplification caches. More...

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)
twa_graph_ptr run (twa_graph_ptr input, formula f=nullptr)
 Optimize an automaton. More...
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_ = false
bool acd_was_used_

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 prefered 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 (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 

Optimize an automaton.

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

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