spot::twacube Class Reference

Class for representing a thread-safe twa. More...

#include <spot/twacube/twacube.hh>

Inheritance diagram for spot::twacube:

Collaboration diagram for spot::twacube:

Public Types
typedef digraph< cstate, transition >	graph_t
typedef graph_t::edge_storage_t	edge_storage_t

Public Member Functions
	twacube (const std::vector< std::string > aps)
	Build a new automaton from a list of atomic propositions.
acc_cond &	acc ()
	Returns the acceptance condition associated to the automaton.
std::vector< std::string >	ap () const
	Returns the names of the atomic properties.
unsigned	new_state ()
	This method creates a new state.
void	set_initial (unsigned init)
	Updates the initial state to init.
unsigned	get_initial () const
	Returns the id of the initial state in the automaton.
cstate *	state_from_int (unsigned i)
	Accessor for a state from its id.
void	create_transition (unsigned src, const cube &cube, const acc_cond::mark_t &mark, unsigned dst)
	create a transition between state src and state dst, using cube as the labelling cube and mark as the acceptance mark.
const cubeset &	get_cubeset () const
	Accessor the cube's manipulator.
bool	succ_contiguous () const
	Check if all the successors of a state are located contiguously in memory. This is mandatory for swarming techniques.
unsigned	num_states () const
unsigned	num_edges () const
const graph_t &	get_graph ()
	Returns the underlying graph for this automaton.
const graph_t::edge_storage_t &	trans_storage (std::shared_ptr< trans_index > ci, unsigned seed=0) const
	Returns the storage associated to a transition.
const transition &	trans_data (std::shared_ptr< trans_index > ci, unsigned seed=0) const
	Returns the data associated to a transition.
std::shared_ptr< trans_index >	succ (unsigned i) const

Friends
std::ostream &	operator<< (std::ostream &os, const twacube &twa)

Detailed Description

Class for representing a thread-safe twa.

Constructor & Destructor Documentation

twacube()

spot::twacube::twacube

(

const std::vector< std::string >

aps

)

Build a new automaton from a list of atomic propositions.

Member Function Documentation

acc()

acc_cond & spot::twacube::acc

(

)

Returns the acceptance condition associated to the automaton.

ap()

std::vector< std::string > spot::twacube::ap

(

)

const

Returns the names of the atomic properties.

create_transition()

void spot::twacube::create_transition	(	unsigned	src,
		const cube &	cube,
		const acc_cond::mark_t &	mark,
		unsigned	dst )

create a transition between state src and state dst, using cube as the labelling cube and mark as the acceptance mark.

get_cubeset()

const cubeset & spot::twacube::get_cubeset

(

)

const

Accessor the cube's manipulator.

get_graph()

const graph_t & spot::twacube::get_graph ( )

inline

Returns the underlying graph for this automaton.

get_initial()

unsigned spot::twacube::get_initial

(

)

const

Returns the id of the initial state in the automaton.

new_state()

unsigned spot::twacube::new_state

(

)

This method creates a new state.

set_initial()

void spot::twacube::set_initial

(

unsigned

init

)

Updates the initial state to init.

state_from_int()

cstate * spot::twacube::state_from_int

(

unsigned

i

)

Accessor for a state from its id.

succ_contiguous()

bool spot::twacube::succ_contiguous

(

)

const

Check if all the successors of a state are located contiguously in memory. This is mandatory for swarming techniques.

trans_data()

const transition & spot::twacube::trans_data ( std::shared_ptr< trans_index > ci, unsigned seed = 0 ) const

inline

Returns the data associated to a transition.

Returns the successor of state i.

trans_storage()

const graph_t::edge_storage_t & spot::twacube::trans_storage ( std::shared_ptr< trans_index > ci, unsigned seed = 0 ) const

inline

Returns the storage associated to a transition.

---

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

• spot/twacube/twacube.hh