spot 2.11.6.dev
Loading...
Searching...
No Matches
sccinfo.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2014-2021, 2023 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,
405 };
406
407 inline
408 bool operator!(scc_info_options me)
409 {
410 return me == scc_info_options::NONE;
411 }
412
413 inline
415 {
416 typedef std::underlying_type_t<scc_info_options> ut;
417 return static_cast<scc_info_options>(static_cast<ut>(left)
418 & static_cast<ut>(right));
419 }
420
421 inline
423 {
424 typedef std::underlying_type_t<scc_info_options> ut;
425 return static_cast<scc_info_options>(static_cast<ut>(left)
426 | static_cast<ut>(right));
427 }
428
429 class SPOT_API scc_and_mark_filter;
430
449 class SPOT_API scc_info
450 {
451 public:
452 // scc_node used to be an inner class, but Swig 3.0.10 does not
453 // support that yet.
454 typedef scc_info_node scc_node;
455 typedef scc_info_node::scc_succs scc_succs;
456
457 // These types used to be defined here in Spot up to 2.9.
459 typedef spot::edge_filter edge_filter;
460
461 protected:
462
463 std::vector<unsigned> sccof_;
464 std::vector<scc_node> node_;
465 const_twa_graph_ptr aut_;
466 unsigned initial_state_;
467 edge_filter filter_;
468 void* filter_data_;
469 int one_acc_scc_ = -1;
470 scc_info_options options_;
471
472 // Update the useful_ bits. Called automatically.
473 void determine_usefulness();
474
475 const scc_node& node(unsigned scc) const
476 {
477 return node_[scc];
478 }
479
480#ifndef SWIG
481 private:
482 [[noreturn]] static void report_need_track_states();
483 [[noreturn]] static void report_need_track_succs();
484 [[noreturn]] static void report_incompatible_stop_on_acc();
485#endif
486
487 public:
490 scc_info(const_twa_graph_ptr aut,
491 // Use ~0U instead of -1U to work around a bug in Swig.
492 // See https://github.com/swig/swig/issues/993
493 unsigned initial_state = ~0U,
494 edge_filter filter = nullptr,
495 void* filter_data = nullptr,
496 scc_info_options options = scc_info_options::ALL);
497
498 scc_info(const_twa_graph_ptr aut, scc_info_options options)
499 : scc_info(aut, ~0U, nullptr, nullptr, options)
500 {
501 }
503
511 // we separate the two functions so that we can rename
512 // scc_info(x,options) into scc_info_with_options(x,options) in Python.
513 // Otherwrise calling scc_info(aut,options) can be confused with
514 // scc_info(aut,initial_state).
517 {
518 }
520
521 const_twa_graph_ptr get_aut() const
522 {
523 return aut_;
524 }
525
526 scc_info_options get_options() const
527 {
528 return options_;
529 }
530
531 edge_filter get_filter() const
532 {
533 return filter_;
534 }
535
536 void* get_filter_data() const
537 {
538 return filter_data_;
539 }
540
541 unsigned scc_count() const
542 {
543 return node_.size();
544 }
545
555 {
556 return one_acc_scc_;
557 }
558
559 bool reachable_state(unsigned st) const
560 {
561 return scc_of(st) != -1U;
562 }
563
564 unsigned scc_of(unsigned st) const
565 {
566 return sccof_[st];
567 }
568
569 std::vector<scc_node>::const_iterator begin() const
570 {
571 return node_.begin();
572 }
573
574 std::vector<scc_node>::const_iterator end() const
575 {
576 return node_.end();
577 }
578
579 std::vector<scc_node>::const_iterator cbegin() const
580 {
581 return node_.cbegin();
582 }
583
584 std::vector<scc_node>::const_iterator cend() const
585 {
586 return node_.cend();
587 }
588
589 std::vector<scc_node>::const_reverse_iterator rbegin() const
590 {
591 return node_.rbegin();
592 }
593
594 std::vector<scc_node>::const_reverse_iterator rend() const
595 {
596 return node_.rend();
597 }
598
599 const std::vector<unsigned>& states_of(unsigned scc) const
600 {
601 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
602 report_need_track_states();
603 return node(scc).states();
604 }
605
611 internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
612 edges_of(unsigned scc) const
613 {
614 auto& states = states_of(scc);
615 return {states.begin(), states.end(),
616 &aut_->edge_vector(), &aut_->states(),
617 &aut_->get_graph().dests_vector(),
618 internal::keep_all(), filter_, const_cast<void*>(filter_data_)};
619 }
620
629 inner_edges_of(unsigned scc) const
630 {
631 auto& states = states_of(scc);
632 return {states.begin(), states.end(),
633 &aut_->edge_vector(), &aut_->states(),
634 &aut_->get_graph().dests_vector(),
635 internal::keep_inner_scc(sccof_, scc), filter_,
636 const_cast<void*>(filter_data_)};
637 }
638
639 unsigned one_state_of(unsigned scc) const
640 {
641 return node(scc).one_state();
642 }
643
645 unsigned initial() const
646 {
647 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
648 return scc_of(initial_state_);
649 }
650
651 const scc_succs& succ(unsigned scc) const
652 {
653 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
654 report_need_track_succs();
655 return node(scc).succ();
656 }
657
658 bool is_trivial(unsigned scc) const
659 {
660 return node(scc).is_trivial();
661 }
662
663 SPOT_DEPRECATED("use acc_sets_of() instead")
664 acc_cond::mark_t acc(unsigned scc) const
665 {
666 return acc_sets_of(scc);
667 }
668
669 bool is_accepting_scc(unsigned scc) const
670 {
671 return node(scc).is_accepting();
672 }
673
674 bool is_rejecting_scc(unsigned scc) const
675 {
676 return node(scc).is_rejecting();
677 }
678
681 bool is_maximally_accepting_scc(unsigned scc) const
682 {
683 return aut_->acc().accepting(acc_sets_of(scc));
684 }
685
691
696 bool check_scc_emptiness(unsigned n) const;
697
705 void get_accepting_run(unsigned scc, twa_run_ptr r) const;
706
707 bool is_useful_scc(unsigned scc) const
708 {
709 if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
710 report_incompatible_stop_on_acc();
711 if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
712 report_need_track_succs();
713 return node(scc).is_useful();
714 }
715
716 bool is_useful_state(unsigned st) const
717 {
718 return reachable_state(st) && is_useful_scc(scc_of(st));
719 }
720
723 std::vector<std::set<acc_cond::mark_t>> marks() const;
724 std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
725
726 // Same as above, with old names.
727 SPOT_DEPRECATED("use marks() instead")
728 std::vector<std::set<acc_cond::mark_t>> used_acc() const
729 {
730 return marks();
731 }
732 SPOT_DEPRECATED("use marks_of() instead")
733 std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
734 {
735 return marks_of(scc);
736 }
737
741 acc_cond::mark_t acc_sets_of(unsigned scc) const
742 {
743 return node(scc).acc_marks();
744 }
745
749 {
750 return node(scc).common_marks();
751 }
752
753 std::vector<bool> weak_sccs() const;
754
755 bdd scc_ap_support(unsigned scc) const;
756
766 std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
767 acc_cond::mark_t sets,
768 bool preserve_names = false) const;
769 protected:
771 void
773 acc_cond::mark_t all_fin,
774 acc_cond::mark_t all_inf,
775 unsigned nb_pairs,
776 std::vector<acc_cond::rs_pair>& pairs,
777 std::vector<unsigned>& res,
778 std::vector<unsigned>& old) const;
779 public:
784 std::vector<unsigned>
785 states_on_acc_cycle_of(unsigned scc) const;
786 };
787
788
794 class SPOT_API scc_and_mark_filter
795 {
796 protected:
797 const scc_info* lower_si_;
798 unsigned lower_scc_;
799 acc_cond::mark_t cut_sets_;
800 const_twa_graph_ptr aut_;
801 acc_cond old_acc_;
802 bool restore_old_acc_ = false;
803 const bitvect* keep_ = nullptr;
804
806 filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
807 unsigned dst, void* data);
808
810 filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data);
811
813 filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t& e,
814 unsigned dst, void* data);
815
816 public:
823 unsigned lower_scc,
824 acc_cond::mark_t cut_sets)
825 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
826 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
827 {
828 auto f = lower_si.get_filter();
829 if (f == &filter_mark_
830 || f == &filter_scc_and_mark_
831 || f == &filter_scc_and_mark_and_edges_)
832 {
833 const void* data = lower_si.get_filter_data();
834 auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
835 cut_sets_ |= d.cut_sets_;
836 if (f == &filter_scc_and_mark_and_edges_)
837 keep_ = d.keep_;
838 }
839 }
840
841 scc_and_mark_filter(const scc_info& lower_si,
842 unsigned lower_scc,
843 acc_cond::mark_t cut_sets,
844 const bitvect& keep)
845 : scc_and_mark_filter(lower_si, lower_scc, cut_sets)
846 {
847 keep_ = &keep;
848 }
849
854 scc_and_mark_filter(const const_twa_graph_ptr& aut,
855 acc_cond::mark_t cut_sets)
856 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
857 old_acc_(aut_->get_acceptance())
858 {
859 }
860
862 {
863 restore_acceptance();
864 }
865
866 void override_acceptance(const acc_cond& new_acc)
867 {
868 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
869 restore_old_acc_ = true;
870 }
871
872 void restore_acceptance()
873 {
874 if (!restore_old_acc_)
875 return;
876 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
877 restore_old_acc_ = false;
878 }
879
880 const_twa_graph_ptr get_aut() const
881 {
882 return aut_;
883 }
884
885 unsigned start_state() const
886 {
887 if (lower_si_)
888 return lower_si_->one_state_of(lower_scc_);
889 return aut_->get_init_state_number();
890 }
891
892 scc_info::edge_filter get_filter() const
893 {
894 if (keep_)
895 return filter_scc_and_mark_and_edges_;
896 if (lower_si_)
897 return filter_scc_and_mark_;
898 if (cut_sets_)
899 return filter_mark_;
900 return nullptr;
901 }
902 };
903
907 SPOT_API std::ostream&
908 dump_scc_info_dot(std::ostream& out,
909 const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
910
911}
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:795
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:854
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:822
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:450
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition sccinfo.hh:498
bool is_maximally_accepting_scc(unsigned scc) const
Whether a cycle going through all edges of the SCC is accepting.
Definition sccinfo.hh:681
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:554
unsigned initial() const
Get number of the SCC containing the initial state.
Definition sccinfo.hh:645
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:629
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:515
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:748
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:612
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:741
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
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:85
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.8