spot-x.x 4.76 KB
Newer Older
1
2
[NAME]
spot-x \- Common fine-tuning options.
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

[ENVIRONMENT VARIABLES]

14
15
16
17
18
19
20
21
22
.TP
\fBSPOT_DOTDEFAULT\fR
Whenever the \f(CW--dot\fR option is used without argument (even
implicitely), the contents of this variable is used as default
argument.  If you have some default setting in \fBSPOT_DOTDEFAULT\fR
but want to alter them temporarily for one call, use
\f(CW--dot=.yyy\fR: the dot character will be replaced by the contents
of the \f(CWSPOT_DOTDEFAULT\fR environment variable.

23
24
25
26
27
28
.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.

29
30
31
32
33
34
35
36
37
38
39
40
.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.

41
.TP
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
\fBSPOT_SATSOLVER\fR
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 \f(CW"glucose -verb=0 -model %I >%O"\fR, it is correct for
glucose version 3.0 (for older versions, remove the \fCW(-model\fR
option).  The escape sequences \f(CW%I\fR and \f(CW%O\fR respectively
denote the names of the input and output files.  These temporary files
are created in the directory specified by \fBSPOT_TMPDIR\fR or
\fBTMPDIR\fR (see below).  The SAT-solver should follow the convention
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.
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90

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

91
92
93
94
95
96
97
[BIBLIOGRAPHY]
.TP
1.
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the
Powerset Construction for Restricted Classes of
ω-Automata. Proceedings of ATVA'07.  LNCS 4762.

98
99
100
101
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.

102
103
104
105
.TP
2.
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
Jan Strejček: Compositional Approach to Suspension and Other
106
Improvements to LTL Translation.  Proceedings of SPIN'13.  LNCS 7976.
107
108
109
110

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

111
112
113
114
115
116
117
118
.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.

119
120
[SEE ALSO]
.BR ltl2tgba (1)
121
.BR ltl2tgta (1)
122
.BR dstar2tgba (1)
123
.BR autfilt (1)