22 #include <spot/misc/hash.hh> 24 #include <spot/twa/twa.hh> 28 #include <spot/misc/bddlt.hh> 29 #include <spot/ta/ta.hh> 34 class state_ta_explicit;
53 add_to_initial_states_set(
state* s, bdd condition = bddfalse);
59 bool add_at_beginning =
false);
62 delete_stuttering_transitions();
66 virtual const_states_set_t get_initial_states_set()
const override;
71 succ_iter(
const spot::state* s, bdd condition)
const override;
73 bdd_dict_ptr get_dict()
const;
79 is_accepting_state(
const spot::state* s)
const override;
82 is_livelock_accepting_state(
const spot::state* s)
const override;
85 is_initial_state(
const spot::state* s)
const override;
88 get_state_condition(
const spot::state* s)
const override;
102 artificial_initial_state_ = s;
107 delete_stuttering_and_hole_successors(
const spot::state* s);
122 ta::states_set_t states_set_;
123 ta::const_states_set_t initial_states_set_;
141 typedef std::list<transition*> transitions;
144 bool is_initial_state =
false,
145 bool is_accepting_state =
false,
146 bool is_livelock_accepting_state =
false,
147 transitions* trans =
nullptr) :
148 tgba_state_(tgba_state), tgba_condition_(tgba_condition),
149 is_initial_state_(is_initial_state), is_accepting_state_(
150 is_accepting_state), is_livelock_accepting_state_(
151 is_livelock_accepting_state), transitions_(trans)
155 virtual int compare(
const spot::state* other)
const override;
156 virtual size_t hash()
const override;
169 get_transitions()
const;
173 get_transitions(bdd condition)
const;
176 add_transition(
transition* t,
bool add_at_beginning =
false);
179 get_tgba_state()
const;
181 get_tgba_condition()
const;
183 is_accepting_state()
const;
185 set_accepting_state(
bool is_accepting_state);
187 is_livelock_accepting_state()
const;
189 set_livelock_accepting_state(
bool is_livelock_accepting_state);
192 is_initial_state()
const;
194 set_initial_state(
bool is_initial_state);
198 is_hole_state()
const;
203 delete_stuttering_and_hole_successors();
210 const state* tgba_state_;
211 const bdd tgba_condition_;
212 bool is_initial_state_;
213 bool is_accepting_state_;
214 bool is_livelock_accepting_state_;
215 transitions* transitions_;
216 std::unordered_map<int, transitions*, std::hash<int>>
217 transitions_by_condition;
229 virtual bool first()
override;
230 virtual bool next()
override;
231 virtual bool done()
const override;
233 virtual const state* dst()
const override;
234 virtual bdd cond()
const override;
239 state_ta_explicit::transitions* transitions_;
240 state_ta_explicit::transitions::const_iterator i_;
243 typedef std::shared_ptr<ta_explicit> ta_explicit_ptr;
244 typedef std::shared_ptr<const ta_explicit> const_ta_explicit_ptr;
246 inline ta_explicit_ptr
247 make_ta_explicit(
const const_twa_ptr& tgba,
251 return std::make_shared<ta_explicit>(tgba, n_acc, artificial_initial_state);
Definition: automata.hh:26
virtual spot::state * get_artificial_initial_state() const override
Get the artificial initial state set of the automaton. Return 0 if this artificial state is not imple...
Definition: taexplicit.hh:94
Successor iterators used by spot::ta_explicit.
Definition: taexplicit.hh:222
Abstract class for states.
Definition: twa.hh:50
Explicit transitions.
Definition: taexplicit.hh:134
Definition: taexplicit.hh:39
virtual void destroy() const override
Release a state.
Definition: taexplicit.hh:159
Definition: taexplicit.hh:128
A Testing Automaton.
Definition: ta.hh:75
Iterate over the successors of a state.
Definition: ta.hh:197