spot  2.10.6.dev
graph.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2018, 2020-2022 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 <map>
30 #include <iostream>
31 #include <thread>
32 
33 namespace spot
34 {
35  template <typename State_Data, typename Edge_Data>
36  class SPOT_API digraph;
37 
38  namespace internal
39  {
40 #ifndef SWIG
41  template <typename Of, typename ...Args>
43  {
44  static const bool value = false;
45  };
46 
47  template <typename Of, typename Arg1, typename ...Args>
48  struct first_is_base_of<Of, Arg1, Args...>
49  {
50  static const bool value =
51  std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
52  };
53 #endif
54 
55  // The boxed_label class stores Data as an attribute called
56  // "label" if boxed is true. It is an empty class if Data is
57  // void, and it simply inherits from Data if boxed is false.
58  //
59  // The data() method offers an homogeneous access to the Data
60  // instance.
61  template <typename Data, bool boxed = !std::is_class<Data>::value>
62  struct SPOT_API boxed_label
63  {
64  typedef Data data_t;
65  Data label;
66 
67 #ifndef SWIG
68  template <typename... Args,
69  typename = typename std::enable_if<
70  !first_is_base_of<boxed_label, Args...>::value>::type>
71  boxed_label(Args&&... args)
72  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
73  : label{std::forward<Args>(args)...}
74  {
75  }
76 #endif
77 
78  // if Data is a POD type, G++ 4.8.2 wants default values for all
79  // label fields unless we define this default constructor here.
80  explicit boxed_label()
81  noexcept(std::is_nothrow_constructible<Data>::value)
82  {
83  }
84 
85  Data& data()
86  {
87  return label;
88  }
89 
90  const Data& data() const
91  {
92  return label;
93  }
94 
95  bool operator<(const boxed_label& other) const
96  {
97  return label < other.label;
98  }
99  };
100 
101  template <>
102  struct SPOT_API boxed_label<void, true>: public std::tuple<>
103  {
104  typedef std::tuple<> data_t;
105  std::tuple<>& data()
106  {
107  return *this;
108  }
109 
110  const std::tuple<>& data() const
111  {
112  return *this;
113  }
114 
115  };
116 
117  template <typename Data>
118  struct SPOT_API boxed_label<Data, false>: public Data
119  {
120  typedef Data data_t;
121 
122 #ifndef SWIG
123  template <typename... Args,
124  typename = typename std::enable_if<
125  !first_is_base_of<boxed_label, Args...>::value>::type>
126  boxed_label(Args&&... args)
127  noexcept(std::is_nothrow_constructible<Data, Args...>::value)
128  : Data{std::forward<Args>(args)...}
129  {
130  }
131 #endif
132 
133  // if Data is a POD type, G++ 4.8.2 wants default values for all
134  // label fields unless we define this default constructor here.
135  explicit boxed_label()
136  noexcept(std::is_nothrow_constructible<Data>::value)
137  {
138  }
139 
140  Data& data()
141  {
142  return *this;
143  }
144 
145  const Data& data() const
146  {
147  return *this;
148  }
149  };
150 
152  // State storage for digraphs
154 
155  // We have two implementations, one with attached State_Data, and
156  // one without.
157 
158  template <typename Edge, typename State_Data>
159  struct SPOT_API distate_storage final: public State_Data
160  {
161  Edge succ = 0; // First outgoing edge (used when iterating)
162  Edge succ_tail = 0; // Last outgoing edge (used for
163  // appending new edges)
164 #ifndef SWIG
165  template <typename... Args,
166  typename = typename std::enable_if<
167  !first_is_base_of<distate_storage, Args...>::value>::type>
168  distate_storage(Args&&... args)
169  noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
170  : State_Data{std::forward<Args>(args)...}
171  {
172  }
173 #endif
174  };
175 
177  // Edge storage
179 
180  // Again two implementation: one with label, and one without.
181 
182  template <typename StateIn,
183  typename StateOut, typename Edge, typename Edge_Data>
184  struct SPOT_API edge_storage final: public Edge_Data
185  {
186  typedef Edge edge;
187 
188  StateOut dst; // destination
189  Edge next_succ; // next outgoing edge with same
190  // source, or 0
191  StateIn src; // source
192 
193  explicit edge_storage()
194  noexcept(std::is_nothrow_constructible<Edge_Data>::value)
195  : Edge_Data{}
196  {
197  }
198 
199 #ifndef SWIG
200  template <typename... Args>
201  edge_storage(StateOut dst, Edge next_succ,
202  StateIn src, Args&&... args)
203  noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
204  && std::is_nothrow_constructible<StateOut, StateOut>::value
205  && std::is_nothrow_constructible<Edge, Edge>::value)
206  : Edge_Data{std::forward<Args>(args)...},
207  dst(dst), next_succ(next_succ), src(src)
208  {
209  }
210 #endif
211 
212  bool operator<(const edge_storage& other) const
213  {
214  if (src < other.src)
215  return true;
216  if (src > other.src)
217  return false;
218  // This might be costly if the destination is a vector
219  if (dst < other.dst)
220  return true;
221  if (dst > other.dst)
222  return false;
223  return this->data() < other.data();
224  }
225 
226  bool operator==(const edge_storage& other) const
227  {
228  return src == other.src &&
229  dst == other.dst &&
230  this->data() == other.data();
231  }
232  };
233 
235  // Edge iterator
237 
238  // This holds a graph and a edge number that is the start of
239  // a list, and it iterates over all the edge_storage_t elements
240  // of that list.
241 
242  template <typename Graph>
243  class SPOT_API edge_iterator
244  {
245  public:
246  typedef typename std::conditional<std::is_const<Graph>::value,
247  const typename Graph::edge_storage_t,
248  typename Graph::edge_storage_t>::type
249  value_type;
250  typedef value_type& reference;
251  typedef value_type* pointer;
252  typedef std::ptrdiff_t difference_type;
253  typedef std::forward_iterator_tag iterator_category;
254 
255  typedef typename Graph::edge edge;
256 
257  edge_iterator() noexcept
258  : g_(nullptr), t_(0)
259  {
260  }
261 
262  edge_iterator(Graph* g, edge t) noexcept
263  : g_(g), t_(t)
264  {
265  }
266 
267  bool operator==(edge_iterator o) const
268  {
269  return t_ == o.t_;
270  }
271 
272  bool operator!=(edge_iterator o) const
273  {
274  return t_ != o.t_;
275  }
276 
277  reference operator*() const
278  {
279  return g_->edge_storage(t_);
280  }
281 
282  pointer operator->() const
283  {
284  return &g_->edge_storage(t_);
285  }
286 
287  edge_iterator operator++()
288  {
289  t_ = operator*().next_succ;
290  return *this;
291  }
292 
293  edge_iterator operator++(int)
294  {
295  edge_iterator ti = *this;
296  t_ = operator*().next_succ;
297  return ti;
298  }
299 
300  operator bool() const
301  {
302  return t_;
303  }
304 
305  edge trans() const
306  {
307  return t_;
308  }
309 
310  protected:
311  Graph* g_;
312  edge t_;
313  };
314 
315  template <typename Graph>
316  class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
317  {
318  typedef edge_iterator<Graph> super;
319  public:
320  typedef typename Graph::state_storage_t state_storage_t;
321  typedef typename Graph::edge edge;
322 
323  killer_edge_iterator(Graph* g, edge t, state_storage_t& src) noexcept
324  : super(g, t), src_(src), prev_(0)
325  {
326  }
327 
328  killer_edge_iterator operator++()
329  {
330  prev_ = this->t_;
331  this->t_ = this->operator*().next_succ;
332  return *this;
333  }
334 
335  killer_edge_iterator operator++(int)
336  {
337  killer_edge_iterator ti = *this;
338  ++*this;
339  return ti;
340  }
341 
342  // Erase the current edge and advance the iterator.
343  void erase()
344  {
345  edge next = this->operator*().next_succ;
346 
347  // Update source state and previous edges
348  if (prev_)
349  {
350  this->g_->edge_storage(prev_).next_succ = next;
351  }
352  else
353  {
354  if (src_.succ == this->t_)
355  src_.succ = next;
356  }
357  if (src_.succ_tail == this->t_)
358  {
359  src_.succ_tail = prev_;
360  SPOT_ASSERT(next == 0);
361  }
362 
363  // Erased edges have themselves as next_succ.
364  this->operator*().next_succ = this->t_;
365 
366  // Advance iterator to next edge.
367  this->t_ = next;
368 
369  ++this->g_->killed_edge_;
370  }
371 
372  protected:
373  state_storage_t& src_;
374  edge prev_;
375  };
376 
377 
379  // State OUT
381 
382  // Fake container listing the outgoing edges of a state.
383 
384  template <typename Graph>
385  class SPOT_API state_out
386  {
387  public:
388  typedef typename Graph::edge edge;
389  state_out(Graph* g, edge t) noexcept
390  : g_(g), t_(t)
391  {
392  }
393 
394  edge_iterator<Graph> begin() const
395  {
396  return {g_, t_};
397  }
398 
399  edge_iterator<Graph> end() const
400  {
401  return {};
402  }
403 
404  void recycle(edge t)
405  {
406  t_ = t;
407  }
408 
409  protected:
410  Graph* g_;
411  edge t_;
412  };
413 
415  // all_trans
417 
418  template <typename Graph>
419  class SPOT_API all_edge_iterator
420  {
421  public:
422  typedef typename std::conditional<std::is_const<Graph>::value,
423  const typename Graph::edge_storage_t,
424  typename Graph::edge_storage_t>::type
425  value_type;
426  typedef value_type& reference;
427  typedef value_type* pointer;
428  typedef std::ptrdiff_t difference_type;
429  typedef std::forward_iterator_tag iterator_category;
430 
431  protected:
432  typedef typename std::conditional<std::is_const<Graph>::value,
433  const typename Graph::edge_vector_t,
434  typename Graph::edge_vector_t>::type
435  tv_t;
436 
437  unsigned t_;
438  tv_t& tv_;
439 
440  void skip_()
441  {
442  unsigned s = tv_.size();
443  do
444  ++t_;
445  while (t_ < s && tv_[t_].next_succ == t_);
446  }
447 
448  public:
449  all_edge_iterator(unsigned pos, tv_t& tv) noexcept
450  : t_(pos), tv_(tv)
451  {
452  skip_();
453  }
454 
455  all_edge_iterator(tv_t& tv) noexcept
456  : t_(tv.size()), tv_(tv)
457  {
458  }
459 
460  all_edge_iterator& operator++()
461  {
462  skip_();
463  return *this;
464  }
465 
466  all_edge_iterator operator++(int)
467  {
468  all_edge_iterator old = *this;
469  ++*this;
470  return old;
471  }
472 
473  bool operator==(all_edge_iterator o) const
474  {
475  return t_ == o.t_;
476  }
477 
478  bool operator!=(all_edge_iterator o) const
479  {
480  return t_ != o.t_;
481  }
482 
483  reference operator*() const
484  {
485  return tv_[t_];
486  }
487 
488  pointer operator->() const
489  {
490  return &tv_[t_];
491  }
492  };
493 
494 
495  template <typename Graph>
496  class SPOT_API all_trans
497  {
498  public:
499  typedef typename std::conditional<std::is_const<Graph>::value,
500  const typename Graph::edge_vector_t,
501  typename Graph::edge_vector_t>::type
502  tv_t;
504  private:
505  tv_t& tv_;
506  public:
507 
508  all_trans(tv_t& tv) noexcept
509  : tv_(tv)
510  {
511  }
512 
513  iter_t begin() const
514  {
515  return {0, tv_};
516  }
517 
518  iter_t end() const
519  {
520  return {tv_};
521  }
522  };
523 
524  class SPOT_API const_universal_dests
525  {
526  private:
527  const unsigned* begin_;
528  const unsigned* end_;
529  unsigned tmp_;
530  public:
531  const_universal_dests(const unsigned* begin, const unsigned* end) noexcept
532  : begin_(begin), end_(end)
533  {
534  }
535 
536  const_universal_dests(unsigned state) noexcept
537  : begin_(&tmp_), end_(&tmp_ + 1), tmp_(state)
538  {
539  }
540 
541  const unsigned* begin() const
542  {
543  return begin_;
544  }
545 
546  const unsigned* end() const
547  {
548  return end_;
549  }
550  };
551 
552  template<class G>
554  {
555  std::map<std::vector<unsigned>, unsigned> uniq_;
556  G& g_;
557  public:
558 
559  univ_dest_mapper(G& graph)
560  : g_(graph)
561  {
562  }
563 
564  template<class I>
565  unsigned new_univ_dests(I begin, I end)
566  {
567  std::vector<unsigned> tmp(begin, end);
568  std::sort(tmp.begin(), tmp.end());
569  tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
570  auto p = uniq_.emplace(tmp, 0);
571  if (p.second)
572  p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
573  return p.first->second;
574  }
575 
576  };
577 
578  } // namespace internal
579 
580 
585  template <typename State_Data, typename Edge_Data>
586  class digraph
587  {
588  friend class internal::edge_iterator<digraph>;
589  friend class internal::edge_iterator<const digraph>;
591 
592  public:
595 
596  // Extra data to store on each state or edge.
597  typedef State_Data state_data_t;
598  typedef Edge_Data edge_data_t;
599 
600  // State and edges are identified by their indices in some
601  // vector.
602  typedef unsigned state;
603  typedef unsigned edge;
604 
605  typedef internal::distate_storage<edge,
608  typedef internal::edge_storage<state, state, edge,
611  typedef std::vector<state_storage_t> state_vector;
612  typedef std::vector<edge_storage_t> edge_vector_t;
613 
614  // A sequence of universal destination groups of the form:
615  // (n state_1 state_2 ... state_n)*
616  typedef std::vector<unsigned> dests_vector_t;
617 
618  protected:
619  state_vector states_;
620  edge_vector_t edges_;
621  dests_vector_t dests_; // Only used by alternating automata.
622  // Number of erased edges.
623  unsigned killed_edge_;
624  public:
631  digraph(unsigned max_states = 10, unsigned max_trans = 0)
632  : killed_edge_(0)
633  {
634  states_.reserve(max_states);
635  if (max_trans == 0)
636  max_trans = max_states * 2;
637  edges_.reserve(max_trans + 1);
638  // Edge number 0 is not used, because we use this index
639  // to mark the absence of a edge.
640  edges_.resize(1);
641  // This causes edge 0 to be considered as dead.
642  edges_[0].next_succ = 0;
643  }
644 
646  unsigned num_states() const
647  {
648  return states_.size();
649  }
650 
654  unsigned num_edges() const
655  {
656  return edges_.size() - killed_edge_ - 1;
657  }
658 
660  bool is_existential() const
661  {
662  return dests_.empty();
663  }
664 
670  template <typename... Args>
671  state new_state(Args&&... args)
672  {
673  state s = states_.size();
674  states_.emplace_back(std::forward<Args>(args)...);
675  return s;
676  }
677 
684  template <typename... Args>
685  state new_states(unsigned n, Args&&... args)
686  {
687  state s = states_.size();
688  states_.reserve(s + n);
689  while (n--)
690  states_.emplace_back(std::forward<Args>(args)...);
691  return s;
692  }
693 
699  state_storage_t&
700  state_storage(state s)
701  {
702  return states_[s];
703  }
704 
705  const state_storage_t&
706  state_storage(state s) const
707  {
708  return states_[s];
709  }
711 
717  typename state_storage_t::data_t&
718  state_data(state s)
719  {
720  return states_[s].data();
721  }
722 
723  const typename state_storage_t::data_t&
724  state_data(state s) const
725  {
726  return states_[s].data();
727  }
729 
735  edge_storage_t&
736  edge_storage(edge s)
737  {
738  return edges_[s];
739  }
740 
741  const edge_storage_t&
742  edge_storage(edge s) const
743  {
744  return edges_[s];
745  }
747 
753  typename edge_storage_t::data_t&
754  edge_data(edge s)
755  {
756  return edges_[s].data();
757  }
758 
759  const typename edge_storage_t::data_t&
760  edge_data(edge s) const
761  {
762  return edges_[s].data();
763  }
765 
771  template <typename... Args>
772  edge
773  new_edge(state src, state dst, Args&&... args)
774  {
775  edge t = edges_.size();
776  edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
777 
778  edge st = states_[src].succ_tail;
779  SPOT_ASSERT(st < t || !st);
780  if (!st)
781  states_[src].succ = t;
782  else
783  edges_[st].next_succ = t;
784  states_[src].succ_tail = t;
785  return t;
786  }
787 
795  template <typename I>
796  state
797  new_univ_dests(I dst_begin, I dst_end)
798  {
799  unsigned sz = std::distance(dst_begin, dst_end);
800  if (sz == 1)
801  return *dst_begin;
802  SPOT_ASSERT(sz > 1);
803  unsigned d = dests_.size();
804  dests_.emplace_back(sz);
805  dests_.insert(dests_.end(), dst_begin, dst_end);
806  return ~d;
807  }
808 
815  template <typename I, typename... Args>
816  edge
817  new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args)
818  {
819  return new_edge(src, new_univ_dests(dst_begin, dst_end),
820  std::forward<Args>(args)...);
821  }
822 
828  template <typename... Args>
829  edge
830  new_univ_edge(state src, const std::initializer_list<state>& dsts,
831  Args&&... args)
832  {
833  return new_univ_edge(src, dsts.begin(), dsts.end(),
834  std::forward<Args>(args)...);
835  }
836 
837  internal::const_universal_dests univ_dests(state src) const
838  {
839  if ((int)src < 0)
840  {
841  unsigned pos = ~src;
842  const unsigned* d = dests_.data();
843  d += pos;
844  unsigned num = *d;
845  return { d + 1, d + num + 1 };
846  }
847  else
848  {
849  return src;
850  }
851  }
852 
853  internal::const_universal_dests univ_dests(const edge_storage_t& e) const
854  {
855  return univ_dests(e.dst);
856  }
857 
859  state index_of_state(const state_storage_t& ss) const
860  {
861  SPOT_ASSERT(!states_.empty());
862  return &ss - &states_.front();
863  }
864 
866  edge index_of_edge(const edge_storage_t& tt) const
867  {
868  SPOT_ASSERT(!edges_.empty());
869  return &tt - &edges_.front();
870  }
871 
875  out(state src)
876  {
877  return {this, states_[src].succ};
878  }
879 
882  {
883  return out(index_of_state(src));
884  }
885 
887  out(state src) const
888  {
889  return {this, states_[src].succ};
890  }
891 
893  out(state_storage_t& src) const
894  {
895  return out(index_of_state(src));
896  }
898 
905  {
906  return {this, src.succ, src};
907  }
908 
910  out_iteraser(state src)
911  {
912  return out_iteraser(state_storage(src));
913  }
915 
919  const state_vector& states() const
920  {
921  return states_;
922  }
923 
924  state_vector& states()
925  {
926  return states_;
927  }
929 
935  {
936  return edges_;
937  }
938 
940  {
941  return edges_;
942  }
944 
953  const edge_vector_t& edge_vector() const
954  {
955  return edges_;
956  }
957 
958  edge_vector_t& edge_vector()
959  {
960  return edges_;
961  }
963 
970  bool is_valid_edge(edge t) const
971  {
972  // Erased edges have their next_succ pointing to
973  // themselves.
974  return (t < edges_.size() &&
975  edges_[t].next_succ != t);
976  }
977 
982  bool is_dead_edge(unsigned t) const
983  {
984  return edges_[t].next_succ == t;
985  }
986 
987  bool is_dead_edge(const edge_storage_t& t) const
988  {
989  return t.next_succ == index_of_edge(t);
990  }
992 
998  const dests_vector_t& dests_vector() const
999  {
1000  return dests_;
1001  }
1002 
1003  dests_vector_t& dests_vector()
1004  {
1005  return dests_;
1006  }
1008 
1010  void dump_storage(std::ostream& o) const
1011  {
1012  unsigned tend = edges_.size();
1013  for (unsigned t = 1; t < tend; ++t)
1014  {
1015  o << 't' << t << ": (s"
1016  << edges_[t].src << ", ";
1017  int d = edges_[t].dst;
1018  if (d < 0)
1019  o << 'd' << ~d;
1020  else
1021  o << 's' << d;
1022  o << ") t" << edges_[t].next_succ << '\n';
1023  }
1024  unsigned send = states_.size();
1025  for (unsigned s = 0; s < send; ++s)
1026  {
1027  o << 's' << s << ": t"
1028  << states_[s].succ << " t"
1029  << states_[s].succ_tail << '\n';
1030  }
1031  unsigned dend = dests_.size();
1032  unsigned size = 0;
1033  for (unsigned s = 0; s < dend; ++s)
1034  {
1035  o << 'd' << s << ": ";
1036  if (size == 0)
1037  {
1038  o << '#';
1039  size = dests_[s];
1040  }
1041  else
1042  {
1043  o << 's';
1044  --size;
1045  }
1046  o << dests_[s] << '\n';
1047  }
1048  }
1049 
1050  enum dump_storage_items {
1051  DSI_GraphHeader = 1,
1052  DSI_GraphFooter = 2,
1053  DSI_StatesHeader = 4,
1054  DSI_StatesBody = 8,
1055  DSI_StatesFooter = 16,
1056  DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1057  DSI_EdgesHeader = 32,
1058  DSI_EdgesBody = 64,
1059  DSI_EdgesFooter = 128,
1060  DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1061  DSI_DestsHeader = 256,
1062  DSI_DestsBody = 512,
1063  DSI_DestsFooter = 1024,
1064  DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1065  DSI_All =
1066  DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1067  };
1068 
1070  void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const
1071  {
1072  if (dsi & DSI_GraphHeader)
1073  o << "digraph g { \nnode [shape=plaintext]\n";
1074  unsigned send = states_.size();
1075  if (dsi & DSI_StatesHeader)
1076  {
1077  o << ("states [label=<\n"
1078  "<table border='0' cellborder='1' cellspacing='0'>\n"
1079  "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1080  for (unsigned s = 0; s < send; ++s)
1081  o << "<td sides='b' bgcolor='yellow' port='s" << s << "'>"
1082  << s << "</td>\n";
1083  o << "</tr>\n";
1084  }
1085  if (dsi & DSI_StatesBody)
1086  {
1087  o << "<tr><td port='ss'>succ</td>\n";
1088  for (unsigned s = 0; s < send; ++s)
1089  {
1090  o << "<td port='ss" << s;
1091  if (states_[s].succ)
1092  o << "' bgcolor='cyan";
1093  o << "'>" << states_[s].succ << "</td>\n";
1094  }
1095  o << "</tr><tr><td port='st'>succ_tail</td>\n";
1096  for (unsigned s = 0; s < send; ++s)
1097  {
1098  o << "<td port='st" << s;
1099  if (states_[s].succ_tail)
1100  o << "' bgcolor='cyan";
1101  o << "'>" << states_[s].succ_tail << "</td>\n";
1102  }
1103  o << "</tr>\n";
1104  }
1105  if (dsi & DSI_StatesFooter)
1106  o << "</table>>]\n";
1107  unsigned eend = edges_.size();
1108  if (dsi & DSI_EdgesHeader)
1109  {
1110  o << ("edges [label=<\n"
1111  "<table border='0' cellborder='1' cellspacing='0'>\n"
1112  "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1113  for (unsigned e = 1; e < eend; ++e)
1114  {
1115  o << "<td sides='b' bgcolor='"
1116  << (e != edges_[e].next_succ ? "cyan" : "gray")
1117  << "' port='e" << e << "'>" << e << "</td>\n";
1118  }
1119  o << "</tr>";
1120  }
1121  if (dsi & DSI_EdgesBody)
1122  {
1123  o << "<tr><td port='ed'>dst</td>\n";
1124  for (unsigned e = 1; e < eend; ++e)
1125  {
1126  o << "<td port='ed" << e;
1127  int d = edges_[e].dst;
1128  if (d < 0)
1129  o << "' bgcolor='pink'>~" << ~d;
1130  else
1131  o << "' bgcolor='yellow'>" << d;
1132  o << "</td>\n";
1133  }
1134  o << "</tr><tr><td port='en'>next_succ</td>\n";
1135  for (unsigned e = 1; e < eend; ++e)
1136  {
1137  o << "<td port='en" << e;
1138  if (edges_[e].next_succ)
1139  {
1140  if (edges_[e].next_succ != e)
1141  o << "' bgcolor='cyan";
1142  else
1143  o << "' bgcolor='gray";
1144  }
1145  o << "'>" << edges_[e].next_succ << "</td>\n";
1146  }
1147  o << "</tr><tr><td port='es'>src</td>\n";
1148  for (unsigned e = 1; e < eend; ++e)
1149  o << "<td port='es" << e << "' bgcolor='yellow'>"
1150  << edges_[e].src << "</td>\n";
1151  o << "</tr>\n";
1152  }
1153  if (dsi & DSI_EdgesFooter)
1154  o << "</table>>]\n";
1155  if (!dests_.empty())
1156  {
1157  unsigned dend = dests_.size();
1158  if (dsi & DSI_DestsHeader)
1159  {
1160  o << ("dests [label=<\n"
1161  "<table border='0' cellborder='1' cellspacing='0'>\n"
1162  "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1163  unsigned d = 0;
1164  while (d < dend)
1165  {
1166  o << "<td sides='b' bgcolor='pink' port='d"
1167  << d << "'>~" << d << "</td>\n";
1168  unsigned cnt = dests_[d];
1169  d += cnt + 1;
1170  while (cnt--)
1171  o << "<td sides='b'></td>\n";
1172  }
1173  o << "</tr>\n";
1174  }
1175  if (dsi & DSI_DestsBody)
1176  {
1177  o << "<tr><td port='dd'>#cnt/dst</td>\n";
1178  unsigned d = 0;
1179  while (d < dend)
1180  {
1181  unsigned cnt = dests_[d];
1182  o << "<td port='d'>#" << cnt << "</td>\n";
1183  ++d;
1184  while (cnt--)
1185  {
1186  o << "<td bgcolor='yellow' port='dd"
1187  << d << "'>" << dests_[d] << "</td>\n";
1188  ++d;
1189  }
1190  }
1191  o << "</tr>\n";
1192  }
1193  if (dsi & DSI_DestsFooter)
1194  o << "</table>>]\n";
1195  }
1196  if (dsi & DSI_GraphFooter)
1197  o << "}\n";
1198  }
1199 
1206  {
1207  if (killed_edge_ == 0)
1208  return;
1209  auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1210  [this](const edge_storage_t& t) {
1211  return this->is_dead_edge(t);
1212  });
1213  edges_.erase(i, edges_.end());
1214  killed_edge_ = 0;
1215  }
1216 
1222  template<class Predicate = std::less<edge_storage_t>>
1223  void sort_edges_(Predicate p = Predicate())
1224  {
1225  //std::cerr << "\nbefore\n";
1226  //dump_storage(std::cerr);
1227  std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1228  }
1229 
1239  template<class Predicate = std::less<edge_storage_t>>
1240  void sort_edges_srcfirst_(Predicate p = Predicate())
1241  {
1242  //std::cerr << "\nbefore\n";
1243  //dump_storage(std::cerr);
1244  const auto N = num_states();
1245  // Read threads once
1246  const unsigned nthreads = get_nthreads();
1247 
1248  auto idx_list = std::vector<unsigned>(N+1);
1249  auto new_edges = edge_vector_t();
1250  new_edges.reserve(edges_.size());
1251  if (SPOT_UNLIKELY(edges_.empty()))
1252  throw std::runtime_error("Empty edge vector!");
1253  new_edges.resize(1);
1254  // This causes edge 0 to be considered as dead.
1255  new_edges[0].next_succ = 0;
1256  // Copy the edges such that they are sorted by src
1257  for (auto s = 0u; s < N; ++s)
1258  {
1259  idx_list[s] = new_edges.size();
1260  for (const auto& e : out(s))
1261  new_edges.push_back(e);
1262  }
1263  idx_list[N] = new_edges.size();
1264  // New edge sorted by source
1265  // If we have few edge or only one threads
1266  // Benchmark few?
1267  auto bne = new_edges.begin();
1268  if (nthreads == 1 || edges_.size() < 1000)
1269  {
1270  for (auto s = 0u; s < N; ++s)
1271  std::stable_sort(bne + idx_list[s],
1272  bne + idx_list[s+1],
1273  p);
1274  }
1275  else
1276  {
1277  static auto tv = std::vector<std::thread>();
1278  SPOT_ASSERT(tv.empty());
1279  tv.resize(nthreads);
1280  for (unsigned id = 0; id < nthreads; ++id)
1281  tv[id] = std::thread(
1282  [bne, id, N, &idx_list, p, nthreads]()
1283  {
1284  for (auto s = id; s < N; s+=nthreads)
1285  std::stable_sort(bne + idx_list[s],
1286  bne + idx_list[s+1],
1287  p);
1288  return;
1289  });
1290  for (auto& t : tv)
1291  t.join();
1292  tv.clear();
1293  }
1294  // Done
1295  std::swap(edges_, new_edges);
1296  // Like after normal sort_edges, they need to be chained before usage
1297  }
1298 
1306  template<bool Stable = false, class Predicate = std::less<edge_storage_t>>
1307  void sort_edges_of_(Predicate p = Predicate(),
1308  const std::vector<bool>* to_sort_ptr = nullptr)
1309  {
1310  SPOT_ASSERT((to_sort_ptr == nullptr)
1311  || (to_sort_ptr->size() == num_states()));
1312  //std::cerr << "\nbefore\n";
1313  //dump_storage(std::cerr);
1314  auto pi = [&](unsigned t1, unsigned t2)
1315  {return p(edges_[t1], edges_[t2]); };
1316 
1317  // Sort the outgoing edges of each selected state according
1318  // to predicate p. Do that in place.
1319  std::vector<unsigned> sort_idx_;
1320  unsigned ns = num_states();
1321  for (unsigned i = 0; i < ns; ++i)
1322  {
1323  if (to_sort_ptr && !(*to_sort_ptr)[i])
1324  continue;
1325  unsigned t = states_[i].succ;
1326  if (t == 0)
1327  continue;
1328  sort_idx_.clear();
1329  do
1330  {
1331  sort_idx_.push_back(t);
1332  t = edges_[t].next_succ;
1333  } while (t != 0);
1334  if constexpr (Stable)
1335  std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
1336  else
1337  std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
1338  // Update the graph
1339  states_[i].succ = sort_idx_.front();
1340  states_[i].succ_tail = sort_idx_.back();
1341  const unsigned n_outs_n1 = sort_idx_.size() - 1;
1342  for (unsigned k = 0; k < n_outs_n1; ++k)
1343  edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
1344  edges_[sort_idx_.back()].next_succ = 0; // terminal
1345  }
1346  // Done
1347  }
1348 
1354  {
1355  state last_src = -1U;
1356  edge tend = edges_.size();
1357  for (edge t = 1; t < tend; ++t)
1358  {
1359  state src = edges_[t].src;
1360  if (src != last_src)
1361  {
1362  states_[src].succ = t;
1363  if (last_src != -1U)
1364  {
1365  states_[last_src].succ_tail = t - 1;
1366  edges_[t - 1].next_succ = 0;
1367  }
1368  while (++last_src != src)
1369  {
1370  states_[last_src].succ = 0;
1371  states_[last_src].succ_tail = 0;
1372  }
1373  }
1374  else
1375  {
1376  edges_[t - 1].next_succ = t;
1377  }
1378  }
1379  if (last_src != -1U)
1380  {
1381  states_[last_src].succ_tail = tend - 1;
1382  edges_[tend - 1].next_succ = 0;
1383  }
1384  unsigned send = states_.size();
1385  while (++last_src != send)
1386  {
1387  states_[last_src].succ = 0;
1388  states_[last_src].succ_tail = 0;
1389  }
1390  //std::cerr << "\nafter\n";
1391  //dump_storage(std::cerr);
1392  }
1393 
1399  void rename_states_(const std::vector<unsigned>& newst)
1400  {
1401  SPOT_ASSERT(newst.size() == states_.size());
1402  unsigned tend = edges_.size();
1403  for (unsigned t = 1; t < tend; t++)
1404  {
1405  edges_[t].dst = newst[edges_[t].dst];
1406  edges_[t].src = newst[edges_[t].src];
1407  }
1408  }
1409 
1427  void defrag_states(const std::vector<unsigned>& newst, unsigned used_states)
1428  {
1429  SPOT_ASSERT(newst.size() >= states_.size());
1430  SPOT_ASSERT(used_states > 0);
1431 
1432  //std::cerr << "\nbefore defrag\n";
1433  //dump_storage(std::cerr);
1434 
1435  // Shift all states in states_, as indicated by newst.
1436  unsigned send = states_.size();
1437  for (state s = 0; s < send; ++s)
1438  {
1439  state dst = newst[s];
1440  if (dst == s)
1441  continue;
1442  if (dst == -1U)
1443  {
1444  // This is an erased state. Mark all its edges as
1445  // dead (i.e., t.next_succ should point to t for each of
1446  // them).
1447  auto t = states_[s].succ;
1448  while (t)
1449  std::swap(t, edges_[t].next_succ);
1450  continue;
1451  }
1452  states_[dst] = std::move(states_[s]);
1453  }
1454  states_.resize(used_states);
1455 
1456  // Shift all edges in edges_. The algorithm is
1457  // similar to remove_if, but it also keeps the correspondence
1458  // between the old and new index as newidx[old] = new.
1459  unsigned tend = edges_.size();
1460  std::vector<edge> newidx(tend);
1461  unsigned dest = 1;
1462  for (edge t = 1; t < tend; ++t)
1463  {
1464  if (is_dead_edge(t))
1465  continue;
1466  if (t != dest)
1467  edges_[dest] = std::move(edges_[t]);
1468  newidx[t] = dest;
1469  ++dest;
1470  }
1471  edges_.resize(dest);
1472  killed_edge_ = 0;
1473 
1474  // Adjust next_succ and dst pointers in all edges.
1475  for (edge t = 1; t < dest; ++t)
1476  {
1477  auto& tr = edges_[t];
1478  tr.src = newst[tr.src];
1479  tr.dst = newst[tr.dst];
1480  tr.next_succ = newidx[tr.next_succ];
1481  }
1482 
1483  // Adjust succ and succ_tails pointers in all states.
1484  for (auto& s: states_)
1485  {
1486  s.succ = newidx[s.succ];
1487  s.succ_tail = newidx[s.succ_tail];
1488  }
1489 
1490  //std::cerr << "\nafter defrag\n";
1491  //dump_storage(std::cerr);
1492  }
1493 
1494  // prototype was changed in Spot 2.10
1495  SPOT_DEPRECATED("use reference version of this method")
1496  void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
1497  {
1498  return defrag_states(newst, used_states);
1499  }
1501  };
1502 }
A directed graph.
Definition: graph.hh:587
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:646
void dump_storage_as_dot(std::ostream &o, int dsi=DSI_All) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1070
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:987
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1010
const edge_storage_t::data_t & edge_data(edge s) const
return the Edgeg_Data of an edge.
Definition: graph.hh:760
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:904
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:881
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:919
void sort_edges_of_(Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
Sort edges of the given states.
Definition: graph.hh:1307
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:685
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:671
edge index_of_edge(const edge_storage_t &tt) const
Convert a storage reference into an edge number.
Definition: graph.hh:866
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:893
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:970
edge_storage_t::data_t & edge_data(edge s)
return the Edgeg_Data of an edge.
Definition: graph.hh:754
const dests_vector_t & dests_vector() const
The vector used to store universal destinations.
Definition: graph.hh:998
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1003
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:736
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:742
edge new_univ_edge(state src, const std::initializer_list< state > &dsts, Args &&... args)
Create a new universal edge.
Definition: graph.hh:830
bool is_existential() const
Whether the automaton uses only existential branching.
Definition: graph.hh:660
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:706
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:875
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:910
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1205
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:631
state new_univ_dests(I dst_begin, I dst_end)
Create a new universal destination group.
Definition: graph.hh:797
state_vector & states()
Return the vector of states.
Definition: graph.hh:924
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1399
void defrag_states(const std::vector< unsigned > &newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1427
void sort_edges_srcfirst_(Predicate p=Predicate())
Sort all edges by src first, then, within edges of the same source use the predicate.
Definition: graph.hh:1240
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:700
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:887
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:654
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:718
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:953
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:859
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1223
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:982
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:958
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:817
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1353
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:939
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:773
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:934
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:724
Definition: graph.hh:420
Definition: graph.hh:497
Definition: graph.hh:244
Definition: graph.hh:317
Definition: graph.hh:386
Definition: graph.hh:554
Abstract class for states.
Definition: twa.hh:51
@ 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:27
Definition: graph.hh:63
Definition: graph.hh:160
Definition: graph.hh:185
Definition: graph.hh:43

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