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

satmin: ignore (s,l,d2) if (s,l,d1) is already in result

Browse source 
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2013-09-11 14:36:08 +02:00
parent 90a466d6a3
commit b318b151c8
2 changed files with 85 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

50
src/tgbaalgos/dtbasat.cc
View file

@ -95,6 +95,32 @@ namespace spot
} }
}; };
struct src_cond
{
int src;
bdd cond;
src_cond(int src, bdd cond)
: src(src), cond(cond)
{
}
bool operator<(const src_cond& other) const
{
if (this->src < other.src)
return true;
if (this->src > other.src)
return false;
return this->cond.id() < other.cond.id();
}
bool operator==(const src_cond& other) const
{
return (this->src == other.src
&& this->cond.id() == other.cond.id());
}
};
struct state_pair struct state_pair
{ {
int a; int a;
@ -678,6 +704,7 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::set<int> acc_states; std::set<int> acc_states;
std::set<src_cond> seen_trans;
for (sat_solution::const_iterator i = solution.begin(); for (sat_solution::const_iterator i = solution.begin();
i != solution.end(); ++i) i != solution.end(); ++i)
{ {
@ -694,17 +721,22 @@ namespace spot
if (t != satdict.revtransid.end()) if (t != satdict.revtransid.end())
{ {
last_aut_trans = a->create_transition(t->second.src, // Skip (s,l,d2) if we have already seen some (s,l,d1).
t->second.dst); if (seen_trans.insert(src_cond(t->second.src,
last_aut_trans->condition = t->second.cond; t->second.cond)).second)
last_sat_trans = &t->second; {
last_aut_trans = a->create_transition(t->second.src,
t->second.dst);
last_aut_trans->condition = t->second.cond;
last_sat_trans = &t->second;
dout << v << "\t" << t->second << "δ\n"; dout << v << "\t" << t->second << "δ\n";
// Mark the transition as accepting if the source is. // Mark the transition as accepting if the source is.
if (state_based if (state_based
&& acc_states.find(t->second.src) != acc_states.end()) && acc_states.find(t->second.src) != acc_states.end())
last_aut_trans->acceptance_conditions = acc; last_aut_trans->acceptance_conditions = acc;
}
} }
else else
{ {

56
src/tgbaalgos/dtgbasat.cc
View file

@ -96,6 +96,32 @@ namespace spot
} }
}; };
struct src_cond
{
int src;
bdd cond;
src_cond(int src, bdd cond)
: src(src), cond(cond)
{
}
bool operator<(const src_cond& other) const
{
if (this->src < other.src)
return true;
if (this->src > other.src)
return false;
return this->cond.id() < other.cond.id();
}
bool operator==(const src_cond& other) const
{
return (this->src == other.src
&& this->cond.id() == other.cond.id());
}
};
struct transition_acc struct transition_acc
{ {
int src; int src;
@ -875,6 +901,7 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::map<int, bdd> state_acc; std::map<int, bdd> state_acc;
std::set<src_cond> seen_trans;
for (sat_solution::const_iterator i = solution.begin(); for (sat_solution::const_iterator i = solution.begin();
i != solution.end(); ++i) i != solution.end(); ++i)
{ {
@ -891,19 +918,24 @@ namespace spot
if (t != satdict.revtransid.end()) if (t != satdict.revtransid.end())
{ {
last_aut_trans = a->create_transition(t->second.src, // Skip (s,l,d2) if we have already seen some (s,l,d1).
t->second.dst); if (seen_trans.insert(src_cond(t->second.src,
last_aut_trans->condition = t->second.cond; t->second.cond)).second)
last_sat_trans = &t->second;
dout << v << "\t" << t->second << "δ\n";
if (state_based)
{ {
std::map<int, bdd>::const_iterator i = last_aut_trans = a->create_transition(t->second.src,
state_acc.find(t->second.src); t->second.dst);
if (i != state_acc.end()) last_aut_trans->condition = t->second.cond;
last_aut_trans->acceptance_conditions = i->second; last_sat_trans = &t->second;
dout << v << "\t" << t->second << "δ\n";
if (state_based)
{
std::map<int, bdd>::const_iterator i =
state_acc.find(t->second.src);
if (i != state_acc.end())
last_aut_trans->acceptance_conditions = i->second;
}
} }
} }
else else