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*>,
124 struct distance_sort :
125 public std::binary_function<const iterator_pair&,
126 const iterator_pair&, bool>
129 operator()(
const iterator_pair& lhs,
const iterator_pair& rhs)
const
131 return std::distance(lhs.first, lhs.second) <
132 std::distance(rhs.first, rhs.second);
136 std::vector<taa_tgba::transition*>::const_iterator i_;
137 std::vector<taa_tgba::transition*> succ_;
139 const acc_cond& acc_;
144 template<
typename label>
152 for (
auto i: name_state_map_)
154 for (
auto i2: *i.second)
160 void set_init_state(
const label& s)
162 std::vector<label> v(1);
166 void set_init_state(
const std::vector<label>& s)
168 init_ = add_state_set(s);
172 create_transition(
const label& s,
173 const std::vector<label>& d)
175 state* src = add_state(s);
176 state_set* dst = add_state_set(d);
179 t->condition = bddtrue;
180 t->acceptance_conditions = {};
181 src->emplace_back(t);
186 create_transition(
const label& s,
const label& d)
188 std::vector<std::string> vec;
190 return create_transition(s, vec);
198 t->acceptance_conditions |= p.first->second;
212 const state_set* ss = se->get_state();
213 return format_state_set(ss);
219 typename ns_map::const_iterator i;
220 for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
222 taa_tgba::state::const_iterator i2;
223 os <<
"State: " << label_to_string(i->first) << std::endl;
224 for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
226 os <<
' ' << format_state_set((*i2)->dst)
227 <<
", C:" << (*i2)->condition
228 <<
", A:" << (*i2)->acceptance_conditions << std::endl;
234 typedef label label_t;
236 typedef std::unordered_map<label, taa_tgba::state*> ns_map;
237 typedef std::unordered_map<
const taa_tgba::state*, label,
240 ns_map name_state_map_;
241 sn_map state_name_map_;
249 taa_tgba::state* add_state(
const label& name)
251 typename ns_map::iterator i = name_state_map_.find(name);
252 if (i == name_state_map_.end())
254 taa_tgba::state* s =
new taa_tgba::state;
255 name_state_map_[name] = s;
256 state_name_map_[s] = name;
263 taa_tgba::state_set* add_state_set(
const std::vector<label>& names)
266 for (
unsigned i = 0; i < names.size(); ++i)
267 ss->insert(add_state(names[i]));
268 state_set_vec_.emplace_back(ss);
272 std::string format_state_set(
const taa_tgba::state_set* ss)
const
274 state_set::const_iterator i1 = ss->begin();
275 typename sn_map::const_iterator i2;
277 return std::string(
"{}");
280 i2 = state_name_map_.find(*i1);
281 SPOT_ASSERT(i2 != state_name_map_.end());
282 return "{" + label_to_string(i2->second) +
"}";
286 std::string res(
"{");
287 while (i1 != ss->end())
289 i2 = state_name_map_.find(*i1++);
290 SPOT_ASSERT(i2 != state_name_map_.end());
291 res += label_to_string(i2->second);
294 res[res.size() - 1] =
'}';
317 typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
318 typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
320 inline taa_tgba_string_ptr make_taa_tgba_string(
const bdd_dict_ptr& dict)
342 typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
343 typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
345 inline taa_tgba_formula_ptr make_taa_tgba_formula(
const bdd_dict_ptr& dict)
An acceptance condition.
Definition: acc.hh:61
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:146
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
Definition: taatgba.hh:209
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:217
virtual std::string label_to_string(const label_t &lbl) const =0
Return a label as a string.
Definition: taatgba.hh:306
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:89
A hash function for pointers.
Definition: hash.hh:41
An Equivalence Relation for state*.
Definition: twa.hh:151
Hash Function for state*.
Definition: twa.hh:175
Explicit transitions.
Definition: taatgba.hh:46