spot  2.12
taatgba.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <set>
22 #include <iosfwd>
23 #include <vector>
24 #include <string>
25 #include <spot/misc/hash.hh>
26 #include <spot/tl/formula.hh>
27 #include <spot/twa/bdddict.hh>
28 #include <spot/twa/twa.hh>
29 
30 namespace spot
31 {
34  class SPOT_API taa_tgba: public twa
35  {
36  public:
37  taa_tgba(const bdd_dict_ptr& dict);
38 
39  struct transition;
40  typedef std::list<transition*> state;
41  typedef std::set<state*> state_set;
42 
44  struct transition
45  {
46  bdd condition;
47  acc_cond::mark_t acceptance_conditions;
48  const state_set* dst;
49  };
50 
51  void add_condition(transition* t, formula f);
52 
54  virtual ~taa_tgba();
55  virtual spot::state* get_init_state() const override final;
56  virtual twa_succ_iterator* succ_iter(const spot::state* state)
57  const override final;
58 
59  protected:
60 
61  typedef std::vector<taa_tgba::state_set*> ss_vec;
62 
63  taa_tgba::state_set* init_;
64  ss_vec state_set_vec_;
65 
66  std::map<formula, acc_cond::mark_t> acc_map_;
67 
68  private:
69  // Disallow copy.
70  taa_tgba(const taa_tgba& other) = delete;
71  taa_tgba& operator=(const taa_tgba& other) = delete;
72  };
73 
75  class SPOT_API set_state final: public spot::state
76  {
77  public:
78  set_state(const taa_tgba::state_set* s, bool delete_me = false)
79  : s_(s), delete_me_(delete_me)
80  {
81  }
82 
83  virtual int compare(const spot::state*) const override;
84  virtual size_t hash() const override;
85  virtual set_state* clone() const override;
86 
87  virtual ~set_state()
88  {
89  if (delete_me_)
90  delete s_;
91  }
92 
93  const taa_tgba::state_set* get_state() const;
94  private:
95  const taa_tgba::state_set* s_;
96  bool delete_me_;
97  };
98 
99  class SPOT_API taa_succ_iterator final: public twa_succ_iterator
100  {
101  public:
102  taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);
103  virtual ~taa_succ_iterator();
104 
105  virtual bool first() override;
106  virtual bool next() override;
107  virtual bool done() const override;
108 
109  virtual set_state* dst() const override;
110  virtual bdd cond() const override;
111  virtual acc_cond::mark_t acc() const override;
112 
113  private:
116  typedef taa_tgba::state::const_iterator iterator;
117  typedef std::pair<iterator, iterator> iterator_pair;
118  typedef std::vector<iterator_pair> bounds_t;
119  typedef std::unordered_map<const spot::set_state*,
120  std::vector<taa_tgba::transition*>,
121  state_ptr_hash, state_ptr_equal> seen_map;
122 
123  struct distance_sort
124  {
125  bool
126  operator()(const iterator_pair& lhs, const iterator_pair& rhs) const
127  {
128  return std::distance(lhs.first, lhs.second) <
129  std::distance(rhs.first, rhs.second);
130  }
131  };
132 
133  std::vector<taa_tgba::transition*>::const_iterator i_;
134  std::vector<taa_tgba::transition*> succ_;
135  seen_map seen_;
136  const acc_cond& acc_;
137  };
138 
141  template<typename label>
142  class SPOT_API taa_tgba_labelled: public taa_tgba
143  {
144  public:
145  taa_tgba_labelled(const bdd_dict_ptr& dict) : taa_tgba(dict) {};
146 
148  {
149  for (auto i: name_state_map_)
150  {
151  for (auto i2: *i.second)
152  delete i2;
153  delete i.second;
154  }
155  }
156 
157  void set_init_state(const label& s)
158  {
159  std::vector<label> v(1);
160  v[0] = s;
161  set_init_state(v);
162  }
163  void set_init_state(const std::vector<label>& s)
164  {
165  init_ = add_state_set(s);
166  }
167 
168  transition*
169  create_transition(const label& s,
170  const std::vector<label>& d)
171  {
172  state* src = add_state(s);
173  state_set* dst = add_state_set(d);
174  transition* t = new transition;
175  t->dst = dst;
176  t->condition = bddtrue;
177  t->acceptance_conditions = {};
178  src->emplace_back(t);
179  return t;
180  }
181 
182  transition*
183  create_transition(const label& s, const label& d)
184  {
185  std::vector<std::string> vec;
186  vec.emplace_back(d);
187  return create_transition(s, vec);
188  }
189 
190  void add_acceptance_condition(transition* t, formula f)
191  {
192  auto p = acc_map_.emplace(f, acc_cond::mark_t({}));
193  if (p.second)
194  p.first->second = acc_cond::mark_t({acc().add_set()});
195  t->acceptance_conditions |= p.first->second;
196  }
197 
206  virtual std::string format_state(const spot::state* s) const override
207  {
208  const spot::set_state* se = down_cast<const spot::set_state*>(s);
209  const state_set* ss = se->get_state();
210  return format_state_set(ss);
211  }
212 
214  void output(std::ostream& os) const
215  {
216  typename ns_map::const_iterator i;
217  for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
218  {
219  taa_tgba::state::const_iterator i2;
220  os << "State: " << label_to_string(i->first) << std::endl;
221  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
222  {
223  os << ' ' << format_state_set((*i2)->dst)
224  << ", C:" << (*i2)->condition
225  << ", A:" << (*i2)->acceptance_conditions << std::endl;
226  }
227  }
228  }
229 
230  protected:
231  typedef label label_t;
232 
233  typedef std::unordered_map<label, taa_tgba::state*> ns_map;
234  typedef std::unordered_map<const taa_tgba::state*, label,
235  ptr_hash<taa_tgba::state> > sn_map;
236 
237  ns_map name_state_map_;
238  sn_map state_name_map_;
239 
241  virtual std::string label_to_string(const label_t& lbl) const = 0;
242 
243  private:
246  taa_tgba::state* add_state(const label& name)
247  {
248  typename ns_map::iterator i = name_state_map_.find(name);
249  if (i == name_state_map_.end())
250  {
251  taa_tgba::state* s = new taa_tgba::state;
252  name_state_map_[name] = s;
253  state_name_map_[s] = name;
254  return s;
255  }
256  return i->second;
257  }
258 
260  taa_tgba::state_set* add_state_set(const std::vector<label>& names)
261  {
262  state_set* ss = new state_set;
263  for (unsigned i = 0; i < names.size(); ++i)
264  ss->insert(add_state(names[i]));
265  state_set_vec_.emplace_back(ss);
266  return ss;
267  }
268 
269  std::string format_state_set(const taa_tgba::state_set* ss) const
270  {
271  state_set::const_iterator i1 = ss->begin();
272  typename sn_map::const_iterator i2;
273  if (ss->empty())
274  return std::string("{}");
275  if (ss->size() == 1)
276  {
277  i2 = state_name_map_.find(*i1);
278  SPOT_ASSERT(i2 != state_name_map_.end());
279  return "{" + label_to_string(i2->second) + "}";
280  }
281  else
282  {
283  std::string res("{");
284  while (i1 != ss->end())
285  {
286  i2 = state_name_map_.find(*i1++);
287  SPOT_ASSERT(i2 != state_name_map_.end());
288  res += label_to_string(i2->second);
289  res += ",";
290  }
291  res[res.size() - 1] = '}';
292  return res;
293  }
294  }
295  };
296 
297  class SPOT_API taa_tgba_string final:
298 #ifndef SWIG
299  public taa_tgba_labelled<std::string>
300 #else
301  public taa_tgba
302 #endif
303  {
304  public:
305  taa_tgba_string(const bdd_dict_ptr& dict) :
307  ~taa_tgba_string()
308  {}
309  protected:
310  virtual std::string label_to_string(const std::string& label)
311  const override;
312  };
313 
314  typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
315  typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
316 
317  inline taa_tgba_string_ptr make_taa_tgba_string(const bdd_dict_ptr& dict)
318  {
319  return SPOT_make_shared_enabled__(taa_tgba_string, dict);
320  }
321 
322  class SPOT_API taa_tgba_formula final:
323 #ifndef SWIG
324  public taa_tgba_labelled<formula>
325 #else
326  public taa_tgba
327 #endif
328  {
329  public:
330  taa_tgba_formula(const bdd_dict_ptr& dict) :
333  {}
334  protected:
335  virtual std::string label_to_string(const label_t& label)
336  const override;
337  };
338 
339  typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
340  typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
341 
342  inline taa_tgba_formula_ptr make_taa_tgba_formula(const bdd_dict_ptr& dict)
343  {
344  return SPOT_make_shared_enabled__(taa_tgba_formula, dict);
345  }
346 }
An acceptance condition.
Definition: acc.hh:61
Main class for temporal logic formula.
Definition: formula.hh:732
Set of states deriving from spot::state.
Definition: taatgba.hh:76
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:47
Definition: taatgba.hh:100
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:328
virtual std::string label_to_string(const label_t &label) const override
Return a label as a string.
Definition: taatgba.hh:143
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
Definition: taatgba.hh:206
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:214
virtual std::string label_to_string(const label_t &lbl) const =0
Return a label as a string.
Definition: taatgba.hh:303
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:35
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:394
A Transition-based ω-Automaton.
Definition: twa.hh:619
LTL/PSL formula interface.
Definition: automata.hh:26
std::unordered_set< const state *, state_ptr_hash, state_ptr_equal > state_set
Unordered set of abstract states.
Definition: twa.hh:186
An acceptance mark.
Definition: acc.hh:84
A hash function for pointers.
Definition: hash.hh:36
An Equivalence Relation for state*.
Definition: twa.hh:147
Hash Function for state*.
Definition: twa.hh:171
Explicit transitions.
Definition: taatgba.hh:45

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1