26 #include <spot/twaalgos/gtec/status.hh> 27 #include <spot/twaalgos/emptiness.hh> 28 #include <spot/twaalgos/emptiness_stats.hh> 93 SPOT_API emptiness_check_ptr
139 couvreur99(
const const_twa_ptr& a, option_map options = option_map());
142 class SPOT_API couvreur99_check:
public emptiness_check,
public ec_statistics
148 couvreur99_check(
const const_twa_ptr& a, option_map o = option_map());
150 virtual ~couvreur99_check();
153 virtual emptiness_check_result_ptr check()
override;
155 virtual std::ostream& print_stats(std::ostream& os)
const override;
165 std::shared_ptr<const couvreur99_check_status> result()
const;
168 std::shared_ptr<couvreur99_check_status> ecs_;
174 void remove_component(
const state* start_delete);
180 unsigned get_removed_components()
const;
181 unsigned get_vmsize()
const;
194 virtual emptiness_check_result_ptr check()
override;
208 std::stack<acc_cond::mark_t> arc;
215 typedef std::list<successor> succ_queue;
218 succ_queue::iterator pos;
228 typedef std::list<todo_item> todo_list;
234 void dump_queue(std::ostream& os = std::cerr);
Manage a map of options.
Definition: optionmap.hh:37
A version of spot::couvreur99_check that tries to visit known states first.
Definition: gtec.hh:188
An implementation of the Couvreur99 emptiness-check algorithm.
Definition: gtec.hh:145
Abstract class for states.
Definition: twa.hh:50
unsigned removed_components
Number of dead SCC removed by the algorithm.
Definition: gtec.hh:179
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:177
emptiness_check_ptr couvreur99(const const_twa_ptr &a, option_map options=option_map())
Check whether the language of an automate is empty.
bool group_
Whether successors should be grouped for states in the same SCC.
Definition: gtec.hh:237