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

tgba_digraph: add a purge_dead_states() method

* src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc (purge_dead_states): New.
* src/graph/graph.hh (defrag_states): New methods.
* src/tgbaalgos/dtgbacomp.cc: Use it.
* src/tgbatest/det.test: Fix state number.
parent 63708ddc
......@@ -273,8 +273,7 @@ namespace spot
killer_trans_iterator operator++(int)
{
killer_trans_iterator ti = *this;
prev_ = this->t_;
this->t_ = this->operator*().next_succ;
++*this;
return ti;
}
......@@ -302,7 +301,7 @@ namespace spot
// Erased transitions have themselves as next_succ.
this->operator*().next_succ = this->t_;
// Advance iterator to next transitions.
// Advance iterator to next transition.
this->t_ = next;
++this->g_->killed_trans_;
......@@ -647,6 +646,57 @@ namespace spot
}
}
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
{
assert(newst.size() == states_.size());
assert(used_states > 0);
// Shift all states in states_, as indicated by newst.
unsigned send = states_.size();
for (state s = 0; s < send; ++s)
{
state dst = newst[s];
if (dst == s || dst == -1U)
continue;
states_[dst] = std::move(states_[s]);
}
states_.resize(used_states);
// Shift all transitions in transitions_. The algorithm is
// similar to remove_if, but it also keeps the correspondence
// between the old and new index as newidx[old] = new.
unsigned tend = transitions_.size();
std::vector<transition> newidx(tend);
unsigned dest = 1;
for (transition t = 1; t < tend; ++t)
{
if (is_dead_transition(t))
continue;
if (t != dest)
transitions_[dest] = std::move(transitions_[t]);
newidx[t] = dest;
++dest;
}
transitions_.resize(dest);
killed_trans_ = 0;
// Adjust next_succ and dst pointers in all transitions.
for (transition t = 1; t < dest; ++t)
{
auto& tr = transitions_[t];
tr.next_succ = newidx[tr.next_succ];
tr.dst = newst[tr.dst];
assert(tr.dst != -1U);
}
// Adjust succ and succ_tails pointers in all states.
for (auto& s: states_)
{
s.succ = newidx[s.succ];
s.succ_tail = newidx[s.succ_tail];
}
}
};
}
......
......@@ -24,14 +24,15 @@ namespace spot
{
void tgba_digraph::merge_transitions()
{
for (auto& s: g_.states())
{
// Map a pair (dest state, acc) to the first transition seen
// with such characteristic.
typedef std::pair<graph_t::state, acc_cond::mark_t> key_t;
std::unordered_map<key_t, graph_t::transition, pair_hash> trmap;
for (auto& s: g_.states())
{
// Get a clear map for each state.
trmap.clear();
auto t = g_.out_iteraser(s);
while (t)
......@@ -61,4 +62,57 @@ namespace spot
g_.defrag();
}
void tgba_digraph::purge_dead_states()
{
unsigned num_states = g_.num_states();
if (num_states == 0)
return;
std::vector<unsigned> info(num_states, 0);
// In this loop, info[s] means that the state is useless.
bool untouched;
do
{
untouched = true;
for (unsigned s = 0; s < num_states; ++s)
{
if (info[s])
continue;
bool useless = true;
auto t = g_.out_iteraser(s);
while (t)
{
// Erase any transition to a unused state.
if (info[t->dst])
{
t.erase();
continue;
}
// if we have a transition, to a used state,
// then the state is useful.
useless = false;
++t;
}
if (useless)
{
info[s] = true;
untouched = false;
}
}
}
while (!untouched);
// Assume that the initial state is useful.
info[init_number_] = false;
// Now renumber each used state.
unsigned current = 0;
for (auto& v: info)
if (v)
v = -1U;
else
v = current++;
if (current == info.size())
return; // No useless state.
init_number_ = info[init_number_];
g_.defrag_states(std::move(info), current);
}
}
......@@ -388,6 +388,9 @@ namespace spot
/// extremities and acceptance.
void merge_transitions();
/// Remove all states without successors.
void purge_dead_states();
bool state_is_accepting(unsigned s) const
{
assert(has_state_based_acc());
......
......@@ -101,7 +101,7 @@ namespace spot
res->new_transition(src, sink, missingcond);
}
res->merge_transitions();
// FIXME: Remove unreachable states.
res->purge_dead_states();
return res;
}
......
......@@ -105,7 +105,7 @@ digraph G {
2 -> 4 [label="!b"]
3 [label="3"]
3 -> 3 [label="!a\n{0}"]
4 [label="5"]
4 [label="4"]
4 -> 4 [label="!b\n{0}"]
}
EOF
......
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