Commit d9f3ca71 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

dtbasat: implement dba_sat_minimize()

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add option -RS.
parent 3fd49da1
......@@ -37,6 +37,7 @@ tgbaalgos_HEADERS = \
degen.hh \
dottydec.hh \
dotty.hh \
dtbasat.hh \
dupexp.hh \
eltl2tgba_lacim.hh \
emptiness.hh \
......@@ -84,6 +85,7 @@ libtgbaalgos_la_SOURCES = \
degen.cc \
dotty.cc \
dottydec.cc \
dtbasat.cc \
dupexp.cc \
eltl2tgba_lacim.cc \
emptiness.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include <fstream>
#include <sstream>
#include "dtbasat.hh"
#include "reachiter.hh"
#include <map>
#include <utility>
#include "scc.hh"
#include "tgba/bddprint.hh"
#include "ltlast/constant.hh"
#include "stats.hh"
#include "misc/tmpfile.hh"
// If the following DEBUG macro is set to 1, the temporary files used
// to communicate with the SAT-solver will be left in the current
// directory. (The files dtba-sat.cnf and dtba-sat.out contain the
// input and output for the last successful minimization attempted, or
// for the only failed attempt if the minimization failed.)
//
// Additionally, the CNF file will be output with a comment before
// each clause, and an additional output file (dtba-sat.dbg) will be
// created with a list of all positive variables in the result and
// their meaning.
//
// Note that the code use unique temporary filenames, so it is safe to
// run several such minimizations in parallel. It only when DEBUG=1
// that some of these files will be renamed to the above hard-coded
// names, possibly causing confusion if multiple minimizations are
// debugged in parallel and in the same directory.
#define DEBUG 0
#if DEBUG
#define dout out << "c "
#else
#define dout while (0) out
#endif
namespace spot
{
namespace
{
static bdd_dict* debug_dict = 0;
struct transition
{
int src;
bdd cond;
int dst;
transition(int src, bdd cond, int dst)
: src(src), cond(cond), dst(dst)
{
}
bool operator<(const transition& other) const
{
if (this->src < other.src)
return true;
if (this->src > other.src)
return false;
if (this->dst < other.dst)
return true;
if (this->dst > other.dst)
return false;
return this->cond.id() < other.cond.id();
}
bool operator==(const transition& other) const
{
return (this->src == other.src
&& this->dst == other.dst
&& this->cond.id() == other.cond.id());
}
};
struct state_pair
{
int a;
int b;
state_pair(int a, int b)
: a(a), b(b)
{
}
bool operator<(const state_pair& other) const
{
if (this->a < other.a)
return true;
if (this->a > other.a)
return false;
if (this->b < other.b)
return true;
if (this->b > other.b)
return false;
return false;
}
};
struct path
{
int src_cand;
int src_ref;
int dst_cand;
int dst_ref;
path(int src_cand, int src_ref,
int dst_cand, int dst_ref)
: src_cand(src_cand), src_ref(src_ref),
dst_cand(dst_cand), dst_ref(dst_ref)
{
}
bool operator<(const path& other) const
{
if (this->src_cand < other.src_cand)
return true;
if (this->src_cand > other.src_cand)
return false;
if (this->src_ref < other.src_ref)
return true;
if (this->src_ref > other.src_ref)
return false;
if (this->dst_cand < other.dst_cand)
return true;
if (this->dst_cand > other.dst_cand)
return false;
if (this->dst_ref < other.dst_ref)
return true;
if (this->dst_ref > other.dst_ref)
return false;
return false;
}
};
std::ostream& operator<<(std::ostream& os, const state_pair& p)
{
os << "<" << p.a << "," << p.b << ">";
return os;
}
std::ostream& operator<<(std::ostream& os, const transition& t)
{
os << "<" << t.src << ","
<< bdd_format_formula(debug_dict, t.cond)
<< "," << t.dst << ">";
return os;
}
std::ostream& operator<<(std::ostream& os, const path& p)
{
os << "<"
<< p.src_cand << ","
<< p.src_ref << ","
<< p.dst_cand << ","
<< p.dst_ref << ">";
return os;
}
struct dict
{
typedef std::map<transition, int> trans_map;
trans_map transid;
trans_map transacc;
typedef std::map<int, transition> rev_map;
rev_map revtransid;
rev_map revtransacc;
std::map<state_pair, int> prodid;
std::map<path, int> pathid_ref;
std::map<path, int> pathid_cand;
int nvars;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> state_map;
typedef Sgi::hash_map<int, const state*> int_map;
state_map state_to_int;
int_map int_to_state;
int cand_size;
~dict()
{
state_map::const_iterator s = state_to_int.begin();
while (s != state_to_int.end())
// Always advance the iterator before deleting the key.
s++->first->destroy();
}
};
class filler_dfs: public tgba_reachable_iterator_depth_first
{
protected:
dict& d;
int size_;
bdd ap_;
public:
filler_dfs(const tgba* aut, dict& d, bdd ap)
:tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap)
{
d.nvars = 0;
}
int size()
{
return size_;
}
void end()
{
size_ = seen.size();
if (d.cand_size == -1)
d.cand_size = size_ - 1;
int seen_size = seen.size();
for (int i = 1; i <= seen_size; ++i)
{
for (int j = 1; j <= d.cand_size; ++j)
{
d.prodid[state_pair(j, i)] = ++d.nvars;
for (int k = 1; k <= seen_size; ++k)
for (int l = 1; l <= d.cand_size; ++l)
{
path p(j, i, l, k);
d.pathid_ref[p] = ++d.nvars;
d.pathid_cand[p] = ++d.nvars;
}
}
}
for (dict::state_map::const_iterator i = seen.begin();
i != seen.end(); ++i)
{
d.int_to_state[i->second] = i->first;
}
std::swap(d.state_to_int, seen);
for (int i = 1; i <= d.cand_size; ++i)
for (int j = 1; j <= d.cand_size; ++j)
{
bdd all = bddtrue;
while (all != bddfalse)
{
bdd one = bdd_satoneset(all, ap_, bddfalse);
all -= one;
transition t(i, one, j);
d.transid[t] = ++d.nvars;
d.revtransid.insert(dict::rev_map::value_type(d.nvars, t));
d.transacc[t] = ++d.nvars;
d.revtransacc.insert(dict::rev_map::value_type(d.nvars, t));
}
}
}
};
static
void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d)
{
int nclauses = 0;
int ref_size = 0;
scc_map sm(ref);
sm.build_map();
bdd ap = sm.aprec_set_of(sm.initial());
// Number all the SAT variable we may need.
{
filler_dfs f(ref, d, ap);
f.run();
ref_size = f.size();
}
// empty automaton is impossible
if (d.cand_size == 0)
{
out << "p cnf 1 2\n-1 0\n1 0\n";
return;
}
// An empty line for the header
out << " \n";
#if DEBUG
debug_dict = ref->get_dict();
#endif
dout << "(1) the candidate automaton is complete\n";
for (int q1 = 1; q1 <= d.cand_size; ++q1)
{
bdd all = bddtrue;
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
#if DEBUG
dout;
for (int q2 = 1; q2 <= d.cand_size; q2++)
{
transition t(q1, s, q2);
out << t << "δ";
if (q2 != d.cand_size)
out << " ∨ ";
}
out << "\n";
#endif
for (int q2 = 1; q2 <= d.cand_size; q2++)
{
transition t(q1, s, q2);
int ti = d.transid[t];
out << ti << " ";
}
out << "0\n";
++nclauses;
}
}
dout << "(2) the initial state is reachable\n";
dout << state_pair(1, 1) << "\n";
out << d.prodid[state_pair(1, 1)] << " 0\n";
++nclauses;
for (std::map<state_pair, int>::const_iterator pit = d.prodid.begin();
pit != d.prodid.end(); ++pit)
{
int q1 = pit->first.a;
int q1p = pit->first.b;
dout << "(2) states Cand[" << q1 << "] and Ref[" << q1p
<< "] are 0-length paths\n";
path p(q1, q1p, q1, q1p);
dout << pit->first << " → (" << p << "R ∧ " << p << "C)\n";
out << -pit->second << " " << d.pathid_ref[p] <<" 0\n";
out << -pit->second << " " << d.pathid_cand[p] <<" 0\n";
nclauses += 2;
dout << "(3) augmenting paths based on Cand[" << q1
<< "] and Ref[" << q1p << "]\n";
tgba_succ_iterator* it = ref->succ_iter(d.int_to_state[q1p]);
for (it->first(); !it->done(); it->next())
{
const state* dps = it->current_state();
int dp = d.state_to_int[dps];
dps->destroy();
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
for (int q2 = 1; q2 <= d.cand_size; q2++)
{
transition t(q1, s, q2);
int ti = d.transid[t];
state_pair p2(q2, dp);
int succ = d.prodid[p2];
dout << pit->first << " ∧ " << t << "δ → " << p2 << "\n";
out << -pit->second << " " << -ti << " "
<< succ << " 0\n";
++nclauses;
}
}
}
delete it;
}
bdd all_acc = ref->all_acceptance_conditions();
// construction of contraints (4,5) : all loops in the product
// where no accepting run is detected in the ref. automaton,
// must also be marked as not accepting in the cand. automaton
for (int q1 = 1; q1 <= d.cand_size; ++q1)
for (int q1p = 1; q1p <= ref_size; ++q1p)
{
for (int q2 = 1; q2 <= d.cand_size; ++q2)
for (int q2p = 1; q2p <= ref_size; ++q2p)
{
path p1(q1, q1p, q2, q2p);
dout << "(4&5) matching paths from reference based on "
<< p1 << "\n";
int pid1 = d.pathid_ref[p1];
tgba_succ_iterator* it = ref->succ_iter(d.int_to_state[q2p]);
for (it->first(); !it->done(); it->next())
{
const state* dps = it->current_state();
int dp = d.state_to_int[dps];
dps->destroy();
if (it->current_acceptance_conditions() == all_acc)
continue;
for (int q3 = 1; q3 <= d.cand_size; ++q3)
{
if (dp == q1p && q3 == q1) // (4) looping
{
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
transition t(q2, s, q1);
int ti = d.transid[t];
int ta = d.transacc[t];
dout << p1 << "R ∧ " << t << "δ → ¬" << t
<< "F\n";
out << -pid1 << " " << -ti << " "
<< -ta << " 0\n";
++nclauses;
}
}
else // (5) not looping
{
path p2 = path(q1, q1p, q3, dp);
int pid2 = d.pathid_ref[p2];
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
transition t(q2, s, q3);
int ti = d.transid[t];
dout << p1 << "R ∧ " << t << "δ → " << p2
<< "R\n";
out << -pid1 << " " << -ti << " "
<< pid2 << " 0\n";
++nclauses;
}
}
}
}
delete it;
}
}
// construction of contraints (6,7): all loops in the product
// where accepting run is detected in the ref. automaton, must
// also be marked as accepting in the candidate.
for (int q1 = 1; q1 <= d.cand_size; ++q1)
for (int q1p = 1; q1p <= ref_size; ++q1p)
{
for (int q2 = 1; q2 <= d.cand_size; ++q2)
for (int q2p = 1; q2p <= ref_size; ++q2p)
{
path p1(q1, q1p, q2, q2p);
dout << "(6&7) matching paths from candidate based on "
<< p1 << "\n";
int pid1 = d.pathid_cand[p1];
tgba_succ_iterator* it = ref->succ_iter(d.int_to_state[q2p]);
for (it->first(); !it->done(); it->next())
{
const state* dps = it->current_state();
int dp = d.state_to_int[dps];
dps->destroy();
for (int q3 = 1; q3 <= d.cand_size; q3++)
{
if (dp == q1p && q3 == q1) // (6) looping
{
// We only care about the looping case if
// it is accepting in the reference.
if (it->current_acceptance_conditions()
!= all_acc)
continue;
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
transition t(q2, s, q1);
int ti = d.transid[t];
int ta = d.transacc[t];
dout << p1 << "C ∧ " << t << "δ → " << t
<< "F\n";
out << -pid1 << " " << -ti << " " << ta
<< " 0\n";
++nclauses;
}
}
else // (7) no loop
{
path p2 = path(q1, q1p, q3, dp);
int pid2 = d.pathid_cand[p2];
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
transition t(q2, s, q3);
int ti = d.transid[t];
int ta = d.transacc[t];
dout << p1 << "C ∧ " << t << "δ ∧ ¬"
<< t << "F → " << p2 << "C\n";
out << -pid1 << " " << -ti << " "
<< ta << " " << pid2 << " 0\n";
++nclauses;
}
}
}
}
delete it;
}
}
out.seekp(0);
out << "p cnf " << d.nvars << " " << nclauses;
}
static std::string
get_solution(const char* filename)
{
std::fstream in(filename, std::ios_base::in);
std::string line;
while (std::getline(in, line))
{
if (line.empty() || line[0] == 'c')
continue;
if (line[0] == 'v')
break;
}
if (line[0] == 'v')
return line.c_str() + 1;
return "";
}
static tgba_explicit_number*
sat_build(const std::string& solution, dict& satdict, const tgba* aut)
{
bdd_dict* autdict = aut->get_dict();
tgba_explicit_number* a = new tgba_explicit_number(autdict);
autdict->register_all_variables_of(aut, a);
const ltl::formula* t = ltl::constant::true_instance();
bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a));
a->set_acceptance_conditions(acc);
for (int s = 1; s < satdict.cand_size; ++s)
a->add_state(s);
std::stringstream sol(solution);
state_explicit_number::transition* last_aut_trans = 0;
const transition* last_sat_trans = 0;
#if DEBUG
std::fstream out("dtba-sat.dbg",
std::ios_base::trunc | std::ios_base::out);
std::set<int> positive;
#else
// "out" is not used, but it has to exist for the dout() macro to
// compile.
std::ostream& out(std::cout);
#endif