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