23 #include <spot/twa/twagraph.hh> 24 #include <spot/twaalgos/emptiness.hh> 66 template <
typename Iterator>
67 bool operator()(Iterator, Iterator)
const noexcept
78 const std::vector<unsigned>& sccof_;
79 unsigned desired_scc_;
81 keep_inner_scc(
const std::vector<unsigned>& sccof,
unsigned desired_scc)
82 : sccof_(sccof), desired_scc_(desired_scc)
86 template <
typename Iterator>
87 bool operator()(Iterator begin, Iterator end)
const noexcept
91 if (sccof_[*begin++] == desired_scc_)
100 template <
typename Graph,
typename Filter>
104 typedef typename std::conditional<std::is_const<Graph>::value,
105 const typename Graph::edge_storage_t,
106 typename Graph::edge_storage_t>::type
108 typedef value_type& reference;
109 typedef value_type* pointer;
110 typedef std::ptrdiff_t difference_type;
111 typedef std::forward_iterator_tag iterator_category;
113 typedef std::vector<unsigned>::const_iterator state_iterator;
115 typedef typename std::conditional<std::is_const<Graph>::value,
116 const typename Graph::edge_vector_t,
117 typename Graph::edge_vector_t>::type
120 typedef typename std::conditional<std::is_const<Graph>::value,
121 const typename Graph::state_vector,
122 typename Graph::state_vector>::type
124 typedef const typename Graph::dests_vector_t dv_t;
139 void inc_state_maybe_()
141 while (!t_ && (++pos_ != end_))
142 t_ = (*sv_)[*pos_].succ;
147 t_ = (*tv_)[t_].next_succ;
152 bool ignore_current()
154 unsigned dst = (*this)->dst;
158 if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
161 return efilter_((*tv_)[t_], dst, efilter_data_)
162 != edge_filter_choice::keep;
168 const unsigned* d = dv_->data() + ~dst;
169 if (!filt_(d + 1, d + *d + 1))
175 const unsigned* end = d + *d + 1;
176 for (
const unsigned* i = d + 1; i != end; ++i)
178 if (efilter_((*tv_)[t_], *i, efilter_data_)
179 == edge_filter_choice::keep)
190 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
192 : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
193 efilter_(efilter), efilter_data_(efilter_data)
198 t_ = (*sv_)[*pos_].succ;
200 while (pos_ != end_ && ignore_current())
208 while (pos_ != end_ && ignore_current());
221 return pos_ == o.pos_ && t_ == o.t_;
226 return pos_ != o.pos_ || t_ != o.t_;
229 reference operator*()
const 234 pointer operator->()
const 241 template <
typename Graph,
typename Filter>
246 typedef typename iter_t::tv_t tv_t;
247 typedef typename iter_t::sv_t sv_t;
248 typedef typename iter_t::dv_t dv_t;
249 typedef typename iter_t::state_iterator state_iterator;
251 state_iterator begin_;
261 scc_edges(state_iterator begin, state_iterator end,
262 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
264 : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
265 efilter_(efilter), efilter_data_(efilter_data)
271 return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
276 return {end_, end_,
nullptr,
nullptr,
nullptr, filt_,
nullptr,
nullptr};
287 typedef std::vector<unsigned> scc_succs;
291 std::vector<unsigned> states_;
301 acc_({}), trivial_(
true), accepting_(
false),
302 rejecting_(
false), useful_(
false)
308 : acc_(acc), common_(common),
309 trivial_(trivial), accepting_(
false),
310 rejecting_(
false), useful_(
false)
314 bool is_trivial()
const 339 bool is_useful()
const 354 const std::vector<unsigned>& states()
const 359 unsigned one_state()
const 364 const scc_succs& succ()
const 408 typedef std::underlying_type_t<scc_info_options> ut;
410 & static_cast<ut>(right));
416 typedef std::underlying_type_t<scc_info_options> ut;
418 | static_cast<ut>(right));
421 class SPOT_API scc_and_mark_filter;
447 typedef scc_info_node::scc_succs scc_succs;
455 std::vector<unsigned> sccof_;
456 std::vector<scc_node> node_;
457 const_twa_graph_ptr aut_;
458 unsigned initial_state_;
461 int one_acc_scc_ = -1;
465 void determine_usefulness();
467 const scc_node& node(
unsigned scc)
const 474 [[noreturn]]
static void report_need_track_states();
475 [[noreturn]]
static void report_need_track_succs();
476 [[noreturn]]
static void report_incompatible_stop_on_acc();
485 unsigned initial_state = ~0
U,
486 edge_filter filter =
nullptr,
487 void* filter_data =
nullptr,
491 :
scc_info(aut, ~0
U, nullptr, nullptr, options)
513 const_twa_graph_ptr get_aut()
const 523 edge_filter get_filter()
const 528 const void* get_filter_data()
const 533 unsigned scc_count()
const 551 bool reachable_state(
unsigned st)
const 553 return scc_of(st) != -1
U;
556 unsigned scc_of(
unsigned st)
const 561 std::vector<scc_node>::const_iterator begin()
const 563 return node_.begin();
566 std::vector<scc_node>::const_iterator end()
const 571 std::vector<scc_node>::const_iterator cbegin()
const 573 return node_.cbegin();
576 std::vector<scc_node>::const_iterator cend()
const 581 std::vector<scc_node>::const_reverse_iterator rbegin()
const 583 return node_.rbegin();
586 std::vector<scc_node>::const_reverse_iterator rend()
const 591 const std::vector<unsigned>& states_of(
unsigned scc)
const 594 report_need_track_states();
595 return node(scc).states();
606 auto& states = states_of(scc);
607 return {states.begin(), states.end(),
608 &aut_->edge_vector(), &aut_->states(),
609 &aut_->get_graph().dests_vector(),
623 auto& states = states_of(scc);
624 return {states.begin(), states.end(),
625 &aut_->edge_vector(), &aut_->states(),
626 &aut_->get_graph().dests_vector(),
628 const_cast<void*
>(filter_data_)};
631 unsigned one_state_of(
unsigned scc)
const 633 return node(scc).one_state();
639 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
640 return scc_of(initial_state_);
643 const scc_succs& succ(
unsigned scc)
const 646 report_need_track_succs();
647 return node(scc).succ();
650 bool is_trivial(
unsigned scc)
const 652 return node(scc).is_trivial();
658 return acc_sets_of(scc);
661 bool is_accepting_scc(
unsigned scc)
const 663 return node(scc).is_accepting();
666 bool is_rejecting_scc(
unsigned scc)
const 668 return node(scc).is_rejecting();
675 void determine_unknown_acceptance();
681 bool check_scc_emptiness(
unsigned n)
const;
690 void get_accepting_run(
unsigned scc, twa_run_ptr r)
const;
692 bool is_useful_scc(
unsigned scc)
const 695 report_incompatible_stop_on_acc();
697 report_need_track_succs();
698 return node(scc).is_useful();
701 bool is_useful_state(
unsigned st)
const 703 return reachable_state(st) && is_useful_scc(scc_of(st));
708 std::vector<std::set<acc_cond::mark_t>> marks()
const;
709 std::set<acc_cond::mark_t> marks_of(
unsigned scc)
const;
713 std::vector<std::set<acc_cond::mark_t>> used_acc()
const 718 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const 720 return marks_of(scc);
728 return node(scc).acc_marks();
735 return node(scc).common_marks();
738 std::vector<bool> weak_sccs()
const;
740 bdd scc_ap_support(
unsigned scc)
const;
751 std::vector<twa_graph_ptr> split_on_sets(
unsigned scc,
753 bool preserve_names =
false)
const;
757 states_on_acc_cycle_of_rec(
unsigned scc,
761 std::vector<acc_cond::rs_pair>& pairs,
762 std::vector<unsigned>& res,
763 std::vector<unsigned>& old)
const;
769 std::vector<unsigned>
770 states_on_acc_cycle_of(
unsigned scc)
const;
779 class SPOT_API scc_and_mark_filter
785 const_twa_graph_ptr aut_;
787 bool restore_old_acc_ =
false;
791 unsigned dst,
void* data);
804 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
805 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
807 auto f = lower_si.get_filter();
808 if (f == &filter_mark_ || f == &filter_scc_and_mark_)
810 const void* data = lower_si.get_filter_data();
811 auto& d = *
reinterpret_cast<const scc_and_mark_filter*
>(data);
812 cut_sets_ |= d.cut_sets_;
822 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
823 old_acc_(aut_->get_acceptance())
827 ~scc_and_mark_filter()
829 restore_acceptance();
832 void override_acceptance(
const acc_cond& new_acc)
834 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(new_acc);
835 restore_old_acc_ =
true;
838 void restore_acceptance()
840 if (!restore_old_acc_)
842 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(old_acc_);
843 restore_old_acc_ =
false;
846 const_twa_graph_ptr get_aut()
const 851 unsigned start_state()
const 854 return lower_si_->one_state_of(lower_scc_);
855 return aut_->get_init_state_number();
858 scc_info::edge_filter get_filter()
const 861 return filter_scc_and_mark_;
872 SPOT_API std::ostream&
873 dump_scc_info_dot(std::ostream& out,
874 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:441
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:801
Definition: sccinfo.hh:242
Storage for SCC related information.
Definition: sccinfo.hh:284
Default behavior: explore everything and track states and succs.
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:733
Definition: sccinfo.hh:101
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:820
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:604
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:546
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:56
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:726
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:372
An acceptance condition.
Definition: acc.hh:60
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:490
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:324
scc_info(const scc_and_mark_filter &filt)
Create an scc_info map from some filter.
Definition: sccinfo.hh:507
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:637
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:334
Definition: sccinfo.hh:64
Definition: sccinfo.hh:75
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:621
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:58
Graph-based representation of a TωA.
Definition: twagraph.hh:200
An acceptance mark.
Definition: acc.hh:87