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

sccinfo: stop keeping track of conditions between SCCs

They are unused.

* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Do
not keep track of conditions between two SCCs.
* src/twaalgos/minimize.cc, src/twaalgos/ltl2tgba_fm.cc:
Adjust.
parent e540eaee
......@@ -1198,8 +1198,8 @@ namespace spot
if (!coacc)
{
// ... or if any of its successors is coaccessible.
for (auto& i: sm->succ(n))
if (coaccessible[i.dst])
for (unsigned i: sm->succ(n))
if (coaccessible[i])
{
coacc = true;
break;
......
......@@ -545,10 +545,10 @@ namespace spot
// Also SCCs are useless if all their successor are
// useless.
unsigned l = k;
for (auto& j: succ)
for (unsigned j: succ)
{
is_useless &= useless[j.dst];
unsigned dj = d[j.dst];
is_useless &= useless[j];
unsigned dj = d[j];
if (dj < l)
l = dj;
}
......
......@@ -127,7 +127,7 @@ namespace spot
// Record the transition between the SCC being popped
// and the previous SCC.
if (!root_.empty())
root_.front().node.succ_.emplace_back(cond, num);
root_.front().node.succ_.emplace_back(num);
}
continue;
}
......@@ -162,15 +162,10 @@ namespace spot
// Record that there is a transition from this SCC to the
// dest SCC labelled with cond.
auto& succ = root_.front().node.succ_;
scc_succs::iterator i = std::find_if(succ.begin(), succ.end(),
[spi](const scc_trans& x) {
return (x.dst ==
(unsigned) spi);
});
scc_succs::iterator i =
std::find(succ.begin(), succ.end(), (unsigned) spi);
if (i == succ.end())
succ.emplace_back(cond, spi);
else
i->cond |= cond;
succ.emplace_back(spi);
continue;
}
......@@ -243,8 +238,8 @@ namespace spot
continue;
}
node_[i].useful_ = false;
for (auto j: node_[i].succ())
if (node_[j.dst].is_useful())
for (unsigned j: node_[i].succ())
if (node_[j].is_useful())
{
node_[i].useful_ = true;
break;
......@@ -358,19 +353,11 @@ namespace spot
}
out << "\"]\n";
for (auto& i: m->succ(state))
for (unsigned dest: m->succ(state))
{
int dest = i.dst;
bdd label = i.cond;
out << " " << state << " -> " << dest
<< " [label=\"";
escape_str(out, bdd_format_formula(aut->get_dict(), label));
out << "\"]\n";
out << " " << state << " -> " << dest << '\n';
if (seen[dest])
continue;
seen[dest] = true;
q.push(dest);
}
......
......@@ -27,17 +27,7 @@ namespace spot
class SPOT_API scc_info
{
public:
struct scc_trans
{
scc_trans(bdd cond, unsigned dst)
: cond(cond), dst(dst)
{
}
bdd cond;
unsigned dst;
};
typedef std::vector<scc_trans> scc_succs;
typedef std::vector<unsigned> scc_succs;
class scc_node
{
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment