spot 2.16
Loading...
Searching...
No Matches
Public Member Functions | List of all members
spot::lasso_enumerator Class Referencefinal

Lazily enumerate lasso-shaped accepted runs/words of bounded size. More...

#include <spot/twaalgos/lasso.hh>

Collaboration diagram for spot::lasso_enumerator:

Public Member Functions

 lasso_enumerator (const const_twa_graph_ptr &aut, unsigned min_stem, unsigned max_stem, unsigned min_cycle, unsigned max_cycle)
 Construct a lasso enumerator.
 
 lasso_enumerator (const lasso_enumerator &)=delete
 
lasso_enumeratoroperator= (const lasso_enumerator &)=delete
 
twa_run_ptr next_run ()
 Return the next accepted run, or nullptr when exhausted.
 
twa_word_ptr next_word ()
 Return the next accepted word, or nullptr when exhausted.
 

Detailed Description

Lazily enumerate lasso-shaped accepted runs/words of bounded size.

A lasso consists of a finite stem path followed by an infinite cycle. Given bounds on the stem and cycle lengths, this class enumerates all accepted lasso-shaped runs in order of increasing total length (stem + cycle), breaking ties by shorter stem first.

All acceptance conditions are supported.

If the automaton is non-deterministic, the enumeration does not remove duplicate words or runs.

Constructor & Destructor Documentation

◆ lasso_enumerator()

spot::lasso_enumerator::lasso_enumerator ( const const_twa_graph_ptr aut,
unsigned  min_stem,
unsigned  max_stem,
unsigned  min_cycle,
unsigned  max_cycle 
)

Construct a lasso enumerator.

Parameters
autautomaton with any acceptance condition
min_stemminimum stem length (≥0)
max_stemmaximum stem length (≥min_stem; UINT_MAX = unbounded)
min_cycleminimum cycle length (≥1)
max_cyclemaximum cycle length (≥min_cycle; UINT_MAX = unbounded)
Exceptions
std::invalid_argumentif the bounds are inconsistent.

Member Function Documentation

◆ next_run()

twa_run_ptr spot::lasso_enumerator::next_run ( )

Return the next accepted run, or nullptr when exhausted.

◆ next_word()

twa_word_ptr spot::lasso_enumerator::next_word ( )

Return the next accepted word, or nullptr when exhausted.


The documentation for this class 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 Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.8