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 edge_filter get_filter()
const 486 const void* get_filter_data()
const 491 unsigned scc_count()
const 502 bool reachable_state(
unsigned st)
const 504 return scc_of(st) != -1
U;
507 unsigned scc_of(
unsigned st)
const 512 std::vector<scc_node>::const_iterator begin()
const 514 return node_.begin();
517 std::vector<scc_node>::const_iterator end()
const 522 std::vector<scc_node>::const_iterator cbegin()
const 524 return node_.cbegin();
527 std::vector<scc_node>::const_iterator cend()
const 532 std::vector<scc_node>::const_reverse_iterator rbegin()
const 534 return node_.rbegin();
537 std::vector<scc_node>::const_reverse_iterator rend()
const 542 const std::vector<unsigned>& states_of(
unsigned scc)
const 545 report_need_track_states();
546 return node(scc).states();
557 auto& states = states_of(scc);
558 return {states.begin(), states.end(),
559 &aut_->edge_vector(), &aut_->states(),
560 &aut_->get_graph().dests_vector(),
574 auto& states = states_of(scc);
575 return {states.begin(), states.end(),
576 &aut_->edge_vector(), &aut_->states(),
577 &aut_->get_graph().dests_vector(),
581 unsigned one_state_of(
unsigned scc)
const 583 return node(scc).one_state();
589 SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
590 return scc_of(initial_state_);
593 const scc_succs& succ(
unsigned scc)
const 596 report_need_track_succs();
597 return node(scc).succ();
600 bool is_trivial(
unsigned scc)
const 602 return node(scc).is_trivial();
608 return acc_sets_of(scc);
611 bool is_accepting_scc(
unsigned scc)
const 613 return node(scc).is_accepting();
616 bool is_rejecting_scc(
unsigned scc)
const 618 return node(scc).is_rejecting();
625 void determine_unknown_acceptance();
631 bool check_scc_emptiness(
unsigned n)
const;
640 void get_accepting_run(
unsigned scc, twa_run_ptr r)
const;
642 bool is_useful_scc(
unsigned scc)
const 645 report_incompatible_stop_on_acc();
647 report_need_track_succs();
648 return node(scc).is_useful();
651 bool is_useful_state(
unsigned st)
const 653 return reachable_state(st) && is_useful_scc(scc_of(st));
658 std::vector<std::set<acc_cond::mark_t>> marks()
const;
659 std::set<acc_cond::mark_t> marks_of(
unsigned scc)
const;
663 std::vector<std::set<acc_cond::mark_t>> used_acc()
const 668 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const 670 return marks_of(scc);
678 return node(scc).acc_marks();
685 return node(scc).common_marks();
688 std::vector<bool> weak_sccs()
const;
690 bdd scc_ap_support(
unsigned scc)
const;
701 std::vector<twa_graph_ptr> split_on_sets(
unsigned scc,
703 bool preserve_names =
false)
const;
707 states_on_acc_cycle_of_rec(
unsigned scc,
711 std::vector<acc_cond::rs_pair>& pairs,
712 std::vector<unsigned>& res,
713 std::vector<unsigned>& old)
const;
719 std::vector<unsigned>
720 states_on_acc_cycle_of(
unsigned scc)
const;
729 class SPOT_API scc_and_mark_filter
735 const_twa_graph_ptr aut_;
737 bool restore_old_acc_ =
false;
741 unsigned dst,
void* data);
754 : lower_si_(&lower_si), lower_scc_(lower_scc), cut_sets_(cut_sets),
755 aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
757 auto f = lower_si.get_filter();
758 if (f == &filter_mark_ || f == &filter_scc_and_mark_)
760 const void* data = lower_si.get_filter_data();
761 auto& d = *
reinterpret_cast<const scc_and_mark_filter*
>(data);
762 cut_sets_ |= d.cut_sets_;
772 : lower_si_(nullptr), cut_sets_(cut_sets), aut_(aut),
773 old_acc_(aut_->get_acceptance())
777 ~scc_and_mark_filter()
779 restore_acceptance();
782 void override_acceptance(
const acc_cond& new_acc)
784 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(new_acc);
785 restore_old_acc_ =
true;
788 void restore_acceptance()
790 if (!restore_old_acc_)
792 std::const_pointer_cast<
twa_graph>(aut_)->set_acceptance(old_acc_);
793 restore_old_acc_ =
false;
796 const_twa_graph_ptr get_aut()
const 801 unsigned start_state()
const 804 return lower_si_->one_state_of(lower_scc_);
805 return aut_->get_init_state_number();
811 return filter_scc_and_mark_;
822 SPOT_API std::ostream&
823 dump_scc_info_dot(std::ostream& out,
824 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:751
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:683
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:770
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:555
int one_accepting_scc() const
Return the number of one accepting SCC if any, -1 otherwise.
Definition: sccinfo.hh:497
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:676
scc_info_options
Options to alter the behavior of scc_info.
Definition: sccinfo.hh:305
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: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:587
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:572
Graph-based representation of a TωA.
Definition: twagraph.hh:200
An acceptance mark.
Definition: acc.hh:87