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_};
218 typedef std::vector<unsigned> scc_succs;
224 std::vector<unsigned> states_;
231 acc_(0
U), trivial_(
true), accepting_(
false),
232 rejecting_(
false), useful_(
false)
238 acc_(acc), common_(common),
239 trivial_(trivial), accepting_(
false),
240 rejecting_(
false), useful_(
false)
244 bool is_trivial()
const 267 bool is_useful()
const 282 const std::vector<unsigned>& states()
const 287 const scc_succs& succ()
const 312 typedef scc_info_node::scc_succs scc_succs;
346 std::vector<unsigned> sccof_;
347 std::vector<scc_node> node_;
348 const_twa_graph_ptr aut_;
349 unsigned initial_state_;
354 void determine_usefulness();
356 const scc_node& node(
unsigned scc)
const 366 unsigned initial_state = ~0
U,
367 edge_filter filter =
nullptr,
368 void* filter_data =
nullptr);
370 const_twa_graph_ptr get_aut()
const 375 unsigned scc_count()
const 380 bool reachable_state(
unsigned st)
const 382 return scc_of(st) != -1
U;
385 unsigned scc_of(
unsigned st)
const 390 std::vector<scc_node>::const_iterator begin()
const 392 return node_.begin();
395 std::vector<scc_node>::const_iterator end()
const 400 std::vector<scc_node>::const_iterator cbegin()
const 402 return node_.cbegin();
405 std::vector<scc_node>::const_iterator cend()
const 410 std::vector<scc_node>::const_reverse_iterator rbegin()
const 412 return node_.rbegin();
415 std::vector<scc_node>::const_reverse_iterator rend()
const 420 const std::vector<unsigned>& states_of(
unsigned scc)
const 422 return node(scc).states();
433 auto& states = states_of(scc);
434 return {states.begin(), states.end(),
435 &aut_->edge_vector(), &aut_->states(),
436 &aut_->get_graph().dests_vector(),
450 auto& states = states_of(scc);
451 return {states.begin(), states.end(),
452 &aut_->edge_vector(), &aut_->states(),
453 &aut_->get_graph().dests_vector(),
457 unsigned one_state_of(
unsigned scc)
const 459 return states_of(scc).front();
465 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
466 return scc_of(initial_state_);
469 const scc_succs& succ(
unsigned scc)
const 471 return node(scc).succ();
474 bool is_trivial(
unsigned scc)
const 476 return node(scc).is_trivial();
481 return node(scc).acc_marks();
484 bool is_accepting_scc(
unsigned scc)
const 486 return node(scc).is_accepting();
489 bool is_rejecting_scc(
unsigned scc)
const 491 return node(scc).is_rejecting();
496 void determine_unknown_acceptance();
498 bool is_useful_scc(
unsigned scc)
const 500 return node(scc).is_useful();
503 bool is_useful_state(
unsigned st)
const 505 return reachable_state(st) && node(scc_of(st)).is_useful();
510 std::vector<std::set<acc_cond::mark_t>> used_acc()
const;
512 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const;
524 return node(scc).common_marks();
527 std::vector<bool> weak_sccs()
const;
529 bdd scc_ap_support(
unsigned scc)
const;
536 SPOT_API std::ostream&
537 dump_scc_info_dot(std::ostream& out,
538 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:306
Definition: sccinfo.hh:178
Storage for SCC related information.
Definition: sccinfo.hh:215
acc_cond::mark_t common_sets_of(unsigned scc) const
sets that contain the entire SCC
Definition: sccinfo.hh:522
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:431
acc_cond::mark_t acc_sets_of(unsigned scc) const
sets that contain at least one transition of the SCC
Definition: sccinfo.hh:515
bool is_accepting() const
True if we are sure that the SCC is accepting.
Definition: sccinfo.hh:253
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:463
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:338
bool is_rejecting() const
Definition: sccinfo.hh:262
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:448