spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
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:
Inheritance graph
Collaboration diagram for spot::translator:
Collaboration graph

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...
 

Protected Types

enum  {
  Any = 0, Small = 1, Deterministic = 2, Complete = 4,
  SBAcc = 8, Unambiguous = 16
}
 

Protected Member Functions

void setup_opt (const option_map *opt)
 
void build_simplifier (const bdd_dict_ptr &dict)
 
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)
 
twa_graph_ptr do_sba_simul (const twa_graph_ptr &input, int opt)
 
twa_graph_ptr do_degen (const twa_graph_ptr &input)
 
twa_graph_ptr do_scc_filter (const twa_graph_ptr &a, bool arg)
 
twa_graph_ptr do_scc_filter (const twa_graph_ptr &a)
 

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 det_scc_ = true
 
bool det_simul_ = true
 
bool det_stutter_ = true
 
int 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
 
bool state_based_ = false
 
bool wdba_minimize_ = true
 

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.

Member Function Documentation

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

Convert f into an automaton.

The formula f is simplified internally.

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::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.


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 Mon Feb 20 2017 07:08:26 for spot by doxygen 1.8.8