From 5445007070c8afa5cb24e79955f6eb811066158f Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Wed, 15 Mar 2017 16:21:33 +0100
Subject: [PATCH] ltsmin: extract spins interface

* spot/ltsmin/Makefile.am, spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh,
spot/ltsmin/spins_interface.hh: here.
---
 spot/ltsmin/Makefile.am        |  2 +-
 spot/ltsmin/ltsmin.cc          | 39 ---------------------
 spot/ltsmin/ltsmin.hh          |  4 +--
 spot/ltsmin/spins_interface.hh | 62 ++++++++++++++++++++++++++++++++++
 4 files changed, 65 insertions(+), 42 deletions(-)
 create mode 100644 spot/ltsmin/spins_interface.hh

diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am
index 6f3b6ae3d..42dc9e62a 100644
--- a/spot/ltsmin/Makefile.am
+++ b/spot/ltsmin/Makefile.am
@@ -24,7 +24,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 ltsmindir = $(pkgincludedir)/ltsmin
 
-ltsmin_HEADERS = ltsmin.hh
+ltsmin_HEADERS = ltsmin.hh spins_interface.hh
 
 lib_LTLIBRARIES = libspotltsmin.la
 libspotltsmin_la_DEPENDENCIES = \
diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc
index 206d9f886..5b518ebc9 100644
--- a/spot/ltsmin/ltsmin.cc
+++ b/spot/ltsmin/ltsmin.cc
@@ -55,45 +55,6 @@ namespace spot
 {
   namespace
   {
-    ////////////////////////////////////////////////////////////////////////
-    // spins interface
-
-    typedef struct transition_info {
-      int* labels; // edge labels, NULL, or pointer to the edge label(s)
-      int  group;  // holds transition group or -1 if unknown
-    } transition_info_t;
-
-    typedef void (*TransitionCB)(void *ctx,
-                                 transition_info_t *transition_info,
-                                 int *dst);
-  }
-
-  struct spins_interface
-  {
-    lt_dlhandle handle;        // handle to the dynamic library
-    void (*get_initial_state)(void *to);
-    int (*have_property)();
-    int (*get_successors)(void* m, int *in, TransitionCB, void *arg);
-    int (*get_state_size)();
-    const char* (*get_state_variable_name)(int var);
-    int (*get_state_variable_type)(int var);
-    int (*get_type_count)();
-    const char* (*get_type_name)(int type);
-    int (*get_type_value_count)(int type);
-    const char* (*get_type_value_name)(int type, int value);
-
-    ~spins_interface()
-    {
-      if (handle)
-        lt_dlclose(handle);
-      lt_dlexit();
-    }
-  };
-
-  namespace
-  {
-    typedef std::shared_ptr<const spins_interface> spins_interface_ptr;
-
     ////////////////////////////////////////////////////////////////////////
     // STATE
 
diff --git a/spot/ltsmin/ltsmin.hh b/spot/ltsmin/ltsmin.hh
index da787c631..dc54ee1a2 100644
--- a/spot/ltsmin/ltsmin.hh
+++ b/spot/ltsmin/ltsmin.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2016, 2019 Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2016, 2017, 2019 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -19,6 +19,7 @@
 
 #pragma once
 
+#include <spot/ltsmin/spins_interface.hh>
 #include <spot/kripke/kripke.hh>
 #include <spot/twacube/twacube.hh>
 #include <spot/tl/apcollect.hh>
@@ -27,7 +28,6 @@
 
 namespace spot
 {
-  struct spins_interface;
   class cspins_iterator;
   typedef int* cspins_state;
 
diff --git a/spot/ltsmin/spins_interface.hh b/spot/ltsmin/spins_interface.hh
new file mode 100644
index 000000000..f77f87aca
--- /dev/null
+++ b/spot/ltsmin/spins_interface.hh
@@ -0,0 +1,62 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 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/>.
+
+#pragma once
+
+#include <ltdl.h>
+#include <memory>
+namespace spot
+{
+  ////////////////////////////////////////////////////////////////////////
+  // spins interface
+
+  typedef struct transition_info
+  {
+    int* labels; // edge labels, NULL, or pointer to the edge label(s)
+    int  group;  // holds transition group or -1 if unknown
+  } transition_info_t;
+
+  typedef void (*TransitionCB)(void *ctx,
+                               transition_info_t *transition_info,
+                               int *dst);
+
+  struct spins_interface
+  {
+    lt_dlhandle handle;        // handle to the dynamic library
+    void (*get_initial_state)(void *to);
+    int (*have_property)();
+    int (*get_successors)(void* m, int *in, TransitionCB, void *arg);
+    int (*get_state_size)();
+    const char* (*get_state_variable_name)(int var);
+    int (*get_state_variable_type)(int var);
+    int (*get_type_count)();
+    const char* (*get_type_name)(int type);
+    int (*get_type_value_count)(int type);
+    const char* (*get_type_value_name)(int type, int value);
+
+    ~spins_interface()
+    {
+      if (handle)
+        lt_dlclose(handle);
+      lt_dlexit();
+    }
+  };
+
+  using spins_interface_ptr = std::shared_ptr<const spins_interface>;
+}