Class for representing a thread-safe twa.
More...
#include <spot/twacube/twacube.hh>
|
| 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 |
|
|
std::ostream & | operator<< (std::ostream &os, const twacube &twa) |
|
Class for representing a thread-safe twa.
◆ twacube()
spot::twacube::twacube |
( |
const std::vector< std::string > |
aps | ) |
|
Build a new automaton from a list of atomic propositions.
◆ 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()
Returns the storage associated to a transition.
The documentation for this class was generated from the following file: