NuSMV/code/nusmv/core/trace/pkg_trace.h File Reference

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

Go to the source code of this file.

Functions
void	Trace_Eval_evaluate_defines (Trace_ptr trace)
	Force the evaluation of the defines of the trace.
int	Trace_execute_partial_trace (const NuSMVEnv_ptr env, const Trace_ptr trace, const PartialTraceExecutor_ptr exec_info, const NodeList_ptr language)
	Partial trace re-execution and fill-in.
int	Trace_execute_trace (const NuSMVEnv_ptr env, const Trace_ptr trace, const CompleteTraceExecutor_ptr exec_info)
	Complete trace re-execution.
int	TracePkg_execute_partial_traces (NuSMVEnv_ptr env, TraceMgr_ptr trace_mgr, FILE *output_stream, char *engine, int verbosity, int trace_no)
	Executes traces stored in the Trace Manager.
int	TracePkg_execute_traces (NuSMVEnv_ptr env, TraceMgr_ptr trace_mgr, FILE *output_stream, char *engine, int verbosity, int trace_no)
	Executes traces stored in the Trace Manager.
int	TracePkg_get_default_trace_plugin (TraceMgr_ptr gtm)
	Returns the trace plugin currently selected as default.
NodeList_ptr	TracePkg_get_filtered_symbols (TraceMgr_ptr gtm, const NodeList_ptr symbols)
	Returns the filtered list of symbols.
void	TracePkg_init (NuSMVEnv_ptr env)
	The header file for the trace package.
void	TracePkg_quit (NuSMVEnv_ptr env)
	Quits the Trace package.
Trace_ptr	TracePkg_read_trace (NuSMVEnv_ptr env, SexpFsm_ptr sexp_fsm, const char *filename, boolean halt_if_undef, boolean halt_if_wrong_section)
	Reads the trace from the specified file into the memory.
boolean	TracePkg_set_default_trace_plugin (TraceMgr_ptr gtm, int dp)
	Called when the user selects a trace plugin to be used as default.
bdd_ptr	TraceUtils_fetch_as_bdd (Trace_ptr trace, TraceIter step, TraceIteratorType iter_type, BddEnc_ptr bdd_enc)
	Extracts assignments in (trace, step) to a set of symbols.
be_ptr	TraceUtils_fetch_as_be (Trace_ptr trace, TraceIter step, TraceIteratorType iter_type, BeEnc_ptr be_enc, BddEnc_ptr bdd_enc)
	Extracts assignments in (trace, step) to a set of symbols.
Expr_ptr	TraceUtils_fetch_as_big_and (Trace_ptr trace, TraceIter step, TraceIteratorType iter_type)
	Extracts assignments in (trace, step) to a set of symbols.
Expr_ptr	TraceUtils_fetch_as_sexp (Trace_ptr trace, TraceIter step, TraceIteratorType iter_type)
	Extracts assignments in (trace, step) to a set of symbols.

---

Function Documentation

void Trace_Eval_evaluate_defines

(

Trace_ptr

trace

)

Force the evaluation of the defines of the trace.

Useful for use the trace even if the encoder is destroyed

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

Partial trace re-execution and fill-in.

Partial trace re-execution and fill-in.

Tries to complete the given trace using the given incomplete trace executor. If successful, a complete trace is registered into the Trace Manager.

0 is returned if trace could be succesfully completed. 1 is returned otherwise

None

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

Complete trace re-execution.

Complete trace re-execution. In order to be run, the trace must be complete w.r.t. master fsm language. Returns 0 if a trace is executed successfully, and 1 otherwise.

None

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

Executes traces stored in the Trace Manager.

if trace_no equals to zero, all the traces will be executed

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

Executes traces stored in the Trace Manager.

if trace_no equals to zero, all the traces will be executed

int TracePkg_get_default_trace_plugin

(

TraceMgr_ptr

gtm

)

Returns the trace plugin currently selected as default.

Returns the trace plugin currently selected as default

NodeList_ptr TracePkg_get_filtered_symbols	(	TraceMgr_ptr	gtm,
		const NodeList_ptr	symbols
	)

Returns the filtered list of symbols.

Returned list is the result of filtering the input list, using standard filtering strategies that apply to symbols in traces.

The returned list must be freed by the caller

See also:

TraceMgr_is_visible_symbol

void TracePkg_init

(

NuSMVEnv_ptr

env

)

The header file for the trace package.

Author:

Ashutosh Trivedi, Marco Pensallorto

Todo:

: Missing description

AutomaticStart

Initializes the Trace Package. TraceMgr get initialized.

See also:

TracePkg_quit

void TracePkg_quit

(

NuSMVEnv_ptr

env

)

Quits the Trace package.

See also:

TracePkg_init

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

Reads the trace from the specified file into the memory.

In case of error, NULL is returned. The trace will be stored in the tracemgr, that has the ownership

boolean TracePkg_set_default_trace_plugin	(	TraceMgr_ptr	gtm,
		int	dp
	)

Called when the user selects a trace plugin to be used as default.

Returns true upon success, false otherwise

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

Extracts assignments in (trace, step) to a set of symbols.

Builds a bdd representing the assignments from a given step in trace. The symbols to be assigned are picked according to \"iter_type\". Refer to documentation of the TraceIteratorType for possible sets.

Remarks: returned bdd is referenced

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

Extracts assignments in (trace, step) to a set of symbols.

Builds a be representing the assignments from a given step in trace. The symbols to be assigned are picked according to \"iter_type\". Refer to documentation of the TraceIteratorType for possible sets.

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

Extracts assignments in (trace, step) to a set of symbols.

Do the same thing as TraceUtils_fetch_as_sexp, but do not simplify or reorder the pointers of expressions created.

See also:

TraceUtils_fetch_as_sexp

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

Extracts assignments in (trace, step) to a set of symbols.

Builds a sexp representing the assignments from a given step in trace. The symbols to be assigned are picked according to \"iter_type\". Refer to documentation of the TraceIteratorType for possible sets.

Remarks: returned expression is find-node'd

See also:

TraceUtils_fetch_as_big_and