29 #include <spot/misc/optionmap.hh> 30 #include <spot/twa/twagraph.hh> 31 #include <spot/twaalgos/emptiness_stats.hh> 36 typedef std::shared_ptr<twa_run> twa_run_ptr;
37 typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
110 virtual twa_run_ptr accepting_run();
127 const char* parse_options(
char* options);
134 virtual void options_updated(
const option_map& old);
140 typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
144 public std::enable_shared_from_this<emptiness_check>
168 const char* parse_options(
char* options);
171 virtual bool safe()
const;
187 virtual emptiness_check_result_ptr check() = 0;
193 virtual const ec_statistics* emptiness_check_statistics()
const;
196 virtual std::ostream& print_stats(std::ostream& os)
const;
199 virtual void options_updated(
const option_map& old);
206 typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
209 typedef std::shared_ptr<emptiness_check_instantiator>
210 emptiness_check_instantiator_ptr;
217 emptiness_check_ptr instantiate(
const const_twa_ptr& a)
const;
236 unsigned int min_sets()
const;
242 unsigned int max_sets()
const;
361 SPOT_API emptiness_check_instantiator_ptr
383 : s(s), label(label), acc(acc)
391 typedef std::list<step> steps;
398 twa_run(
const const_twa_ptr& aut)
409 twa_run_ptr reduce()
const;
419 twa_run_ptr project(
const const_twa_ptr& other,
bool right =
false);
431 bool replay(std::ostream& os,
bool debug =
false)
const;
436 void highlight(
unsigned color);
444 twa_graph_ptr as_twa(
bool preserve_names =
false)
const;
461 friend std::ostream& operator<<(std::ostream& os,
const twa_run& run);
Definition: automata.hh:26
Definition: emptiness.hh:377
Emptiness-check statistics.
Definition: emptiness_stats.hh:60
Common interface to emptiness check algorithms.
Definition: emptiness.hh:143
Manage a map of options.
Definition: optionmap.hh:37
const option_map & options() const
Definition: emptiness.hh:222
Abstract class for states.
Definition: twa.hh:50
Dynamically create emptiness checks. Given their name and options.
Definition: emptiness.hh:213
option_map o_
The options.
Definition: emptiness.hh:137
const option_map & options() const
Return the options parametrizing how the accepting run is computed.
Definition: emptiness.hh:121
emptiness_check_instantiator_ptr make_emptiness_check_instantiator(const char *name, const char **err)
Create an emptiness-check instantiator, given the name of an emptiness check.
An accepted run, for a twa.
Definition: emptiness.hh:375
const option_map & options() const
Return the options parametrizing how the emptiness check is realized.
Definition: emptiness.hh:162
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:136
The result of an emptiness check.
Definition: emptiness.hh:84
Definition: emptiness_stats.hh:35
option_map o_
The options.
Definition: emptiness.hh:203
const const_twa_ptr & automaton() const
The automaton that this emptiness-check inspects.
Definition: emptiness.hh:155
const const_twa_ptr & automaton() const
The automaton on which an accepting_run() was found.
Definition: emptiness.hh:114
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:202
option_map & options()
Definition: emptiness.hh:228