An accepted run, for a twa. More...

#include <spot/twaalgos/emptiness.hh>

Collaboration diagram for spot::twa_run:

Classes
struct	step
	A single step in a TωA run, pairing a state with an edge label and acceptance marks. More...

Public Types
typedef std::list< step >	steps
	Ordered sequence of run steps.

Public Member Functions
	twa_run (const const_twa_ptr &aut) noexcept
	Construct an empty run for the given automaton.

	twa_run (const twa_run &run)
	Copy constructor.

twa_run &	operator= (const twa_run &run)
	Copy-assignment operator.

void	ensure_non_empty_cycle (const char *where) const
	Raise an exception if the cycle is empty.

twa_run_ptr	reduce () const
	Reduce an accepting run.

twa_run_ptr	project (const const_twa_ptr &other, bool right=false)
	Project an accepting run.

bool	replay (std::ostream &os, bool debug=false) const
	Replay a run.

void	highlight (unsigned color)
	Highlight the accepting run on the automaton.

twa_graph_ptr	as_twa (bool preserve_names=false) const
	Convert the run into a lasso-shaped automaton.

Public Attributes
steps	prefix
	The prefix part of the run.

steps	cycle
	The cycle part of the run.

const_twa_ptr	aut
	The automaton this run is associated with.

Friends
std::ostream &	operator<< (std::ostream &os, const twa_run &run)
	Display a twa_run.

Detailed Description

An accepted run, for a twa.

Member Typedef Documentation

◆ steps

typedef std::list<step> spot::twa_run::steps

Ordered sequence of run steps.

Constructor & Destructor Documentation

◆ twa_run() [1/2]

spot::twa_run::twa_run ( const const_twa_ptr & aut )

inlinenoexcept

Construct an empty run for the given automaton.

◆ twa_run() [2/2]

spot::twa_run::twa_run ( const twa_run & run )

Copy constructor.

Member Function Documentation

◆ as_twa()

twa_graph_ptr spot::twa_run::as_twa ( bool preserve_names = false ) const

Convert the run into a lasso-shaped automaton.

This preserves the original acceptance condition.

If preserve_names is set, the created states are named using the format_state() result from the original state.

◆ ensure_non_empty_cycle()

void spot::twa_run::ensure_non_empty_cycle ( const char * where ) const

Raise an exception if the cycle is empty.

It is OK for a twa_run to have an empty cycle while the run is being filled by some procedure. But after that, we expect cycles to be non-empty. Calling this function will raise an std::runtime_error if the cycle is empty, giving where (usually the name of the calling function) as context.

◆ highlight()

void spot::twa_run::highlight ( unsigned color )

Highlight the accepting run on the automaton.

Note that this works only if the automaton is a twa_graph_ptr.

◆ operator=()

twa_run & spot::twa_run::operator= ( const twa_run & run )

Copy-assignment operator.

◆ project()

twa_run_ptr spot::twa_run::project	(	const const_twa_ptr &	other,
		bool	right = `false`
	)

Project an accepting run.

This only works if the automaton associated to this run has been created with otf_product() or product(), and other is one of the two operands of the product.

Use the right Boolean to specify whether other was a left or right operand.

◆ reduce()

twa_run_ptr spot::twa_run::reduce ( ) const

Reduce an accepting run.

Return a run which is still accepting for aut, but is no longer than this one.

This is done by trying to find a fragment of the accepting cycle that is accepting, and trying to close a cycle around this fragment with fewer edges than in the original cycle. (This step works best in Fin-less automata.) And then trying to find a shorter prefix leading to any state of the cycle.

An std::runtime_error is thrown if the run to reduce is not accepting.

◆ replay()

bool spot::twa_run::replay	(	std::ostream &	os,
		bool	debug = `false`
	)		const

Replay a run.

This is similar to os << run;, except that the run is actually replayed on the automaton while it is printed. The output will stop if the run cannot be completed.

Parameters

os	the stream on which the replay should be traced
debug	if set the output will be more verbose and extra debugging information will be output on failure

Returns: true iff the run could be completed

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<<	(	std::ostream &	os,
		const twa_run &	run
	)

friend

Display a twa_run.

Output the prefix and cycle parts of the twa_run run on os.

The automaton object (stored by run) is used only to format the states, and to know how to print the BDDs describing the conditions and acceptance conditions of the run; it is not used to replay the run. In other words this function will work even if the twa_run you are trying to print appears to connect states that are not connected.

This is unlike replay_twa_run(), which will ensure the run actually exists in the automaton (and will also display any transition annotation).

Member Data Documentation

◆ aut

const_twa_ptr spot::twa_run::aut

The automaton this run is associated with.

◆ cycle

steps spot::twa_run::cycle

The cycle part of the run.

◆ prefix

steps spot::twa_run::prefix

The prefix part of the run.

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

spot/twaalgos/emptiness.hh

Classes

Public Types

Public Member Functions

Public Attributes

Friends