spot-x - Common fine-tuning options and environment variables.
Common fine-tuning options for binaries built with Spot.
The argument of -x
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.
- Control usage of implication-based rewriting. (0) disables it, (1) enables
rules based on syntactic implications, (2) additionally allows
automata-based implication checks, (3) enables more rules based on
automata-based implication checks. The default value depends on the
- 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.
- 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.
- Set to 0 to disable the translation of automata as product or sum of
- Default to 1. Set to 0 to disable simulation on the skeleton automaton
during compositional suspension. Only used when comp-susp=1.
- 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.
- 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.
- 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".
- 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
- 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.
- If non-zero, the degeneralization algorithm will compute an independent
degeneralization order for each SCC it processes. This is currently
disabled by default.
- If non-zero (the default), make sure the output of the degenalization has
as many SCCs as the input, by removing superfluous ones.
- If non-zero (the default), the degeneralization algorithm will reset its
level any time it exits an SCC.
- Set to 0 to disable scc-based optimizations in the determinization
- Set to 0 to disable simulation-based optimizations in the determinization
- Set to 0 to disable optimizations based on the stutter-invariance in the
- Set to 0 to disable alternate constructions for GF(guarantee)->[D]BA
and FG(safety)->DCA. Those constructions are from an LICS'18 paper by
J. Esparza, J. Křentínský, and S. Sickert. This is
enabled by default for medium and high optimization levels. Unless we are
building deterministic automata, the resulting automata are compared to
the automata built using the more traditional pipeline, and only kept if
they are better.
- If set to a positive integer N, a formula with N atomic propositions or
more will have its Boolean subformulas abstracted as atomic propositions
during the translation to automaton. This relabeling can speeds the
translation if a few Boolean subformulas use a large number of atomic
propositions. By default N=4. Setting this value to 0 will disable the
- 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
- Set the value of sat-incr-steps. This variable is used by two SAT-based
minimization algorithms: (2) and (3). They are both described below.
- Find the lower bound of default sat-minimize procedure (1). This relies on
the fact that the size of the minimal automaton is at least equal to the
total number of different languages recognized by the automaton's
- Set it to enable SAT-based minimization of deterministic TGBA. Depending
on its value (from 1 to 4) it changes the algorithm to perform. The
default value is (1) and it proves to be the most effective method.
SAT-based minimization uses PicoSAT (distributed with Spot), but another
installed SAT-solver can be set thanks to the SPOT_SATSOLVER environment
variable. Enabling SAT-based minimization will also enable tba-det.
- 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.
- 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.
- 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.
- 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.
- 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.
- Set to 0 to disable WDBA-minimization. Enabled by default.
- Used by default, 1 performs a binary search, checking N/2, etc. The
upper bound being N (the size of the starting automaton), the lower bound
is always 1 except when sat-langmap option is used.
- Use PicoSAT assumptions. Each iteration encodes the search of an (N-1)
state equivalent automaton, and additionally assumes that the last
sat-incr-steps states are unnecessary. On failure, relax the
assumptions to do a binary search between N-1 and N-1-
sat-incr-steps. sat-incr-steps defaults to 6.
- After an (N-1) state automaton has been found, use incremental solving for
the next sat-incr-steps iterations by forbidding the usage of an
additional state without reencoding the problem again. A full encoding
will occur after sat-incr-steps iterations unless
sat-incr-steps=-1 (see SPOT_XCNF environment variable).
sat-incr-steps defaults to 2.
- This naive method tries to reduce the size of the automaton one state at a
time. Note that it restarts all the encoding each time.
- If this variable is set to any value, statistics about BDD garbage
collection and resizing will be output on standard error.
- 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.
- If this variable is set to any value, the automaton parser of Spot is
executed in debug mode, showing how the input is processed.
- 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.
- 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.
- If this variable is set, a few sanity checks performed by the HOA parser
are skipped. The tests in questions correspond to issues in third-party
tools that output incorrect HOA (e.g., declaring the automaton with
property "univ-branch" when no universal branching is actually
- Specifies the default algorithm that should be used by the is_obligation()
function. The value should be one of the following:
- Make sure that the formula and its negation are realizable by
non-deterministic co-Büchi automata.
- Make sure that the formula and its negation are realizable by
deterministic Büchi automata.
- Make sure that the formula is realizable by a weak and deterministic
- If this variable is set, Out-Of-Memory errors will abort() the program
(potentially generating a coredump) instead of raising an exception. This
is useful to debug a program and to obtain a stack trace pointing to the
function doing the allocation. When this variable is unset (the default),
std::bad_alloc are thrown on memory allocation failures, and the stack is
usually unwinded up to top-level, losing the original context of the
error. Note that at least ltlcross has some custom handling of
std::bad_alloc to recover from products that are too large (by ignoring
them), and setting this variable will interfer with that.
- Select the default algorithm that must be used to check the persistence or
recurrence property of a formula f. The values it can take are 1 or 2.
Both methods work either on f or !f thanks to the duality of persistence
and recurrence classes. See
"https://spot.lrde.epita.fr/hierarchy.html" for more details. If
it is set to:
- It will try to check if f (or !f) is co-Büchi realizable in order
to tell if f belongs to the persistence (or the recurrence) class.
- It checks if f (or !f) is det-Büchi realizable to tell if f belongs
to the recurrence (or the persistence) class.
- 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: input number of states, target 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,
automaton produced at this step in HOA format.
- If set, this variable should indicate how to call an external SAT-solver -
by default, Spot uses PicoSAT, which is distributed with. This is used by
the sat-minimize option described above. The format to follow is the
following: "<sat_solver> [options] %I >%O". 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
- 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.
- Select the default check used to decide stutter invariance. The variable
should hold a value between 1 and 8, corresponding to the following tests
described in our Spin'15 paper (see the BIBLIOGRAPHY section). The default
- sl(a) x sl(!a)
- sl(cl(a)) x !a
- cl(sl(a)) x !a
- sl2(a) x sl2(!a)
- sl2(cl(a)) x !a
- cl(sl2(a)) x !a
- sl(a) x sl(!a), performed on-the-fly
- cl(a) x cl(!a)
- 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.
- When this variable is defined, temporary files are not removed. This is
mostly useful for debugging.
- Assign a folder path to this variable to generate XCNF files whenever
SAT-based minimization is used - the file is outputed as
"incr.xcnf" in the specified directory. This feature works only
with an external SAT-solver. See SPOT_SATSOLVER to know how to
provide one. Also note that this needs an incremental approach without
restarting the encoding i.e "sat-minimize=3,param=-1" for
ltl2tgba and ltl2tgta or "incr,param=-1" for autfilt (see
sat-minimize options described above or autfilt man page). The XCNF format
is the one used by the SAT incremental competition.
- 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.
- 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.
- 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.
- Thibaud Michaud and Alexandre Duret-Lutz: Practical stutter-invariance
checks for ω-regular languages, Proceedings of SPIN'15. LNCS 9232.
Describes the stutter-invariance checks that can be selected through
- Javier Esparza, Jan Křetínský and Salomon Sickert:
One Theorem to Rule Them All: A Unified Translation of LTL into
ω-Automata. Proceedings of LICS'18. To appear.
Describes (among other things) the constructions used for translating
formulas of the form GF(guarantee) or FG(safety), that can be disabled
with -x gf-guarantee=0.
Report bugs to <firstname.lastname@example.org>.
Copyright © 2018 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.
Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.