NuSMV/code/nusmv/core/trace/pkg_trace.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_PKG_TRACE_H__
#define __NUSMV_CORE_TRACE_PKG_TRACE_H__

#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/trace/exec/traceExec.h"
#include "nusmv/core/cinit/NuSMVEnv.h"
/* #include "trace/exec/TraceExecInfo.h" */



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

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

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

/* package */

void TracePkg_init(NuSMVEnv_ptr env);

void TracePkg_quit(NuSMVEnv_ptr env);

/* self-test */
#if defined TRACE_DEBUG

int TracePkg_test_package(FILE* out, FILE* err);
#endif

/* Filtering services for external packags */

NodeList_ptr
TracePkg_get_filtered_symbols(TraceMgr_ptr gtm,
                              const NodeList_ptr symbols);

/* Trace Manager */

int TracePkg_get_default_trace_plugin(TraceMgr_ptr gtm);

boolean TracePkg_set_default_trace_plugin(TraceMgr_ptr gtm,
                                                 int dp);

/* Trace execution */

int
Trace_execute_trace(const NuSMVEnv_ptr env,
                    const Trace_ptr trace,
                    const CompleteTraceExecutor_ptr exec_info);

int
Trace_execute_partial_trace(const NuSMVEnv_ptr env,
                            const Trace_ptr trace,
                            const PartialTraceExecutor_ptr exec_info,
                            const NodeList_ptr language);

/* Custom value fetch functions */

bdd_ptr
TraceUtils_fetch_as_bdd(Trace_ptr trace, TraceIter step,
                        TraceIteratorType iter_type,
                        BddEnc_ptr bdd_enc);

be_ptr
TraceUtils_fetch_as_be(Trace_ptr trace, TraceIter step,
                       TraceIteratorType iter_type,
                       BeEnc_ptr be_enc, BddEnc_ptr bdd_enc);

Expr_ptr
TraceUtils_fetch_as_sexp(Trace_ptr trace, TraceIter step,
                         TraceIteratorType iter_type);

Expr_ptr
TraceUtils_fetch_as_big_and(Trace_ptr trace, TraceIter step,
                            TraceIteratorType iter_type);

void Trace_Eval_evaluate_defines(Trace_ptr trace);

Trace_ptr TracePkg_read_trace(NuSMVEnv_ptr env,
                                     SexpFsm_ptr sexp_fsm,
                                     const char* filename,
                                     boolean halt_if_undef,
                                     boolean halt_if_wrong_section);

int TracePkg_execute_traces(NuSMVEnv_ptr env,
                                   TraceMgr_ptr trace_mgr,
                                   FILE* output_stream,
                                   char* engine,
                                   int verbosity,
                                   int trace_no);

int TracePkg_execute_partial_traces(NuSMVEnv_ptr env,
                                           TraceMgr_ptr trace_mgr,
                                           FILE* output_stream,
                                           char* engine,
                                           int verbosity,
                                           int trace_no);
           
#endif /* __TRACE__H  */

---