Module Getters

Functions for getting objects from a Module. More...

Collaboration diagram for Module Getters:

Functions
const char *	nuxmv_module_get_name (nuxmv_env env, nuxmv_module module)
	Get the name of a module.
int	nuxmv_module_get_param_num (nuxmv_env env, nuxmv_module module)
	Get the number of parameters of a module.
nuxmv_expr	nuxmv_module_get_param (nuxmv_env env, nuxmv_module module, int param_idx)
	Get the i-th parameter of a module.
int	nuxmv_module_get_state_var_num (nuxmv_env env, nuxmv_module module)
	Get the number of state variables in a module.
nuxmv_var_decl	nuxmv_module_get_state_var (nuxmv_env env, nuxmv_module module, int var_idx)
	Get the i-th state variable of a module.
int	nuxmv_module_get_input_var_num (nuxmv_env env, nuxmv_module module)
	Get the number of input variables in a module.
nuxmv_var_decl	nuxmv_module_get_input_var (nuxmv_env env, nuxmv_module module, int var_idx)
	Get the i-th input variable of a module.
int	nuxmv_module_get_frozen_var_num (nuxmv_env env, nuxmv_module module)
	Get the number of frozen variables in a module.
nuxmv_var_decl	nuxmv_module_get_frozen_var (nuxmv_env env, nuxmv_module module, int var_idx)
	Get the i-th frozen variable of a module.
int	nuxmv_module_get_function_num (nuxmv_env env, nuxmv_module module)
	Get the number of uninterpreted function declarations in a module.
nuxmv_fun_decl	nuxmv_module_get_function (nuxmv_env env, nuxmv_module module, int fun_idx)
	Get the i-th uninterpreted function declaration of a module.
int	nuxmv_module_get_init_num (nuxmv_env env, nuxmv_module module)
	Get the number of initial constraints in a module.
nuxmv_expr	nuxmv_module_get_init (nuxmv_env env, nuxmv_module module, int init_idx)
	Get the i-th initial constraint of a module.
int	nuxmv_module_get_trans_num (nuxmv_env env, nuxmv_module module)
	Get the number of transition constraints in a module.
nuxmv_expr	nuxmv_module_get_trans (nuxmv_env env, nuxmv_module module, int trans_idx)
	Get the i-th transition constraint of a module.
int	nuxmv_module_get_invar_num (nuxmv_env env, nuxmv_module module)
	Get the number of invariant constraints in a module.
nuxmv_expr	nuxmv_module_get_invar (nuxmv_env env, nuxmv_module module, int invar_idx)
	Get the i-th invariant constraint of a module.
int	nuxmv_module_get_justice_num (nuxmv_env env, nuxmv_module module)
	Get the number of justice constraints in a module.
nuxmv_expr	nuxmv_module_get_justice (nuxmv_env env, nuxmv_module module, int just_idx)
	Get the i-th justice constraint of a module.
int	nuxmv_module_get_compassion_num (nuxmv_env env, nuxmv_module module)
	Get the number of compassions in a module.
nuxmv_compassion	nuxmv_module_get_compassion (nuxmv_env env, nuxmv_module module, int comp_idx)
	Get the i-th compassion of a module.
int	nuxmv_module_get_define_num (nuxmv_env env, nuxmv_module module)
	Get the number of define declarations in a module.
nuxmv_define_decl	nuxmv_module_get_define (nuxmv_env env, nuxmv_module module, int def_idx)
	Get the i-th define declaration of a module.
int	nuxmv_module_get_init_assign_num (nuxmv_env env, nuxmv_module module)
	Get the number of initial assignments in a module.
nuxmv_assign	nuxmv_module_get_init_assign (nuxmv_env env, nuxmv_module module, int assign_idx)
	Get the i-th initial assignment of a module.
int	nuxmv_module_get_next_assign_num (nuxmv_env env, nuxmv_module module)
	Get the number of next assignments in a module.
nuxmv_assign	nuxmv_module_get_next_assign (nuxmv_env env, nuxmv_module module, int assign_idx)
	Get the i-th next assignment of a module.
int	nuxmv_module_get_invar_assign_num (nuxmv_env env, nuxmv_module module)
	Get the number of invariant assignments in a module.
nuxmv_assign	nuxmv_module_get_invar_assign (nuxmv_env env, nuxmv_module module, int assign_idx)
	Get the i-th invariant assignment of a module.
int	nuxmv_module_get_property_num (nuxmv_env env, nuxmv_module module)
	Get the number of properties in a module.
nuxmv_property	nuxmv_module_get_property (nuxmv_env env, nuxmv_module module, int prop_idx)
	Get the i-th property of a module.
int	nuxmv_module_get_submodule_num (nuxmv_env env, nuxmv_module module)
	Get the number of submodules in a module.
const char *	nuxmv_module_get_submodule_name (nuxmv_env env, nuxmv_module module, int sub_idx)
	Get the name of the i-th submodule of a module.
nuxmv_module	nuxmv_module_get_submodule (nuxmv_env env, nuxmv_module module, int sub_idx)
	Get the i-th submodule of a module.
int	nuxmv_module_get_submodule_param_num (nuxmv_env env, nuxmv_module module, int sub_idx)
	Get the number of parameters in a submodule.
nuxmv_expr	nuxmv_module_get_submodule_param (nuxmv_env env, nuxmv_module module, int sub_idx, int param_idx)
	Get the i-th parameter of a submodule.
int	nuxmv_serialize_module_to_string (nuxmv_env env, nuxmv_module module, bool with_submodules, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size)
	Serialize a module to a string in SMV format.

Detailed Description

Functions for getting objects from a Module.

---

Function Documentation

nuxmv_module_get_compassion()

nuxmv_compassion nuxmv_module_get_compassion	(	nuxmv_env	env,
		nuxmv_module	module,
		int	comp_idx
	)

Get the i-th compassion of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	comp_idx	The index of the compassion counting from 0.

Returns

The compassion of the module. In case of error, NUXMV_VALID_COMPASSION() evaluates to false.

See also

• nuxmv_module_add_compassion()
• nuxmv_module_get_compassion_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_compassion_num()

int nuxmv_module_get_compassion_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of compassions in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the compassion number from.

Returns

The number of compassions in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_compassion()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_define()

nuxmv_define_decl nuxmv_module_get_define	(	nuxmv_env	env,
		nuxmv_module	module,
		int	def_idx
	)

Get the i-th define declaration of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	def_idx	The index of the define declaration counting from 0.

Returns

The define declaration of the module. In case of error, NUXMV_VALID_DEFINE_DECL() evaluates to false.

See also

• nuxmv_module_add_define()
• nuxmv_module_get_define_num()
• nuxmv_model_get_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_define_num()

int nuxmv_module_get_define_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of define declarations in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the define declaration number from.

Returns

The number of define declarations in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_frozen_var()

nuxmv_var_decl nuxmv_module_get_frozen_var	(	nuxmv_env	env,
		nuxmv_module	module,
		int	var_idx
	)

Get the i-th frozen variable of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	var_idx	The index of the frozen variable counting from 0.

Returns

The frozen variable of the module. In case of error, NUXMV_VALID_VAR_DECL() evaluates to false.

See also

• nuxmv_module_add_frozen_var()
• nuxmv_module_get_frozen_var_num()
• nuxmv_model_get_frozen_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_frozen_var_num()

int nuxmv_module_get_frozen_var_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of frozen variables in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the frozen variable number from.

Returns

The number of frozen variables in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_frozen_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_function()

nuxmv_fun_decl nuxmv_module_get_function	(	nuxmv_env	env,
		nuxmv_module	module,
		int	fun_idx
	)

Get the i-th uninterpreted function declaration of a module.

Parameters

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

Returns

The uninterpreted function declaration of the module. In case of error, NUXMV_VALID_FUN_DECL() evaluates to false.

See also

• nuxmv_module_add_function()
• nuxmv_module_get_function_num
• nuxmv_model_get_function()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_function_num()

int nuxmv_module_get_function_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of uninterpreted function declarations in a module.

Parameters

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

Returns

The number of uninterpreted function declarations in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_function()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_init()

nuxmv_expr nuxmv_module_get_init	(	nuxmv_env	env,
		nuxmv_module	module,
		int	init_idx
	)

Get the i-th initial constraint of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	init_idx	The index of the initial constraint counting from 0.

Returns

The initial constraint of the module. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_init()
• nuxmv_module_get_init_num()
• nuxmv_module_get_init_assign()
• nuxmv_model_get_init()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_init_assign()

nuxmv_assign nuxmv_module_get_init_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		int	assign_idx
	)

Get the i-th initial assignment of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	assign_idx	The index of the initial assignment counting from 0.

Returns

The initial assignment of the module. In case of error, NUXMV_VALID_ASSIGN() evaluates to false.

See also

• nuxmv_module_add_init_assign()
• nuxmv_module_get_init_assign_num()
• nuxmv_model_get_init_assign()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_init_assign_num()

int nuxmv_module_get_init_assign_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of initial assignments in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the initial assignment number from.

Returns

The number of initial assignments in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_init_assign()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_init_num()

int nuxmv_module_get_init_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of initial constraints in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the initial constraint number from.

Returns

The number of initial constraints in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_init()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_input_var()

nuxmv_var_decl nuxmv_module_get_input_var	(	nuxmv_env	env,
		nuxmv_module	module,
		int	var_idx
	)

Get the i-th input variable of a module.

Parameters

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

Returns

The input variable of the module. In case of error, NUXMV_VALID_VAR_DECL() evaluates to false.

See also

• nuxmv_module_add_input_var()
• nuxmv_module_get_input_var_num()
• nuxmv_model_get_input_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_input_var_num()

int nuxmv_module_get_input_var_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of input variables in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the input variable number from.

Returns

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

Note

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

See also

• nuxmv_module_get_input_var()

Requirements: ??

nuxmv_module_get_invar()

nuxmv_expr nuxmv_module_get_invar	(	nuxmv_env	env,
		nuxmv_module	module,
		int	invar_idx
	)

Get the i-th invariant constraint of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	invar_idx	The index of the invariant constraint counting from 0.

Returns

The invariant constraint of the module. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_invar()
• nuxmv_module_get_invar_num()
• nuxmv_module_get_invar_assign()
• nuxmv_model_get_invar()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_invar_assign()

nuxmv_assign nuxmv_module_get_invar_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		int	assign_idx
	)

Get the i-th invariant assignment of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	assign_idx	The index of the invariant assignment counting from 0.

Returns

The invariant assignment of the module. In case of error, NUXMV_VALID_ASSIGN() evaluates to false.

See also

• nuxmv_module_add_invar_assign()
• nuxmv_module_get_invar_assign_num()
• nuxmv_model_get_invar_assign()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_module_get_invar_assign_num()

int nuxmv_module_get_invar_assign_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of invariant assignments in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the invariant assignment number from.

Returns

The number of invariant assignments in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_invar_assign()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_module_get_invar_num()

int nuxmv_module_get_invar_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of invariant constraints in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the invariant constraint number from.

Returns

The number of invariant constraints in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_invar()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_justice()

nuxmv_expr nuxmv_module_get_justice	(	nuxmv_env	env,
		nuxmv_module	module,
		int	just_idx
	)

Get the i-th justice constraint of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	just_idx	The index of the justice constraint counting from 0.

Returns

The justice constraint of the module. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_justice()
• nuxmv_module_get_justice_num()
• nuxmv_model_get_justice()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_justice_num()

int nuxmv_module_get_justice_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of justice constraints in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the justice constraint number from.

Returns

The number of justice constraints in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_justice()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_name()

const char * nuxmv_module_get_name	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the name of a module.

Parameters

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

Returns

The name of the module, or NULL in case of error.

See also

• nuxmv_env_get_last_error_message()

nuxmv_module_get_next_assign()

nuxmv_assign nuxmv_module_get_next_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		int	assign_idx
	)

Get the i-th next assignment of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	assign_idx	The index of the next assignment counting from 0.

Returns

The next assignment of the module. In case of error, NUXMV_VALID_ASSIGN() evaluates to false.

See also

• nuxmv_module_add_next_assign()
• nuxmv_module_get_next_assign_num()
• nuxmv_model_get_next_assign()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_module_get_next_assign_num()

int nuxmv_module_get_next_assign_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of next assignments in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the next assignment number from.

Returns

The number of next assignments in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_next_assign()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_module_get_param()

nuxmv_expr nuxmv_module_get_param	(	nuxmv_env	env,
		nuxmv_module	module,
		int	param_idx
	)

Get the i-th parameter of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	param_idx	The index of the parameter counting from 0.

Returns

The parameter of the module. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_params()
• nuxmv_module_get_param_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_param_num()

int nuxmv_module_get_param_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of parameters of a module.

Parameters

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

Returns

The number of parameters of the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_param()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_property()

nuxmv_property nuxmv_module_get_property	(	nuxmv_env	env,
		nuxmv_module	module,
		int	prop_idx
	)

Get the i-th property of a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	prop_idx	The index of the property counting from 0.

Returns

The property of the module. In case of error, NUXMV_VALID_PROPERTY() evaluates to false.

See also

• nuxmv_module_add_property()
• nuxmv_module_get_property_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.008

nuxmv_module_get_property_num()

int nuxmv_module_get_property_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of properties in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the property number from.

Returns

The number of properties in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_property()
• nuxmv_env_get_last_error_message()

Requirements: 03.008

nuxmv_module_get_state_var()

nuxmv_var_decl nuxmv_module_get_state_var	(	nuxmv_env	env,
		nuxmv_module	module,
		int	var_idx
	)

Get the i-th state variable of a module.

Parameters

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

Returns

The state variable of the module. In case of error, NUXMV_VALID_VAR_DECL() evaluates to false.

See also

• nuxmv_module_add_state_var()
• nuxmv_module_get_state_var_num()
• nuxmv_model_get_state_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_state_var_num()

int nuxmv_module_get_state_var_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of state variables in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the state variable number from.

Returns

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

Note

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

See also

• nuxmv_module_get_state_var()

Requirements: 03.009.02

nuxmv_module_get_submodule()

nuxmv_module nuxmv_module_get_submodule	(	nuxmv_env	env,
		nuxmv_module	module,
		int	sub_idx
	)

Get the i-th submodule of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	sub_idx	The index of the submodule counting from 0.

Returns

The i-th submodule. In case of error, NUXMV_VALID_MODEL() evaluates to false.

See also

• nuxmv_module_add_submodule()
• nuxmv_module_get_submodule_num()
• nuxmv_module_get_submodule_name()
• nuxmv_module_get_submodule_param()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_submodule_name()

const char * nuxmv_module_get_submodule_name	(	nuxmv_env	env,
		nuxmv_module	module,
		int	sub_idx
	)

Get the name of the i-th submodule of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	sub_idx	The index of the submodule counting from 0.

Returns

The name of the i-th submodule as a null-terminated string or NULL in case of error.

See also

• nuxmv_module_add_submodule()
• nuxmv_module_get_submodule_num()
• nuxmv_module_get_submodule()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_submodule_num()

int nuxmv_module_get_submodule_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of submodules in a module.

Parameters

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

Returns

The number of submodules in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_submodule()
• nuxmv_module_get_submodule_name()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_submodule_param()

nuxmv_expr nuxmv_module_get_submodule_param	(	nuxmv_env	env,
		nuxmv_module	module,
		int	sub_idx,
		int	param_idx
	)

Get the i-th parameter of a submodule.

Parameters

[in]	env	The environment to inspect.
[in]	module	The parent module to inspect.
[in]	sub_idx	The submodule to extract the parameter number from.
[in]	param_idx	The index of the parameter counting from 0.

Returns

The parameter of the submodule. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_submodule()
• nuxmv_module_get_submodule_num()
• nuxmv_module_get_submodule_param_num()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_submodule_param_num()

int nuxmv_module_get_submodule_param_num	(	nuxmv_env	env,
		nuxmv_module	module,
		int	sub_idx
	)

Get the number of parameters in a submodule.

Parameters

[in]	env	The environment to inspect.
[in]	module	The parent module to inspect.
[in]	sub_idx	The submodule to extract the parameter number from.

Returns

The number of parameters in the submodule or -1 in case of error.

Note

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

See also

• nuxmv_module_get_submodule_num()
• nuxmv_module_get_submodule_param()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_trans()

nuxmv_expr nuxmv_module_get_trans	(	nuxmv_env	env,
		nuxmv_module	module,
		int	trans_idx
	)

Get the i-th transition constraint of a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to inspect.
[in]	trans_idx	The index of the transition constraint counting from 0.

Returns

The transition constraint of the module. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_module_add_trans()
• nuxmv_module_get_trans_num()
• nuxmv_model_get_trans()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_module_get_trans_num()

int nuxmv_module_get_trans_num	(	nuxmv_env	env,
		nuxmv_module	module
	)

Get the number of transition constraints in a module.

Parameters

[in]	env	The environment to inspect.
[in]	module	The module to extract the transition constraint number from.

Returns

The number of transition constraints in the module or -1 in case of error.

Note

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

See also

• nuxmv_module_get_trans()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.02

nuxmv_serialize_module_to_string()

int nuxmv_serialize_module_to_string	(	nuxmv_env	env,
		nuxmv_module	module,
		bool	with_submodules,
		nuxmv_serialized_chunk_callback	callback,
		void *	user_data,
		char *	data,
		size_t	data_size
	)

Serialize a module to a string in SMV format.

This function converts the given module into a string representation using the SMV 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]	module	The module to serialize.
[in]	with_submodules	Flag indicating whether submodules should be (recursively) serialized.
[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 model 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_serialize_model_to_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.002