spot::twa_word Struct Reference

An infinite word stored as a lasso. More...

#include <spot/twaalgos/word.hh>

Collaboration diagram for spot::twa_word:

Public Types
typedef std::list< bdd >	seq_t
	Type for a sequence of BDD conditions. More...

Public Member Functions
	twa_word (const bdd_dict_ptr &dict) noexcept
	Construct an empty word with the given BDD dictionary. More...
	twa_word (const twa_run_ptr &run) noexcept
	Construct a word from a twa_run. More...
void	simplify ()
	Simplify a lasso-shaped word. More...
void	use_all_aps (bdd aps, bool positive=false)
	Use all atomic propositions. More...
bdd_dict_ptr	get_dict () const
	Return the BDD dictionary. More...
twa_graph_ptr	as_automaton () const
	Convert the twa_word as an automaton. More...
bool	intersects (const_twa_ptr aut) const
	Check if the twa_word intersects another automaton. More...

Public Attributes
seq_t	prefix
	Finite prefix of the word. More...
seq_t	cycle
	Infinite repeating cycle of the word. More...

Friends
std::ostream &	operator<< (std::ostream &os, const twa_word &w)
	Print a twa_word. More...

Detailed Description

An infinite word stored as a lasso.

This is not exactly a word in the traditional sense because we use boolean formulas instead of letters. So technically a twa_word can represent a set of words.

This class only represents lasso-shaped words using two lists of BDDs: one list of the prefix, one list for the cycle.

Member Typedef Documentation

seq_t

typedef std::list<bdd> spot::twa_word::seq_t

Type for a sequence of BDD conditions.

Constructor & Destructor Documentation

twa_word() [1/2]

spot::twa_word::twa_word ( const bdd_dict_ptr &  dict )

noexcept

Construct an empty word with the given BDD dictionary.

twa_word() [2/2]

spot::twa_word::twa_word ( const twa_run_ptr &  run )

noexcept

Construct a word from a twa_run.

Member Function Documentation

as_automaton()

twa_graph_ptr spot::twa_word::as_automaton

(

)

const

Convert the twa_word as an automaton.

Convert the twa_word into a lasso-shaped automaton with "true" acceptance condition.

This is useful to evaluate a word on an automaton.

get_dict()

bdd_dict_ptr spot::twa_word::get_dict ( ) const

inline

Return the BDD dictionary.

intersects()

bool spot::twa_word::intersects ( const_twa_ptr  aut ) const

inline

Check if the twa_word intersects another automaton.

If the twa_word actually represent a word (i.e., if each Boolean formula that label its steps have a unique satisfying valuation), this is equivalent to a membership test.

simplify()

void spot::twa_word::simplify

(

)

Simplify a lasso-shaped word.

The simplified twa_word may represent a subset of the actual words represented by the original twa_word. The typical use-case is that a counterexample generated by an emptiness-check was converted into a twa_word (maybe accepting several words) and we want to present a simpler word as a counterexample to the user. ltlcross does that, for instance.

This method performs three reductions:

• If all the formulas on the cycle are compatible, the cycle will be reduced to a loop with the intersection of all formulas.
• If the end of the prefix can be folded into the cycle, remove those letters, and rotate the cycle accordingly.
• If any formula contains a disjunction, replace it by a single operand.

use_all_aps()

void spot::twa_word::use_all_aps	(	bdd	aps,
		bool	positive = false
	)

Use all atomic propositions.

Make sure each letter actually uses all variables in aps. By default, missing variables are introduced as negative, but setting positive to true will reverse that.

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  os, const twa_word &  w  )

friend

Print a twa_word.

Words are printed as

BF;BF;...;BF;cycle{BF;BF;...;BF}

where BF denote Boolean Formulas. The prefix part (before cycle{...}) can be empty. The cycle part (inside cycle{...}) may not be empty.

Member Data Documentation

cycle

seq_t spot::twa_word::cycle

Infinite repeating cycle of the word.

prefix

seq_t spot::twa_word::prefix

Finite prefix of the word.

---

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

• spot/twaalgos/word.hh