|
spot
2.16
|
Classes | |
| struct | spot::transition_info |
| Transition information passed to callbacks during state-space exploration. More... | |
| 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, regardless of the input format. 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 whether the state will be compressed or not. This class aims to simplify this management. More... | |
| typedef struct spot::transition_info | spot::transition_info_t |
| Transition information passed to callbacks during state-space exploration. More... | |
| typedef void(* | spot::TransitionCB) (void *ctx, transition_info_t *transition_info, int *dst) |
| Callback used by the PINS interface. More... | |
| typedef std::shared_ptr< const spins_interface > | spot::spins_interface_ptr |
| Shared pointer to a Spins interface. More... | |
| 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 and 1). More... | |
| typedef std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > | spot::ltsmin_kripkecube_ptr |
| shortcut to manipulate the kripke below More... | |
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 and 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
| typedef std::shared_ptr<spot::kripkecube<spot::cspins_state, spot::cspins_iterator> > spot::ltsmin_kripkecube_ptr |
#include <spot/ltsmin/spins_kripke.hh>
shortcut to manipulate the kripke below
| typedef std::shared_ptr<const spins_interface> spot::spins_interface_ptr |
#include <spot/ltsmin/spins_interface.hh>
Shared pointer to a Spins interface.
| typedef struct spot::transition_info spot::transition_info_t |
#include <spot/ltsmin/spins_interface.hh>
Transition information passed to callbacks during state-space exploration.
| typedef void(* spot::TransitionCB) (void *ctx, transition_info_t *transition_info, int *dst) |
#include <spot/ltsmin/spins_interface.hh>
Callback used by the PINS interface.
1.9.1