spot 2.11.2.dev
spins_kripke.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et
3// Développement de l'Epita (LRDE)
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <spot/bricks/brick-hash>
23#include <spot/bricks/brick-hashset>
24#include <spot/kripke/kripke.hh>
25#include <spot/ltsmin/spins_interface.hh>
26#include <spot/misc/fixpool.hh>
27#include <spot/misc/mspool.hh>
28#include <spot/misc/intvcomp.hh>
29#include <spot/misc/intvcmp2.hh>
30#include <spot/twacube/cube.hh>
31
34namespace spot
35{
44 typedef int* cspins_state;
45
48 {
49 bool operator()(const cspins_state lhs, const cspins_state rhs) const
50 {
51 return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
52 }
53 };
54
57 {
58 size_t operator()(const cspins_state that) const
59 {
60 return that[0];
61 }
62 };
63
68 {
69 public:
74 cspins_state_manager(unsigned int state_size, int compress);
75
78
84 cspins_state alloc_setup(int* dst, int* cmp, size_t cmpsize);
85
87 void decompress(cspins_state s, int* uncompressed, unsigned size) const;
88
91
93 unsigned int size() const;
94
95 private:
98 bool compress_;
99 const unsigned int state_size_;
100 void (*fn_compress_)(const int*, size_t, int*, size_t&);
101 void (*fn_decompress_)(const int*, size_t, int*, size_t);
102 };
103
104 // \brief This structure is used as a parameter during callback when
105 // generating states from the shared librarie produced by LTSmin.
107 {
108 cspins_state_manager* manager; // The state manager
109 std::vector<cspins_state>* succ; // The successors of a state
110 int* compressed; // Area to store compressed state
111 int* uncompressed; // Area to store uncompressed state
112 bool compress; // Should the state be compressed?
113 bool selfloopize; // Should the state be selfloopized
114 };
115
121 class cspins_iterator final
122 {
123 public:
124 // Inner struct used to pack the various arguments required by the iterator
126 {
127 cspins_state s;
128 const spot::spins_interface* d;
129 cspins_state_manager& manager;
131 cube cond;
132 bool compress;
133 bool selfloopize;
135 int dead_idx;
136 unsigned tid;
137 };
138
139 cspins_iterator(const cspins_iterator&) = delete;
141
143 void recycle(cspins_iterator_param& p);
145
146 void next();
147 bool done() const;
148 cspins_state state() const;
149 cube condition() const;
150
151 private:
153 unsigned compute_index() const;
154
155 inline void setup_iterator(cspins_state s,
156 const spot::spins_interface* d,
157 cspins_state_manager& manager,
159 cube& cond,
160 bool compress,
161 bool selfloopize,
163 int dead_idx);
164
165 std::vector<cspins_state> successors_;
166 unsigned int current_;
167 cube cond_;
168 unsigned tid_;
169 };
170
171
172 // A specialisation of the template class kripke that is thread safe.
173 template<>
175 {
176 // Define operators that are available for atomic proposition
177 enum class relop
178 {
179 OP_EQ_VAR, // 1 == a
180 OP_NE_VAR, // 1 != a
181 OP_LT_VAR, // 1 < a
182 OP_GT_VAR, // 1 > a
183 OP_LE_VAR, // 1 <= a
184 OP_GE_VAR, // 1 >= a
185 VAR_OP_EQ, // a == 1
186 VAR_OP_NE, // a != 1
187 VAR_OP_LT, // a < 1
188 VAR_OP_GT, // a >= 1
189 VAR_OP_LE, // a <= 1
190 VAR_OP_GE, // a >= 1
191 VAR_OP_EQ_VAR, // a == b
192 VAR_OP_NE_VAR, // a != b
193 VAR_OP_LT_VAR, // a < b
194 VAR_OP_GT_VAR, // a > b
195 VAR_OP_LE_VAR, // a <= b
196 VAR_OP_GE_VAR, // a >= b
197 VAR_DEAD // The atomic proposition used to label deadlock
198 };
199
200 // Structure for complex atomic proposition
201 struct one_prop
202 {
203 int lval; // Index of left variable or raw number
204 relop op; // The operator
205 int rval; // Index or right variable or raw number
206 };
207
208 // Data structure to store complex atomic propositions
209 typedef std::vector<one_prop> prop_set;
210 prop_set pset_;
211
212 public:
213 kripkecube(spins_interface_ptr sip, bool compress,
214 std::vector<std::string> visible_aps,
215 bool selfloopize, std::string dead_prop,
216 unsigned int nb_threads);
217 ~kripkecube();
218 cspins_state initial(unsigned tid);
219 std::string to_string(const cspins_state s, unsigned tid = 0) const;
220 cspins_iterator* succ(const cspins_state s, unsigned tid);
221 void recycle(cspins_iterator* it, unsigned tid);
222
224 const std::vector<std::string> ap();
225
227 unsigned get_threads();
228
229 private:
232 void match_aps(std::vector<std::string>& aps, std::string dead_prop);
233
236 void compute_condition(cube c, cspins_state s, unsigned tid = 0);
237
238 spins_interface_ptr sip_; // The interface to the shared library
239 const spot::spins_interface* d_; // To avoid numerous sip_.get()
240 cspins_state_manager* manager_; // One manager per thread
241 bool compress_; // Should a compression be performed
242
243 // One per threads to store no longer used iterators (and save memory)
244 std::vector<std::vector<cspins_iterator*>> recycle_;
245
246 inner_callback_parameters* inner_; // One callback per thread
247 cubeset cubeset_; // A single cubeset to manipulate cubes
248 bool selfloopize_; // Should selfloopize be performed
249 int dead_idx_; // If yes, index of the "dead ap"
250 std::vector<std::string> aps_; // All the atomic propositions
251 unsigned int nb_threads_; // The number of threads used
252 };
253
255 typedef std::shared_ptr<spot::kripkecube<spot::cspins_state,
258
259}
260
261#include <spot/ltsmin/spins_kripke.hxx>
This class provides an iterator over the successors of a state. All successors are computed once when...
Definition: spins_kripke.hh:122
The management of states (i.e. allocation/deallocation) can be painless since every time we have to c...
Definition: spins_kripke.hh:68
void dealloc(cspins_state s)
Help the manager to reclam the memory of a state.
int * unbox_state(cspins_state s) const
Get Rid of the internal representation of the state.
void decompress(cspins_state s, int *uncompressed, unsigned size) const
Helper to decompress a state.
cspins_state alloc_setup(int *dst, int *cmp, size_t cmpsize)
Builder for a state from a raw description given in dst.
cspins_state_manager(unsigned int state_size, int compress)
Build a manager for a state of state_size variables and indicate wether compression should be used:
unsigned int size() const
The size of a state.
Definition: cube.hh:69
unsigned get_threads()
The number of thread used by this kripke.
const std::vector< std::string > ap()
List the atomic propositions used by this kripke.
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
std::string to_string(const State, unsigned tid) const
Provides a string representation of the parameter state.
SuccIterator * succ(const State, unsigned tid)
Returns an iterator over the successors of the parameter state.
State initial(unsigned tid)
Returns the initial State of the System. The tid parameter is used internally for sharing this struct...
void recycle(SuccIterator *, unsigned tid)
Allocation and deallocation of iterator is costly. This method allows to reuse old iterators.
A multiple-size memory pool implementation.
Definition: mspool.hh:36
Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w....
Definition: spins_interface.hh:45
Abstract class for states.
Definition: twa.hh:51
op
Operator types.
Definition: formula.hh:79
Definition: automata.hh:27
int * cspins_state
A Spins state is represented as an array of integer Note that this array has two reserved slots (posi...
Definition: spins_kripke.hh:44
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:66
std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > ltsmin_kripkecube_ptr
shortcut to manipulate the kripke below
Definition: spins_kripke.hh:257
Definition: spins_kripke.hh:126
This class provides the ability to compare two states.
Definition: spins_kripke.hh:48
This class provides the ability to hash a state.
Definition: spins_kripke.hh:57
Definition: spins_kripke.hh:107

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