Translate an LTL formula into an optimized twa_graph. More...

#include <spot/twaalgos/translate.hh>

Inheritance diagram for spot::translator:

Collaboration diagram for spot::translator:

Public Types
enum	output_type
	Output type selection (inherited from postprocessor). More...

typedef int	output_pref
	Output preferences bitmask.

enum	optimization_level
	Optimization level selection. More...

Public Member Functions
	translator (tl_simplifier simpl, const option_map opt=nullptr)
	Construct a translator with a given simplifier.

	translator (const bdd_dict_ptr &dict, const option_map *opt=nullptr)
	Construct a translator with a given BDD dictionary.

	translator (const option_map *opt=nullptr)
	Construct a translator with optional options.

void	set_type (output_type type)
	Select the desired output type.

void	set_pref (output_pref pref)
	Select the desired output characteristics.

void	set_level (optimization_level level)
	Set the optimization 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 , Obligation = 64 }

Protected Member Functions
void	setup_opt (const option_map *opt)
	Initialize options from an option_map.

void	build_simplifier (const bdd_dict_ptr &dict)
	Build the LTL simplifier with the given dict.

twa_graph_ptr	run_aux (formula f)
	Run translation on a formula.

twa_graph_ptr	run_q (formula f)
	Run translation on a quantified formula.

twa_graph_ptr	finish_obligation_mtdswa (formula f, mtdswa_ptr mtdwa)
	Finalize the result of obligation_to_mtdswa().

twa_graph_ptr	translate_via_fm (formula f, bool unambiguous)
	Translate a formula via ltl_to_tgba_fm and branching post.

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
	Perform the simulation step.

twa_graph_ptr	do_sba_simul (const twa_graph_ptr &input, int opt) const
	Perform state-based acceptance simulation.

twa_graph_ptr	choose_degen (const twa_graph_ptr &input) const
	Choose degeneralization strategy.

twa_graph_ptr	do_degen (const twa_graph_ptr &input) const
	Perform the degeneralization step.

twa_graph_ptr	do_degen_tba (const twa_graph_ptr &input) const
	Perform TBA degeneralization.

twa_graph_ptr	do_scc_filter (const twa_graph_ptr &a, bool arg) const
	Perform the SCC filter step.

twa_graph_ptr	do_scc_filter (const twa_graph_ptr &a) const
	Perform the SCC filter step.

twa_graph_ptr	finalize (twa_graph_ptr tmp) const
	Finalize the automaton.

Static Protected Member Functions
static void	add_leading_x (twa_graph_ptr &aut, unsigned n)
	Prepend n leading X states before the initial state.

Protected Attributes
output_type	type_ = TGBA
	Output type option.

int	pref_ = Small
	Output preference option.

optimization_level	level_ = High
	Optimization level option.

bool	degen_reset_ = true
	Degeneralization reset option.

bool	degen_order_ = false
	Degeneralization order option.

int	degen_cache_ = 1
	Degeneralization cache option.

bool	degen_lskip_ = true
	Degeneralization level-skip option.

bool	degen_lowinit_ = false
	Degeneralization low-init option.

bool	degen_remscc_ = true
	Degeneralization remove-SCC option.

bool	det_scc_ = true
	Determinization use-SCC option.

int	det_simul_ = -1
	Determinization simulation option.

bool	det_stutter_ = true
	Determinization stutter option.

int	det_max_states_ = -1
	Determinization max states limit.

int	det_max_edges_ = -1
	Determinization max edges limit.

int	simul_ = -1
	Simulation option.

int	simul_method_ = -1
	Simulation method option.

int	simul_trans_pruning_ = 512
	Simulation transition pruning option.

int	dpa_simul_ = -1
	DPA simulation option.

int	dba_simul_ = -1
	DBA simulation option.

int	scc_filter_ = -1
	SCC filter option.

int	ba_simul_ = -1
	BA simulation option.

bool	tba_determinisation_ = false
	TBA determinization option.

int	sat_minimize_ = 0
	SAT minimization option.

int	sat_incr_steps_ = 0
	SAT incremental steps option.

bool	sat_langmap_ = false
	SAT language map option.

int	sat_acc_ = 0
	SAT acceptance sets option.

int	sat_states_ = 0
	SAT states option.

int	gen_reduce_parity_ = 1
	Generalized parity reduction option.

bool	state_based_ = false
	State-based acceptance option.

int	wdba_minimize_ = -1
	WDBA minimization option.

int	simul_max_ = 4096
	Simulation max states option.

int	merge_states_min_ = 128
	Merge states minimum option.

int	wdba_det_max_ = 4096
	WDBA determinization max states.

bool	acd_ = true
	ACD option.

bool	acd_was_used_
	Whether ACD was used.

int	rde_ = -1
	RDE option.

Detailed Description

Translate an LTL formula into an optimized twa_graph.

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

Member Typedef Documentation

◆ output_pref

typedef int spot::postprocessor::output_pref

Output preferences bitmask.

Member Enumeration Documentation

◆ optimization_level

enum spot::postprocessor::optimization_level

Optimization level selection.

◆ output_type

enum spot::postprocessor::output_type

Output type selection (inherited from postprocessor).

Constructor & Destructor Documentation

◆ translator() [1/3]

spot::translator::translator	(	tl_simplifier *	simpl,
		const option_map *	opt = `nullptr`
	)

inline

Construct a translator with a given simplifier.

◆ translator() [2/3]

spot::translator::translator	(	const bdd_dict_ptr &	dict,
		const option_map *	opt = `nullptr`
	)

inline

Construct a translator with a given BDD dictionary.

◆ translator() [3/3]

spot::translator::translator ( const option_map * opt = nullptr )

inline

Construct a translator with optional options.

References spot::make_bdd_dict().

Member Function Documentation

◆ add_leading_x()

static void spot::translator::add_leading_x	(	twa_graph_ptr &	aut,
		unsigned	n
	)

staticprotected

Prepend n leading X states before the initial state.

◆ build_simplifier()

void spot::translator::build_simplifier ( const bdd_dict_ptr & dict )

protected

Build the LTL simplifier with the given dict.

◆ choose_degen()

twa_graph_ptr spot::postprocessor::choose_degen ( const twa_graph_ptr & input ) const

protectedinherited

Choose degeneralization strategy.

◆ clear_caches()

void spot::translator::clear_caches ( )

Clear the LTL simplification caches.

◆ do_degen()

twa_graph_ptr spot::postprocessor::do_degen ( const twa_graph_ptr & input ) const

protectedinherited

Perform the degeneralization step.

◆ do_degen_tba()

twa_graph_ptr spot::postprocessor::do_degen_tba ( const twa_graph_ptr & input ) const

protectedinherited

Perform TBA degeneralization.

◆ do_sba_simul()

twa_graph_ptr spot::postprocessor::do_sba_simul	(	const twa_graph_ptr &	input,
		int	opt
	)		const

protectedinherited

Perform state-based acceptance simulation.

◆ do_scc_filter() [1/2]

twa_graph_ptr spot::postprocessor::do_scc_filter ( const twa_graph_ptr & a ) const

protectedinherited

Perform the SCC filter step.

◆ do_scc_filter() [2/2]

twa_graph_ptr spot::postprocessor::do_scc_filter	(	const twa_graph_ptr &	a,
		bool	arg
	)		const

protectedinherited

Perform the SCC filter step.

◆ do_simul()

twa_graph_ptr spot::postprocessor::do_simul	(	const twa_graph_ptr &	input,
		int	opt
	)		const

protectedinherited

Perform the simulation step.

◆ finalize()

twa_graph_ptr spot::postprocessor::finalize ( twa_graph_ptr tmp ) const

protectedinherited

Finalize the automaton.

◆ finish_obligation_mtdswa()

twa_graph_ptr spot::translator::finish_obligation_mtdswa	(	formula	f,
		mtdswa_ptr	mtdwa
	)

protected

Finalize the result of obligation_to_mtdswa().

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

◆ run_aux()

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

protected

Run translation on a formula.

◆ run_q()

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

protected

Run translation on a quantified formula.

◆ set_level() [1/2]

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_level() [2/2]

void spot::translator::set_level ( optimization_level level )

inline

Set the optimization level.

◆ set_pref()

void spot::translator::set_pref ( output_pref pref )

inline

Select the desired output characteristics.

◆ set_type() [1/2]

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 recognizes a larger language otherwise.

BA is a historical type that means Buchi and additionally sets state-based acceptance (this should normally be set with set_pref(SBAcc)).

If set_type() is not called, the default output_type is GeneralizedBuchi.

◆ set_type() [2/2]

void spot::translator::set_type ( output_type type )

inline

Select the desired output type.

◆ setup_opt()

void spot::translator::setup_opt ( const option_map * opt )

protected

Initialize options from an option_map.

◆ translate_via_fm()

twa_graph_ptr spot::translator::translate_via_fm	(	formula	f,
		bool	unambiguous
	)

protected

Translate a formula via ltl_to_tgba_fm and branching post.

Member Data Documentation

◆ acd_

bool spot::postprocessor::acd_ = true

protectedinherited

ACD option.

◆ acd_was_used_

bool spot::postprocessor::acd_was_used_

protectedinherited

Whether ACD was used.

◆ ba_simul_

int spot::postprocessor::ba_simul_ = -1

protectedinherited

BA simulation option.

◆ dba_simul_

int spot::postprocessor::dba_simul_ = -1

protectedinherited

DBA simulation option.

◆ degen_cache_

int spot::postprocessor::degen_cache_ = 1

protectedinherited

Degeneralization cache option.

◆ degen_lowinit_

bool spot::postprocessor::degen_lowinit_ = false

protectedinherited

Degeneralization low-init option.

◆ degen_lskip_

bool spot::postprocessor::degen_lskip_ = true

protectedinherited

Degeneralization level-skip option.

◆ degen_order_

bool spot::postprocessor::degen_order_ = false

protectedinherited

Degeneralization order option.

◆ degen_remscc_

bool spot::postprocessor::degen_remscc_ = true

protectedinherited

Degeneralization remove-SCC option.

◆ degen_reset_

bool spot::postprocessor::degen_reset_ = true

protectedinherited

Degeneralization reset option.

◆ det_max_edges_

int spot::postprocessor::det_max_edges_ = -1

protectedinherited

Determinization max edges limit.

◆ det_max_states_

int spot::postprocessor::det_max_states_ = -1

protectedinherited

Determinization max states limit.

◆ det_scc_

bool spot::postprocessor::det_scc_ = true

protectedinherited

Determinization use-SCC option.

◆ det_simul_

int spot::postprocessor::det_simul_ = -1

protectedinherited

Determinization simulation option.

◆ det_stutter_

bool spot::postprocessor::det_stutter_ = true

protectedinherited

Determinization stutter option.

◆ dpa_simul_

int spot::postprocessor::dpa_simul_ = -1

protectedinherited

DPA simulation option.

◆ gen_reduce_parity_

int spot::postprocessor::gen_reduce_parity_ = 1

protectedinherited

Generalized parity reduction option.

◆ level_

optimization_level spot::postprocessor::level_ = High

protectedinherited

Optimization level option.

◆ merge_states_min_

int spot::postprocessor::merge_states_min_ = 128

protectedinherited

Merge states minimum option.

◆ pref_

int spot::postprocessor::pref_ = Small

protectedinherited

Output preference option.

◆ rde_

int spot::postprocessor::rde_ = -1

protectedinherited

RDE option.

◆ sat_acc_

int spot::postprocessor::sat_acc_ = 0

protectedinherited

SAT acceptance sets option.

◆ sat_incr_steps_

int spot::postprocessor::sat_incr_steps_ = 0

protectedinherited

SAT incremental steps option.

◆ sat_langmap_

bool spot::postprocessor::sat_langmap_ = false

protectedinherited

SAT language map option.

◆ sat_minimize_

int spot::postprocessor::sat_minimize_ = 0

protectedinherited

SAT minimization option.

◆ sat_states_

int spot::postprocessor::sat_states_ = 0

protectedinherited

SAT states option.

◆ scc_filter_

int spot::postprocessor::scc_filter_ = -1

protectedinherited

SCC filter option.

◆ simul_

int spot::postprocessor::simul_ = -1

protectedinherited

Simulation option.

◆ simul_max_

int spot::postprocessor::simul_max_ = 4096

protectedinherited

Simulation max states option.

◆ simul_method_

int spot::postprocessor::simul_method_ = -1

protectedinherited

Simulation method option.

◆ simul_trans_pruning_

int spot::postprocessor::simul_trans_pruning_ = 512

protectedinherited

Simulation transition pruning option.

◆ state_based_

bool spot::postprocessor::state_based_ = false

protectedinherited

State-based acceptance option.

◆ tba_determinisation_

bool spot::postprocessor::tba_determinisation_ = false

protectedinherited

TBA determinization option.

◆ type_

output_type spot::postprocessor::type_ = TGBA

protectedinherited

Output type option.

◆ wdba_det_max_

int spot::postprocessor::wdba_det_max_ = 4096

protectedinherited

WDBA determinization max states.

◆ wdba_minimize_

int spot::postprocessor::wdba_minimize_ = -1

protectedinherited

WDBA minimization option.

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

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ output_pref

Member Enumeration Documentation

◆ optimization_level

◆ output_type

Constructor & Destructor Documentation

◆ translator() [1/3]

◆ translator() [2/3]

◆ translator() [3/3]

Member Function Documentation

◆ add_leading_x()

◆ build_simplifier()

◆ choose_degen()

◆ clear_caches()

◆ do_degen()

◆ do_degen_tba()

◆ do_sba_simul()

◆ do_scc_filter() [1/2]

◆ do_scc_filter() [2/2]

◆ do_simul()

◆ finalize()

◆ finish_obligation_mtdswa()

◆ run() [1/3]

◆ run() [2/3]

◆ run() [3/3]

◆ run_aux()

◆ run_q()

◆ set_level() [1/2]

◆ set_level() [2/2]

◆ set_pref()

◆ set_type() [1/2]

◆ set_type() [2/2]

◆ setup_opt()

◆ translate_via_fm()

Member Data Documentation

◆ acd_

◆ acd_was_used_

◆ ba_simul_

◆ dba_simul_

◆ degen_cache_

◆ degen_lowinit_

◆ degen_lskip_

◆ degen_order_

◆ degen_remscc_

◆ degen_reset_

◆ det_max_edges_

◆ det_max_states_

◆ det_scc_

◆ det_simul_

◆ det_stutter_

◆ dpa_simul_

◆ gen_reduce_parity_

◆ level_

◆ merge_states_min_

◆ pref_

◆ rde_

◆ sat_acc_

◆ sat_incr_steps_

◆ sat_langmap_

◆ sat_minimize_

◆ sat_states_

◆ scc_filter_

◆ simul_

◆ simul_max_

◆ simul_method_

◆ simul_trans_pruning_

◆ state_based_

◆ tba_determinisation_

◆ type_

◆ wdba_det_max_

◆ wdba_minimize_