Translating LTL formulas into TωA

Classes
struct	spot::fm_edge
	A single successor edge from a formula-state. More...
struct	spot::fm_simple_edge
	A simplified successor edge without condition. More...
class	spot::ltl_to_tgba_fm_otf
	On-the-fly LTL→TGBA explorer. More...
class	spot::translator
	Translate an LTL formula into an optimized twa_graph. More...

Typedefs
typedef std::vector< std::pair< bool, bdd > >	spot::quantifier_list
	List of quantifiers: each pair holds a Boolean (true = universal, false = existential) and a BDD over the quantified propositions. More...

Functions
twa_graph_ptr	spot::compsusp (formula f, const bdd_dict_ptr &dict, bool no_wdba=false, bool no_simulation=false, bool early_susp=false, bool no_susp_product=false, bool wdba_smaller=false, bool oblig=false)
	Compositional translation algorithm with resetable suspension. More...
twa_graph_ptr	spot::gf_guarantee_to_ba_maybe (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
	Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
twa_graph_ptr	spot::gf_guarantee_to_ba (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
	Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
twa_graph_ptr	spot::fg_safety_to_dca_maybe (formula fg, const bdd_dict_ptr &dict, bool state_based)
	Convert FG(φ) into a DCA if φ is a safety property. More...
twa_graph_ptr	spot::fg_safety_to_dca (formula fg, const bdd_dict_ptr &dict, bool state_based=false)
	Convert FG(φ) into a DCA if φ is a safety property. More...
taa_tgba_formula_ptr	spot::ltl_to_taa (formula f, const bdd_dict_ptr &dict, bool refined_rules=false)
	Build a spot::taa* from an LTL formula. More...
twa_graph_ptr	spot::ltl_to_tgba_fm (formula f, const bdd_dict_ptr &dict, bool exprop=false, bool symb_merge=true, bool branching_postponement=false, bool fair_loop_approx=false, const atomic_prop_set *unobs=nullptr, tl_simplifier *simplifier=nullptr, bool unambiguous=false, const output_aborter *aborter=nullptr, bool label_with_ltl=false, bool force_obligation=false)
	Build a spot::twa_graph_ptr from an LTL or PSL formula. More...
std::pair< quantifier_list, formula >	spot::extract_quantifier_list (formula f, bdd_dict_ptr dict, void *for_me)
	Convert quantified LTL to unquantified LTL + quantifier_list. More...
template<typename T >
std::pair< quantifier_list, formula >	spot::extract_quantifier_list (formula f, bdd_dict_ptr dict, std::shared_ptr< T > for_me)
	Convert quantified LTL to unquantified LTL + quantifier_list. More...

Detailed Description

Typedef Documentation

quantifier_list

typedef std::vector<std::pair<bool, bdd> > spot::quantifier_list

#include <spot/twaalgos/quantify.hh>

List of quantifiers: each pair holds a Boolean (true = universal, false = existential) and a BDD over the quantified propositions.

Function Documentation

compsusp()

twa_graph_ptr spot::compsusp	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	no_wdba = false,
		bool	no_simulation = false,
		bool	early_susp = false,
		bool	no_susp_product = false,
		bool	wdba_smaller = false,
		bool	oblig = false
	)

#include <spot/twaalgos/compsusp.hh>

Compositional translation algorithm with resetable suspension.

Described in "Compositional Approach to Suspension and Other Improvements to LTL Translation", Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček (SPIN'13).

If no_wdba or no_simulation is true, the corresponding operation is not performed on the skeleton automaton. If early_susp is true, then composition starts on the transition that enters the accepting SCC, not just in the SCC itself. If no_susp_product is true, then the composition is not performed and the skeleton automaton is returned for debugging. If wdba_smaller is true, then the WDBA-minimization of the skeleton is used only if it produces a smaller automaton.

Finally the oblig flag is a work in progress and should not be set to true.

This interface is subject to change, and clients aiming for long-term stability should better use the services of the spot::translator class instead.

extract_quantifier_list() [1/2]

template<typename T >

std::pair<quantifier_list, formula> spot::extract_quantifier_list	(	formula	f,
		bdd_dict_ptr	dict,
		std::shared_ptr< T >	for_me
	)

#include <spot/twaalgos/quantify.hh>

Convert quantified LTL to unquantified LTL + quantifier_list.

If the input is ∀a,b:∃c,d:φ, this returns ([(true, a&b), (false, c&d)], φ) where φ is an unquitified LTL, a&b and c&d are BDDs, and the true/false indicate universal/existential quantifications.

The atomic propositions used in BDD variables will be registered into dict for for_me.

References spot::extract_quantifier_list().

extract_quantifier_list() [2/2]

std::pair<quantifier_list, formula> spot::extract_quantifier_list	(	formula	f,
		bdd_dict_ptr	dict,
		void *	for_me
	)

#include <spot/twaalgos/quantify.hh>

Convert quantified LTL to unquantified LTL + quantifier_list.

If the input is ∀a,b:∃c,d:φ, this returns ([(true, a&b), (false, c&d)], φ) where φ is an unquitified LTL, a&b and c&d are BDDs, and the true/false indicate universal/existential quantifications.

The atomic propositions used in BDD variables will be registered into dict for for_me.

Referenced by spot::extract_quantifier_list().

fg_safety_to_dca()

twa_graph_ptr spot::fg_safety_to_dca	(	formula	fg,
		const bdd_dict_ptr &	dict,
		bool	state_based = false
	)

#include <spot/twaalgos/gfguarantee.hh>

Convert FG(φ) into a DCA if φ is a safety property.

This is similar to fg_safety_to_dba_maybe() except it raises an exception if the input formula is not of the supported form.

fg_safety_to_dca_maybe()

twa_graph_ptr spot::fg_safety_to_dca_maybe	(	formula	fg,
		const bdd_dict_ptr &	dict,
		bool	state_based
	)

#include <spot/twaalgos/gfguarantee.hh>

Convert FG(φ) into a DCA if φ is a safety property.

This is the dual of gf_guarantee_to_ba_maybe(). See that function for details.

Return nullptr if the input formula is not of the supported form.

gf_guarantee_to_ba()

twa_graph_ptr spot::gf_guarantee_to_ba	(	formula	gf,
		const bdd_dict_ptr &	dict,
		bool	deterministic = true,
		bool	state_based = false
	)

#include <spot/twaalgos/gfguarantee.hh>

Convert GF(φ) into a (D)BA if φ is a guarantee property.

This is similar to gf_guarantee_to_ba_maybe() except it raises an exception if the input formula is not of the supported form.

gf_guarantee_to_ba_maybe()

twa_graph_ptr spot::gf_guarantee_to_ba_maybe	(	formula	gf,
		const bdd_dict_ptr &	dict,
		bool	deterministic = true,
		bool	state_based = false
	)

#include <spot/twaalgos/gfguarantee.hh>

Convert GF(φ) into a (D)BA if φ is a guarantee property.

If the formula gf has the form GΦ where Φ matches either F(φ) or F(φ₁)&F(φ₂)&...&F(φₙ), we translate Φ into A_Φ and attempt to minimize it to a WDBA W_Φ. If the resulting automaton is terminal, we then call g_f_terminal_inplace(W_Φ). If deterministic is not set, we keep the minimized automaton only if g_f_terminal_inplace(A_Φ) is larger.

Return nullptr if the input formula is not of the supported form.

This construction generalizes a construction in a LICS'18 paper by Esparza et al. [esparza.18.lics] This version will work if Φ represents a safety property, even if it is not a syntactic safety. When building deterministic transition-based automata, it will also try to remove useless trivial components at the beginning of wdba(A_Φ).

ltl_to_taa()

taa_tgba_formula_ptr spot::ltl_to_taa	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	refined_rules = false
	)

#include <spot/twaalgos/ltl2taa.hh>

Build a spot::taa* from an LTL formula.

This is based on [tauriainen.06.tr] .

Parameters

f	The formula to translate into an automaton.
dict	The spot::bdd_dict the constructed automaton should use.
refined_rules	If this parameter is set, refined rules are used.

Returns

A spot::taa that recognizes the language of f.

ltl_to_tgba_fm()

twa_graph_ptr spot::ltl_to_tgba_fm	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	exprop = false,
		bool	symb_merge = true,
		bool	branching_postponement = false,
		bool	fair_loop_approx = false,
		const atomic_prop_set *	unobs = nullptr,
		tl_simplifier *	simplifier = nullptr,
		bool	unambiguous = false,
		const output_aborter *	aborter = nullptr,
		bool	label_with_ltl = false,
		bool	force_obligation = false
	)

#include <spot/twaalgos/ltl2tgba_fm.hh>

Build a spot::twa_graph_ptr from an LTL or PSL formula.

This originally derived from an algorithm by Couvreur [couvreur.99.fm] , but it has been improved in many ways [duret.14.ijccbs] .

Parameters

f	The formula to translate into an automaton.
dict	The spot::bdd_dict the constructed automaton should use.
exprop	When set, the algorithm will consider all properties combinations possible on each state, in an attempt to reduce the non-determinism. The automaton will have the same size as without this option, but because the transitions will be more deterministic, the product automaton will be smaller (or, at worst, equal).
symb_merge	When false, states with the same symbolic representation (these are equivalent formulas) will not be merged.
branching_postponement	When set, several transitions leaving from the same state with the same label (i.e., condition + acceptance conditions) will be merged. [sebastiani.03.charme]
fair_loop_approx	When set, a really simple characterization of unstable state is used to suppress all acceptance conditions from incoming transitions.
unobs	When non-zero, the atomic propositions in the LTL formula are interpreted as events that exclude each other. The events in the formula are observable events, and unobs can be filled with additional unobservable events.
simplifier	If this parameter is set, the LTL formulas representing each state of the automaton will be simplified before computing the successor. simpl should be configured for the type of reduction you want, see spot::tl_simplifier. This idea is taken from [thirioux.02.fmics] .
unambiguous	When true, unambiguous TGBA will be produced using the trick described in [benedikt.13.tacas] .
aborter	When given, aborts the construction whenever the constructed automaton would become larger than specified by the output_aborter.
label_with_ltl	keep one LTL formula equivalent to the language recognized by each state, and use that to name each state.
force_obligation	when true, force the result to satisfy the obligation property, as if the formula is already an obligation.

Returns

A spot::twa_graph that recognizes the language of f.