tgbagraph: add a merge_transitions() method.
* src/graph/graph.hh: Add some framework to erase transitions, and defrag the resulting transitions_ vector on demand. Also remove the nb_states() and nb_transitions() because num_states() and num_transitions() already exist. * src/graphtest/graph.cc, src/graphtest/ngraph.cc: Adjust to use num_states(). * src/tgba/tgbagraph.hh (merge_transitions): New method. * src/misc/hash.hh: Add a pair_hash class, needed by merge_transitions(). * src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: Add states for transitions removal and merge_transitions().
This commit is contained in:
Alexandre Duret-Lutz
parent
9909699c63
commit
424de90385
7 changed files with 286 additions and 10 deletions
|
|
@ -239,11 +239,80 @@ namespace spot
|
|||
return t_;
|
||||
}
|
||||
|
||||
transition trans() const
|
||||
{
|
||||
return t_;
|
||||
}
|
||||
|
||||
protected:
|
||||
Graph* g_;
|
||||
transition t_;
|
||||
};
|
||||
|
||||
template <typename Graph>
|
||||
class SPOT_API killer_trans_iterator: public trans_iterator<Graph>
|
||||
{
|
||||
typedef trans_iterator<Graph> super;
|
||||
public:
|
||||
typedef typename Graph::state_storage_t state_storage_t;
|
||||
typedef typename Graph::transition transition;
|
||||
|
||||
killer_trans_iterator(Graph* g, transition t, state_storage_t& src):
|
||||
super(g, t), src_(src), prev_(0)
|
||||
{
|
||||
}
|
||||
|
||||
killer_trans_iterator operator++()
|
||||
{
|
||||
prev_ = this->t_;
|
||||
this->t_ = this->operator*().next_succ;
|
||||
return *this;
|
||||
}
|
||||
|
||||
killer_trans_iterator operator++(int)
|
||||
{
|
||||
killer_trans_iterator ti = *this;
|
||||
prev_ = this->t_;
|
||||
this->t_ = this->operator*().next_succ;
|
||||
return ti;
|
||||
}
|
||||
|
||||
// Erase the current transition and advance the iterator.
|
||||
void erase()
|
||||
{
|
||||
transition next = this->operator*().next_succ;
|
||||
|
||||
// Update source state and previous transitions
|
||||
if (prev_)
|
||||
{
|
||||
this->g_->trans_storage(prev_).next_succ = next;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (src_.succ == this->t_)
|
||||
src_.succ = next;
|
||||
}
|
||||
if (src_.succ_tail == this->t_)
|
||||
{
|
||||
src_.succ_tail = prev_;
|
||||
assert(next == 0);
|
||||
}
|
||||
|
||||
// Erased transitions have themselves as next_succ.
|
||||
this->operator*().next_succ = this->t_;
|
||||
|
||||
// Advance iterator to next transitions.
|
||||
this->t_ = next;
|
||||
|
||||
++this->g_->killed_trans_;
|
||||
}
|
||||
|
||||
protected:
|
||||
state_storage_t& src_;
|
||||
transition prev_;
|
||||
};
|
||||
|
||||
|
||||
//////////////////////////////////////////////////
|
||||
// State OUT
|
||||
//////////////////////////////////////////////////
|
||||
|
|
@ -289,6 +358,7 @@ namespace spot
|
|||
{
|
||||
friend class internal::trans_iterator<digraph>;
|
||||
friend class internal::trans_iterator<const digraph>;
|
||||
friend class internal::killer_trans_iterator<digraph>;
|
||||
|
||||
public:
|
||||
typedef internal::trans_iterator<digraph> iterator;
|
||||
|
|
@ -325,7 +395,8 @@ namespace spot
|
|||
protected:
|
||||
state_vector states_;
|
||||
trans_vector transitions_;
|
||||
|
||||
// Number of erased transitions.
|
||||
unsigned killed_trans_;
|
||||
public:
|
||||
/// \brief construct an empty graph
|
||||
///
|
||||
|
|
@ -334,6 +405,7 @@ namespace spot
|
|||
/// limits, but just hints to pre-allocate a data structure that
|
||||
/// may hold that much items.
|
||||
digraph(unsigned max_states = 10, unsigned max_trans = 0)
|
||||
: killed_trans_(0)
|
||||
{
|
||||
states_.reserve(max_states);
|
||||
if (max_trans == 0)
|
||||
|
|
@ -351,7 +423,15 @@ namespace spot
|
|||
|
||||
unsigned num_transitions() const
|
||||
{
|
||||
return transitions_.size();
|
||||
return transitions_.size() - killed_trans_ - 1;
|
||||
}
|
||||
|
||||
bool valid_trans(transition t) const
|
||||
{
|
||||
// Erased transitions have their next_succ pointing to
|
||||
// themselves.
|
||||
return (t < transitions_.size() &&
|
||||
transitions_[t].next_succ != t);
|
||||
}
|
||||
|
||||
template <typename... Args>
|
||||
|
|
@ -449,26 +529,52 @@ namespace spot
|
|||
return t;
|
||||
}
|
||||
|
||||
state index_of_state(state_storage_t& ss)
|
||||
{
|
||||
assert(!states_.empty());
|
||||
return &ss - &states_.front();
|
||||
}
|
||||
|
||||
transition index_of_transition(trans_storage_t& tt)
|
||||
{
|
||||
assert(!transitions_.empty());
|
||||
return &tt - &transitions_.front();
|
||||
}
|
||||
|
||||
internal::state_out<digraph>
|
||||
out(state src)
|
||||
{
|
||||
return {this, states_[src].succ};
|
||||
}
|
||||
|
||||
internal::state_out<digraph>
|
||||
out(state_storage_t& src)
|
||||
{
|
||||
return out(index_of_state(src));
|
||||
}
|
||||
|
||||
internal::state_out<const digraph>
|
||||
out(state src) const
|
||||
{
|
||||
return {this, states_[src].succ};
|
||||
}
|
||||
|
||||
unsigned nb_states() const
|
||||
internal::state_out<const digraph>
|
||||
out(state_storage_t& src) const
|
||||
{
|
||||
return states_.size();
|
||||
return out(index_of_state(src));
|
||||
}
|
||||
|
||||
unsigned nb_trans() const
|
||||
internal::killer_trans_iterator<digraph>
|
||||
out_iteraser(state_storage_t& src)
|
||||
{
|
||||
return transitions_.size();
|
||||
return {this, src.succ, src};
|
||||
}
|
||||
|
||||
internal::killer_trans_iterator<digraph>
|
||||
out_iteraser(state src)
|
||||
{
|
||||
return out_iteraser(state_storage(src));
|
||||
}
|
||||
|
||||
const state_vector& states() const
|
||||
|
|
@ -481,6 +587,42 @@ namespace spot
|
|||
return states_;
|
||||
}
|
||||
|
||||
void defrag()
|
||||
{
|
||||
if (killed_trans_ == 0) // Nothing to do.
|
||||
return;
|
||||
|
||||
// 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 (transitions_[t].next_succ == t)
|
||||
continue;
|
||||
if (t != dest)
|
||||
transitions_[dest] = std::move(transitions_[t]);
|
||||
newidx[t] = dest;
|
||||
++dest;
|
||||
}
|
||||
|
||||
transitions_.resize(dest);
|
||||
killed_trans_ = 0;
|
||||
|
||||
// Adjust next_succ pointers in all transitions.
|
||||
for (transition t = 1; t < dest; ++t)
|
||||
transitions_[t].next_succ = newidx[transitions_[t].next_succ];
|
||||
|
||||
// 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];
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@ void
|
|||
dot(std::ostream& out, spot::digraph<SL, TL>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
unsigned c = g.nb_states();
|
||||
unsigned c = g.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
|
|
|
|||
|
|
@ -73,7 +73,7 @@ void
|
|||
dot(std::ostream& out, const spot::digraph<SL, TL>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
unsigned c = g.nb_states();
|
||||
unsigned c = g.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
|
|
@ -93,7 +93,7 @@ dot(std::ostream& out, const spot::named_graph<G1, G2, G3, G4>& g)
|
|||
{
|
||||
out << "digraph {\n";
|
||||
auto& gg = g.graph();
|
||||
unsigned c = gg.nb_states();
|
||||
unsigned c = gg.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
|
|
|
|||
|
|
@ -44,6 +44,7 @@ void f1()
|
|||
auto s1 = g.new_state();
|
||||
auto s2 = g.new_state();
|
||||
auto s3 = g.new_state();
|
||||
g.new_transition(s1, s1, bddfalse, bddfalse);
|
||||
g.new_transition(s1, s2, p1, bddfalse);
|
||||
g.new_transition(s1, s3, p2, !a1 & a2);
|
||||
g.new_transition(s2, s3, p1 & p2, a1 & !a2);
|
||||
|
|
@ -52,6 +53,36 @@ void f1()
|
|||
g.new_transition(s3, s3, bddtrue, (!a1 & a2) | (a1 & !a2));
|
||||
|
||||
spot::dotty_reachable(std::cout, &tg);
|
||||
|
||||
{
|
||||
auto i = g.out_iteraser(s3);
|
||||
++i;
|
||||
i.erase();
|
||||
i.erase();
|
||||
assert(!i);
|
||||
spot::dotty_reachable(std::cout, &tg);
|
||||
}
|
||||
|
||||
{
|
||||
auto i = g.out_iteraser(s3);
|
||||
i.erase();
|
||||
assert(!i);
|
||||
spot::dotty_reachable(std::cout, &tg);
|
||||
}
|
||||
|
||||
g.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2));
|
||||
g.new_transition(s3, s2, p1 >> p2, bddfalse);
|
||||
g.new_transition(s3, s1, bddtrue, (!a1 & a2) | (a1 & !a2));
|
||||
|
||||
std::cerr << tg.num_transitions() << '\n';
|
||||
assert(tg.num_transitions() == 7);
|
||||
|
||||
spot::dotty_reachable(std::cout, &tg);
|
||||
tg.merge_transitions();
|
||||
spot::dotty_reachable(std::cout, &tg);
|
||||
|
||||
std::cerr << tg.num_transitions() << '\n';
|
||||
assert(tg.num_transitions() == 5);
|
||||
}
|
||||
|
||||
int main()
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ digraph G {
|
|||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="0"]
|
||||
1 -> 1 [label="0\n"]
|
||||
1 -> 2 [label="p1\n"]
|
||||
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||
2 [label="1"]
|
||||
|
|
@ -46,6 +47,55 @@ digraph G {
|
|||
3 -> 2 [label="!p1 | p2\n"]
|
||||
3 -> 3 [label="1\n{Acc[p2], Acc[p1]}"]
|
||||
}
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="0"]
|
||||
1 -> 1 [label="0\n"]
|
||||
1 -> 2 [label="p1\n"]
|
||||
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||
2 [label="1"]
|
||||
2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
|
||||
3 [label="2"]
|
||||
3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"]
|
||||
}
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="0"]
|
||||
1 -> 1 [label="0\n"]
|
||||
1 -> 2 [label="p1\n"]
|
||||
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||
2 [label="1"]
|
||||
2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
|
||||
3 [label="2"]
|
||||
}
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="0"]
|
||||
1 -> 1 [label="0\n"]
|
||||
1 -> 2 [label="p1\n"]
|
||||
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||
2 [label="1"]
|
||||
2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
|
||||
3 [label="2"]
|
||||
3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"]
|
||||
3 -> 2 [label="!p1 | p2\n"]
|
||||
3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
|
||||
}
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="0"]
|
||||
1 -> 2 [label="p1\n"]
|
||||
1 -> 3 [label="p2\n{Acc[p2]}"]
|
||||
2 [label="1"]
|
||||
2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
|
||||
3 [label="2"]
|
||||
3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
|
||||
3 -> 2 [label="!p1 | p2\n"]
|
||||
}
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
|
|
|||
|
|
@ -75,6 +75,18 @@ namespace spot
|
|||
return s;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
struct pair_hash
|
||||
{
|
||||
template<typename T, typename U>
|
||||
std::size_t operator()(const std::pair<T, U> &p) const
|
||||
{
|
||||
return wang32_hash(static_cast<size_t>(p.first) ^
|
||||
static_cast<size_t>(p.second));
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_HASH_HH
|
||||
|
|
|
|||
|
|
@ -233,7 +233,7 @@ namespace spot
|
|||
{
|
||||
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
|
||||
assert(s);
|
||||
assert(s->succ < g_.num_transitions());
|
||||
assert(!s->succ || g_.valid_trans(s->succ));
|
||||
|
||||
if (this->iter_cache_)
|
||||
{
|
||||
|
|
@ -308,6 +308,47 @@ namespace spot
|
|||
{
|
||||
return bddtrue;
|
||||
}
|
||||
|
||||
/// Iterate over all transitions, and merge those with compatible
|
||||
/// extremities and acceptance.
|
||||
void 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, int> key_t;
|
||||
std::unordered_map<key_t, graph_t::transition, pair_hash> trmap;
|
||||
|
||||
auto t = g_.out_iteraser(s);
|
||||
while (t)
|
||||
{
|
||||
// Simply skip false transitions.
|
||||
if (t->cond == bddfalse)
|
||||
{
|
||||
t.erase();
|
||||
continue;
|
||||
}
|
||||
|
||||
key_t k(t->dst, t->acc.id());
|
||||
auto p = trmap.insert(make_pair(k, t.trans()));
|
||||
if (!p.second)
|
||||
{
|
||||
// A previous transitions exist for k, merge the
|
||||
// condition, and schedule the transition for
|
||||
// removal.
|
||||
g_.trans_data(p.first->second).cond |= t->cond;
|
||||
t.erase();
|
||||
}
|
||||
else
|
||||
{
|
||||
++t;
|
||||
}
|
||||
}
|
||||
}
|
||||
g_.defrag();
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue