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
127 scc_info(const_twa_graph_ptr aut);
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();
189 acc_cond::mark_t acc(
unsigned scc)
const
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;
224 acc_cond::mark_t acc_sets_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
bool is_rejecting() const
Definition: sccinfo.hh:86
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:39
Definition: formula.hh:1671
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