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. More...
acc_cond &	acc ()
	Returns the acceptance condition associated to the automaton. More...
std::vector< std::string >	ap () const
	Returns the names of the atomic properties. More...
unsigned	new_state ()
	This method creates a new state. More...
void	set_initial (unsigned init)
	Updates the initial state to init. More...
unsigned	get_initial () const
	Returns the id of the initial state in the automaton. More...
cstate *	state_from_int (unsigned i)
	Accessor for a state from its id. More...
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. More...
const cubeset &	get_cubeset () const
	Accessor the cube's manipulator. More...
bool	succ_contiguous () const
	Check if all the successors of a state are located contiguously in memory. This is mandatory for swarming techniques. More...
unsigned	num_states () const
unsigned	num_edges () const
const graph_t &	get_graph ()
	Returns the underlying graph for this automaton. More...
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. More...
const transition &	trans_data (std::shared_ptr< trans_index > ci, unsigned seed=0) const
	Returns the data associated to a transition. More...
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