spot  2.7.1
sccinfo.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
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 <vector>
23 #include <spot/twa/twagraph.hh>
24 
25 namespace spot
26 {
27  class scc_info;
28 
29  namespace internal
30  {
31  struct keep_all
32  {
33  template <typename Iterator>
34  bool operator()(Iterator, Iterator) const noexcept
35  {
36  return true;
37  }
38  };
39 
40  // Keep only transitions that have at least one destination in the
41  // current SCC.
43  {
44  private:
45  const std::vector<unsigned>& sccof_;
46  unsigned desired_scc_;
47  public:
48  keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
49  : sccof_(sccof), desired_scc_(desired_scc)
50  {
51  }
52 
53  template <typename Iterator>
54  bool operator()(Iterator begin, Iterator end) const noexcept
55  {
56  bool want = false;
57  while (begin != end)
58  if (sccof_[*begin++] == desired_scc_)
59  {
60  want = true;
61  break;
62  }
63  return want;
64  }
65  };
66 
67  template <typename Graph, typename Filter>
68  class SPOT_API scc_edge_iterator
69  {
70  public:
71  typedef typename std::conditional<std::is_const<Graph>::value,
72  const typename Graph::edge_storage_t,
73  typename Graph::edge_storage_t>::type
74  value_type;
75  typedef value_type& reference;
76  typedef value_type* pointer;
77  typedef std::ptrdiff_t difference_type;
78  typedef std::forward_iterator_tag iterator_category;
79 
80  typedef std::vector<unsigned>::const_iterator state_iterator;
81 
82  typedef typename std::conditional<std::is_const<Graph>::value,
83  const typename Graph::edge_vector_t,
84  typename Graph::edge_vector_t>::type
85  tv_t;
86 
87  typedef typename std::conditional<std::is_const<Graph>::value,
88  const typename Graph::state_vector,
89  typename Graph::state_vector>::type
90  sv_t;
91  typedef const typename Graph::dests_vector_t dv_t;
92  protected:
93 
94  state_iterator pos_;
95  state_iterator end_;
96  unsigned t_;
97  tv_t* tv_;
98  sv_t* sv_;
99  dv_t* dv_;
100 
101  Filter filt_;
102 
103  void inc_state_maybe_()
104  {
105  while (!t_ && (++pos_ != end_))
106  t_ = (*sv_)[*pos_].succ;
107  }
108 
109  void inc_()
110  {
111  t_ = (*tv_)[t_].next_succ;
112  inc_state_maybe_();
113  }
114 
115  bool ignore_current()
116  {
117  unsigned dst = (*this)->dst;
118  if ((int)dst >= 0)
119  // Non-universal branching => a single destination.
120  return !filt_(&(*this)->dst, 1 + &(*this)->dst);
121  // Universal branching => multiple destinations.
122  const unsigned* d = dv_->data() + ~dst;
123  return !filt_(d + 1, d + *d + 1);
124  }
125 
126  public:
127  scc_edge_iterator(state_iterator begin, state_iterator end,
128  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
129  : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
130  {
131  if (pos_ == end_)
132  return;
133 
134  t_ = (*sv_)[*pos_].succ;
135  inc_state_maybe_();
136  while (pos_ != end_ && ignore_current())
137  inc_();
138  }
139 
140  scc_edge_iterator& operator++()
141  {
142  do
143  inc_();
144  while (pos_ != end_ && ignore_current());
145  return *this;
146  }
147 
148  scc_edge_iterator operator++(int)
149  {
150  scc_edge_iterator old = *this;
151  ++*this;
152  return old;
153  }
154 
155  bool operator==(scc_edge_iterator o) const
156  {
157  return pos_ == o.pos_ && t_ == o.t_;
158  }
159 
160  bool operator!=(scc_edge_iterator o) const
161  {
162  return pos_ != o.pos_ || t_ != o.t_;
163  }
164 
165  reference operator*() const
166  {
167  return (*tv_)[t_];
168  }
169 
170  pointer operator->() const
171  {
172  return &**this;
173  }
174  };
175 
176 
177  template <typename Graph, typename Filter>
178  class SPOT_API scc_edges
179  {
180  public:
182  typedef typename iter_t::tv_t tv_t;
183  typedef typename iter_t::sv_t sv_t;
184  typedef typename iter_t::dv_t dv_t;
185  typedef typename iter_t::state_iterator state_iterator;
186  private:
187  state_iterator begin_;
188  state_iterator end_;
189  tv_t* tv_;
190  sv_t* sv_;
191  dv_t* dv_;
192  Filter filt_;
193  public:
194 
195  scc_edges(state_iterator begin, state_iterator end,
196  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
197  : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
198  {
199  }
200 
201  iter_t begin() const
202  {
203  return {begin_, end_, tv_, sv_, dv_, filt_};
204  }
205 
206  iter_t end() const
207  {
208  return {end_, end_, nullptr, nullptr, nullptr, filt_};
209  }
210  };
211  }
212 
213 
216  class SPOT_API scc_info_node
217  {
218  public:
219  typedef std::vector<unsigned> scc_succs;
220  friend class scc_info;
221  protected:
222  scc_succs succ_;
223  std::vector<unsigned> states_; // States of the component
224  unsigned one_state_;
225  acc_cond::mark_t acc_;
226  acc_cond::mark_t common_;
227  bool trivial_:1;
228  bool accepting_:1; // Necessarily accepting
229  bool rejecting_:1; // Necessarily rejecting
230  bool useful_:1;
231  public:
232  scc_info_node() noexcept:
233  acc_({}), trivial_(true), accepting_(false),
234  rejecting_(false), useful_(false)
235  {
236  }
237 
239  acc_cond::mark_t common, bool trivial) noexcept
240  : acc_(acc), common_(common),
241  trivial_(trivial), accepting_(false),
242  rejecting_(false), useful_(false)
243  {
244  }
245 
246  bool is_trivial() const
247  {
248  return trivial_;
249  }
250 
256  bool is_accepting() const
257  {
258  return accepting_;
259  }
260 
266  bool is_rejecting() const
267  {
268  return rejecting_;
269  }
270 
271  bool is_useful() const
272  {
273  return useful_;
274  }
275 
276  acc_cond::mark_t acc_marks() const
277  {
278  return acc_;
279  }
280 
281  acc_cond::mark_t common_marks() const
282  {
283  return common_;
284  }
285 
286  const std::vector<unsigned>& states() const
287  {
288  return states_;
289  }
290 
291  unsigned one_state() const
292  {
293  return one_state_;
294  }
295 
296  const scc_succs& succ() const
297  {
298  return succ_;
299  }
300  };
301 
304  enum class scc_info_options
305  {
308  NONE = 0,
313  STOP_ON_ACC = 1,
318  TRACK_STATES = 2,
322  TRACK_SUCCS = 4,
328  };
329 
330  inline
331  bool operator!(scc_info_options me)
332  {
333  return me == scc_info_options::NONE;
334  }
335 
336  inline
337  scc_info_options operator&(scc_info_options left, scc_info_options right)
338  {
339  typedef std::underlying_type_t<scc_info_options> ut;
340  return static_cast<scc_info_options>(static_cast<ut>(left)
341  & static_cast<ut>(right));
342  }
343 
344  inline
345  scc_info_options operator|(scc_info_options left, scc_info_options right)
346  {
347  typedef std::underlying_type_t<scc_info_options> ut;
348  return static_cast<scc_info_options>(static_cast<ut>(left)
349  | static_cast<ut>(right));
350  }
351 
370  class SPOT_API scc_info
371  {
372  public:
373  // scc_node used to be an inner class, but Swig 3.0.10 does not
374  // support that yet.
375  typedef scc_info_node scc_node;
376  typedef scc_info_node::scc_succs scc_succs;
402  enum class edge_filter_choice { keep, ignore, cut };
403  typedef edge_filter_choice
404  (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
405  void* filter_data);
407 
408  protected:
409 
410  std::vector<unsigned> sccof_;
411  std::vector<scc_node> node_;
412  const_twa_graph_ptr aut_;
413  unsigned initial_state_;
414  edge_filter filter_;
415  void* filter_data_;
416  int one_acc_scc_ = -1;
417  scc_info_options options_;
418 
419  // Update the useful_ bits. Called automatically.
420  void determine_usefulness();
421 
422  const scc_node& node(unsigned scc) const
423  {
424  return node_[scc];
425  }
426 
427 #ifndef SWIG
428  private:
429  [[noreturn]] static void report_need_track_states();
430  [[noreturn]] static void report_need_track_succs();
431  [[noreturn]] static void report_incompatible_stop_on_acc();
432 #endif
433 
434  public:
437  scc_info(const_twa_graph_ptr aut,
438  // Use ~0U instead of -1U to work around a bug in Swig.
439  // See https://github.com/swig/swig/issues/993
440  unsigned initial_state = ~0U,
441  edge_filter filter = nullptr,
442  void* filter_data = nullptr,
444 
445  scc_info(const_twa_graph_ptr aut, scc_info_options options)
446  : scc_info(aut, ~0U, nullptr, nullptr, options)
447  {
448  }
450 
451  const_twa_graph_ptr get_aut() const
452  {
453  return aut_;
454  }
455 
456  unsigned scc_count() const
457  {
458  return node_.size();
459  }
460 
462  int one_accepting_scc() const
463  {
464  return one_acc_scc_;
465  }
466 
467  bool reachable_state(unsigned st) const
468  {
469  return scc_of(st) != -1U;
470  }
471 
472  unsigned scc_of(unsigned st) const
473  {
474  return sccof_[st];
475  }
476 
477  std::vector<scc_node>::const_iterator begin() const
478  {
479  return node_.begin();
480  }
481 
482  std::vector<scc_node>::const_iterator end() const
483  {
484  return node_.end();
485  }
486 
487  std::vector<scc_node>::const_iterator cbegin() const
488  {
489  return node_.cbegin();
490  }
491 
492  std::vector<scc_node>::const_iterator cend() const
493  {
494  return node_.cend();
495  }
496 
497  std::vector<scc_node>::const_reverse_iterator rbegin() const
498  {
499  return node_.rbegin();
500  }
501 
502  std::vector<scc_node>::const_reverse_iterator rend() const
503  {
504  return node_.rend();
505  }
506 
507  const std::vector<unsigned>& states_of(unsigned scc) const
508  {
509  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
510  report_need_track_states();
511  return node(scc).states();
512  }
513 
520  edges_of(unsigned scc) const
521  {
522  auto& states = states_of(scc);
523  return {states.begin(), states.end(),
524  &aut_->edge_vector(), &aut_->states(),
525  &aut_->get_graph().dests_vector(),
527  }
528 
537  inner_edges_of(unsigned scc) const
538  {
539  auto& states = states_of(scc);
540  return {states.begin(), states.end(),
541  &aut_->edge_vector(), &aut_->states(),
542  &aut_->get_graph().dests_vector(),
543  internal::keep_inner_scc(sccof_, scc)};
544  }
545 
546  unsigned one_state_of(unsigned scc) const
547  {
548  return node(scc).one_state();
549  }
550 
552  unsigned initial() const
553  {
554  SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
555  return scc_of(initial_state_);
556  }
557 
558  const scc_succs& succ(unsigned scc) const
559  {
560  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
561  report_need_track_succs();
562  return node(scc).succ();
563  }
564 
565  bool is_trivial(unsigned scc) const
566  {
567  return node(scc).is_trivial();
568  }
569 
570  SPOT_DEPRECATED("use acc_sets_of() instead")
571  acc_cond::mark_t acc(unsigned scc) const
572  {
573  return acc_sets_of(scc);
574  }
575 
576  bool is_accepting_scc(unsigned scc) const
577  {
578  return node(scc).is_accepting();
579  }
580 
581  bool is_rejecting_scc(unsigned scc) const
582  {
583  return node(scc).is_rejecting();
584  }
585 
590  void determine_unknown_acceptance();
591 
596  bool check_scc_emptiness(unsigned n);
597 
598  bool is_useful_scc(unsigned scc) const
599  {
600  if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
601  report_incompatible_stop_on_acc();
602  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
603  report_need_track_succs();
604  return node(scc).is_useful();
605  }
606 
607  bool is_useful_state(unsigned st) const
608  {
609  return reachable_state(st) && is_useful_scc(scc_of(st));
610  }
611 
614  std::vector<std::set<acc_cond::mark_t>> marks() const;
615  std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
616 
617  // Same as above, with old names.
618  SPOT_DEPRECATED("use marks() instead")
619  std::vector<std::set<acc_cond::mark_t>> used_acc() const
620  {
621  return marks();
622  }
623  SPOT_DEPRECATED("use marks_of() instead")
624  std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
625  {
626  return marks_of(scc);
627  }
628 
632  acc_cond::mark_t acc_sets_of(unsigned scc) const
633  {
634  return node(scc).acc_marks();
635  }
636 
639  acc_cond::mark_t common_sets_of(unsigned scc) const
640  {
641  return node(scc).common_marks();
642  }
643 
644  std::vector<bool> weak_sccs() const;
645 
646  bdd scc_ap_support(unsigned scc) const;
647 
657  std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
658  acc_cond::mark_t sets,
659  bool preserve_names = false) const;
660  protected:
662  void
663  states_on_acc_cycle_of_rec(unsigned scc,
664  acc_cond::mark_t all_fin,
665  acc_cond::mark_t all_inf,
666  unsigned nb_pairs,
667  std::vector<acc_cond::rs_pair>& pairs,
668  std::vector<unsigned>& res,
669  std::vector<unsigned>& old) const;
670  public:
675  std::vector<unsigned>
676  states_on_acc_cycle_of(unsigned scc) const;
677  };
678 
679 
683  SPOT_API std::ostream&
684  dump_scc_info_dot(std::ostream& out,
685  const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
686 
687 }
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:370
Definition: sccinfo.hh:178
Storage for SCC related information.
Definition: sccinfo.hh:216
Default behavior: explore everything and track states and succs.
Definition: graph.hh:183
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:639
Definition: sccinfo.hh:68
internal::scc_edges< const twa_graph::graph_t, internal::keep_all > edges_of(unsigned scc) const
A fake container to iterate over all edges leaving any state of an SCC.
Definition: sccinfo.hh:520
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:462
acc_cond::mark_t acc_sets_of(unsigned scc) const
Returns, for a given SCC, the set of all colors appearing in it. It is the set of colors that appear ...
Definition: sccinfo.hh:632
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:304
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:445
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:256
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:552
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:402
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:266
Definition: twa.hh:1697
Definition: sccinfo.hh:31
Definition: sccinfo.hh:42
internal::scc_edges< const twa_graph::graph_t, internal::keep_inner_scc > inner_edges_of(unsigned scc) const
A fake container to iterate over all edges between states of an SCC.
Definition: sccinfo.hh:537
An acceptance mark.
Definition: acc.hh:81

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.8.13