spot  2.0.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
graph.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
3 // Développement de l'Epita.
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 <spot/misc/common.hh>
23 #include <vector>
24 #include <type_traits>
25 #include <tuple>
26 #include <cassert>
27 #include <iterator>
28 #include <algorithm>
29 #include <iostream>
30 #include <type_traits>
31 
32 namespace spot
33 {
34  template <typename State_Data, typename Edge_Data, bool Alternating = false>
35  class SPOT_API digraph;
36 
37  namespace internal
38  {
39 #ifndef SWIG
40  template <typename Of, typename ...Args>
42  {
43  static const bool value = false;
44  };
45 
46  template <typename Of, typename Arg1, typename ...Args>
47  struct first_is_base_of<Of, Arg1, Args...>
48  {
49  static const bool value =
50  std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
51  };
52 #endif
53 
54  // The boxed_label class stores Data as an attribute called
55  // "label" if boxed is true. It is an empty class if Data is
56  // void, and it simply inherits from Data if boxed is false.
57  //
58  // The data() method offers an homogeneous access to the Data
59  // instance.
60  template <typename Data, bool boxed = !std::is_class<Data>::value>
61  struct SPOT_API boxed_label
62  {
63  typedef Data data_t;
64  Data label;
65 
66 #ifndef SWIG
67  template <typename... Args,
68  typename = typename std::enable_if<
69  !first_is_base_of<boxed_label, Args...>::value>::type>
70  boxed_label(Args&&... args)
71  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
72  : label{std::forward<Args>(args)...}
73  {
74  }
75 #endif
76 
77  // if Data is a POD type, G++ 4.8.2 wants default values for all
78  // label fields unless we define this default constructor here.
79  explicit boxed_label()
80  noexcept(std::is_nothrow_constructible<Data>::value)
81  {
82  }
83 
84  Data& data()
85  {
86  return label;
87  }
88 
89  const Data& data() const
90  {
91  return label;
92  }
93 
94  bool operator<(const boxed_label& other) const
95  {
96  return label < other.label;
97  }
98  };
99 
100  template <>
101  struct SPOT_API boxed_label<void, true>: public std::tuple<>
102  {
103  typedef std::tuple<> data_t;
104  std::tuple<>& data()
105  {
106  return *this;
107  }
108 
109  const std::tuple<>& data() const
110  {
111  return *this;
112  }
113 
114  };
115 
116  template <typename Data>
117  struct SPOT_API boxed_label<Data, false>: public Data
118  {
119  typedef Data data_t;
120 
121 #ifndef SWIG
122  template <typename... Args,
123  typename = typename std::enable_if<
124  !first_is_base_of<boxed_label, Args...>::value>::type>
125  boxed_label(Args&&... args)
126  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
127  : Data{std::forward<Args>(args)...}
128  {
129  }
130 #endif
131 
132  // if Data is a POD type, G++ 4.8.2 wants default values for all
133  // label fields unless we define this default constructor here.
134  explicit boxed_label()
135  noexcept(std::is_nothrow_constructible<Data>::value)
136  {
137  }
138 
139  Data& data()
140  {
141  return *this;
142  }
143 
144  const Data& data() const
145  {
146  return *this;
147  }
148  };
149 
151  // State storage for digraphs
153 
154  // We have two implementations, one with attached State_Data, and
155  // one without.
156 
157  template <typename Edge, typename State_Data>
158  struct SPOT_API distate_storage final: public State_Data
159  {
160  Edge succ = 0; // First outgoing edge (used when iterating)
161  Edge succ_tail = 0; // Last outgoing edge (used for
162  // appending new edges)
163 #ifndef SWIG
164  template <typename... Args,
165  typename = typename std::enable_if<
166  !first_is_base_of<distate_storage, Args...>::value>::type>
167  distate_storage(Args&&... args)
168  noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
169  : State_Data{std::forward<Args>(args)...}
170  {
171  }
172 #endif
173  };
174 
176  // Edge storage
178 
179  // Again two implementation: one with label, and one without.
180 
181  template <typename StateIn,
182  typename StateOut, typename Edge, typename Edge_Data>
183  struct SPOT_API edge_storage final: public Edge_Data
184  {
185  typedef Edge edge;
186 
187  StateOut dst; // destination
188  Edge next_succ; // next outgoing edge with same
189  // source, or 0
190  StateIn src; // source
191 
192  explicit edge_storage()
193  noexcept(std::is_nothrow_constructible<Edge_Data>::value)
194  : Edge_Data{}
195  {
196  }
197 
198 #ifndef SWIG
199  template <typename... Args>
200  edge_storage(StateOut dst, Edge next_succ,
201  StateIn src, Args&&... args)
202  noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
203  && std::is_nothrow_constructible<StateOut, StateOut>::value
204  && std::is_nothrow_constructible<Edge, Edge>::value)
205  : Edge_Data{std::forward<Args>(args)...},
206  dst(dst), next_succ(next_succ), src(src)
207  {
208  }
209 #endif
210 
211  bool operator<(const edge_storage& other) const
212  {
213  if (src < other.src)
214  return true;
215  if (src > other.src)
216  return false;
217  // This might be costly if the destination is a vector
218  if (dst < other.dst)
219  return true;
220  if (dst > other.dst)
221  return false;
222  return this->data() < other.data();
223  }
224 
225  bool operator==(const edge_storage& other) const
226  {
227  return src == other.src &&
228  dst == other.dst &&
229  this->data() == other.data();
230  }
231  };
232 
234  // Edge iterator
236 
237  // This holds a graph and a edge number that is the start of
238  // a list, and it iterates over all the edge_storage_t elements
239  // of that list.
240 
241  template <typename Graph>
242  class SPOT_API edge_iterator: public
243  std::iterator<std::forward_iterator_tag,
244  typename
245  std::conditional<std::is_const<Graph>::value,
246  const typename Graph::edge_storage_t,
247  typename Graph::edge_storage_t>::type>
248  {
249  typedef
250  std::iterator<std::forward_iterator_tag,
251  typename
252  std::conditional<std::is_const<Graph>::value,
253  const typename Graph::edge_storage_t,
254  typename Graph::edge_storage_t>::type>
255  super;
256  public:
257  typedef typename Graph::edge edge;
258 
259  edge_iterator() noexcept
260  : g_(nullptr), t_(0)
261  {
262  }
263 
264  edge_iterator(Graph* g, edge t) noexcept
265  : g_(g), t_(t)
266  {
267  }
268 
269  bool operator==(edge_iterator o) const
270  {
271  return t_ == o.t_;
272  }
273 
274  bool operator!=(edge_iterator o) const
275  {
276  return t_ != o.t_;
277  }
278 
279  typename super::reference
280  operator*()
281  {
282  return g_->edge_storage(t_);
283  }
284 
285  const typename super::reference
286  operator*() const
287  {
288  return g_->edge_storage(t_);
289  }
290 
291  typename super::pointer
292  operator->()
293  {
294  return &g_->edge_storage(t_);
295  }
296 
297  const typename super::pointer
298  operator->() const
299  {
300  return &g_->edge_storage(t_);
301  }
302 
303  edge_iterator operator++()
304  {
305  t_ = operator*().next_succ;
306  return *this;
307  }
308 
309  edge_iterator operator++(int)
310  {
311  edge_iterator ti = *this;
312  t_ = operator*().next_succ;
313  return ti;
314  }
315 
316  operator bool() const
317  {
318  return t_;
319  }
320 
321  edge trans() const
322  {
323  return t_;
324  }
325 
326  protected:
327  Graph* g_;
328  edge t_;
329  };
330 
331  template <typename Graph>
332  class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
333  {
334  typedef edge_iterator<Graph> super;
335  public:
336  typedef typename Graph::state_storage_t state_storage_t;
337  typedef typename Graph::edge edge;
338 
339  killer_edge_iterator(Graph* g, edge t, state_storage_t& src) noexcept
340  : super(g, t), src_(src), prev_(0)
341  {
342  }
343 
344  killer_edge_iterator operator++()
345  {
346  prev_ = this->t_;
347  this->t_ = this->operator*().next_succ;
348  return *this;
349  }
350 
351  killer_edge_iterator operator++(int)
352  {
353  killer_edge_iterator ti = *this;
354  ++*this;
355  return ti;
356  }
357 
358  // Erase the current edge and advance the iterator.
359  void erase()
360  {
361  edge next = this->operator*().next_succ;
362 
363  // Update source state and previous edges
364  if (prev_)
365  {
366  this->g_->edge_storage(prev_).next_succ = next;
367  }
368  else
369  {
370  if (src_.succ == this->t_)
371  src_.succ = next;
372  }
373  if (src_.succ_tail == this->t_)
374  {
375  src_.succ_tail = prev_;
376  assert(next == 0);
377  }
378 
379  // Erased edges have themselves as next_succ.
380  this->operator*().next_succ = this->t_;
381 
382  // Advance iterator to next edge.
383  this->t_ = next;
384 
385  ++this->g_->killed_edge_;
386  }
387 
388  protected:
389  state_storage_t& src_;
390  edge prev_;
391  };
392 
393 
395  // State OUT
397 
398  // Fake container listing the outgoing edges of a state.
399 
400  template <typename Graph>
401  class SPOT_API state_out
402  {
403  public:
404  typedef typename Graph::edge edge;
405  state_out(Graph* g, edge t) noexcept
406  : g_(g), t_(t)
407  {
408  }
409 
410  edge_iterator<Graph> begin()
411  {
412  return {g_, t_};
413  }
414 
416  {
417  return {};
418  }
419 
420  void recycle(edge t)
421  {
422  t_ = t;
423  }
424 
425  protected:
426  Graph* g_;
427  edge t_;
428  };
429 
431  // all_trans
433 
434  template <typename Graph>
435  class SPOT_API all_edge_iterator: public
436  std::iterator<std::forward_iterator_tag,
437  typename
438  std::conditional<std::is_const<Graph>::value,
439  const typename Graph::edge_storage_t,
440  typename Graph::edge_storage_t>::type>
441  {
442  typedef
443  std::iterator<std::forward_iterator_tag,
444  typename
445  std::conditional<std::is_const<Graph>::value,
446  const typename Graph::edge_storage_t,
447  typename Graph::edge_storage_t>::type>
448  super;
449 
450  typedef typename std::conditional<std::is_const<Graph>::value,
451  const typename Graph::edge_vector_t,
452  typename Graph::edge_vector_t>::type
453  tv_t;
454 
455  unsigned t_;
456  tv_t& tv_;
457 
458  void skip_()
459  {
460  unsigned s = tv_.size();
461  do
462  ++t_;
463  while (t_ < s && tv_[t_].next_succ == t_);
464  }
465 
466  public:
467  all_edge_iterator(unsigned pos, tv_t& tv) noexcept
468  : t_(pos), tv_(tv)
469  {
470  skip_();
471  }
472 
473  all_edge_iterator(tv_t& tv) noexcept
474  : t_(tv.size()), tv_(tv)
475  {
476  }
477 
478  all_edge_iterator& operator++()
479  {
480  skip_();
481  return *this;
482  }
483 
484  all_edge_iterator operator++(int)
485  {
486  all_edge_iterator old = *this;
487  ++*this;
488  return old;
489  }
490 
491  bool operator==(all_edge_iterator o) const
492  {
493  return t_ == o.t_;
494  }
495 
496  bool operator!=(all_edge_iterator o) const
497  {
498  return t_ != o.t_;
499  }
500 
501  typename super::reference
502  operator*()
503  {
504  return tv_[t_];
505  }
506 
507  const typename super::reference
508  operator*() const
509  {
510  return tv_[t_];
511  }
512 
513  const typename super::pointer
514  operator->()
515  {
516  return &tv_[t_];
517  }
518 
519  typename super::pointer
520  operator->() const
521  {
522  return &tv_[t_];
523  }
524  };
525 
526 
527  template <typename Graph>
528  class SPOT_API all_trans
529  {
530  public:
531  typedef typename std::conditional<std::is_const<Graph>::value,
532  const typename Graph::edge_vector_t,
533  typename Graph::edge_vector_t>::type
534  tv_t;
536  private:
537  tv_t& tv_;
538  public:
539 
540  all_trans(tv_t& tv) noexcept
541  : tv_(tv)
542  {
543  }
544 
545  iter_t begin()
546  {
547  return {0, tv_};
548  }
549 
550  iter_t end()
551  {
552  return {tv_};
553  }
554  };
555 
556  } // namespace internal
557 
558 
564  template <typename State_Data, typename Edge_Data, bool Alternating>
565  class digraph
566  {
567  friend class internal::edge_iterator<digraph>;
568  friend class internal::edge_iterator<const digraph>;
570 
571  public:
572  typedef internal::edge_iterator<digraph> iterator;
573  typedef internal::edge_iterator<const digraph> const_iterator;
574 
576  static constexpr bool alternating()
577  {
578  return Alternating;
579  }
580 
581  // Extra data to store on each state or edge.
582  typedef State_Data state_data_t;
583  typedef Edge_Data edge_data_t;
584 
585  // State and edges are identified by their indices in some
586  // vector.
587  typedef unsigned state;
588  typedef unsigned edge;
589 
590  // The type of an output state (when seen from a edge)
591  // depends on the kind of graph we build
592  typedef typename std::conditional<Alternating,
593  std::vector<state>,
594  state>::type out_state;
595 
596  typedef internal::distate_storage<edge,
598  state_storage_t;
599  typedef internal::edge_storage<state, out_state, edge,
601  edge_storage_t;
602  typedef std::vector<state_storage_t> state_vector;
603  typedef std::vector<edge_storage_t> edge_vector_t;
604  protected:
605  state_vector states_;
606  edge_vector_t edges_;
607  // Number of erased edges.
608  unsigned killed_edge_;
609  public:
616  digraph(unsigned max_states = 10, unsigned max_trans = 0)
617  : killed_edge_(0)
618  {
619  states_.reserve(max_states);
620  if (max_trans == 0)
621  max_trans = max_states * 2;
622  edges_.reserve(max_trans + 1);
623  // Edge number 0 is not used, because we use this index
624  // to mark the absence of a edge.
625  edges_.resize(1);
626  // This causes edge 0 to be considered as dead.
627  edges_[0].next_succ = 0;
628  }
629 
631  unsigned num_states() const
632  {
633  return states_.size();
634  }
635 
639  unsigned num_edges() const
640  {
641  return edges_.size() - killed_edge_ - 1;
642  }
643 
649  template <typename... Args>
650  state new_state(Args&&... args)
651  {
652  state s = states_.size();
653  states_.emplace_back(std::forward<Args>(args)...);
654  return s;
655  }
656 
663  template <typename... Args>
664  state new_states(unsigned n, Args&&... args)
665  {
666  state s = states_.size();
667  states_.reserve(s + n);
668  while (n--)
669  states_.emplace_back(std::forward<Args>(args)...);
670  return s;
671  }
672 
678  state_storage_t&
679  state_storage(state s)
680  {
681  assert(s < states_.size());
682  return states_[s];
683  }
684 
685  const state_storage_t&
686  state_storage(state s) const
687  {
688  assert(s < states_.size());
689  return states_[s];
690  }
692 
698  typename state_storage_t::data_t&
699  state_data(state s)
700  {
701  assert(s < states_.size());
702  return states_[s].data();
703  }
704 
705  const typename state_storage_t::data_t&
706  state_data(state s) const
707  {
708  assert(s < states_.size());
709  return states_[s].data();
710  }
712 
718  edge_storage_t&
719  edge_storage(edge s)
720  {
721  assert(s < edges_.size());
722  return edges_[s];
723  }
724 
725  const edge_storage_t&
726  edge_storage(edge s) const
727  {
728  assert(s < edges_.size());
729  return edges_[s];
730  }
732 
738  typename edge_storage_t::data_t&
739  edge_data(edge s)
740  {
741  assert(s < edges_.size());
742  return edges_[s].data();
743  }
744 
745  const typename edge_storage_t::data_t&
746  edge_data(edge s) const
747  {
748  assert(s < edges_.size());
749  return edges_[s].data();
750  }
752 
758  template <typename... Args>
759  edge
760  new_edge(state src, out_state dst, Args&&... args)
761  {
762  assert(src < states_.size());
763 
764  edge t = edges_.size();
765  edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
766 
767  edge st = states_[src].succ_tail;
768  assert(st < t || !st);
769  if (!st)
770  states_[src].succ = t;
771  else
772  edges_[st].next_succ = t;
773  states_[src].succ_tail = t;
774  return t;
775  }
776 
778  state index_of_state(const state_storage_t& ss) const
779  {
780  assert(!states_.empty());
781  return &ss - &states_.front();
782  }
783 
785  edge index_of_edge(const edge_storage_t& tt) const
786  {
787  assert(!edges_.empty());
788  return &tt - &edges_.front();
789  }
790 
794  out(state src)
795  {
796  return {this, states_[src].succ};
797  }
798 
800  out(state_storage_t& src)
801  {
802  return out(index_of_state(src));
803  }
804 
806  out(state src) const
807  {
808  return {this, states_[src].succ};
809  }
810 
812  out(state_storage_t& src) const
813  {
814  return out(index_of_state(src));
815  }
817 
823  out_iteraser(state_storage_t& src)
824  {
825  return {this, src.succ, src};
826  }
827 
829  out_iteraser(state src)
830  {
831  return out_iteraser(state_storage(src));
832  }
834 
838  const state_vector& states() const
839  {
840  return states_;
841  }
842 
843  state_vector& states()
844  {
845  return states_;
846  }
848 
854  {
855  return edges_;
856  }
857 
859  {
860  return edges_;
861  }
863 
872  const edge_vector_t& edge_vector() const
873  {
874  return edges_;
875  }
876 
877  edge_vector_t& edge_vector()
878  {
879  return edges_;
880  }
882 
889  bool is_valid_edge(edge t) const
890  {
891  // Erased edges have their next_succ pointing to
892  // themselves.
893  return (t < edges_.size() &&
894  edges_[t].next_succ != t);
895  }
896 
901  bool is_dead_edge(unsigned t) const
902  {
903  return edges_[t].next_succ == t;
904  }
905 
906  bool is_dead_edge(const edge_storage_t& t) const
907  {
908  return t.next_succ == index_of_edge(t);
909  }
911 
912 
914  void dump_storage(std::ostream& o) const
915  {
916  unsigned tend = edges_.size();
917  for (unsigned t = 1; t < tend; ++t)
918  {
919  o << 't' << t << ": (s"
920  << edges_[t].src << ", s"
921  << edges_[t].dst << ") t"
922  << edges_[t].next_succ << '\n';
923  }
924  unsigned send = states_.size();
925  for (unsigned s = 0; s < send; ++s)
926  {
927  o << 's' << s << ": t"
928  << states_[s].succ << " t"
929  << states_[s].succ_tail << '\n';
930  }
931  }
932 
939  {
940  if (killed_edge_ == 0)
941  return;
942  auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
943  [this](const edge_storage_t& t) {
944  return this->is_dead_edge(t);
945  });
946  edges_.erase(i, edges_.end());
947  killed_edge_ = 0;
948  }
949 
955  template<class Predicate = std::less<edge_storage_t>>
956  void sort_edges_(Predicate p = Predicate())
957  {
958  //std::cerr << "\nbefore\n";
959  //dump_storage(std::cerr);
960  std::stable_sort(edges_.begin() + 1, edges_.end(), p);
961  }
962 
968  {
969  state last_src = -1U;
970  edge tend = edges_.size();
971  for (edge t = 1; t < tend; ++t)
972  {
973  state src = edges_[t].src;
974  if (src != last_src)
975  {
976  states_[src].succ = t;
977  if (last_src != -1U)
978  {
979  states_[last_src].succ_tail = t - 1;
980  edges_[t - 1].next_succ = 0;
981  }
982  while (++last_src != src)
983  {
984  states_[last_src].succ = 0;
985  states_[last_src].succ_tail = 0;
986  }
987  }
988  else
989  {
990  edges_[t - 1].next_succ = t;
991  }
992  }
993  if (last_src != -1U)
994  {
995  states_[last_src].succ_tail = tend - 1;
996  edges_[tend - 1].next_succ = 0;
997  }
998  unsigned send = states_.size();
999  while (++last_src != send)
1000  {
1001  states_[last_src].succ = 0;
1002  states_[last_src].succ_tail = 0;
1003  }
1004  //std::cerr << "\nafter\n";
1005  //dump_storage(std::cerr);
1006  }
1007 
1013  void rename_states_(const std::vector<unsigned>& newst)
1014  {
1015  assert(newst.size() == states_.size());
1016  unsigned tend = edges_.size();
1017  for (unsigned t = 1; t < tend; t++)
1018  {
1019  edges_[t].dst = newst[edges_[t].dst];
1020  edges_[t].src = newst[edges_[t].src];
1021  }
1022  }
1023 
1029  void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
1030  {
1031  assert(newst.size() == states_.size());
1032  assert(used_states > 0);
1033 
1034  //std::cerr << "\nbefore defrag\n";
1035  //dump_storage(std::cerr);
1036 
1037  // Shift all states in states_, as indicated by newst.
1038  unsigned send = states_.size();
1039  for (state s = 0; s < send; ++s)
1040  {
1041  state dst = newst[s];
1042  if (dst == s)
1043  continue;
1044  if (dst == -1U)
1045  {
1046  // This is an erased state. Mark all its edges as
1047  // dead (i.e., t.next_succ should point to t for each of
1048  // them).
1049  auto t = states_[s].succ;
1050  while (t)
1051  std::swap(t, edges_[t].next_succ);
1052  continue;
1053  }
1054  states_[dst] = std::move(states_[s]);
1055  }
1056  states_.resize(used_states);
1057 
1058  // Shift all edges in edges_. The algorithm is
1059  // similar to remove_if, but it also keeps the correspondence
1060  // between the old and new index as newidx[old] = new.
1061  unsigned tend = edges_.size();
1062  std::vector<edge> newidx(tend);
1063  unsigned dest = 1;
1064  for (edge t = 1; t < tend; ++t)
1065  {
1066  if (is_dead_edge(t))
1067  continue;
1068  if (t != dest)
1069  edges_[dest] = std::move(edges_[t]);
1070  newidx[t] = dest;
1071  ++dest;
1072  }
1073  edges_.resize(dest);
1074  killed_edge_ = 0;
1075 
1076  // Adjust next_succ and dst pointers in all edges.
1077  for (edge t = 1; t < dest; ++t)
1078  {
1079  auto& tr = edges_[t];
1080  tr.next_succ = newidx[tr.next_succ];
1081  tr.dst = newst[tr.dst];
1082  tr.src = newst[tr.src];
1083  assert(tr.dst != -1U);
1084  }
1085 
1086  // Adjust succ and succ_tails pointers in all states.
1087  for (auto& s: states_)
1088  {
1089  s.succ = newidx[s.succ];
1090  s.succ_tail = newidx[s.succ_tail];
1091  }
1092 
1093  //std::cerr << "\nafter defrag\n";
1094  //dump_storage(std::cerr);
1095  }
1096  };
1097 }
const edge_storage_t::data_t & edge_data(edge s) const
return the Edgeg_Data of an edge.
Definition: graph.hh:746
Definition: graph.hh:32
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:639
Definition: graph.hh:61
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:906
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:719
edge_storage_t::data_t & edge_data(edge s)
return the Edgeg_Data of an edge.
Definition: graph.hh:739
state new_state(Args &&...args)
Create a new states.
Definition: graph.hh:650
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:631
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:938
Definition: graph.hh:242
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:686
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:812
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:794
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:967
Abstract class for states.
Definition: twa.hh:43
Definition: graph.hh:183
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:838
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:901
Definition: graph.hh:158
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:800
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:778
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:806
Definition: graph.hh:528
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:872
Definition: graph.hh:41
edge index_of_edge(const edge_storage_t &tt) const
Conveart a storage reference into an edge number.
Definition: graph.hh:785
state_vector & states()
Return the vector of states.
Definition: graph.hh:843
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:858
state new_states(unsigned n, Args &&...args)
Create n new states.
Definition: graph.hh:664
void defrag_states(std::vector< unsigned > &&newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1029
Definition: graph.hh:435
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:853
static constexpr bool alternating()
Whether the automaton is alternating.
Definition: graph.hh:576
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:877
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:889
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:706
edge new_edge(state src, out_state dst, Args &&...args)
Create a new edge.
Definition: graph.hh:760
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:616
A directed graph.
Definition: graph.hh:35
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:829
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:679
Definition: graph.hh:401
void sort_edges_(Predicate p=Predicate())
Sort all edge according to a predicate.
Definition: graph.hh:956
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1013
internal::killer_edge_iterator< digraph > out_iteraser(state_storage_t &src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:823
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:914
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:699
Definition: graph.hh:332
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:726

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Jul 11 2016 09:54:34 for spot by doxygen 1.8.8