spot 2.11.2.dev
sccinfo.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2014-2021 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#include <spot/misc/bitvect.hh>
26
27namespace spot
28{
29 class scc_info;
30
57 enum class edge_filter_choice { keep, ignore, cut };
59 (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
60 void* filter_data);
62
63 namespace internal
64 {
65 struct keep_all
66 {
67 template <typename Iterator>
68 bool operator()(Iterator, Iterator) const noexcept
69 {
70 return true;
71 }
72 };
73
74 // Keep only transitions that have at least one destination in the
75 // current SCC.
77 {
78 private:
79 const std::vector<unsigned>& sccof_;
80 unsigned desired_scc_;
81 public:
82 keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
83 : sccof_(sccof), desired_scc_(desired_scc)
84 {
85 }
86
87 template <typename Iterator>
88 bool operator()(Iterator begin, Iterator end) const noexcept
89 {
90 bool want = false;
91 while (begin != end)
92 if (sccof_[*begin++] == desired_scc_)
93 {
94 want = true;
95 break;
96 }
97 return want;
98 }
99 };
100
101 template <typename Graph, typename Filter>
102 class SPOT_API scc_edge_iterator
103 {
104 public:
105 typedef typename std::conditional<std::is_const<Graph>::value,
106 const typename Graph::edge_storage_t,
107 typename Graph::edge_storage_t>::type
108 value_type;
109 typedef value_type& reference;
110 typedef value_type* pointer;
111 typedef std::ptrdiff_t difference_type;
112 typedef std::forward_iterator_tag iterator_category;
113
114 typedef std::vector<unsigned>::const_iterator state_iterator;
115
116 typedef typename std::conditional<std::is_const<Graph>::value,
117 const typename Graph::edge_vector_t,
118 typename Graph::edge_vector_t>::type
119 tv_t;
120
121 typedef typename std::conditional<std::is_const<Graph>::value,
122 const typename Graph::state_vector,
123 typename Graph::state_vector>::type
124 sv_t;
125 typedef const typename Graph::dests_vector_t dv_t;
126 protected:
127
128 state_iterator pos_;
129 state_iterator end_;
130 unsigned t_;
131 tv_t* tv_;
132 sv_t* sv_;
133 dv_t* dv_;
134
135 Filter filt_;
136 edge_filter efilter_;
137 void* efilter_data_;
138
139
140 void inc_state_maybe_()
141 {
142 while (!t_ && (++pos_ != end_))
143 t_ = (*sv_)[*pos_].succ;
144 }
145
146 void inc_()
147 {
148 t_ = (*tv_)[t_].next_succ;
149 inc_state_maybe_();
150 }
151
152 // Do we ignore the current transition?
153 bool ignore_current()
154 {
155 unsigned dst = (*this)->dst;
156 if ((int)dst >= 0)
157 {
158 // Non-universal branching => a single destination.
159 if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
160 return true;
161 if (efilter_)
162 return efilter_((*tv_)[t_], dst, efilter_data_)
163 != edge_filter_choice::keep;
164 return false;
165 }
166 else
167 {
168 // Universal branching => multiple destinations.
169 const unsigned* d = dv_->data() + ~dst;
170 if (!filt_(d + 1, d + *d + 1))
171 return true;
172 if (efilter_)
173 {
174 // Keep the transition if at least one destination
175 // is not filtered.
176 const unsigned* end = d + *d + 1;
177 for (const unsigned* i = d + 1; i != end; ++i)
178 {
179 if (efilter_((*tv_)[t_], *i, efilter_data_)
180 == edge_filter_choice::keep)
181 return false;
182 return true;
183 }
184 }
185 return false;
186 }
187 }
188
189 public:
190 scc_edge_iterator(state_iterator begin, state_iterator end,
191 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
192 edge_filter efilter, void* efilter_data) noexcept
193 : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
194 efilter_(efilter), efilter_data_(efilter_data)
195 {
196 if (pos_ == end_)
197 return;
198
199 t_ = (*sv_)[*pos_].succ;
200 inc_state_maybe_();
201 while (pos_ != end_ && ignore_current())
202 inc_();
203 }
204
205 scc_edge_iterator& operator++()
206 {
207 do
208 inc_();
209 while (pos_ != end_ && ignore_current());
210 return *this;
211 }
212
213 scc_edge_iterator operator++(int)
214 {
215 scc_edge_iterator old = *this;
216 ++*this;
217 return old;
218 }
219
220 bool operator==(scc_edge_iterator o) const
221 {
222 return pos_ == o.pos_ && t_ == o.t_;
223 }
224
225 bool operator!=(scc_edge_iterator o) const
226 {
227 return pos_ != o.pos_ || t_ != o.t_;
228 }
229
230 reference operator*() const
231 {
232 return (*tv_)[t_];
233 }
234
235 pointer operator->() const
236 {
237 return &**this;
238 }
239 };
240
241
242 template <typename Graph, typename Filter>
243 class SPOT_API scc_edges
244 {
245 public:
247 typedef typename iter_t::tv_t tv_t;
248 typedef typename iter_t::sv_t sv_t;
249 typedef typename iter_t::dv_t dv_t;
250 typedef typename iter_t::state_iterator state_iterator;
251 private:
252 state_iterator begin_;
253 state_iterator end_;
254 tv_t* tv_;
255 sv_t* sv_;
256 dv_t* dv_;
257 Filter filt_;
258 edge_filter efilter_;
259 void* efilter_data_;
260 public:
261
262 scc_edges(state_iterator begin, state_iterator end,
263 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
264 edge_filter efilter, void* efilter_data) noexcept
265 : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
266 efilter_(efilter), efilter_data_(efilter_data)
267 {
268 }
269
270 iter_t begin() const
271 {
272 return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
273 }
274
275 iter_t end() const
276 {
277 return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr};
278 }
279 };
280 }
281
282
285 class SPOT_API scc_info_node
286 {
287 public:
288 typedef std::vector<unsigned> scc_succs;
289 friend class scc_info;
290 protected:
291 scc_succs succ_;
292 std::vector<unsigned> states_; // States of the component
293 unsigned one_state_;
294 acc_cond::mark_t acc_;
295 acc_cond::mark_t common_;
296 bool trivial_:1;
297 bool accepting_:1; // Necessarily accepting
298 bool rejecting_:1; // Necessarily rejecting
299 bool useful_:1;
300 public:
301 scc_info_node() noexcept:
302 acc_({}), trivial_(true), accepting_(false),
303 rejecting_(false), useful_(false)
304 {
305 }
306
308 acc_cond::mark_t common, bool trivial) noexcept
309 : acc_(acc), common_(common),
310 trivial_(trivial), accepting_(false),
311 rejecting_(false), useful_(false)
312 {
313 }
314
315 bool is_trivial() const
316 {
317 return trivial_;
318 }
319
325 bool is_accepting() const
326 {
327 return accepting_;
328 }
329
335 bool is_rejecting() const
336 {
337 return rejecting_;
338 }
339
340 bool is_useful() const
341 {
342 return useful_;
343 }
344
345 acc_cond::mark_t acc_marks() const
346 {
347 return acc_;
348 }
349
350 acc_cond::mark_t common_marks() const
351 {
352 return common_;
353 }
354
355 const std::vector<unsigned>& states() const
356 {
357 return states_;
358 }
359
360 unsigned one_state() const
361 {
362 return one_state_;
363 }
364
365 const scc_succs& succ() const
366 {
367 return succ_;
368 }
369 };
370
374 {
378 NONE = 0,
383 STOP_ON_ACC = 1,
388 TRACK_STATES = 2,
392 TRACK_SUCCS = 4,
398 };
399
400 inline
401 bool operator!(scc_info_options me)
402 {
403 return me == scc_info_options::NONE;
404 }
405
406 inline
408 {
409 typedef std::underlying_type_t<scc_info_options> ut;
410 return static_cast<scc_info_options>(static_cast<ut>(left)
411 & static_cast<ut>(right));
412 }
413
414 inline
416 {
417 typedef std::underlying_type_t<scc_info_options> ut;
418 return static_cast<scc_info_options>(static_cast<ut>(left)
419 | static_cast<ut>(right));
420 }
421
422 class SPOT_API scc_and_mark_filter;
423
442 class SPOT_API scc_info
443 {
444 public:
445 // scc_node used to be an inner class, but Swig 3.0.10 does not
446 // support that yet.
447 typedef scc_info_node scc_node;
448 typedef scc_info_node::scc_succs scc_succs;
449
450 // These types used to be defined here in Spot up to 2.9.
453
454 protected:
455
456 std::vector<unsigned> sccof_;
457 std::vector<scc_node> node_;
458 const_twa_graph_ptr aut_;
459 unsigned initial_state_;
460 edge_filter filter_;
461 void* filter_data_;
462 int one_acc_scc_ = -1;
463 scc_info_options options_;
464
465 // Update the useful_ bits. Called automatically.
466 void determine_usefulness();
467
468 const scc_node& node(unsigned scc) const
469 {
470 return node_[scc];
471 }
472
473#ifndef SWIG
474 private:
475 [[noreturn]] static void report_need_track_states();
476 [[noreturn]] static void report_need_track_succs();
477 [[noreturn]] static void report_incompatible_stop_on_acc();
478#endif
479
480 public:
483 scc_info(const_twa_graph_ptr aut,
484 // Use ~0U instead of -1U to work around a bug in Swig.
485 // See https://github.com/swig/swig/issues/993
486 unsigned initial_state = ~0U,
487 edge_filter filter = nullptr,
488 void* filter_data = nullptr,
490
491 scc_info(const_twa_graph_ptr aut, scc_info_options options)
492 : scc_info(aut, ~0U, nullptr, nullptr, options)
493 {
494 }
496
504 // we separate the two functions so that we can rename
505 // scc_info(x,options) into scc_info_with_options(x,options) in Python.
506 // Otherwrise calling scc_info(aut,options) can be confused with
507 // scc_info(aut,initial_state).
510 {
511 }
513
514 const_twa_graph_ptr get_aut() const
515 {
516 return aut_;
517 }
518
519 scc_info_options get_options() const
520 {
521 return options_;
522 }
523
524 edge_filter get_filter() const
525 {
526 return filter_;
527 }
528
529 void* get_filter_data() const
530 {
531 return filter_data_;
532 }
533
534 unsigned scc_count() const
535 {
536 return node_.size();
537 }
538
548 {
549 return one_acc_scc_;
550 }
551
552 bool reachable_state(unsigned st) const
553 {
554 return scc_of(st) != -1U;
555 }
556
557 unsigned scc_of(unsigned st) const
558 {
559 return sccof_[st];
560 }
561
562 std::vector<scc_node>::const_iterator begin() const
563 {
564 return node_.begin();
565 }
566
567 std::vector<scc_node>::const_iterator end() const
568 {
569 return node_.end();
570 }
571
572 std::vector<scc_node>::const_iterator cbegin() const
573 {
574 return node_.cbegin();
575 }
576
577 std::vector<scc_node>::const_iterator cend() const
578 {
579 return node_.cend();
580 }
581
582 std::vector<scc_node>::const_reverse_iterator rbegin() const
583 {
584 return node_.rbegin();
585 }
586
587 std::vector<scc_node>::const_reverse_iterator rend() const
588 {
589 return node_.rend();
590 }
591
592 const std::vector<unsigned>& states_of(unsigned scc) const
593 {
594 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
595 report_need_track_states();
596 return node(scc).states();
597 }
598
604 internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
605 edges_of(unsigned scc) const
606 {
607 auto& states = states_of(scc);
608 return {states.begin(), states.end(),
609 &aut_->edge_vector(), &aut_->states(),
610 &aut_->get_graph().dests_vector(),
611 internal::keep_all(), filter_, const_cast<void*>(filter_data_)};
612 }
613
622 inner_edges_of(unsigned scc) const
623 {
624 auto& states = states_of(scc);
625 return {states.begin(), states.end(),
626 &aut_->edge_vector(), &aut_->states(),
627 &aut_->get_graph().dests_vector(),
628 internal::keep_inner_scc(sccof_, scc), filter_,
629 const_cast<void*>(filter_data_)};
630 }
631
632 unsigned one_state_of(unsigned scc) const
633 {
634 return node(scc).one_state();
635 }
636
638 unsigned initial() const
639 {
640 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
641 return scc_of(initial_state_);
642 }
643
644 const scc_succs& succ(unsigned scc) const
645 {
646 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
647 report_need_track_succs();
648 return node(scc).succ();
649 }
650
651 bool is_trivial(unsigned scc) const
652 {
653 return node(scc).is_trivial();
654 }
655
656 SPOT_DEPRECATED("use acc_sets_of() instead")
657 acc_cond::mark_t acc(unsigned scc) const
658 {
659 return acc_sets_of(scc);
660 }
661
662 bool is_accepting_scc(unsigned scc) const
663 {
664 return node(scc).is_accepting();
665 }
666
667 bool is_rejecting_scc(unsigned scc) const
668 {
669 return node(scc).is_rejecting();
670 }
671
674 bool is_maximally_accepting_scc(unsigned scc) const
675 {
676 return aut_->acc().accepting(acc_sets_of(scc));
677 }
678
684
689 bool check_scc_emptiness(unsigned n) const;
690
698 void get_accepting_run(unsigned scc, twa_run_ptr r) const;
699
700 bool is_useful_scc(unsigned scc) const
701 {
702 if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
703 report_incompatible_stop_on_acc();
704 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
705 report_need_track_succs();
706 return node(scc).is_useful();
707 }
708
709 bool is_useful_state(unsigned st) const
710 {
711 return reachable_state(st) && is_useful_scc(scc_of(st));
712 }
713
716 std::vector<std::set<acc_cond::mark_t>> marks() const;
717 std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
718
719 // Same as above, with old names.
720 SPOT_DEPRECATED("use marks() instead")
721 std::vector<std::set<acc_cond::mark_t>> used_acc() const
722 {
723 return marks();
724 }
725 SPOT_DEPRECATED("use marks_of() instead")
726 std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
727 {
728 return marks_of(scc);
729 }
730
734 acc_cond::mark_t acc_sets_of(unsigned scc) const
735 {
736 return node(scc).acc_marks();
737 }
738
742 {
743 return node(scc).common_marks();
744 }
745
746 std::vector<bool> weak_sccs() const;
747
748 bdd scc_ap_support(unsigned scc) const;
749
759 std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
760 acc_cond::mark_t sets,
761 bool preserve_names = false) const;
762 protected:
764 void
766 acc_cond::mark_t all_fin,
767 acc_cond::mark_t all_inf,
768 unsigned nb_pairs,
769 std::vector<acc_cond::rs_pair>& pairs,
770 std::vector<unsigned>& res,
771 std::vector<unsigned>& old) const;
772 public:
777 std::vector<unsigned>
778 states_on_acc_cycle_of(unsigned scc) const;
779 };
780
781
787 class SPOT_API scc_and_mark_filter
788 {
789 protected:
790 const scc_info* lower_si_;
791 unsigned lower_scc_;
792 acc_cond::mark_t cut_sets_;
793 const_twa_graph_ptr aut_;
794 acc_cond old_acc_;
795 bool restore_old_acc_ = false;
796 const bitvect* keep_ = nullptr;
797
799 filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
800 unsigned dst, void* data);
801
803 filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data);
804
806 filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t& e,
807 unsigned dst, void* data);
808
809 public:
816 unsigned lower_scc,
817 acc_cond::mark_t cut_sets)
818 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
819 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
820 {
821 auto f = lower_si.get_filter();
822 if (f == &filter_mark_
823 || f == &filter_scc_and_mark_
824 || f == &filter_scc_and_mark_and_edges_)
825 {
826 const void* data = lower_si.get_filter_data();
827 auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
828 cut_sets_ |= d.cut_sets_;
829 if (f == &filter_scc_and_mark_and_edges_)
830 keep_ = d.keep_;
831 }
832 }
833
834 scc_and_mark_filter(const scc_info& lower_si,
835 unsigned lower_scc,
836 acc_cond::mark_t cut_sets,
837 const bitvect& keep)
838 : scc_and_mark_filter(lower_si, lower_scc, cut_sets)
839 {
840 keep_ = &keep;
841 }
842
847 scc_and_mark_filter(const const_twa_graph_ptr& aut,
848 acc_cond::mark_t cut_sets)
849 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
850 old_acc_(aut_->get_acceptance())
851 {
852 }
853
855 {
856 restore_acceptance();
857 }
858
859 void override_acceptance(const acc_cond& new_acc)
860 {
861 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
862 restore_old_acc_ = true;
863 }
864
865 void restore_acceptance()
866 {
867 if (!restore_old_acc_)
868 return;
869 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
870 restore_old_acc_ = false;
871 }
872
873 const_twa_graph_ptr get_aut() const
874 {
875 return aut_;
876 }
877
878 unsigned start_state() const
879 {
880 if (lower_si_)
881 return lower_si_->one_state_of(lower_scc_);
882 return aut_->get_init_state_number();
883 }
884
885 scc_info::edge_filter get_filter() const
886 {
887 if (keep_)
888 return filter_scc_and_mark_and_edges_;
889 if (lower_si_)
890 return filter_scc_and_mark_;
891 if (cut_sets_)
892 return filter_mark_;
893 return nullptr;
894 }
895 };
896
900 SPOT_API std::ostream&
901 dump_scc_info_dot(std::ostream& out,
902 const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
903
904}
An acceptance condition.
Definition: acc.hh:62
A bit vector.
Definition: bitvect.hh:52
Definition: sccinfo.hh:103
Definition: sccinfo.hh:244
Create a filter for SCC and marks.
Definition: sccinfo.hh:788
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:847
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:815
Storage for SCC related information.
Definition: sccinfo.hh:286
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:335
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:325
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:443
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:491
bool is_maximally_accepting_scc(unsigned scc) const
Whether a cycle going through all edges of the SCC is accepting.
Definition: sccinfo.hh:674
std::vector< std::set< acc_cond::mark_t > > marks() const
Returns, for each accepting SCC, the set of all marks appearing in it.
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:547
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:638
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:622
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.
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:508
std::vector< unsigned > states_on_acc_cycle_of(unsigned scc) const
: Get all states visited by any accepting cycles of the 'scc'.
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().
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:741
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:605
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:734
scc_info(const scc_and_mark_filter &filt, scc_info_options options)
Create an scc_info map from some filter.
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.
@ U
until
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...
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:59
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:374
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:57
@ ALL
Default behavior: explore everything and track states and succs.
Definition: automata.hh:27
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:131
An acceptance mark.
Definition: acc.hh:90
Definition: graph.hh:188
Definition: sccinfo.hh:66
Definition: sccinfo.hh:77

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