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

Rewrite the check of WDBA state acceptance in minimize().

* src/tgbaalgos/powerset.hh (power_map): New structure, allowing
the caller to retrieve the set of original states corresponding to
the set in the deterministic automaton.
(power_set): Adjust prototype to take a power_map instead of the
acc_list.
* src/tgbaalgos/powerset.cc (power_set): Strip all code using
acc_list, and update power_set.
* src/tgbaalgos/minimize.cc (minimize): Rewrite, using an
algorithm similar to the one in the Dax paper to check whether
state of the minimized automaton should be accepting.
parent 37a8d1dc
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add trivial() and one_state_of() functions to scc_map. Rewrite the check of WDBA state acceptance in minimize().
* src/tgbaalgos/powerset.hh (power_map): New structure, allowing
the caller to retrieve the set of original states corresponding to
the set in the deterministic automaton.
(power_set): Adjust prototype to take a power_map instead of the
acc_list.
* src/tgbaalgos/powerset.cc (power_set): Strip all code using
acc_list, and update power_set.
* src/tgbaalgos/minimize.cc (minimize): Rewrite, using an
algorithm similar to the one in the Dax paper to check whether
state of the minimized automaton should be accepting.
2011-01-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial, * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial,
scc_map::one_state_of): Two new helper functions. scc_map::one_state_of): Two new helper functions.
......
...@@ -19,6 +19,9 @@ ...@@ -19,6 +19,9 @@
// 02111-1307, USA. // 02111-1307, USA.
#include <queue> #include <queue>
#include <deque>
#include <set>
#include <list>
#include "minimize.hh" #include "minimize.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
...@@ -28,7 +31,9 @@ ...@@ -28,7 +31,9 @@
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/safety.hh" #include "tgbaalgos/safety.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/bfssteps.hh"
namespace spot namespace spot
{ {
...@@ -141,28 +146,174 @@ namespace spot ...@@ -141,28 +146,174 @@ namespace spot
return res; return res;
} }
namespace
{
struct wdba_search_acc_loop : public bfs_steps
{
wdba_search_acc_loop(const tgba* det_a,
unsigned scc_n, scc_map& sm,
power_map& pm, const state* dest)
: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
{
seen.insert(dest);
}
virtual
~wdba_search_acc_loop()
{
hash_set::const_iterator i = seen.begin();
while (i != seen.end())
{
hash_set::const_iterator old = i;
++i;
delete *old;
}
}
virtual const state*
filter(const state* s)
{
// Use the state from seen.
hash_set::const_iterator i = seen.find(s);
if (i == seen.end())
{
seen.insert(s);
}
else
{
delete s;
s = *i;
}
// Ignore states outside SCC #n.
if (sm.scc_of_state(s) != scc_n)
return 0;
return s;
}
virtual bool
match(tgba_run::step&, const state* to)
{
return to == dest;
}
unsigned scc_n;
scc_map& sm;
power_map& pm;
const state* dest;
hash_set seen;
};
bool
wdba_scc_is_accepting(const tgba_explicit_number* det_a, unsigned scc_n,
const tgba* orig_a, scc_map& sm, power_map& pm)
{
// Get some state from the SCC #n.
const state* start = sm.one_state_of(scc_n)->clone();
// Find a loop around START in SCC #n.
wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start);
tgba_run::steps loop;
const state* reached = wsal.search(start, loop);
assert(reached == start);
(void)reached;
// Build an automaton representing this loop.
tgba_explicit_number loop_a(det_a->get_dict());
tgba_run::steps::const_iterator i;
int loop_size = loop.size();
int n;
for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
{
loop_a.create_transition(n - 1, n)->condition = i->label;
delete i->s;
}
assert(i != loop.end());
loop_a.create_transition(n - 1, 0)->condition = i->label;
delete i->s;
assert(++i == loop.end());
const state* loop_a_init = loop_a.get_init_state();
assert(loop_a.get_label(loop_a_init) == 0);
// Check if the loop is accepting in the original automaton.
bool accepting = false;
// Iterate on each original state corresponding to start.
const power_map::power_state& ps = pm.states_of(det_a->get_label(start));
for (power_map::power_state::const_iterator it = ps.begin();
it != ps.end() && !accepting; ++it)
{
// Contrustruct a product between
// LOOP_A, and ORIG_A starting in *IT.
tgba* p = new tgba_product_init(&loop_a, orig_a,
loop_a_init, *it);
emptiness_check* ec = couvreur99(p);
emptiness_check_result* res = ec->check();
if (res)
accepting = true;
delete res;
delete ec;
delete p;
}
delete loop_a_init;
return accepting;
}
}
tgba_explicit* minimize(const tgba* a, bool monitor) tgba_explicit* minimize(const tgba* a, bool monitor)
{ {
// The list of accepting states of a.
std::list<const state*> acc_list;
std::queue<hash_set*> todo; std::queue<hash_set*> todo;
// The list of equivalent states. // The list of equivalent states.
std::list<hash_set*> done; std::list<hash_set*> done;
tgba_explicit* det_a = tgba_powerset(a, monitor ? 0 : &acc_list);
hash_set* final = new hash_set; hash_set* final = new hash_set;
hash_set* non_final = new hash_set; hash_set* non_final = new hash_set;
hash_map state_set_map; hash_map state_set_map;
bdd_dict* dict = det_a->get_dict();
std::list<const state*>::iterator li; tgba_explicit_number* det_a;
for (li = acc_list.begin(); li != acc_list.end(); ++li)
final->insert(*li); {
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();
for (unsigned n = 0; n < scc_count; ++n)
{
// Trivial SCCs are not accepting.
if (sm.trivial(n))
continue;
if (wdba_scc_is_accepting(det_a, n, a, sm, pm))
{
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());
}
}
}
}
init_sets(det_a, *final, *non_final); init_sets(det_a, *final, *non_final);
// Size of det_a // Size of det_a
unsigned size = final->size() + non_final->size(); unsigned size = final->size() + non_final->size();
// Use bdd variables to number sets. set_num is the first variable // Use bdd variables to number sets. set_num is the first variable
// available. // available.
unsigned set_num = dict->register_anonymous_variables(size, det_a); unsigned set_num =
det_a->get_dict()->register_anonymous_variables(size, det_a);
std::set<int> free_var; std::set<int> free_var;
for (unsigned i = set_num; i < set_num + size; ++i) for (unsigned i = set_num; i < set_num + size; ++i)
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
...@@ -22,46 +22,33 @@ ...@@ -22,46 +22,33 @@
// 02111-1307, USA. // 02111-1307, USA.
#include <set> #include <set>
#include <map>
#include <deque> #include <deque>
#include "powerset.hh" #include "powerset.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
#include "tgbaalgos/powerset.hh" #include "tgbaalgos/powerset.hh"
#include "tgbaalgos/scc.hh"
#include "bdd.h" #include "bdd.h"
namespace spot namespace spot
{ {
tgba_explicit* tgba_explicit_number*
tgba_powerset(const tgba* aut, tgba_powerset(const tgba* aut, power_map& pm)
std::list<const state*>* acc_list)
{ {
typedef Sgi::hash_set<const state*, state_ptr_hash, typedef power_map::power_state power_state;
state_ptr_equal> state_set; typedef std::map<power_map::power_state, int> power_set;
typedef std::set<const state*, state_ptr_less_than> power_state; typedef std::deque<power_map::power_state> todo_list;
typedef std::map<power_state, int> power_set;
typedef std::deque<power_state> todo_list;
power_set seen; power_set seen;
todo_list todo; todo_list todo;
scc_map m(aut);
tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict()); tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict());
state_set states;
{ {
power_state ps; power_state ps;
state* s = aut->get_init_state(); state* s = aut->get_init_state();
states.insert(s); pm.states.insert(s);
ps.insert(s); ps.insert(s);
todo.push_back(ps); todo.push_back(ps);
seen[ps] = 1; seen[ps] = 1;
if (acc_list) pm.map_[1] = ps;
{
m.build_map();
if (m.accepting(m.scc_of_state(s)))
acc_list->push_front(new state_explicit(res->add_state(1)));
}
} }
unsigned state_num = 1; unsigned state_num = 1;
...@@ -86,30 +73,13 @@ namespace spot ...@@ -86,30 +73,13 @@ namespace spot
// Construct the set of all states reachable via COND. // Construct the set of all states reachable via COND.
power_state dest; power_state dest;
bool accepting = false;
for (i = src.begin(); i != src.end(); ++i) for (i = src.begin(); i != src.end(); ++i)
{ {
tgba_succ_iterator *si = aut->succ_iter(*i); tgba_succ_iterator *si = aut->succ_iter(*i);
for (si->first(); !si->done(); si->next()) for (si->first(); !si->done(); si->next())
if ((cond >> si->current_condition()) == bddtrue) if ((cond >> si->current_condition()) == bddtrue)
{ {
const state* s = si->current_state(); const state* s = pm.canonicalize(si->current_state());
state_set::const_iterator i = states.find(s);
if (i != states.end())
{
delete s;
s = *i;
}
else
{
states.insert(s);
}
if (acc_list)
{
unsigned scc_num = m.scc_of_state(s);
if (m.accepting(scc_num))
accepting = true;
}
dest.insert(s); dest.insert(s);
} }
delete si; delete si;
...@@ -129,29 +99,21 @@ namespace spot ...@@ -129,29 +99,21 @@ namespace spot
{ {
dest_num = ++state_num; dest_num = ++state_num;
seen[dest] = dest_num; seen[dest] = dest_num;
pm.map_[dest_num] = dest;
todo.push_back(dest); todo.push_back(dest);
t = res->create_transition(seen[src], dest_num); t = res->create_transition(seen[src], dest_num);
if (accepting)
{
const state* dst = new state_explicit(t->dest);
acc_list->push_front(dst);
}
} }
res->add_conditions(t, cond); res->add_conditions(t, cond);
} }
} }
res->merge_transitions(); res->merge_transitions();
// Release all states.
state_set::const_iterator i = states.begin();
while (i != states.end())
{
// Advance the iterator before deleting the key.
const state* s = *i;
++i;
delete s;
}
return res; return res;
} }
tgba_explicit_number*
tgba_powerset(const tgba* aut)
{
power_map pm;
return tgba_powerset(aut, pm);
}
} }
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2011 Laboratoire de Recherche et Développement de
// l'Epita.
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
...@@ -23,21 +25,72 @@ ...@@ -23,21 +25,72 @@
# define SPOT_TGBAALGOS_POWERSET_HH # define SPOT_TGBAALGOS_POWERSET_HH
# include <list> # include <list>
# include <map>
# include "tgba/tgbaexplicit.hh" # include "tgba/tgbaexplicit.hh"
namespace spot namespace spot
{ {
struct power_map
{
typedef std::set<const state*, state_ptr_less_than> power_state;
typedef std::map<int, power_state> power_map_data;
typedef Sgi::hash_set<const state*, state_ptr_hash,
state_ptr_equal> state_set;
~power_map()
{
// Release all states.
state_set::const_iterator i = states.begin();
while (i != states.end())
{
// Advance the iterator before deleting the key.
const state* s = *i;
++i;
delete s;
}
}
const power_state&
states_of(int s) const
{
return map_.find(s)->second;
}
const state*
canonicalize(const state* s)
{
state_set::const_iterator i = states.find(s);
if (i != states.end())
{
delete s;
s = *i;
}
else
{
states.insert(s);
}
return s;
}
power_map_data map_;
state_set states;
};
/// \brief Build a deterministic automaton, ignoring acceptance conditions. /// \brief Build a deterministic automaton, ignoring acceptance conditions.
/// \ingroup tgba_misc /// \ingroup tgba_misc
/// ///
/// This create a deterministic automaton that recognize the /// This create a deterministic automaton that recognizes the
/// same language as \a aut would if its acceptance conditions /// same language as \a aut would if its acceptance conditions
/// were ignored. This is the classical powerset algorithm. /// were ignored. This is the classical powerset algorithm.
/// If acc_list is not 0. Whenever a power state is created from one ///
/// accepting state (a state belonging to an accepting SCC), then this power /// If \a pm is supplied it will be filled with the set of original states
/// state is added to acc_list. /// associated to each state of the deterministic automaton.
tgba_explicit* tgba_powerset(const tgba* aut, //@{
std::list<const state*>* acc_list = 0); tgba_explicit_number* tgba_powerset(const tgba* aut, power_map& pm);
tgba_explicit_number* tgba_powerset(const tgba* aut);
//@}
} }
#endif // SPOT_TGBAALGOS_POWERSET_HH #endif // SPOT_TGBAALGOS_POWERSET_HH
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