24 #include <spot/graph/graph.hh>
25 #include <spot/misc/hash.hh>
26 #include <spot/twa/acc.hh>
27 #include <spot/twacube/cube.hh>
28 #include <spot/twacube/fwd.hh>
58 public std::enable_shared_from_this<trans_index>
93 return !idx_ || idx_ > st_.succ_tail;
98 inline unsigned current(
unsigned seed = 0)
const
102 if (SPOT_UNLIKELY(!seed))
109 SPOT_ASSERT(primes[seed] > (st_.succ_tail-st_.succ+1));
110 unsigned long long c = (idx_-st_.succ) + 1;
111 unsigned long long p = primes[seed];
112 unsigned long long s = (st_.succ_tail-st_.succ+1);
113 return (
unsigned) (((c*p) % s)+st_.succ);
118 const graph_t::state_storage_t& st_;
122 class SPOT_API
twacube final:
public std::enable_shared_from_this<twacube>
136 std::vector<std::string>
ap()
const;
164 unsigned num_states()
const
166 return theg_.num_states();
169 unsigned num_edges()
const
171 return theg_.num_edges();
174 typedef digraph<cstate, transition> graph_t;
181 typedef graph_t::edge_storage_t edge_storage_t;
184 const graph_t::edge_storage_t&
186 unsigned seed = 0)
const
188 return theg_.edge_storage(ci->current(seed));
193 unsigned seed = 0)
const
195 return theg_.edge_data(ci->current(seed));
199 std::shared_ptr<trans_index> succ(
unsigned i)
const
201 return std::make_shared<trans_index>(i, theg_);
204 friend SPOT_API std::ostream& operator<<(std::ostream& os,
209 const std::vector<std::string> aps_;
214 inline twacube_ptr make_twacube(
const std::vector<std::string> aps)
216 return std::make_shared<twacube>(aps);
An acceptance condition.
Definition: acc.hh:62
Class for thread-safe states.
Definition: twacube.hh:34
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:712
Abstract class for states.
Definition: twa.hh:51
Class for iterators over transitions.
Definition: twacube.hh:59
bool done() const
Returns a boolean indicating wether all the transitions have been iterated.
Definition: twacube.hh:91
unsigned current(unsigned seed=0) const
Returns the current transition according to a specific seed. The seed is traditionnally the thread id...
Definition: twacube.hh:98
void reset()
Reset the iterator on the first element.
Definition: twacube.hh:78
void next()
Iterate over the next transition.
Definition: twacube.hh:84
Class for representing a transition.
Definition: twacube.hh:44
Class for representing a thread-safe twa.
Definition: twacube.hh:123
const graph_t & get_graph()
Returns the underlying graph for this automaton.
Definition: twacube.hh:177
unsigned new_state()
This method creates a new state.
acc_cond & acc()
Returns the acceptance condition associated to the automaton.
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...
unsigned get_initial() const
Returns the id of the initial state in the automaton.
bool succ_contiguous() const
Check if all the successors of a state are located contiguously in memory. This is mandatory for swar...
const transition & trans_data(std::shared_ptr< trans_index > ci, unsigned seed=0) const
Returns the data associated to a transition.
Definition: twacube.hh:192
const cubeset & get_cubeset() const
Accessor the cube's manipulator.
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.
Definition: twacube.hh:185
twacube(const std::vector< std::string > aps)
Build a new automaton from a list of atomic propositions.
void set_initial(unsigned init)
Updates the initial state to init.
cstate * state_from_int(unsigned i)
Accessor for a state from its id.
std::vector< std::string > ap() const
Returns the names of the atomic properties.
Definition: automata.hh:27
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:66
An acceptance mark.
Definition: acc.hh:85