26 #include <spot/misc/hash.hh>
28 #include <spot/twa/bdddict.hh>
29 #include <spot/twa/twa.hh>
41 typedef std::list<transition*> state;
62 typedef std::vector<
taa_tgba::state_set*> ss_vec;
65 ss_vec state_set_vec_;
79 set_state(
const taa_tgba::state_set* s,
bool delete_me =
false)
80 : s_(s), delete_me_(delete_me)
85 virtual size_t hash()
const override;
94 const taa_tgba::state_set* get_state()
const;
96 const taa_tgba::state_set* s_;
108 virtual bool done()
const override;
111 virtual bdd
cond()
const override;
117 typedef taa_tgba::state::const_iterator iterator;
118 typedef std::pair<iterator, iterator> iterator_pair;
119 typedef std::vector<iterator_pair> bounds_t;
121 std::vector<taa_tgba::transition*>,
127 operator()(
const iterator_pair& lhs,
const iterator_pair& rhs)
const
129 return std::distance(lhs.first, lhs.second) <
130 std::distance(rhs.first, rhs.second);
134 std::vector<taa_tgba::transition*>::const_iterator i_;
135 std::vector<taa_tgba::transition*> succ_;
137 const acc_cond& acc_;
142 template<
typename label>
150 for (
auto i: name_state_map_)
152 for (
auto i2: *i.second)
158 void set_init_state(
const label& s)
160 std::vector<label> v(1);
164 void set_init_state(
const std::vector<label>& s)
166 init_ = add_state_set(s);
170 create_transition(
const label& s,
171 const std::vector<label>& d)
173 state* src = add_state(s);
174 state_set* dst = add_state_set(d);
177 t->condition = bddtrue;
178 t->acceptance_conditions = {};
179 src->emplace_back(t);
184 create_transition(
const label& s,
const label& d)
186 std::vector<std::string> vec;
188 return create_transition(s, vec);
196 t->acceptance_conditions |= p.first->second;
210 const state_set* ss = se->get_state();
211 return format_state_set(ss);
217 typename ns_map::const_iterator i;
218 for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
220 taa_tgba::state::const_iterator i2;
221 os <<
"State: " << label_to_string(i->first) << std::endl;
222 for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
224 os <<
' ' << format_state_set((*i2)->dst)
225 <<
", C:" << (*i2)->condition
226 <<
", A:" << (*i2)->acceptance_conditions << std::endl;
232 typedef label label_t;
234 typedef std::unordered_map<label, taa_tgba::state*> ns_map;
235 typedef std::unordered_map<
const taa_tgba::state*, label,
238 ns_map name_state_map_;
239 sn_map state_name_map_;
247 taa_tgba::state* add_state(
const label& name)
249 typename ns_map::iterator i = name_state_map_.find(name);
250 if (i == name_state_map_.end())
252 taa_tgba::state* s =
new taa_tgba::state;
253 name_state_map_[name] = s;
254 state_name_map_[s] = name;
261 taa_tgba::state_set* add_state_set(
const std::vector<label>& names)
264 for (
unsigned i = 0; i < names.size(); ++i)
265 ss->insert(add_state(names[i]));
266 state_set_vec_.emplace_back(ss);
270 std::string format_state_set(
const taa_tgba::state_set* ss)
const
272 state_set::const_iterator i1 = ss->begin();
273 typename sn_map::const_iterator i2;
275 return std::string(
"{}");
278 i2 = state_name_map_.find(*i1);
279 SPOT_ASSERT(i2 != state_name_map_.end());
280 return "{" + label_to_string(i2->second) +
"}";
284 std::string res(
"{");
285 while (i1 != ss->end())
287 i2 = state_name_map_.find(*i1++);
288 SPOT_ASSERT(i2 != state_name_map_.end());
289 res += label_to_string(i2->second);
292 res[res.size() - 1] =
'}';
315 typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
316 typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
318 inline taa_tgba_string_ptr make_taa_tgba_string(
const bdd_dict_ptr& dict)
340 typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
341 typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
343 inline taa_tgba_formula_ptr make_taa_tgba_formula(
const bdd_dict_ptr& dict)
An acceptance condition.
Definition: acc.hh:62
Set of states deriving from spot::state.
Definition: taatgba.hh:77
virtual set_state * clone() const override
Duplicate a state.
virtual size_t hash() const override
Hash a state.
virtual int compare(const spot::state *) const override
Compares two states (that come from the same automaton).
Abstract class for states.
Definition: twa.hh:51
Definition: taatgba.hh:101
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 acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
virtual set_state * dst() const override
Get the destination state of the current edge.
virtual bool done() const override
Check whether the iteration is finished.
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: taatgba.hh:144
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
Definition: taatgba.hh:207
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:215
virtual std::string label_to_string(const label_t &lbl) const =0
Return a label as a string.
Definition: taatgba.hh:304
virtual std::string label_to_string(const std::string &label) const override
Return a label as a string.
A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class,...
Definition: taatgba.hh:36
virtual spot::state * get_init_state() const override final
Get the initial state of the automaton.
virtual ~taa_tgba()
TGBA interface.
Iterate over the successors of a state.
Definition: twa.hh:398
A Transition-based ω-Automaton.
Definition: twa.hh:623
Definition: automata.hh:27
std::unordered_set< const state *, state_ptr_hash, state_ptr_equal > state_set
Unordered set of abstract states.
Definition: twa.hh:190
An acceptance mark.
Definition: acc.hh:85
A hash function for pointers.
Definition: hash.hh:40
An Equivalence Relation for state*.
Definition: twa.hh:151
Hash Function for state*.
Definition: twa.hh:175
Explicit transitions.
Definition: taatgba.hh:46