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>
51 return 0 == memcmp(lhs, rhs, (2+rhs[1])*
sizeof(
int));
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);
109 std::vector<cspins_state>* succ;
149 cube condition()
const;
153 unsigned compute_index()
const;
165 std::vector<cspins_state> successors_;
166 unsigned int current_;
209 typedef std::vector<one_prop> prop_set;
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);
224 const std::vector<std::string>
ap();
232 void match_aps(std::vector<std::string>& aps, std::string dead_prop);
238 spins_interface_ptr sip_;
244 std::vector<std::vector<cspins_iterator*>> recycle_;
250 std::vector<std::string> aps_;
251 unsigned int nb_threads_;
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.
A fixed-size memory pool implementation.
Definition fixpool.hh:47
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