|
spot 2.12.2
|
Modules | |
| Emptiness-check algorithms | |
| TωA runs and supporting functions | |
| Emptiness-check statistics | |
Classes | |
| class | spot::emptiness_check_result |
| The result of an emptiness check. More... | |
| class | spot::emptiness_check |
| Common interface to emptiness check algorithms. More... | |
| class | spot::emptiness_check_instantiator |
| Dynamically create emptiness checks. Given their name and options. More... | |
Typedefs | |
| typedef std::shared_ptr< emptiness_check_result > | spot::emptiness_check_result_ptr |
| typedef std::shared_ptr< emptiness_check > | spot::emptiness_check_ptr |
| typedef std::shared_ptr< emptiness_check_instantiator > | spot::emptiness_check_instantiator_ptr |
Functions | |
| emptiness_check_instantiator_ptr | spot::make_emptiness_check_instantiator (const char *name, const char **err) |
| Create an emptiness-check instantiator, given the name of an emptiness check. More... | |
You can create an emptiness check either by instantiating it explicitly (calling one of the functions of this list), or indirectly via spot::make_emptiness_check_instantiator(). The latter function allows user-options to influence the choice of the emptiness-check algorithm used, and the intermediate instantiator object can be used to query to properties of the emptiness check selected.
All emptiness-check algorithms follow the same interface. Basically once you have constructed an instance of spot::emptiness_check, you should call spot::emptiness_check::check() to check the automaton.
If spot::emptiness_check::check() returns 0, then the automaton was found empty. Otherwise the automaton accepts some run. (Beware that some algorithms—those using bit-state hashing—may found the automaton to be empty even if it is not actually empty.)
When spot::emptiness_check::check() does not return 0, it returns an instance of spot::emptiness_check_result. You can try to call spot::emptiness_check_result::accepting_run() to obtain an accepting run. For some emptiness-check algorithms, spot::emptiness_check_result::accepting_run() will require some extra computation. Most emptiness-check algorithms are able to return such an accepting run, however this is not mandatory and spot::emptiness_check_result::accepting_run() can return 0 (this does not means by anyway that no accepting run exist).
The acceptance run returned by spot::emptiness_check_result::accepting_run(), if any, is of type spot::twa_run. This page gathers existing operations on these objects.
| emptiness_check_instantiator_ptr spot::make_emptiness_check_instantiator | ( | const char * | name, |
| const char ** | err | ||
| ) |
#include <spot/twaalgos/emptiness.hh>
Create an emptiness-check instantiator, given the name of an emptiness check.
This is a convenient entry point to instantiate an emptiness check with user-supplied options.
| name | should have the form "name" or "name(options)". |
nullptr. If the name of the algorithm was unknown, *err will be set to name. If some fragment of the options could not be parsed, *err will point to that fragment.The following names supported and correspond to different emptiness check algorithms:
Cou99 uses spot::couvreur99(), that works with Fin-less acceptance conditions, with any number of acceptance sets. The following options can be used:
shy Compute all successors of each state, then explore already visited states first. This usually helps to merge SCCs, and thus exit sooner. However because all successors have to be computed and stored, it often consume more memory.group Setting this option is meaningful only when shy is used. If set (the default), the successors of all the states that belong to the same SCC will be considered when choosing a successor. Otherwise, only the successor of the topmost state on the DFS stack are considered.poprem Specifies how the algorithm should handle the destruction of non-accepting maximal strongly connected components. If poprem is set, the algorithm will keep a list of all states of a SCC that are fully processed and should be removed once the MSCC is popped. If poprem is unset (the default), the MSCC will be traversed again (i.e. generating the successors of the root recursively) for deletion. This is a choice between memory and speed.Examples:
GC04 uses spot::explicit_gv04_check() and works on automata with Fin-less acceptance conditions using at most one acceptance set. No options are supported.
Example:
CVWY90 uses spot::magic_search() and work on automata with Fin-less acceptance conditions using at most one acceptance set. Set option bsh to the size of a hash-table if you want to activate bit-state hashing.
Examples:
SE05 uses spot::se05() and works on work on automata with Fin-less acceptance conditions using at most one acceptance set. Set option bsh to the size of a hash-table if you want to activate bit-state hashing.
Examples:
Tau03 uses spot::explicit_tau03_search() and work on automata with Fin-less acceptance conditions using at least one acceptance set. No options are supported.
Example:
Tau03_opt uses spot::explicit_tau03_opt_search() and work on automata with any Fin-less acceptance. The following options are supported:
weights This option is set by default and activates the usage of weights in the top-level DFS as well as in nested DFSs.redweights This option is set by default, and activates the usage of weights in nested DFSs. It is meaningful only if weights is set.condstack This option is unset by default, and activates the use of the "conditional stack" optimization described by Heikki Tauriainen.Example:
1.9.4