23 #include <spot/twa/twagraph.hh>
30 typedef std::vector<unsigned> scc_succs;
38 std::vector<unsigned> states_;
45 acc_(0
U), trivial_(
true), accepting_(
false),
46 rejecting_(
false), useful_(
false)
51 acc_(acc), trivial_(trivial), accepting_(
false),
52 rejecting_(
false), useful_(
false)
56 bool is_trivial()
const
79 bool is_useful()
const
89 const std::vector<unsigned>& states()
const
94 const scc_succs& succ()
const
102 std::vector<unsigned> sccof_;
103 std::vector<scc_node> node_;
104 const_twa_graph_ptr aut_;
107 void determine_usefulness();
109 const scc_node& node(
unsigned scc)
const
115 scc_info(const_twa_graph_ptr aut);
117 const_twa_graph_ptr get_aut()
const
122 unsigned scc_count()
const
127 bool reachable_state(
unsigned st)
const
129 return scc_of(st) != -1
U;
132 unsigned scc_of(
unsigned st)
const
138 SPOT_RETURN(node_.begin());
140 SPOT_RETURN(node_.end());
142 SPOT_RETURN(node_.cbegin());
144 SPOT_RETURN(node_.cend());
146 SPOT_RETURN(node_.rbegin());
148 SPOT_RETURN(node_.rend());
150 const
std::vector<
unsigned>& states_of(
unsigned scc)
const
152 return node(scc).states();
155 unsigned one_state_of(
unsigned scc)
const
157 return states_of(scc).front();
163 SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
164 return scc_count() - 1;
167 const scc_succs& succ(
unsigned scc)
const
169 return node(scc).succ();
172 bool is_trivial(
unsigned scc)
const
174 return node(scc).is_trivial();
177 acc_cond::mark_t acc(
unsigned scc)
const
179 return node(scc).acc_marks();
182 bool is_accepting_scc(
unsigned scc)
const
184 return node(scc).is_accepting();
187 bool is_rejecting_scc(
unsigned scc)
const
189 return node(scc).is_rejecting();
194 void determine_unknown_acceptance();
196 bool is_useful_scc(
unsigned scc)
const
198 return node(scc).is_useful();
201 bool is_useful_state(
unsigned st)
const
203 return reachable_state(st) && node(scc_of(st)).is_useful();
208 std::vector<std::set<acc_cond::mark_t>> used_acc()
const;
210 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const;
212 acc_cond::mark_t acc_sets_of(
unsigned scc)
const;
214 std::vector<bool> weak_sccs()
const;
216 bdd scc_ap_support(
unsigned scc)
const;
223 SPOT_API std::ostream&
224 dump_scc_info_dot(std::ostream& out,
225 const_twa_graph_ptr aut, scc_info* sccinfo =
nullptr);
Definition: sccinfo.hh:32
bool is_rejecting() const
Definition: sccinfo.hh:74
Definition: sccinfo.hh:27
Definition: formula.hh:1671
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:161
bool is_accepting() const
True if we are sure that the SCC is accepting.
Definition: sccinfo.hh:65