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

Revert "* src/tgbaalgos/dtbasat.cc: Better encoding for weak SCCs."

Browse source 
This was simply wrong.

* src/tgbaalgos/dtbasat.cc: reverts commit
fc5a00d24d5964d6f6a48d362ecbdec357eaf154.
This commit is contained in:
Alexandre Duret-Lutz 2013-12-17 15:58:54 +01:00
parent b4d0b9ee42
commit 7a26a4f1ec
1 changed files with 68 additions and 209 deletions
Download patch file Download diff file Expand all files Collapse all files

159
src/tgbaalgos/dtbasat.cc
View file

@ -25,7 +25,6 @@
#include <map>
#include <utility>
#include "scc.hh"
#include "isweakscc.hh"
#include "tgba/bddprint.hh"
#include "ltlast/constant.hh"
#include "stats.hh"
@ -206,10 +205,8 @@ namespace spot
typedef std::map<int, transition> rev_map;
rev_map revtransid;
rev_map revtransacc;
std::set<int> weak_scc;
std::map<state_pair, int> prodid;
std::map<state_pair, int> pathcand;
std::map<path, int> pathid_ref;
std::map<path, int> pathid_cand;
int nvars;
@ -245,10 +242,6 @@ namespace spot
state_based_(state_based), sm_(sm)
{
d.nvars = 0;
unsigned count = sm.scc_count();
for (unsigned i = 0; i < count; ++i)
if (!sm_.trivial(i) && is_weak_scc(sm, i))
d.weak_scc.insert(i);
}
int size()
@ -272,15 +265,14 @@ namespace spot
{
unsigned i_scc = sm_.scc_of_state(d.int_to_state[i]);
bool is_weak = sm_.trivial(i_scc)
|| (d.weak_scc.find(i_scc) != d.weak_scc.end());
bool is_trivial = sm_.trivial(i_scc);
for (int j = 1; j <= d.cand_size; ++j)
{
d.prodid[state_pair(j, i)] = ++d.nvars;
// skip weak or trivial SCCs
if (is_weak)
// skip trivial SCCs
if (is_trivial)
continue;
for (int k = 1; k <= size_; ++k)
@ -325,17 +317,6 @@ namespace spot
}
}
}
if (!d.weak_scc.empty())
{
for (int i = 1; i <= d.cand_size; ++i)
for (int j = 1; j <= d.cand_size; ++j)
{
state_pair pc(i, j);
d.pathcand[pc] = ++d.nvars;
}
}
}
};
@ -487,49 +468,6 @@ namespace spot
delete it;
}
if (!d.weak_scc.empty())
{
dout << "Rules for tracking paths in the candidate\n";
for (int q1 = 1; q1 <= d.cand_size; q1++)
{
state_pair q1q1(q1, q1);
int q1q1id = d.pathcand[q1q1];
dout << q1q1 << "C\n";
out << q1q1id << " 0\n";
++nclauses;
for (int q2 = 1; q2 <= d.cand_size; q2++)
{
state_pair q1q2(q1, q2);
int q1q2id = d.pathcand[q1q2];
for (int q3 = 1; q3 <= d.cand_size; q3++)
{
if (q3 == q1)
continue;
state_pair q1q3(q1, q3);
int q1q3id = d.pathcand[q1q3];
bdd all = bddtrue;
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
transition t(q2, s, q3);
int ti = d.transid[t];
dout << q1q2 << "C ∧ " << t << "δ → "
<< q1q3 << "C\n";
out << -q1q2id << ' ' << -ti << ' ' << q1q3id
<< " 0\n";
++nclauses;
}
}
}
}
}
bdd all_acc = ref->all_acceptance_conditions();
// construction of contraints (4,5) : all loops in the product
@ -546,9 +484,6 @@ namespace spot
// cycle, so they must belong to the same SCC.
if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc)
continue;
if (d.weak_scc.find(q1p_scc) == d.weak_scc.end())
{
// The SCC is not weak.
for (int q1 = 1; q1 <= d.cand_size; ++q1)
for (int q2 = 1; q2 <= d.cand_size; ++q2)
{
@ -586,16 +521,15 @@ namespace spot
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap,
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";
dout << p1 << "R ∧ " << t << "δ → ¬" << t
<< "F\n";
out << -pid1 << " " << -ti << " "
<< -ta << " 0\n";
++nclauses;
@ -614,15 +548,14 @@ namespace spot
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap,
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";
dout << p1 << "R ∧ " << t << "δ → " << p2
<< "R\n";
out << -pid1 << " " << -ti << " "
<< pid2 << " 0\n";
++nclauses;
@ -633,77 +566,6 @@ namespace spot
delete it;
}
}
else // The SCC is weak.
{
for (int q1 = 1; q1 <= d.cand_size; ++q1)
{
state_pair q1q1p(q1, q1p);
int q1q1pid = d.prodid[q1q1p];
for (int q2 = 1; q2 <= d.cand_size; ++q2)
{
state_pair q2q2p(q2, q2p);
int q2q2pid = d.prodid[q2q2p];
state_pair q1q2(q1, q2);
int q1q2id = d.pathcand[q1q2];
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();
// Skip destinations different from q1.
if (dp != q1p)
continue;
bdd all = it->current_condition();
while (all != bddfalse)
{
bdd s = bdd_satoneset(all, ap,
bddfalse);
all -= s;
transition t(q2, s, q1);
int tid = d.transid[t];
int tacc = d.transacc[t];
if (sm.accepting(q1p_scc))
{
dout << q1q1p << " ∧ "
<< q2q2p << " ∧ "
<< q1q2 << "C ∧ "
<< t << "δ → " << t << "F \n";
out << -q1q1pid << ' '
<< -q2q2pid << ' '
<< -q1q2id << ' '
<< -tid << ' '
<< tacc << " 0\n";
}
else
{
dout << q1q1p << " ∧ "
<< q2q2p << " ∧ "
<< q1q2 << "C ∧ "
<< t << "δ → ¬" << t << "F \n";
out << -q1q1pid << ' '
<< -q2q2pid << ' '
<< -q1q2id << ' '
<< -tid << ' '
<< -tacc << " 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
@ -719,9 +581,6 @@ namespace spot
// cycle, so they must belong to the same SCC.
if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc)
continue;
// Weak SCCs have already be dealt with.
if (d.weak_scc.find(q1p_scc) != d.weak_scc.end())
continue;
for (int q1 = 1; q1 <= d.cand_size; ++q1)
for (int q2 = 1; q2 <= d.cand_size; ++q2)
{