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

Cleanup the DFA minimization algorithm.

* src/tgbaalgos/minimize.cc (minimize):  Move the minimization
code into...
(minimize_dfa): ... this new function, and fix the condition
under which a partition is considered to be minimal.  Also
use a map instead of a list to lookup known formulae.
parent ef317685
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Cleanup the DFA minimization algorithm.
* src/tgbaalgos/minimize.cc (minimize): Move the minimization
code into...
(minimize_dfa): ... this new function, and fix the condition
under which a partition is considered to be minimal. Also
use a map instead of a list to lookup known formulae.
2011-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speed up the obligation test.
......
......@@ -18,14 +18,25 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
//#define TRACE
#ifdef TRACE
# define trace std::cerr
#else
# define trace while (0) std::cerr
#endif
#include <queue>
#include <deque>
#include <set>
#include <list>
#include <vector>
#include <sstream>
#include "minimize.hh"
#include "ltlast/allnodes.hh"
#include "misc/hash.hh"
#include "misc/bddlt.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/powerset.hh"
......@@ -43,6 +54,31 @@ namespace spot
typedef Sgi::hash_map<const state*, unsigned,
state_ptr_hash, state_ptr_equal> hash_map;
namespace
{
static std::ostream&
dump_hash_set(const hash_set* hs, const tgba* aut, std::ostream& out)
{
out << "{";
const char* sep = "";
for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i)
{
out << sep << aut->format_state(*i);
sep = ", ";
}
out << "}";
return out;
}
static std::string
format_hash_set(const hash_set* hs, const tgba* aut)
{
std::ostringstream s;
dump_hash_set(hs, aut, s);
return s.str();
}
}
// Given an automaton a, find all states that are not in "final" and add
// them to the set "non_final".
void init_sets(const tgba_explicit* a,
......@@ -269,76 +305,19 @@ namespace spot
}
tgba_explicit_number* minimize(const tgba* a, bool monitor)
tgba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a,
hash_set* final)
{
std::queue<hash_set*> todo;
// The list of equivalent states.
std::list<hash_set*> done;
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
hash_map state_set_map;
tgba_explicit_number* det_a;
{
power_map pm;
det_a = tgba_powerset(a, pm);
if (!monitor)
{
// For each SCC of the deterministic automaton, determine if
// it is accepting or not.
scc_map sm(det_a);
sm.build_map();
unsigned scc_count = sm.scc_count();
std::vector<bool> accepting(scc_count);
// SCC are numbered in topological order
for (unsigned n = 0; n < scc_count; ++n)
{
bool acc = true;
if (sm.trivial(n))
{
// Trivial SCCs are accepting if all their
// successors are accepting.
typedef std::list<hash_set*> partition_t;
partition_t cur_run;
partition_t next_run;
// This corresponds to the algorithm in Fig. 1 of
// "Efficient minimization of deterministic weak
// omega-automata" written by Christof Löding and
// published in Information Processing Letters 79
// (2001) pp 105--109. Except we do not keep track
// of the actual color associated to each SCC.
// The list of equivalent states.
partition_t done;
const scc_map::succ_type& succ = sm.succ(n);
for (scc_map::succ_type::const_iterator i = succ.begin();
i != succ.end(); ++i)
{
if (!accepting[i->first])
{
acc = false;
break;
}
}
}
else
{
// Regular SCCs are accepting if any of their loop
// corresponds to an accepting
acc = wdba_scc_is_accepting(det_a, n, a, sm, pm);
}
hash_map state_set_map;
accepting[n] = acc;
if (acc)
{
std::list<const state*> l = sm.states_of(n);
std::list<const state*>::const_iterator il;
for (il = l.begin(); il != l.end(); ++il)
final->insert((*il)->clone());
}
}
}
}
hash_set* non_final = new hash_set;
init_sets(det_a, *final, *non_final);
// Size of det_a
......@@ -361,7 +340,7 @@ namespace spot
used_var[set_num] = s;
free_var.erase(set_num);
if (s > 1)
todo.push(final);
cur_run.push_back(final);
else
done.push_back(final);
for (hash_set::const_iterator i = final->begin();
......@@ -382,7 +361,7 @@ namespace spot
used_var[num] = s;
free_var.erase(num);
if (s > 1)
todo.push(non_final);
cur_run.push_back(non_final);
else
done.push_back(non_final);
for (hash_set::const_iterator i = non_final->begin();
......@@ -396,84 +375,119 @@ namespace spot
// A bdd_states_map is a list of formulae (in a BDD form) associated with a
// destination set of states.
typedef std::list<std::pair<bdd, hash_set*> > bdd_states_map;
// While we have unprocessed sets.
while (!todo.empty())
{
// Get a set to process.
hash_set* cur = todo.front();
todo.pop();
hash_set::iterator hi;
bdd_states_map bdd_map;
for (hi = cur->begin(); hi != cur->end(); ++hi)
{
const state* src = *hi;
bdd f = bddfalse;
tgba_succ_iterator* si = det_a->succ_iter(src);
for (si->first(); !si->done(); si->next())
{
const state* dst = si->current_state();
unsigned dst_set = state_set_map[dst];
delete dst;
f |= (bdd_ithvar(dst_set) & si->current_condition());
}
delete si;
bdd_states_map::iterator bsi;
// Have we already seen this formula ?
for (bsi = bdd_map.begin(); bsi != bdd_map.end() && bsi->first != f;
++bsi)
continue;
if (bsi == bdd_map.end())
{
// No, create a new set.
hash_set* new_set = new hash_set;
new_set->insert(src);
bdd_map.push_back(std::make_pair<bdd, hash_set*>(f, new_set));
}
else
{
// Yes, add the current state to the set.
hash_set* set = bsi->second;
set->insert(src);
}
}
bdd_states_map::iterator bsi = bdd_map.begin();
// The set is minimal.
if (bdd_map.size() == 1)
done.push_back(bsi->second);
else
typedef std::map<bdd, hash_set*, bdd_less_than> bdd_states_map;
bool did_split = true;
while (did_split)
{
for (; bsi != bdd_map.end(); ++bsi)
{
hash_set* set = bsi->second;
// Free the number associated to these states.
unsigned num = state_set_map[*set->begin()];
assert(used_var.find(num) != used_var.end());
unsigned left = (used_var[num] -= set->size());
// Make sure LEFT does not become negative (hence bigger
// than SIZE when read as unsigned)
assert(left < size);
if (left == 0)
{
used_var.erase(num);
free_var.insert(num);
}
// Pick a free number
assert(!free_var.empty());
num = *free_var.begin();
free_var.erase(free_var.begin());
used_var[num] = set->size();
for (hash_set::iterator hit = set->begin(); hit != set->end(); ++hit)
state_set_map[*hit] = num;
// Trivial sets can't be splitted any further.
if (set->size() == 1)
done.push_back(set);
else
todo.push(set);
}
did_split = false;
while (!cur_run.empty())
{
// Get a set to process.
hash_set* cur = cur_run.front();
cur_run.pop_front();
trace << "processing " << format_hash_set(cur, det_a) << std::endl;
hash_set::iterator hi;
bdd_states_map bdd_map;
for (hi = cur->begin(); hi != cur->end(); ++hi)
{
const state* src = *hi;
bdd f = bddfalse;
tgba_succ_iterator* si = det_a->succ_iter(src);
for (si->first(); !si->done(); si->next())
{
const state* dst = si->current_state();
unsigned dst_set = state_set_map[dst];
delete dst;
f |= (bdd_ithvar(dst_set) & si->current_condition());
}
delete si;
// Have we already seen this formula ?
bdd_states_map::iterator bsi = bdd_map.find(f);
if (bsi == bdd_map.end())
{
// No, create a new set.
hash_set* new_set = new hash_set;
new_set->insert(src);
bdd_map[f] = new_set;
}
else
{
// Yes, add the current state to the set.
bsi->second->insert(src);
}
}
bdd_states_map::iterator bsi = bdd_map.begin();
if (bdd_map.size() == 1)
{
// The set was not split.
trace << "set " << format_hash_set(bsi->second, det_a)
<< " was not split" << std::endl;
next_run.push_back(bsi->second);
}
else
{
for (; bsi != bdd_map.end(); ++bsi)
{
hash_set* set = bsi->second;
// Free the number associated to these states.
unsigned num = state_set_map[*set->begin()];
assert(used_var.find(num) != used_var.end());
unsigned left = (used_var[num] -= set->size());
// Make sure LEFT does not become negative (hence bigger
// than SIZE when read as unsigned)
assert(left < size);
if (left == 0)
{
used_var.erase(num);
free_var.insert(num);
}
// Pick a free number
assert(!free_var.empty());
num = *free_var.begin();
free_var.erase(free_var.begin());
used_var[num] = set->size();
for (hash_set::iterator hit = set->begin();
hit != set->end(); ++hit)
state_set_map[*hit] = num;
// Trivial sets can't be splitted any further.
if (set->size() == 1)
{
trace << "set " << format_hash_set(set, det_a)
<< " is minimal" << std::endl;
done.push_back(set);
}
else
{
did_split = true;
trace << "set " << format_hash_set(set, det_a)
<< " should be processed further" << std::endl;
next_run.push_back(set);
}
}
}
delete cur;
}
if (did_split)
trace << "splitting did occur during this pass." << std::endl;
else
trace << "splitting did not occur during this pass." << std::endl;
std::swap(cur_run, next_run);
}
delete cur;
}
done.splice(done.end(), cur_run);
#ifdef TRACE
trace << "Final partition: ";
for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
trace << format_hash_set(*i, det_a) << " ";
trace << std::endl;
#endif
// Build the result.
tgba_explicit_number* res = build_result(det_a, done, final_copy);
......@@ -491,6 +505,74 @@ namespace spot
return res;
}
tgba_explicit_number* minimize(const tgba* a, bool monitor)
{
hash_set* final = new hash_set;
tgba_explicit_number* det_a;
{
power_map pm;
det_a = tgba_powerset(a, pm);
if (!monitor)
{
// For each SCC of the deterministic automaton, determine if
// it is accepting or not.
scc_map sm(det_a);
sm.build_map();
unsigned scc_count = sm.scc_count();
std::vector<bool> accepting(scc_count);
// SCC are numbered in topological order
for (unsigned n = 0; n < scc_count; ++n)
{
bool acc = true;
if (sm.trivial(n))
{
// Trivial SCCs are accepting if all their
// successors are accepting.
// This corresponds to the algorithm in Fig. 1 of
// "Efficient minimization of deterministic weak
// omega-automata" written by Christof Löding and
// published in Information Processing Letters 79
// (2001) pp 105--109. Except we do not keep track
// of the actual color associated to each SCC.
const scc_map::succ_type& succ = sm.succ(n);
for (scc_map::succ_type::const_iterator i = succ.begin();
i != succ.end(); ++i)
{
if (!accepting[i->first])
{
acc = false;
break;
}
}
}
else
{
// Regular SCCs are accepting if any of their loop
// corresponds to an accepting
acc = wdba_scc_is_accepting(det_a, n, a, sm, pm);
}
accepting[n] = acc;
if (acc)
{
std::list<const state*> l = sm.states_of(n);
std::list<const state*>::const_iterator il;
for (il = l.begin(); il != l.end(); ++il)
final->insert((*il)->clone());
}
}
}
}
return minimize_dfa(det_a, final);
}
const tgba*
minimize_obligation(const tgba* aut_f,
const ltl::formula* f, const tgba* aut_neg_f)
......
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