spot  2.8.3
taatgba.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et Développement de
3 // 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 = {};
181  src->emplace_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.emplace_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, acc_cond::mark_t({}));
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  const state_set* ss = se->get_state();
213  return format_state_set(ss);
214  }
215 
217  void output(std::ostream& os) const
218  {
219  typename ns_map::const_iterator i;
220  for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
221  {
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)
225  {
226  os << ' ' << format_state_set((*i2)->dst)
227  << ", C:" << (*i2)->condition
228  << ", A:" << (*i2)->acceptance_conditions << std::endl;
229  }
230  }
231  }
232 
233  protected:
234  typedef label label_t;
235 
236  typedef std::unordered_map<label, taa_tgba::state*> ns_map;
237  typedef std::unordered_map<const taa_tgba::state*, label,
238  ptr_hash<taa_tgba::state> > sn_map;
239 
240  ns_map name_state_map_;
241  sn_map state_name_map_;
242 
244  virtual std::string label_to_string(const label_t& lbl) const = 0;
245 
246  private:
249  taa_tgba::state* add_state(const label& name)
250  {
251  typename ns_map::iterator i = name_state_map_.find(name);
252  if (i == name_state_map_.end())
253  {
254  taa_tgba::state* s = new taa_tgba::state;
255  name_state_map_[name] = s;
256  state_name_map_[s] = name;
257  return s;
258  }
259  return i->second;
260  }
261 
263  taa_tgba::state_set* add_state_set(const std::vector<label>& names)
264  {
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);
269  return ss;
270  }
271 
272  std::string format_state_set(const taa_tgba::state_set* ss) const
273  {
274  state_set::const_iterator i1 = ss->begin();
275  typename sn_map::const_iterator i2;
276  if (ss->empty())
277  return std::string("{}");
278  if (ss->size() == 1)
279  {
280  i2 = state_name_map_.find(*i1);
281  SPOT_ASSERT(i2 != state_name_map_.end());
282  return "{" + label_to_string(i2->second) + "}";
283  }
284  else
285  {
286  std::string res("{");
287  while (i1 != ss->end())
288  {
289  i2 = state_name_map_.find(*i1++);
290  SPOT_ASSERT(i2 != state_name_map_.end());
291  res += label_to_string(i2->second);
292  res += ",";
293  }
294  res[res.size() - 1] = '}';
295  return res;
296  }
297  }
298  };
299 
300  class SPOT_API taa_tgba_string final:
301 #ifndef SWIG
302  public taa_tgba_labelled<std::string>
303 #else
304  public taa_tgba
305 #endif
306  {
307  public:
308  taa_tgba_string(const bdd_dict_ptr& dict) :
310  ~taa_tgba_string()
311  {}
312  protected:
313  virtual std::string label_to_string(const std::string& label)
314  const override;
315  };
316 
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;
319 
320  inline taa_tgba_string_ptr make_taa_tgba_string(const bdd_dict_ptr& dict)
321  {
322  return SPOT_make_shared_enabled__(taa_tgba_string, dict);
323  }
324 
325  class SPOT_API taa_tgba_formula final:
326 #ifndef SWIG
327  public taa_tgba_labelled<formula>
328 #else
329  public taa_tgba
330 #endif
331  {
332  public:
333  taa_tgba_formula(const bdd_dict_ptr& dict) :
336  {}
337  protected:
338  virtual std::string label_to_string(const label_t& label)
339  const override;
340  };
341 
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;
344 
345  inline taa_tgba_formula_ptr make_taa_tgba_formula(const bdd_dict_ptr& dict)
346  {
347  return SPOT_make_shared_enabled__(taa_tgba_formula, dict);
348  }
349 }
Definition: automata.hh:26
An Equivalence Relation for state*.
Definition: twa.hh:150
A Transition-based ω-Automaton.
Definition: twa.hh:622
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
Abstract class for states.
Definition: twa.hh:50
A hash function for pointers.
Definition: hash.hh:38
Main class for temporal logic formula.
Definition: formula.hh:686
Explicit transitions.
Definition: taatgba.hh:45
Definition: taatgba.hh:325
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

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.8.13