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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8