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

get rid of tgba_tba_proxy

Browse source 
Replace it by a new degeneralize_tba(), that use the same tricks as
degeneralize().

* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: Delete.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Implement
a degeneralize_tba() function sharing its code
with degeneralize().
* src/tgbatest/ltl2tgba.cc: Rename -D to -DT so that we can pass it the
same option as -DS.
* src/tgbatest/degenid.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/ltlcounter.test,
src/tgbatest/ltlcross.test, src/tgbatest/spotlbtt.test,
src/tgbatest/ltl2tgba.test: Adjust.
* src/tgbatest/det.test, src/tgbatest/emptchk.test: Adjust numbers to
the smaller output.
* src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
src/tgbatest/randtgba.cc, src/tgbatest/complementation.cc,
wrap/python/spot.i, wrap/python/tests/ltl2tgba.py,
src/sabatest/sabacomplementtgba.cc: Adjust to the removal
of tgba_tba_proxy, using degeneralize_tba() if needed.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-12 13:32:32 +02:00
parent e9893586cc
commit 5739240c0f
25 changed files with 488 additions and 1090 deletions
Download patch file Download diff file Expand all files Collapse all files

747
src/tgbaalgos/degen.cc
View file

@ -249,363 +249,408 @@ namespace spot
i->second.print(i->first, dict);
}
};
template<bool want_sba>
tgba_digraph*
degeneralize_aux(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{
bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
bdd_dict* dict = a->get_dict();
// The result automaton is an SBA.
auto res = new tgba_digraph(dict);
if (want_sba)
res->set_bprop(tgba_digraph::StateBasedAcc);
// We use the same BDD variables as the input, except for the
// acceptance.
dict->register_all_variables_of(a, res);
dict->unregister_all_typed_variables(bdd_dict::acc, res);
// Invent a new acceptance set for the degeneralized automaton.
int accvar =
dict->register_acceptance_variable(ltl::constant::true_instance(), res);
bdd degen_acc = bdd_ithvar(accvar);
res->set_acceptance_conditions(degen_acc);
// Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can
// be used as a level in degen_state to indicate the next expected
// acceptance set. Level order.size() is a special level used to
// denote accepting states.
std::vector<bdd> order;
{
// The order is arbitrary, but it turns out that using push_back
// instead of push_front often gives better results because
// acceptance sets at the beginning if the cycle are more often
// used in the automaton. (This surprising fact is probably
// related to the order in which we declare the BDD variables
// during the translation.)
bdd all = a->all_acceptance_conditions();
while (all != bddfalse)
{
bdd next = bdd_satone(all);
all -= next;
order.push_back(next);
}
}
// Initialize scc_orders
bdd allacc = a->all_acceptance_conditions();
scc_orders orders(a->all_acceptance_conditions(), skip_levels);
// Make sure we always use the same pointer for identical states
// from the input automaton.
state_unicity_table uniq;
// Accepting loop checker, for some heuristics.
has_acc_loop acc_loop(a, uniq);
// These maps make it possible to convert degen_state to number
// and vice-versa.
ds2num_map ds2num;
// This map is used to find transitions that go to the same
// destination with the same acceptance. The integer key is
// (dest*2+acc) where dest is the destination state number, and
// acc is 1 iff the transition is accepting. The source
// is always that of the current iteration.
typedef std::map<int, unsigned> tr_cache_t;
tr_cache_t tr_cache;
// State level cache
typedef std::map<const state*, unsigned> lvl_cache_t;
lvl_cache_t lvl_cache;
// Compute SCCs in order to use any optimization.
scc_map m(a);
if (use_scc)
m.build_map();
// Cache for common outgoing acceptances.
outgoing_acc outgoing(a, use_scc ? &m : 0);
queue_t todo;
const state* s0 = uniq(a->get_init_state());
degen_state s(s0, 0);
// As a heuristic for building SBA, if the initial state has at
// least one accepting self-loop, start the degeneralization on
// the accepting level.
if (want_sba && acc_loop.check(s0))
s.second = order.size();
// Otherwise, check for acceptance conditions common to all
// outgoing transitions, and assume we have already seen these and
// start on the associated level.
if (s.second == 0)
{
bdd acc = outgoing.common_acc(s.first);
if (use_cust_acc_orders)
s.second = orders.next_level(m.initial(), s.second, acc);
else
while (s.second < order.size() && bdd_implies(order[s.second], acc))
{
++s.second;
if (!skip_levels)
break;
}
// There is not accepting level for TBA, let reuse level 0.
if (!want_sba && s.second == order.size())
s.second = 0;
}
ds2num[s] = res->new_state();
todo.push_back(s);
// If use_lvl_cache is on insert initial state to level cache
// Level cache 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())
{
s = todo.front();
todo.pop_front();
int src = ds2num[s];
unsigned slevel = s.second;
// If we have a state on the last level, it should be accepting.
bool is_acc = slevel == order.size();
// On the accepting level, start again from level 0.
if (want_sba && is_acc)
slevel = 0;
// Check SCC for state s
int s_scc = -1;
if (use_scc)
s_scc = m.scc_of_state(s.first);
for (auto i: a->succ(s.first))
{
degen_state d(uniq(i->current_state()), 0);
// Check whether the target SCC is accepting
bool is_scc_acc;
int scc;
if (use_scc)
{
scc = m.scc_of_state(d.first);
is_scc_acc = m.accepting(scc);
}
else
{
// If we have no SCC information, treat all SCCs as
// accepting.
scc = -1;
is_scc_acc = true;
}
// The old level is slevel. What should be the new one?
bdd acc = i->current_acceptance_conditions();
bdd otheracc = outgoing.common_acc(d.first);
if (want_sba && is_acc)
{
// Ignore the last expected acceptance set (the value of
// *prev below) if it is common to all other outgoing
// transitions (of the current state) AND if it is not
// used by any outgoing transition of the destination
// state.
//
// 1) It's correct to do that, because this acceptance
// set is common to other outgoing transitions.
// Therefore if we make a cycle to this state we
// will eventually see that acceptance set thanks
// to the "pulling" of the common acceptance sets
// of the destination state (d.first).
//
// 2) It's also desirable because it makes the
// degeneralization idempotent (up to a renaming
// of states). Consider the following automaton
// where 1 is initial and => marks accepting
// transitions: 1=>1, 1=>2, 2->2, 2->1. This is
// already an SBA, with 1 as accepting state.
// However if you try degeralize it without
// ignoring *prev, you'll get two copies of state
// 2, depending on whether we reach it using 1=>2
// or from 2->2. If this example was not clear,
// 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())
{
unsigned prev = order.size() - 1;
bdd common = outgoing.common_acc(s.first);
if (bdd_implies(order[prev], common))
{
bdd u = outgoing.union_acc(d.first);
if (!bdd_implies(order[prev], u))
acc -= order[prev];
}
}
}
// A transition in the SLEVEL acceptance set should
// be directed to the next acceptance set. If the
// current transition is also in the next acceptance
// set, then go to the one after, etc.
//
// See Denis Oddoux's PhD thesis for a nice
// explanation (in French).
// @PhDThesis{ oddoux.03.phd,
// author = {Denis Oddoux},
// title = {Utilisation des automates alternants pour un
// model-checking efficace des logiques
// temporelles lin{\'e}aires.},
// school = {Universit{\'e}e Paris 7},
// year = {2003},
// address= {Paris, France},
// month = {December}
// }
if (is_scc_acc)
{
// If lvl_cache is used and switching SCCs, use level
// from cache
if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end())
{
d.second = lvl_cache[d.first];
}
else
{
// Complete (or replace) the acceptance sets of
// this link with the acceptance sets common to
// all transitions leaving the destination state.
if (s_scc == scc)
acc |= otheracc;
else
acc = otheracc;
// If use_z_lvl is on, start with level zero 0 when
// swhitching SCCs
unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0;
// 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
{
// As a heuristic, if we enter the SCC on a
// state that has at least one accepting
// self-loop, start the degeneralization on
// the accepting level.
if (s_scc != scc && acc_loop.check(d.first))
{
d.second = order.size();
}
else
{
// Consider both the current acceptance
// sets, and the acceptance sets common to
// the outgoing transitions of the
// destination state. But don't do
// that if the state is accepting and we
// are not skipping levels.
if (skip_levels || !is_acc)
while (next < order.size()
&& bdd_implies(order[next], acc))
{
++next;
if (!skip_levels)
break;
}
d.second = next;
}
}
}
}
// In case we are building a TBA is_acc has to be
// set differently for each transition, and
// we do not need to stay use final level.
if (!want_sba)
{
is_acc = d.second == order.size();
if (is_acc) // The transition is accepting
{
d.second = 0; // Make it go to the first level.
// Skip levels as much as possible.
if (acc != allacc && !skip_levels)
{
if (use_cust_acc_orders)
{
d.second = orders.next_level(scc, d.second, acc);
}
else
{
while (d.second < order.size() &&
bdd_implies(order[d.second], acc))
++d.second;
}
}
}
}
// Have we already seen this destination?
int dest;
ds2num_map::const_iterator di = ds2num.find(d);
if (di != ds2num.end())
{
dest = di->second;
}
else
{
dest = res->new_state();
ds2num[d] = dest;
todo.push_back(d);
// Insert new state to cache
if (use_lvl_cache)
{
auto res = lvl_cache.emplace(d.first, d.second);
if (!res.second)
{
if (use_lvl_cache == 3)
res.first->second =
std::max(res.first->second, d.second);
else if (use_lvl_cache == 2)
res.first->second =
std::min(res.first->second, d.second);
}
}
}
unsigned& t = tr_cache[dest * 2 + is_acc];
if (t == 0)
{
// Actually create the transition. If the source
// state is accepting, we have to put degen_acc on all
// outgoing transitions. (We are still building a
// TGBA; we only assure that it can be used as an
// SBA.)
bdd acc = bddfalse;
if (is_acc)
acc = degen_acc;
t = res->new_transition(src, dest,
i->current_condition(), acc);
}
else
{
res->trans_data(t).cond |= i->current_condition();
}
}
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;
}
}
tgba_digraph*
degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{
bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
use_lvl_cache, skip_levels);
}
bdd_dict* dict = a->get_dict();
// The result automaton is an SBA.
auto res = new tgba_digraph(dict);
res->set_bprop(tgba_digraph::SBA);
// We use the same BDD variables as the input, except for the
// acceptance.
dict->register_all_variables_of(a, res);
dict->unregister_all_typed_variables(bdd_dict::acc, res);
// Invent a new acceptance set for the degeneralized automaton.
int accvar =
dict->register_acceptance_variable(ltl::constant::true_instance(), res);
bdd degen_acc = bdd_ithvar(accvar);
res->set_acceptance_conditions(degen_acc);
// Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can
// be used as a level in degen_state to indicate the next expected
// acceptance set. Level order.size() is a special level used to
// denote accepting states.
std::vector<bdd> order;
{
// The order is arbitrary, but it turns out that using push_back
// instead of push_front often gives better results because
// acceptance sets at the beginning if the cycle are more often
// used in the automaton. (This surprising fact is probably
// related to the order in which we declare the BDD variables
// during the translation.)
bdd all = a->all_acceptance_conditions();
while (all != bddfalse)
{
bdd next = bdd_satone(all);
all -= next;
order.push_back(next);
}
}
// Initialize scc_orders
scc_orders orders(a->all_acceptance_conditions(), skip_levels);
// Make sure we always use the same pointer for identical states
// from the input automaton.
state_unicity_table uniq;
// Accepting loop checker, for some heuristics.
has_acc_loop acc_loop(a, uniq);
// These maps make it possible to convert degen_state to number
// and vice-versa.
ds2num_map ds2num;
// This map is used to find transitions that go to the same
// destination with the same acceptance. The integer key is
// (dest*2+acc) where dest is the destination state number, and
// acc is 1 iff the transition is accepting. The source
// is always that of the current iteration.
typedef std::map<int, unsigned> tr_cache_t;
tr_cache_t tr_cache;
// State level cache
typedef std::map<const state*, unsigned> lvl_cache_t;
lvl_cache_t lvl_cache;
// Compute SCCs in order to use any optimization.
scc_map m(a);
if (use_scc)
m.build_map();
// Cache for common outgoing acceptances.
outgoing_acc outgoing(a, use_scc ? &m : 0);
queue_t todo;
const state* s0 = uniq(a->get_init_state());
degen_state s(s0, 0);
// As an heuristic, if the initial state at least one accepting
// self-loop, start the degeneralization on the accepting level.
if (acc_loop.check(s0))
s.second = order.size();
// Otherwise, check for acceptance conditions common to all
// outgoing transitions, and assume we have already seen these and
// start on the associated level.
if (s.second == 0)
{
bdd acc = outgoing.common_acc(s.first);
if (use_cust_acc_orders)
s.second = orders.next_level(m.initial(), s.second, acc);
else
while (s.second < order.size() && bdd_implies(order[s.second], acc))
{
++s.second;
if (!skip_levels)
break;
}
}
ds2num[s] = res->new_state();
todo.push_back(s);
// If use_lvl_cache is on insert initial state to level cache
// Level cache 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())
{
s = todo.front();
todo.pop_front();
int src = ds2num[s];
unsigned slevel = s.second;
// If we have a state on the last level, it should be accepting.
bool is_acc = slevel == order.size();
// On the accepting level, start again from level 0.
if (is_acc)
slevel = 0;
// Check SCC for state s
int s_scc = -1;
if (use_scc)
s_scc = m.scc_of_state(s.first);
for (auto i: a->succ(s.first))
{
degen_state d(uniq(i->current_state()), 0);
#ifdef DEGEN_DEBUG
if (names.find(d.first) == names.end())
names[d.first] = uniq.size();
#endif
// Check whether the target SCC is accepting
bool is_scc_acc;
int scc;
if (use_scc)
{
scc = m.scc_of_state(d.first);
is_scc_acc = m.accepting(scc);
}
else
{
// If we have no SCC information, treat all SCCs as
// accepting.
scc = -1;
is_scc_acc = true;
}
// The old level is slevel. What should be the new one?
bdd acc = i->current_acceptance_conditions();
bdd otheracc = outgoing.common_acc(d.first);
if (is_acc)
{
// Ignore the last expected acceptance set (the value of
// *prev below) if it is common to all other outgoing
// transitions (of the current state) AND if it is not
// used by any outgoing transition of the destination
// state.
//
// 1) It's correct to do that, because this acceptance
// set is common to other outgoing transitions.
// Therefore if we make a cycle to this state we
// will eventually see that acceptance set thanks
// to the "pulling" of the common acceptance sets
// of the destination state (d.first).
//
// 2) It's also desirable because it makes the
// degeneralization idempotent (up to a renaming of
// states). Consider the following automaton where
// 1 is initial and => marks accepting transitions:
// 1=>1, 1=>2, 2->2, 2->1 This is already an SBA,
// with 1 as accepting state. However if you try
// degeralize it without ignoring *prev, you'll get
// two copies of state 2, depending on whether we
// reach it using 1=>2 or from 2->2. If this
// example was not clear, uncomment the 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())
{
unsigned prev = order.size() - 1;
bdd common = outgoing.common_acc(s.first);
if (bdd_implies(order[prev], common))
{
bdd u = outgoing.union_acc(d.first);
if (!bdd_implies(order[prev], u))
acc -= order[prev];
}
}
}
// A transition in the SLEVEL acceptance set should
// be directed to the next acceptance set. If the
// current transition is also in the next acceptance
// set, then go to the one after, etc.
//
// See Denis Oddoux's PhD thesis for a nice
// explanation (in French).
// @PhDThesis{ oddoux.03.phd,
// author = {Denis Oddoux},
// title = {Utilisation des automates alternants pour un
// model-checking efficace des logiques
// temporelles lin{\'e}aires.},
// school = {Universit{\'e}e Paris 7},
// year = {2003},
// address= {Paris, France},
// month = {December}
// }
if (is_scc_acc)
{
// If lvl_cache is used and switching SCCs, use level
// from cache
if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end())
{
d.second = lvl_cache[d.first];
}
else
{
// Complete (or replace) the acceptance sets of
// this link with the acceptance sets common to
// all transitions leaving the destination state.
if (s_scc == scc)
acc |= otheracc;
else
acc = otheracc;
// If use_z_lvl is on, start with level zero 0 when
// swhitching SCCs
unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0;
// 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
{
// As a heuristic, if we enter the SCC on a
// state that has at least one accepting
// self-loop, start the degeneralization on
// the accepting level.
if (s_scc != scc && acc_loop.check(d.first))
{
d.second = order.size();
}
else
{
// Consider both the current acceptance
// sets, and the acceptance sets common to
// the outgoing transitions of the
// destination state. But don't do
// that if the state is accepting and we
// are not skipping levels.
if (skip_levels || !is_acc)
while (next < order.size()
&& bdd_implies(order[next], acc))
{
++next;
if (!skip_levels)
break;
}
d.second = next;
}
}
}
}
// Have we already seen this destination?
int dest;
ds2num_map::const_iterator di = ds2num.find(d);
if (di != ds2num.end())
{
dest = di->second;
}
else
{
dest = res->new_state();
ds2num[d] = dest;
todo.push_back(d);
// Insert new state to cache
if (use_lvl_cache)
{
auto res = lvl_cache.emplace(d.first, d.second);
if (!res.second)
{
if (use_lvl_cache == 3)
res.first->second =
std::max(res.first->second, d.second);
else if (use_lvl_cache == 2)
res.first->second =
std::min(res.first->second, d.second);
}
}
}
unsigned& t = tr_cache[dest * 2 + is_acc];
if (t == 0)
{
// Actually create the transition. If the source
// state is accepting, we have to put degen_acc on all
// outgoing transitions. (We are still building a
// TGBA; we only assure that it can be used as an
// SBA.)
bdd acc = bddfalse;
if (is_acc)
acc = degen_acc;
t = res->new_transition(src, dest,
i->current_condition(), acc);
}
else
{
res->trans_data(t).cond |= i->current_condition();
}
}
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;
tgba_digraph*
degeneralize_tba(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{
return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
use_lvl_cache, skip_levels);
}
}