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

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