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
111 assert(scc < node_.size());
116 scc_info(const_twa_graph_ptr aut);
118 const_twa_graph_ptr get_aut()
const
123 unsigned scc_count()
const
128 bool reachable_state(
unsigned st)
const
130 return scc_of(st) != -1
U;
133 unsigned scc_of(
unsigned st)
const
135 assert(st < sccof_.size());
140 SPOT_RETURN(node_.begin());
142 SPOT_RETURN(node_.end());
144 SPOT_RETURN(node_.cbegin());
146 SPOT_RETURN(node_.cend());
148 SPOT_RETURN(node_.rbegin());
150 SPOT_RETURN(node_.rend());
152 const
std::vector<
unsigned>& states_of(
unsigned scc)
const
154 return node(scc).states();
157 unsigned one_state_of(
unsigned scc)
const
159 return states_of(scc).front();
165 assert(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
166 return scc_count() - 1;
169 const scc_succs& succ(
unsigned scc)
const
171 return node(scc).succ();
174 bool is_trivial(
unsigned scc)
const
176 return node(scc).is_trivial();
179 acc_cond::mark_t acc(
unsigned scc)
const
181 return node(scc).acc_marks();
184 bool is_accepting_scc(
unsigned scc)
const
186 return node(scc).is_accepting();
189 bool is_rejecting_scc(
unsigned scc)
const
191 return node(scc).is_rejecting();
196 void determine_unknown_acceptance();
198 bool is_useful_scc(
unsigned scc)
const
200 return node(scc).is_useful();
203 bool is_useful_state(
unsigned st)
const
205 return reachable_state(st) && node(scc_of(st)).is_useful();
210 std::vector<std::set<acc_cond::mark_t>> used_acc()
const;
212 std::set<acc_cond::mark_t> used_acc_of(
unsigned scc)
const;
214 acc_cond::mark_t acc_sets_of(
unsigned scc)
const;
216 std::vector<bool> weak_sccs()
const;
218 bdd scc_ap_support(
unsigned scc)
const;
225 SPOT_API std::ostream&
226 dump_scc_info_dot(std::ostream& out,
227 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:1652
unsigned initial() const
Get number of the SCC containing the initial state.
Definition: sccinfo.hh:163
bool is_accepting() const
True if we are sure that the SCC is accepting.
Definition: sccinfo.hh:65