823dc56e6b
* NEWS: Update. * doc/org/satmin.org: Update satmin page. * bin/man/spot-x.x: Document SPOT_XCNF and edit SPOT_SATSOLVER. * bin/spot-x.cc: Update satmin options. * bin/autfilt.cc: Update satmin related documentations. * bin/man/autfilt.x: Update autfilt options.
108 lines
3.9 KiB
Text
108 lines
3.9 KiB
Text
.\" -*- coding: utf-8 -*-
|
|
[NAME]
|
|
autfilt \- filter, convert, and transform omega-automata
|
|
[DESCRIPTION]
|
|
.\" Add any additional description here
|
|
[OPTIONS FOR SAT\-MINIMIZATION]
|
|
.TP
|
|
\fB\fP
|
|
By default, SAT\-based minimization executes 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
|
|
\fBacc=DOUBLEQUOTEDSTRING\fP
|
|
DOUBLEQUOTEDSTRING is an acceptance formula in the HOA syntax, or a
|
|
parametrized acceptance name (the different acc\-name: options from HOA).
|
|
|
|
.TP
|
|
\fBcolored\fP
|
|
force all transitions (or all states if \fB\-S\fR is used) to belong to exactly
|
|
one acceptance condition.
|
|
|
|
.TP
|
|
\fBmax\-states=M\fP
|
|
M is an upper-bound on the maximum number of states of the constructed
|
|
automaton.
|
|
|
|
.TP
|
|
\fBsat\-incr=M\fP
|
|
use an incremental approach for SAT-based minimization algorithm. M can be
|
|
either \fB1\fR or \fB2\fR. They correspond respectively to
|
|
\fB\-x sat\-minimize=2\fR and \fB\-x sat\-minimize=3\fR options. They restart
|
|
the encoding only after (N\-1)\-\fBsat\-incr\-steps\fR states have been won.
|
|
Each iterations of both starts by encoding the research of an N\-1 automaton,
|
|
N being the size of the starting automaton. \fB1\fR uses Picosat assumptions.
|
|
It additionally assumes that the last \fBsat-incr-steps\fR states are
|
|
unnecessary. On failure, it 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. \fB2\fR, as for it, after an N-1 state automaton has been found, uses
|
|
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 occurs after \fBsat\-incr\-steps\fR iterations unless
|
|
\fBsat\-incr\-steps=\-1\fR (see SPOT_XCNF environment variable described in
|
|
spot\-x). It defaults to 2.
|
|
|
|
.TP
|
|
\fBsat\-incr\-steps=M\fP
|
|
set the value of \fBsat\-incr\-steps\fR to M. This is used by \fBsat\-incr\fR
|
|
option.
|
|
|
|
.TP
|
|
\fBsat-naive\fP
|
|
use the naive algorithm to find a smaller automaton. It starts from N (N being
|
|
the size of the starting automaton) and then checks N\-1, N\-2, etc. until the
|
|
last successful check.
|
|
|
|
.TP
|
|
\fBsat-langmap\fP
|
|
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 states.
|
|
|
|
.TP
|
|
\fBstates=M\fP
|
|
M is a fixed number of states to use in the result (all the states needs
|
|
not be accessible in the result. Therefore, the output might be smaller
|
|
nonetheless). The SAT\-based procedure is just used once to synthesize
|
|
one automaton, and no further minimization is attempted.
|
|
|
|
[BIBLIOGRAPHY]
|
|
The following papers are related to some of the transformations implemented
|
|
in autfilt.
|
|
|
|
.TP
|
|
\(bu
|
|
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud:
|
|
Strength-based decomposition of the property Büchi automaton for faster
|
|
model checking. Proceedings of TACAS'13. LNCS 7795.
|
|
|
|
The \fB\-\-strength\-decompose\fR option implements the definitions
|
|
given in the above paper.
|
|
.TP
|
|
\(bu
|
|
František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, and Jan Strejček:
|
|
On refinement of Büchi automata for explicit model checking.
|
|
Proceedings of SPIN'15. LNCS 9232.
|
|
|
|
That paper gives the motivation for options \fB\-\-exclusive\-ap\fR
|
|
and \fB\-\-simplify\-exclusive\-ap\fR.
|
|
.TP
|
|
\(bu
|
|
Thibaud Michaud and Alexandre Duret-Lutz:
|
|
Practical stutter-invariance checks for ω-regular languages.
|
|
Proceedings of SPIN'15. LNCS 9232.
|
|
|
|
Describes the algorithms used by the \fB\-\-destut\fR and
|
|
\fB\-\-instut\fR options. These options correpond respectively to
|
|
cl() and sl() in the paper.
|
|
.TP
|
|
\(bu
|
|
Souheib Baarir and Alexandre Duret-Lutz: SAT-based minimization of
|
|
deterministic ω-automata. Proceedings of LPAR'15 (a.k.a LPAR-20).
|
|
LNCS 9450.
|
|
|
|
Describes the \fB\-\-sat\-minimize\fR option.
|
|
[SEE ALSO]
|
|
.BR spot-x (7)
|
|
.BR dstar2tgba (1)
|