NAME

SYNOPSIS

DESCRIPTION

The argument of -x or --extra-options is a comma-separated list of KEY=INT assignments that are passed to the post-processing or translation routines (they may be passed to other algorithms in the future). These options are mostly used for benchmarking and debugging purpose. KEY (without any value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.

SAT-MINIMIZE VALUES

1

The default, 1, performs a binary search between 1 and N. The lower bound can sometimes be improved when the sat-langmap option is used.

2

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.

3

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.

4

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.

ENVIRONMENT VARIABLES

SPOT_BDD_TRACE

If this variable is set to any value, statistics about BDD garbage collection and resizing will be output on standard error.

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_DEBUG_PARSER

If this variable is set to any value, the automaton parser of Spot is executed in debug mode, showing how the input is processed.

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_HOA_TOLERANT

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 used)

SPOT_O_CHECK

Specifies the default algorithm that should be used by the is_obligation() function. The value should be one of the following:

SPOT_OOM_ABORT

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.

SPOT_PR_CHECK

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 between 1 and 3. All methods work either on f or !f thanks to the duality of persistence and recurrence classes. See this page for more details. If it is set to:

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: 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.

SPOT_SATSOLVER

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 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_STUTTER_CHECK

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 is 8.

SPOT_SIMULATION_REDUCTION

Choose which simulation based reduction to use: 1 force signature-based BDD implementation, 2 force matrix-based implementation and 0 is default, a heuristic is used to choose which implementation to use.

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.

SPOT_XCNF

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.

BIBLIOGRAPHY

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.

4.

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 SPOT_STUTTER_CHECK.

5.

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.

REPORTING BUGS

COPYRIGHT

SEE ALSO