Since Spot 0.2, Spot uses a generic interface to designate EmptinessCheckAlgorithms and pass them options. This takes the form of a string like the following:
Algorithm(Option1 Option2 ...)
Of course, Algorithm specifies the emptiness-check algorithm. The parentheses are required only if any option is supplied. Internally, all options are stored as (string, integer) pair. In its more generic form, the option specification should look like a variable assignment. For instance
CVWY90(bsh=4000)
will instantiate the CVWY90 algorithm with option bsh set to 4000. The default value of each option depends on the algorithm.
The following shorthands are also supported
syntax |
same as |
option |
option=1 |
!option |
option=0 |
option=10K |
option=10240 |
option=10M |
option=10485760 |
Spot implements the following EmptinessCheckAlgorithms, with the following options.
1. Algorithms
Cou99 [couvreur.99.fm] The default behavior corresponds to that of the paper. 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
The setting of these 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.
Cou99 Cou99(shy !group) Cou99(shy group) Cou99(poprem) Cou99(poprem shy !group) Cou99(poprem shy group)
GV04 [geldenhuys.04.tacas] No options. Example:
GV04
CVWY90 [courcoubetis.90.cav]
bsh This option activates bit-state hashing. It should be set to the size of the hash map.
CVWY90 CVWY90(bsh=4M)
SE05 [schwoon.05.tacas]
bsh This option activates bit-state hashing. It should be set to the size of the hash map.
- Examples:
SE05 SE05(bsh=4M)
Tau03 [tauriainen.03.a83] No options. Example:
Tau03
Tau03_opt [couvreur.05.spin]
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 in a submitted paper.
ordering This option is unset by default, and activates the use of the "ordering" heuristic described by Heikki Tauriainen
in [tauriainen.05.a96].
Tau03_opt Tau03_opt(!weights) Tau03_opt(!redweights) Tau03_opt(condstack) Tau03_opt(condstack !weights) Tau03_opt(condstack !redweights)
