spot-x − Common fine-tuning options and environment variables.
−−extra-options
STRING
−x STRING
Common fine−tuning options for binaries built with Spot.
The argument of −x or −−extra−options is a comma−separated list of KEY=INT assignments that are passed to the post−processing routines (they may be passed to other algorithms in the future). These options are mostly used for benchmarking and debugging purpose. KEYR (without any value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.
comp−susp
Set to 1 to enable compositional suspension, as described in our SPIN’13 paper (see Bibliography below). Set to 2, to build only the skeleton TGBA without composing it. Set to 0 (the default) to disable.
early−susp
When set to 1, start compositional suspension on the transitions that enter accepting SCCs, and not only on the transitions inside accepting SCCs. This option defaults to 0, and is only used when comp−susp=1.
skel−simul
Default to 1. Set to 0 to disable simulation on the skeleton automaton during compositional suspension. Only used when comp−susp=1.
skel−wdba
Set to 0 to disable WDBA minimization on the skeleton automaton during compositional suspension. Set to 1 always WDBA−minimize the skeleton . Set to 2 to keep the WDBA only if it is smaller than the original skeleton. This option is only used when comp−susp=1 and default to 1 or 2 depending on whether −−small or −−deterministic is specified.
ba−simul
Set to 0 to disable simulation−based reductions on the Büchi automaton (i.e., after degeneralization has been performed). Set to 1 to use only direct simulation. Set to 2 to use only reverse simulation. Set to 3 to iterate both direct and reverse simulations. The default is 3 in −−high mode, and 0 otherwise.
degen−lcache
If non−zero (the default is 1), whenever the degeneralization algorithm enters an SCC on a state that has already been associated to a level elsewhere, it should reuse that level. Different values can be used to select which level to reuse: 1 always uses the first level created, 2 uses the minimum level seen so far, and 3 uses the maximum level seen so far. The "lcache" stands for "level cache".
degen−lowinit
Whenever the degeneralization algorihm enters a new SCC (or starts from the initial state), it starts on some level L that is compatible with all outgoing transitions. If degen−lowinit is zero (the default) and the corresponding state (in the generalized automaton) has an accepting self−loop, then level L is replaced by the accepting level, as it might favor finding accepting cycles earlier. If degen−lowinit is non−zero, then level L is always used without looking for the presence of an accepting self−loop.
degen−lskip
If non−zero (the default), the degeneralization algorithm will skip as much levels as possible for each transition. This is enabled by default as it very often reduce the number of resulting states. A consequence of skipping levels is that the degeneralized automaton tends to have smaller cycles around the accepting states. Disabling skipping will produce automata with large cycles, and often with more states.
degen−order
If non−zero, the degeneralization algorithm will compute an independent degeneralization order for each SCC it processes. This is currently disabled by default.
degen−reset
If non−zero (the default), the degeneralization algorithm will reset its level any time it exits an SCC.
det−scc
Set to 0 to disable scc−based optimizations in the determinization algorithm.
det−simul
Set to 0 to disable simulation−based optimizations in the determinization algorithm.
det−stutter
Set to 0 to disable optimizations based on the stutter−invariance in the determinization algorithm.
sat−acc
When this is set to some positive integer, the SAT−based will attempt to construct a TGBA with the given number of acceptance sets. states. It may however return an automaton with less acceptance sets if some of these are useless. Setting sat−acc automatically sets sat−minimize to 1 if not set differently.
sat−minimize
Set to 1 to enable SAT−based minimization of deterministic TGBA: it starts with the number of states of the input, and iteratively tries to find a deterministic TGBA with one less state. Set to 2 to perform a binary search instead. Disabled (0) by default. The sat solver to use can be set with the SPOT_SATSOLVER environment variable (see below). By default the procedure looks for a TGBA with the same number of acceptance set; this can be changed with the sat−acc option, or of course by using −B to construct a Büchi automaton. Enabling SAT−based minimization will also enable tba−det.
sat−states
When this is set to some positive integer, the SAT−based minimization will attempt to construct a TGBA with the given number of states. It may however return an automaton with less states if some of these are unreachable or useless. Setting sat−states automatically enables sat−minimize, but no iteration is performed. If no equivalent automaton could be constructed with the given number of states, the original automaton is returned.
scc−filter
Set to 1 (the default) to enable SCC−pruning and acceptance simplification at the beginning of post−processing. Transitions that are outside of accepting SCC are removed from accepting sets, except those that enter into an accepting SCC. Set to 2 to remove even these entering transition from the accepting sets. Set to 0 to disable this SCC−pruning and acceptance simpification pass.
simul |
Set to 0 to disable simulation−based reductions. Set to 1 to use only direct simulation. Set to 2 to use only reverse simulation. Set to 3 to iterate both direct and reverse simulations. The default is 3, except when option −−low is specified, in which case the default is 1. |
state−based
Set to 1 to instruct the SAT−minimization procedure to produce a TGBA where all outgoing transition of a state have the same acceptance sets. By default this is only enabled when option −B is used.
tba−det
Set to 1 to attempt a powerset determinization if the TGBA is not already deterministic. Doing so will degeneralize the automaton. This is disabled by default, unless sat−minimize is set.
wdba−minimize
Set to 0 to disable WDBA−minimization. Enabled by default.
SPOT_DEFAULT_FORMAT
Set to a value of dot or hoa to override the default format used to output automata. Up to Spot 1.9.6 the default output format for automata used to be dot. Starting with Spot 1.9.7, the default output format switched to hoa as it is more convenient when chaining tools in a pipe. Set this variable to dot to get the old behavior. Additional options may be passed to the printer by suffixing the output format with = and the options. For instance running
% SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
is the same as running
% autfilt --dot=bar ...
but the use of the environment variable makes more sense if you set it up once for many commands.
SPOT_DOTDEFAULT
Whenever the --dot option is used without argument (even implicitely via SPOT_DEFAULT_FORMAT), the contents of this variable is used as default argument. If you have some default settings in SPOT_DOTDEFAULT and want to append to options xyz temporarily for one call, use --dot=.xyz: the dot character will be replaced by the contents of the SPOT_DOTDEFAULT environment variable.
SPOT_DOTEXTRA
The contents of this variable is added to any dot output, immediately before the first state is output. This makes it easy to override global attributes of the graph.
SPOT_SATLOG
If set to a filename, the SAT-based minimization routines will append statistics about each iteration to the named file. Each line lists the following comma-separated values: requested number of states, number of reachable states in the output, number of edges in the output, number of transitions in the output, number of variables in the SAT problem, number of clauses in the SAT problem, user time for encoding the SAT problem, system time for encoding the SAT problem, user time for solving the SAT problem, system time for solving the SAT problem.
SPOT_SATSOLVER
If set, this variable should indicate how to call a SAT−solver. This is used by the sat−minimize option described above. The default value is "glucose -verb=0 -model %I >%O", it is correct for glucose version 3.0 (for older versions, remove the W(-model option). The escape sequences %I and %O respectively denote the names of the input and output files. These temporary files are created in the directory specified by SPOT_TMPDIR or TMPDIR (see below). The SAT-solver should follow the convention of the SAT Competition for its input and output format.
SPOT_STREETT_CONV_MIN
The number of Streett pairs above which conversion from Streett acceptance to generalized-Büchi acceptance should be made with a dedicated algorithm. By default this is 3, i.e., if a Streett automaton with 3 acceptance pairs or more has to be converted into generalized-Büchi, the dedicated algorithm is used. This algorithm is close to the classical conversion from Streett to Büchi, but with several tweaks. When this algorithm is not used, the standard "Fin-removal" approach is used instead: first the acceptance condition is converted into disjunctive normal form (DNF), then Fin acceptance is removed like for Rabin automata, yielding a disjuction of generalized Büchi acceptance, and the result is finally converted into conjunctive normal form (CNF) to obtain a generalized Büchi acceptance. Both algorithms have a worst-case size that is exponential in the number of Streett pairs, but in practice the dedicated algorithm works better for most Streett automata with 3 or more pairs (and many 2-pair Streett automata as well, but the difference here is less clear). Setting this variable to 0 will disable the dedicated algorithm. Setting it to 1 will enable it for all Streett automata, however we do not recommand setting it to less than 2, because the "Fin-removal" approach is better for single-pair Streett automata.
SPOT_TMPDIR, TMPDIR
These variables control in which directory temporary files (e.g., those who contain the input and output when interfacing with translators) are created. TMPDIR is only read if SPOT_TMPDIR does not exist. If none of these environment variables exist, or if their value is empty, files are created in the current directory.
SPOT_TMPKEEP
When this variable is defined, temporary files are not removed. This is mostly useful for debugging.
1. |
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA’07. LNCS 4762. |
Describes the WDBA-minimization algorithm implemented in Spot. The algorithm used for the tba-det options is also a generalization (to TBA instead of BA) of what they describe in sections 3.2 and 3.3.
2. |
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček: Compositional Approach to Suspension and Other Improvements to LTL Translation. Proceedings of SPIN’13. LNCS 7976. |
Describes the compositional suspension, the simulation-based reductions, and the SCC-based simplifications.
3. |
Rüdiger Ehlers: Minimising Deterministic Büchi Automata Precisely using SAT Solving. Proceedings of SAT’10. LNCS 6175. |
Our SAT-based minimization procedures are generalizations of this paper to deal with TBA or TGBA.
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2016 Laboratoire de Recherche et Développement
de l’Epita. License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and
redistribute it. There is NO WARRANTY, to the extent
permitted by law.
ltl2tgba(1) ltl2tgta(1) dstar2tgba(1) autfilt(1)