Commit 679b6cff authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

degen: consider incoming edges to select initial levels

Fixes #257.

* spot/twaalgos/degen.cc: Implement this optimization.
* tests/core/degendet.test: Add a few test cases.
* tests/core/ltl2tgba2.test: Adjust expected sizes.
* NEWS: Mention the change.
parent e1c14eb9
...@@ -57,6 +57,11 @@ New in spot 2.3.3.dev (not yet released) ...@@ -57,6 +57,11 @@ New in spot 2.3.3.dev (not yet released)
Streett acceptance. The dual function is Streett acceptance. The dual function is
spot::acc_cond::is_rabin_like() works similarly. spot::acc_cond::is_rabin_like() works similarly.
- The degeneralize() function has learned to consider acceptance
marks common to all edges comming to a state to select its initial
level. A similar trick was already used in sbacc(), and saves a
few states in some cases.
Python: Python:
- The 'spot.gen' package exports the functions from libspotgen. - The 'spot.gen' package exports the functions from libspotgen.
......
...@@ -55,20 +55,26 @@ namespace spot ...@@ -55,20 +55,26 @@ namespace spot
// 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;
// Acceptance set common to all outgoing edges (of the same // Acceptance set common to all outgoing or incoming edges (of the
// SCC -- we do not care about the other) of some state. // same SCC -- we do not care about the others) of some state.
class outgoing_acc final class inout_acc final
{ {
const_twa_graph_ptr a_; const_twa_graph_ptr a_;
typedef std::tuple<acc_cond::mark_t, typedef std::tuple<acc_cond::mark_t,
acc_cond::mark_t,
acc_cond::mark_t, acc_cond::mark_t,
bool> cache_entry; bool> cache_entry;
std::vector<cache_entry> cache_; std::vector<cache_entry> cache_;
const scc_info* sm_; const scc_info* sm_;
unsigned scc_of(unsigned s)
{
return sm_ ? sm_->scc_of(s) : 0;
}
void fill_cache(unsigned s) void fill_cache(unsigned s)
{ {
unsigned s1 = sm_ ? sm_->scc_of(s) : 0; unsigned s1 = scc_of(s);
acc_cond::mark_t common = a_->acc().all_sets(); acc_cond::mark_t common = a_->acc().all_sets();
acc_cond::mark_t union_ = 0U; acc_cond::mark_t union_ = 0U;
bool has_acc_self_loop = false; bool has_acc_self_loop = false;
...@@ -77,12 +83,12 @@ namespace spot ...@@ -77,12 +83,12 @@ namespace spot
{ {
// Ignore edges that leave the SCC of s. // Ignore edges that leave the SCC of s.
unsigned d = t.dst; unsigned d = t.dst;
unsigned s2 = sm_ ? sm_->scc_of(d) : 0; if (scc_of(d) != s1)
if (s2 != s1)
continue; continue;
common &= t.acc; common &= t.acc;
union_ |= t.acc; union_ |= t.acc;
std::get<2>(cache_[d]) &= t.acc;
// an accepting self-loop? // an accepting self-loop?
has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc); has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
...@@ -90,37 +96,56 @@ namespace spot ...@@ -90,37 +96,56 @@ namespace spot
} }
if (!seen) if (!seen)
common = 0U; common = 0U;
cache_[s] = std::make_tuple(common, union_, has_acc_self_loop); std::get<0>(cache_[s]) = common;
std::get<1>(cache_[s]) = union_;
std::get<3>(cache_[s]) = has_acc_self_loop;
} }
public: public:
outgoing_acc(const const_twa_graph_ptr& a, const scc_info* sm): inout_acc(const const_twa_graph_ptr& a, const scc_info* sm):
a_(a), cache_(a->num_states()), sm_(sm) a_(a), cache_(a->num_states()), sm_(sm)
{ {
unsigned n = a->num_states(); unsigned n = a->num_states();
acc_cond::mark_t all = a_->acc().all_sets();
// slot 2 will hold acceptance mark that are common to the
// incoming transitions of each state. For know with all
// marks if there is some incoming edge. The nextx loop will
// constrain this value.
for (auto& e: a_->edges())
if (scc_of(e.src) == scc_of(e.dst))
std::get<2>(cache_[e.dst]) = all;
for (unsigned s = 0; s < n; ++s) for (unsigned s = 0; s < n; ++s)
fill_cache(s); fill_cache(s);
for (unsigned s = 0; s < n; ++s)
std::get<2>(cache_[s]) |= std::get<0>(cache_[s]);
} }
// Intersection of all outgoing acceptance sets // Intersection of all outgoing acceptance sets
acc_cond::mark_t common_acc(unsigned s) acc_cond::mark_t common_out_acc(unsigned s)
{ {
assert(s < cache_.size()); assert(s < cache_.size());
return std::get<0>(cache_[s]); return std::get<0>(cache_[s]);
} }
// Union of all outgoing acceptance sets // Union of all outgoing acceptance sets
acc_cond::mark_t union_acc(unsigned s) acc_cond::mark_t union_out_acc(unsigned s)
{ {
assert(s < cache_.size()); assert(s < cache_.size());
return std::get<1>(cache_[s]); return std::get<1>(cache_[s]);
} }
// Intersection of all incoming acceptance sets
acc_cond::mark_t common_inout_acc(unsigned s)
{
assert(s < cache_.size());
return std::get<2>(cache_[s]);
}
// Has an accepting self-loop // Has an accepting self-loop
bool has_acc_selfloop(unsigned s) bool has_acc_selfloop(unsigned s)
{ {
assert(s < cache_.size()); assert(s < cache_.size());
return std::get<2>(cache_[s]); return std::get<3>(cache_[s]);
} }
}; };
...@@ -264,22 +289,23 @@ namespace spot ...@@ -264,22 +289,23 @@ namespace spot
if (use_scc) if (use_scc)
m = new scc_info(a); m = new scc_info(a);
// Cache for common outgoing acceptances. // Cache for common outgoing/incoming acceptances.
outgoing_acc outgoing(a, m); inout_acc inout(a, m);
queue_t todo; queue_t todo;
// As a heuristic for building SBA, if the initial state has at // As a heuristic for building SBA, if the initial state has at
// least one accepting self-loop, start the degeneralization on // least one accepting self-loop, start the degeneralization on
// the accepting level. // the accepting level.
if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first)) if (want_sba && !ignaccsl && inout.has_acc_selfloop(s.first))
s.second = order.size(); s.second = order.size();
// Otherwise, check for acceptance conditions common to all // Otherwise, check for acceptance conditions common to all
// outgoing edges, and assume we have already seen these and // outgoing edges, plus those common to all incoming edges, and
// start on the associated level. // assume we have already seen these and start on the associated
// level.
if (s.second == 0) if (s.second == 0)
{ {
auto set = outgoing.common_acc(s.first); auto set = inout.common_inout_acc(s.first);
if (SPOT_UNLIKELY(use_cust_acc_orders)) if (SPOT_UNLIKELY(use_cust_acc_orders))
s.second = orders.next_level(m->initial(), s.second, set); s.second = orders.next_level(m->initial(), s.second, set);
else else
...@@ -366,7 +392,7 @@ namespace spot ...@@ -366,7 +392,7 @@ namespace spot
// The old level is slevel. What should be the new one? // The old level is slevel. What should be the new one?
auto acc = i.acc; auto acc = i.acc;
auto otheracc = outgoing.common_acc(d.first); auto otheracc = inout.common_inout_acc(d.first);
if (want_sba && is_acc) if (want_sba && is_acc)
{ {
...@@ -407,10 +433,10 @@ namespace spot ...@@ -407,10 +433,10 @@ namespace spot
if (!order.empty()) if (!order.empty())
{ {
unsigned prev = order.size() - 1; unsigned prev = order.size() - 1;
auto common = outgoing.common_acc(s.first); auto common = inout.common_out_acc(s.first);
if (common.has(order[prev])) if (common.has(order[prev]))
{ {
auto u = outgoing.union_acc(d.first); auto u = inout.union_out_acc(d.first);
if (!u.has(order[prev])) if (!u.has(order[prev]))
acc -= a->acc().mark(order[prev]); acc -= a->acc().mark(order[prev]);
} }
...@@ -446,7 +472,8 @@ namespace spot ...@@ -446,7 +472,8 @@ namespace spot
{ {
// Complete (or replace) the acceptance sets of // Complete (or replace) the acceptance sets of
// this link with the acceptance sets common to // this link with the acceptance sets common to
// all edges leaving the destination state. // all edges of the destination SCC entering or
// leaving the destination state.
if (s_scc == scc) if (s_scc == scc)
acc |= otheracc; acc |= otheracc;
else else
...@@ -471,18 +498,18 @@ namespace spot ...@@ -471,18 +498,18 @@ namespace spot
// the accepting level. // the accepting level.
if (s_scc != scc if (s_scc != scc
&& !ignaccsl && !ignaccsl
&& outgoing.has_acc_selfloop(d.first)) && inout.has_acc_selfloop(d.first))
{ {
d.second = order.size(); d.second = order.size();
} }
else else
{ {
// Consider both the current acceptance // Consider both the current acceptance
// sets, and the acceptance sets common to // sets, and the acceptance sets common
// the outgoing edges of the // to the outgoing edges of the
// destination state. But don't do // destination state. But don't do that
// that if the state is accepting and we // if the state is accepting and we are
// are not skipping levels. // not skipping levels.
if (skip_levels || !is_acc) if (skip_levels || !is_acc)
while (next < order.size() while (next < order.size()
&& acc.has(order[next])) && acc.has(order[next]))
...@@ -506,7 +533,7 @@ namespace spot ...@@ -506,7 +533,7 @@ namespace spot
if (is_acc) // The edge is accepting if (is_acc) // The edge is accepting
{ {
d.second = 0; // Make it go to the first level. d.second = 0; // Make it go to the first level.
// Skip levels as much as possible. // Skip as many levels as possible.
if (!a->acc().accepting(acc) && !skip_levels) if (!a->acc().accepting(acc) && !skip_levels)
{ {
if (use_cust_acc_orders) if (use_cust_acc_orders)
...@@ -544,9 +571,7 @@ namespace spot ...@@ -544,9 +571,7 @@ namespace spot
#ifdef DEGEN_DEBUG #ifdef DEGEN_DEBUG
std::cout << "Orig. order: \t"; std::cout << "Orig. order: \t";
for (auto i: order) for (auto i: order)
{ std::cout << i << ", ";
std::cout << i << ", ";
}
std::cout << '\n'; std::cout << '\n';
orders.print(); orders.print();
#endif #endif
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et Développement # Copyright (C) 2011, 2015-2017 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
...@@ -43,3 +43,13 @@ done ...@@ -43,3 +43,13 @@ done
# used to be reused, instead of the first one. # used to be reused, instead of the first one.
run 0 ltl2tgba -B -f '(b & Fa) U XXG(a M Gb)' --stats=%s,%t >out run 0 ltl2tgba -B -f '(b & Fa) U XXG(a M Gb)' --stats=%s,%t >out
test "4,14" = "`cat out`" test "4,14" = "`cat out`"
# Some optimization in the degeneralization allows this formula
# to be reduced to 3 and 5 states...
run 0 ltl2tgba -B -f 'G(Fp1 & (F!p1 W X!p1))' -f 'F(!p0 & Fp0) W Gp0' \
--stats=%s >out
cat >exp<<EOF
3
5
EOF
diff out exp
...@@ -163,7 +163,7 @@ hkrss-patterns,32, 3,46, 3,46, 3,46, 3,46 ...@@ -163,7 +163,7 @@ hkrss-patterns,32, 3,46, 3,46, 3,46, 3,46
hkrss-patterns,33, 3,46, 3,46, 3,46, 3,46 hkrss-patterns,33, 3,46, 3,46, 3,46, 3,46
hkrss-patterns,34, 2,12, 2,12, 2,12, 2,12 hkrss-patterns,34, 2,12, 2,12, 2,12, 2,12
hkrss-patterns,35, 2,7, 2,7, 2,7, 2,7 hkrss-patterns,35, 2,7, 2,7, 2,7, 2,7
hkrss-patterns,36, 34,192, 34,192, 35,208, 35,208 hkrss-patterns,36, 34,192, 34,192, 34,192, 34,192
hkrss-patterns,37, 2,30, 2,30, 2,30, 2,30 hkrss-patterns,37, 2,30, 2,30, 2,30, 2,30
hkrss-patterns,38, 2,7, 2,7, 3,10, 3,10 hkrss-patterns,38, 2,7, 2,7, 3,10, 3,10
hkrss-patterns,39, 3,11, 3,11, 3,11, 3,11 hkrss-patterns,39, 3,11, 3,11, 3,11, 3,11
......
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