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;
62 typedef std::vector<taa_tgba::state_set*> ss_vec;
64 taa_tgba::state_set* init_;
65 ss_vec state_set_vec_;
67 std::map<formula, acc_cond::mark_t> acc_map_;
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 = {};
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;
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_;
244 virtual std::string label_to_string(
const label_t& lbl)
const = 0;
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)
265 state_set* ss =
new state_set;
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] =
'}';
313 virtual std::string label_to_string(
const std::string& label)
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)
338 virtual std::string label_to_string(
const label_t& label)
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)
Definition: automata.hh:26
An Equivalence Relation for state*.
Definition: twa.hh:150
A Transition-based ω-Automaton.
Definition: twa.hh:622
A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class...
Definition: taatgba.hh:35
Definition: taatgba.hh:100
Abstract class for states.
Definition: twa.hh:50
A hash function for pointers.
Definition: hash.hh:38
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
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:217
An acceptance condition.
Definition: acc.hh:58
Hash Function for state*.
Definition: twa.hh:174
Definition: taatgba.hh:300
Set of states deriving from spot::state.
Definition: taatgba.hh:76
Definition: taatgba.hh:145
An acceptance mark.
Definition: acc.hh:81