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

is_weak_scc and friend: make them work for alternating automata

Browse source 
* spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh,
spot/twaalgos/mask.cc, spot/twaalgos/mask.hh: Adjust to
work with alternating automata.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh
(determine_unknown_acceptance): Do not complain about
not supporting alternating automata if there is not
indeterminate acceptance.
* spot/twaalgos/stats.cc: Fix a bug were %[iw]c was
read as %[iww]c.
* tests/core/alternating.test: Test is_inherently_weak_scc() and
is_weak_scc().
* python/spot/impl.i: Add missing python bindings
for isweakscc.hh.
This commit is contained in:
Alexandre Duret-Lutz 2017-08-03 18:27:47 +02:00
parent e041db6101
commit 223b0c6a9e
9 changed files with 154 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

2
python/spot/impl.i
View file

@ -143,6 +143,7 @@
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/split.hh>
@ -574,6 +575,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/stats.hh>
%include <spot/twaalgos/isdet.hh>
%include <spot/twaalgos/isunamb.hh>
%include <spot/twaalgos/isweakscc.hh>
%include <spot/twaalgos/simulation.hh>
%include <spot/twaalgos/postproc.hh>
%include <spot/twaalgos/product.hh>

50
spot/twaalgos/isweakscc.cc
View file

@ -23,20 +23,29 @@
namespace spot
{
namespace
{
[[noreturn]] static void
invalid_scc_number(const char* fn)
{
throw std::invalid_argument(std::string(fn) + "(): invalid SCC number");
}
}
bool
scc_has_rejecting_cycle(scc_info& map, unsigned scc)
{
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("scc_has_rejecting_cycle");
auto aut = map.get_aut();
if (!aut->is_existential())
throw std::runtime_error
("scc_has_rejecting_cycle() does not support alternation");
// We check that by cloning the SCC and complementing its
// acceptance condition.
std::vector<bool> keep(aut->num_states(), false);
auto& states = map.states_of(scc);
for (auto s: states)
keep[s] = true;
auto sccaut = mask_keep_accessible_states(aut, keep, states.front());
auto sccaut = mask_keep_accessible_states(aut, keep, states.front(),
/* drop_univ_branch = */ true);
sccaut->set_acceptance(sccaut->acc().num_sets(),
sccaut->get_acceptance().complement());
return !sccaut->is_empty();
@ -45,9 +54,8 @@ namespace spot
bool
is_inherently_weak_scc(scc_info& map, unsigned scc)
{
if (!map.get_aut()->is_existential())
throw std::runtime_error
("is_inherently_weak_scc() does not support alternation");
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("is_inherently_weak_scc");
// Weak SCCs are inherently weak.
if (is_weak_scc(map, scc))
return true;
@ -60,10 +68,8 @@ namespace spot
bool
is_weak_scc(scc_info& map, unsigned scc)
{
if (!map.get_aut()->is_existential())
throw std::runtime_error
("is_weak_scc() does not support alternation");
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("is_weak_scc");
// Rejecting SCCs are weak.
if (map.is_rejecting_scc(scc))
return true;
@ -74,10 +80,9 @@ namespace spot
bool
is_complete_scc(scc_info& map, unsigned scc)
{
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("is_complete_scc");
auto a = map.get_aut();
if (!a->is_existential())
throw std::runtime_error
("is_complete_scc() does not support alternation");
for (auto s: map.states_of(scc))
{
bool has_succ = false;
@ -85,8 +90,16 @@ namespace spot
for (auto& t: a->out(s))
{
has_succ = true;
if (map.scc_of(t.dst) == scc)
sumall |= t.cond;
bool in = true;
for (auto d: a->univ_dests(t.dst))
if (map.scc_of(d) != scc)
{
in = false;
break;
}
if (!in)
continue;
sumall |= t.cond;
if (sumall == bddtrue)
break;
}
@ -99,9 +112,8 @@ namespace spot
bool
is_terminal_scc(scc_info& map, unsigned scc)
{
if (!map.get_aut()->is_existential())
throw std::runtime_error
("is_terminal_scc() does not support alternation");
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("is_terminal_scc");
// If all transitions use all acceptance conditions, the SCC is weak.
return (map.is_accepting_scc(scc)

6
spot/twaalgos/isweakscc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -54,7 +54,9 @@ namespace spot
/// \brief Whether the SCC number \a scc in \a map is complete.
///
/// An SCC is complete iff for all states and all label there exists
/// a transition that stays into this SCC.
/// a transition that stays into this SCC. For this function,
/// universal transitions are considered in the SCC if all there
/// destination are into the SCC.
SPOT_API bool
is_complete_scc(scc_info& map, unsigned scc);

19
spot/twaalgos/mask.cc
View file

@ -69,7 +69,8 @@ namespace spot
twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
std::vector<bool>& to_keep,
unsigned int init)
unsigned int init,
bool drop_univ_branches)
{
if (to_keep.size() < in->num_states())
to_keep.resize(in->num_states(), false);
@ -83,9 +84,21 @@ namespace spot
acc_cond::mark_t&,
unsigned dst)
{
if (!to_keep[src] || !to_keep[dst])
if (!to_keep[src])
{
cond = bddfalse;
return;
}
bool want = false;
for (auto d: in->univ_dests(dst))
if (to_keep[d])
{
want = true;
break;
}
if (!want)
cond = bddfalse;
}, init);
}, init, drop_univ_branches);
return res;
}

50
spot/twaalgos/mask.hh
View file

@ -44,16 +44,16 @@ namespace spot
/// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
/// to retrieve it.
///
/// If \a drop_univ_branches branch is set, universal branching is replaced
/// by existential branching during the copy.
///
/// \param init The optional new initial state.
template<typename Trans>
void transform_accessible(const const_twa_graph_ptr& old,
twa_graph_ptr& cpy,
Trans trans, unsigned int init)
Trans trans, unsigned int init,
bool drop_univ_branches = false)
{
if (!old->is_existential())
throw std::runtime_error
("transform_accessible() does not support alternation");
std::vector<unsigned> todo;
std::vector<unsigned> seen(old->num_states(), -1U);
@ -75,7 +75,27 @@ namespace spot
return tmp;
};
cpy->set_init_state(new_state(init));
// Deal with alternating automata, possibly.
std::map<std::vector<unsigned>, unsigned> uniq;
auto new_univ_state =
[&](unsigned old_state) -> unsigned
{
if (!old->is_univ_dest(old_state))
return new_state(old_state);
std::vector<unsigned> tmp;
for (auto s: old->univ_dests(old_state))
tmp.emplace_back(new_state(s));
std::sort(tmp.begin(), tmp.end());
tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
auto p = uniq.emplace(tmp, 0);
if (p.second)
p.first->second =
cpy->get_graph().new_univ_dests(tmp.begin(), tmp.end());
return p.first->second;
};
cpy->set_init_state(new_univ_state(init));
if (seen[init] != 0)
throw std::runtime_error
("the destination automaton of transform_accessible() should be empty");
@ -93,13 +113,15 @@ namespace spot
bdd cond = t.cond;
acc_cond::mark_t acc = t.acc;
trans(t.src, cond, acc, t.dst);
if (cond != bddfalse)
cpy->new_edge(new_src, new_state(t.dst),
cond, acc);
if (cond == bddfalse)
continue;
if (drop_univ_branches)
for (unsigned d: old->univ_dests(t.dst))
cpy->new_edge(new_src, new_state(d), cond, acc);
else
cpy->new_edge(new_src, new_univ_state(t.dst), cond, acc);
}
}
orig_states->shrink_to_fit();
}
@ -186,9 +208,13 @@ namespace spot
/// will be set to \a init. Only states that are accessible from \a
/// init via states in \a to_keep will be preserved.
///
/// If \a drop_univ_branches branch is set, universal branching is replaced
/// by existential branching during the copy.
///
/// \see mask_keep_states
SPOT_API
twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
std::vector<bool>& to_keep,
unsigned int init);
unsigned int init,
bool drop_univ_branches = false);
}

6
spot/twaalgos/sccinfo.cc
View file

@ -367,15 +367,15 @@ namespace spot
void scc_info::determine_unknown_acceptance()
{
if (!aut_->is_existential())
throw std::runtime_error("scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
std::vector<bool> k;
unsigned n = scc_count();
bool changed = false;
for (unsigned s = 0; s < n; ++s)
if (!is_rejecting_scc(s) && !is_accepting_scc(s))
{
if (!aut_->is_existential())
throw std::runtime_error("scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
auto& node = node_[s];
if (k.empty())
k.resize(aut_->num_states());

62
spot/twaalgos/sccinfo.hh
View file

@ -30,13 +30,15 @@ namespace spot
{
struct keep_all
{
template <typename Edge>
bool operator()(const Edge&) const noexcept
template <typename Iterator>
bool operator()(Iterator, Iterator) const noexcept
{
return true;
}
};
// Keep only transitions that have at least one destination in the
// current SCC.
struct keep_inner_scc
{
private:
@ -48,10 +50,17 @@ namespace spot
{
}
template <typename Edge>
bool operator()(const Edge& ed) const noexcept
template <typename Iterator>
bool operator()(Iterator begin, Iterator end) const noexcept
{
return sccof_[ed.dst] == desired_scc_;
bool want = false;
while (begin != end)
if (sccof_[*begin++] == desired_scc_)
{
want = true;
break;
}
return want;
}
};
@ -79,6 +88,7 @@ namespace spot
const typename Graph::state_vector,
typename Graph::state_vector>::type
sv_t;
typedef const typename Graph::dests_vector_t dv_t;
protected:
state_iterator pos_;
@ -86,6 +96,8 @@ namespace spot
unsigned t_;
tv_t* tv_;
sv_t* sv_;
dv_t* dv_;
Filter filt_;
void inc_state_maybe_()
@ -100,17 +112,28 @@ namespace spot
inc_state_maybe_();
}
bool ignore_current()
{
unsigned dst = (*this)->dst;
if ((int)dst >= 0)
// Non-universal branching => a single destination.
return !filt_(&(*this)->dst, 1 + &(*this)->dst);
// Universal branching => multiple destinations.
const unsigned* d = dv_->data() + ~dst;
return !filt_(d + 1, d + *d + 1);
}
public:
scc_edge_iterator(state_iterator begin, state_iterator end,
tv_t* tv, sv_t* sv, Filter filt) noexcept
: pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), filt_(filt)
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
: pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
{
if (pos_ == end_)
return;
t_ = (*sv_)[*pos_].succ;
inc_state_maybe_();
while (pos_ != end_ && !filt_(**this))
while (pos_ != end_ && ignore_current())
inc_();
}
@ -118,7 +141,7 @@ namespace spot
{
do
inc_();
while (pos_ != end_ && !filt_(**this));
while (pos_ != end_ && ignore_current());
return *this;
}
@ -158,29 +181,31 @@ namespace spot
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::dv_t dv_t;
typedef typename iter_t::state_iterator state_iterator;
private:
state_iterator begin_;
state_iterator end_;
tv_t* tv_;
sv_t* sv_;
dv_t* dv_;
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)
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
: begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
{
}
iter_t begin() const
{
return {begin_, end_, tv_, sv_, filt_};
return {begin_, end_, tv_, sv_, dv_, filt_};
}
iter_t end() const
{
return {end_, end_, nullptr, nullptr, filt_};
return {end_, end_, nullptr, nullptr, nullptr, filt_};
}
};
}
@ -408,23 +433,24 @@ namespace spot
auto& states = states_of(scc);
return {states.begin(), states.end(),
&aut_->edge_vector(), &aut_->states(),
&aut_->get_graph().dests_vector(),
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.
/// The difference with edges_of() is that inner_edges_of()
/// ignores edges leaving the SCC are ignored. In the case of
/// alternating automaton, an edge is considered to be part of the
/// SCC of one of its destination is in the SCC.
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(),
&aut_->get_graph().dests_vector(),
internal::keep_inner_scc(sccof_, scc)};
}

18
spot/twaalgos/stats.cc
View file

@ -256,15 +256,25 @@ namespace spot
break;
case 'i':
if (pos[1] == 'w')
inherently_weak = true;
{
inherently_weak = true;
++pos;
}
else
error(std::string(pos, pos + 2));
{
error(std::string(pos, pos + 2));
}
break;
case 'I':
if (pos[1] == 'W')
non_inherently_weak = true;
{
non_inherently_weak = true;
++pos;
}
else
error(std::string(pos, pos + 2));
{
error(std::string(pos, pos + 2));
}
break;
case ' ':
case '\t':

2
tests/core/alternating.test
View file

@ -1840,6 +1840,7 @@ State: 2 "t"
EOF
autfilt --tgba in 2>out && exit 1
grep 'autfilt.*weak.*alternating' out
test '0 2 2 1' = "`autfilt --stats='%[Wiw]c %[w]c %[iw]c %[W]c' in`"
cat >in <<EOF
HOA: v1
@ -1860,3 +1861,4 @@ State: 3 /*{0}*/
EOF
autfilt --tgba in 2>out && exit 1
grep 'autfilt.*weak.*alternating' out
test '2 0 2 2' = "`autfilt --stats='%[Wiw]c %[w]c %[iw]c %[W]c' in`"