NuSMV/code/nusmv/core/trace/Trace.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------

  This file is part of the ``trace'' package of NuSMV version 2.
  Copyright (C) 2010 by FBK.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Publi
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>.

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_TRACE_TRACE_H__
#define __NUSMV_CORE_TRACE_TRACE_H__

#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"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct Trace_TAG* Trace_ptr;
typedef struct TraceVarFrame_TAG* TraceIter;

#define TRACE_FOREACH(trace, iter)                                  \
  for ((iter)=Trace_first_iter(trace); TRACE_END_ITER != (iter);    \
       (iter)=TraceIter_get_next(iter))

#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)))

#define TRACE_SYMBOLS_FOREACH(trace, type, iter, symbol)            \
  iter = Trace_symbols_iter((trace), (type));                       \
  while (Trace_symbols_iter_fetch((&iter), (&symbol)))


typedef enum TraceType_TAG {
  TRACE_TYPE_UNSPECIFIED = -1, /* reserved */

  TRACE_TYPE_CNTEXAMPLE = 0,
  TRACE_TYPE_SIMULATION,
  TRACE_TYPE_EXECUTION,

  TRACE_TYPE_END,
} TraceType;


typedef enum TraceIteratorType_TAG {

  TRACE_ITER_NONE=0,

  /* vars */
  TRACE_ITER_F_VARS=0x2,
  TRACE_ITER_S_VARS=0x4,
  TRACE_ITER_I_VARS=0x8,

  /* var groups */
  TRACE_ITER_SF_VARS=0x6,
  TRACE_ITER_ALL_VARS=0xe,

  /* defines */
  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,

  /* vars+defines groups */
  TRACE_ITER_SF_SYMBOLS = 0x16,
  TRACE_ITER_S_SYMBOLS = 0x14,
  TRACE_ITER_I_SYMBOLS = 0x28,

  /* transitional groups: the following iterator types are used to
     describe defines across a transition: COMBINATORIAL holds all the
     defines which depend on (S, I), (N), (S, N), (I, N), (S, I, N).
     In addition to all the defines aforementioned, TRANSITIONAL
     contains INPUT defines as well. */
  TRACE_ITER_COMBINATORIAL=0x7c0,
  TRACE_ITER_TRANSITIONAL=0x07e0,

} TraceIteratorType;


typedef struct TraceStepIter_TAG
{
  Trace_ptr trace;
  TraceIter step;
  TraceIteratorType type;

  unsigned section;
  unsigned cursor;
} TraceStepIter;


typedef struct TraceSymbolsIter_TAG
{
  Trace_ptr trace;
  TraceIteratorType type;

  unsigned section;
  unsigned cursor;
} TraceSymbolsIter;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define TRACE(x) \
  ((Trace_ptr) x)

#define TRACE_CHECK_INSTANCE(x) \
  (nusmv_assert(TRACE(x) != TRACE(NULL)))

#define TRACE_ITER(x) \
  ((TraceIter) x)

#define TRACE_ITER_CHECK_INSTANCE(x) \
  (nusmv_assert(TRACE_ITER(x) != TRACE_ITER(NULL)))

#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_ITER(x) \
  ((TraceStepIter) x)

#define TRACE_SYMBOLS_ITER_CHECK_INSTANCE(x) \
  (nusmv_assert(TRACE_SYMBOLS_ITER(x) != TRACE_SYMBOLS_ITER(NULL)))

#define TRACE_END_ITER TRACE_ITER(NULL)

#define TRACE_STEP_END_ITER TRACE_STEP_ITER(NULL)

#define TRACE_SYMBOLS_END_ITER TRACE_SYMBOLS_ITER(NULL)

/* reserved for Trace Manager */

#define TRACE_UNREGISTERED -1

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

/* Constructors, Destructors, Copiers and Cleaners ****************************/

Trace_ptr
Trace_create(SymbTable_ptr st, const char* desc,
             const TraceType type, NodeList_ptr symbols,
             boolean is_volatile);

Trace_ptr
Trace_create_allow_bits(SymbTable_ptr st, const char* desc,
                  const TraceType type, NodeList_ptr symbols,
                  boolean is_volatile);

Trace_ptr
Trace_copy(const Trace_ptr self, const TraceIter until_here,
           boolean is_volatile);

Trace_ptr
Trace_concat(Trace_ptr self, Trace_ptr* other);

void
Trace_destroy(Trace_ptr self);


/* Queries ********************************************************************/

boolean
Trace_equals(const Trace_ptr self, const Trace_ptr other);

boolean
Trace_is_empty(const Trace_ptr self);


/* metadata */

const char*
Trace_get_desc(const Trace_ptr self);

void
Trace_set_desc(const Trace_ptr self, const char* desc);

boolean
Trace_is_volatile(const Trace_ptr self);

int
Trace_get_id(const Trace_ptr self);

boolean
Trace_is_registered(const Trace_ptr self);

void
Trace_register(const Trace_ptr self, int id);

void
Trace_unregister(const Trace_ptr self);

TraceType
Trace_get_type(const Trace_ptr self);

void
Trace_set_type(Trace_ptr self, TraceType trace_type);

unsigned
Trace_get_length(const Trace_ptr self);


/* freeze/thaw */

boolean
Trace_is_frozen(const Trace_ptr self);

boolean
Trace_is_thawed(const Trace_ptr self);

void
Trace_freeze(Trace_ptr self);

void
Trace_thaw(Trace_ptr self);


/* step management */

TraceIter
Trace_append_step(Trace_ptr self);

boolean
Trace_step_is_loopback(const Trace_ptr self, TraceIter step);

void
Trace_step_force_loopback(const Trace_ptr self, TraceIter step);

/* data accessors */

boolean
Trace_step_put_value(Trace_ptr self, TraceIter step,
                      node_ptr symb, node_ptr value);

node_ptr
Trace_step_get_value(const Trace_ptr self, TraceIter step,
                     node_ptr symb);

/* horizontal iterators, used to traverse a trace */

TraceIter
Trace_first_iter(const Trace_ptr self);

TraceIter
Trace_ith_iter(const Trace_ptr self, unsigned i);

TraceIter
Trace_last_iter(const Trace_ptr self);

TraceIter
TraceIter_get_next(const TraceIter iter);

TraceIter
TraceIter_get_prev(const TraceIter iter);

boolean
TraceIter_is_end(const TraceIter iter);

/* vertical iterators (hint: use macros instead) */

TraceStepIter
Trace_step_iter(const Trace_ptr self, const TraceIter step,
                const TraceIteratorType iter_type);

boolean
Trace_step_iter_fetch(TraceStepIter* step_iter,
                      node_ptr* symb, node_ptr* value);

TraceSymbolsIter
Trace_symbols_iter(const Trace_ptr self,
                   const TraceIteratorType iter_type);

boolean
Trace_symbols_iter_fetch(TraceSymbolsIter* symbols_iter,
                         node_ptr *symb);

/* language queries */

SymbTable_ptr
Trace_get_symb_table(Trace_ptr self);

NodeList_ptr
Trace_get_symbols(const Trace_ptr self);

NodeList_ptr
Trace_get_s_vars(const Trace_ptr self);

NodeList_ptr
Trace_get_sf_vars(const Trace_ptr self);

NodeList_ptr
Trace_get_i_vars(const Trace_ptr self);

boolean
Trace_symbol_in_language(const Trace_ptr self, node_ptr symb);

boolean
Trace_covers_language(const Trace_ptr self, NodeList_ptr symbols);

boolean
Trace_symbol_is_assigned(Trace_ptr self, TraceIter step, node_ptr symb);

boolean
Trace_is_complete(Trace_ptr self, NodeList_ptr vars, boolean report);

const char* TraceType_to_string(const NuSMVEnv_ptr env,
                                const TraceType self);

boolean Trace_has_loopback(const Trace_ptr self);


boolean Trace_validate_loopback(const Trace_ptr self, int loopback_idx);

int Trace_get_first_loopback_from(const Trace_ptr self, TraceIter* step);

void Trace_print_loopbacks(const Trace_ptr self, OStream_ptr stream);


#endif /* __NUSMV_CORE_TRACE_TRACE_H___ */

---