Trace Getters

Functions for getting information out of a Trace. More...

Collaboration diagram for Trace Getters:

Macros
#define	NUXMV_VALID_TRACE_VALUE(symb_val)
	Valid trace value.

Functions
int	nuxmv_trace_get_step_num (nuxmv_env env, nuxmv_trace trace)
	Get the number of steps in a trace.
int	nuxmv_trace_get_step_state_num (nuxmv_env env, nuxmv_trace trace, int step_idx)
	Get the number of state variables in a trace.
nuxmv_trace_value	nuxmv_trace_get_step_state (nuxmv_env env, nuxmv_trace trace, int step_idx, int var_idx)
	Get the value of a state variable from the i-th step of a trace.
int	nuxmv_trace_get_step_input_num (nuxmv_env env, nuxmv_trace trace, int step_idx)
	Get the number of input variables in a trace.
nuxmv_trace_value	nuxmv_trace_get_step_input (nuxmv_env env, nuxmv_trace trace, int step_idx, int var_idx)
	Get the value of an input variable from the i-th step of a trace.
int	nuxmv_trace_get_step_define_num (nuxmv_env env, nuxmv_trace trace, int step_idx)
	Get the number of defines in a trace.
nuxmv_trace_value	nuxmv_trace_get_step_define (nuxmv_env env, nuxmv_trace trace, int step_idx, int def_idx)
	Get the value of a define from the i-th step of a trace.
int	nuxmv_trace_get_function_num (nuxmv_env env, nuxmv_trace trace)
	Get the number of uninterpreted functions in a trace.
nuxmv_trace_value	nuxmv_trace_get_function (nuxmv_env env, nuxmv_trace trace, int fun_idx)
	Get the value of a uninterpreted function from a trace.
int	nuxmv_trace_get_loopback (nuxmv_env env, nuxmv_trace trace)
	Get the the step the trace loops back, if any.

Detailed Description

Functions for getting information out of a Trace.

---

Macro Definition Documentation

NUXMV_VALID_TRACE_VALUE

#define NUXMV_VALID_TRACE_VALUE

(

symb_val

)

Value:

    (NUXMV_VALID_EXPR((symb_val).identifier) &&                                \
     NUXMV_VALID_EXPR((symb_val).value))

Valid trace value.

This macro checks whether symb_val is a valid nuxmv_trace_value.

Parameters

[in]

symb_val

The symbol value to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_OPT()

Function Documentation

nuxmv_trace_get_function()

nuxmv_trace_value nuxmv_trace_get_function	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	fun_idx
	)

Get the value of a uninterpreted function from a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.
[in]	fun_idx	The index of the uninterpreted function counting from 0.

Returns

The uninterpreted function of the trace. In case of error, NUXMV_VALID_TRACE_VALUE() evaluates to false.

See also

• nuxmv_trace_get_function_num()
• nuxmv_module_get_function()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_function_num()

int nuxmv_trace_get_function_num	(	nuxmv_env	env,
		nuxmv_trace	trace
	)

Get the number of uninterpreted functions in a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to extract the uninterpreted function number from.

Returns

The number of uninterpreted functions in the trace or -1 in case of error.

Note

Should the environment or the trace be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_trace_get_function()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_loopback()

int nuxmv_trace_get_loopback	(	nuxmv_env	env,
		nuxmv_trace	trace
	)

Get the the step the trace loops back, if any.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.

Returns

The number of the step, counting from 0, the trace jumps back to; -1 in case of error; -2 if trace didn't loop.

See also

• nuxmv_make_trace_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_define()

nuxmv_trace_value nuxmv_trace_get_step_define	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx,
		int	def_idx
	)

Get the value of a define from the i-th step of a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.
[in]	step_idx	The index of the step to inspect counting from 0.
[in]	def_idx	The index of the define counting from 0.

Returns

The define of the trace. In case of error, NUXMV_VALID_TRACE_VALUE() evaluates to false.

See also

• nuxmv_trace_get_step_num()
• nuxmv_trace_get_step_define_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_define_num()

int nuxmv_trace_get_step_define_num	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx
	)

Get the number of defines in a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to extract the define number from.
[in]	step_idx	The index of the step to inspect counting from 0.

Returns

The number of defines in the trace or -1 in case of error.

Note

Should the environment or the trace be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_trace_get_step_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_input()

nuxmv_trace_value nuxmv_trace_get_step_input	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx,
		int	var_idx
	)

Get the value of an input variable from the i-th step of a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.
[in]	step_idx	The index of the step to inspect counting from 0.
[in]	var_idx	The index of the input variable counting from 0.

Returns

The input variable of the trace. In case of error, NUXMV_VALID_TRACE_VALUE() evaluates to false.

See also

• nuxmv_trace_get_step_num()
• nuxmv_trace_get_step_input_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_input_num()

int nuxmv_trace_get_step_input_num	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx
	)

Get the number of input variables in a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to extract the input variable number from.
[in]	step_idx	The index of the step to inspect counting from 0.

Returns

The number of input variables in the trace or -1 in case of error.

Note

Should the environment or the trace be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_trace_get_step_input()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_num()

int nuxmv_trace_get_step_num	(	nuxmv_env	env,
		nuxmv_trace	trace
	)

Get the number of steps in a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.

Returns

The number of steps in the trace or -1 in case of error.

See also

• nuxmv_trace_get_step_state()
• nuxmv_trace_get_step_input()
• nuxmv_trace_get_step_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_state()

nuxmv_trace_value nuxmv_trace_get_step_state	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx,
		int	var_idx
	)

Get the value of a state variable from the i-th step of a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to inspect.
[in]	step_idx	The index of the step to inspect counting from 0.
[in]	var_idx	The index of the state variable counting from 0.

Returns

The value of the state variable in the trace. In case of error, NUXMV_VALID_TRACE_VALUE() evaluates to false.

See also

• nuxmv_trace_get_step_num()
• nuxmv_trace_get_step_state_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.007

nuxmv_trace_get_step_state_num()

int nuxmv_trace_get_step_state_num	(	nuxmv_env	env,
		nuxmv_trace	trace,
		int	step_idx
	)

Get the number of state variables in a trace.

Parameters

[in]	env	The environment to inspect.
[in]	trace	The trace to extract the state variable number from.
[in]	step_idx	The index of the step to inspect counting from 0.

Returns

The number of state variables in the trace or -1 in case of error.

Note

Should the environment or the trace be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_trace_get_step_state()
• nuxmv_env_get_last_error_message()

Requirements: 03.007