spot  2.12.1
spins_kripke.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 <spot/bricks/brick-hash>
22 #include <spot/bricks/brick-hashset>
23 #include <spot/kripke/kripke.hh>
24 #include <spot/ltsmin/spins_interface.hh>
25 #include <spot/misc/fixpool.hh>
26 #include <spot/misc/mspool.hh>
27 #include <spot/misc/intvcomp.hh>
28 #include <spot/misc/intvcmp2.hh>
29 #include <spot/twacube/cube.hh>
30 
33 namespace spot
34 {
43  typedef int* cspins_state;
44 
47  {
48  bool operator()(const cspins_state lhs, const cspins_state rhs) const
49  {
50  return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
51  }
52  };
53 
56  {
57  size_t operator()(const cspins_state that) const
58  {
59  return that[0];
60  }
61  };
62 
67  {
68  public:
73  cspins_state_manager(unsigned int state_size, int compress);
74 
76  int* unbox_state(cspins_state s) const;
77 
83  cspins_state alloc_setup(int* dst, int* cmp, size_t cmpsize);
84 
86  void decompress(cspins_state s, int* uncompressed, unsigned size) const;
87 
90 
92  unsigned int size() const;
93 
94  private:
96  multiple_size_pool msp_;
97  bool compress_;
98  const unsigned int state_size_;
99  void (*fn_compress_)(const int*, size_t, int*, size_t&);
100  void (*fn_decompress_)(const int*, size_t, int*, size_t);
101  };
102 
103  // \brief This structure is used as a parameter during callback when
104  // generating states from the shared librarie produced by LTSmin.
106  {
107  cspins_state_manager* manager; // The state manager
108  std::vector<cspins_state>* succ; // The successors of a state
109  int* compressed; // Area to store compressed state
110  int* uncompressed; // Area to store uncompressed state
111  bool compress; // Should the state be compressed?
112  bool selfloopize; // Should the state be selfloopized
113  };
114 
120  class cspins_iterator final
121  {
122  public:
123  // Inner struct used to pack the various arguments required by the iterator
125  {
126  cspins_state s;
127  const spot::spins_interface* d;
128  cspins_state_manager& manager;
130  cube cond;
131  bool compress;
132  bool selfloopize;
134  int dead_idx;
135  unsigned tid;
136  };
137 
138  cspins_iterator(const cspins_iterator&) = delete;
139  cspins_iterator(cspins_iterator&) = delete;
140 
142  void recycle(cspins_iterator_param& p);
143  ~cspins_iterator();
144 
145  void next();
146  bool done() const;
147  cspins_state state() const;
148  cube condition() const;
149 
150  private:
152  unsigned compute_index() const;
153 
154  inline void setup_iterator(cspins_state s,
155  const spot::spins_interface* d,
156  cspins_state_manager& manager,
158  cube& cond,
159  bool compress,
160  bool selfloopize,
161  cubeset& cubeset,
162  int dead_idx);
163 
164  std::vector<cspins_state> successors_;
165  unsigned int current_;
166  cube cond_;
167  unsigned tid_;
168  };
169 
170 
171  // A specialisation of the template class kripke that is thread safe.
172  template<>
174  {
175  // Define operators that are available for atomic proposition
176  enum class relop
177  {
178  OP_EQ_VAR, // 1 == a
179  OP_NE_VAR, // 1 != a
180  OP_LT_VAR, // 1 < a
181  OP_GT_VAR, // 1 > a
182  OP_LE_VAR, // 1 <= a
183  OP_GE_VAR, // 1 >= a
184  VAR_OP_EQ, // a == 1
185  VAR_OP_NE, // a != 1
186  VAR_OP_LT, // a < 1
187  VAR_OP_GT, // a >= 1
188  VAR_OP_LE, // a <= 1
189  VAR_OP_GE, // a >= 1
190  VAR_OP_EQ_VAR, // a == b
191  VAR_OP_NE_VAR, // a != b
192  VAR_OP_LT_VAR, // a < b
193  VAR_OP_GT_VAR, // a > b
194  VAR_OP_LE_VAR, // a <= b
195  VAR_OP_GE_VAR, // a >= b
196  VAR_DEAD // The atomic proposition used to label deadlock
197  };
198 
199  // Structure for complex atomic proposition
200  struct one_prop
201  {
202  int lval; // Index of left variable or raw number
203  relop op; // The operator
204  int rval; // Index or right variable or raw number
205  };
206 
207  // Data structure to store complex atomic propositions
208  typedef std::vector<one_prop> prop_set;
209  prop_set pset_;
210 
211  public:
212  kripkecube(spins_interface_ptr sip, bool compress,
213  std::vector<std::string> visible_aps,
214  bool selfloopize, std::string dead_prop,
215  unsigned int nb_threads);
216  ~kripkecube();
217  cspins_state initial(unsigned tid);
218  std::string to_string(const cspins_state s, unsigned tid = 0) const;
219  cspins_iterator* succ(const cspins_state s, unsigned tid);
220  void recycle(cspins_iterator* it, unsigned tid);
221 
223  const std::vector<std::string> ap();
224 
226  unsigned get_threads();
227 
228  private:
231  void match_aps(std::vector<std::string>& aps, std::string dead_prop);
232 
235  void compute_condition(cube c, cspins_state s, unsigned tid = 0);
236 
237  spins_interface_ptr sip_; // The interface to the shared library
238  const spot::spins_interface* d_; // To avoid numerous sip_.get()
239  cspins_state_manager* manager_; // One manager per thread
240  bool compress_; // Should a compression be performed
241 
242  // One per threads to store no longer used iterators (and save memory)
243  std::vector<std::vector<cspins_iterator*>> recycle_;
244 
245  inner_callback_parameters* inner_; // One callback per thread
246  cubeset cubeset_; // A single cubeset to manipulate cubes
247  bool selfloopize_; // Should selfloopize be performed
248  int dead_idx_; // If yes, index of the "dead ap"
249  std::vector<std::string> aps_; // All the atomic propositions
250  unsigned int nb_threads_; // The number of threads used
251  };
252 
254  typedef std::shared_ptr<spot::kripkecube<spot::cspins_state,
257 
258 }
259 
260 #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:121
The management of states (i.e. allocation/deallocation) can be painless since every time we have to c...
Definition: spins_kripke.hh:67
void dealloc(cspins_state s)
Help the manager to reclam the memory of a 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:
int * unbox_state(cspins_state s) const
Get Rid of the internal representation of the state.
unsigned int size() const
The size of a state.
Definition: cube.hh:68
const std::vector< std::string > ap()
List the atomic propositions used by this kripke.
unsigned get_threads()
The number of thread used by this kripke.
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
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:35
Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w....
Definition: spins_interface.hh:44
Abstract class for states.
Definition: twa.hh:47
op
Operator types.
Definition: formula.hh:78
Definition: automata.hh:26
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:43
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:65
std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > ltsmin_kripkecube_ptr
shortcut to manipulate the kripke below
Definition: spins_kripke.hh:256
Definition: spins_kripke.hh:125
This class provides the ability to compare two states.
Definition: spins_kripke.hh:47
This class provides the ability to hash a state.
Definition: spins_kripke.hh:56
Definition: spins_kripke.hh:106

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.1