#include "nusmv/core/utils/object.h"
#include "nusmv/core/dd/DDMgr.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/trace/TraceLabel.h"
Go to the source code of this file.
Defines | |
#define | SIMULATE_STATE(self) ((SimulateState_ptr) self) |
To cast and check instances of class SimulateState. | |
#define | SIMULATE_STATE_CHECK_INSTANCE(self) (nusmv_assert(SIMULATE_STATE(self) != SIMULATE_STATE(NULL))) |
Typedefs | |
typedef struct SimulateState_TAG * | SimulateState_ptr |
Functions | |
bdd_ptr | SimulateState_get_bdd (SimulateState_ptr const self) |
Getter for the bdd field. | |
TraceLabel | SimulateState_get_trace_label (SimulateState_ptr const self) |
Getter for the trace_label field. | |
void | SimulateState_set_all (SimulateState_ptr const self, bdd_ptr const state, TraceLabel const label) |
Set all fields of the class. | |
SimulateState_ptr | SimulateState_set_in_env (NuSMVEnv_ptr const env, bdd_ptr const bdd, TraceLabel const trace_label) |
Create an istance and add to environment or set it if already present. |
#define SIMULATE_STATE | ( | self | ) | ((SimulateState_ptr) self) |
To cast and check instances of class SimulateState.
These macros must be used respectively to cast and to check instances of class SimulateState
#define SIMULATE_STATE_CHECK_INSTANCE | ( | self | ) | (nusmv_assert(SIMULATE_STATE(self) != SIMULATE_STATE(NULL))) |
typedef struct SimulateState_TAG* SimulateState_ptr |
bdd_ptr SimulateState_get_bdd | ( | SimulateState_ptr const | self | ) |
Getter for the bdd field.
Getter for the bdd field
TraceLabel SimulateState_get_trace_label | ( | SimulateState_ptr const | self | ) |
Getter for the trace_label field.
Getter for the trace_label field
void SimulateState_set_all | ( | SimulateState_ptr const | self, | |
bdd_ptr const | state, | |||
TraceLabel const | label | |||
) |
SimulateState_ptr SimulateState_set_in_env | ( | NuSMVEnv_ptr const | env, | |
bdd_ptr const | bdd, | |||
TraceLabel const | trace_label | |||
) |
Create an istance and add to environment or set it if already present.
Create an istance and add to environment or set it if already present