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

alternation: speed up remove_alternation when few labels are used

Browse source 
Related to issue #566.

* spot/twaalgos/alternation.cc (alternation_remover::run): Here.
* tests/core/566.test: Augment test case.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2024-03-17 22:42:18 +01:00
parent 1e512d422b
commit f26f3243dd
3 changed files with 102 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

132
spot/twaalgos/alternation.cc
View file

@ -22,6 +22,7 @@
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/misc/minato.hh>
#include <spot/misc/bddlt.hh>
namespace spot
{
@ -361,7 +362,7 @@ namespace spot
(has_reject_more_ + reject_1_count_) > SPOT_MAX_ACCSETS)
return nullptr;
// Rejecting SCCs of size 1 can be handled using genralized
// Rejecting SCCs of size 1 can be handled using generalized
// Büchi acceptance, using one set per SCC, as in Gastin &
// Oddoux CAV'01. See also Boker & et al. ICALP'10. Larger
// rejecting SCCs require a more expensive procedure known as
@ -375,6 +376,54 @@ namespace spot
// This will raise an exception if we request too many sets.
res->set_generalized_buchi(has_reject_more_ + reject_1_count_);
// Before we start, let's decide how we will iterate on the
// BDD that we use to encode the transition function. We have
// two way of doing so: iterating over 2^AP, or precomputing a
// set of "separated labels" that cover all labels. The
// latter is a good idea if that set is much smaller than
// 2^AP, but we cannot always know that before hand.
std::vector<bdd> separated_labels;
unsigned n_ap = aut_->ap().size();
// If |AP| is small, don't bother with the computation of
// separated labels.
bool will_use_labels = n_ap > 5;
if (will_use_labels)
{
std::set<bdd, bdd_less_than> all_labels;
// Gather all labels, but stop if we see too many.
// The threshold below is arbitrary.
unsigned max_labels = 100 * n_ap;
for (auto& e: aut_->edges())
{
if (all_labels.insert(e.cond).second)
if (all_labels.size() > max_labels)
{
will_use_labels = false;
break;
}
}
if (will_use_labels)
{
separated_labels.reserve(all_labels.size());
separated_labels.push_back(bddtrue);
for (auto& lab: all_labels)
{
// make sure don't realloc during the loop
separated_labels.reserve(separated_labels.size() * 2);
// Do not use a range-based or iterator-based for loop
// here, as push_back invalidates the end iterator.
for (unsigned cur = 0, sz = separated_labels.size();
cur < sz; ++cur)
if (bdd common = separated_labels[cur] & lab;
common != bddfalse)
{
separated_labels[cur] -= lab;
separated_labels.push_back(common);
}
}
}
}
// We for easier computation of outgoing sets, we will
// represent states using BDD variables.
allocate_state_vars();
@ -459,44 +508,53 @@ namespace spot
bdd ap = bdd_exist(bdd_support(bs), all_vars_);
bdd all_letters = bdd_exist(bs, all_vars_);
// First loop over all possible valuations atomic properties.
for (bdd oneletter: minterms_of(all_letters, ap))
{
minato_isop isop(bdd_restrict(bs, oneletter));
bdd dest;
while ((dest = isop.next()) != bddfalse)
{
v.clear();
acc_cond::mark_t m = bdd_to_state(dest, v);
// Given a label, and BDD expression representing
// the combination of destinations, create the edges.
auto create_edges = [&](bdd label, bdd dest_formula)
{
minato_isop isop(dest_formula);
bdd dest;
while ((dest = isop.next()) != bddfalse)
{
v.clear();
acc_cond::mark_t m = bdd_to_state(dest, v);
// if there is no promise "f" between a state
// that does not have f, and a state that have
// "f", we can add one. Doing so will help later
// simplifications performed by postprocessor. An
// example where this is needed is the VWAA
// generated by ltl[23]ba for GFa. Without the
// next loop, the final TGBA has 2 states instead
// of 1.
for (unsigned m1: (all_marks - m).sets())
{
if (has_reject_more_ && m1 == 0)
continue;
auto& sv = s_to_ss[s];
unsigned ms = mark_to_state_[m1];
if (std::find(v.begin(), v.end(), ms) != v.end())
{
unsigned ms = mark_to_state_[m1];
if (std::find(sv.begin(), sv.end(), ms) == sv.end())
m.set(m1);
}
}
// if there is no promise "f" between a state
// that does not have f, and a state that have
// "f", we can add one. Doing so will help later
// simplifications performed by postprocessor. An
// example where this is needed is the VWAA
// generated by ltl[23]ba for GFa. Without the
// next loop, the final TGBA has 2 states instead
// of 1.
for (unsigned m1: (all_marks - m).sets())
{
if (has_reject_more_ && m1 == 0)
continue;
auto& sv = s_to_ss[s];
unsigned ms = mark_to_state_[m1];
if (std::find(v.begin(), v.end(), ms) != v.end())
{
unsigned ms = mark_to_state_[m1];
if (std::find(sv.begin(), sv.end(), ms) == sv.end())
m.set(m1);
}
}
unsigned d = new_state(v, has_mark);
if (has_mark)
m.set(0);
res->new_edge(s, d, oneletter, all_marks - m);
}
}
unsigned d = new_state(v, has_mark);
if (has_mark)
m.set(0);
res->new_edge(s, d, label, all_marks - m);
}
};
if (!will_use_labels)
// Loop over all possible valuations atomic properties.
for (bdd oneletter: minterms_of(all_letters, ap))
create_edges(oneletter, bdd_restrict(bs, oneletter));
else
for (bdd label: separated_labels)
create_edges(label, bdd_relprod(label, bs, res->ap_vars()));
}
res->merge_edges();
return res;