spot
2.13.0.dev
Loading...
Searching...
No Matches
spot
ltsmin
spins_interface.hh
1
// -*- coding: utf-8 -*-
2
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3
//
4
// This file is part of Spot, a model checking library.
5
//
6
// Spot is free software; you can redistribute it and/or modify it
7
// under the terms of the GNU General Public License as published by
8
// the Free Software Foundation; either version 3 of the License, or
9
// (at your option) any later version.
10
//
11
// Spot is distributed in the hope that it will be useful, but WITHOUT
12
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14
// License for more details.
15
//
16
// You should have received a copy of the GNU General Public License
17
// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19
#pragma once
20
21
#include <memory>
22
#include <spot/misc/common.hh>
23
24
namespace
spot
25
{
27
// spins interface
28
29
typedef
struct
transition_info
30
{
31
int
* labels;
// edge labels, NULL, or pointer to the edge label(s)
32
int
group;
// holds transition group or -1 if unknown
33
}
transition_info_t
;
34
35
typedef
void (*TransitionCB)(
void
*ctx,
36
transition_info_t
*
transition_info
,
37
int
*dst);
38
43
class
SPOT_API
spins_interface
44
{
45
public
:
46
spins_interface
() =
default
;
47
spins_interface
(
const
std::string& file_arg);
48
~spins_interface
();
49
50
// The various functions that can be called once the object
51
// has been instanciated.
52
void (*get_initial_state)(
void
*to);
53
int (*have_property)();
54
int (*get_successors)(
void
* m,
int
*in, TransitionCB,
void
*arg);
55
int (*get_state_size)();
56
const
char
* (*get_state_variable_name)(
int
var);
57
int (*get_state_variable_type)(
int
var);
58
int (*get_type_count)();
59
const
char
* (*get_type_name)(
int
type);
60
int (*get_type_value_count)(
int
type);
61
const
char
* (*get_type_value_name)(
int
type,
int
value);
62
63
private
:
64
// handle to the dynamic library. The variable is of type lt_dlhandle, but
65
// we need this trick since we cannot put ltdl.h in public headers
66
void
* handle;
67
};
68
69
using
spins_interface_ptr = std::shared_ptr<const spins_interface>;
70
}
spot::spins_interface
Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w....
Definition
spins_interface.hh:44
spot
Definition
automata.hh:26
spot::transition_info
Definition
spins_interface.hh:30
Please direct any
question
,
comment
, or
bug report
to the Spot mailing list at
spot@lrde.epita.fr
.
Generated on Fri Feb 27 2015 10:00:07 for spot by
1.9.8