26 #include <spot/misc/hash.hh>
28 #include <spot/twa/bdddict.hh>
29 #include <spot/twa/twa.hh>
41 typedef std::list<transition*> state;
42 typedef std::set<state*> state_set;
56 virtual spot::state* get_init_state() const override final;
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)
84 virtual int compare(
const spot::state*)
const override;
85 virtual size_t hash()
const override;
86 virtual set_state* clone()
const override;
94 const taa_tgba::state_set* get_state()
const;
96 const taa_tgba::state_set* s_;
106 virtual bool first()
override;
107 virtual bool next()
override;
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_;
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 = 0
U;
186 create_transition(
const label& s,
const label& d)
188 std::vector<std::string> vec;
190 return create_transition(s, vec);
195 auto p = acc_map_.emplace(f, 0);
198 t->acceptance_conditions |= p.first->second;
213 const state_set* ss = se->get_state();
214 return format_state_set(ss);
220 typename ns_map::const_iterator i;
221 for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
223 taa_tgba::state::const_iterator i2;
224 os <<
"State: " << label_to_string(i->first) << std::endl;
225 for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
227 os <<
' ' << format_state_set((*i2)->dst)
228 <<
", C:" << (*i2)->condition
229 <<
", A:" << (*i2)->acceptance_conditions << std::endl;
235 typedef label label_t;
237 typedef std::unordered_map<label, taa_tgba::state*> ns_map;
238 typedef std::unordered_map<
const taa_tgba::state*, label,
241 ns_map name_state_map_;
242 sn_map state_name_map_;
245 virtual std::string label_to_string(
const label_t& lbl)
const = 0;
250 taa_tgba::state* add_state(
const label& name)
252 typename ns_map::iterator i = name_state_map_.find(name);
253 if (i == name_state_map_.end())
255 taa_tgba::state* s =
new taa_tgba::state;
256 name_state_map_[name] = s;
257 state_name_map_[s] = name;
264 taa_tgba::state_set* add_state_set(
const std::vector<label>& names)
266 state_set* ss =
new state_set;
267 for (
unsigned i = 0; i < names.size(); ++i)
268 ss->insert(add_state(names[i]));
269 state_set_vec_.push_back(ss);
273 std::string format_state_set(
const taa_tgba::state_set* ss)
const
275 state_set::const_iterator i1 = ss->begin();
276 typename sn_map::const_iterator i2;
278 return std::string(
"{}");
281 i2 = state_name_map_.find(*i1);
282 SPOT_ASSERT(i2 != state_name_map_.end());
283 return "{" + label_to_string(i2->second) +
"}";
287 std::string res(
"{");
288 while (i1 != ss->end())
290 i2 = state_name_map_.find(*i1++);
291 SPOT_ASSERT(i2 != state_name_map_.end());
292 res += label_to_string(i2->second);
295 res[res.size() - 1] =
'}';
314 virtual std::string label_to_string(
const std::string& label)
318 typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
319 typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
321 inline taa_tgba_string_ptr make_taa_tgba_string(
const bdd_dict_ptr& dict)
323 return std::make_shared<taa_tgba_string>(dict);
339 virtual std::string label_to_string(
const label_t& label)
343 typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
344 typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
346 inline taa_tgba_formula_ptr make_taa_tgba_formula(
const bdd_dict_ptr& dict)
348 return std::make_shared<taa_tgba_formula>(dict);
An Equivalence Relation for state*.
Definition: twa.hh:150
A Transition-based ω-Automaton.
Definition: twa.hh:621
A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class...
Definition: taatgba.hh:35
Definition: taatgba.hh:100
Definition: formula.hh:1658
Abstract class for states.
Definition: twa.hh:50
A hash function for pointers.
Definition: hash.hh:39
Explicit transitions.
Definition: taatgba.hh:45
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
Definition: taatgba.hh:209
Iterate over the successors of a state.
Definition: twa.hh:397
Hash Function for state*.
Definition: twa.hh:174
Definition: taatgba.hh:301
Set of states deriving from spot::state.
Definition: taatgba.hh:76
Definition: taatgba.hh:145
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:218