spot 2.12.2
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
24namespace 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
34
35 typedef void (*TransitionCB)(void *ctx,
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);
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}
Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w....
Definition: spins_interface.hh:44
Definition: automata.hh:26
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 doxygen 1.9.4