spot  2.12
sccinfo.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <vector>
22 #include <spot/twa/twagraph.hh>
23 #include <spot/twaalgos/emptiness.hh>
24 #include <spot/misc/bitvect.hh>
25 
26 namespace spot
27 {
28  class scc_info;
29 
56  enum class edge_filter_choice { keep, ignore, cut };
58  (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
59  void* filter_data);
61 
62  namespace internal
63  {
64  struct keep_all
65  {
66  template <typename Iterator>
67  bool operator()(Iterator, Iterator) const noexcept
68  {
69  return true;
70  }
71  };
72 
73  // Keep only transitions that have at least one destination in the
74  // current SCC.
76  {
77  private:
78  const std::vector<unsigned>& sccof_;
79  unsigned desired_scc_;
80  public:
81  keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
82  : sccof_(sccof), desired_scc_(desired_scc)
83  {
84  }
85 
86  template <typename Iterator>
87  bool operator()(Iterator begin, Iterator end) const noexcept
88  {
89  bool want = false;
90  while (begin != end)
91  if (sccof_[*begin++] == desired_scc_)
92  {
93  want = true;
94  break;
95  }
96  return want;
97  }
98  };
99 
100  template <typename Graph, typename Filter>
101  class SPOT_API scc_edge_iterator
102  {
103  public:
104  typedef typename std::conditional<std::is_const<Graph>::value,
105  const typename Graph::edge_storage_t,
106  typename Graph::edge_storage_t>::type
107  value_type;
108  typedef value_type& reference;
109  typedef value_type* pointer;
110  typedef std::ptrdiff_t difference_type;
111  typedef std::forward_iterator_tag iterator_category;
112 
113  typedef std::vector<unsigned>::const_iterator state_iterator;
114 
115  typedef typename std::conditional<std::is_const<Graph>::value,
116  const typename Graph::edge_vector_t,
117  typename Graph::edge_vector_t>::type
118  tv_t;
119 
120  typedef typename std::conditional<std::is_const<Graph>::value,
121  const typename Graph::state_vector,
122  typename Graph::state_vector>::type
123  sv_t;
124  typedef const typename Graph::dests_vector_t dv_t;
125  protected:
126 
127  state_iterator pos_;
128  state_iterator end_;
129  unsigned t_;
130  tv_t* tv_;
131  sv_t* sv_;
132  dv_t* dv_;
133 
134  Filter filt_;
135  edge_filter efilter_;
136  void* efilter_data_;
137 
138 
139  void inc_state_maybe_()
140  {
141  while (!t_ && (++pos_ != end_))
142  t_ = (*sv_)[*pos_].succ;
143  }
144 
145  void inc_()
146  {
147  t_ = (*tv_)[t_].next_succ;
148  inc_state_maybe_();
149  }
150 
151  // Do we ignore the current transition?
152  bool ignore_current()
153  {
154  unsigned dst = (*this)->dst;
155  if ((int)dst >= 0)
156  {
157  // Non-universal branching => a single destination.
158  if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
159  return true;
160  if (efilter_)
161  return efilter_((*tv_)[t_], dst, efilter_data_)
162  != edge_filter_choice::keep;
163  return false;
164  }
165  else
166  {
167  // Universal branching => multiple destinations.
168  const unsigned* d = dv_->data() + ~dst;
169  if (!filt_(d + 1, d + *d + 1))
170  return true;
171  if (efilter_)
172  {
173  // Keep the transition if at least one destination
174  // is not filtered.
175  const unsigned* end = d + *d + 1;
176  for (const unsigned* i = d + 1; i != end; ++i)
177  {
178  if (efilter_((*tv_)[t_], *i, efilter_data_)
179  == edge_filter_choice::keep)
180  return false;
181  return true;
182  }
183  }
184  return false;
185  }
186  }
187 
188  public:
189  scc_edge_iterator(state_iterator begin, state_iterator end,
190  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
191  edge_filter efilter, void* efilter_data) noexcept
192  : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
193  efilter_(efilter), efilter_data_(efilter_data)
194  {
195  if (pos_ == end_)
196  return;
197 
198  t_ = (*sv_)[*pos_].succ;
199  inc_state_maybe_();
200  while (pos_ != end_ && ignore_current())
201  inc_();
202  }
203 
204  scc_edge_iterator& operator++()
205  {
206  do
207  inc_();
208  while (pos_ != end_ && ignore_current());
209  return *this;
210  }
211 
212  scc_edge_iterator operator++(int)
213  {
214  scc_edge_iterator old = *this;
215  ++*this;
216  return old;
217  }
218 
219  bool operator==(scc_edge_iterator o) const
220  {
221  return pos_ == o.pos_ && t_ == o.t_;
222  }
223 
224  bool operator!=(scc_edge_iterator o) const
225  {
226  return pos_ != o.pos_ || t_ != o.t_;
227  }
228 
229  reference operator*() const
230  {
231  return (*tv_)[t_];
232  }
233 
234  pointer operator->() const
235  {
236  return &**this;
237  }
238  };
239 
240 
241  template <typename Graph, typename Filter>
242  class SPOT_API scc_edges
243  {
244  public:
246  typedef typename iter_t::tv_t tv_t;
247  typedef typename iter_t::sv_t sv_t;
248  typedef typename iter_t::dv_t dv_t;
249  typedef typename iter_t::state_iterator state_iterator;
250  private:
251  state_iterator begin_;
252  state_iterator end_;
253  tv_t* tv_;
254  sv_t* sv_;
255  dv_t* dv_;
256  Filter filt_;
257  edge_filter efilter_;
258  void* efilter_data_;
259  public:
260 
261  scc_edges(state_iterator begin, state_iterator end,
262  tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
263  edge_filter efilter, void* efilter_data) noexcept
264  : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
265  efilter_(efilter), efilter_data_(efilter_data)
266  {
267  }
268 
269  iter_t begin() const
270  {
271  return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
272  }
273 
274  iter_t end() const
275  {
276  return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr};
277  }
278  };
279  }
280 
281 
284  class SPOT_API scc_info_node
285  {
286  public:
287  typedef std::vector<unsigned> scc_succs;
288  friend class scc_info;
289  protected:
290  scc_succs succ_;
291  std::vector<unsigned> states_; // States of the component
292  unsigned one_state_;
293  acc_cond::mark_t acc_;
294  acc_cond::mark_t common_;
295  bool trivial_:1;
296  bool accepting_:1; // Necessarily accepting
297  bool rejecting_:1; // Necessarily rejecting
298  bool useful_:1;
299  public:
300  scc_info_node() noexcept:
301  acc_({}), trivial_(true), accepting_(false),
302  rejecting_(false), useful_(false)
303  {
304  }
305 
307  acc_cond::mark_t common, bool trivial) noexcept
308  : acc_(acc), common_(common),
309  trivial_(trivial), accepting_(false),
310  rejecting_(false), useful_(false)
311  {
312  }
313 
314  bool is_trivial() const
315  {
316  return trivial_;
317  }
318 
324  bool is_accepting() const
325  {
326  return accepting_;
327  }
328 
334  bool is_rejecting() const
335  {
336  return rejecting_;
337  }
338 
339  bool is_useful() const
340  {
341  return useful_;
342  }
343 
344  acc_cond::mark_t acc_marks() const
345  {
346  return acc_;
347  }
348 
349  acc_cond::mark_t common_marks() const
350  {
351  return common_;
352  }
353 
354  const std::vector<unsigned>& states() const
355  {
356  return states_;
357  }
358 
359  unsigned one_state() const
360  {
361  return one_state_;
362  }
363 
364  const scc_succs& succ() const
365  {
366  return succ_;
367  }
368  };
369 
372  enum class scc_info_options
373  {
377  NONE = 0,
382  STOP_ON_ACC = 1,
387  TRACK_STATES = 2,
391  TRACK_SUCCS = 4,
404  };
405 
406  inline
407  bool operator!(scc_info_options me)
408  {
409  return me == scc_info_options::NONE;
410  }
411 
412  inline
413  scc_info_options operator&(scc_info_options left, scc_info_options right)
414  {
415  typedef std::underlying_type_t<scc_info_options> ut;
416  return static_cast<scc_info_options>(static_cast<ut>(left)
417  & static_cast<ut>(right));
418  }
419 
420  inline
422  {
423  typedef std::underlying_type_t<scc_info_options> ut;
424  return static_cast<scc_info_options>(static_cast<ut>(left)
425  | static_cast<ut>(right));
426  }
427 
428  class SPOT_API scc_and_mark_filter;
429 
448  class SPOT_API scc_info
449  {
450  public:
451  // scc_node used to be an inner class, but Swig 3.0.10 does not
452  // support that yet.
453  typedef scc_info_node scc_node;
454  typedef scc_info_node::scc_succs scc_succs;
455 
456  // These types used to be defined here in Spot up to 2.9.
459 
460  protected:
461 
462  std::vector<unsigned> sccof_;
463  std::vector<scc_node> node_;
464  const_twa_graph_ptr aut_;
465  unsigned initial_state_;
466  edge_filter filter_;
467  void* filter_data_;
468  int one_acc_scc_ = -1;
469  scc_info_options options_;
470 
471  // Update the useful_ bits. Called automatically.
472  void determine_usefulness();
473 
474  const scc_node& node(unsigned scc) const
475  {
476  return node_[scc];
477  }
478 
479 #ifndef SWIG
480  private:
481  [[noreturn]] static void report_need_track_states();
482  [[noreturn]] static void report_need_track_succs();
483  [[noreturn]] static void report_incompatible_stop_on_acc();
484 #endif
485 
486  public:
489  scc_info(const_twa_graph_ptr aut,
490  // Use ~0U instead of -1U to work around a bug in Swig.
491  // See https://github.com/swig/swig/issues/993
492  unsigned initial_state = ~0U,
493  edge_filter filter = nullptr,
494  void* filter_data = nullptr,
496 
497  scc_info(const_twa_graph_ptr aut, scc_info_options options)
498  : scc_info(aut, ~0U, nullptr, nullptr, options)
499  {
500  }
502 
510  // we separate the two functions so that we can rename
511  // scc_info(x,options) into scc_info_with_options(x,options) in Python.
512  // Otherwise calling scc_info(aut,options) can be confused with
513  // scc_info(aut,initial_state).
515  : scc_info(filt, scc_info_options::ALL)
516  {
517  }
519 
520  const_twa_graph_ptr get_aut() const
521  {
522  return aut_;
523  }
524 
525  scc_info_options get_options() const
526  {
527  return options_;
528  }
529 
530  edge_filter get_filter() const
531  {
532  return filter_;
533  }
534 
535  void* get_filter_data() const
536  {
537  return filter_data_;
538  }
539 
540  unsigned scc_count() const
541  {
542  return node_.size();
543  }
544 
553  int one_accepting_scc() const
554  {
555  return one_acc_scc_;
556  }
557 
558  bool reachable_state(unsigned st) const
559  {
560  return scc_of(st) != -1U;
561  }
562 
563  unsigned scc_of(unsigned st) const
564  {
565  return sccof_[st];
566  }
567 
568  std::vector<scc_node>::const_iterator begin() const
569  {
570  return node_.begin();
571  }
572 
573  std::vector<scc_node>::const_iterator end() const
574  {
575  return node_.end();
576  }
577 
578  std::vector<scc_node>::const_iterator cbegin() const
579  {
580  return node_.cbegin();
581  }
582 
583  std::vector<scc_node>::const_iterator cend() const
584  {
585  return node_.cend();
586  }
587 
588  std::vector<scc_node>::const_reverse_iterator rbegin() const
589  {
590  return node_.rbegin();
591  }
592 
593  std::vector<scc_node>::const_reverse_iterator rend() const
594  {
595  return node_.rend();
596  }
597 
598  const std::vector<unsigned>& states_of(unsigned scc) const
599  {
600  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
601  report_need_track_states();
602  return node(scc).states();
603  }
604 
610  internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
611  edges_of(unsigned scc) const
612  {
613  auto& states = states_of(scc);
614  return {states.begin(), states.end(),
615  &aut_->edge_vector(), &aut_->states(),
616  &aut_->get_graph().dests_vector(),
617  internal::keep_all(), filter_, const_cast<void*>(filter_data_)};
618  }
619 
628  inner_edges_of(unsigned scc) const
629  {
630  auto& states = states_of(scc);
631  return {states.begin(), states.end(),
632  &aut_->edge_vector(), &aut_->states(),
633  &aut_->get_graph().dests_vector(),
634  internal::keep_inner_scc(sccof_, scc), filter_,
635  const_cast<void*>(filter_data_)};
636  }
637 
638  unsigned one_state_of(unsigned scc) const
639  {
640  return node(scc).one_state();
641  }
642 
644  unsigned initial() const
645  {
646  SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
647  return scc_of(initial_state_);
648  }
649 
650  const scc_succs& succ(unsigned scc) const
651  {
652  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
653  report_need_track_succs();
654  return node(scc).succ();
655  }
656 
657  bool is_trivial(unsigned scc) const
658  {
659  return node(scc).is_trivial();
660  }
661 
662  SPOT_DEPRECATED("use acc_sets_of() instead")
663  acc_cond::mark_t acc(unsigned scc) const
664  {
665  return acc_sets_of(scc);
666  }
667 
668  bool is_accepting_scc(unsigned scc) const
669  {
670  return node(scc).is_accepting();
671  }
672 
673  bool is_rejecting_scc(unsigned scc) const
674  {
675  return node(scc).is_rejecting();
676  }
677 
680  bool is_maximally_accepting_scc(unsigned scc) const
681  {
682  return aut_->acc().accepting(acc_sets_of(scc));
683  }
684 
690 
695  bool check_scc_emptiness(unsigned n) const;
696 
704  void get_accepting_run(unsigned scc, twa_run_ptr r) const;
705 
706  bool is_useful_scc(unsigned scc) const
707  {
708  if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
709  report_incompatible_stop_on_acc();
710  if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
711  report_need_track_succs();
712  return node(scc).is_useful();
713  }
714 
715  bool is_useful_state(unsigned st) const
716  {
717  return reachable_state(st) && is_useful_scc(scc_of(st));
718  }
719 
722  std::vector<std::set<acc_cond::mark_t>> marks() const;
723  std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
724 
725  // Same as above, with old names.
726  SPOT_DEPRECATED("use marks() instead")
727  std::vector<std::set<acc_cond::mark_t>> used_acc() const
728  {
729  return marks();
730  }
731  SPOT_DEPRECATED("use marks_of() instead")
732  std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
733  {
734  return marks_of(scc);
735  }
736 
740  acc_cond::mark_t acc_sets_of(unsigned scc) const
741  {
742  return node(scc).acc_marks();
743  }
744 
747  acc_cond::mark_t common_sets_of(unsigned scc) const
748  {
749  return node(scc).common_marks();
750  }
751 
752  std::vector<bool> weak_sccs() const;
753 
754  bdd scc_ap_support(unsigned scc) const;
755 
781  std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
782  acc_cond::mark_t sets,
783  bool preserve_names = false) const;
784  protected:
786  void
788  acc_cond::mark_t all_fin,
789  acc_cond::mark_t all_inf,
790  unsigned nb_pairs,
791  std::vector<acc_cond::rs_pair>& pairs,
792  std::vector<unsigned>& res,
793  std::vector<unsigned>& old) const;
794  public:
799  std::vector<unsigned>
800  states_on_acc_cycle_of(unsigned scc) const;
801  };
802 
803 
809  class SPOT_API scc_and_mark_filter
810  {
811  protected:
812  const scc_info* lower_si_;
813  unsigned lower_scc_;
814  acc_cond::mark_t cut_sets_;
815  const_twa_graph_ptr aut_;
816  acc_cond old_acc_;
817  bool restore_old_acc_ = false;
818  const bitvect* keep_ = nullptr;
819 
821  filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
822  unsigned dst, void* data);
823 
825  filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data);
826 
828  filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t& e,
829  unsigned dst, void* data);
830 
831  public:
837  scc_and_mark_filter(const scc_info& lower_si,
838  unsigned lower_scc,
839  acc_cond::mark_t cut_sets)
840  : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
841  aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
842  {
843  auto f = lower_si.get_filter();
844  if (f == &filter_mark_
845  || f == &filter_scc_and_mark_
846  || f == &filter_scc_and_mark_and_edges_)
847  {
848  const void* data = lower_si.get_filter_data();
849  auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
850  cut_sets_ |= d.cut_sets_;
851  if (f == &filter_scc_and_mark_and_edges_)
852  keep_ = d.keep_;
853  }
854  }
855 
856  scc_and_mark_filter(const scc_info& lower_si,
857  unsigned lower_scc,
858  acc_cond::mark_t cut_sets,
859  const bitvect& keep)
860  : scc_and_mark_filter(lower_si, lower_scc, cut_sets)
861  {
862  keep_ = &keep;
863  }
864 
869  scc_and_mark_filter(const const_twa_graph_ptr& aut,
870  acc_cond::mark_t cut_sets)
871  : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
872  old_acc_(aut_->get_acceptance())
873  {
874  }
875 
877  {
878  restore_acceptance();
879  }
880 
881  void override_acceptance(const acc_cond& new_acc)
882  {
883  std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
884  restore_old_acc_ = true;
885  }
886 
887  void restore_acceptance()
888  {
889  if (!restore_old_acc_)
890  return;
891  std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
892  restore_old_acc_ = false;
893  }
894 
895  const_twa_graph_ptr get_aut() const
896  {
897  return aut_;
898  }
899 
900  unsigned start_state() const
901  {
902  if (lower_si_)
903  return lower_si_->one_state_of(lower_scc_);
904  return aut_->get_init_state_number();
905  }
906 
907  scc_info::edge_filter get_filter() const
908  {
909  if (keep_)
910  return filter_scc_and_mark_and_edges_;
911  if (lower_si_)
912  return filter_scc_and_mark_;
913  if (cut_sets_)
914  return filter_mark_;
915  return nullptr;
916  }
917  };
918 
922  SPOT_API std::ostream&
923  dump_scc_info_dot(std::ostream& out,
924  const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
925 
926 }
An acceptance condition.
Definition: acc.hh:61
A bit vector.
Definition: bitvect.hh:51
Definition: sccinfo.hh:102
Definition: sccinfo.hh:243
Create a filter for SCC and marks.
Definition: sccinfo.hh:810
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:869
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:837
Storage for SCC related information.
Definition: sccinfo.hh:285
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:334
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:324
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:449
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:497
bool is_maximally_accepting_scc(unsigned scc) const
Whether a cycle going through all edges of the SCC is accepting.
Definition: sccinfo.hh:680
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:553
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:644
std::vector< unsigned > states_on_acc_cycle_of(unsigned scc) const
: Get all states visited by any accepting cycles of the 'scc'.
bool check_scc_emptiness(unsigned n) const
Recompute whether an SCC is accepting or not.
void determine_unknown_acceptance()
Study the SCCs that are currently reported neither as accepting nor as rejecting because of the prese...
void get_accepting_run(unsigned scc, twa_run_ptr r) const
Retrieves an accepting run of the automaton whose cycle is in the SCC.
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:611
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:628
scc_info(const_twa_graph_ptr aut, unsigned initial_state=~0U, edge_filter filter=nullptr, void *filter_data=nullptr, scc_info_options options=scc_info_options::ALL)
Create the scc_info map for aut.
scc_info(const scc_and_mark_filter &filt)
Create an scc_info map from some filter.
Definition: sccinfo.hh:514
void states_on_acc_cycle_of_rec(unsigned scc, acc_cond::mark_t all_fin, acc_cond::mark_t all_inf, unsigned nb_pairs, std::vector< acc_cond::rs_pair > &pairs, std::vector< unsigned > &res, std::vector< unsigned > &old) const
: Recursive function used by states_on_acc_cycle_of().
std::vector< std::set< acc_cond::mark_t > > marks() const
Returns, for each accepting SCC, the set of all marks appearing in it.
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:747
std::vector< twa_graph_ptr > split_on_sets(unsigned scc, acc_cond::mark_t sets, bool preserve_names=false) const
Split an SCC into multiple automata separated by some acceptance sets.
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:740
scc_info(const scc_and_mark_filter &filt, scc_info_options options)
Create an scc_info map from some filter.
@ U
until
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:58
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:373
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:56
@ ALL
Default behavior: explore everything and track states and succs.
Definition: automata.hh:26
std::ostream & dump_scc_info_dot(std::ostream &out, const_twa_graph_ptr aut, scc_info *sccinfo=nullptr)
Dump the SCC graph of aut on out.
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:130
An acceptance mark.
Definition: acc.hh:84
Definition: graph.hh:187
Definition: sccinfo.hh:65
Definition: sccinfo.hh:76

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