25 #include <spot/ta/taproduct.hh>
26 #include <spot/misc/optionmap.hh>
27 #include <spot/twaalgos/emptiness_stats.hh>
37 ta_succ_iterator_product*> pair_state_iter;
89 typedef state_map<int> hash_type;
113 check(
bool disable_second_pass =
false,
114 bool disable_heuristic_for_livelock_detection =
false);
121 livelock_detection(
const const_ta_product_ptr& t);
125 print_stats(std::ostream& os)
const;
129 clear(hash_type& h, std::stack<pair_state_iter> todo, std::queue<
133 clear(hash_type& h, std::stack<pair_state_iter> todo,
139 heuristic_livelock_detection(
const state * stuttering_succ,
140 hash_type& h,
int h_livelock_root, std::set<
const state*,
143 const_ta_product_ptr
a_;
147 bool is_full_2_pass_;
Emptiness-check statistics.
Definition: emptiness_stats.hh:121
Manage a map of options.
Definition: optionmap.hh:36
Abstract class for states.
Definition: twa.hh:43
const_ta_product_ptr a_
The automaton.
Definition: emptinessta.hh:143
An implementation of the emptiness-check algorithm for a product between a TA and a Kripke structure...
Definition: emptinessta.hh:87
option_map o_
The options.
Definition: emptinessta.hh:144
Iterate over the successors of a state.
Definition: ta.hh:197
Strict Weak Ordering for state*.
Definition: twa.hh:120