spot-x.x 8.11 KB
Newer Older
1
[NAME]
2
spot-x \- Common fine-tuning options and environment variables.
3

4
5
6
7
[SYNOPSIS]
.B \-\-extra-options STRING
.br
.B \-x STRING
8

9
10
[DESCRIPTION]
.\" Add any additional description here
11

12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
[SAT\-MINIMIZE VALUES]
.TP
\fB1\fR
Used by default, \fB1\fR 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 \fBsat-langmap\fR option is used.

.TP
\fB2\fR
Use PicoSAT assumptions. Each iteration encodes the search of an (N\-1) state
equivalent automaton, and additionally assumes that the last
\fBsat\-incr\-steps\fR states are unnecessary. On failure, relax the assumptions
to do a binary search between N\-1 and N\-1\-\fBsat\-incr\-steps\fR.
\fBsat\-incr\-steps\fR defaults to 6.

.TP
\fB3\fR
After an (N\-1) state automaton has been found, use incremental solving for
the next \fBsat\-incr\-steps\fR iterations by forbidding the usage of an
additional state without reencoding the problem again. A full encoding will
occur after \fBsat\-incr\-steps\fR iterations unless \fBsat\-incr\-steps=-1\fR
(see \fBSPOT_XCNF\fR environment variable). \fBsat\-incr\-steps\fR defaults to
2.

.TP
\fB4\fR
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.
40

41
[ENVIRONMENT VARIABLES]
42
43
44
45
46
47
48
49
50
51
52
53
54
.TP
\fBSPOT_DEFAULT_FORMAT\fR
Set to a value of \fBdot\fR or \fBhoa\fR to override the default
format used to output automata.  Up to Spot 1.9.6 the default output
format for automata used to be \fBdot\fR.  Starting with Spot 1.9.7,
the default output format switched to \fBhoa\fR as it is more
convenient when chaining tools in a pipe.  Set this variable to
\fBdot\fR to get the old behavior.  Additional options may be
passed to the printer by suffixing the output format with
\fB=\fR and the options.  For instance running
.in +4n
.nf
.ft C
55
% SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
56
57
58
59
60
61
62
63
64
65
66
67
.fi
.in -4n
is the same as running
.in +4n
.nf
.ft C
% autfilt --dot=bar ...
.fi
.in -4n
but the use of the environment variable makes more sense if you set
it up once for many commands.

68
69
70
71
72
.TP
\fBSPOT_DEBUG_PARSER\fR
If this variable is set to any value, the automaton parser of Spot is
executed in debug mode, showing how the input is processed.

73
74
75
.TP
\fBSPOT_DOTDEFAULT\fR
Whenever the \f(CW--dot\fR option is used without argument (even
76
77
implicitely via \fBSPOT_DEFAULT_FORMAT\fR), the contents of this
variable is used as default argument.  If you have some default
78
79
80
81
settings in \fBSPOT_DOTDEFAULT\fR and want to append to options
\f(CWxyz\fR temporarily for one call, use \f(CW--dot=.xyz\fR:
the dot character will be replaced by the contents of the
\f(CWSPOT_DOTDEFAULT\fR environment variable.
82

83
84
85
86
87
88
.TP
\fBSPOT_DOTEXTRA\fR
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.

89
90
91
92
93
94
95
96
97
98
99
100
.TP
\fBSPOT_SATLOG\fR
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.

101
.TP
102
\fBSPOT_SATSOLVER\fR
103
104
105
106
107
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: \f(CW"<sat_solver> [options] %I >%O"\fR.
The escape sequences \f(CW%I\fR and \f(CW%O\fR respectively
108
109
denote the names of the input and output files.  These temporary files
are created in the directory specified by \fBSPOT_TMPDIR\fR or
110
\fBTMPDIR\fR (see below). The SAT\-solver should follow the convention
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
of the SAT Competition for its input and output format.

.TP
\fBSPOT_STREETT_CONV_MIN\fR
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.
136

137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
.TP
\fBSPOT_STUTTER_CHECK\fR
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.
.RS
.IP 1
sl(a) x sl(!a)
.IP 2
sl(cl(a)) x !a
.IP 3
cl(sl(a)) x !a
.IP 4
sl2(a) x sl2(!a)
.IP 5
sl2(cl(a)) x !a
.IP 6
cl(sl2(a)) x !a
.IP 7
sl(a) x sl(!a), performed on-the-fly
.IP 8
cl(a) x cl(!a)
.RE

162
163
164
165
166
167
168
169
170
171
172
173
174
175
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
These variables control in which directory temporary files (e.g.,
those who contain the input and output when interfacing with
translators) are created.  \fBTMPDIR\fR is only read if
\fBSPOT_TMPDIR\fR does not exist.  If none of these environment
variables exist, or if their value is empty, files are created in the
current directory.

.TP
\fBSPOT_TMPKEEP\fR
When this variable is defined, temporary files are not removed.
This is mostly useful for debugging.

176
177
178
179
180
181
182
183
184
185
186
.TP
\fBSPOT_XCNF\fR
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 \fBSPOT_SATSOLVER\fR 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.

187
188
189
190
191
192
193
[BIBLIOGRAPHY]
.TP
1.
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the
Powerset Construction for Restricted Classes of
ω-Automata. Proceedings of ATVA'07.  LNCS 4762.

194
195
196
197
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.

198
199
200
201
.TP
2.
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
Jan Strejček: Compositional Approach to Suspension and Other
202
Improvements to LTL Translation.  Proceedings of SPIN'13.  LNCS 7976.
203
204
205
206

Describes the compositional suspension, the simulation-based
reductions, and the SCC-based simplifications.

207
208
209
210
211
212
213
214
.TP
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.

215
216
217
218
219
220
221
222
223
.TP
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
\fBSPOT_STUTTER_CHECK\fR.


224
225
[SEE ALSO]
.BR ltl2tgba (1)
226
.BR ltl2tgta (1)
227
.BR dstar2tgba (1)
228
.BR autfilt (1)