23 #include <spot/twa/twagraph.hh> 42 typedef std::vector<unsigned> scc_succs;
50 std::vector<unsigned> states_;
57 acc_(0
U), trivial_(
true), accepting_(
false),
58 rejecting_(
false), useful_(
false)
63 acc_(acc), trivial_(trivial), accepting_(
false),
64 rejecting_(
false), useful_(
false)
68 bool is_trivial()
const 91 bool is_useful()
const 101 const std::vector<unsigned>& states()
const 106 const scc_succs& succ()
const 114 std::vector<unsigned> sccof_;
115 std::vector<scc_node> node_;
116 const_twa_graph_ptr aut_;
119 void determine_usefulness();
121 const scc_node& node(
unsigned scc)
const 129 const_twa_graph_ptr get_aut()
const 134 unsigned scc_count()
const 139 bool reachable_state(
unsigned st)
const 141 return scc_of(st) != -1
U;
144 unsigned scc_of(
unsigned st)
const 150 SPOT_RETURN(node_.begin());
152 SPOT_RETURN(node_.end());
154 SPOT_RETURN(node_.cbegin());
156 SPOT_RETURN(node_.cend());
158 SPOT_RETURN(node_.rbegin());
160 SPOT_RETURN(node_.rend());
162 const std::vector<unsigned>& states_of(
unsigned scc)
const 164 return node(scc).states();
167 unsigned one_state_of(
unsigned scc)
const 169 return states_of(scc).front();
175 SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
176 return scc_count() - 1;
179 const scc_succs& succ(
unsigned scc)
const 181 return node(scc).succ();
184 bool is_trivial(
unsigned scc)
const 186 return node(scc).is_trivial();
191 return node(scc).acc_marks();
194 bool is_accepting_scc(
unsigned scc)
const 196 return node(scc).is_accepting();
199 bool is_rejecting_scc(
unsigned scc)
const 201 return node(scc).is_rejecting();
206 void determine_unknown_acceptance();
208 bool is_useful_scc(
unsigned scc)
const 210 return node(scc).is_useful();
213 bool is_useful_state(
unsigned st)
const 215 return reachable_state(st) && node(scc_of(st)).is_useful();
220 std::vector<std::set<acc_cond::mark_t>> used_acc()
const;
222 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const;
226 std::vector<bool> weak_sccs()
const;
228 bdd scc_ap_support(
unsigned scc)
const;
235 SPOT_API std::ostream&
236 dump_scc_info_dot(std::ostream& out,
237 const_twa_graph_ptr aut,
scc_info* sccinfo =
nullptr);
Definition: sccinfo.hh:44
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:39
bool is_rejecting() const
Definition: sccinfo.hh:86
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:173
bool is_accepting() const
True if we are sure that the SCC is accepting.
Definition: sccinfo.hh:77