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

Go to the documentation of this file.

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


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

  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 Public
  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_MGR_H__
#define __NUSMV_CORE_TRACE_TRACE_MGR_H__

#include "nusmv/core/dd/dd.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/array.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/trace/plugins/TracePlugin.h"
#include "nusmv/core/trace/exec/PartialTraceExecutor.h"
#include "nusmv/core/trace/exec/CompleteTraceExecutor.h"
#include "nusmv/core/trace/eval/BaseEvaluator.h"
#include "nusmv/core/trace/TraceLabel.h"
#include "nusmv/core/trace/TraceOpt.h"
#include "nusmv/core/node/node.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define TRACE_MGR_DEFAULT_PLUGIN -1

#define TRACE_MGR_LAST_TRACE -1

#define ENV_TRACE_EXPLAINER_CHANGES_ONLY "env_trace_explainer_changes_only"

#define ENV_TRACE_EXPLAINER "env_trace_explainer"

#define ENV_TRACE_TABLE_COLUMN "env_trace_table_column"

#define ENV_TRACE_TABLE_ROW "env_trace_table_row"

#define ENV_TRACE_XML_DUMPER "env_trace_xml_dumper"

#define ENV_TRACE_COMPACT "env_trace_compact"

#define ENV_TRACE_EMBEDDED_XML_DUMPER "env_trace_embedded_xml_dumper"

#define ENV_TRACE_EMPTY_INDEX "etraceemptyindex"

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


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

typedef struct TraceMgr_TAG* TraceMgr_ptr;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

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

#define TRACE_MGR(x) \
        ((TraceMgr_ptr) x)

#define TRACE_MGR_CHECK_INSTANCE(x) \
        (nusmv_assert(TRACE_MGR(x) != TRACE_MGR(NULL)))

/*---------------------------------------------------------------------------*/
/* Function prototype                                                        */
/*---------------------------------------------------------------------------*/

/* TraceMgr Constructor/Destructor */

TraceMgr_ptr TraceMgr_create(NuSMVEnv_ptr env);

void TraceMgr_destroy(TraceMgr_ptr self);

/* TraceMgr Getters */

int TraceMgr_get_size(const TraceMgr_ptr self);

Trace_ptr
TraceMgr_get_trace_at_index(const TraceMgr_ptr self,
                            int index);

/* TraceMgr register functions */

int TraceMgr_register_trace(TraceMgr_ptr self,
                                   Trace_ptr trace);

/* Evaluators management */

BaseEvaluator_ptr
TraceMgr_get_evaluator(TraceMgr_ptr self);

void
TraceMgr_register_evaluator(TraceMgr_ptr self,
                            BaseEvaluator_ptr eval);

void TraceMgr_unregister_evaluator(TraceMgr_ptr self);

/* Complete trace executors management functions */

void
TraceMgr_register_complete_trace_executor(TraceMgr_ptr self,
       const char* executor_name, const char* executor_desc,
       const CompleteTraceExecutor_ptr executor);

CompleteTraceExecutor_ptr
TraceMgr_get_complete_trace_executor(const TraceMgr_ptr self,
                                         const char* name);

array_t*
TraceMgr_get_complete_trace_executor_ids(const TraceMgr_ptr self);

const char*
TraceMgr_get_complete_trace_executor_desc(const TraceMgr_ptr self,
                                          const char* name);

CompleteTraceExecutor_ptr
TraceMgr_get_default_complete_trace_executor(
      const TraceMgr_ptr global_trace_manager);

/* Partial trace executors management functions */

void
TraceMgr_register_partial_trace_executor(TraceMgr_ptr self,
       const char* executor_name, const char* executor_desc,
       const PartialTraceExecutor_ptr executor);

array_t*
TraceMgr_get_partial_trace_executor_ids(const TraceMgr_ptr self);

PartialTraceExecutor_ptr
TraceMgr_get_partial_trace_executor(const TraceMgr_ptr self,
                                    const char* name);

const char*
TraceMgr_get_partial_trace_executor_desc(const TraceMgr_ptr self,
                                         const char* name);

PartialTraceExecutor_ptr
TraceMgr_get_default_partial_trace_executor(const TraceMgr_ptr global_trace_manager);

/* Registration of layers */

void
TraceMgr_register_layer(TraceMgr_ptr self,
                        const char* layer_name);

void
TraceMgr_unregister_layer(TraceMgr_ptr self,
                          const char* layer_name);

boolean
TraceMgr_is_layer_registered(const TraceMgr_ptr self,
                             const char* layer_name);

array_t*
TraceMgr_get_registered_layers(const TraceMgr_ptr self);


/* Other Functions */

void
TraceMgr_set_current_trace_number(TraceMgr_ptr self,
                                      int trace_id);

int
TraceMgr_get_current_trace_number(TraceMgr_ptr self);

boolean
TraceMgr_is_visible_symbol(TraceMgr_ptr self, node_ptr symbol);

int TraceMgr_show_traces(TraceMgr_ptr const self,
                                const int plugin_index,
                                const boolean is_all,
                                const int trace,
                                TraceOpt_ptr const trace_opt,
                                const int traceno,
                                int from_state,
                                int to_state);

int
TraceMgr_execute_traces(TraceMgr_ptr const self,
                        CompleteTraceExecutor_ptr const executor,
                        const int first_trace,
                        const int last_trace);

int
TraceMgr_execute_partial_traces(TraceMgr_ptr const self,
                                PartialTraceExecutor_ptr const executor,
                                const int first_trace,
                                const int last_trace);

/* Functions related to Labels */

boolean
TraceMgr_is_label_valid(TraceMgr_ptr self, TraceLabel label);

TraceIter
TraceMgr_get_iterator_from_label(TraceMgr_ptr self,
                                     TraceLabel label);

int
TraceMgr_get_abs_index_from_label(TraceMgr_ptr self,
                                      TraceLabel label);

/* Interaction with trace plugins *********************************************/

int TraceMgr_get_plugin_size(const TraceMgr_ptr self);

int
TraceMgr_get_internal_plugin_size(const TraceMgr_ptr self);

TracePlugin_ptr
TraceMgr_get_plugin_at_index(const TraceMgr_ptr self,
                                 int index);

void TraceMgr_init_plugins(TraceMgr_ptr self);

int TraceMgr_register_plugin(TraceMgr_ptr self,
                                        TracePlugin_ptr plugin);

int TraceMgr_execute_plugin(const TraceMgr_ptr self,
                                       const TraceOpt_ptr opt,
                                       int plugin_index,
                                       int trace_index);

void
TraceMgr_set_default_plugin(TraceMgr_ptr self,
                                int plugin_id);

int
TraceMgr_get_default_plugin(TraceMgr_ptr self);

int TraceMgr_show_plugins(TraceMgr_ptr const self,
                                 const boolean is_show_all,
                                 const int dp);

boolean
TraceMgr_is_plugin_internal(const TraceMgr_ptr self, int index);

/******************************************************************************/


#endif /* __NUSMV_CORE_TRACE_TRACE_MGR_H__ */

---