scc_info: introduce edges_of() and inner_edges_of()
This is motivated by some upcoming patch by Heňo. * spot/twaalgos/sccinfo.hh (edges_of, inner_edges_of): New methods. * spot/twaalgos/sccinfo.cc, spot/twaalgos/strength.cc: Use them. * spot/twa/twagraph.hh (edge_number): Add an overload. * python/spot/impl.i: Bind the new methods. * tests/python/sccinfo.py: Add tests. * NEWS: Mention the changes.
This commit is contained in:
Alexandre Duret-Lutz
parent
e089509a0c
commit
8e19d3f47e
7 changed files with 265 additions and 30 deletions
|
|
@ -294,20 +294,16 @@ namespace spot
|
|||
std::set<acc_cond::mark_t> scc_info::used_acc_of(unsigned scc) const
|
||||
{
|
||||
std::set<acc_cond::mark_t> res;
|
||||
for (auto src: states_of(scc))
|
||||
for (auto& t: aut_->out(src))
|
||||
if (scc_of(t.dst) == scc)
|
||||
res.insert(t.acc);
|
||||
for (auto& t: inner_edges_of(scc))
|
||||
res.insert(t.acc);
|
||||
return res;
|
||||
}
|
||||
|
||||
acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const
|
||||
{
|
||||
acc_cond::mark_t res = 0U;
|
||||
for (auto src: states_of(scc))
|
||||
for (auto& t: aut_->out(src))
|
||||
if (scc_of(t.dst) == scc)
|
||||
res |= t.acc;
|
||||
for (auto& t: inner_edges_of(scc))
|
||||
res |= t.acc;
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
@ -345,9 +341,8 @@ namespace spot
|
|||
bdd scc_info::scc_ap_support(unsigned scc) const
|
||||
{
|
||||
bdd support = bddtrue;
|
||||
for (auto s: states_of(scc))
|
||||
for (auto& t: aut_->out(s))
|
||||
support &= bdd_support(t.cond);
|
||||
for (auto& t: edges_of(scc))
|
||||
support &= bdd_support(t.cond);
|
||||
return support;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -24,6 +24,168 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
class scc_info;
|
||||
|
||||
namespace internal
|
||||
{
|
||||
struct keep_all
|
||||
{
|
||||
template <typename Edge>
|
||||
bool operator()(const Edge&) const noexcept
|
||||
{
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
struct keep_inner_scc
|
||||
{
|
||||
private:
|
||||
const std::vector<unsigned>& sccof_;
|
||||
unsigned desired_scc_;
|
||||
public:
|
||||
keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
|
||||
: sccof_(sccof), desired_scc_(desired_scc)
|
||||
{
|
||||
}
|
||||
|
||||
template <typename Edge>
|
||||
bool operator()(const Edge& ed) const noexcept
|
||||
{
|
||||
return sccof_[ed.dst] == desired_scc_;
|
||||
}
|
||||
};
|
||||
|
||||
template <typename Graph, typename Filter>
|
||||
class SPOT_API scc_edge_iterator
|
||||
{
|
||||
public:
|
||||
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||
const typename Graph::edge_storage_t,
|
||||
typename Graph::edge_storage_t>::type
|
||||
value_type;
|
||||
typedef value_type& reference;
|
||||
typedef value_type* pointer;
|
||||
typedef std::ptrdiff_t difference_type;
|
||||
typedef std::forward_iterator_tag iterator_category;
|
||||
|
||||
typedef std::vector<unsigned>::const_iterator state_iterator;
|
||||
|
||||
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||
const typename Graph::edge_vector_t,
|
||||
typename Graph::edge_vector_t>::type
|
||||
tv_t;
|
||||
|
||||
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||
const typename Graph::state_vector,
|
||||
typename Graph::state_vector>::type
|
||||
sv_t;
|
||||
protected:
|
||||
|
||||
state_iterator pos_;
|
||||
state_iterator end_;
|
||||
unsigned t_;
|
||||
tv_t* tv_;
|
||||
sv_t* sv_;
|
||||
Filter filt_;
|
||||
|
||||
void inc_state_maybe_()
|
||||
{
|
||||
while (!t_ && (++pos_ != end_))
|
||||
t_ = (*sv_)[*pos_].succ;
|
||||
}
|
||||
|
||||
void inc_()
|
||||
{
|
||||
t_ = (*tv_)[t_].next_succ;
|
||||
inc_state_maybe_();
|
||||
}
|
||||
|
||||
public:
|
||||
scc_edge_iterator(state_iterator begin, state_iterator end,
|
||||
tv_t* tv, sv_t* sv, Filter filt) noexcept
|
||||
: pos_(begin), end_(end), tv_(tv), sv_(sv), filt_(filt)
|
||||
{
|
||||
if (pos_ == end_)
|
||||
return;
|
||||
|
||||
t_ = (*sv_)[*pos_].succ;
|
||||
inc_state_maybe_();
|
||||
while (pos_ != end_ && !filt_(**this))
|
||||
inc_();
|
||||
}
|
||||
|
||||
scc_edge_iterator& operator++()
|
||||
{
|
||||
do
|
||||
inc_();
|
||||
while (pos_ != end_ && !filt_(**this));
|
||||
return *this;
|
||||
}
|
||||
|
||||
scc_edge_iterator operator++(int)
|
||||
{
|
||||
scc_edge_iterator old = *this;
|
||||
++*this;
|
||||
return old;
|
||||
}
|
||||
|
||||
bool operator==(scc_edge_iterator o) const
|
||||
{
|
||||
return pos_ == o.pos_ && t_ == o.t_;
|
||||
}
|
||||
|
||||
bool operator!=(scc_edge_iterator o) const
|
||||
{
|
||||
return pos_ != o.pos_ || t_ != o.t_;
|
||||
}
|
||||
|
||||
reference operator*() const
|
||||
{
|
||||
return (*tv_)[t_];
|
||||
}
|
||||
|
||||
pointer operator->() const
|
||||
{
|
||||
return &**this;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
template <typename Graph, typename Filter>
|
||||
class SPOT_API scc_edges
|
||||
{
|
||||
public:
|
||||
typedef scc_edge_iterator<Graph, Filter> iter_t;
|
||||
typedef typename iter_t::tv_t tv_t;
|
||||
typedef typename iter_t::sv_t sv_t;
|
||||
typedef typename iter_t::state_iterator state_iterator;
|
||||
private:
|
||||
state_iterator begin_;
|
||||
state_iterator end_;
|
||||
unsigned t_;
|
||||
tv_t* tv_;
|
||||
sv_t* sv_;
|
||||
Filter filt_;
|
||||
public:
|
||||
|
||||
scc_edges(state_iterator begin, state_iterator end,
|
||||
tv_t* tv, sv_t* sv, Filter filt) noexcept
|
||||
: begin_(begin), end_(end), tv_(tv), sv_(sv), filt_(filt)
|
||||
{
|
||||
}
|
||||
|
||||
iter_t begin() const
|
||||
{
|
||||
return {begin_, end_, tv_, sv_, filt_};
|
||||
}
|
||||
|
||||
iter_t end() const
|
||||
{
|
||||
return {end_, end_, nullptr, nullptr, filt_};
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
/// Storage for SCC related information.
|
||||
class SPOT_API scc_info_node
|
||||
|
|
@ -189,6 +351,37 @@ namespace spot
|
|||
return node(scc).states();
|
||||
}
|
||||
|
||||
/// \brief A fake container to iterate over all edges leaving any
|
||||
/// state of an SCC.
|
||||
///
|
||||
/// The difference with inner_edges_of() is that edges_of() include
|
||||
/// outgoing edges from all the states, even if they leave the SCC.
|
||||
internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
|
||||
edges_of(unsigned scc) const
|
||||
{
|
||||
auto& states = states_of(scc);
|
||||
return {states.begin(), states.end(),
|
||||
&aut_->edge_vector(), &aut_->states(),
|
||||
internal::keep_all()};
|
||||
}
|
||||
|
||||
/// \brief A fake container to iterate over all edges between
|
||||
/// states of an SCC.
|
||||
///
|
||||
/// The difference with edges_of() is that inner_edges_of() ignores
|
||||
/// edges leaving the SCC are ignored.
|
||||
internal::scc_edges<const twa_graph::graph_t, internal::keep_inner_scc>
|
||||
inner_edges_of(unsigned scc) const
|
||||
{
|
||||
if (!aut_->is_existential())
|
||||
throw std::runtime_error
|
||||
("inner_edges_of(): alternating automata are not supported");
|
||||
auto& states = states_of(scc);
|
||||
return {states.begin(), states.end(),
|
||||
&aut_->edge_vector(), &aut_->states(),
|
||||
internal::keep_inner_scc(sccof_, scc)};
|
||||
}
|
||||
|
||||
unsigned one_state_of(unsigned scc) const
|
||||
{
|
||||
return states_of(scc).front();
|
||||
|
|
|
|||
|
|
@ -51,25 +51,24 @@ namespace spot
|
|||
bool first = true;
|
||||
acc_cond::mark_t m = 0U;
|
||||
if (is_weak)
|
||||
for (auto src: si->states_of(i))
|
||||
for (auto& t: aut->out(src))
|
||||
// In case of a universal edge we only need to check
|
||||
// the first destination of an inside the SCC, because
|
||||
// the other have the same t.acc.
|
||||
if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i)
|
||||
{
|
||||
if (first)
|
||||
{
|
||||
first = false;
|
||||
m = t.acc;
|
||||
}
|
||||
else if (m != t.acc)
|
||||
{
|
||||
is_weak = false;
|
||||
if (!inweak)
|
||||
goto exit;
|
||||
}
|
||||
}
|
||||
for (auto& t: si->edges_of(i))
|
||||
// In case of a universal edge we only need to check if
|
||||
// the first destination of an edge is inside the SCC,
|
||||
// because the others have the same t.acc.
|
||||
if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i)
|
||||
{
|
||||
if (first)
|
||||
{
|
||||
first = false;
|
||||
m = t.acc;
|
||||
}
|
||||
else if (m != t.acc)
|
||||
{
|
||||
is_weak = false;
|
||||
if (!inweak)
|
||||
goto exit;
|
||||
}
|
||||
}
|
||||
if (!is_weak && si->is_accepting_scc(i))
|
||||
{
|
||||
assert(inweak);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue