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

Public Member Functions
	twa_word (const bdd_dict_ptr &dict) noexcept

	twa_word (const twa_run_ptr &run) noexcept

void	simplify ()
	Simplify a lasso-shaped word. More...

void	use_all_aps (bdd aps, bool positive=false)
	Use all atomic proposition. More...

bdd_dict_ptr	get_dict () const

twa_graph_ptr	as_automaton () const
	Convert the twa_word as an automaton. More...

bool	intersects (const_twa_ptr aut) const
	Check if a the twa_word intersect another automaton. More...

Public Attributes
seq_t	prefix

seq_t	cycle

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 represent lasso-shaped words using two list of BDDs: one list of the prefix, one list for the cycle.

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.

◆ intersects()

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

inline

Check if a the twa_word intersect 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 proposition.

Make sure each letters actually use 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.

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

spot/twaalgos/word.hh

Public Types

Public Member Functions

Public Attributes

Friends