Commit fdb157bf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

satmin: cleanup interfaces and minimization loops

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
(dtba_sat_minimize): Split into...
(dtba_sat_synthetize, dtba_sat_minimize): These.
(dtba_sat_minimize_dichotomy): New function.
* src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh
(dtgba_sat_minimize, dtgba_sat_synthetize): Likewise.
* src/tgbatest/ltl2tgba.cc: Adjust to new interface.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
Cleanup option processing for SAT options.
* src/tgbatest/satmin.test: Adjust.
* src/bin/spot-x.cc, src/bin/man/spot-x.x, NEWS: Document.
parent b09ef5be
......@@ -58,6 +58,14 @@ New in spot 1.1.4a (not relased)
number of seconds spent building the output automaton (excluding
the time spent parsing the input).
- ltl2tgba and dstar2tgba can use a SAT-solver to minimize
deterministic automata. Doing so is only needed on properties
that are stronger than obligations (for which our
WDBA-minimization procedure will return a minimimal
deterministic automaton more efficiently) and is disabled by
default. See the spot-x(7) man page for documentation about the
related options: sat-minimize, sat-states, sat-acc, state-based.
* All the parsers implemented in Spot now use the same type
to store locations.
......
[NAME]
spot-x \- Common fine-tuning options.
[SYNOPSIS]
.B \-\-extra-options STRING
.br
.B \-x STRING
[DESCRIPTION]
.\" Add any additional description here
[ENVIRONMENT VARIABLES]
.TP
\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 %I >%O"\fR. 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).
.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.
[BIBLIOGRAPHY]
.TP
1.
......@@ -13,7 +41,10 @@ Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the
Powerset Construction for Restricted Classes of
ω-Automata. Proceedings of ATVA'07. LNCS 4762.
Describes the WDBA-minimization algorithm implemented in Spot.
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.
.TP
2.
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
......@@ -23,6 +54,14 @@ Improvements to LTL Translation. Proceedings of SPIN'13. LNCS 7976.
Describes the compositional suspension, the simulation-based
reductions, and the SCC-based simplifications.
.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.
[SEE ALSO]
.BR ltl2tgba (1)
.BR ltl2tgta (1)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
......@@ -92,6 +93,37 @@ simulation. Set to 3 to iterate both direct and reverse simulations. \
The default is 3 in --high mode, and 0 otherwise.") },
{ DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \
Enabled by default.") },
{ DOC("tba-det", "Set to 1 to attempt a powerset determinization \
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 to 1 to enable SAT-based minimization of deterministic \
TGBA: it starts with the number of states of the input, and iteratively \
tries to find a deterministic TGBA with one less state. Set to 2 to perform \
a binary search instead. Disabled (0) by default. The sat solver to use \
can be set with the SPOT_SATSOLVER environment variable (see below). By \
default the procedure looks for a TGBA with the same number of acceptance \
set; this can be changed with the sat-acc option, or of course by using -B \
to construct a Büchi automaton. Enabling SAT-based minimization will \
also enable tba-det.") },
{ 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 \
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 \
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 \
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.") },
{ 0, 0, 0, 0, 0, 0 }
};
......
......@@ -51,8 +51,10 @@
#define DEBUG 0
#if DEBUG
#define dout out << "c "
#define trace std::cerr
#else
#define dout while (0) out
#define dout while (0) std::cout
#define trace dout
#endif
namespace spot
......@@ -317,8 +319,32 @@ namespace spot
#if DEBUG
debug_dict = ref->get_dict();
dout << "ref_size: " << ref_size << "\n";
dout << "cand_size: " << d.cand_size << "\n";
#endif
// dout << "symmetry-breaking clauses\n";
// int k = 1;
// bdd all = bddtrue;
// while (all != bddfalse)
// {
// bdd s = bdd_satoneset(all, ap, bddfalse);
// all -= s;
// for (int q1 = 1; q1 < d.cand_size; ++q1)
// for (int q2 = q1 + 2; q2 <= d.cand_size; ++q2)
// if ((q1 - 1) * d.cand_size + q2 + 2 <= k)
// {
// transition t(q1, s, q2);
// int ti = d.transid[t];
// dout << "¬" << t << "\n";
// out << -ti << " 0\n";
// ++nclauses;
// }
// ++k;
// }
// if (!nclauses)
// dout << "(none)\n";
dout << "(1) the candidate automaton is complete\n";
for (int q1 = 1; q1 <= d.cand_size; ++q1)
{
......@@ -712,86 +738,89 @@ namespace spot
}
tgba_explicit_number*
dtba_sat_minimize(const tgba* a, int target_state_number,
bool state_based)
dtba_sat_synthetize(const tgba* a, int target_state_number,
bool state_based)
{
int ref_states =
target_state_number == -1
? stats_reachable(a).states - 1
: target_state_number;
std::string current_solution;
std::string last_solution;
dict* last = 0;
trace << "dtba_sat_synthetize(..., states = " << target_state_number
<< ", state_based = " << state_based << ")\n";
std::string solution;
dict* current = 0;
temporary_file* cnf = 0;
temporary_file* out = 0;
do
{
if (DEBUG && current)
{
xrename(out->name(), "dtba-sat.out");
xrename(cnf->name(), "dtba-sat.cnf");
}
delete out;
delete cnf;
std::swap(current_solution, last_solution);
delete last;
last = current;
current = new dict;
current->cand_size = ref_states--;
cnf = create_tmpfile("dtba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
out = create_tmpfile("dtba-sat-", ".out");
satsolver(cnf, out);
current_solution = get_solution(out->name());
}
while (target_state_number == -1 && !current_solution.empty());
current = new dict;
current->cand_size = target_state_number;
cnf = create_tmpfile("dtba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
out = create_tmpfile("dtba-sat-", ".out");
satsolver(cnf, out);
solution = get_solution(out->name());
tgba_explicit_number* res = 0;
if (!solution.empty())
res = sat_build(solution, *current, a, state_based);
delete current;
if (target_state_number != -1)
if (DEBUG)
{
std::swap(current_solution, last_solution);
if (last_solution.empty())
{
last = 0;
delete current;
}
else
{
last = current;
}
xrename(out->name(), "dtba-sat.out");
xrename(cnf->name(), "dtba-sat.cnf");
}
else
delete out;
delete cnf;
trace << "dtba_sat_synthetize(...) = " << res << "\n";
return res;
}
tgba_explicit_number*
dtba_sat_minimize(const tgba* a, bool state_based)
{
int n_states = stats_reachable(a).states;
tgba_explicit_number* prev = 0;
for (;;)
{
delete current;
tgba_explicit_number* next =
dtba_sat_synthetize(prev ? prev : a, --n_states, state_based);
if (next == 0)
break;
delete prev;
prev = next;
}
return prev;
}
tgba_explicit_number* res;
if (last == 0)
tgba_explicit_number*
dtba_sat_minimize_dichotomy(const tgba* a, bool state_based)
{
int max_states = stats_reachable(a).states - 1;
int min_states = 1;
tgba_explicit_number* prev = 0;
while (min_states <= max_states)
{
res = 0;
if (DEBUG)
int target = (max_states + min_states) / 2;
tgba_explicit_number* next =
dtba_sat_synthetize(prev ? prev : a, target, state_based);
if (next == 0)
{
xrename(out->name(), "dtba-sat.out");
xrename(cnf->name(), "dtba-sat.cnf");
min_states = target + 1;
}
else
{
delete prev;
prev = next;
max_states = target - 1;
}
}
else
{
res = sat_build(last_solution, *last, a, state_based);
delete last;
}
delete out;
delete cnf;
return res;
return prev;
}
}
......@@ -20,32 +20,47 @@
#ifndef SPOT_TGBAALGOS_DTBASAT_HH
# define SPOT_TGBAALGOS_DTBASAT_HH
#include <iosfwd>
#include "tgba/tgba.hh"
#include "tgba/tgbaexplicit.hh"
namespace spot
{
/// \brief Attempt to reduce a deterministic TBA with a SAT solver.
/// \brief Attempt to synthetize an equivalent deterministic TBA
/// with a SAT solver.
///
/// \param a the TGBA to reduce. It should have only one acceptance
/// set and be deterministic. I.e., it should be a deterministic TBA.
/// \param a the input TGBA. It should have only one acceptance
/// set and be deterministic. I.e., it should be a deterministic TBA.
///
/// \param target_state_number the expected number of states wanted
/// in the resulting automaton. If \a target_state_number is left
/// to its default value of -1, this function will attempt to build
/// the smallest possible deterministic TBA is can produce.
/// \param target_state_number the desired number of states wanted
/// in the resulting automaton. The result may have less than \a
/// target_state_number reachable states.
///
/// \param state_based set to true to force all outgoing transitions
/// of a state to share the same acceptance condition, effectively
/// turning the TBA into a BA.
///
/// If no automaton with \a target_state_number states is found, or
/// (in case <code>target_state_number == -1</code>) if no smaller
/// automaton is found, then a null pointer is returned.
/// If no equivalent deterministic TBA with \a target_state_number
/// states is found, a null pointer
SPOT_API tgba_explicit_number*
dtba_sat_minimize(const tgba* a, int target_state_number = -1,
bool state_based = false);
dtba_sat_synthetize(const tgba* a, int target_state_number,
bool state_based = false);
/// \brief Attempt to minimize a deterministic TBA with a SAT solver.
///
/// This calls dtba_sat_synthetize() in a loop, with a decreasing
/// number of states, and returns the last successfully built TBA.
///
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API tgba_explicit_number*
dtba_sat_minimize(const tgba* a, bool state_based = false);
/// \brief Attempt to minimize a deterministic TBA with a SAT solver.
///
/// This calls dtba_sat_synthetize() in a loop, but attempting to
/// find the minimum number of states using a binary search.
//
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API tgba_explicit_number*
dtba_sat_minimize_dichotomy(const tgba* a, bool state_based = false);
}
#endif // SPOT_TGBAALGOS_DTBASAT_HH
......@@ -52,16 +52,16 @@
#define DEBUG 0
#if DEBUG
#define dout out << "c "
#define trace std::cerr
#else
#define dout while (0) out
#define dout while (0) std::cout
#define trace dout
#endif
namespace spot
{
namespace
{
static bdd_dict* debug_dict = 0;
struct transition
......@@ -477,9 +477,6 @@ namespace spot
sm.build_map();
bdd ap = sm.aprec_set_of(sm.initial());
#if DEBUG
debug_dict = ref->get_dict();
#endif
// Number all the SAT variable we may need.
{
......@@ -488,6 +485,12 @@ namespace spot
ref_size = f.size();
}
#if DEBUG
debug_dict = ref->get_dict();
dout << "ref_size: " << ref_size << "\n";
dout << "cand_size: " << d.cand_size << "\n";
#endif
// empty automaton is impossible
if (d.cand_size == 0)
{
......@@ -937,87 +940,96 @@ namespace spot
}
tgba_explicit_number*
dtgba_sat_minimize(const tgba* a, unsigned cand_nacc,
int target_state_number, bool state_based)
dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number,
int target_state_number, bool state_based)
{
int ref_states =
target_state_number == -1
? stats_reachable(a).states - 1
: target_state_number;
std::string current_solution;
std::string last_solution;
dict* last = 0;
trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number
<< ", states = " << target_state_number
<< ", state_based = " << state_based << ")\n";
std::string solution;
dict* current = 0;
temporary_file* cnf = 0;
temporary_file* out = 0;
do
{
if (DEBUG && current)
{
xrename(out->name(), "dtgba-sat.out");
xrename(cnf->name(), "dtgba-sat.cnf");
}
delete out;
delete cnf;
std::swap(current_solution, last_solution);
delete last;
last = current;
current = new dict(a);
current->cand_size = ref_states--;
current->cand_nacc = cand_nacc;
cnf = create_tmpfile("dtgba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtgba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
out = create_tmpfile("dtgba-sat-", ".out");
satsolver(cnf, out);
current_solution = get_solution(out->name());
}
while (target_state_number == -1 && !current_solution.empty());
current = new dict(a);
current->cand_size = target_state_number;
current->cand_nacc = target_acc_number;
cnf = create_tmpfile("dtgba-sat-", ".cnf");
std::fstream cnfs(cnf->name(),
std::ios_base::trunc | std::ios_base::out);
dtgba_to_sat(cnfs, a, *current, state_based);
cnfs.close();
out = create_tmpfile("dtgba-sat-", ".out");
satsolver(cnf, out);
solution = get_solution(out->name());
tgba_explicit_number* res = 0;
if (!solution.empty())
res = sat_build(solution, *current, a, state_based);
delete current;
if (target_state_number != -1)
if (DEBUG)
{
std::swap(current_solution, last_solution);
if (last_solution.empty())
{
last = 0;
delete current;
}
else
{
last = current;
}
xrename(out->name(), "dtgba-sat.out");
xrename(cnf->name(), "dtgba-sat.cnf");
}
else
delete out;
delete cnf;
trace << "dtgba_sat_synthetize(...) = " << res << "\n";
return res;
}
tgba_explicit_number*
dtgba_sat_minimize(const tgba* a, unsigned target_acc_number,
bool state_based)
{
int n_states = stats_reachable(a).states;
tgba_explicit_number* prev = 0;
for (;;)
{
delete current;
tgba_explicit_number* next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
--n_states, state_based);
if (next == 0)
break;
delete prev;
prev = next;
}
return prev;
}
tgba_explicit_number*
dtgba_sat_minimize_dichotomy(const tgba* a, unsigned target_acc_number,
bool state_based)
{
int max_states = stats_reachable(a).states - 1;
int min_states = 1;
tgba_explicit_number* res;
if (last == 0)
tgba_explicit_number* prev = 0;
while (min_states <= max_states)
{
res = 0;
if (DEBUG)
int target = (max_states + min_states) / 2;
tgba_explicit_number* next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target,
state_based);
if (next == 0)
{
xrename(out->name(), "dtgba-sat.out");
xrename(cnf->name(), "dtgba-sat.cnf");
min_states = target + 1;
}
else
{
delete prev;
prev = next;
max_states = target - 1;
}
}
else
{
res = sat_build(last_solution, *last, a, state_based);
delete last;
}
delete out;
delete cnf;
return res;
return prev;
}
}
......@@ -20,36 +20,54 @@
#ifndef SPOT_TGBAALGOS_DTGBASAT_HH
# define SPOT_TGBAALGOS_DTGBASAT_HH
#include <iosfwd>
#include "tgba/tgba.hh"
#include "tgba/tgbaexplicit.hh"
namespace spot
{
/// \brief Attempt to reduce a deterministic TGBA with a SAT solver.
/// \brief Attempt to synthetize am equivalent deterministic TGBA
/// with a SAT solver.
///
/// \param a the TGBA to reduce. It should have only one acceptance
/// set and be deterministic. I.e., it should be a deterministic TBA.
/// \param a the input TGBA. It should be a deterministic TGBA.
///
/// \param cand_nacc is the number of acceptance sets in the result.
/// \param target_acc_number is the number of acceptance sets wanted
/// in the result.
///
/// \param target_state_number is the desired number of states in
/// the result. The output may have less than \a
/// target_state_number reachable states.
///
/// \param state_based set to true to force all outgoing transitions
/// of a state to share the same acceptance conditions, effectively
/// turning the TGBA into a TBA.
///
/// \param target_state_number the expected number of states wanted
/// in the resulting automaton. If \a target_state_number is left
/// to its default value of -1, this function will attempt to build
/// the smallest possible deterministic TGBA is can produce.
///
/// This functions attempts to find a TGBA with \a cand_nacc
/// This functions attempts to find a TGBA with \a target_acc_number
/// acceptance sets and target_state_number states that is
/// equivalent to \a a. If no such TGBA is found, a null pointer is
/// returned.
SPOT_API tgba_explicit_number*
dtgba_sat_minimize(const tgba* a, unsigned cand_nacc,
int target_state_number = -1,
dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number,
int target_state_number,
bool state_based = false);
/// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
///
/// This calls dtgba_sat_synthetize() in a loop, with a decreasing
/// number of states, and returns the last successfully built TGBA.
///
/// If no smaller TGBA exist, this returns a null pointer.
SPOT_API tgba_explicit_number*
dtgba_sat_minimize(const tgba* a, unsigned target_acc_number,
bool state_based = false);
/// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
///
/// This calls dtgba_sat_synthetize() in a loop, but attempting to