Trace Struct Reference

#include <Trace_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
boolean	allow_bits
node_ptr *	buckets [TRACE_SECTION_END]
const char *	desc
TraceVarFrame_ptr	first_frame
boolean	frozen
TraceFrozenFrame_ptr	frozen_frame
NodeList_ptr	i_vars
int	id
boolean	is_volatile
TraceVarFrame_ptr	last_frame
unsigned	length
unsigned	n_buckets [TRACE_SECTION_END]
NodeList_ptr	s_vars
NodeList_ptr	sf_vars
SymbTable_ptr	st
hash_ptr	symb2address
hash_ptr	symb2layername
hash_ptr	symb2section
NodeList_ptr	symbols
TraceType	type
Related Functions
(Note that these are not member functions.)
TraceIter	trace_append_step (Trace_ptr self)
TraceIter	Trace_append_step (Trace_ptr self)
	Extends a trace by adding a new step to it.
Trace_ptr	trace_concat (Trace_ptr self, Trace_ptr *other)
Trace_ptr	Trace_concat (Trace_ptr self, Trace_ptr *other)
	Trace concatenation.
Trace_ptr	trace_copy (Trace_ptr self, TraceIter until_here, boolean is_volatile)
Trace_ptr	Trace_copy (const Trace_ptr self, const TraceIter until_here, boolean is_volatile)
	Trace class copy constructor.
boolean	Trace_covers_language (const Trace_ptr self, NodeList_ptr symbols)
	Tests whether all given symbols are in \"self\"'s language.
Trace_ptr	Trace_create (SymbTable_ptr st, const char *desc, const TraceType type, NodeList_ptr symbols, boolean is_volatile)
	Trace class constructor.
Trace_ptr	Trace_create_allow_bits (SymbTable_ptr st, const char *desc, const TraceType type, NodeList_ptr symbols, boolean is_volatile)
	Trace class constructor.
void	trace_destroy (Trace_ptr self)
void	Trace_destroy (Trace_ptr self)
	Trace class destructor.
boolean	trace_equals (const Trace_ptr self, const Trace_ptr other)
boolean	Trace_equals (const Trace_ptr self, const Trace_ptr other)
	Equality predicate between traces.
TraceIter	trace_first_iter (const Trace_ptr self)
TraceIter	Trace_first_iter (const Trace_ptr self)
	Returns a trace iterator pointing to the first step of the trace.
void	trace_freeze (Trace_ptr self)
void	Trace_freeze (Trace_ptr self)
	Freezes a trace.
const char *	trace_get_desc (const Trace_ptr self)
const char *	Trace_get_desc (const Trace_ptr self)
	Gets the description of given trace.
int	Trace_get_first_loopback_from (const Trace_ptr self, TraceIter *step)
	Returns the first loopback found on self from step.
NodeList_ptr	trace_get_i_vars (const Trace_ptr self)
NodeList_ptr	Trace_get_i_vars (const Trace_ptr self)
	Exposes the list of input vars in trace language.
int	trace_get_id (const Trace_ptr self)
int	Trace_get_id (const Trace_ptr self)
	Gets the id of given trace.
const char *	trace_get_layer_from_symb (const Trace_ptr self, const node_ptr symb)
unsigned	trace_get_length (const Trace_ptr self)
unsigned	Trace_get_length (const Trace_ptr self)
	Gets the length of the trace.
NodeList_ptr	trace_get_s_vars (const Trace_ptr self)
NodeList_ptr	Trace_get_s_vars (const Trace_ptr self)
	Exposes the list of state vars in trace language.
NodeList_ptr	trace_get_sf_vars (const Trace_ptr self)
NodeList_ptr	Trace_get_sf_vars (const Trace_ptr self)
	Exposes the list of state-frozen vars in trace language.
SymbTable_ptr	trace_get_symb_table (Trace_ptr self)
SymbTable_ptr	Trace_get_symb_table (Trace_ptr self)
	Exposes Trace internal symbol table.
NodeList_ptr	trace_get_symbols (const Trace_ptr self)
NodeList_ptr	Trace_get_symbols (const Trace_ptr self)
	Exposes the list of symbols in trace language.
TraceType	trace_get_type (const Trace_ptr self)
TraceType	Trace_get_type (const Trace_ptr self)
	Gets the type of the trace.
boolean	Trace_has_loopback (const Trace_ptr self)
	Checks if a Trace has at least one loopback.
boolean	Trace_is_complete (Trace_ptr self, NodeList_ptr vars, boolean report)
	Checks if a Trace is complete on the given set of vars.
boolean	trace_is_complete_vars (const Trace_ptr self, const NodeList_ptr vars, FILE *report_stream)
boolean	trace_is_empty (const Trace_ptr self)
boolean	Trace_is_empty (const Trace_ptr self)
	Checks whether the trace is empty or not.
boolean	trace_is_frozen (const Trace_ptr self)
boolean	Trace_is_frozen (const Trace_ptr self)
	Determine whether the \"self\" trace is frozen.
boolean	trace_is_registered (Trace_ptr self)
boolean	Trace_is_registered (const Trace_ptr self)
	Checks whether trace is registered with the trace manager.
boolean	trace_is_thawed (const Trace_ptr self)
boolean	Trace_is_thawed (const Trace_ptr self)
	Determine whether the \"self\" trace is thawed.
boolean	trace_is_volatile (const Trace_ptr self)
boolean	Trace_is_volatile (const Trace_ptr self)
	Determine whether the \"self\" trace is volatile.
unsigned	trace_iter_i (const Trace_ptr self, TraceIter iter)
TraceIter	trace_ith_iter (const Trace_ptr self, unsigned i)
TraceIter	Trace_ith_iter (const Trace_ptr self, unsigned i)
	Returns a trace iterator pointing to the i-th step of the trace.
TraceIter	trace_last_iter (const Trace_ptr self)
TraceIter	Trace_last_iter (const Trace_ptr self)
	Returns a trace iterator pointing to the last step of the trace.
void	Trace_print_loopbacks (const Trace_ptr self, OStream_ptr stream)
	Prints available loopbacks in self.
void	trace_register (Trace_ptr self, int id)
void	Trace_register (const Trace_ptr self, int id)
	Sets the id of given trace.
void	trace_set_desc (Trace_ptr self, const char *desc)
void	Trace_set_desc (const Trace_ptr self, const char *desc)
	Sets the description of given trace.
void	trace_set_type (Trace_ptr self, TraceType trace_type)
void	Trace_set_type (Trace_ptr self, TraceType trace_type)
	Sets the type of the trace.
boolean	trace_step_check_defines (Trace_ptr self, const TraceIter step, NodeList_ptr failures)
void	trace_step_evaluate_defines (Trace_ptr self, const TraceIter step)
	Evaluates defines for a trace.
void	trace_step_force_loopback (const Trace_ptr self, TraceIter step)
void	Trace_step_force_loopback (const Trace_ptr self, TraceIter step)
	Forces a loopback on a frozen trace.
node_ptr	trace_step_get_value (const Trace_ptr self, const TraceIter step, const node_ptr symb)
node_ptr	Trace_step_get_value (const Trace_ptr self, TraceIter step, node_ptr symb)
	Retrieves an assignment from a trace step.
boolean	trace_step_is_loopback (const Trace_ptr self, const TraceIter step)
boolean	Trace_step_is_loopback (const Trace_ptr self, TraceIter step)
	Tests whether state is \"step\" is a loopback state w.r.t the last state in \"self\".
TraceStepIter	trace_step_iter (const Trace_ptr self, const TraceIter step, TraceIteratorType iter_type)
TraceStepIter	Trace_step_iter (const Trace_ptr self, const TraceIter step, const TraceIteratorType iter_type)
	Step iterator factory constructor.
boolean	trace_step_put_value (Trace_ptr self, const TraceIter step, const node_ptr symb, const node_ptr value)
boolean	Trace_step_put_value (Trace_ptr self, TraceIter step, node_ptr symb, node_ptr value)
	Stores an assignment into a trace step.
boolean	trace_step_test_loopback (Trace_ptr self, const TraceIter step)
node_ptr	trace_symbol_bwd_lookup (Trace_ptr self, TraceSection section, unsigned offset)
boolean	trace_symbol_fwd_lookup (Trace_ptr self, node_ptr symb, TraceSection section, unsigned index)
SymbCategory	trace_symbol_get_category (Trace_ptr self, node_ptr symb)
boolean	trace_symbol_in_language (const Trace_ptr self, const node_ptr symb)
boolean	Trace_symbol_in_language (const Trace_ptr self, node_ptr symb)
	Tests whether a symbol is \"self\"'s language.
boolean	trace_symbol_is_assigned (const Trace_ptr self, const TraceIter step, node_ptr symb)
boolean	Trace_symbol_is_assigned (Trace_ptr self, TraceIter step, node_ptr symb)
	Checks if given symbol is assigned at given step.
TraceSymbolsIter	trace_symbols_iter (const Trace_ptr self, TraceIteratorType iter_type)
TraceSymbolsIter	Trace_symbols_iter (const Trace_ptr self, const TraceIteratorType iter_type)
	Symbols iterator factory constructor.
void	trace_thaw (Trace_ptr self)
void	Trace_thaw (Trace_ptr self)
	Thaws a trace.
void	trace_unregister (Trace_ptr self)
void	Trace_unregister (const Trace_ptr self)
	Unregisters a trace.
boolean	Trace_validate_loopback (const Trace_ptr self, int loopback_idx)
	Checks if loopback_idx is a valid loopback on Trace.

Detailed Description

Trace Class.

The header file for the Trace class.

This class contains informations about a Trace:

id: Unique ID of the registered traces. -1 for unregistered traces.
desc: Description of the trace.
length: Diameter of the trace. (i.e. the number of transitions)
type: Type of the trace.
first_step: Pointer to the first step of the doubly linked list of TraceSteps.
last_node: Pointer to the last node of the doubly linked list of TraceSteps.
defines_evaluated: Internal index used to perform lazy evaluation of defines.
symb2index: Symbol to index hash table for fast look-up.

Author:: Marco Pensallorto optional

Todo:: Missing synopsis

Todo:: Missing description

Member Function Documentation

Trace::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

TraceIter trace_append_step ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

TraceIter Trace_append_step ( Trace_ptr self ) [related]

Extends a trace by adding a new step to it.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

The returned step can be used as parameter to all Trace_step_xxx functions

See also:: Trace_create, Trace_step_put_value, Trace_step_get_value, Trace_step_get_iter, Trace_step_get_next_value

Trace_ptr trace_concat	(	Trace_ptr	self,
		Trace_ptr *	other
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

Trace_ptr Trace_concat	(	Trace_ptr	self,
		Trace_ptr *	other
	)			`[related]`

Trace concatenation.

Destructively* concatenates \"other\" to \"self\". That is, \"self\" is appended all available data about variables and defines from \"*other\". Frozen vars and state vars of the conjunction state for both \"self\" and \"other\" traces are synctactically checked for consistency. Their values are merged in the resulting trace.

Warning: an internal error is raised if an inconsistency is detected.

Returned valued is \"self\".

\"self\" is extended, \"*other\" is destroyed and its pointer is set to NULL.

Trace_ptr trace_copy	(	Trace_ptr	self,
		TraceIter	until_here,
		boolean	is_volatile
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

Trace_ptr Trace_copy	(	const Trace_ptr	self,
		const TraceIter	until_here,
		boolean	is_volatile
	)			`[related]`

Trace class copy constructor.

Returns an independent copy of \"self\" trace. If a non-NULL \"until_here\" iterator is passed copying process halts when \"until_here\" iterator has been reached. To obtain a full copy, pass TRACE_END_ITER as the \"until_here\" paramter. Loopback information is propagated to the copy only if a full copy is required.

If the trace is not volatile, all trace structures are internally duplicated in an independent copy. Same for volatile traces, made exception for the symbol table, since only a reference of the original trace's symbol table will be retained. In this case, the caller must take care of the original trace symbol table, which must NOT be freed until the created trace instance is destroyed. In detail:

If the original trace is volatile, then it's copy is valid unless the symbol table given at creation time is destroyed. In all other cases, the returned trace is valid.

If the original trace is not volatile, then the returned copy is valid as long as the original trace is valid.

Notice that a volatile copy "C" of a volatile copy "B" of a non-volatile trace "A" needs "A" to exist, and so on.

Remarks:

The full copy of a frozen trace is a frozen trace. Partial copies are always thawed.

See also:: Trace_thaw, Trace_freeze, Trace_destroy

boolean Trace_covers_language	(	const Trace_ptr	self,
		NodeList_ptr	symbols
	)			`[related]`

Tests whether all given symbols are in \"self\"'s language.

Returns true iff all symbols are part of the language defined for \"self\" defined at creation time.

required

See also:: optional

Trace_ptr Trace_create	(	SymbTable_ptr	st,
		const char *	desc,
		const TraceType	type,
		NodeList_ptr	symbols,
		boolean	is_volatile
	)			`[related]`

Trace class constructor.

AutomaticStart

Allocates and initializes a trace. In NuSMV, a trace is an engine-independent description of a computation path for some FSM. The newly created trace is associated with a language, that is a set of symbols (variables and defines) that can occur in the trace. Notice that bits (from boolean encoding) are not allowed in the language. To allow bits, use create_allow_bits.

In addition, a description and a type can be given to a trace.

If the trace is not volatile, all input parameters are internally duplicated in an independent copy. The caller is responsible for freeing them. Same for volatile traces, made exception for the symbol table, since only a reference will be retained. In this case, the caller is responsible for freeing them, and take care of the symbol table, which must NOT be freed until the created trace instance is destroyed.

Remarks:

First step is already allocated for the returned trace. Use Trace_first_iter to obtain a valid iterator pointing to the initial step. Use Trace_add_step to append further steps.

See also:: Trace_first_iter, Trace_append_step, Trace_destroy

Trace_ptr Trace_create_allow_bits	(	SymbTable_ptr	st,
		const char *	desc,
		const TraceType	type,
		NodeList_ptr	symbols,
		boolean	is_volatile
	)			`[related]`

Trace class constructor.

Allocates and initializes a trace. In NuSMV, a trace is an engine-independent description of a computation path for some FSM. The newly created trace is associated with a language, that is a set of symbols (variables and defines) that can occur in the trace. Bits (from boolean encoding) are allowed in the language, along with their corresponding scalar variables if needed.

In addition, a description and a type can be given to a trace.

If the trace is not volatile, all input parameters are internally duplicated in an independent copy. The caller is responsible for freeing them. Same for volatile traces, made exception for the symbol table, since only a reference will be retained. In this case, the caller is responsible for freeing them, and take care of the symbol table, which must NOT be freed until the created trace instance is destroyed.

Remarks:

First step is already allocated for the returned trace. Use Trace_first_iter to obtain a valid iterator pointing to the initial step. Use Trace_add_step to append further steps.

See also:: Trace_first_iter, Trace_append_step, Trace_destroy

void trace_destroy ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

void Trace_destroy ( Trace_ptr self ) [related]

Trace class destructor.

Frees all the resources used by \"self\" trace instance

See also:: Trace_create, Trace_copy

boolean trace_equals	(	const Trace_ptr	self,
		const Trace_ptr	other
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_equals	(	const Trace_ptr	self,
		const Trace_ptr	other
	)			`[related]`

Equality predicate between traces.

Two traces are equals iff:

1. They're the same object or NULL.

or

2. They have exactly the same language, length, assignments for all variables in all times and the same loopbacks.

(Defines are not taken into account for equality.)

They need not be both frozen of thawed, neither being both registered or unregistered. (Of course two traces cannot* have the same ID).

required

See also:: optional

TraceIter trace_first_iter ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

TraceIter Trace_first_iter ( const Trace_ptr self ) [related]

Returns a trace iterator pointing to the first step of the trace.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

The returned step can be used as parameter to all Trace_step_xxx functions.

Remarks:

the first step holds *no* input information.

See also:: Trace_last_iter

void trace_freeze ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

void Trace_freeze ( Trace_ptr self ) [related]

Freezes a trace.

A frozen trace holds explicit information about loopbacks. Its length and assignments are immutable, that is it cannot be appended more steps, nor can it accept more values that those already stored in it.

Still it is possible to register/unregister the trace and to change its type or description.

required

See also:: optional

const char * trace_get_desc ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

const char * Trace_get_desc ( const Trace_ptr self ) [related]

Gets the description of given trace.

int Trace_get_first_loopback_from	(	const Trace_ptr	self,
		TraceIter *	step
	)			`[related]`

Returns the first loopback found on self from step.

Search for the first loopback on trace from step and return its id. In case there is no loopbacks returns -1. Remark: step can be NULL to indicate to start from the first step.

None

NodeList_ptr trace_get_i_vars ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

NodeList_ptr Trace_get_i_vars ( const Trace_ptr self ) [related]

Exposes the list of input vars in trace language.

Returned list belongs to \"self\". Do not change or dispose it.

required

See also:: optional

int trace_get_id ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

int Trace_get_id ( const Trace_ptr self ) [related]

Gets the id of given trace.

Returns the ID of given trace. A valid id is a non-negative number.

const char * trace_get_layer_from_symb	(	const Trace_ptr	self,
		const node_ptr	symb
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

unsigned trace_get_length ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

unsigned Trace_get_length ( const Trace_ptr self ) [related]

Gets the length of the trace.

Length for a trace is defined as the number of the transitions in it. Thus, a trace consisting only of an initial state is a 0-length trace. A trace with two states is a 1-length trace and so forth.

See also:: TraceType

NodeList_ptr trace_get_s_vars ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

NodeList_ptr Trace_get_s_vars ( const Trace_ptr self ) [related]

Exposes the list of state vars in trace language.

Returned list belongs to \"self\". Do not change or dispose it.

required

See also:: optional

NodeList_ptr trace_get_sf_vars ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

NodeList_ptr Trace_get_sf_vars ( const Trace_ptr self ) [related]

Exposes the list of state-frozen vars in trace language.

Returned list belongs to \"self\". Do not change or dispose it.

required

See also:: optional

SymbTable_ptr trace_get_symb_table ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

SymbTable_ptr Trace_get_symb_table ( Trace_ptr self ) [related]

Exposes Trace internal symbol table.

Returns the trace symbol table. The symbol table is owned by the trace and should *not* be modified in any way.

required

See also:: optional

NodeList_ptr trace_get_symbols ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

NodeList_ptr Trace_get_symbols ( const Trace_ptr self ) [related]

Exposes the list of symbols in trace language.

Returned list belongs to \"self\". Do not change or dispose it.

required

See also:: optional

TraceType trace_get_type ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

TraceType Trace_get_type ( const Trace_ptr self ) [related]

Gets the type of the trace.

For a list of see definition of TraceType enum

See also:: TraceType

boolean Trace_has_loopback ( const Trace_ptr self ) [related]

Checks if a Trace has at least one loopback.

Return true iff a Trace has at least one loopback

None

boolean Trace_is_complete	(	Trace_ptr	self,
		NodeList_ptr	vars,
		boolean	report
	)			`[related]`

Checks if a Trace is complete on the given set of vars.

Checks if a Trace is complete on the given set of vars

None

boolean trace_is_complete_vars	(	const Trace_ptr	self,
		const NodeList_ptr	vars,
		FILE *	report_stream
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean trace_is_empty ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_is_empty ( const Trace_ptr self ) [related]

Checks whether the trace is empty or not.

A trace is empty if the length is 0 and there are no assignments in the initial states

See also:: TraceType

boolean trace_is_frozen ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_is_frozen ( const Trace_ptr self ) [related]

Determine whether the \"self\" trace is frozen.

A frozen trace holds explicit information about loopbacks and can not be appended a step, or added a variable value.

Warning: after freezing no automatic looback calculation will be performed: it is up to the owner of the trace to manually add loopback information using Trace_step_force_loopback.

required

See also:: optional

boolean trace_is_registered ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_is_registered ( const Trace_ptr self ) [related]

Checks whether trace is registered with the trace manager.

boolean trace_is_thawed ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_is_thawed ( const Trace_ptr self ) [related]

Determine whether the \"self\" trace is thawed.

A thawed trace holds no explicit information about loopbacks and can be appended a step and

Warning: after thawing the trace will not persistently retain any loopback information. In particular it is illegal* to force a loopback on a thawed trace.

required

See also:: optional

boolean trace_is_volatile ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_is_volatile ( const Trace_ptr self ) [related]

Determine whether the \"self\" trace is volatile.

A volatile trace does not own a symbol table instance, so it is valid as long as the symbol table does not change and is available. A non-volatile trace instead owns a copy of the symbol table given at construction time and is completely independand among system changes over time

unsigned trace_iter_i	(	const Trace_ptr	self,
		TraceIter	iter
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

TraceIter trace_ith_iter	(	const Trace_ptr	self,
		unsigned	i
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

TraceIter Trace_ith_iter	(	const Trace_ptr	self,
		unsigned	i
	)			`[related]`

Returns a trace iterator pointing to the i-th step of the trace.

Returns a trace iterator pointing to the i-th step of the trace. Counting starts at 1. Thus, here is the sequence of first k steps for a trace.

S1 i2 S2 i3 S3 ... ik Sk

Remarks:

the first step holds *no* input information.

See also:: Trace_first_iter, Trace_last_iter

TraceIter trace_last_iter ( const Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

TraceIter Trace_last_iter ( const Trace_ptr self ) [related]

Returns a trace iterator pointing to the last step of the trace.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

The returned step can be used as parameter to all Trace_step_xxx functions

See also:: Trace_first_iter

void Trace_print_loopbacks	(	const Trace_ptr	self,
		OStream_ptr	stream
	)			`[related]`

Prints available loopbacks in self.

Prints available loopbacks in self

None

void trace_register	(	Trace_ptr	self,
		int	id
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

void Trace_register	(	const Trace_ptr	self,
		int	id
	)			`[related]`

Sets the id of given trace.

Sets the ID of the given trace. A valid ID is a non-negative number.

void trace_set_desc	(	Trace_ptr	self,
		const char *	desc
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

void Trace_set_desc	(	const Trace_ptr	self,
		const char *	desc
	)			`[related]`

Sets the description of given trace.

The string in \"desc\" is duplicated inside the trace. The caller can dispose the actual parameter.

Remarks: NIL(char) is accepted as a non-descriptive description.

void trace_set_type	(	Trace_ptr	self,
		TraceType	trace_type
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

void Trace_set_type	(	Trace_ptr	self,
		TraceType	trace_type
	)			`[related]`

Sets the type of the trace.

For a list of see definition of TraceType enum

See also:: TraceType

boolean trace_step_check_defines	(	Trace_ptr	self,
		const TraceIter	step,
		NodeList_ptr	failures
	)			`[related]`

void trace_step_evaluate_defines	(	Trace_ptr	self,
		const TraceIter	step
	)			`[related]`

Evaluates defines for a trace.

Evaluates define for a trace, based on assignments to state, frozen and input variables.

If a previous value exists for a define, The mismatch is reported to the caller by appending a failure node describing the error to the "failures" list. If "failures" is NULL failures are silently discarded. If no previous value exists for a given define, assigns the define to the calculated value according to vars assignments. The "failures" list must be either NULL or a valid, empty list.

0 is returned if no mismatching were detected, 1 otherwise

The trace is filled with defines, failures list is populated as necessary.

void trace_step_force_loopback	(	const Trace_ptr	self,
		TraceIter	step
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

void Trace_step_force_loopback	(	const Trace_ptr	self,
		TraceIter	step
	)			`[related]`

Forces a loopback on a frozen trace.

Use this function to store explicit loopback information in a frozen trace. The trace will retain loopback data until being thawed again.

required

See also:: optional

node_ptr trace_step_get_value	(	const Trace_ptr	self,
		const TraceIter	step,
		const node_ptr	symb
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

node_ptr Trace_step_get_value	(	const Trace_ptr	self,
		TraceIter	step,
		node_ptr	symb
	)			`[related]`

Retrieves an assignment from a trace step.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

\"step\" must be a valid step for the trace. \"symb\" must belong to the language associated to the trace at creation time. The value stored into the step is returned or Nil if no such value exists.

Remarks: An internal error is raised if \"symb\" is not in trace language.

See also:: Trace_create, Trace_step_put_value, Trace_step_get_value, Trace_step_get_iter, Trace_step_get_next_value

boolean trace_step_is_loopback	(	const Trace_ptr	self,
		const TraceIter	step
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_step_is_loopback	(	const Trace_ptr	self,
		TraceIter	step
	)			`[related]`

Tests whether state is \"step\" is a loopback state w.r.t the last state in \"self\".

This function behaves accordingly to two different modes a trace can be: frozen or thawed(default).

If the trace is frozen, permanent loopback information is used to determine if \"step\" has a loopback state. No further loopback computation is made.

If the trace is thawed, dynamic loopback calculation takes place, using a variant of Rabin-Karp pattern matching algorithm

See also:: Trace_create, Trace_step_put_value, Trace_step_get_value, Trace_step_get_iter, Trace_step_get_next_value

TraceStepIter trace_step_iter	(	const Trace_ptr	self,
		const TraceIter	step,
		TraceIteratorType	iter_type
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

TraceStepIter Trace_step_iter	(	const Trace_ptr	self,
		const TraceIter	step,
		const TraceIteratorType	iter_type
	)			`[related]`

Step iterator factory constructor.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

\"step\" must be a valid step for the trace. An iterator over the assignments in \"step\" is returned. This iterator can be used with Trace_step_iter_fetch.

Hint: do not use this function. Use TRACE_STEP_FOREACH macro instead (it is way easier and more readable).

See also:: TRACE_STEP_FOREACH

boolean trace_step_put_value	(	Trace_ptr	self,
		const TraceIter	step,
		const node_ptr	symb,
		const node_ptr	value
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_step_put_value	(	Trace_ptr	self,
		TraceIter	step,
		node_ptr	symb,
		node_ptr	value
	)			`[related]`

Stores an assignment into a trace step.

A step is a container for incoming input and next state(i.e. it has the form <i, S>)

\"step\" must be a valid step for the trace. If symb belongs to the language associated to the trace at creation time, the normalized value of \"value\" is stored into the step. Assignment is checked for type correctness.

Returns true iff the value was succesfully assigned to symb in given step of self.

Remarks:

Assignments to symbols not in trace language are silently ignored.

See also:: Trace_append_step, Trace_step_get_value

boolean trace_step_test_loopback	(	Trace_ptr	self,
		const TraceIter	step
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

node_ptr trace_symbol_bwd_lookup	(	Trace_ptr	self,
		TraceSection	section,
		unsigned	offset
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean trace_symbol_fwd_lookup	(	Trace_ptr	self,
		node_ptr	symb,
		TraceSection *	section,
		unsigned *	index
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

SymbCategory trace_symbol_get_category	(	Trace_ptr	self,
		node_ptr	symb
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean trace_symbol_in_language	(	const Trace_ptr	self,
		const node_ptr	symb
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_symbol_in_language	(	const Trace_ptr	self,
		node_ptr	symb
	)			`[related]`

Tests whether a symbol is \"self\"'s language.

Returns true iff symb is part of the language defined for \"self\" defined at creation time.

required

See also:: optional

boolean trace_symbol_is_assigned	(	const Trace_ptr	self,
		const TraceIter	step,
		node_ptr	symb
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

boolean Trace_symbol_is_assigned	(	Trace_ptr	self,
		TraceIter	step,
		node_ptr	symb
	)			`[related]`

Checks if given symbol is assigned at given step.

Returns true iff given symbols is assigned at given step. Remarks: An internal error is raised if \"symb\" is not in trace language.

See also:: Trace_step_get_value

TraceSymbolsIter trace_symbols_iter	(	const Trace_ptr	self,
		TraceIteratorType	iter_type
	)			`[related]`

Todo:: Missing synopsis

Todo:: Missing description

TraceSymbolsIter Trace_symbols_iter	(	const Trace_ptr	self,
		const TraceIteratorType	iter_type
	)			`[related]`

Symbols iterator factory constructor.

An iterator over the symbols in \"self\" is returned. This iterator can be used with Trace_symbols_iter_fetch.

Hint: do not use this function. Use TRACE_SYMBOLS_FOREACH macro instead (it is way easier and more readable).

See also:: TRACE_SYMBOLS_FOREACH

void trace_thaw ( Trace_ptr self ) [related]

Todo:: Missing synopsis

Todo:: Missing description

void Trace_thaw ( Trace_ptr self ) [related]

Thaws a trace.

A thawed traces holds no explicit information about loopbacks and can be appended a step and added values in the customary trace building process.

Warning: after thawing the trace will not persistently retain any loopback information. In particular it is illegal* to force a loopback on a thawed trace.

required