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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1