alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

degen: introduce three optimizations

Browse source 
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Add three
options use_z_level, use_cust_acc_orders, and use_lvl_cache.
This commit is contained in:
Tomáš Babiak 2012-12-05 20:00:55 +01:00 • committed by Alexandre Duret-Lutz
parent 35e16a0b9a
commit 774a266bfe
2 changed files with 350 additions and 171 deletions
Download patch file Download diff file Expand all files Collapse all files

518
src/tgbaalgos/degen.cc
View file

@ -24,6 +24,10 @@
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include <deque> #include <deque>
#include <vector> #include <vector>
#include "tgbaalgos/scc.hh"
#include "tgba/bddprint.hh"
//#define DEGEN_DEBUG
namespace spot namespace spot
{ {
@ -39,7 +43,7 @@ namespace spot
size_t size_t
operator()(const degen_state& s) const operator()(const degen_state& s) const
{ {
return s.first->hash() & wang32_hash(s.second); return s.first->hash() & wang32_hash(s.second);
} }
}; };
@ -47,17 +51,17 @@ namespace spot
{ {
bool bool
operator()(const degen_state& left, operator()(const degen_state& left,
const degen_state& right) const const degen_state& right) const
{ {
if (left.second != right.second) if (left.second != right.second)
return false; return false;
return left.first->compare(right.first) == 0; return left.first->compare(right.first) == 0;
} }
}; };
// Associate the degeneralized state to its number. // Associate the degeneralized state to its number.
typedef Sgi::hash_map<degen_state, int, typedef Sgi::hash_map<degen_state, int,
degen_state_hash, degen_state_equal> ds2num_map; degen_state_hash, degen_state_equal> ds2num_map;
// Queue of state to be processed. // Queue of state to be processed.
typedef std::deque<degen_state> queue_t; typedef std::deque<degen_state> queue_t;
@ -66,22 +70,22 @@ namespace spot
class unicity_table class unicity_table
{ {
typedef Sgi::hash_set<const state*, typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> uniq_set; state_ptr_hash, state_ptr_equal> uniq_set;
uniq_set m; uniq_set m;
public: public:
const state* operator()(const state* s) const state* operator()(const state* s)
{ {
uniq_set::const_iterator i = m.find(s); uniq_set::const_iterator i = m.find(s);
if (i == m.end()) if (i == m.end())
{ {
m.insert(s); m.insert(s);
return s; return s;
} }
else else
{ {
s->destroy(); s->destroy();
return *i; return *i;
} }
} }
~unicity_table() ~unicity_table()
@ -94,6 +98,12 @@ namespace spot
(*old)->destroy(); (*old)->destroy();
} }
} }
size_t
size()
{
return m.size();
}
}; };
// Acceptance set common to all outgoing transitions of some state. // Acceptance set common to all outgoing transitions of some state.
@ -102,7 +112,7 @@ namespace spot
const tgba* a_; const tgba* a_;
typedef std::pair<bdd, bdd> cache_entry; typedef std::pair<bdd, bdd> cache_entry;
typedef Sgi::hash_map<const state*, cache_entry, typedef Sgi::hash_map<const state*, cache_entry,
state_ptr_hash, state_ptr_equal> cache_t; state_ptr_hash, state_ptr_equal> cache_t;
cache_t cache_; cache_t cache_;
public: public:
@ -112,42 +122,122 @@ namespace spot
cache_t::const_iterator fill_cache(const state* s) cache_t::const_iterator fill_cache(const state* s)
{ {
bdd common = a_->all_acceptance_conditions(); bdd common = a_->all_acceptance_conditions();
bdd union_ = bddfalse; bdd union_ = bddfalse;
tgba_succ_iterator* it = a_->succ_iter(s); tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next()) for (it->first(); !it->done(); it->next())
{ {
bdd set = it->current_acceptance_conditions(); bdd set = it->current_acceptance_conditions();
common &= set; common &= set;
union_ |= set; union_ |= set;
} }
delete it; delete it;
cache_entry e(common, union_); cache_entry e(common, union_);
return cache_.insert(std::make_pair(s, e)).first; return cache_.insert(std::make_pair(s, e)).first;
} }
// Intersection of all outgoing acceptance sets // Intersection of all outgoing acceptance sets
bdd common_acc(const state* s) bdd common_acc(const state* s)
{ {
cache_t::const_iterator i = cache_.find(s); cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end()) if (i == cache_.end())
i = fill_cache(s); i = fill_cache(s);
return i->second.first; return i->second.first;
} }
// Union of all outgoing acceptance sets // Union of all outgoing acceptance sets
bdd union_acc(const state* s) bdd union_acc(const state* s)
{ {
cache_t::const_iterator i = cache_.find(s); cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end()) if (i == cache_.end())
i = fill_cache(s); i = fill_cache(s);
return i->second.second; return i->second.second;
}
};
// Order of accepting sets (for one SCC)
class acc_order
{
std::vector<bdd> order_;
bdd found_;
public:
unsigned
next_level(bdd all, int slevel, bdd acc)
{
bdd temp = acc;
if (all != found_)
{
// Check for new conditions in acc
if ((acc & found_) != acc)
{
bdd acc_t = acc;
while (acc_t != bddfalse)
{
bdd next = bdd_satone(acc_t);
acc_t -= next;
// Add new condition
if ((next & found_) != next)
{
order_.push_back(next);
found_ |= next;
}
}
}
}
acc = temp;
unsigned next = slevel;
while (next < order_.size()
&& (acc & order_[next]) == order_[next])
++next;
return next;
}
void
print(int scc, const bdd_dict* dict)
{
std::vector<bdd>::iterator i;
std::cout << "Order_" << scc << ":\t";
for (i=order_.begin(); i!=order_.end(); i++)
{
bdd_print_acc(std::cout, dict, *i);
std::cout << ", ";
}
std::cout << std::endl;
}
};
// Accepting order for each SCC
class scc_orders
{
bdd all_;
std::map<int, acc_order> orders_;
public:
scc_orders(bdd all): all_(all)
{
}
unsigned
next_level(int scc, int slevel, bdd acc)
{
return orders_[scc].next_level(all_, slevel, acc);
}
void
print(const bdd_dict* dict)
{
std::map<int, acc_order>::iterator i;
for (i = orders_.begin(); i != orders_.end(); i++)
i->second.print(i->first, dict);
} }
}; };
} }
sba* sba*
degeneralize(const tgba* a) degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
bool use_lvl_cache)
{ {
bdd_dict* dict = a->get_dict(); bdd_dict* dict = a->get_dict();
@ -177,13 +267,16 @@ namespace spot
// during the translation.) // during the translation.)
bdd all = a->all_acceptance_conditions(); bdd all = a->all_acceptance_conditions();
while (all != bddfalse) while (all != bddfalse)
{ {
bdd next = bdd_satone(all); bdd next = bdd_satone(all);
all -= next; all -= next;
order.push_back(next); order.push_back(next);
} }
} }
// Initialize scc_orders
scc_orders orders(a->all_acceptance_conditions());
outgoing_acc outgoing(a); outgoing_acc outgoing(a);
// Make sure we always use the same pointer for identical states // Make sure we always use the same pointer for identical states
@ -202,6 +295,17 @@ namespace spot
typedef std::map<int, state_explicit_number::transition*> tr_cache_t; typedef std::map<int, state_explicit_number::transition*> tr_cache_t;
tr_cache_t tr_cache; tr_cache_t tr_cache;
// State level cash
typedef std::map<const state*, int> lvl_cache_t;
lvl_cache_t lvl_cache;
// Compute SCCs in order to use custom acc order for each SCC
// or lvl_cache
scc_map m(a);
if (use_cust_acc_orders || use_lvl_cache)
m.build_map();
queue_t todo; queue_t todo;
const state* s0 = uniq(a->get_init_state()); const state* s0 = uniq(a->get_init_state());
@ -213,84 +317,116 @@ namespace spot
bdd all = a->all_acceptance_conditions(); bdd all = a->all_acceptance_conditions();
tgba_succ_iterator* it = a->succ_iter(s0); tgba_succ_iterator* it = a->succ_iter(s0);
for (it->first(); !it->done(); it->next()) for (it->first(); !it->done(); it->next())
{ {
// Look only for transitions that are accepting. // Look only for transitions that are accepting.
if (all != it->current_acceptance_conditions()) if (all != it->current_acceptance_conditions())
continue; continue;
// Look only for self-loops. // Look only for self-loops.
const state* dest = uniq(it->current_state()); const state* dest = uniq(it->current_state());
if (dest == s0) if (dest == s0)
{ {
// The initial state has an accepting self-loop. // The initial state has an accepting self-loop.
s.second = order.size(); s.second = order.size();
break; break;
} }
} }
delete it; delete it;
} }
#ifdef DEGEN_DEBUG
std::map<const state*, int>names;
names[s.first] = 1;
ds2num[s] = 10000*names[s.first] + 100*s.second + m.scc_of_state(s.first);
#else
ds2num[s] = 0; ds2num[s] = 0;
#endif
todo.push_back(s); todo.push_back(s);
// If use_lvl_cache is on insert initial state to level cash
// Level cash stores first encountered level for each state.
// When entering an SCC first the lvl_cache is checked.
// If such state exists level from chache is used.
// If not, a new level (starting with 0) is computed.
if (use_lvl_cache)
lvl_cache[s.first] = s.second;
while (!todo.empty()) while (!todo.empty())
{ {
s = todo.front(); s = todo.front();
todo.pop_front(); todo.pop_front();
int src = ds2num[s]; int src = ds2num[s];
unsigned slevel = s.second; unsigned slevel = s.second;
// If we have a state on the last level, it should be accepting. // If we have a state on the last level, it should be accepting.
bool is_acc = slevel == order.size(); bool is_acc = slevel == order.size();
// On the accepting level, start again from level 0. // On the accepting level, start again from level 0.
if (is_acc) if (is_acc)
slevel = 0; slevel = 0;
tgba_succ_iterator* i = a->succ_iter(s.first); // Check SCC for state s
for (i->first(); !i->done(); i->next()) int s_scc = -1;
{ if (use_lvl_cache || use_cust_acc_orders)
degen_state d(uniq(i->current_state()), 0); s_scc = m.scc_of_state(s.first);
// The old level is slevel. What should be the new one? tgba_succ_iterator* i = a->succ_iter(s.first);
bdd acc = i->current_acceptance_conditions(); for (i->first(); !i->done(); i->next())
bdd otheracc = outgoing.common_acc(d.first); {
degen_state d(uniq(i->current_state()), 0);
if (is_acc) #ifdef DEGEN_DEBUG
{ if (names.find(d.first) == names.end())
// Ignore the last expected acceptance set (the value of names[d.first] = uniq.size();
// *prev below) if it is common to all other outgoing #endif
// transitions (of the current state) AND if it is not
// used by any outgoing transition of the destination // Check whether the target's SCC is accepting
// state. bool is_scc_acc = false;
// int scc = m.scc_of_state(i->current_state());
// 1) It's correct to do that, because this acceptance if (m.accepting(scc))
// set is common to other outgoing transitions. is_scc_acc = true;
// Therefore if we make a cycle to this state we
// will eventually see that acceptance set thanks // The old level is slevel. What should be the new one?
// to the "pulling" of the common acceptance sets bdd acc = i->current_acceptance_conditions();
// of the destination state (d.first). bdd otheracc = outgoing.common_acc(d.first);
//
// 2) It's also desirable because it makes the if (is_acc)
// degeneralization idempotent (up to a renaming of {
// states). Consider the following automaton where // Ignore the last expected acceptance set (the value of
// 1 is initial and => marks accepting transitions: // *prev below) if it is common to all other outgoing
// 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, // transitions (of the current state) AND if it is not
// with 1 as accepting state. However if you try // used by any outgoing transition of the destination
// degeralize it without ignoring *prev, you'll get // state.
// two copies of states 2, depending on whether we //
// reach it using 1=>2 or from 2->2. If this // 1) It's correct to do that, because this acceptance
// example was not clear, uncomment this following // set is common to other outgoing transitions.
// "if" block, and play with the "degenid.test" // Therefore if we make a cycle to this state we
// test case. // will eventually see that acceptance set thanks
// // to the "pulling" of the common acceptance sets
// 3) Ignoring all common acceptance sets would also // of the destination state (d.first).
// be correct, but it would make the //
// degeneralization produce larger automata in some // 2) It's also desirable because it makes the
// cases. The current condition to ignore only one // degeneralization idempotent (up to a renaming of
// acceptance set if is this not used by the next // states). Consider the following automaton where
// state is a heuristic that is compatible with // 1 is initial and => marks accepting transitions:
// point 2) above while not causing more states to // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA,
// be generated in our benchmark of 188 formulae // with 1 as accepting state. However if you try
// from the literature. // degeralize it without ignoring *prev, you'll get
// two copies of states 2, depending on whether we
// reach it using 1=>2 or from 2->2. If this
// example was not clear, uncomment this following
// "if" block, and play with the "degenid.test"
// test case.
//
// 3) Ignoring all common acceptance sets would also
// be correct, but it would make the
// degeneralization produce larger automata in some
// cases. The current condition to ignore only one
// acceptance set if is this not used by the next
// state is a heuristic that is compatible with
// point 2) above while not causing more states to
// be generated in our benchmark of 188 formulae
// from the literature.
if (!order.empty()) if (!order.empty())
{ {
unsigned prev = order.size() - 1; unsigned prev = order.size() - 1;
@ -302,70 +438,112 @@ namespace spot
acc -= order[prev]; acc -= order[prev];
} }
} }
} }
// A transition in the SLEVEL acceptance set should // A transition in the SLEVEL acceptance set should
// be directed to the next acceptance set. If the // be directed to the next acceptance set. If the
// current transition is also in the next acceptance // current transition is also in the next acceptance
// set, then go to the one after, etc. // set, then go to the one after, etc.
// //
// See Denis Oddoux's PhD thesis for a nice // See Denis Oddoux's PhD thesis for a nice
// explanation (in French). // explanation (in French).
// @PhDThesis{ oddoux.03.phd, // @PhDThesis{ oddoux.03.phd,
// author = {Denis Oddoux}, // author = {Denis Oddoux},
// title = {Utilisation des automates alternants pour un // title = {Utilisation des automates alternants pour un
// model-checking efficace des logiques // model-checking efficace des logiques
// temporelles lin{\'e}aires.}, // temporelles lin{\'e}aires.},
// school = {Universit{\'e}e Paris 7}, // school = {Universit{\'e}e Paris 7},
// year = {2003}, // year = {2003},
// address= {Paris, France}, // address= {Paris, France},
// month = {December} // month = {December}
// } // }
unsigned next = slevel; if (is_scc_acc)
// Consider both the current acceptance sets, and the {
// acceptance sets common to the outgoing transitions of acc |= otheracc;
// the destination state. // If use_z_lvl is on, start with level zero 0 when swhitching SCCs
acc |= otheracc; unsigned next = (!use_z_lvl || s_scc == scc)?slevel:0;
while (next < order.size() && bdd_implies(order[next], acc))
++next;
d.second = next; // If lvl_cache is used and switching SCCs, use level from cahce
if (use_lvl_cache && s_scc != scc && lvl_cache.find(d.first) != lvl_cache.end())
{
d.second = lvl_cache[d.first];
}
else
{
// If using custom acc orders, get next level for this scc
if (use_cust_acc_orders)
d.second = orders.next_level(scc, next, acc);
// Else compute level according the global acc order
else
{
// Consider both the current acceptance sets, and the
// acceptance sets common to the outgoing transitions of
// the destination state.
while (next < order.size()
&& (acc & order[next]) == order[next])
++next;
// Have we already seen this destination? d.second = next;
int dest; }
ds2num_map::const_iterator di = ds2num.find(d); }
if (di != ds2num.end()) }
{
dest = di->second;
}
else
{
dest = ds2num.size();
ds2num[d] = dest;
todo.push_back(d);
}
state_explicit_number::transition*& t = // Have we already seen this destination?
tr_cache[dest * 2 + is_acc]; int dest;
ds2num_map::const_iterator di = ds2num.find(d);
if (di != ds2num.end())
{
dest = di->second;
}
else
{
#ifdef DEGEN_DEBUG
dest = 10000*names[d.first] + 100*d.second + scc;
#else
dest = ds2num.size();
#endif
ds2num[d] = dest;
todo.push_back(d);
// Insert new state to cash
if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end())
lvl_cache[d.first] = d.second;
}
if (t == 0) state_explicit_number::transition*& t =
{ tr_cache[dest * 2 + is_acc];
// Actually create the transition.
t = res->create_transition(src, dest); if (t == 0)
t->condition = i->current_condition(); {
// If the source state is accepting, we have to put // Actually create the transition.
// degen_acc on all outgoing transitions. (We are still t = res->create_transition(src, dest);
// building a TGBA; we only assure that it can be used as t->condition = i->current_condition();
// an SBA.) // If the source state is accepting, we have to put
t->acceptance_conditions = is_acc ? degen_acc : bddfalse; // degen_acc on all outgoing transitions. (We are still
} // building a TGBA; we only assure that it can be used as
else // an SBA.)
{ t->acceptance_conditions = is_acc ? degen_acc : bddfalse;
t->condition |= i->current_condition(); }
} else
} {
delete i; t->condition |= i->current_condition();
tr_cache.clear(); }
}
delete i;
tr_cache.clear();
} }
#ifdef DEGEN_DEBUG
std::vector<bdd>::iterator i;
std::cout << "Orig. order: \t";
for (i=order.begin(); i!=order.end(); i++)
{
bdd_print_acc(std::cout, dict, *i);
std::cout << ", ";
}
std::cout << std::endl;
orders.print(dict);
#endif
res->merge_transitions();
return res; return res;
} }
} }

3
src/tgbaalgos/degen.hh
View file

@ -35,7 +35,8 @@ namespace spot
/// ///
/// \see tgba_sba_proxy, tgba_tba_proxy /// \see tgba_sba_proxy, tgba_tba_proxy
/// \ingroup tgba_misc /// \ingroup tgba_misc
sba* degeneralize(const tgba* a); sba* degeneralize(const tgba* a, bool use_z_lvl = true, bool use_cust_acc_orders = true,
bool use_lvl_cache = true);
} }