23 #include <spot/twa/twagraph.hh>
24 #include <spot/twaalgos/emptiness.hh>
25 #include <spot/misc/bitvect.hh>
67 template <
typename Iterator>
68 bool operator()(Iterator, Iterator)
const noexcept
79 const std::vector<unsigned>& sccof_;
80 unsigned desired_scc_;
82 keep_inner_scc(
const std::vector<unsigned>& sccof,
unsigned desired_scc)
83 : sccof_(sccof), desired_scc_(desired_scc)
87 template <
typename Iterator>
88 bool operator()(Iterator begin, Iterator end)
const noexcept
92 if (sccof_[*begin++] == desired_scc_)
101 template <
typename Graph,
typename Filter>
105 typedef typename std::conditional<std::is_const<Graph>::value,
106 const typename Graph::edge_storage_t,
107 typename Graph::edge_storage_t>::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;
114 typedef std::vector<unsigned>::const_iterator state_iterator;
116 typedef typename std::conditional<std::is_const<Graph>::value,
117 const typename Graph::edge_vector_t,
118 typename Graph::edge_vector_t>::type
121 typedef typename std::conditional<std::is_const<Graph>::value,
122 const typename Graph::state_vector,
123 typename Graph::state_vector>::type
125 typedef const typename Graph::dests_vector_t dv_t;
140 void inc_state_maybe_()
142 while (!t_ && (++pos_ != end_))
143 t_ = (*sv_)[*pos_].succ;
148 t_ = (*tv_)[t_].next_succ;
153 bool ignore_current()
155 unsigned dst = (*this)->dst;
159 if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
162 return efilter_((*tv_)[t_], dst, efilter_data_)
163 != edge_filter_choice::keep;
169 const unsigned* d = dv_->data() + ~dst;
170 if (!filt_(d + 1, d + *d + 1))
176 const unsigned* end = d + *d + 1;
177 for (
const unsigned* i = d + 1; i != end; ++i)
179 if (efilter_((*tv_)[t_], *i, efilter_data_)
180 == edge_filter_choice::keep)
191 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
193 : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
194 efilter_(efilter), efilter_data_(efilter_data)
199 t_ = (*sv_)[*pos_].succ;
201 while (pos_ != end_ && ignore_current())
209 while (pos_ != end_ && ignore_current());
222 return pos_ == o.pos_ && t_ == o.t_;
227 return pos_ != o.pos_ || t_ != o.t_;
230 reference operator*()
const
235 pointer operator->()
const
242 template <
typename Graph,
typename Filter>
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;
252 state_iterator begin_;
262 scc_edges(state_iterator begin, state_iterator end,
263 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
265 : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
266 efilter_(efilter), efilter_data_(efilter_data)
272 return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
277 return {end_, end_,
nullptr,
nullptr,
nullptr, filt_,
nullptr,
nullptr};
288 typedef std::vector<unsigned> scc_succs;
292 std::vector<unsigned> states_;
302 acc_({}), trivial_(
true), accepting_(
false),
303 rejecting_(
false), useful_(
false)
309 : acc_(acc), common_(common),
310 trivial_(trivial), accepting_(
false),
311 rejecting_(
false), useful_(
false)
315 bool is_trivial()
const
340 bool is_useful()
const
345 acc_cond::mark_t acc_marks()
const
350 acc_cond::mark_t common_marks()
const
355 const std::vector<unsigned>& states()
const
360 unsigned one_state()
const
365 const scc_succs& succ()
const
409 typedef std::underlying_type_t<scc_info_options> ut;
411 &
static_cast<ut
>(right));
417 typedef std::underlying_type_t<scc_info_options> ut;
419 |
static_cast<ut
>(right));
422 class SPOT_API scc_and_mark_filter;
448 typedef scc_info_node::scc_succs scc_succs;
456 std::vector<unsigned> sccof_;
457 std::vector<scc_node> node_;
458 const_twa_graph_ptr aut_;
459 unsigned initial_state_;
462 int one_acc_scc_ = -1;
466 void determine_usefulness();
468 const scc_node& node(
unsigned scc)
const
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();
486 unsigned initial_state = ~0U,
487 edge_filter filter =
nullptr,
488 void* filter_data =
nullptr,
492 :
scc_info(aut, ~0
U, nullptr, nullptr, options)
514 const_twa_graph_ptr get_aut()
const
529 void* get_filter_data()
const
534 unsigned scc_count()
const
552 bool reachable_state(
unsigned st)
const
554 return scc_of(st) != -1U;
557 unsigned scc_of(
unsigned st)
const
562 std::vector<scc_node>::const_iterator begin()
const
564 return node_.begin();
567 std::vector<scc_node>::const_iterator end()
const
572 std::vector<scc_node>::const_iterator cbegin()
const
574 return node_.cbegin();
577 std::vector<scc_node>::const_iterator cend()
const
582 std::vector<scc_node>::const_reverse_iterator rbegin()
const
584 return node_.rbegin();
587 std::vector<scc_node>::const_reverse_iterator rend()
const
592 const std::vector<unsigned>& states_of(
unsigned scc)
const
595 report_need_track_states();
596 return node(scc).states();
604 internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
607 auto& states = states_of(scc);
608 return {states.begin(), states.end(),
609 &aut_->edge_vector(), &aut_->states(),
610 &aut_->get_graph().dests_vector(),
624 auto& states = states_of(scc);
625 return {states.begin(), states.end(),
626 &aut_->edge_vector(), &aut_->states(),
627 &aut_->get_graph().dests_vector(),
629 const_cast<void*
>(filter_data_)};
632 unsigned one_state_of(
unsigned scc)
const
634 return node(scc).one_state();
640 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
641 return scc_of(initial_state_);
644 const scc_succs& succ(
unsigned scc)
const
647 report_need_track_succs();
648 return node(scc).succ();
651 bool is_trivial(
unsigned scc)
const
653 return node(scc).is_trivial();
657 acc_cond::mark_t acc(
unsigned scc)
const
659 return acc_sets_of(scc);
662 bool is_accepting_scc(
unsigned scc)
const
664 return node(scc).is_accepting();
667 bool is_rejecting_scc(
unsigned scc)
const
669 return node(scc).is_rejecting();
676 return aut_->acc().accepting(acc_sets_of(scc));
700 bool is_useful_scc(
unsigned scc)
const
703 report_incompatible_stop_on_acc();
705 report_need_track_succs();
706 return node(scc).is_useful();
709 bool is_useful_state(
unsigned st)
const
711 return reachable_state(st) && is_useful_scc(scc_of(st));
716 std::vector<std::set<acc_cond::mark_t>>
marks()
const;
717 std::set<acc_cond::mark_t> marks_of(
unsigned scc)
const;
721 std::vector<std::set<
acc_cond::mark_t>> used_acc()
const
726 std::set<
acc_cond::mark_t> used_acc_of(
unsigned scc)
const
728 return marks_of(scc);
736 return node(scc).acc_marks();
743 return node(scc).common_marks();
746 std::vector<bool> weak_sccs()
const;
748 bdd scc_ap_support(
unsigned scc)
const;
761 bool preserve_names =
false)
const;
769 std::vector<acc_cond::rs_pair>& pairs,
770 std::vector<unsigned>& res,
771 std::vector<unsigned>& old)
const;
777 std::vector<unsigned>
793 const_twa_graph_ptr aut_;
795 bool restore_old_acc_ =
false;
796 const bitvect* keep_ =
nullptr;
800 unsigned dst,
void* data);
807 unsigned dst,
void* data);
818 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
819 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
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_)
826 const void* data = lower_si.get_filter_data();
828 cut_sets_ |= d.cut_sets_;
829 if (f == &filter_scc_and_mark_and_edges_)
849 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
850 old_acc_(aut_->get_acceptance())
856 restore_acceptance();
859 void override_acceptance(
const acc_cond& new_acc)
861 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(new_acc);
862 restore_old_acc_ =
true;
865 void restore_acceptance()
867 if (!restore_old_acc_)
869 std::const_pointer_cast<twa_graph>(aut_)->set_acceptance(old_acc_);
870 restore_old_acc_ =
false;
873 const_twa_graph_ptr get_aut()
const
878 unsigned start_state()
const
881 return lower_si_->one_state_of(lower_scc_);
882 return aut_->get_init_state_number();
885 scc_info::edge_filter get_filter()
const
888 return filter_scc_and_mark_and_edges_;
890 return filter_scc_and_mark_;
900 SPOT_API std::ostream&
902 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
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
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
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:605
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
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
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:741
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:734
scc_info(const scc_and_mark_filter &filt, scc_info_options options)
Create an scc_info map from some filter.
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
@ TRACK_STATES_IF_FIN_USED
@ 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: sccinfo.hh:66
Definition: sccinfo.hh:77