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

tgbaexplicit: speed up merge_transitions()

* src/tgba/tgbaexplicit.hh (merge_transitions): Use a hash table
to merge compatible transitions.
* src/tgbatest/readsave.test: Add a test case.
parent 0bdfd9c7
......@@ -373,31 +373,45 @@ namespace spot
void
merge_transitions()
{
typedef typename transitions_t::iterator trans_t;
typedef std::map<int, trans_t> acc_map;
typedef Sgi::hash_map<const spot::state*, acc_map> dest_map;
typename ls_map::iterator i;
for (i = ls_.begin(); i != ls_.end(); ++i)
{
typename transitions_t::iterator t1;
for (t1 = i->second.successors.begin();
t1 != i->second.successors.end(); ++t1)
{
bdd acc = t1->acceptance_conditions;
const state_explicit<label_t, label_hash_t>* dest = t1->dest;
// Find another transition with the same destination and
// acceptance conditions.
typename transitions_t::iterator t2 = t1;
++t2;
while (t2 != i->second.successors.end())
{
typename transitions_t::iterator t2copy = t2++;
if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
const spot::state* last_dest = 0;
dest_map dm;
typename dest_map::iterator dmi = dm.end();
typename transitions_t::iterator t1 = i->second.successors.begin();
// Loop over all outgoing transitions (cond,acc,dest), and
// store them into dest_map[dest][acc] so that we can merge
// conditions.
while (t1 != i->second.successors.end())
{
t1->condition |= t2copy->condition;
i->second.successors.erase(t2copy);
const spot::state* dest = t1->dest;
if (dest != last_dest)
{
last_dest = dest;
dmi = dm.find(dest);
if (dmi == dm.end())
dmi = dm.insert(std::make_pair(dest, acc_map())).first;
}
int acc = t1->acceptance_conditions.id();
typename acc_map::iterator it = dmi->second.find(acc);
if (it == dmi->second.end())
{
dmi->second[acc] = t1;
++t1;
}
else
{
it->second->condition |= t1->condition;
t1 = i->second.successors.erase(t1);
}
}
}
}
}
}
/// Return the state_explicit for \a name, creating the state if
......@@ -585,6 +599,12 @@ namespace spot
neg_acceptance_conditions_ &= neg;
// Append neg to all acceptance conditions.
// FIXME: Declaring acceptance conditions after the automaton
// has been constructed is very slow because we traverse the
// entire automaton for each new acceptance condition. It would
// be better to fix the automaton in a single pass after all
// acceptance conditions have been declared.
typename ls_map::iterator i;
for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
{
......
#!/bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Dveloppement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
......@@ -58,6 +58,27 @@ diff input stdout
rm -f input stdout expected
# Transition merging
cat >input <<\EOF
acc = c;
s1, s2, "a&!b", c;
s1, s2, "b&a", c;
s1, s2, "!b", ;
s2, s1, "!b", ;
s2, s1, "a&!b", c;
s2, s1, "b&a", c;
EOF
cat >expected <<\EOF
acc = "c";
"s1", "s2", "a", "c";
"s1", "s2", "!b",;
"s2", "s1", "!b",;
"s2", "s1", "a", "c";
EOF
run 0 ../ltl2tgba -b -X input > stdout
diff stdout expected
# Likewise, with a randomly generated TGBA.
run 0 ../randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
......
Supports Markdown
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