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

degen, sbacc: merge accepting sinks

Browse source 
Fixes #276.

* spot/twaalgos/sbacc.cc, spot/twaalgos/degen.cc: Detect accepting
sinks, and merge them.
* tests/python/dualize.py: Adjust.
* tests/python/sbacc.py: More test cases.
This commit is contained in:
Alexandre Duret-Lutz 2017-07-24 16:13:56 +02:00
parent d12b2cd5b0
commit 37f3154f1d
5 changed files with 170 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -150,6 +150,9 @@ New in spot 2.3.5.dev (not yet released)
- spot::sbacc() is now able to work on alternating automata.
- spot::sbacc() and spot::degeneralize() learned to merge
accepting sinks.
- If the SPOT_BDD_TRACE envorinment variable is set, statistics
about BDD garbage collection and table resizing are shown.

87
spot/twaalgos/degen.cc
View file

@ -50,7 +50,8 @@ namespace spot
};
// Associate the degeneralized state to its number.
typedef std::unordered_map<degen_state, int, degen_state_hash> ds2num_map;
typedef std::unordered_map<degen_state, unsigned,
degen_state_hash> ds2num_map;
// Queue of state to be processed.
typedef std::deque<degen_state> queue_t;
@ -60,14 +61,16 @@ namespace spot
class inout_acc final
{
const_twa_graph_ptr a_;
typedef std::tuple<acc_cond::mark_t,
acc_cond::mark_t,
acc_cond::mark_t,
bool> cache_entry;
typedef std::tuple<acc_cond::mark_t, // common out
acc_cond::mark_t, // union out
acc_cond::mark_t, // common in, then common in+out
bool, // has self-loop
bool> cache_entry; // is true state
std::vector<cache_entry> cache_;
unsigned last_true_state_;
const scc_info* sm_;
unsigned scc_of(unsigned s)
unsigned scc_of(unsigned s) const
{
return sm_ ? sm_->scc_of(s) : 0;
}
@ -78,6 +81,7 @@ namespace spot
acc_cond::mark_t common = a_->acc().all_sets();
acc_cond::mark_t union_ = 0U;
bool has_acc_self_loop = false;
bool is_true_state = false;
bool seen = false;
for (auto& t: a_->out(s))
{
@ -91,7 +95,15 @@ namespace spot
std::get<2>(cache_[d]) &= t.acc;
// an accepting self-loop?
has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
if ((t.dst == s) && a_->acc().accepting(t.acc))
{
has_acc_self_loop = true;
if (t.cond == bddtrue)
{
is_true_state = true;
last_true_state_ = s;
}
}
seen = true;
}
if (!seen)
@ -99,6 +111,7 @@ namespace spot
std::get<0>(cache_[s]) = common;
std::get<1>(cache_[s]) = union_;
std::get<3>(cache_[s]) = has_acc_self_loop;
std::get<4>(cache_[s]) = is_true_state;
}
public:
@ -109,7 +122,7 @@ namespace spot
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
// marks if there is some incoming edge. The next loop will
// constrain this value.
for (auto& e: a_->edges())
if (scc_of(e.src) == scc_of(e.dst))
@ -121,32 +134,42 @@ namespace spot
}
// Intersection of all outgoing acceptance sets
acc_cond::mark_t common_out_acc(unsigned s)
acc_cond::mark_t common_out_acc(unsigned s) const
{
assert(s < cache_.size());
return std::get<0>(cache_[s]);
}
// Union of all outgoing acceptance sets
acc_cond::mark_t union_out_acc(unsigned s)
acc_cond::mark_t union_out_acc(unsigned s) const
{
assert(s < cache_.size());
return std::get<1>(cache_[s]);
}
// Intersection of all incoming acceptance sets
acc_cond::mark_t common_inout_acc(unsigned s)
acc_cond::mark_t common_inout_acc(unsigned s) const
{
assert(s < cache_.size());
return std::get<2>(cache_[s]);
}
// Has an accepting self-loop
bool has_acc_selfloop(unsigned s)
bool has_acc_selfloop(unsigned s) const
{
assert(s < cache_.size());
return std::get<3>(cache_[s]);
}
bool is_true_state(unsigned s) const
{
assert(s < cache_.size());
return std::get<4>(cache_[s]);
}
unsigned last_true_state() const
{
return last_true_state_;
}
};
// Order of accepting sets (for one SCC)
@ -253,8 +276,6 @@ namespace spot
// denote accepting states.
std::vector<unsigned> order;
{
// FIXME: revisit this comment once everything compiles again.
//
// The order is arbitrary, but it turns out that using emplace_back
// instead of push_front often gives better results because
// acceptance sets at the beginning if the cycle are more often
@ -280,10 +301,6 @@ namespace spot
typedef std::map<int, unsigned> tr_cache_t;
tr_cache_t tr_cache;
// Read this early, because it might create a state if the
// automaton is empty.
degen_state s(a->get_init_state_number(), 0);
// State->level cache
std::vector<std::pair<unsigned, bool>> lvl_cache(a->num_states());
@ -297,6 +314,8 @@ namespace spot
queue_t todo;
degen_state s(a->get_init_state_number(), 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.
@ -323,11 +342,30 @@ namespace spot
s.second = 0;
}
auto new_state = [&](degen_state& ds)
auto new_state = [&](degen_state ds)
{
// Merge all true states into a single one.
bool ts = inout.is_true_state(ds.first);
if (ts)
ds = {inout.last_true_state(), 0U};
auto di = ds2num.find(ds);
if (di != ds2num.end())
return di->second;
unsigned ns = res->new_state();
ds2num[ds] = ns;
todo.emplace_back(ds);
if (ts)
{
res->new_acc_edge(ns, ns, bddtrue, true);
// As we do not process all outgoing transition of
// ds.first, it is possible that a non-deterministic
// automaton becomes deterministic.
if (res->prop_universal().is_false())
res->prop_universal(trival::maybe());
}
else
todo.emplace_back(ds);
assert(ns == orig_states->size());
orig_states->emplace_back(ds.first);
@ -555,12 +593,7 @@ namespace spot
}
// 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 = new_state(d);
int dest = new_state(d);
unsigned& t = tr_cache[dest * 2 + is_acc];

28
spot/twaalgos/sbacc.cc
View file

@ -52,12 +52,22 @@ namespace spot
std::vector<acc_cond::mark_t> common_out(ns, all);
// Marks that label one incoming transition from the same SCC.
std::vector<acc_cond::mark_t> one_in(ns, 0U);
std::vector<bool> true_state(ns, false);
acc_cond::mark_t true_state_acc = 0U;
unsigned true_state_last;
for (auto& e: old->edges())
for (unsigned d: old->univ_dests(e.dst))
if (si.scc_of(e.src) == si.scc_of(d))
{
common_in[d] &= e.acc;
common_out[e.src] &= e.acc;
if (e.src == e.dst && e.cond == bddtrue
&& old->acc().accepting(e.acc))
{
true_state[d] = true;
true_state_acc = e.acc;
true_state_last = e.src;
}
}
for (unsigned s = 0; s < ns; ++s)
common_out[s] |= common_in[s];
@ -80,13 +90,29 @@ namespace spot
auto new_state =
[&](unsigned state, acc_cond::mark_t m) -> unsigned
{
bool ts = true_state[state];
if (ts)
{
state = true_state_last; // Merge all true states.
m = 0U;
}
pair_t x(state, m);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
unsigned s = res->new_state();
p.first->second = s;
todo.emplace_back(x, s);
if (ts)
{
res->new_edge(s, s, bddtrue, true_state_acc);
// As we do not process all outgoing transition of
// STATE, it is possible that a non-deterministic
// automaton becomes deterministic.
if (res->prop_universal().is_false())
res->prop_universal(trival::maybe());
}
else
todo.emplace_back(x, s);
}
return p.first->second;
};

16
tests/python/dualize.py
View file

@ -401,16 +401,20 @@ assert h == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[0&1] 1
[!0 | !1] 2
State: 1
[0&!1] 2
[!0] 2
State: 1 {0}
[t] 1
State: 2
[t] 2
[0] 2
[!0] 2
--END--"""
aut = spot.automaton("""

70
tests/python/sbacc.py
View file

@ -24,3 +24,73 @@ assert not aut.prop_state_acc().is_true()
aut = spot.sbacc(aut)
assert aut.num_states() == 2
assert aut.prop_state_acc().is_true()
aut = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1] 1
[0&!1] 2
State: 1
[t] 1 {0}
[0] 0
State: 2
[t] 2 {1}
[0] 1
--END--""")
s = spot.sbacc(aut)
h = s.to_str('hoa')
assert h == """HOA: v1
States: 2
Start: 0
AP: 2 "b" "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[1] 1
State: 1 {1}
[t] 1
--END--"""
aut = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1] 1
[0&!1] 2
State: 1
[t] 1 {0 1}
[0] 0
State: 2
[t] 2 {1 0}
[0] 1
--END--""")
d = spot.degeneralize(aut)
h = d.to_str('hoa')
assert h == """HOA: v1
States: 2
Start: 0
AP: 2 "b" "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[1] 1
State: 1 {0}
[t] 1
--END--"""