22 #include <spot/ta/taproduct.hh> 23 #include <spot/misc/optionmap.hh> 24 #include <spot/twaalgos/emptiness_stats.hh> 34 ta_succ_iterator_product*> pair_state_iter;
87 typedef state_map<int> hash_type;
111 check(
bool disable_second_pass =
false,
112 bool disable_heuristic_for_livelock_detection =
false);
119 livelock_detection(
const const_ta_product_ptr& t);
123 print_stats(std::ostream& os)
const;
127 clear(hash_type& h, std::stack<pair_state_iter> todo, std::queue<
131 clear(hash_type& h, std::stack<pair_state_iter> todo,
137 heuristic_livelock_detection(
const state * stuttering_succ,
138 hash_type& h,
int h_livelock_root, std::set<
const state*,
141 const_ta_product_ptr
a_;
145 bool is_full_2_pass_;
Definition: automata.hh:26
Emptiness-check statistics.
Definition: emptiness_stats.hh:60
Manage a map of options.
Definition: optionmap.hh:37
Abstract class for states.
Definition: twa.hh:50
const_ta_product_ptr a_
The automaton.
Definition: emptinessta.hh:141
Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is emp...
Definition: emptinessta.hh:85
option_map o_
The options.
Definition: emptinessta.hh:142
Iterate over the successors of a state.
Definition: ta.hh:197
Strict Weak Ordering for state*.
Definition: twa.hh:127