diff --git a/python/spot/impl.i b/python/spot/impl.i index 96c821462..6affd03f8 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -182,7 +182,6 @@ namespace swig typedef OutIterator out_iterator; typedef ValueType value_type; typedef SwigPyIterator_T base; - typedef ForwardIterator_T 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 inline SwigPyIterator* make_forward_iterator(const OutIter& current, @@ -228,6 +228,64 @@ namespace swig { return new ForwardIterator_T(current, begin, end, seq); } + + // Likewise, but without returning a pointer. + template::value_type, + typename FromOper = from_oper > + class ForwardIterator_T_NP : public SwigPyIterator_T + { + public: + FromOper from; + typedef OutIterator out_iterator; + typedef ValueType value_type; + typedef SwigPyIterator_T base; + + ForwardIterator_T_NP(out_iterator curr, out_iterator first, + out_iterator last, PyObject *seq) + : SwigPyIterator_T(curr, seq), begin(first), end(last) + { + } + + PyObject *value() const { + if (base::current == end) { + throw stop_iteration(); + } else { + return from(static_cast(*(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 + inline SwigPyIterator* + make_forward_iterator_np(const OutIter& current, + const OutIter& begin, + const OutIter& end, PyObject *seq = 0) + { + return new ForwardIterator_T_NP(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 >); %fragment(SWIG_Traits_frag(spot::internal::edge_storage >)); -%typemap(out, optimal="1") spot::internal::state_out> { +%typemap(out, optimal="1") spot::internal::all_trans> { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, SWIG_POINTER_OWN); } -%typemap(edges, optimal="1") spot::internal::all_trans> { +%typemap(out, optimal="1") spot::internal::const_universal_dests { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, - SWIG_POINTER_OWN); + SWIG_POINTER_OWN); } -%noexception spot::twa_graph::out; %noexception spot::twa_graph::edges; -%include +%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 %template(twa_graph_state_out) spot::internal::state_out>; %template(twa_graph_all_trans) spot::internal::all_trans>; %template(twa_graph_edge_boxed_data) spot::internal::boxed_label; @@ -645,7 +730,6 @@ namespace std { } } - %extend spot::internal::state_out> { 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& 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__() { diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 6ee124266..c1963ca56 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -172,10 +172,16 @@ namespace spot { public: typedef digraph 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> + edge_storage_t; + static_assert(std::is_same::value, "type mismatch"); + // We avoid using graph_t::state for the very same reason. typedef unsigned state_num; static_assert(std::is_same::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(&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; - ss << n; + 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(); } @@ -377,13 +413,13 @@ namespace spot } unsigned new_edge(unsigned src, unsigned dst, - bdd cond, acc_cond::mark_t acc = 0U) + bdd cond, acc_cond::mark_t acc = 0U) { return g_.new_edge(src, dst, cond, acc); } unsigned new_acc_edge(unsigned src, unsigned dst, - bdd cond, bool acc = true) + bdd cond, bool acc = true) { if (acc) return g_.new_edge(src, dst, cond, this->acc().all_sets()); @@ -391,6 +427,19 @@ namespace spot return g_.new_edge(src, dst, cond); } + template + 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 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 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 - edges() const + edges() const noexcept { return g_.edges(); } #endif internal::all_trans - 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&& newst, unsigned used_states); diff --git a/tests/Makefile.am b/tests/Makefile.am index 6f11509f6..c4df74f53 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/alternating.py b/tests/python/alternating.py new file mode 100755 index 000000000..20015e079 --- /dev/null +++ b/tests/python/alternating.py @@ -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 . + +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