25 #include <spot/misc/hash.hh>
26 #include <spot/twa/twa.hh>
54 virtual void add_state(
const state* s) = 0;
56 virtual const state* next_state() = 0;
61 virtual bool want_state(
const state* s)
const;
86 virtual void process_link(
const state* in_s,
int in,
87 const state* out_s,
int out,
105 virtual void add_state(
const state* s)
override;
106 virtual const state* next_state()
override;
129 virtual bool want_state(
const state* s)
const;
132 virtual void start();
154 virtual void process_link(
const state* in_s,
int in,
155 const state* out_s,
int out,
171 virtual void push(
const state* s,
int sn);
192 virtual void push(
const state* s,
int sn)
override;
193 virtual void pop()
override;
195 std::unordered_set<int> stack_;
Iterate over all states of an automaton using a DFS.
Definition: reachiter.hh:114
std::deque< stack_item > todo
the DFS stack
Definition: reachiter.hh:168
state_map< int > seen
States already seen.
Definition: reachiter.hh:93
virtual void push(const state *s, int sn) override
Push a new state in todo.
Abstract class for states.
Definition: twa.hh:50
Iterate over all reachable states of a spot::tgba.
Definition: reachiter.hh:34
An implementation of spot::twa_reachable_iterator that browses states breadth first.
Definition: reachiter.hh:99
Definition: reachiter.hh:162
Iterate over all states of an automaton using a DFS.
Definition: reachiter.hh:181
Iterate over the successors of a state.
Definition: twa.hh:397
state_map< int > seen
States already seen.
Definition: reachiter.hh:161
const_twa_ptr aut_
The spot::tgba to explore.
Definition: reachiter.hh:159
const_twa_ptr aut_
The spot::tgba to explore.
Definition: reachiter.hh:91
virtual void pop() override
Pop the DFS stack.
std::deque< const state * > todo
A queue of states yet to explore.
Definition: reachiter.hh:109
bool on_stack(int sn) const
Whether state sn is on the DFS stack.