spot  2.12
graph.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 <spot/misc/common.hh>
22 #include <spot/misc/_config.h>
23 #include <vector>
24 #include <type_traits>
25 #include <tuple>
26 #include <cassert>
27 #include <iterator>
28 #include <algorithm>
29 #include <map>
30 #include <iostream>
31 #ifdef SPOT_ENABLE_PTHREAD
32 # include <thread>
33 #endif // SPOT_ENABLE_PTHREAD
34 
35 namespace spot
36 {
37  template <typename State_Data, typename Edge_Data>
38  class SPOT_API digraph;
39 
40  namespace internal
41  {
42 #ifndef SWIG
43  template <typename Of, typename ...Args>
45  {
46  static const bool value = false;
47  };
48 
49  template <typename Of, typename Arg1, typename ...Args>
50  struct first_is_base_of<Of, Arg1, Args...>
51  {
52  static const bool value =
53  std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
54  };
55 #endif
56 
57  // The boxed_label class stores Data as an attribute called
58  // "label" if boxed is true. It is an empty class if Data is
59  // void, and it simply inherits from Data if boxed is false.
60  //
61  // The data() method offers an homogeneous access to the Data
62  // instance.
63  template <typename Data, bool boxed = !std::is_class<Data>::value>
64  struct SPOT_API boxed_label
65  {
66  typedef Data data_t;
67  Data label;
68 
69 #ifndef SWIG
70  template <typename... Args,
71  typename = typename std::enable_if<
72  !first_is_base_of<boxed_label, Args...>::value>::type>
73  boxed_label(Args&&... args)
74  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
75  : label{std::forward<Args>(args)...}
76  {
77  }
78 #endif
79 
80  // if Data is a POD type, G++ 4.8.2 wants default values for all
81  // label fields unless we define this default constructor here.
82  explicit boxed_label()
83  noexcept(std::is_nothrow_constructible<Data>::value)
84  {
85  }
86 
87  Data& data()
88  {
89  return label;
90  }
91 
92  const Data& data() const
93  {
94  return label;
95  }
96 
97  bool operator<(const boxed_label& other) const
98  {
99  return label < other.label;
100  }
101  };
102 
103  template <>
104  struct SPOT_API boxed_label<void, true>: public std::tuple<>
105  {
106  typedef std::tuple<> data_t;
107  std::tuple<>& data()
108  {
109  return *this;
110  }
111 
112  const std::tuple<>& data() const
113  {
114  return *this;
115  }
116 
117  };
118 
119  template <typename Data>
120  struct SPOT_API boxed_label<Data, false>: public Data
121  {
122  typedef Data data_t;
123 
124 #ifndef SWIG
125  template <typename... Args,
126  typename = typename std::enable_if<
127  !first_is_base_of<boxed_label, Args...>::value>::type>
128  boxed_label(Args&&... args)
129  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
130  : Data{std::forward<Args>(args)...}
131  {
132  }
133 #endif
134 
135  // if Data is a POD type, G++ 4.8.2 wants default values for all
136  // label fields unless we define this default constructor here.
137  explicit boxed_label()
138  noexcept(std::is_nothrow_constructible<Data>::value)
139  {
140  }
141 
142  Data& data()
143  {
144  return *this;
145  }
146 
147  const Data& data() const
148  {
149  return *this;
150  }
151  };
152 
154  // State storage for digraphs
156 
157  // We have two implementations, one with attached State_Data, and
158  // one without.
159 
160  template <typename Edge, typename State_Data>
161  struct SPOT_API distate_storage final: public State_Data
162  {
163  Edge succ = 0; // First outgoing edge (used when iterating)
164  Edge succ_tail = 0; // Last outgoing edge (used for
165  // appending new edges)
166 #ifndef SWIG
167  template <typename... Args,
168  typename = typename std::enable_if<
169  !first_is_base_of<distate_storage, Args...>::value>::type>
170  distate_storage(Args&&... args)
171  noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
172  : State_Data{std::forward<Args>(args)...}
173  {
174  }
175 #endif
176  };
177 
179  // Edge storage
181 
182  // Again two implementation: one with label, and one without.
183 
184  template <typename StateIn,
185  typename StateOut, typename Edge, typename Edge_Data>
186  struct SPOT_API edge_storage final: public Edge_Data
187  {
188  typedef Edge edge;
189 
190  StateOut dst; // destination
191  Edge next_succ; // next outgoing edge with same
192  // source, or 0
193  StateIn src; // source
194 
195  explicit edge_storage()
196  noexcept(std::is_nothrow_constructible<Edge_Data>::value)
197  : Edge_Data{}
198  {
199  }
200 
201 #ifndef SWIG
202  template <typename... Args>
203  edge_storage(StateOut dst, Edge next_succ,
204  StateIn src, Args&&... args)
205  noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
206  && std::is_nothrow_constructible<StateOut, StateOut>::value
207  && std::is_nothrow_constructible<Edge, Edge>::value)
208  : Edge_Data{std::forward<Args>(args)...},
209  dst(dst), next_succ(next_succ), src(src)
210  {
211  }
212 #endif
213 
214  bool operator<(const edge_storage& other) const
215  {
216  if (src < other.src)
217  return true;
218  if (src > other.src)
219  return false;
220  // This might be costly if the destination is a vector
221  if (dst < other.dst)
222  return true;
223  if (dst > other.dst)
224  return false;
225  return this->data() < other.data();
226  }
227 
228  bool operator==(const edge_storage& other) const
229  {
230  return src == other.src &&
231  dst == other.dst &&
232  this->data() == other.data();
233  }
234  };
235 
237  // Edge iterator
239 
240  // This holds a graph and a edge number that is the start of
241  // a list, and it iterates over all the edge_storage_t elements
242  // of that list.
243 
244  template <typename Graph>
245  class SPOT_API edge_iterator
246  {
247  public:
248  typedef typename std::conditional<std::is_const<Graph>::value,
249  const typename Graph::edge_storage_t,
250  typename Graph::edge_storage_t>::type
251  value_type;
252  typedef value_type& reference;
253  typedef value_type* pointer;
254  typedef std::ptrdiff_t difference_type;
255  typedef std::forward_iterator_tag iterator_category;
256 
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  reference operator*() const
280  {
281  return g_->edge_storage(t_);
282  }
283 
284  pointer operator->() const
285  {
286  return &g_->edge_storage(t_);
287  }
288 
289  edge_iterator operator++()
290  {
291  t_ = operator*().next_succ;
292  return *this;
293  }
294 
295  edge_iterator operator++(int)
296  {
297  edge_iterator ti = *this;
298  t_ = operator*().next_succ;
299  return ti;
300  }
301 
302  operator bool() const
303  {
304  return t_;
305  }
306 
307  edge trans() const
308  {
309  return t_;
310  }
311 
312  protected:
313  Graph* g_;
314  edge t_;
315  };
316 
317  template <typename Graph>
318  class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
319  {
320  typedef edge_iterator<Graph> super;
321  public:
322  typedef typename Graph::state_storage_t state_storage_t;
323  typedef typename Graph::edge edge;
324 
325  killer_edge_iterator(Graph* g, edge t, state_storage_t& src) noexcept
326  : super(g, t), src_(src), prev_(0)
327  {
328  }
329 
330  killer_edge_iterator operator++()
331  {
332  prev_ = this->t_;
333  this->t_ = this->operator*().next_succ;
334  return *this;
335  }
336 
337  killer_edge_iterator operator++(int)
338  {
339  killer_edge_iterator ti = *this;
340  ++*this;
341  return ti;
342  }
343 
344  // Erase the current edge and advance the iterator.
345  void erase()
346  {
347  edge next = this->operator*().next_succ;
348 
349  // Update source state and previous edges
350  if (prev_)
351  {
352  this->g_->edge_storage(prev_).next_succ = next;
353  }
354  else
355  {
356  if (src_.succ == this->t_)
357  src_.succ = next;
358  }
359  if (src_.succ_tail == this->t_)
360  {
361  src_.succ_tail = prev_;
362  SPOT_ASSERT(next == 0);
363  }
364 
365  // Erased edges have themselves as next_succ.
366  this->operator*().next_succ = this->t_;
367 
368  // Advance iterator to next edge.
369  this->t_ = next;
370 
371  ++this->g_->killed_edge_;
372  }
373 
374  protected:
375  state_storage_t& src_;
376  edge prev_;
377  };
378 
379 
381  // State OUT
383 
384  // Fake container listing the outgoing edges of a state.
385 
386  template <typename Graph>
387  class SPOT_API state_out
388  {
389  public:
390  typedef typename Graph::edge edge;
391  state_out(Graph* g, edge t) noexcept
392  : g_(g), t_(t)
393  {
394  }
395 
396  edge_iterator<Graph> begin() const
397  {
398  return {g_, t_};
399  }
400 
401  edge_iterator<Graph> end() const
402  {
403  return {};
404  }
405 
406  void recycle(edge t)
407  {
408  t_ = t;
409  }
410 
411  protected:
412  Graph* g_;
413  edge t_;
414  };
415 
417  // all_trans
419 
420  template <typename Graph>
421  class SPOT_API all_edge_iterator
422  {
423  public:
424  typedef typename std::conditional<std::is_const<Graph>::value,
425  const typename Graph::edge_storage_t,
426  typename Graph::edge_storage_t>::type
427  value_type;
428  typedef value_type& reference;
429  typedef value_type* pointer;
430  typedef std::ptrdiff_t difference_type;
431  typedef std::forward_iterator_tag iterator_category;
432 
433  protected:
434  typedef typename std::conditional<std::is_const<Graph>::value,
435  const typename Graph::edge_vector_t,
436  typename Graph::edge_vector_t>::type
437  tv_t;
438 
439  unsigned t_;
440  tv_t& tv_;
441 
442  void skip_()
443  {
444  unsigned s = tv_.size();
445  do
446  ++t_;
447  while (t_ < s && tv_[t_].next_succ == t_);
448  }
449 
450  public:
451  all_edge_iterator(unsigned pos, tv_t& tv) noexcept
452  : t_(pos), tv_(tv)
453  {
454  skip_();
455  }
456 
457  all_edge_iterator(tv_t& tv) noexcept
458  : t_(tv.size()), tv_(tv)
459  {
460  }
461 
462  all_edge_iterator& operator++()
463  {
464  skip_();
465  return *this;
466  }
467 
468  all_edge_iterator operator++(int)
469  {
470  all_edge_iterator old = *this;
471  ++*this;
472  return old;
473  }
474 
475  bool operator==(all_edge_iterator o) const
476  {
477  return t_ == o.t_;
478  }
479 
480  bool operator!=(all_edge_iterator o) const
481  {
482  return t_ != o.t_;
483  }
484 
485  reference operator*() const
486  {
487  return tv_[t_];
488  }
489 
490  pointer operator->() const
491  {
492  return &tv_[t_];
493  }
494  };
495 
496 
497  template <typename Graph>
498  class SPOT_API all_trans
499  {
500  public:
501  typedef typename std::conditional<std::is_const<Graph>::value,
502  const typename Graph::edge_vector_t,
503  typename Graph::edge_vector_t>::type
504  tv_t;
506  private:
507  tv_t& tv_;
508  public:
509 
510  all_trans(tv_t& tv) noexcept
511  : tv_(tv)
512  {
513  }
514 
515  iter_t begin() const
516  {
517  return {0, tv_};
518  }
519 
520  iter_t end() const
521  {
522  return {tv_};
523  }
524  };
525 
526  class SPOT_API const_universal_dests
527  {
528  private:
529  const unsigned* begin_;
530  const unsigned* end_;
531  unsigned tmp_;
532  public:
533  const_universal_dests(const unsigned* begin, const unsigned* end) noexcept
534  : begin_(begin), end_(end)
535  {
536  }
537 
538  const_universal_dests(unsigned state) noexcept
539  : begin_(&tmp_), end_(&tmp_ + 1), tmp_(state)
540  {
541  }
542 
543  const unsigned* begin() const
544  {
545  return begin_;
546  }
547 
548  const unsigned* end() const
549  {
550  return end_;
551  }
552  };
553 
554  template<class G>
556  {
557  std::map<std::vector<unsigned>, unsigned> uniq_;
558  G& g_;
559  public:
560 
561  univ_dest_mapper(G& graph)
562  : g_(graph)
563  {
564  }
565 
566  template<class I>
567  unsigned new_univ_dests(I begin, I end)
568  {
569  std::vector<unsigned> tmp(begin, end);
570  std::sort(tmp.begin(), tmp.end());
571  tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
572  auto p = uniq_.emplace(tmp, 0);
573  if (p.second)
574  p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
575  return p.first->second;
576  }
577 
578  unsigned new_univ_dests(std::vector<unsigned>&& tmp)
579  {
580  std::sort(tmp.begin(), tmp.end());
581  tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
582  auto p = uniq_.emplace(tmp, 0);
583  if (p.second)
584  p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
585  return p.first->second;
586  }
587  };
588 
589  } // namespace internal
590 
591 
596  template <typename State_Data, typename Edge_Data>
597  class digraph
598  {
599  friend class internal::edge_iterator<digraph>;
600  friend class internal::edge_iterator<const digraph>;
602 
603  public:
606 
607  // Extra data to store on each state or edge.
608  typedef State_Data state_data_t;
609  typedef Edge_Data edge_data_t;
610 
611  // State and edges are identified by their indices in some
612  // vector.
613  typedef unsigned state;
614  typedef unsigned edge;
615 
616  typedef internal::distate_storage<edge,
619  typedef internal::edge_storage<state, state, edge,
622  typedef std::vector<state_storage_t> state_vector;
623  typedef std::vector<edge_storage_t> edge_vector_t;
624 
625  // A sequence of universal destination groups of the form:
626  // (n state_1 state_2 ... state_n)*
627  typedef std::vector<unsigned> dests_vector_t;
628 
629  protected:
630  state_vector states_;
631  edge_vector_t edges_;
632  dests_vector_t dests_; // Only used by alternating automata.
633  // Number of erased edges.
634  unsigned killed_edge_;
635  public:
642  digraph(unsigned max_states = 10, unsigned max_trans = 0)
643  : killed_edge_(0)
644  {
645  states_.reserve(max_states);
646  if (max_trans == 0)
647  max_trans = max_states * 2;
648  edges_.reserve(max_trans + 1);
649  // Edge number 0 is not used, because we use this index
650  // to mark the absence of a edge.
651  edges_.resize(1);
652  // This causes edge 0 to be considered as dead.
653  edges_[0].next_succ = 0;
654  }
655 
657  unsigned num_states() const
658  {
659  return states_.size();
660  }
661 
665  unsigned num_edges() const
666  {
667  return edges_.size() - killed_edge_ - 1;
668  }
669 
671  bool is_existential() const
672  {
673  return dests_.empty();
674  }
675 
681  template <typename... Args>
682  state new_state(Args&&... args)
683  {
684  state s = states_.size();
685  states_.emplace_back(std::forward<Args>(args)...);
686  return s;
687  }
688 
695  template <typename... Args>
696  state new_states(unsigned n, Args&&... args)
697  {
698  state s = states_.size();
699  states_.reserve(s + n);
700  while (n--)
701  states_.emplace_back(std::forward<Args>(args)...);
702  return s;
703  }
704 
710  state_storage_t&
711  state_storage(state s)
712  {
713  return states_[s];
714  }
715 
716  const state_storage_t&
717  state_storage(state s) const
718  {
719  return states_[s];
720  }
722 
728  typename state_storage_t::data_t&
729  state_data(state s)
730  {
731  return states_[s].data();
732  }
733 
734  const typename state_storage_t::data_t&
735  state_data(state s) const
736  {
737  return states_[s].data();
738  }
740 
746  edge_storage_t&
747  edge_storage(edge s)
748  {
749  return edges_[s];
750  }
751 
752  const edge_storage_t&
753  edge_storage(edge s) const
754  {
755  return edges_[s];
756  }
758 
764  typename edge_storage_t::data_t&
765  edge_data(edge s)
766  {
767  return edges_[s].data();
768  }
769 
770  const typename edge_storage_t::data_t&
771  edge_data(edge s) const
772  {
773  return edges_[s].data();
774  }
776 
782  template <typename... Args>
783  edge
784  new_edge(state src, state dst, Args&&... args)
785  {
786  edge t = edges_.size();
787  edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
788 
789  edge st = states_[src].succ_tail;
790  SPOT_ASSERT(st < t || !st);
791  if (!st)
792  states_[src].succ = t;
793  else
794  edges_[st].next_succ = t;
795  states_[src].succ_tail = t;
796  return t;
797  }
798 
806  template <typename I>
807  state
808  new_univ_dests(I dst_begin, I dst_end)
809  {
810  unsigned sz = std::distance(dst_begin, dst_end);
811  if (sz == 1)
812  return *dst_begin;
813  SPOT_ASSERT(sz > 1);
814  unsigned d = dests_.size();
815  if (!dests_.empty()
816  && &*dst_begin >= &dests_.front()
817  && &*dst_begin <= &dests_.back()
818  && (dests_.capacity() - dests_.size()) < (sz + 1))
819  {
820  // If dst_begin...dst_end points into dests_ and dests_ risk
821  // being reallocated, we have to save the destination
822  // states before we lose them.
823  std::vector<unsigned> tmp(dst_begin, dst_end);
824  dests_.emplace_back(sz);
825  dests_.insert(dests_.end(), tmp.begin(), tmp.end());
826  }
827  else
828  {
829  dests_.emplace_back(sz);
830  dests_.insert(dests_.end(), dst_begin, dst_end);
831  }
832  return ~d;
833  }
834 
841  template <typename I, typename... Args>
842  edge
843  new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args)
844  {
845  return new_edge(src, new_univ_dests(dst_begin, dst_end),
846  std::forward<Args>(args)...);
847  }
848 
854  template <typename... Args>
855  edge
856  new_univ_edge(state src, const std::initializer_list<state>& dsts,
857  Args&&... args)
858  {
859  return new_univ_edge(src, dsts.begin(), dsts.end(),
860  std::forward<Args>(args)...);
861  }
862 
863  internal::const_universal_dests univ_dests(state src) const
864  {
865  if ((int)src < 0)
866  {
867  unsigned pos = ~src;
868  const unsigned* d = dests_.data();
869  d += pos;
870  unsigned num = *d;
871  return { d + 1, d + num + 1 };
872  }
873  else
874  {
875  return src;
876  }
877  }
878 
879  internal::const_universal_dests univ_dests(const edge_storage_t& e) const
880  {
881  return univ_dests(e.dst);
882  }
883 
885  state index_of_state(const state_storage_t& ss) const
886  {
887  SPOT_ASSERT(!states_.empty());
888  return &ss - &states_.front();
889  }
890 
892  edge index_of_edge(const edge_storage_t& tt) const
893  {
894  SPOT_ASSERT(!edges_.empty());
895  return &tt - &edges_.front();
896  }
897 
901  out(state src)
902  {
903  return {this, states_[src].succ};
904  }
905 
908  {
909  return out(index_of_state(src));
910  }
911 
913  out(state src) const
914  {
915  return {this, states_[src].succ};
916  }
917 
919  out(state_storage_t& src) const
920  {
921  return out(index_of_state(src));
922  }
924 
931  {
932  return {this, src.succ, src};
933  }
934 
936  out_iteraser(state src)
937  {
938  return out_iteraser(state_storage(src));
939  }
941 
945  const state_vector& states() const
946  {
947  return states_;
948  }
949 
950  state_vector& states()
951  {
952  return states_;
953  }
955 
961  {
962  return edges_;
963  }
964 
966  {
967  return edges_;
968  }
970 
979  const edge_vector_t& edge_vector() const
980  {
981  return edges_;
982  }
983 
984  edge_vector_t& edge_vector()
985  {
986  return edges_;
987  }
989 
996  bool is_valid_edge(edge t) const
997  {
998  // Erased edges have their next_succ pointing to
999  // themselves.
1000  return (t < edges_.size() &&
1001  edges_[t].next_succ != t);
1002  }
1003 
1008  bool is_dead_edge(unsigned t) const
1009  {
1010  return edges_[t].next_succ == t;
1011  }
1012 
1013  bool is_dead_edge(const edge_storage_t& t) const
1014  {
1015  return t.next_succ == index_of_edge(t);
1016  }
1018 
1024  const dests_vector_t& dests_vector() const
1025  {
1026  return dests_;
1027  }
1028 
1029  dests_vector_t& dests_vector()
1030  {
1031  return dests_;
1032  }
1034 
1036  void dump_storage(std::ostream& o) const
1037  {
1038  unsigned tend = edges_.size();
1039  for (unsigned t = 1; t < tend; ++t)
1040  {
1041  o << 't' << t << ": (s"
1042  << edges_[t].src << ", ";
1043  int d = edges_[t].dst;
1044  if (d < 0)
1045  o << 'd' << ~d;
1046  else
1047  o << 's' << d;
1048  o << ") t" << edges_[t].next_succ << '\n';
1049  }
1050  unsigned send = states_.size();
1051  for (unsigned s = 0; s < send; ++s)
1052  {
1053  o << 's' << s << ": t"
1054  << states_[s].succ << " t"
1055  << states_[s].succ_tail << '\n';
1056  }
1057  unsigned dend = dests_.size();
1058  unsigned size = 0;
1059  for (unsigned s = 0; s < dend; ++s)
1060  {
1061  o << 'd' << s << ": ";
1062  if (size == 0)
1063  {
1064  o << '#';
1065  size = dests_[s];
1066  }
1067  else
1068  {
1069  o << 's';
1070  --size;
1071  }
1072  o << dests_[s] << '\n';
1073  }
1074  }
1075 
1076  enum dump_storage_items {
1077  DSI_GraphHeader = 1,
1078  DSI_GraphFooter = 2,
1079  DSI_StatesHeader = 4,
1080  DSI_StatesBody = 8,
1081  DSI_StatesFooter = 16,
1082  DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1083  DSI_EdgesHeader = 32,
1084  DSI_EdgesBody = 64,
1085  DSI_EdgesFooter = 128,
1086  DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1087  DSI_DestsHeader = 256,
1088  DSI_DestsBody = 512,
1089  DSI_DestsFooter = 1024,
1090  DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1091  DSI_All =
1092  DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1093  };
1094 
1096  void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const
1097  {
1098  if (dsi & DSI_GraphHeader)
1099  o << "digraph g { \nnode [shape=plaintext]\n";
1100  unsigned send = states_.size();
1101  if (dsi & DSI_StatesHeader)
1102  {
1103  o << ("states [label=<\n"
1104  "<table border='0' cellborder='1' cellspacing='0'>\n"
1105  "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1106  for (unsigned s = 0; s < send; ++s)
1107  o << "<td sides='b' bgcolor='yellow' port='s" << s << "'>"
1108  << s << "</td>\n";
1109  o << "</tr>\n";
1110  }
1111  if (dsi & DSI_StatesBody)
1112  {
1113  o << "<tr><td port='ss'>succ</td>\n";
1114  for (unsigned s = 0; s < send; ++s)
1115  {
1116  o << "<td port='ss" << s;
1117  if (states_[s].succ)
1118  o << "' bgcolor='cyan";
1119  o << "'>" << states_[s].succ << "</td>\n";
1120  }
1121  o << "</tr><tr><td port='st'>succ_tail</td>\n";
1122  for (unsigned s = 0; s < send; ++s)
1123  {
1124  o << "<td port='st" << s;
1125  if (states_[s].succ_tail)
1126  o << "' bgcolor='cyan";
1127  o << "'>" << states_[s].succ_tail << "</td>\n";
1128  }
1129  o << "</tr>\n";
1130  }
1131  if (dsi & DSI_StatesFooter)
1132  o << "</table>>]\n";
1133  unsigned eend = edges_.size();
1134  if (dsi & DSI_EdgesHeader)
1135  {
1136  o << ("edges [label=<\n"
1137  "<table border='0' cellborder='1' cellspacing='0'>\n"
1138  "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1139  for (unsigned e = 1; e < eend; ++e)
1140  {
1141  o << "<td sides='b' bgcolor='"
1142  << (e != edges_[e].next_succ ? "cyan" : "gray")
1143  << "' port='e" << e << "'>" << e << "</td>\n";
1144  }
1145  o << "</tr>";
1146  }
1147  if (dsi & DSI_EdgesBody)
1148  {
1149  o << "<tr><td port='ed'>dst</td>\n";
1150  for (unsigned e = 1; e < eend; ++e)
1151  {
1152  o << "<td port='ed" << e;
1153  int d = edges_[e].dst;
1154  if (d < 0)
1155  o << "' bgcolor='pink'>~" << ~d;
1156  else
1157  o << "' bgcolor='yellow'>" << d;
1158  o << "</td>\n";
1159  }
1160  o << "</tr><tr><td port='en'>next_succ</td>\n";
1161  for (unsigned e = 1; e < eend; ++e)
1162  {
1163  o << "<td port='en" << e;
1164  if (edges_[e].next_succ)
1165  {
1166  if (edges_[e].next_succ != e)
1167  o << "' bgcolor='cyan";
1168  else
1169  o << "' bgcolor='gray";
1170  }
1171  o << "'>" << edges_[e].next_succ << "</td>\n";
1172  }
1173  o << "</tr><tr><td port='es'>src</td>\n";
1174  for (unsigned e = 1; e < eend; ++e)
1175  o << "<td port='es" << e << "' bgcolor='yellow'>"
1176  << edges_[e].src << "</td>\n";
1177  o << "</tr>\n";
1178  }
1179  if (dsi & DSI_EdgesFooter)
1180  o << "</table>>]\n";
1181  if (!dests_.empty())
1182  {
1183  unsigned dend = dests_.size();
1184  if (dsi & DSI_DestsHeader)
1185  {
1186  o << ("dests [label=<\n"
1187  "<table border='0' cellborder='1' cellspacing='0'>\n"
1188  "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1189  unsigned d = 0;
1190  while (d < dend)
1191  {
1192  o << "<td sides='b' bgcolor='pink' port='d"
1193  << d << "'>~" << d << "</td>\n";
1194  unsigned cnt = dests_[d];
1195  d += cnt + 1;
1196  while (cnt--)
1197  o << "<td sides='b'></td>\n";
1198  }
1199  o << "</tr>\n";
1200  }
1201  if (dsi & DSI_DestsBody)
1202  {
1203  o << "<tr><td port='dd'>#cnt/dst</td>\n";
1204  unsigned d = 0;
1205  while (d < dend)
1206  {
1207  unsigned cnt = dests_[d];
1208  o << "<td port='d'>#" << cnt << "</td>\n";
1209  ++d;
1210  while (cnt--)
1211  {
1212  o << "<td bgcolor='yellow' port='dd"
1213  << d << "'>" << dests_[d] << "</td>\n";
1214  ++d;
1215  }
1216  }
1217  o << "</tr>\n";
1218  }
1219  if (dsi & DSI_DestsFooter)
1220  o << "</table>>]\n";
1221  }
1222  if (dsi & DSI_GraphFooter)
1223  o << "}\n";
1224  }
1225 
1232  {
1233  if (killed_edge_ == 0)
1234  return;
1235  auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1236  [this](const edge_storage_t& t) {
1237  return this->is_dead_edge(t);
1238  });
1239  edges_.erase(i, edges_.end());
1240  killed_edge_ = 0;
1241  }
1242 
1248  template<class Predicate = std::less<edge_storage_t>>
1249  void sort_edges_(Predicate p = Predicate())
1250  {
1251  //std::cerr << "\nbefore\n";
1252  //dump_storage(std::cerr);
1253  std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1254  }
1255 
1265  template<class Predicate = std::less<edge_storage_t>>
1266  void sort_edges_srcfirst_(Predicate p = Predicate(),
1267  parallel_policy ppolicy = parallel_policy())
1268  {
1269  SPOT_ASSERT(!edges_.empty());
1270  const unsigned ns = num_states();
1271  std::vector<unsigned> idx_list(ns+1);
1272  edge_vector_t new_edges;
1273  new_edges.reserve(edges_.size());
1274  new_edges.resize(1);
1275  // This causes edge 0 to be considered as dead.
1276  new_edges[0].next_succ = 0;
1277  // Copy all edges so that they are sorted by src
1278  for (unsigned s = 0; s < ns; ++s)
1279  {
1280  idx_list[s] = new_edges.size();
1281  for (const auto& e : out(s))
1282  new_edges.push_back(e);
1283  }
1284  idx_list[ns] = new_edges.size();
1285  // New edge sorted by source
1286  // If we have few edge or only one threads
1287  // Benchmark few?
1288  auto bne = new_edges.begin();
1289 #ifndef SPOT_ENABLE_PTHREAD
1290  (void) ppolicy;
1291 #else
1292  unsigned nthreads = ppolicy.nthreads();
1293  if (nthreads <= 1)
1294 #endif
1295  {
1296  for (unsigned s = 0u; s < ns; ++s)
1297  std::stable_sort(bne + idx_list[s],
1298  bne + idx_list[s+1], p);
1299  }
1300 #ifdef SPOT_ENABLE_PTHREAD
1301  else
1302  {
1303  static std::vector<std::thread> tv;
1304  SPOT_ASSERT(tv.empty());
1305  tv.resize(nthreads);
1306  // FIXME: Due to the way these thread advance into the state
1307  // vector, they access very close memory location. It would
1308  // seems more cache friendly to have threads work on blocks
1309  // of continuous states.
1310  for (unsigned id = 0; id < nthreads; ++id)
1311  tv[id] = std::thread(
1312  [bne, id, ns, &idx_list, p, nthreads]()
1313  {
1314  for (unsigned s = id; s < ns; s += nthreads)
1315  std::stable_sort(bne + idx_list[s],
1316  bne + idx_list[s+1], p);
1317  return;
1318  });
1319  for (auto& t : tv)
1320  t.join();
1321  tv.clear();
1322  }
1323 #endif
1324  std::swap(edges_, new_edges);
1325  // Like after normal sort_edges, they need to be chained before usage
1326  }
1327 
1335  template<bool Stable = false, class Predicate = std::less<edge_storage_t>>
1336  void sort_edges_of_(Predicate p = Predicate(),
1337  const std::vector<bool>* to_sort_ptr = nullptr)
1338  {
1339  SPOT_ASSERT((to_sort_ptr == nullptr)
1340  || (to_sort_ptr->size() == num_states()));
1341  //std::cerr << "\nbefore\n";
1342  //dump_storage(std::cerr);
1343  auto pi = [&](unsigned t1, unsigned t2)
1344  {return p(edges_[t1], edges_[t2]); };
1345 
1346  // Sort the outgoing edges of each selected state according
1347  // to predicate p. Do that in place.
1348  std::vector<unsigned> sort_idx_;
1349  unsigned ns = num_states();
1350  for (unsigned i = 0; i < ns; ++i)
1351  {
1352  if (to_sort_ptr && !(*to_sort_ptr)[i])
1353  continue;
1354  unsigned t = states_[i].succ;
1355  if (t == 0)
1356  continue;
1357  sort_idx_.clear();
1358  do
1359  {
1360  sort_idx_.push_back(t);
1361  t = edges_[t].next_succ;
1362  } while (t != 0);
1363  if constexpr (Stable)
1364  std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
1365  else
1366  std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
1367  // Update the graph
1368  states_[i].succ = sort_idx_.front();
1369  states_[i].succ_tail = sort_idx_.back();
1370  const unsigned n_outs_n1 = sort_idx_.size() - 1;
1371  for (unsigned k = 0; k < n_outs_n1; ++k)
1372  edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
1373  edges_[sort_idx_.back()].next_succ = 0; // terminal
1374  }
1375  // Done
1376  }
1377 
1383  {
1384  state last_src = -1U;
1385  edge tend = edges_.size();
1386  for (edge t = 1; t < tend; ++t)
1387  {
1388  state src = edges_[t].src;
1389  if (src != last_src)
1390  {
1391  states_[src].succ = t;
1392  if (last_src != -1U)
1393  {
1394  states_[last_src].succ_tail = t - 1;
1395  edges_[t - 1].next_succ = 0;
1396  }
1397  while (++last_src != src)
1398  {
1399  states_[last_src].succ = 0;
1400  states_[last_src].succ_tail = 0;
1401  }
1402  }
1403  else
1404  {
1405  edges_[t - 1].next_succ = t;
1406  }
1407  }
1408  if (last_src != -1U)
1409  {
1410  states_[last_src].succ_tail = tend - 1;
1411  edges_[tend - 1].next_succ = 0;
1412  }
1413  unsigned send = states_.size();
1414  while (++last_src != send)
1415  {
1416  states_[last_src].succ = 0;
1417  states_[last_src].succ_tail = 0;
1418  }
1419  //std::cerr << "\nafter\n";
1420  //dump_storage(std::cerr);
1421  }
1422 
1428  void rename_states_(const std::vector<unsigned>& newst)
1429  {
1430  SPOT_ASSERT(newst.size() == states_.size());
1431  unsigned tend = edges_.size();
1432  for (unsigned t = 1; t < tend; t++)
1433  {
1434  edges_[t].dst = newst[edges_[t].dst];
1435  edges_[t].src = newst[edges_[t].src];
1436  }
1437  }
1438 
1456  void defrag_states(const std::vector<unsigned>& newst, unsigned used_states)
1457  {
1458  SPOT_ASSERT(newst.size() >= states_.size());
1459  SPOT_ASSERT(used_states > 0);
1460 
1461  //std::cerr << "\nbefore defrag\n";
1462  //dump_storage(std::cerr);
1463 
1464  // Shift all states in states_, as indicated by newst.
1465  unsigned send = states_.size();
1466  for (state s = 0; s < send; ++s)
1467  {
1468  state dst = newst[s];
1469  if (dst == s)
1470  continue;
1471  if (dst == -1U)
1472  {
1473  // This is an erased state. Mark all its edges as
1474  // dead (i.e., t.next_succ should point to t for each of
1475  // them).
1476  auto t = states_[s].succ;
1477  while (t)
1478  std::swap(t, edges_[t].next_succ);
1479  continue;
1480  }
1481  states_[dst] = std::move(states_[s]);
1482  }
1483  states_.resize(used_states);
1484 
1485  // Shift all edges in edges_. The algorithm is
1486  // similar to remove_if, but it also keeps the correspondence
1487  // between the old and new index as newidx[old] = new.
1488  //
1489  // If you change anything to this logic, you might want to
1490  // double check twa_graph::defrag_states where we need to
1491  // predict the new edges indices in order to update
1492  // highlight-edges.
1493  unsigned tend = edges_.size();
1494  std::vector<edge> newidx(tend);
1495  unsigned dest = 1;
1496  for (edge t = 1; t < tend; ++t)
1497  {
1498  if (is_dead_edge(t))
1499  continue;
1500  if (t != dest)
1501  edges_[dest] = std::move(edges_[t]);
1502  newidx[t] = dest;
1503  ++dest;
1504  }
1505  edges_.resize(dest);
1506  killed_edge_ = 0;
1507 
1508  // Adjust next_succ and dst pointers in all edges.
1509  for (edge t = 1; t < dest; ++t)
1510  {
1511  auto& tr = edges_[t];
1512  tr.src = newst[tr.src];
1513  tr.dst = newst[tr.dst];
1514  tr.next_succ = newidx[tr.next_succ];
1515  }
1516 
1517  // Adjust succ and succ_tails pointers in all states.
1518  for (auto& s: states_)
1519  {
1520  s.succ = newidx[s.succ];
1521  s.succ_tail = newidx[s.succ_tail];
1522  }
1523 
1524  //std::cerr << "\nafter defrag\n";
1525  //dump_storage(std::cerr);
1526  }
1527 
1528  // prototype was changed in Spot 2.10
1529  SPOT_DEPRECATED("use reference version of this method")
1530  void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
1531  {
1532  return defrag_states(newst, used_states);
1533  }
1535  };
1536 }
A directed graph.
Definition: graph.hh:598
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:657
void dump_storage_as_dot(std::ostream &o, int dsi=DSI_All) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1096
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:1013
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1036
const edge_storage_t::data_t & edge_data(edge s) const
return the Edge_Data of an edge.
Definition: graph.hh:771
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:930
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:907
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:945
void sort_edges_of_(Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
Sort edges of the given states.
Definition: graph.hh:1336
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:696
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:682
edge index_of_edge(const edge_storage_t &tt) const
Convert a storage reference into an edge number.
Definition: graph.hh:892
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:919
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:996
void sort_edges_srcfirst_(Predicate p=Predicate(), parallel_policy ppolicy=parallel_policy())
Sort all edges by src first, then, within edges of the same source use the predicate.
Definition: graph.hh:1266
edge_storage_t::data_t & edge_data(edge s)
return the Edge_Data of an edge.
Definition: graph.hh:765
const dests_vector_t & dests_vector() const
The vector used to store universal destinations.
Definition: graph.hh:1024
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1029
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:747
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:753
edge new_univ_edge(state src, const std::initializer_list< state > &dsts, Args &&... args)
Create a new universal edge.
Definition: graph.hh:856
bool is_existential() const
Whether the automaton uses only existential branching.
Definition: graph.hh:671
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:717
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:901
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:936
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1231
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:642
state new_univ_dests(I dst_begin, I dst_end)
Create a new universal destination group.
Definition: graph.hh:808
state_vector & states()
Return the vector of states.
Definition: graph.hh:950
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1428
void defrag_states(const std::vector< unsigned > &newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1456
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:711
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:913
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:665
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:729
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:979
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:885
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1249
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:1008
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:984
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:843
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1382
internal::all_trans< digraph > edges()
Return a fake container with all edges (excluding erased edges)
Definition: graph.hh:965
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:784
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (excluding erased edges)
Definition: graph.hh:960
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:735
Definition: graph.hh:422
Definition: graph.hh:499
Definition: graph.hh:246
Definition: graph.hh:319
Definition: graph.hh:388
Definition: graph.hh:556
This class is used to tell parallel algorithms what resources they may use.
Definition: common.hh:155
Abstract class for states.
Definition: twa.hh:47
@ tt
True.
@ G
Globally.
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
Definition: automata.hh:26
Definition: graph.hh:65
Definition: graph.hh:162
Definition: graph.hh:187
Definition: graph.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