23 #include <spot/twa/twagraph.hh> 24 #include <spot/twaalgos/emptiness.hh> 34 template <
typename Iterator>
35 bool operator()(Iterator, Iterator)
const noexcept
46 const std::vector<unsigned>& sccof_;
47 unsigned desired_scc_;
49 keep_inner_scc(
const std::vector<unsigned>& sccof,
unsigned desired_scc)
50 : sccof_(sccof), desired_scc_(desired_scc)
54 template <
typename Iterator>
55 bool operator()(Iterator begin, Iterator end)
const noexcept
59 if (sccof_[*begin++] == desired_scc_)
68 template <
typename Graph,
typename Filter>
72 typedef typename std::conditional<std::is_const<Graph>::value,
73 const typename Graph::edge_storage_t,
74 typename Graph::edge_storage_t>::type
76 typedef value_type& reference;
77 typedef value_type* pointer;
78 typedef std::ptrdiff_t difference_type;
79 typedef std::forward_iterator_tag iterator_category;
81 typedef std::vector<unsigned>::const_iterator state_iterator;
83 typedef typename std::conditional<std::is_const<Graph>::value,
84 const typename Graph::edge_vector_t,
85 typename Graph::edge_vector_t>::type
88 typedef typename std::conditional<std::is_const<Graph>::value,
89 const typename Graph::state_vector,
90 typename Graph::state_vector>::type
92 typedef const typename Graph::dests_vector_t dv_t;
104 void inc_state_maybe_()
106 while (!t_ && (++pos_ != end_))
107 t_ = (*sv_)[*pos_].succ;
112 t_ = (*tv_)[t_].next_succ;
116 bool ignore_current()
118 unsigned dst = (*this)->dst;
121 return !filt_(&(*this)->dst, 1 + &(*this)->dst);
123 const unsigned* d = dv_->data() + ~dst;
124 return !filt_(d + 1, d + *d + 1);
129 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
130 : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
135 t_ = (*sv_)[*pos_].succ;
137 while (pos_ != end_ && ignore_current())
145 while (pos_ != end_ && ignore_current());
158 return pos_ == o.pos_ && t_ == o.t_;
163 return pos_ != o.pos_ || t_ != o.t_;
166 reference operator*()
const 171 pointer operator->()
const 178 template <
typename Graph,
typename Filter>
183 typedef typename iter_t::tv_t tv_t;
184 typedef typename iter_t::sv_t sv_t;
185 typedef typename iter_t::dv_t dv_t;
186 typedef typename iter_t::state_iterator state_iterator;
188 state_iterator begin_;
196 scc_edges(state_iterator begin, state_iterator end,
197 tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
198 : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
204 return {begin_, end_, tv_, sv_, dv_, filt_};
209 return {end_, end_,
nullptr,
nullptr,
nullptr, filt_};
220 typedef std::vector<unsigned> scc_succs;
224 std::vector<unsigned> states_;
234 acc_({}), trivial_(
true), accepting_(
false),
235 rejecting_(
false), useful_(
false)
241 : acc_(acc), common_(common),
242 trivial_(trivial), accepting_(
false),
243 rejecting_(
false), useful_(
false)
247 bool is_trivial()
const 272 bool is_useful()
const 287 const std::vector<unsigned>& states()
const 292 unsigned one_state()
const 297 const scc_succs& succ()
const 340 typedef std::underlying_type_t<scc_info_options> ut;
342 & static_cast<ut>(right));
348 typedef std::underlying_type_t<scc_info_options> ut;
350 | static_cast<ut>(right));
353 class SPOT_API scc_and_mark_filter;
379 typedef scc_info_node::scc_succs scc_succs;
413 std::vector<unsigned> sccof_;
414 std::vector<scc_node> node_;
415 const_twa_graph_ptr aut_;
416 unsigned initial_state_;
419 int one_acc_scc_ = -1;
423 void determine_usefulness();
425 const scc_node& node(
unsigned scc)
const 432 [[noreturn]]
static void report_need_track_states();
433 [[noreturn]]
static void report_need_track_succs();
434 [[noreturn]]
static void report_incompatible_stop_on_acc();
443 unsigned initial_state = ~0
U,
444 edge_filter filter =
nullptr,
445 void* filter_data =
nullptr,
449 :
scc_info(aut, ~0
U, nullptr, nullptr, options)
471 const_twa_graph_ptr get_aut()
const 481 const void* get_filter_data()
const 486 unsigned scc_count()
const 497 bool reachable_state(
unsigned st)
const 499 return scc_of(st) != -1
U;
502 unsigned scc_of(
unsigned st)
const 507 std::vector<scc_node>::const_iterator begin()
const 509 return node_.begin();
512 std::vector<scc_node>::const_iterator end()
const 517 std::vector<scc_node>::const_iterator cbegin()
const 519 return node_.cbegin();
522 std::vector<scc_node>::const_iterator cend()
const 527 std::vector<scc_node>::const_reverse_iterator rbegin()
const 529 return node_.rbegin();
532 std::vector<scc_node>::const_reverse_iterator rend()
const 537 const std::vector<unsigned>& states_of(
unsigned scc)
const 540 report_need_track_states();
541 return node(scc).states();
552 auto& states = states_of(scc);
553 return {states.begin(), states.end(),
554 &aut_->edge_vector(), &aut_->states(),
555 &aut_->get_graph().dests_vector(),
569 auto& states = states_of(scc);
570 return {states.begin(), states.end(),
571 &aut_->edge_vector(), &aut_->states(),
572 &aut_->get_graph().dests_vector(),
576 unsigned one_state_of(
unsigned scc)
const 578 return node(scc).one_state();
584 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
585 return scc_of(initial_state_);
588 const scc_succs& succ(
unsigned scc)
const 591 report_need_track_succs();
592 return node(scc).succ();
595 bool is_trivial(
unsigned scc)
const 597 return node(scc).is_trivial();
600 SPOT_DEPRECATED(
"use acc_sets_of() instead")
603 return acc_sets_of(scc);
606 bool is_accepting_scc(
unsigned scc)
const 608 return node(scc).is_accepting();
611 bool is_rejecting_scc(
unsigned scc)
const 613 return node(scc).is_rejecting();
620 void determine_unknown_acceptance();
626 bool check_scc_emptiness(
unsigned n);
635 void get_accepting_run(
unsigned scc, twa_run_ptr r)
const;
637 bool is_useful_scc(
unsigned scc)
const 640 report_incompatible_stop_on_acc();
642 report_need_track_succs();
643 return node(scc).is_useful();
646 bool is_useful_state(
unsigned st)
const 648 return reachable_state(st) && is_useful_scc(scc_of(st));
653 std::vector<std::set<acc_cond::mark_t>> marks()
const;
654 std::set<acc_cond::mark_t> marks_of(
unsigned scc)
const;
657 SPOT_DEPRECATED(
"use marks() instead")
658 std::vector<std::set<acc_cond::mark_t>> used_acc()
const 662 SPOT_DEPRECATED(
"use marks_of() instead")
663 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const 665 return marks_of(scc);
673 return node(scc).acc_marks();
680 return node(scc).common_marks();
683 std::vector<bool> weak_sccs()
const;
685 bdd scc_ap_support(
unsigned scc)
const;
696 std::vector<twa_graph_ptr> split_on_sets(
unsigned scc,
698 bool preserve_names =
false)
const;
702 states_on_acc_cycle_of_rec(
unsigned scc,
706 std::vector<acc_cond::rs_pair>& pairs,
707 std::vector<unsigned>& res,
708 std::vector<unsigned>& old)
const;
714 std::vector<unsigned>
715 states_on_acc_cycle_of(
unsigned scc)
const;
724 class SPOT_API scc_and_mark_filter
730 const_twa_graph_ptr aut_;
732 bool restore_old_acc_ =
false;
736 unsigned dst,
void* data)
738 auto& d = *
reinterpret_cast<scc_and_mark_filter*
>(data);
739 if (d.lower_si_->scc_of(dst) != d.lower_scc_)
740 return scc_info::edge_filter_choice::ignore;
741 if (d.cut_sets_ & e.acc)
742 return scc_info::edge_filter_choice::cut;
743 return scc_info::edge_filter_choice::keep;
749 auto& d = *
reinterpret_cast<scc_and_mark_filter*
>(data);
750 if (d.cut_sets_ & e.acc)
751 return scc_info::edge_filter_choice::cut;
752 return scc_info::edge_filter_choice::keep;
764 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
765 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
767 const void* data = lower_si.get_filter_data();
770 auto& d = *
reinterpret_cast<const scc_and_mark_filter*
>(data);
771 cut_sets_ |= d.cut_sets_;
781 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
782 old_acc_(aut_->get_acceptance())
786 ~scc_and_mark_filter()
788 restore_acceptance();
791 void override_acceptance(
const acc_cond& new_acc)
793 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(new_acc);
794 restore_old_acc_ =
true;
797 void restore_acceptance()
799 if (!restore_old_acc_)
801 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(old_acc_);
802 restore_old_acc_ =
false;
805 const_twa_graph_ptr get_aut()
const 810 unsigned start_state()
const 813 return lower_si_->one_state_of(lower_scc_);
814 return aut_->get_init_state_number();
820 return filter_scc_and_mark_;
831 SPOT_API std::ostream&
832 dump_scc_info_dot(std::ostream& out,
833 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
Definition: automata.hh:26
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:373
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:761
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:407
Definition: sccinfo.hh:179
Storage for SCC related information.
Definition: sccinfo.hh:217
Default behavior: explore everything and track states and succs.
acc_cond::mark_t common_sets_of(unsigned scc) const
Definition: sccinfo.hh:678
Definition: sccinfo.hh:69
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:779
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:550
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:492
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:671
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:305
An acceptance condition.
Definition: acc.hh:58
scc_info(const_twa_graph_ptr aut, scc_info_options options)
Create the scc_info map for aut.
Definition: sccinfo.hh:448
bool is_accepting() const
True if we know that the SCC has an accepting cycle.
Definition: sccinfo.hh:257
scc_info(const scc_and_mark_filter &filt)
Create an scc_info map from some filter.
Definition: sccinfo.hh:465
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:582
edge_filter_choice
An edge_filter may be called on each edge to decide what to do with it.
Definition: sccinfo.hh:405
bool is_rejecting() const
True if we know that all cycles in the SCC are rejecting.
Definition: sccinfo.hh:267
Definition: sccinfo.hh:32
Definition: sccinfo.hh:43
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:567
Graph-based representation of a TωA.
Definition: twagraph.hh:199
An acceptance mark.
Definition: acc.hh:81