spot  2.10.6
Classes | Functions
Translating LTL formulas into TωA

Classes

class  spot::translator
 Translate an LTL formula into an optimized spot::tgba. More...
 

Functions

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)
 Build a spot::twa_graph_ptr from an LTL or PSL formula. More...
 

Detailed Description

Function Documentation

◆ 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 of 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 of 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 the LICS'18 paper of J. Esparza, J. Křetínský, and S. Sickert. This version will work if Φ represent 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 [51] .

Parameters
fThe formula to translate into an automaton.
dictThe spot::bdd_dict the constructed automata should use.
refined_rulesIf 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 
)

#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 [12] , but it has been improved in many ways [15] .

Parameters
fThe formula to translate into an automaton.
dictThe spot::bdd_dict the constructed automata should use.
expropWhen 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 worse, equal).
symb_mergeWhen false, states with the same symbolic representation (these are equivalent formulae) will not be merged.
branching_postponementWhen set, several transitions leaving from the same state with the same label (i.e., condition + acceptance conditions) will be merged. [45]
fair_loop_approxWhen set, a really simple characterization of unstable state is used to suppress all acceptance conditions from incoming transitions.
unobsWhen 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.
simplifierIf this parameter is set, the LTL formulae 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 [52] .
unambiguousWhen true, unambigous TGBA will be produced using the trick described in [3] .
aborterWhen given, aborts the construction whenever the constructed automaton would become larger than specified by the output_aborter.
Returns
A spot::twa_graph that recognizes the language of f.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1