spot  2.10.3.dev
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 }
An acceptance condition.
Definition: acc.hh:61
Main class for temporal logic formula.
Definition: formula.hh:715
Set of states deriving from spot::state.
Definition: taatgba.hh:77
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:51
Definition: taatgba.hh:101
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:331
virtual std::string label_to_string(const label_t &label) const override
Return a label as a string.
Definition: taatgba.hh:146
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
Definition: taatgba.hh:209
void output(std::ostream &os) const
Output a TAA in a stream.
Definition: taatgba.hh:217
virtual std::string label_to_string(const label_t &lbl) const =0
Return a label as a string.
Definition: taatgba.hh:306
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:36
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:398
A Transition-based ω-Automaton.
Definition: twa.hh:623
LTL/PSL formula interface.
Definition: automata.hh:27
std::unordered_set< const state *, state_ptr_hash, state_ptr_equal > state_set
Unordered set of abstract states.
Definition: twa.hh:190
An acceptance mark.
Definition: acc.hh:89
A hash function for pointers.
Definition: hash.hh:41
An Equivalence Relation for state*.
Definition: twa.hh:151
Hash Function for state*.
Definition: twa.hh:175
Explicit transitions.
Definition: taatgba.hh:46

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