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>
50 return 0 == memcmp(lhs, rhs, (2+rhs[1])*
sizeof(
int));
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);
108 std::vector<cspins_state>* succ;
148 cube condition()
const;
152 unsigned compute_index()
const;
164 std::vector<cspins_state> successors_;
165 unsigned int current_;
208 typedef std::vector<one_prop> prop_set;
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);
223 const std::vector<std::string>
ap();
231 void match_aps(std::vector<std::string>& aps, std::string dead_prop);
237 spins_interface_ptr sip_;
243 std::vector<std::vector<cspins_iterator*>> recycle_;
249 std::vector<std::string> aps_;
250 unsigned int nb_threads_;
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.
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:46
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: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