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();
73 bdd_dict_ptr get_dict()
const;
102 artificial_initial_state_ = s;
107 delete_stuttering_and_hole_successors(
const spot::state* s);
117 ta_explicit(
const ta_explicit& other) =
delete;
118 ta_explicit& operator=(
const ta_explicit& other) =
delete;
121 state_ta_explicit* artificial_initial_state_;
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)
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);
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;
231 virtual bool done()
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: taexplicit.hh:129
virtual state_ta_explicit * clone() const override
Duplicate a state.
void delete_stuttering_and_hole_successors()
Remove stuttering transitions and transitions leading to states having no successors.
virtual void destroy() const override
Release a state.
Definition: taexplicit.hh:159
virtual size_t hash() const override
Hash a state.
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
bool is_hole_state() const
Return true if the state has no successors.
Abstract class for states.
Definition: twa.hh:51
Successor iterators used by spot::ta_explicit.
Definition: taexplicit.hh:223
virtual bool next() override
Jump to the next successor (if any).
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
virtual bool done() const override
Check whether the iteration is finished.
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
virtual bool first() override
Position the iterator on the first successor (if any).
virtual const state * dst() const override
Get the destination state of the current edge.
Definition: taexplicit.hh:40
virtual ta_succ_iterator * succ_iter(const spot::state *s) const override
Get an iterator over the successors of state.
virtual bool is_initial_state(const spot::state *s) const override
Return true if s is an initial state, otherwise false.
virtual bool is_accepting_state(const spot::state *s) const override
Return true if s is a Buchi-accepting state, otherwise false.
virtual const_states_set_t get_initial_states_set() const override
Get the initial states set of the automaton.
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
virtual ta_succ_iterator * succ_iter(const spot::state *s, bdd condition) const override
Get an iterator over the successors of state filtred by the changeset on transitions.
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
virtual bool is_livelock_accepting_state(const spot::state *s) const override
Return true if s is a livelock-accepting state , otherwise false.
virtual void free_state(const spot::state *s) const override
Release a state s.
virtual bdd get_state_condition(const spot::state *s) const override
Return a BDD condition that represents the valuation of atomic propositions in the state s.
Iterate over the successors of a state.
Definition: ta.hh:198
A Testing Automaton.
Definition: ta.hh:76
Definition: automata.hh:27
std::set< const state * > get_states_set(const const_ta_ptr &t)
Compute states set for an automaton.
An acceptance mark.
Definition: acc.hh:85
Explicit transitions.
Definition: taexplicit.hh:135