23 #include <spot/twa/twagraph.hh> 33 template <
typename Iterator>
34 bool operator()(Iterator, Iterator)
const noexcept
45 const std::vector<unsigned>& sccof_;
46 unsigned desired_scc_;
48 keep_inner_scc(
const std::vector<unsigned>& sccof,
unsigned desired_scc)
49 : sccof_(sccof), desired_scc_(desired_scc)
53 template <
typename Iterator>
54 bool operator()(Iterator begin, Iterator end)
const noexcept
58 if (sccof_[*begin++] == desired_scc_)
67 template <
typename Graph,
typename Filter>
71 typedef typename std::conditional<std::is_const<Graph>::value,
72 const typename Graph::edge_storage_t,
73 typename Graph::edge_storage_t>::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;
80 typedef std::vector<unsigned>::const_iterator state_iterator;
82 typedef typename std::conditional<std::is_const<Graph>::value,
83 const typename Graph::edge_vector_t,
84 typename Graph::edge_vector_t>::type
87 typedef typename std::conditional<std::is_const<Graph>::value,
88 const typename Graph::state_vector,
89 typename Graph::state_vector>::type
91 typedef const typename Graph::dests_vector_t dv_t;
103 void inc_state_maybe_()
105 while (!t_ && (++pos_ != end_))
106 t_ = (*sv_)[*pos_].succ;
111 t_ = (*tv_)[t_].next_succ;
115 bool ignore_current()
117 unsigned dst = (*this)->dst;
120 return !filt_(&(*this)->dst, 1 + &(*this)->dst);
122 const unsigned* d = dv_->data() + ~dst;
123 return !filt_(d + 1, d + *d + 1);
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)
134 t_ = (*sv_)[*pos_].succ;
136 while (pos_ != end_ && ignore_current())
144 while (pos_ != end_ && ignore_current());
157 return pos_ == o.pos_ && t_ == o.t_;
162 return pos_ != o.pos_ || t_ != o.t_;
165 reference operator*()
const 170 pointer operator->()
const 177 template <
typename Graph,
typename Filter>
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;
187 state_iterator begin_;
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)
203 return {begin_, end_, tv_, sv_, dv_, filt_};
208 return {end_, end_,
nullptr,
nullptr,
nullptr, filt_};
219 typedef std::vector<unsigned> scc_succs;
223 std::vector<unsigned> states_;
233 acc_(0
U), trivial_(
true), accepting_(
false),
234 rejecting_(
false), useful_(
false)
240 acc_(acc), common_(common),
241 trivial_(trivial), accepting_(
false),
242 rejecting_(
false), useful_(
false)
246 bool is_trivial()
const 271 bool is_useful()
const 286 const std::vector<unsigned>& states()
const 291 unsigned one_state()
const 296 const scc_succs& succ()
const 339 typedef std::underlying_type_t<scc_info_options> ut;
341 & static_cast<ut>(right));
347 typedef std::underlying_type_t<scc_info_options> ut;
349 | static_cast<ut>(right));
376 typedef scc_info_node::scc_succs scc_succs;
410 std::vector<unsigned> sccof_;
411 std::vector<scc_node> node_;
412 const_twa_graph_ptr aut_;
413 unsigned initial_state_;
416 int one_acc_scc_ = -1;
420 void determine_usefulness();
422 const scc_node& node(
unsigned scc)
const 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();
440 unsigned initial_state = ~0
U,
441 edge_filter filter =
nullptr,
442 void* filter_data =
nullptr,
446 :
scc_info(aut, ~0
U, nullptr, nullptr, options)
451 const_twa_graph_ptr get_aut()
const 456 unsigned scc_count()
const 467 bool reachable_state(
unsigned st)
const 469 return scc_of(st) != -1
U;
472 unsigned scc_of(
unsigned st)
const 477 std::vector<scc_node>::const_iterator begin()
const 479 return node_.begin();
482 std::vector<scc_node>::const_iterator end()
const 487 std::vector<scc_node>::const_iterator cbegin()
const 489 return node_.cbegin();
492 std::vector<scc_node>::const_iterator cend()
const 497 std::vector<scc_node>::const_reverse_iterator rbegin()
const 499 return node_.rbegin();
502 std::vector<scc_node>::const_reverse_iterator rend()
const 507 const std::vector<unsigned>& states_of(
unsigned scc)
const 510 report_need_track_states();
511 return node(scc).states();
522 auto& states = states_of(scc);
523 return {states.begin(), states.end(),
524 &aut_->edge_vector(), &aut_->states(),
525 &aut_->get_graph().dests_vector(),
539 auto& states = states_of(scc);
540 return {states.begin(), states.end(),
541 &aut_->edge_vector(), &aut_->states(),
542 &aut_->get_graph().dests_vector(),
546 unsigned one_state_of(
unsigned scc)
const 548 return node(scc).one_state();
554 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
555 return scc_of(initial_state_);
558 const scc_succs& succ(
unsigned scc)
const 561 report_need_track_succs();
562 return node(scc).succ();
565 bool is_trivial(
unsigned scc)
const 567 return node(scc).is_trivial();
570 SPOT_DEPRECATED(
"use acc_sets_of() instead")
573 return acc_sets_of(scc);
576 bool is_accepting_scc(
unsigned scc)
const 578 return node(scc).is_accepting();
581 bool is_rejecting_scc(
unsigned scc)
const 583 return node(scc).is_rejecting();
590 void determine_unknown_acceptance();
598 bool check_scc_emptiness(
unsigned n, std::vector<bool>* k);
600 bool is_useful_scc(
unsigned scc)
const 603 report_incompatible_stop_on_acc();
605 report_need_track_succs();
606 return node(scc).is_useful();
609 bool is_useful_state(
unsigned st)
const 611 return reachable_state(st) && is_useful_scc(scc_of(st));
616 std::vector<std::set<acc_cond::mark_t>> marks()
const;
617 std::set<acc_cond::mark_t> marks_of(
unsigned scc)
const;
620 SPOT_DEPRECATED(
"use marks() instead")
621 std::vector<std::set<acc_cond::mark_t>> used_acc()
const 625 SPOT_DEPRECATED(
"use marks_of() instead")
626 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const 628 return marks_of(scc);
636 return node(scc).acc_marks();
643 return node(scc).common_marks();
646 std::vector<bool> weak_sccs()
const;
648 bdd scc_ap_support(
unsigned scc)
const;
659 std::vector<twa_graph_ptr> split_on_sets(
unsigned scc,
661 bool preserve_names =
false)
const;
665 states_on_acc_cycle_of_rec(
unsigned scc,
669 std::vector<acc_cond::rs_pair>& pairs,
670 std::vector<unsigned>& res,
671 std::vector<unsigned>& old)
const;
677 std::vector<unsigned>
678 states_on_acc_cycle_of(
unsigned scc)
const;
685 SPOT_API std::ostream&
686 dump_scc_info_dot(std::ostream& out,
687 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
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.
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:641
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:634
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: 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