00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00036 #ifndef __NUSMV_CORE_TRACE_TRACE_H__
00037 #define __NUSMV_CORE_TRACE_TRACE_H__
00038
00039 #include "nusmv/core/set/set.h"
00040 #include "nusmv/core/wff/ExprMgr.h"
00041 #include "nusmv/core/compile/symb_table/SymbTable.h"
00042 #include "nusmv/core/utils/OStream.h"
00043
00044
00045
00046
00047
00054 typedef struct Trace_TAG* Trace_ptr;
00055 typedef struct TraceVarFrame_TAG* TraceIter;
00056
00067 #define TRACE_FOREACH(trace, iter) \
00068 for ((iter)=Trace_first_iter(trace); TRACE_END_ITER != (iter); \
00069 (iter)=TraceIter_get_next(iter))
00070
00081 #define TRACE_STEP_FOREACH(trace, step, type, iter, symbol, value) \
00082 iter = Trace_step_iter((trace), (step), (type)); \
00083 while (Trace_step_iter_fetch((&iter), (&symbol), (&value)))
00084
00094 #define TRACE_SYMBOLS_FOREACH(trace, type, iter, symbol) \
00095 iter = Trace_symbols_iter((trace), (type)); \
00096 while (Trace_symbols_iter_fetch((&iter), (&symbol)))
00097
00098
00105 typedef enum TraceType_TAG {
00106 TRACE_TYPE_UNSPECIFIED = -1,
00107
00108 TRACE_TYPE_CNTEXAMPLE = 0,
00109 TRACE_TYPE_SIMULATION,
00110 TRACE_TYPE_EXECUTION,
00111
00112 TRACE_TYPE_END,
00113 } TraceType;
00114
00115
00125 typedef enum TraceIteratorType_TAG {
00126
00127 TRACE_ITER_NONE=0,
00128
00129
00130 TRACE_ITER_F_VARS=0x2,
00131 TRACE_ITER_S_VARS=0x4,
00132 TRACE_ITER_I_VARS=0x8,
00133
00134
00135 TRACE_ITER_SF_VARS=0x6,
00136 TRACE_ITER_ALL_VARS=0xe,
00137
00138
00139 TRACE_ITER_S_DEFINES=0x10,
00140 TRACE_ITER_I_DEFINES=0x20,
00141
00142 TRACE_ITER_SI_DEFINES=0x40,
00143 TRACE_ITER_N_DEFINES=0x80,
00144 TRACE_ITER_SN_DEFINES=0x100,
00145 TRACE_ITER_IN_DEFINES=0x200,
00146 TRACE_ITER_SIN_DEFINES=0x400,
00147
00148
00149 TRACE_ITER_SF_SYMBOLS = 0x16,
00150 TRACE_ITER_S_SYMBOLS = 0x14,
00151 TRACE_ITER_I_SYMBOLS = 0x28,
00152
00153
00154
00155
00156
00157
00158 TRACE_ITER_COMBINATORIAL=0x7c0,
00159 TRACE_ITER_TRANSITIONAL=0x07e0,
00160
00161 } TraceIteratorType;
00162
00163
00172 typedef struct TraceStepIter_TAG
00173 {
00174 Trace_ptr trace;
00175 TraceIter step;
00176 TraceIteratorType type;
00177
00178 unsigned section;
00179 unsigned cursor;
00180 } TraceStepIter;
00181
00182
00191 typedef struct TraceSymbolsIter_TAG
00192 {
00193 Trace_ptr trace;
00194 TraceIteratorType type;
00195
00196 unsigned section;
00197 unsigned cursor;
00198 } TraceSymbolsIter;
00199
00200
00201
00202
00203
00209 #define TRACE(x) \
00210 ((Trace_ptr) x)
00211
00217 #define TRACE_CHECK_INSTANCE(x) \
00218 (nusmv_assert(TRACE(x) != TRACE(NULL)))
00219
00225 #define TRACE_ITER(x) \
00226 ((TraceIter) x)
00227
00233 #define TRACE_ITER_CHECK_INSTANCE(x) \
00234 (nusmv_assert(TRACE_ITER(x) != TRACE_ITER(NULL)))
00235
00241 #define TRACE_STEP_ITER(x) \
00242 ((TraceStepIter) x)
00243
00249 #define TRACE_STEP_ITER_CHECK_INSTANCE(x) \
00250 (nusmv_assert(TRACE_STEP_ITER(x) != TRACE_STEP_ITER(NULL)))
00251
00257 #define TRACE_SYMBOLS_ITER(x) \
00258 ((TraceStepIter) x)
00259
00265 #define TRACE_SYMBOLS_ITER_CHECK_INSTANCE(x) \
00266 (nusmv_assert(TRACE_SYMBOLS_ITER(x) != TRACE_SYMBOLS_ITER(NULL)))
00267
00273 #define TRACE_END_ITER TRACE_ITER(NULL)
00274
00280 #define TRACE_STEP_END_ITER TRACE_STEP_ITER(NULL)
00281
00287 #define TRACE_SYMBOLS_END_ITER TRACE_SYMBOLS_ITER(NULL)
00288
00289
00290
00296 #define TRACE_UNREGISTERED -1
00297
00300
00301
00302
00303
00304
00305
00340 Trace_ptr
00341 Trace_create(SymbTable_ptr st, const char* desc,
00342 const TraceType type, NodeList_ptr symbols,
00343 boolean is_volatile);
00344
00379 Trace_ptr
00380 Trace_create_allow_bits(SymbTable_ptr st, const char* desc,
00381 const TraceType type, NodeList_ptr symbols,
00382 boolean is_volatile);
00383
00425 Trace_ptr
00426 Trace_copy(const Trace_ptr self, const TraceIter until_here,
00427 boolean is_volatile);
00428
00450 Trace_ptr
00451 Trace_concat(Trace_ptr self, Trace_ptr* other);
00452
00461 void
00462 Trace_destroy(Trace_ptr self);
00463
00464
00465
00466
00491 boolean
00492 Trace_equals(const Trace_ptr self, const Trace_ptr other);
00493
00503 boolean
00504 Trace_is_empty(const Trace_ptr self);
00505
00506
00507
00508
00515 const char*
00516 Trace_get_desc(const Trace_ptr self);
00517
00528 void
00529 Trace_set_desc(const Trace_ptr self, const char* desc);
00530
00542 boolean
00543 Trace_is_volatile(const Trace_ptr self);
00544
00552 int
00553 Trace_get_id(const Trace_ptr self);
00554
00561 boolean
00562 Trace_is_registered(const Trace_ptr self);
00563
00571 void
00572 Trace_register(const Trace_ptr self, int id);
00573
00580 void
00581 Trace_unregister(const Trace_ptr self);
00582
00591 TraceType
00592 Trace_get_type(const Trace_ptr self);
00593
00602 void
00603 Trace_set_type(Trace_ptr self, TraceType trace_type);
00604
00616 unsigned
00617 Trace_get_length(const Trace_ptr self);
00618
00619
00620
00621
00639 boolean
00640 Trace_is_frozen(const Trace_ptr self);
00641
00657 boolean
00658 Trace_is_thawed(const Trace_ptr self);
00659
00676 void
00677 Trace_freeze(Trace_ptr self);
00678
00695 void
00696 Trace_thaw(Trace_ptr self);
00697
00698
00699
00700
00714 TraceIter
00715 Trace_append_step(Trace_ptr self);
00716
00736 boolean
00737 Trace_step_is_loopback(const Trace_ptr self, TraceIter step);
00738
00751 void
00752 Trace_step_force_loopback(const Trace_ptr self, TraceIter step);
00753
00754
00755
00779 boolean
00780 Trace_step_put_value(Trace_ptr self, TraceIter step,
00781 node_ptr symb, node_ptr value);
00782
00801 node_ptr
00802 Trace_step_get_value(const Trace_ptr self, TraceIter step,
00803 node_ptr symb);
00804
00805
00806
00823 TraceIter
00824 Trace_first_iter(const Trace_ptr self);
00825
00842 TraceIter
00843 Trace_ith_iter(const Trace_ptr self, unsigned i);
00844
00857 TraceIter
00858 Trace_last_iter(const Trace_ptr self);
00859
00870 TraceIter
00871 TraceIter_get_next(const TraceIter iter);
00872
00883 TraceIter
00884 TraceIter_get_prev(const TraceIter iter);
00885
00891 boolean
00892 TraceIter_is_end(const TraceIter iter);
00893
00894
00895
00912 TraceStepIter
00913 Trace_step_iter(const Trace_ptr self, const TraceIter step,
00914 const TraceIteratorType iter_type);
00915
00932 boolean
00933 Trace_step_iter_fetch(TraceStepIter* step_iter,
00934 node_ptr* symb, node_ptr* value);
00935
00948 TraceSymbolsIter
00949 Trace_symbols_iter(const Trace_ptr self,
00950 const TraceIteratorType iter_type);
00951
00968 boolean
00969 Trace_symbols_iter_fetch(TraceSymbolsIter* symbols_iter,
00970 node_ptr *symb);
00971
00972
00973
00986 SymbTable_ptr
00987 Trace_get_symb_table(Trace_ptr self);
00988
00999 NodeList_ptr
01000 Trace_get_symbols(const Trace_ptr self);
01001
01012 NodeList_ptr
01013 Trace_get_s_vars(const Trace_ptr self);
01014
01025 NodeList_ptr
01026 Trace_get_sf_vars(const Trace_ptr self);
01027
01038 NodeList_ptr
01039 Trace_get_i_vars(const Trace_ptr self);
01040
01052 boolean
01053 Trace_symbol_in_language(const Trace_ptr self, node_ptr symb);
01054
01066 boolean
01067 Trace_covers_language(const Trace_ptr self, NodeList_ptr symbols);
01068
01079 boolean
01080 Trace_symbol_is_assigned(Trace_ptr self, TraceIter step, node_ptr symb);
01081
01090 boolean
01091 Trace_is_complete(Trace_ptr self, NodeList_ptr vars, boolean report);
01092
01093 const char* TraceType_to_string(const NuSMVEnv_ptr env,
01094 const TraceType self);
01095
01104 boolean Trace_has_loopback(const Trace_ptr self);
01105
01106
01115 boolean Trace_validate_loopback(const Trace_ptr self, int loopback_idx);
01116
01129 int Trace_get_first_loopback_from(const Trace_ptr self, TraceIter* step);
01130
01139 void Trace_print_loopbacks(const Trace_ptr self, OStream_ptr stream);
01140
01141
01144 #endif