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:
131 public ec_statistics,
public emptiness_check
134 couvreur99_check(
const const_twa_ptr& a, option_map o = option_map());
136 virtual ~couvreur99_check();
139 virtual emptiness_check_result_ptr check()
override;
141 virtual std::ostream& print_stats(std::ostream& os)
const override;
151 std::shared_ptr<const couvreur99_check_status> result()
const;
154 std::shared_ptr<couvreur99_check_status> ecs_;
160 void remove_component(
const state* start_delete);
167 unsigned get_removed_components()
const;
168 unsigned get_vmsize()
const;
181 virtual emptiness_check_result_ptr check()
override;
196 std::stack<acc_cond::mark_t> arc;
203 typedef std::list<successor> succ_queue;
206 succ_queue::iterator pos;
216 typedef std::list<todo_item> todo_list;
222 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:175
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:165
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:163
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:227
An acceptance mark.
Definition: acc.hh:81