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

scc_info: keep track of common acceptance sets

Browse source 
* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Do it.
* tests/core/sccdot.test: Add a test case.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2017-05-31 12:16:04 +02:00
parent 78add1d44b
commit 617a7187b3
4 changed files with 62 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -88,6 +88,11 @@ New in spot 2.3.4.dev (not yet released)
- spot::scc_info can now be passed a filter function to ignore
or cut some edges.
- spot::scc_info now keeps track of acceptance sets that are common
to all edges in an SCC. These can be retrieved using
scc_info::common_sets_of(scc), and they are used by scc_info to
classify some SCCs as rejecting more easily.
Python:
- The 'spot.gen' package exports the functions from libspotgen.

56
spot/twaalgos/sccinfo.cc
View file

@ -40,7 +40,8 @@ namespace spot
}
acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition
acc_cond::mark_t acc = 0U; // union of all acceptance sets in the SCC
acc_cond::mark_t acc = 0U; // union of all acceptance marks in the SCC
acc_cond::mark_t common = -1U; // intersection of all marks in the SCC
int index; // Index of the SCC
bool trivial = true; // Whether the SCC has no cycle
bool accepting = false; // Necessarily accepting
@ -130,9 +131,10 @@ namespace spot
if (root_.back().index == h_[curr])
{
unsigned num = node_.size();
auto acc = root_.back().acc;
acc_cond::mark_t acc = root_.back().acc;
acc_cond::mark_t common = root_.back().common;
bool triv = root_.back().trivial;
node_.emplace_back(acc, triv);
node_.emplace_back(acc, common, triv);
// Move all elements of this SCC from the live stack
// to the the node.
@ -176,33 +178,8 @@ namespace spot
succ.insert(succ.end(), dests.begin(), dests.end());
bool accept = !triv && root_.back().accepting;
node_.back().accepting_ = accept;
bool reject = triv || !aut->acc().inf_satisfiable(acc);
// If the SCC acceptance is indeterminate, but has
// only self-loops with the same mark, it is
// necessarily rejecting, otherwise we would have
// found it to be accepting.
if (!accept && !reject && nbs.size() == 1)
{
acc_cond::mark_t selfacc = 0;
bool first = true;
reject = true;
for (const auto& e: aut->out(nbs.front()))
for (unsigned d: aut->univ_dests(e))
if (e.src == d)
{
if (first)
{
selfacc = e.acc;
first = false;
}
else if (selfacc != e.acc)
{
reject = false;
goto break2;
}
}
}
break2:
bool reject = triv ||
aut->acc().maybe_accepting(acc, common).is_false();
node_.back().rejecting_ = reject;
root_.pop_back();
}
@ -250,7 +227,7 @@ namespace spot
continue;
}
auto acc = e.acc;
acc_cond::mark_t acc = e.acc;
// Are we going to a new state?
int spi = h_[dest];
@ -288,11 +265,15 @@ namespace spot
if (dest == e.src)
is_accepting = aut->acc().accepting(acc);
acc_cond::mark_t common = acc;
assert(!root_.empty());
while (threshold > root_.back().index)
{
acc |= root_.back().acc;
acc |= root_.back().in_acc;
acc_cond::mark_t in_acc = root_.back().in_acc;
acc |= in_acc;
common &= root_.back().common;
common &= in_acc;
is_accepting |= root_.back().accepting;
root_.pop_back();
assert(!root_.empty());
@ -303,9 +284,8 @@ namespace spot
// after this loop, the SCC whose index is threshold might have
// been merged with a higher SCC.
// Accumulate all acceptance conditions, states, SCC
// successors, and conditions into the merged SCC.
root_.back().acc |= acc;
root_.back().common &= common;
root_.back().accepting |= is_accepting
|| aut->acc().accepting(root_.back().acc);
// This SCC is no longer trivial.
@ -346,14 +326,6 @@ namespace spot
return res;
}
acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const
{
acc_cond::mark_t res = 0U;
for (auto& t: inner_edges_of(scc))
res |= t.acc;
return res;
}
std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
{
unsigned n = aut_->num_states();

25
spot/twaalgos/sccinfo.hh
View file

@ -195,6 +195,7 @@ namespace spot
protected:
scc_succs succ_;
acc_cond::mark_t acc_;
acc_cond::mark_t common_;
std::vector<unsigned> states_; // States of the component
bool trivial_:1;
bool accepting_:1; // Necessarily accepting
@ -207,8 +208,10 @@ namespace spot
{
}
scc_info_node(acc_cond::mark_t acc, bool trivial):
acc_(acc), trivial_(trivial), accepting_(false),
scc_info_node(acc_cond::mark_t acc,
acc_cond::mark_t common, bool trivial):
acc_(acc), common_(common),
trivial_(trivial), accepting_(false),
rejecting_(false), useful_(false)
{
}
@ -246,6 +249,11 @@ namespace spot
return acc_;
}
acc_cond::mark_t common_marks() const
{
return common_;
}
const std::vector<unsigned>& states() const
{
return states_;
@ -477,7 +485,18 @@ namespace spot
std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
acc_cond::mark_t acc_sets_of(unsigned scc) const;
/// sets that contain at least one transition of the SCC
acc_cond::mark_t acc_sets_of(unsigned scc) const
{
// FIXME: Why do we have two name for this method?
return acc(scc);
}
/// sets that contain the entire SCC
acc_cond::mark_t common_sets_of(unsigned scc) const
{
return node(scc).common_marks();
}
std::vector<bool> weak_sccs() const;

22
tests/core/sccdot.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement de
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement de
# l'Epita
#
# This file is part of Spot, a model checking library.
@ -186,3 +186,23 @@ State: 7
--END--
EOF
diff expected.hoa out.hoa
cat >input <<'EOF'
HOA: v1
States: 2
Start: 0&1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 2 Inf(0) & Fin(1)
--BODY--
State: 0 {0 1}
[0&1] 0
[!0&1] 1
State: 1 {0 1}
[0&!1] 0
[!0&!1] 1
--END--
EOF
# This has one useless component
autfilt --dot=s input | grep grey