26 #include <spot/twaalgos/gtec/status.hh> 27 #include <spot/twaalgos/emptiness.hh> 28 #include <spot/twaalgos/emptiness_stats.hh> 76 SPOT_API emptiness_check_ptr
122 couvreur99(
const const_twa_ptr& a, option_map options = option_map());
125 class SPOT_API couvreur99_check:
public emptiness_check,
public ec_statistics
131 couvreur99_check(
const const_twa_ptr& a, option_map o = option_map());
133 virtual ~couvreur99_check();
136 virtual emptiness_check_result_ptr check()
override;
138 virtual std::ostream& print_stats(std::ostream& os)
const override;
148 std::shared_ptr<const couvreur99_check_status> result()
const;
151 std::shared_ptr<couvreur99_check_status> ecs_;
157 void remove_component(
const state* start_delete);
163 unsigned get_removed_components()
const;
164 unsigned get_vmsize()
const;
177 virtual emptiness_check_result_ptr check()
override;
192 std::stack<acc_cond::mark_t> arc;
199 typedef std::list<successor> succ_queue;
202 succ_queue::iterator pos;
212 typedef std::list<todo_item> todo_list;
218 void dump_queue(std::ostream& os = std::cerr);
Definition: automata.hh:26
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:171
An implementation of the Couvreur99 emptiness-check algorithm.
Definition: gtec.hh:128
Abstract class for states.
Definition: twa.hh:50
unsigned removed_components
Number of dead SCC removed by the algorithm.
Definition: gtec.hh:162
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:160
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:223
An acceptance mark.
Definition: acc.hh:81