ltsmin: extract spins interface
* spot/ltsmin/Makefile.am, spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, spot/ltsmin/spins_interface.hh: here.
This commit is contained in:
parent
8a930c7572
commit
5445007070
4 changed files with 65 additions and 42 deletions
|
|
@ -24,7 +24,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||||
|
|
||||||
ltsmindir = $(pkgincludedir)/ltsmin
|
ltsmindir = $(pkgincludedir)/ltsmin
|
||||||
|
|
||||||
ltsmin_HEADERS = ltsmin.hh
|
ltsmin_HEADERS = ltsmin.hh spins_interface.hh
|
||||||
|
|
||||||
lib_LTLIBRARIES = libspotltsmin.la
|
lib_LTLIBRARIES = libspotltsmin.la
|
||||||
libspotltsmin_la_DEPENDENCIES = \
|
libspotltsmin_la_DEPENDENCIES = \
|
||||||
|
|
|
||||||
|
|
@ -55,45 +55,6 @@ namespace spot
|
||||||
{
|
{
|
||||||
namespace
|
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
|
// STATE
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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)
|
// Developpement de l'Epita (LRDE)
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -19,6 +19,7 @@
|
||||||
|
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
|
#include <spot/ltsmin/spins_interface.hh>
|
||||||
#include <spot/kripke/kripke.hh>
|
#include <spot/kripke/kripke.hh>
|
||||||
#include <spot/twacube/twacube.hh>
|
#include <spot/twacube/twacube.hh>
|
||||||
#include <spot/tl/apcollect.hh>
|
#include <spot/tl/apcollect.hh>
|
||||||
|
|
@ -27,7 +28,6 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
struct spins_interface;
|
|
||||||
class cspins_iterator;
|
class cspins_iterator;
|
||||||
typedef int* cspins_state;
|
typedef int* cspins_state;
|
||||||
|
|
||||||
|
|
|
||||||
62
spot/ltsmin/spins_interface.hh
Normal file
62
spot/ltsmin/spins_interface.hh
Normal file
|
|
@ -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>;
|
||||||
|
}
|
||||||
Loading…
Add table
Add a link
Reference in a new issue