|
spot 2.15
|
Classes | |
| class | spot::spins_interface |
| Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w.r.t the PINS interface. The class can then be manipulated transparently whatever the input format considered. More... | |
| struct | spot::cspins_state_equal |
| This class provides the ability to compare two states. More... | |
| struct | spot::cspins_state_hash |
| This class provides the ability to hash a state. More... | |
| class | spot::cspins_state_manager |
| The management of states (i.e. allocation/deallocation) can be painless since every time we have to consider wether the state will be compressed or not. This class aims to simplify this management. More... | |
Typedefs | |
| typedef int * | spot::cspins_state |
| A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1). | |
Interface to external model checkers DiVinE and SpinS through the LTSmin API.
| typedef int* spot::cspins_state |
#include <spot/ltsmin/spins_kripke.hh>
A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1).
At position 0 we store the hash associated to the state to avoid multiple computations.
At position 1 we store the size of the state: keeping this information allows to compress the state
1.9.8