From cfa3417449eb838f51e5b3d311c44471a2899e4c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 19 Apr 2021 16:46:30 +0200
Subject: [PATCH] improve documentation for -x sat-minimize

* 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.
---
 bin/man/spot-x.x          | 12 +++++++++---
 bin/spot-x.cc             | 23 ++++++++++++-----------
 spot/twaalgos/postproc.cc |  2 +-
 3 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x
index 51ea95edf..b961a8ba3 100644
--- a/bin/man/spot-x.x
+++ b/bin/man/spot-x.x
@@ -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
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index b6b0d57c9..9c310d100 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -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.
@@ -179,11 +179,12 @@ or when det-max-states is set.") },
 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 \
@@ -195,8 +196,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 \
@@ -204,13 +205,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.") },
     { DOC("simul-method",
           "Chose which simulation based reduction to use: 1 force the \
 signature-based BDD implementation, 2 force matrix-based and 0, the default, \
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index dcd27a68b..962a79ebf 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -581,7 +581,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.