Traces

Functions for handling Traces. More...

Collaboration diagram for Traces:

Modules
	Trace Getters
	Functions for getting information out of a Trace.

Macros
#define	NUXMV_VALID_TRACE(trace)   ((trace).repr != NULL)
	Valid trace type.

Functions
nuxmv_trace	nuxmv_make_trace_from_string (nuxmv_env env, nuxmv_trace_format fmt, const char *data, nuxmv_model model)
	Make a trace from string.
int	nuxmv_serialize_trace_to_string (nuxmv_env env, nuxmv_trace trace, nuxmv_trace_format fmt, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size)
	Serialize a trace to a string.
nuxmv_result	nuxmv_trace_check_property (nuxmv_env env, nuxmv_trace trace, nuxmv_property property, nuxmv_model model, const nuxmv_opt *opts, size_t opt_num)
	Check a property on a trace.

Detailed Description

Functions for handling Traces.

---

Macro Definition Documentation

NUXMV_VALID_TRACE

#define NUXMV_VALID_TRACE

(

trace

)

((trace).repr != NULL)

Valid trace type.

This macro checks whether trace is a valid nuxmv_trace.

Parameters

[in]

trace

The trace to inspect.

Returns

true if the option is valid, false otherwise.

Function Documentation

nuxmv_make_trace_from_string()

nuxmv_trace nuxmv_make_trace_from_string	(	nuxmv_env	env,
		nuxmv_trace_format	fmt,
		const char *	data,
		nuxmv_model	model
	)

Make a trace from string.

Parameters

[in]	env	The environment to modify.
[in]	fmt	The format of the input string.
[in]	data	A null-terminated string containing the trace data.
[in]	model	A model to attach the trace to.

Returns

The newly created trace corresponding to the string. In case of error, NUXMV_VALID_TRACE() evaluates to false.

See also

• nuxmv_trace_get_step_num()
• nuxmv_trace_get_function()
• nuxmv_trace_get_loopback()
• nuxmv_result_get_trace()
• nuxmv_serialize_trace_to_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.005

nuxmv_serialize_trace_to_string()

int nuxmv_serialize_trace_to_string	(	nuxmv_env	env,
		nuxmv_trace	trace,
		nuxmv_trace_format	fmt,
		nuxmv_serialized_chunk_callback	callback,
		void *	user_data,
		char *	data,
		size_t	data_size
	)

Serialize a trace to a string.

This function converts the given trace into a string representation using the specified format.

The output is written to the provided buffer. When the serialization process fills up the buffer:

• if a callback is not provided, a value equal to or greater than data_size is returned;
• if a callback is provided, it is invoked with the user-defined context.

The callback is responsible for handling the data chunk (e.g., copying it elsewhere). If the callback returns false, the process is aborted and the function returns the number of bytes written up to that point.

When the serialization process is completed successfully, the output buffer contains a null-terminated string and the callback is called, if any.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to serialize.
[in]	fmt	The format to use for serialization.
[in]	callback	Optional callback function invoked whenever the buffer is full or the serialization process is completed.
[in]	user_data	User-defined context passed to the callback.
[out]	data	The buffer where the serialized model will be stored.
[in]	data_size	The size of the data buffer.

Returns

• The total number of bytes written, including the terminating null byte, upon successful completion;
• a value equal to or greater than data_size, if no callback is provided and the serialized trace was truncated;
• the accumulated number of bytes for all successful calls of the callback, if the callback eventually requests to stop;
• -1 in case of error.

See also

• nuxmv_result_get_trace()
• nuxmv_make_trace_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_check_property()

nuxmv_result nuxmv_trace_check_property	(	nuxmv_env	env,
		nuxmv_trace	trace,
		nuxmv_property	property,
		nuxmv_model	model,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Check a property on a trace.

Parameters

[in]	env	The environment to inspect.
[in]	property	The property to check.
[in]	trace	A trace to check the property on.
[in]	model	A model for the trace.
[in]	opts	A list of options for the check. If no list shall be used it is safe to use NULL or the result of malloc(0), provided that opt_num=0.
[in]	opt_num	The number of options in the list. If no list shall be passed, use 0 as actual value of opt_num.

Returns

The result of the checking. In case of error, NUXMV_VALID_RESULT() evaluates to false.

See also

• NUXMV_COUNT_OF()
• nuxmv_property_check_satisfiability()
• nuxmv_simulation_get_result()
• nuxmv_model_check_deadlock()
• nuxmv_model_check_receptiveness()
• nuxmv_env_get_last_error_message()

Requirements: 02.006

Attention

This function has not been implemented, yet.