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;
35 class ta_explicit_succ_iterator;
54 add_to_initial_states_set(
state* s, bdd condition = bddfalse);
60 bool add_at_beginning =
false);
63 delete_stuttering_transitions();
67 virtual const_states_set_t get_initial_states_set()
const override;
72 succ_iter(
const spot::state* s, bdd condition)
const override;
74 bdd_dict_ptr get_dict()
const;
80 is_accepting_state(
const spot::state* s)
const override;
83 is_livelock_accepting_state(
const spot::state* s)
const override;
86 is_initial_state(
const spot::state* s)
const override;
89 get_state_condition(
const spot::state* s)
const override;
103 artificial_initial_state_ = s;
108 delete_stuttering_and_hole_successors(
const spot::state* s);
118 ta_explicit(
const ta_explicit& other) =
delete;
119 ta_explicit& operator=(
const ta_explicit& other) =
delete;
122 state_ta_explicit* artificial_initial_state_;
123 ta::states_set_t states_set_;
124 ta::const_states_set_t initial_states_set_;
142 typedef std::list<transition*> transitions;
145 bool is_initial_state =
false,
146 bool is_accepting_state =
false,
147 bool is_livelock_accepting_state =
false,
148 transitions* trans =
nullptr) :
149 tgba_state_(tgba_state), tgba_condition_(tgba_condition),
150 is_initial_state_(is_initial_state), is_accepting_state_(
151 is_accepting_state), is_livelock_accepting_state_(
152 is_livelock_accepting_state), transitions_(trans)
156 virtual int compare(
const spot::state* other)
const override;
157 virtual size_t hash()
const override;
170 get_transitions()
const;
174 get_transitions(bdd condition)
const;
177 add_transition(transition* t,
bool add_at_beginning =
false);
180 get_tgba_state()
const;
182 get_tgba_condition()
const;
184 is_accepting_state()
const;
186 set_accepting_state(
bool is_accepting_state);
188 is_livelock_accepting_state()
const;
190 set_livelock_accepting_state(
bool is_livelock_accepting_state);
193 is_initial_state()
const;
195 set_initial_state(
bool is_initial_state);
199 is_hole_state()
const;
204 delete_stuttering_and_hole_successors();
209 state_ta_explicit* stuttering_reachable_livelock;
211 const state* tgba_state_;
212 const bdd tgba_condition_;
213 bool is_initial_state_;
214 bool is_accepting_state_;
215 bool is_livelock_accepting_state_;
216 transitions* transitions_;
217 std::unordered_map<int, transitions*, std::hash<int>>
218 transitions_by_condition;
230 virtual bool first()
override;
231 virtual bool next()
override;
232 virtual bool done()
const override;
234 virtual const state* dst()
const override;
235 virtual bdd cond()
const override;
240 state_ta_explicit::transitions* transitions_;
241 state_ta_explicit::transitions::const_iterator i_;
244 typedef std::shared_ptr<ta_explicit> ta_explicit_ptr;
245 typedef std::shared_ptr<const ta_explicit> const_ta_explicit_ptr;
247 inline ta_explicit_ptr
248 make_ta_explicit(
const const_twa_ptr& tgba,
252 return std::make_shared<ta_explicit>(tgba, n_acc, artificial_initial_state);
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:95
Successor iterators used by spot::ta_explicit.
Definition: taexplicit.hh:223
Abstract class for states.
Definition: twa.hh:50
Explicit transitions.
Definition: taexplicit.hh:135
Definition: taexplicit.hh:40
virtual void destroy() const override
Release a state.
Definition: taexplicit.hh:160
Definition: taexplicit.hh:129
A Testing Automaton.
Definition: ta.hh:75
Iterate over the successors of a state.
Definition: ta.hh:197