From eb02db85daa6b5d69a1f93113abd4dbf58c05ca0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Feb 2019 21:56:15 +0100 Subject: [PATCH] python: improve kripke_graph bindings Related to issue #376. * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the benefit of Swig. * python/spot/impl.i: Add bindings for iterators over kripke_graph states and edges. * tests/python/kripke.py: New file. * tests/Makefile.am: Add it. * NEWS: Update. --- NEWS | 6 +++ python/spot/impl.i | 33 +++++++++++++++++ spot/kripke/kripkegraph.hh | 75 +++++++++++++++++++++++++++++++++++--- tests/Makefile.am | 3 +- tests/python/kripke.py | 75 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 185 insertions(+), 7 deletions(-) create mode 100644 tests/python/kripke.py diff --git a/NEWS b/NEWS index f8102a861..3f2bd9cfc 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ New in spot 2.7.1.dev (not yet released) + Python: + + - Improved support for explicit Kripke structure. It is now + possible to iterate over a kripke_graph object in a way similar to + twa_graph. + Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that diff --git a/python/spot/impl.i b/python/spot/impl.i index 38bdeb916..c8b86a160 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -549,19 +549,29 @@ namespace std { %nodefaultctor spot::internal::killer_edge_iterator; %nodefaultctor spot::internal::all_trans; %nodefaultctor spot::internal::universal_dests; +%traits_swigtype(spot::internal::distate_storage >); +%fragment(SWIG_Traits_frag(spot::internal::distate_storage >)); %traits_swigtype(spot::internal::edge_storage >); %fragment(SWIG_Traits_frag(spot::internal::edge_storage >)); +%traits_swigtype(spot::internal::edge_storage >); +%fragment(SWIG_Traits_frag(spot::internal::edge_storage >)); %typemap(out, optimal="1") spot::internal::all_trans> { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, SWIG_POINTER_OWN); } +%typemap(out, optimal="1") spot::internal::all_trans> { + $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, + SWIG_POINTER_OWN); +} + %typemap(out, optimal="1") spot::internal::const_universal_dests { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, SWIG_POINTER_OWN); } +%noexception spot::kripke_graph::edges; %noexception spot::twa_graph::edges; %noexception spot::twa_graph::univ_dests; @@ -681,6 +691,13 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%template(kripke_graph_state_out) spot::internal::state_out>; +%template(kripke_graph_all_trans) spot::internal::all_trans>; +%template(kripke_graph_edge_boxed_data) spot::internal::boxed_label; +%template(kripke_graph_edge_storage) spot::internal::edge_storage >; +%template(kripke_graph_state_boxed_data) spot::internal::boxed_label; +%template(kripke_graph_state_storage) spot::internal::distate_storage >; +%template(kripke_graph_state_vector) std::vector>>; %include @@ -949,6 +966,14 @@ static void* ptr_for_bdddict(PyObject* obj) } } +%extend spot::internal::state_out> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + %extend spot::internal::killer_edge_iterator> { spot::internal::edge_storage >& current() @@ -966,6 +991,14 @@ static void* ptr_for_bdddict(PyObject* obj) } } +%extend spot::internal::all_trans> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + %extend spot::internal::all_trans> { swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) { diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh index a8bde37a0..348e1ccf5 100644 --- a/spot/kripke/kripkegraph.hh +++ b/spot/kripke/kripkegraph.hh @@ -152,7 +152,28 @@ namespace spot { public: typedef digraph graph_t; - typedef graph_t::edge_storage_t edge_storage_t; + // 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::edge_storage_t as an abstract type. + typedef internal::edge_storage> + edge_storage_t; + static_assert(std::is_same::value, "type mismatch"); + + typedef internal::distate_storage> + state_storage_t; + static_assert(std::is_same::value, "type mismatch"); + typedef std::vector state_vector; + + // We avoid using graph_t::state for the very same reason. + typedef unsigned state_num; + static_assert(std::is_same::value, + "type mismatch"); + protected: graph_t g_; mutable unsigned init_number_; @@ -177,7 +198,7 @@ namespace spot return g_.num_edges(); } - void set_init_state(graph_t::state s) + void set_init_state(state_num s) { if (SPOT_UNLIKELY(s >= num_states())) throw std::invalid_argument @@ -185,7 +206,7 @@ namespace spot init_number_ = s; } - graph_t::state get_init_state_number() const + state_num get_init_state_number() const { // If the kripke has no state, it has no initial state. if (num_states() == 0) @@ -218,7 +239,7 @@ namespace spot } - graph_t::state + state_num state_number(const state* st) const { auto s = down_cast(st); @@ -226,13 +247,13 @@ namespace spot } const kripke_graph_state* - state_from_number(graph_t::state n) const + state_from_number(state_num n) const { return &g_.state_data(n); } kripke_graph_state* - state_from_number(graph_t::state n) + state_from_number(state_num n) { return &g_.state_data(n); } @@ -282,6 +303,48 @@ namespace spot { return g_.new_edge(src, dst); } + + +#ifndef SWIG + const state_vector& states() const + { + return g_.states(); + } +#endif + + state_vector& states() + { + return g_.states(); + } + +#ifndef SWIG + internal::all_trans + edges() const noexcept + { + return g_.edges(); + } +#endif + + internal::all_trans + edges() noexcept + { + return g_.edges(); + } + +#ifndef SWIG + internal::state_out + out(unsigned src) const + { + return g_.out(src); + } +#endif + + internal::state_out + out(unsigned src) + { + return g_.out(src); + } + }; typedef std::shared_ptr kripke_graph_ptr; diff --git a/tests/Makefile.am b/tests/Makefile.am index 2f42108f7..4b332e243 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -372,7 +372,6 @@ TESTS_python = \ python/bugdet.py \ python/complement_semidet.py \ python/declenv.py \ - python/_word.ipynb \ python/decompose_scc.py \ python/dualize.py \ python/except.py \ @@ -380,6 +379,7 @@ TESTS_python = \ python/genem.py \ python/implies.py \ python/interdep.py \ + python/kripke.py \ python/ltl2tgba.test \ python/ltlf.py \ python/ltlparse.py \ @@ -417,6 +417,7 @@ TESTS_python = \ python/tra2tba.py \ python/twagraph.py \ python/toweak.py \ + python/_word.ipynb \ $(TESTS_ipython) endif diff --git a/tests/python/kripke.py b/tests/python/kripke.py new file mode 100644 index 000000000..30f07a81f --- /dev/null +++ b/tests/python/kripke.py @@ -0,0 +1,75 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# 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 +bdict = spot.make_bdd_dict() +k = spot.make_kripke_graph(bdict) +p1 = buddy.bdd_ithvar(k.register_ap("p1")) +p2 = buddy.bdd_ithvar(k.register_ap("p2")) +cond1 = p1 & p2 +cond2 = p1 & -p2 +cond3 = -p1 & -p2 +s2 = k.new_state(cond1) +s1 = k.new_state(cond2) +s3 = k.new_state(cond3) +k.new_edge(s1, s2) +k.new_edge(s2, s2) +k.new_edge(s1, s3) +k.new_edge(s3, s3) +k.new_edge(s3, s2) +k.set_init_state(s1) + +hoa="""HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p2" +acc-name: all +Acceptance: 0 t +properties: state-labels explicit-labels state-acc +--BODY-- +State: [0&!1] 0 "1" +1 2 +State: [0&1] 1 "0" +1 +State: [!0&!1] 2 "2" +2 1 +--END--""" +assert hoa == k.to_str('HOA') +assert k.num_states() == 3 +assert k.num_edges() == 5 + +res = [] +for e in k.out(s1): + res.append((e.src, e.dst)) +assert res == [(1, 0), (1, 2)] + +res = [] +for e in k.edges(): + res.append((e.src, e.dst)) +assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)] + +res = [] +for s in k.states(): + res.append(s.cond()) +assert res == [cond1, cond2, cond3] + +assert k.states()[0].cond() == cond1 +assert k.states()[1].cond() == cond2 +assert k.states()[2].cond() == cond3