spot  2.8.4
sccinfo.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2019 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 #include <spot/twaalgos/emptiness.hh>
25 
26 namespace spot
27 {
28  class scc_info;
29 
30  namespace internal
31  {
32  struct keep_all
33  {
34  template <typename Iterator>
35  bool operator()(Iterator, Iterator) const noexcept
36  {
37  return true;
38  }
39  };
40 
41  // Keep only transitions that have at least one destination in the
42  // current SCC.
44  {
45  private:
46  const std::vector<unsigned>& sccof_;
47  unsigned desired_scc_;
48  public:
49  keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
50  : sccof_(sccof), desired_scc_(desired_scc)
51  {
52  }
53 
54  template <typename Iterator>
55  bool operator()(Iterator begin, Iterator end) const noexcept
56  {
57  bool want = false;
58  while (begin != end)
59  if (sccof_[*begin++] == desired_scc_)
60  {
61  want = true;
62  break;
63  }
64  return want;
65  }
66  };
67 
68  template <typename Graph, typename Filter>
69  class SPOT_API scc_edge_iterator
70  {
71  public:
72  typedef typename std::conditional<std::is_const<Graph>::value,
73  const typename Graph::edge_storage_t,
74  typename Graph::edge_storage_t>::type
75  value_type;
76  typedef value_type& reference;
77  typedef value_type* pointer;
78  typedef std::ptrdiff_t difference_type;
79  typedef std::forward_iterator_tag iterator_category;
80 
81  typedef std::vector<unsigned>::const_iterator state_iterator;
82 
83  typedef typename std::conditional<std::is_const<Graph>::value,
84  const typename Graph::edge_vector_t,
85  typename Graph::edge_vector_t>::type
86  tv_t;
87 
88  typedef typename std::conditional<std::is_const<Graph>::value,
89  const typename Graph::state_vector,
90  typename Graph::state_vector>::type
91  sv_t;
92  typedef const typename Graph::dests_vector_t dv_t;
93  protected:
94 
95  state_iterator pos_;
96  state_iterator end_;
97  unsigned t_;
98  tv_t* tv_;
99  sv_t* sv_;
100  dv_t* dv_;
101 
102  Filter filt_;
103 
104  void inc_state_maybe_()
105  {
106  while (!t_ && (++pos_ != end_))
107  t_ = (*sv_)[*pos_].succ;
108  }
109 
110  void inc_()
111  {
112  t_ = (*tv_)[t_].next_succ;
113  inc_state_maybe_();
114  }
115 
116  bool ignore_current()
117  {
118  unsigned dst = (*this)->dst;
119  if ((int)dst >= 0)
120  // Non-universal branching => a single destination.
121  return !filt_(&(*this)->dst, 1 + &(*this)->dst);
122  // Universal branching => multiple destinations.
123  const unsigned* d = dv_->data() + ~dst;
124  return !filt_(d + 1, d + *d + 1);
125  }
126 
127  public:
128  scc_edge_iterator(state_iterator begin, state_iterator end,
129  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
130  : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
131  {
132  if (pos_ == end_)
133  return;
134 
135  t_ = (*sv_)[*pos_].succ;
136  inc_state_maybe_();
137  while (pos_ != end_ && ignore_current())
138  inc_();
139  }
140 
141  scc_edge_iterator& operator++()
142  {
143  do
144  inc_();
145  while (pos_ != end_ && ignore_current());
146  return *this;
147  }
148 
149  scc_edge_iterator operator++(int)
150  {
151  scc_edge_iterator old = *this;
152  ++*this;
153  return old;
154  }
155 
156  bool operator==(scc_edge_iterator o) const
157  {
158  return pos_ == o.pos_ && t_ == o.t_;
159  }
160 
161  bool operator!=(scc_edge_iterator o) const
162  {
163  return pos_ != o.pos_ || t_ != o.t_;
164  }
165 
166  reference operator*() const
167  {
168  return (*tv_)[t_];
169  }
170 
171  pointer operator->() const
172  {
173  return &**this;
174  }
175  };
176 
177 
178  template <typename Graph, typename Filter>
179  class SPOT_API scc_edges
180  {
181  public:
183  typedef typename iter_t::tv_t tv_t;
184  typedef typename iter_t::sv_t sv_t;
185  typedef typename iter_t::dv_t dv_t;
186  typedef typename iter_t::state_iterator state_iterator;
187  private:
188  state_iterator begin_;
189  state_iterator end_;
190  tv_t* tv_;
191  sv_t* sv_;
192  dv_t* dv_;
193  Filter filt_;
194  public:
195 
196  scc_edges(state_iterator begin, state_iterator end,
197  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
198  : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
199  {
200  }
201 
202  iter_t begin() const
203  {
204  return {begin_, end_, tv_, sv_, dv_, filt_};
205  }
206 
207  iter_t end() const
208  {
209  return {end_, end_, nullptr, nullptr, nullptr, filt_};
210  }
211  };
212  }
213 
214 
217  class SPOT_API scc_info_node
218  {
219  public:
220  typedef std::vector<unsigned> scc_succs;
221  friend class scc_info;
222  protected:
223  scc_succs succ_;
224  std::vector<unsigned> states_; // States of the component
225  unsigned one_state_;
226  acc_cond::mark_t acc_;
227  acc_cond::mark_t common_;
228  bool trivial_:1;
229  bool accepting_:1; // Necessarily accepting
230  bool rejecting_:1; // Necessarily rejecting
231  bool useful_:1;
232  public:
233  scc_info_node() noexcept:
234  acc_({}), trivial_(true), accepting_(false),
235  rejecting_(false), useful_(false)
236  {
237  }
238 
240  acc_cond::mark_t common, bool trivial) noexcept
241  : acc_(acc), common_(common),
242  trivial_(trivial), accepting_(false),
243  rejecting_(false), useful_(false)
244  {
245  }
246 
247  bool is_trivial() const
248  {
249  return trivial_;
250  }
251 
257  bool is_accepting() const
258  {
259  return accepting_;
260  }
261 
267  bool is_rejecting() const
268  {
269  return rejecting_;
270  }
271 
272  bool is_useful() const
273  {
274  return useful_;
275  }
276 
277  acc_cond::mark_t acc_marks() const
278  {
279  return acc_;
280  }
281 
282  acc_cond::mark_t common_marks() const
283  {
284  return common_;
285  }
286 
287  const std::vector<unsigned>& states() const
288  {
289  return states_;
290  }
291 
292  unsigned one_state() const
293  {
294  return one_state_;
295  }
296 
297  const scc_succs& succ() const
298  {
299  return succ_;
300  }
301  };
302 
305  enum class scc_info_options
306  {
309  NONE = 0,
314  STOP_ON_ACC = 1,
319  TRACK_STATES = 2,
323  TRACK_SUCCS = 4,
329  };
330 
331  inline
332  bool operator!(scc_info_options me)
333  {
334  return me == scc_info_options::NONE;
335  }
336 
337  inline
338  scc_info_options operator&(scc_info_options left, scc_info_options right)
339  {
340  typedef std::underlying_type_t<scc_info_options> ut;
341  return static_cast<scc_info_options>(static_cast<ut>(left)
342  & static_cast<ut>(right));
343  }
344 
345  inline
346  scc_info_options operator|(scc_info_options left, scc_info_options right)
347  {
348  typedef std::underlying_type_t<scc_info_options> ut;
349  return static_cast<scc_info_options>(static_cast<ut>(left)
350  | static_cast<ut>(right));
351  }
352 
353  class SPOT_API scc_and_mark_filter;
354 
373  class SPOT_API scc_info
374  {
375  public:
376  // scc_node used to be an inner class, but Swig 3.0.10 does not
377  // support that yet.
378  typedef scc_info_node scc_node;
379  typedef scc_info_node::scc_succs scc_succs;
405  enum class edge_filter_choice { keep, ignore, cut };
406  typedef edge_filter_choice
407  (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
408  void* filter_data);
410 
411  protected:
412 
413  std::vector<unsigned> sccof_;
414  std::vector<scc_node> node_;
415  const_twa_graph_ptr aut_;
416  unsigned initial_state_;
417  edge_filter filter_;
418  void* filter_data_;
419  int one_acc_scc_ = -1;
420  scc_info_options options_;
421 
422  // Update the useful_ bits. Called automatically.
423  void determine_usefulness();
424 
425  const scc_node& node(unsigned scc) const
426  {
427  return node_[scc];
428  }
429 
430 #ifndef SWIG
431  private:
432  [[noreturn]] static void report_need_track_states();
433  [[noreturn]] static void report_need_track_succs();
434  [[noreturn]] static void report_incompatible_stop_on_acc();
435 #endif
436 
437  public:
440  scc_info(const_twa_graph_ptr aut,
441  // Use ~0U instead of -1U to work around a bug in Swig.
442  // See https://github.com/swig/swig/issues/993
443  unsigned initial_state = ~0U,
444  edge_filter filter = nullptr,
445  void* filter_data = nullptr,
447 
448  scc_info(const_twa_graph_ptr aut, scc_info_options options)
449  : scc_info(aut, ~0U, nullptr, nullptr, options)
450  {
451  }
453 
460  scc_info(const scc_and_mark_filter& filt, scc_info_options options);
461  // we separate the two functions so that we can rename
462  // scc_info(x,options) into scc_info_with_options(x,options) in Python.
463  // Otherwrise calling scc_info(aut,options) can be confused with
464  // scc_info(aut,initial_state).
465  scc_info(const scc_and_mark_filter& filt)
466  : scc_info(filt, scc_info_options::ALL)
467  {
468  }
470 
471  const_twa_graph_ptr get_aut() const
472  {
473  return aut_;
474  }
475 
476  scc_info_options get_options() const
477  {
478  return options_;
479  }
480 
481  const void* get_filter_data() const
482  {
483  return filter_data_;
484  }
485 
486  unsigned scc_count() const
487  {
488  return node_.size();
489  }
490 
492  int one_accepting_scc() const
493  {
494  return one_acc_scc_;
495  }
496 
497  bool reachable_state(unsigned st) const
498  {
499  return scc_of(st) != -1U;
500  }
501 
502  unsigned scc_of(unsigned st) const
503  {
504  return sccof_[st];
505  }
506 
507  std::vector<scc_node>::const_iterator begin() const
508  {
509  return node_.begin();
510  }
511 
512  std::vector<scc_node>::const_iterator end() const
513  {
514  return node_.end();
515  }
516 
517  std::vector<scc_node>::const_iterator cbegin() const
518  {
519  return node_.cbegin();
520  }
521 
522  std::vector<scc_node>::const_iterator cend() const
523  {
524  return node_.cend();
525  }
526 
527  std::vector<scc_node>::const_reverse_iterator rbegin() const
528  {
529  return node_.rbegin();
530  }
531 
532  std::vector<scc_node>::const_reverse_iterator rend() const
533  {
534  return node_.rend();
535  }
536 
537  const std::vector<unsigned>& states_of(unsigned scc) const
538  {
539  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
540  report_need_track_states();
541  return node(scc).states();
542  }
543 
550  edges_of(unsigned scc) const
551  {
552  auto& states = states_of(scc);
553  return {states.begin(), states.end(),
554  &aut_->edge_vector(), &aut_->states(),
555  &aut_->get_graph().dests_vector(),
557  }
558 
567  inner_edges_of(unsigned scc) const
568  {
569  auto& states = states_of(scc);
570  return {states.begin(), states.end(),
571  &aut_->edge_vector(), &aut_->states(),
572  &aut_->get_graph().dests_vector(),
573  internal::keep_inner_scc(sccof_, scc)};
574  }
575 
576  unsigned one_state_of(unsigned scc) const
577  {
578  return node(scc).one_state();
579  }
580 
582  unsigned initial() const
583  {
584  SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
585  return scc_of(initial_state_);
586  }
587 
588  const scc_succs& succ(unsigned scc) const
589  {
590  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
591  report_need_track_succs();
592  return node(scc).succ();
593  }
594 
595  bool is_trivial(unsigned scc) const
596  {
597  return node(scc).is_trivial();
598  }
599 
600  SPOT_DEPRECATED("use acc_sets_of() instead")
601  acc_cond::mark_t acc(unsigned scc) const
602  {
603  return acc_sets_of(scc);
604  }
605 
606  bool is_accepting_scc(unsigned scc) const
607  {
608  return node(scc).is_accepting();
609  }
610 
611  bool is_rejecting_scc(unsigned scc) const
612  {
613  return node(scc).is_rejecting();
614  }
615 
620  void determine_unknown_acceptance();
621 
626  bool check_scc_emptiness(unsigned n);
627 
635  void get_accepting_run(unsigned scc, twa_run_ptr r) const;
636 
637  bool is_useful_scc(unsigned scc) const
638  {
639  if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
640  report_incompatible_stop_on_acc();
641  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
642  report_need_track_succs();
643  return node(scc).is_useful();
644  }
645 
646  bool is_useful_state(unsigned st) const
647  {
648  return reachable_state(st) && is_useful_scc(scc_of(st));
649  }
650 
653  std::vector<std::set<acc_cond::mark_t>> marks() const;
654  std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
655 
656  // Same as above, with old names.
657  SPOT_DEPRECATED("use marks() instead")
658  std::vector<std::set<acc_cond::mark_t>> used_acc() const
659  {
660  return marks();
661  }
662  SPOT_DEPRECATED("use marks_of() instead")
663  std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
664  {
665  return marks_of(scc);
666  }
667 
671  acc_cond::mark_t acc_sets_of(unsigned scc) const
672  {
673  return node(scc).acc_marks();
674  }
675 
678  acc_cond::mark_t common_sets_of(unsigned scc) const
679  {
680  return node(scc).common_marks();
681  }
682 
683  std::vector<bool> weak_sccs() const;
684 
685  bdd scc_ap_support(unsigned scc) const;
686 
696  std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
697  acc_cond::mark_t sets,
698  bool preserve_names = false) const;
699  protected:
701  void
702  states_on_acc_cycle_of_rec(unsigned scc,
703  acc_cond::mark_t all_fin,
704  acc_cond::mark_t all_inf,
705  unsigned nb_pairs,
706  std::vector<acc_cond::rs_pair>& pairs,
707  std::vector<unsigned>& res,
708  std::vector<unsigned>& old) const;
709  public:
714  std::vector<unsigned>
715  states_on_acc_cycle_of(unsigned scc) const;
716  };
717 
718 
724  class SPOT_API scc_and_mark_filter
725  {
726  protected:
727  const scc_info* lower_si_;
728  unsigned lower_scc_;
729  acc_cond::mark_t cut_sets_;
730  const_twa_graph_ptr aut_;
731  acc_cond old_acc_;
732  bool restore_old_acc_ = false;
733 
735  filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
736  unsigned dst, void* data)
737  {
738  auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
739  if (d.lower_si_->scc_of(dst) != d.lower_scc_)
740  return scc_info::edge_filter_choice::ignore;
741  if (d.cut_sets_ & e.acc)
742  return scc_info::edge_filter_choice::cut;
743  return scc_info::edge_filter_choice::keep;
744  };
745 
747  filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data)
748  {
749  auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
750  if (d.cut_sets_ & e.acc)
751  return scc_info::edge_filter_choice::cut;
752  return scc_info::edge_filter_choice::keep;
753  };
754 
755  public:
761  scc_and_mark_filter(const scc_info& lower_si,
762  unsigned lower_scc,
763  acc_cond::mark_t cut_sets)
764  : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
765  aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
766  {
767  const void* data = lower_si.get_filter_data();
768  if (data)
769  {
770  auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
771  cut_sets_ |= d.cut_sets_;
772  }
773  }
774 
779  scc_and_mark_filter(const const_twa_graph_ptr& aut,
780  acc_cond::mark_t cut_sets)
781  : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
782  old_acc_(aut_->get_acceptance())
783  {
784  }
785 
786  ~scc_and_mark_filter()
787  {
788  restore_acceptance();
789  }
790 
791  void override_acceptance(const acc_cond& new_acc)
792  {
793  std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
794  restore_old_acc_ = true;
795  }
796 
797  void restore_acceptance()
798  {
799  if (!restore_old_acc_)
800  return;
801  std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
802  restore_old_acc_ = false;
803  }
804 
805  const_twa_graph_ptr get_aut() const
806  {
807  return aut_;
808  }
809 
810  unsigned start_state() const
811  {
812  if (lower_si_)
813  return lower_si_->one_state_of(lower_scc_);
814  return aut_->get_init_state_number();
815  }
816 
817  scc_info::edge_filter get_filter() const
818  {
819  if (lower_si_)
820  return filter_scc_and_mark_;
821  if (cut_sets_)
822  return filter_mark_;
823  return nullptr;
824  }
825  };
826 
827 
831  SPOT_API std::ostream&
832  dump_scc_info_dot(std::ostream& out,
833  const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
834 
835 }
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:373
scc_and_mark_filter(const scc_info &lower_si, unsigned lower_scc, acc_cond::mark_t cut_sets)
Specify how to restrict scc_info to some SCC and acceptance sets.
Definition: sccinfo.hh:761
edge_filter_choice(* edge_filter)(const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:407
Definition: sccinfo.hh:179
Storage for SCC related information.
Definition: sccinfo.hh:217
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:678
Definition: sccinfo.hh:69
scc_and_mark_filter(const const_twa_graph_ptr &aut, acc_cond::mark_t cut_sets)
Specify how to restrict scc_info to some acceptance sets.
Definition: sccinfo.hh:779
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:550
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:492
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:671
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:305
An acceptance condition.
Definition: acc.hh:58
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:448
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:257
scc_info(const scc_and_mark_filter &filt)
Create an scc_info map from some filter.
Definition: sccinfo.hh:465
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:582
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:405
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:267
Definition: twa.hh:1721
Definition: sccinfo.hh:32
Definition: sccinfo.hh:43
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:567
Graph-based representation of a TωA.
Definition: twagraph.hh:199
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