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;
140 typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
144 public std::enable_shared_from_this<emptiness_check>
187 virtual emptiness_check_result_ptr
check() = 0;
206 typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
209 typedef std::shared_ptr<emptiness_check_instantiator>
210 emptiness_check_instantiator_ptr;
361 SPOT_API emptiness_check_instantiator_ptr
383 : s(s), label(label), acc(acc)
389 typedef std::list<step> steps;
396 twa_run(
const const_twa_ptr& aut) noexcept
435 twa_run_ptr
project(
const const_twa_ptr& other,
bool right =
false);
447 bool replay(std::ostream& os,
bool debug =
false)
const;
460 twa_graph_ptr
as_twa(
bool preserve_names =
false)
const;
Emptiness-check statistics.
Definition: emptiness_stats.hh:61
Dynamically create emptiness checks. Given their name and options.
Definition: emptiness.hh:214
const option_map & options() const
Definition: emptiness.hh:222
emptiness_check_ptr instantiate(const const_twa_ptr &a) const
Actually instantiate the emptiness check, for a.
option_map & options()
Definition: emptiness.hh:228
unsigned int min_sets() const
Minimum number of acceptance sets supported by the emptiness check.
unsigned int max_sets() const
Maximum number of acceptance conditions supported by the emptiness check.
The result of an emptiness check.
Definition: emptiness.hh:85
virtual void options_updated(const option_map &old)
Notify option updates.
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
virtual twa_run_ptr accepting_run()
Return a run accepted by the automata passed to the emptiness check.
const char * parse_options(char *options)
Modify the algorithm options.
virtual const unsigned_statistics * statistics() const
Return statistics, if available.
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:136
Common interface to emptiness check algorithms.
Definition: emptiness.hh:145
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:202
option_map o_
The options.
Definition: emptiness.hh:203
virtual std::ostream & print_stats(std::ostream &os) const
Print statistics, if any.
virtual const ec_statistics * emptiness_check_statistics() const
Return emptiness check statistics, if available.
virtual bool safe() const
Return false iff accepting_run() can return 0 for non-empty automata.
virtual void options_updated(const option_map &old)
Notify option updates.
const option_map & options() const
Return the options parametrizing how the emptiness check is realized.
Definition: emptiness.hh:162
const char * parse_options(char *options)
Modify the algorithm options.
virtual const unsigned_statistics * statistics() const
Return statistics, if available.
const const_twa_ptr & automaton() const
The automaton that this emptiness-check inspects.
Definition: emptiness.hh:155
virtual emptiness_check_result_ptr check()=0
Check whether the automaton contain an accepting run.
Manage a map of options.
Definition: optionmap.hh:38
Abstract class for states.
Definition: twa.hh:51
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.
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85
Definition: emptiness.hh:377
An accepted run, for a twa.
Definition: emptiness.hh:376
void highlight(unsigned color)
Highlight the accepting run on the automaton.
twa_run_ptr project(const const_twa_ptr &other, bool right=false)
Project an accepting run.
void ensure_non_empty_cycle(const char *where) const
Raise an exception of the cycle is empty.
twa_graph_ptr as_twa(bool preserve_names=false) const
Convert the run into a lasso-shaped automaton.
twa_run_ptr reduce() const
Reduce an accepting run.
friend std::ostream & operator<<(std::ostream &os, const twa_run &run)
Display a twa_run.
bool replay(std::ostream &os, bool debug=false) const
Replay a run.
Definition: emptiness_stats.hh:36