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

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

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 Tue Apr 11 2017 13:40:04 for spot by doxygen 1.8.8