25 #include <spot/misc/bddlt.hh>
26 #include <spot/twa/twa.hh>
32 class ta_succ_iterator;
82 ta(
const bdd_dict_ptr& d)
92 typedef std::set<state*, state_ptr_less_than> states_set_t;
93 typedef std::set<const state*, state_ptr_less_than> const_states_set_t;
96 virtual const_states_set_t
186 typedef std::shared_ptr<ta> ta_ptr;
187 typedef std::shared_ptr<const ta> const_ta_ptr;
225 std::list<const state*> rem;
249 std::list<const state*>&
256 typedef std::list<connected_component> stack_type;
An acceptance condition.
Definition: acc.hh:62
size_t size() const
How many SCC are in stack.
bool empty() const
Is the stack empty?
void pop()
Pop the top SCC.
std::list< const state * > & rem()
The rem member of the top SCC.
void push(int index)
Stack a new SCC with index index.
connected_component & top()
Access the top SCC.
const connected_component & top() const
Access the top SCC.
Abstract class for states.
Definition: twa.hh:51
Iterate over the successors of a state.
Definition: ta.hh:198
A Testing Automaton.
Definition: ta.hh:76
virtual bool is_accepting_state(const spot::state *s) const =0
Return true if s is a Buchi-accepting state, otherwise false.
virtual std::string format_state(const spot::state *s) const =0
Format the state as a string for printing.
virtual const_states_set_t get_initial_states_set() const =0
Get the initial states set of the automaton.
virtual bool is_livelock_accepting_state(const spot::state *s) const =0
Return true if s is a livelock-accepting state , otherwise false.
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: ta.hh:139
virtual bdd get_state_condition(const spot::state *s) const =0
Return a BDD condition that represents the valuation of atomic propositions in the state s.
virtual void free_state(const spot::state *s) const =0
Release a state s.
virtual bool is_initial_state(const spot::state *s) const =0
Return true if s is an initial state, otherwise false.
virtual const spot::state * get_artificial_initial_state() const
Get the artificial initial state set of the automaton. Return 0 if this artificial state is not imple...
Definition: ta.hh:107
virtual ta_succ_iterator * succ_iter(const spot::state *state) const =0
Get an iterator over the successors of state.
virtual ta_succ_iterator * succ_iter(const spot::state *state, bdd changeset) const =0
Get an iterator over the successors of state filtred by the changeset on transitions.
Iterate over the successors of a state.
Definition: twa.hh:398
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85
acc_cond::mark_t condition
Definition: ta.hh:223
int index
Index of the SCC.
Definition: ta.hh:217