spot  2.3.4
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Public Types | Public Member Functions | Public Attributes | Friends | List of all members
spot::twa_word Struct Referencefinal

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

#include <spot/twaalgos/word.hh>

Collaboration diagram for spot::twa_word:
Collaboration graph

Public Types

typedef std::list< bdd > seq_t
 

Public Member Functions

 twa_word (const bdd_dict_ptr &dict)
 
 twa_word (const twa_run_ptr &run)
 
void simplify ()
 Simplify a lasso-shapped word. More...
 
bdd_dict_ptr get_dict () const
 
twa_graph_ptr as_automaton () const
 Convert the twa_word as an 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

twa_graph_ptr spot::twa_word::as_automaton ( ) const

Convert the twa_word as an automaton.

This is useful to evaluate a word on an automaton.

void spot::twa_word::simplify ( )

Simplify a lasso-shapped 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.

Friends And Related Function Documentation

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:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu May 11 2017 08:27:33 for spot by doxygen 1.8.8