#include "nusmv/core/set/set.h"#include "nusmv/core/wff/ExprMgr.h"#include "nusmv/core/compile/symb_table/SymbTable.h"#include "nusmv/core/utils/OStream.h"Go to the source code of this file.
Data Structures | |
| struct | TraceStepIter |
| Trace vertical iterator type. More... | |
| struct | TraceSymbolsIter |
| Trace vertical iterator type. More... | |
Defines | |
| #define | TRACE(x) ((Trace_ptr) x) |
| #define | TRACE_CHECK_INSTANCE(x) (nusmv_assert(TRACE(x) != TRACE(NULL))) |
| #define | TRACE_END_ITER TRACE_ITER(NULL) |
| Iterator ends. | |
| #define | TRACE_FOREACH(trace, iter) |
| Macro to iterate over trace (horizontal iterator). | |
| #define | TRACE_ITER(x) ((TraceIter) x) |
| #define | TRACE_ITER_CHECK_INSTANCE(x) (nusmv_assert(TRACE_ITER(x) != TRACE_ITER(NULL))) |
| #define | TRACE_STEP_END_ITER TRACE_STEP_ITER(NULL) |
| #define | TRACE_STEP_FOREACH(trace, step, type, iter, symbol, value) |
| Macro to iterate over trace step (vertical iterator). | |
| #define | TRACE_STEP_ITER(x) ((TraceStepIter) x) |
| #define | TRACE_STEP_ITER_CHECK_INSTANCE(x) (nusmv_assert(TRACE_STEP_ITER(x) != TRACE_STEP_ITER(NULL))) |
| #define | TRACE_SYMBOLS_END_ITER TRACE_SYMBOLS_ITER(NULL) |
| #define | TRACE_SYMBOLS_FOREACH(trace, type, iter, symbol) |
| Macro to iterate over symbols (vertical iterator). | |
| #define | TRACE_SYMBOLS_ITER(x) ((TraceStepIter) x) |
| #define | TRACE_SYMBOLS_ITER_CHECK_INSTANCE(x) (nusmv_assert(TRACE_SYMBOLS_ITER(x) != TRACE_SYMBOLS_ITER(NULL))) |
| #define | TRACE_UNREGISTERED -1 |
Typedefs | |
| typedef struct Trace_TAG * | Trace_ptr |
| typedef struct TraceVarFrame_TAG * | TraceIter |
Enumerations | |
| enum | TraceIteratorType { TRACE_ITER_NONE = 0, TRACE_ITER_F_VARS = 0x2, TRACE_ITER_S_VARS = 0x4, TRACE_ITER_I_VARS = 0x8, TRACE_ITER_SF_VARS = 0x6, TRACE_ITER_ALL_VARS = 0xe, TRACE_ITER_S_DEFINES = 0x10, TRACE_ITER_I_DEFINES = 0x20, TRACE_ITER_SI_DEFINES = 0x40, TRACE_ITER_N_DEFINES = 0x80, TRACE_ITER_SN_DEFINES = 0x100, TRACE_ITER_IN_DEFINES = 0x200, TRACE_ITER_SIN_DEFINES = 0x400, TRACE_ITER_SF_SYMBOLS = 0x16, TRACE_ITER_S_SYMBOLS = 0x14, TRACE_ITER_I_SYMBOLS = 0x28, TRACE_ITER_COMBINATORIAL = 0x7c0, TRACE_ITER_TRANSITIONAL = 0x07e0 } |
Trace vertical iterator kind enum. More... | |
| enum | TraceType { TRACE_TYPE_UNSPECIFIED = -1, TRACE_TYPE_CNTEXAMPLE = 0, TRACE_TYPE_SIMULATION, TRACE_TYPE_EXECUTION, TRACE_TYPE_END } |
Trace type enumeration. More... | |
Functions | |
| boolean | Trace_step_iter_fetch (TraceStepIter *step_iter, node_ptr *symb, node_ptr *value) |
| Step iterator next function. | |
| boolean | Trace_symbols_iter_fetch (TraceSymbolsIter *symbols_iter, node_ptr *symb) |
| Symbols iterator next function. | |
| TraceIter | TraceIter_get_next (const TraceIter iter) |
| Returns a trace iterator pointing to the next step of the trace. | |
| TraceIter | TraceIter_get_prev (const TraceIter iter) |
| Returns a trace iterator pointing to the previous step of the trace. | |
| boolean | TraceIter_is_end (const TraceIter iter) |
| Iterator-at-end-of-trace predicate. | |
| const char * | TraceType_to_string (const NuSMVEnv_ptr env, const TraceType self) |
| #define TRACE_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(TRACE(x) != TRACE(NULL))) |
| #define TRACE_END_ITER TRACE_ITER(NULL) |
Iterator ends.
| #define TRACE_FOREACH | ( | trace, | |||
| iter | ) |
for ((iter)=Trace_first_iter(trace); TRACE_END_ITER != (iter); \ (iter)=TraceIter_get_next(iter))
Macro to iterate over trace (horizontal iterator).
Use this macro to iterate from the first step to the last.
none
| #define TRACE_ITER_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(TRACE_ITER(x) != TRACE_ITER(NULL))) |
| #define TRACE_STEP_FOREACH | ( | trace, | |||
| step, | |||||
| type, | |||||
| iter, | |||||
| symbol, | |||||
| value | ) |
iter = Trace_step_iter((trace), (step), (type)); \ while (Trace_step_iter_fetch((&iter), (&symbol), (&value)))
Macro to iterate over trace step (vertical iterator).
Use this macro to iterate over assignments for a given step.
symbol and value are assigned for each iteration
| #define TRACE_STEP_ITER | ( | x | ) | ((TraceStepIter) x) |
| #define TRACE_STEP_ITER_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(TRACE_STEP_ITER(x) != TRACE_STEP_ITER(NULL))) |
| #define TRACE_SYMBOLS_END_ITER TRACE_SYMBOLS_ITER(NULL) |
| #define TRACE_SYMBOLS_FOREACH | ( | trace, | |||
| type, | |||||
| iter, | |||||
| symbol | ) |
iter = Trace_symbols_iter((trace), (type)); \ while (Trace_symbols_iter_fetch((&iter), (&symbol)))
Macro to iterate over symbols (vertical iterator).
Use this macro to iterate over symbols of a trace.
symbol is assigned for each iteration
| #define TRACE_SYMBOLS_ITER | ( | x | ) | ((TraceStepIter) x) |
| #define TRACE_SYMBOLS_ITER_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(TRACE_SYMBOLS_ITER(x) != TRACE_SYMBOLS_ITER(NULL))) |
| typedef struct Trace_TAG* Trace_ptr |
| typedef struct TraceVarFrame_TAG* TraceIter |
| enum TraceIteratorType |
Trace vertical iterator kind enum.
Specific kind of iterators can be required using the appropriate value from this enumeration
| boolean Trace_step_iter_fetch | ( | TraceStepIter * | step_iter, | |
| node_ptr * | symb, | |||
| node_ptr * | value | |||
| ) |
Step iterator next function.
A step iterator is a stateful iterator which yields an single assignment at each call of this function.
\"step_iter\" must be a valid step iterator for the trace. If a valid assignment was found, True is returned. Otherwise False is returned. This indicates end of iteration.
Hint: do not use this function. Use TRACE_SYMBOLS_FOREACH macro instead (it is way easier and more readable).
| boolean Trace_symbols_iter_fetch | ( | TraceSymbolsIter * | symbols_iter, | |
| node_ptr * | symb | |||
| ) |
Symbols iterator next function.
A symbols iterator is a stateful iterator which yields a symbols in the trace language at each call of this function.
\"symbols_iter\" must be a valid symbols iterator for the trace. If a symbols is found, True is returned. Otherwise False is returned. This indicates end of iteration.
Hint: do not use this function. Use TRACE_SYMBOLS_FOREACH macro instead (it is way easier and more readable).
Returns a trace iterator pointing to the next step of the trace.
Returns a trace iterator pointing to the next step of the trace. TRACE_END_ITER is returned if no such iterator exists
Returns a trace iterator pointing to the previous step of the trace.
Returns a trace iterator pointing to the previous step of the trace. TRACE_END_ITER is returned if no such iterator exists
| const char* TraceType_to_string | ( | const NuSMVEnv_ptr | env, | |
| const TraceType | self | |||
| ) |
1.6.1