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_ = 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:

syntactic simplification of the formula
translation of the formula into TGBA
postprocessing of the resulting TGBA to minimize it, or turn it into the required form.

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.

The documentation for this class was generated from the following file:

spot/twaalgos/translate.hh

Public Types

Public Member Functions

Protected Types

Protected Member Functions