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
97 get_initial_states_set()
const = 0;
129 succ_iter(
const spot::state* state, bdd changeset)
const = 0;
153 is_accepting_state(
const spot::state* s)
const = 0;
158 is_livelock_accepting_state(
const spot::state* s)
const = 0;
167 get_state_condition(
const spot::state* s)
const = 0;
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;
Definition: automata.hh:26
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: ta.hh:139
Abstract class for states.
Definition: twa.hh:50
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
Iterate over the successors of a state.
Definition: twa.hh:397
An acceptance condition.
Definition: acc.hh:58
acc_cond::mark_t condition
Definition: ta.hh:223
A Testing Automaton.
Definition: ta.hh:75
int index
Index of the SCC.
Definition: ta.hh:217
Iterate over the successors of a state.
Definition: ta.hh:197
An acceptance mark.
Definition: acc.hh:81