Compute a counter example from a spot::couvreur99_check_status.
More...
#include <spot/twaalgos/gtec/ce.hh>
|
typedef unsigned(unsigned_statistics::* | unsigned_fun) () const |
|
typedef std::map< const char *, unsigned_fun, char_ptr_less_than > | stats_map |
|
Compute a counter example from a spot::couvreur99_check_status.
◆ accepting_cycle()
void spot::couvreur99_check_result::accepting_cycle |
( |
| ) |
|
|
protected |
Called by accepting_run() to find a cycle which traverses all acceptance conditions in the accepted SCC.
◆ accepting_run()
virtual twa_run_ptr spot::couvreur99_check_result::accepting_run |
( |
| ) |
|
|
overridevirtual |
Return a run accepted by the automata passed to the emptiness check.
This method might actually compute the acceptance run. (Not all emptiness check algorithms actually produce a counter-example as a side-effect of checking emptiness, some need some post-processing.)
This can also return 0 if the emptiness check algorithm cannot produce a counter example (that does not mean there is no counter-example; the mere existence of an instance of this class asserts the existence of a counter-example).
Reimplemented from spot::emptiness_check_result.
◆ acss_states()
virtual unsigned spot::couvreur99_check_result::acss_states |
( |
| ) |
const |
|
overridevirtual |
◆ automaton()
const const_twa_ptr & spot::emptiness_check_result::automaton |
( |
| ) |
const |
|
inlineinherited |
◆ options_updated()
virtual void spot::emptiness_check_result::options_updated |
( |
const option_map & |
old | ) |
|
|
protectedvirtualinherited |
◆ parse_options()
const char * spot::emptiness_check_result::parse_options |
( |
char * |
options | ) |
|
|
inherited |
Modify the algorithm options.
◆ statistics()
Return statistics, if available.
◆ a_
const_twa_ptr spot::emptiness_check_result::a_ |
|
protectedinherited |
◆ o_
The documentation for this class was generated from the following file: