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.
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.
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.
virtual unsigned spot::couvreur99_check_result::acss_states |
( |
| ) |
const |
|
overridevirtual |
const const_twa_ptr& spot::emptiness_check_result::automaton |
( |
| ) |
const |
|
inlineinherited |
const option_map& spot::emptiness_check_result::options |
( |
| ) |
const |
|
inlineinherited |
Return the options parametrizing how the accepting run is computed.
virtual void spot::emptiness_check_result::options_updated |
( |
const option_map & |
old | ) |
|
|
protectedvirtualinherited |
const char* spot::emptiness_check_result::parse_options |
( |
char * |
options | ) |
|
|
inherited |
Modify the algorithm options.
Return statistics, if available.
const_twa_ptr spot::emptiness_check_result::a_ |
|
protectedinherited |
The documentation for this class was generated from the following file: