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

@@ -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

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<unsigned int, spot::internal::boxed_label<spot::kripke_graph_state, false> >);
+%fragment(SWIG_Traits_frag(spot::internal::distate_storage<unsigned int, spot::internal::boxed_label<spot::kripke_graph_state, false> >));
 %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> >));
+%traits_swigtype(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<void, true> >);
+%fragment(SWIG_Traits_frag(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<void, true> >));
 
 %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(out, optimal="1") spot::internal::all_trans<spot::digraph<spot::kripke_graph_state, void>> {
+  $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 <spot/kripke/fairkripke.hh>
 %include <spot/kripke/kripke.hh>
 %include <spot/kripke/kripkegraph.hh>
+%template(kripke_graph_state_out) spot::internal::state_out<spot::digraph<spot::kripke_graph_state, void>>;
+%template(kripke_graph_all_trans) spot::internal::all_trans<spot::digraph<spot::kripke_graph_state, void>>;
+%template(kripke_graph_edge_boxed_data) spot::internal::boxed_label<void, true>;
+%template(kripke_graph_edge_storage) spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<void, true> >;
+%template(kripke_graph_state_boxed_data) spot::internal::boxed_label<spot::kripke_graph_state, false>;
+%template(kripke_graph_state_storage) spot::internal::distate_storage<unsigned int, spot::internal::boxed_label<spot::kripke_graph_state, false> >;
+%template(kripke_graph_state_vector) std::vector<spot::internal::distate_storage<unsigned, internal::boxed_label<kripke_graph_state, false>>>;
 
 %include <spot/parseaut/public.hh>
 
@@ -949,6 +966,14 @@ static void* ptr_for_bdddict(PyObject* obj)
    }
 }
 
+%extend spot::internal::state_out<spot::digraph<spot::kripke_graph_state, void>> {
+  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::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
 
   spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >& current()
@@ -966,6 +991,14 @@ static void* ptr_for_bdddict(PyObject* obj)
   }
 }
 
+%extend spot::internal::all_trans<spot::digraph<spot::kripke_graph_state, void>> {
+  swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
+   {
+      return swig::make_forward_iterator(self->begin(), self->begin(),
+				         self->end(), *PYTHON_SELF);
+   }
+}
+
 %extend spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
   swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
    {

spot/kripke/kripkegraph.hh

@@ -152,7 +152,28 @@ namespace spot
   {
   public:
     typedef digraph<kripke_graph_state, void> 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<unsigned, unsigned, unsigned,
+                                         internal::boxed_label
+                                         <void, true>>
+      edge_storage_t;
+    static_assert(std::is_same<typename graph_t::edge_storage_t,
+                  edge_storage_t>::value, "type mismatch");
+
+    typedef internal::distate_storage<unsigned,
+            internal::boxed_label<kripke_graph_state, false>>
+      state_storage_t;
+    static_assert(std::is_same<typename graph_t::state_storage_t,
+                  state_storage_t>::value, "type mismatch");
+    typedef std::vector<state_storage_t> state_vector;
+
+    // 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");
+
   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<const typename graph_t::state_storage_t*>(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<const graph_t>
+    edges() const noexcept
+    {
+      return g_.edges();
+    }
+#endif
+
+    internal::all_trans<graph_t>
+    edges() noexcept
+    {
+      return g_.edges();
+    }
+
+#ifndef SWIG
+    internal::state_out<const graph_t>
+    out(unsigned src) const
+    {
+      return g_.out(src);
+    }
+#endif
+
+    internal::state_out<graph_t>
+    out(unsigned src)
+    {
+      return g_.out(src);
+    }
+
   };
 
   typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;

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
 

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 <http://www.gnu.org/licenses/>.
+
+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