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

twa_graph: add basic support for alternation

Browse source 
This only allows creating universal edges, and reading the associated
destinations.

* spot/twa/twagraph.hh (new_univ_edges, univ_dests, is_alternating): New
function.
* python/spot/impl.i: Add Python bindings.
* tests/python/alternating.py: New file.
* tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-24 17:56:59 +01:00
parent 4903f086e3
commit 6aad559c29
4 changed files with 253 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

123
python/spot/impl.i
View file

@ -182,7 +182,6 @@ namespace swig
typedef OutIterator out_iterator;
typedef ValueType value_type;
typedef SwigPyIterator_T<out_iterator> base;
typedef ForwardIterator_T<OutIterator, ValueType, FromOper> self_type;
ForwardIterator_T(out_iterator curr, out_iterator first,
out_iterator last, PyObject *seq)
@ -200,7 +199,7 @@ namespace swig
SwigPyIterator *copy() const
{
return new self_type(*this);
return new ForwardIterator_T(*this);
}
SwigPyIterator *incr(size_t n = 1)
@ -215,11 +214,12 @@ namespace swig
return this;
}
private:
protected:
out_iterator begin;
out_iterator end;
};
template<typename OutIter>
inline SwigPyIterator*
make_forward_iterator(const OutIter& current,
@ -228,6 +228,64 @@ namespace swig
{
return new ForwardIterator_T<OutIter>(current, begin, end, seq);
}
// Likewise, but without returning a pointer.
template<typename OutIterator,
typename ValueType =
typename std::iterator_traits<OutIterator>::value_type,
typename FromOper = from_oper<ValueType> >
class ForwardIterator_T_NP : public SwigPyIterator_T<OutIterator>
{
public:
FromOper from;
typedef OutIterator out_iterator;
typedef ValueType value_type;
typedef SwigPyIterator_T<out_iterator> base;
ForwardIterator_T_NP(out_iterator curr, out_iterator first,
out_iterator last, PyObject *seq)
: SwigPyIterator_T<OutIterator>(curr, seq), begin(first), end(last)
{
}
PyObject *value() const {
if (base::current == end) {
throw stop_iteration();
} else {
return from(static_cast<value_type>(*(base::current)));
}
}
SwigPyIterator *copy() const
{
return new ForwardIterator_T_NP(*this);
}
SwigPyIterator *incr(size_t n = 1)
{
while (n--) {
if (base::current == end) {
throw stop_iteration();
} else {
++base::current;
}
}
return this;
}
protected:
out_iterator begin;
out_iterator end;
};
template<typename OutIter>
inline SwigPyIterator*
make_forward_iterator_np(const OutIter& current,
const OutIter& begin,
const OutIter& end, PyObject *seq = 0)
{
return new ForwardIterator_T_NP<OutIter>(current, begin, end, seq);
}
}
}
%fragment("ForwardIterator_T");
@ -398,23 +456,50 @@ namespace std {
%nodefaultctor spot::digraph;
%nodefaultctor spot::internal::state_out;
%nodefaultctor spot::internal::all_trans;
%nodefaultctor spot::internal::universal_dests;
%traits_swigtype(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >);
%fragment(SWIG_Traits_frag(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >));
%typemap(out, optimal="1") spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
%typemap(out, optimal="1") spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
$result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor,
SWIG_POINTER_OWN);
}
%typemap(edges, optimal="1") spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
%typemap(out, optimal="1") spot::internal::const_universal_dests {
$result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor,
SWIG_POINTER_OWN);
}
%noexception spot::twa_graph::out;
%noexception spot::twa_graph::edges;
%include <spot/twa/twagraph.hh>
%noexception spot::twa_graph::univ_dests;
// Instead of %feature("shadow") we would like to use just
// %pythonprepend spot::twa_graph::out %{ self.report_univ_dest(src) %}
// However Swig 3.0.2 (from Debian stable) names the argument "*args"
// while Swig 3.0.10 uses "src", and we want to be compatible with both.
%feature("shadow") spot::twa_graph::out %{
def out(self, src: 'unsigned int'):
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_from_number %{
def state_from_number(self, s: 'unsigned int') -> "spot::twa_graph_state const *":
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_acc_sets %{
def state_acc_sets(self, s: 'unsigned int') -> "spot::acc_cond::mark_t":
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_is_accepting %{
def state_is_accepting(self, src) -> "bool":
if type(src) == int:
self.report_univ_dest(src)
return $action(self, src)
%}
%include <spot/twa/twagraph.hh>
%template(twa_graph_state_out) spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
%template(twa_graph_all_trans) spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
%template(twa_graph_edge_boxed_data) spot::internal::boxed_label<spot::twa_graph_edge_data, false>;
@ -645,7 +730,6 @@ namespace std {
}
}
%extend spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
@ -662,6 +746,29 @@ namespace std {
}
}
%extend spot::internal::const_universal_dests {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
return swig::make_forward_iterator_np(self->begin(), self->begin(),
self->end(), *PYTHON_SELF);
}
}
%extend spot::twa_graph {
unsigned new_univ_edge(unsigned src, const std::vector<unsigned>& v,
bdd cond, acc_cond::mark_t acc = 0U)
{
return self->new_univ_edge(src, v.begin(), v.end(), cond, acc);
}
void report_univ_dest(unsigned src)
{
if (self->is_univ_dest(src))
throw std::runtime_error
("universal destinations should be explored with univ_dest()");
}
}
%extend spot::acc_cond::acc_code {
std::string __repr__()
{

91
spot/twa/twagraph.hh
View file

@ -172,10 +172,16 @@ namespace spot
{
public:
typedef digraph<twa_graph_state, twa_graph_edge_data> graph_t;
typedef graph_t::edge_storage_t edge_storage_t;
// We avoid using graph_t::state because graph_t is not
// We avoid using graph_t::edge_storage_t because graph_t is not
// instantiated in the SWIG bindings, and SWIG would therefore
// handle graph_t::state as an abstract type.
// handle graph_t::edge_storage_t as an abstract type.
typedef spot::internal::edge_storage<unsigned, unsigned, unsigned,
internal::boxed_label
<twa_graph_edge_data, false>>
edge_storage_t;
static_assert(std::is_same<typename graph_t::edge_storage_t,
edge_storage_t>::value, "type mismatch");
// We avoid using graph_t::state for the very same reason.
typedef unsigned state_num;
static_assert(std::is_same<typename graph_t::state, state_num>::value,
"type mismatch");
@ -272,7 +278,11 @@ namespace spot
virtual const twa_graph_state* get_init_state() const override
{
return state_from_number(get_init_state_number());
unsigned n = get_init_state_number();
if (SPOT_UNLIKELY(is_univ_dest(n)))
throw std::runtime_error
("get_init_state() does not work with universal initial states");
return state_from_number(n);
}
virtual twa_succ_iterator*
@ -293,6 +303,18 @@ namespace spot
return new twa_graph_succ_iterator<graph_t>(&g_, s->succ);
}
static constexpr bool is_univ_dest(const edge_storage_t& e)
{
return is_univ_dest(e.dst);
}
static constexpr bool is_univ_dest(unsigned s)
{
// Universal destinations are stored with their most-significant
// bit set.
return (int) s < 0;
}
state_num
state_number(const state* st) const
{
@ -310,7 +332,21 @@ namespace spot
std::string format_state(unsigned n) const
{
std::stringstream ss;
if (is_univ_dest(n))
{
bool notfirst = false;
for (unsigned d: univ_dests(n))
{
if (notfirst)
ss << '&';
notfirst = true;
ss << d;
}
}
else
{
ss << n;
}
return ss.str();
}
@ -391,6 +427,19 @@ namespace spot
return g_.new_edge(src, dst, cond);
}
template<class I>
unsigned new_univ_edge(unsigned src, I begin, I end,
bdd cond, acc_cond::mark_t acc = 0U)
{
return g_.new_univ_edge(src, begin, end, cond, acc);
}
unsigned new_univ_edge(unsigned src, std::initializer_list<unsigned> dst,
bdd cond, acc_cond::mark_t acc = 0U)
{
return g_.new_univ_edge(src, dst.begin(), dst.end(), cond, acc);
}
#ifndef SWIG
internal::state_out<const graph_t>
out(unsigned src) const
@ -405,6 +454,23 @@ namespace spot
return g_.out(src);
}
internal::const_universal_dests
univ_dests(unsigned d) const noexcept
{
return g_.univ_dests(d);
}
internal::const_universal_dests
univ_dests(const edge_storage_t& e) const noexcept
{
return g_.univ_dests(e);
}
bool is_alternating() const
{
return g_.is_alternating();
}
#ifndef SWIG
auto states() const
SPOT_RETURN(g_.states());
@ -412,14 +478,14 @@ namespace spot
SPOT_RETURN(g_.states());
internal::all_trans<const graph_t>
edges() const
edges() const noexcept
{
return g_.edges();
}
#endif
internal::all_trans<graph_t>
edges()
edges() noexcept
{
return g_.edges();
}
@ -473,7 +539,6 @@ namespace spot
throw std::runtime_error
("state_acc_sets() should only be called on "
"automata with state-based acceptance");
for (auto& t: g_.out(s))
// Stop at the first edge, since the remaining should be
// labeled identically.
@ -501,14 +566,20 @@ namespace spot
bool operator==(const twa_graph& aut) const
{
auto& dests1 = g_.dests_vector();
auto& dests2 = aut.get_graph().dests_vector();
if (num_states() != aut.num_states() ||
num_edges() != aut.num_edges() ||
num_sets() != aut.num_sets())
num_sets() != aut.num_sets() ||
dests1.size() != dests2.size())
return false;
auto& trans1 = edge_vector();
auto& trans2 = aut.edge_vector();
return std::equal(trans1.begin() + 1, trans1.end(),
trans2.begin() + 1);
if (!std::equal(trans1.begin() + 1, trans1.end(),
trans2.begin() + 1))
return false;
return std::equal(dests1.begin(), dests1.end(),
dests2.begin());
}
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);

1
tests/Makefile.am
View file

@ -324,6 +324,7 @@ TESTS_python = \
python/_aux.ipynb \
python/accparse2.py \
python/alarm.py \
python/alternating.py \
python/bddnqueen.py \
python/bugdet.py \
python/implies.py \

52
tests/python/alternating.py Executable file
View file

@ -0,0 +1,52 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
import spot
import buddy
aut = spot.make_twa_graph(spot._bdd_dict)
p1 = buddy.bdd_ithvar(aut.register_ap("p1"))
p2 = buddy.bdd_ithvar(aut.register_ap("p2"))
m = aut.set_buchi()
aut.new_states(3)
aut.set_init_state(0)
aut.new_univ_edge(0, [1, 2], p1, m)
aut.new_univ_edge(0, [0, 1], p2)
aut.new_univ_edge(1, [0, 2, 1], p1 & p2)
aut.new_edge(2, 2, p1 | p2)
tr = [(s, [[x for x in aut.univ_dests(i)] for i in aut.out(s)])
for s in range(3)]
print(tr)
assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr
assert aut.is_alternating()
received = False
try:
for i in aut.out(0):
for j in aut.out(i.dst):
pass
except RuntimeError:
received = True
assert received