alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

improve documentation for -x sat-minimize

Browse source 
* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization.  It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
This commit is contained in:
Alexandre Duret-Lutz 2021-04-19 16:46:30 +02:00
parent caca8728fe
commit 6253885af7
3 changed files with 22 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

12
bin/man/spot-x.x
View file

@ -10,11 +10,17 @@ spot-x \- Common fine-tuning options and environment variables.
.\" Add any additional description here
[SAT\-MINIMIZE VALUES]
When the sat-minimize=K option is used to enable SAT-based
minimization of deterministic automata, a SAT solver is
used to minimize an input automaton with N states into an
output automaton with 1≤M≤N states. The parameter K specifies
how the smallest possible M should be searched.
.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.
The default, \fB1\fR, performs a binary search between 1 and N. The
lower bound can sometimes be improved when the \fBsat-langmap\fR
option is used.
.TP
\fB2\fR

23
bin/spot-x.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -160,11 +160,12 @@ that are weak and deterministic. The default is 1 in --high mode, else 2 in \
if the TGBA is not already deterministic. Doing so will degeneralize \
the automaton. This is disabled by default, unless sat-minimize is set.") },
{ DOC("sat-minimize",
"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 \
"Set to a value between 1 and 4 to enable SAT-based minimization \
of deterministic ω-automata. If the input has n states, a SAT solver is \
used to find an equivalent automaton with 1≤m<n states. The value between \
1 and 4 selects how the lowest possible m is searched, see the SAT-MINIMIZE \
VALUE section. 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.") },
{ DOC("sat-incr-steps", "Set the value of sat-incr-steps. This variable \
@ -176,8 +177,8 @@ is at least equal to the total number of different languages recognized by \
the automaton's states.") },
{ DOC("sat-states",
"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 \
minimization will attempt to construct an automaton with the given number of \
states. It may however return an automaton with fewer 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 \
@ -185,13 +186,13 @@ automaton is returned.") },
{ DOC("sat-acc",
"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 \
states. It may however return an automaton with fewer acceptance sets if \
some of these are useless. Setting sat-acc automatically \
sets sat-minimize to 1 if not set differently.") },
{ DOC("state-based",
"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.") },
an automaton where all outgoing transition of a state have the same acceptance \
sets. By default this is only enabled when options -B or -S are used.") },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};

2
spot/twaalgos/postproc.cc
View file

@ -534,7 +534,7 @@ namespace spot
else if (sat_acc_ != -1)
target_acc = sat_acc_;
else
// Take the number of acceptance conditions from the input
// Take the number of acceptance sets from the input
// automaton, not from dba, because dba often has been
// degeneralized by tba_determinize_check(). Make sure it
// is at least 1.