Model Variable Getters

Functions for getting Variables from a Model. More...

Collaboration diagram for Model Variable Getters:

Functions
int	nuxmv_model_get_state_var_num (nuxmv_env env, nuxmv_model model)
	Get the number of state variables in a model.
nuxmv_var_decl	nuxmv_model_get_state_var (nuxmv_env env, nuxmv_model model, int var_idx)
	Get the i-th state variable of a model.
int	nuxmv_model_get_input_var_num (nuxmv_env env, nuxmv_model model)
	Get the number of input variables in a model.
nuxmv_var_decl	nuxmv_model_get_input_var (nuxmv_env env, nuxmv_model model, int var_idx)
	Get the i-th input variable of a model.
int	nuxmv_model_get_frozen_var_num (nuxmv_env env, nuxmv_model model)
	Get the number of frozen variables in a model.
nuxmv_var_decl	nuxmv_model_get_frozen_var (nuxmv_env env, nuxmv_model model, int var_idx)
	Get the i-th frozen variable of a model.
int	nuxmv_model_get_function_num (nuxmv_env env, nuxmv_model model)
	Get the number of user-defined function declarations in a model.
nuxmv_fun_decl	nuxmv_model_get_function (nuxmv_env env, nuxmv_model model, int fun_idx)
	Get the i-th user-defined function declaration of a model.
int	nuxmv_model_get_init_num (nuxmv_env env, nuxmv_model model)
	Get the number of initial constraints in a model.
nuxmv_expr	nuxmv_model_get_init (nuxmv_env env, nuxmv_model model, int init_idx)
	Get the i-th initial constraint of a model.
int	nuxmv_model_get_trans_num (nuxmv_env env, nuxmv_model model)
	Get the number of transition constraints in a model.
nuxmv_expr	nuxmv_model_get_trans (nuxmv_env env, nuxmv_model model, int trans_idx)
	Get the i-th transition constraint of a model.
int	nuxmv_model_get_invar_num (nuxmv_env env, nuxmv_model model)
	Get the number of invariant constraints in a model.
nuxmv_expr	nuxmv_model_get_invar (nuxmv_env env, nuxmv_model model, int invar_idx)
	Get the i-th invariant constraint of a model.
int	nuxmv_model_get_justice_num (nuxmv_env env, nuxmv_model model)
	Get the number of justice constraints in a model.
nuxmv_expr	nuxmv_model_get_justice (nuxmv_env env, nuxmv_model model, int just_idx)
	Get the i-th justice constraint of a model.
int	nuxmv_model_get_compassion_num (nuxmv_env env, nuxmv_model model)
	Get the number of compassions in a model.
nuxmv_compassion	nuxmv_model_get_compassion (nuxmv_env env, nuxmv_model model, int comp_idx)
	Get the i-th compassion of a model.
int	nuxmv_model_get_define_num (nuxmv_env env, nuxmv_model model)
	Get the number of define declarations in a model.
nuxmv_define_decl	nuxmv_model_get_define (nuxmv_env env, nuxmv_model model, int def_idx)
	Get the i-th define declaration of a model.

Detailed Description

Functions for getting Variables from a Model.

---

Function Documentation

nuxmv_model_get_compassion()

nuxmv_compassion nuxmv_model_get_compassion	(	nuxmv_env	env,
		nuxmv_model	model,
		int	comp_idx
	)

Get the i-th compassion of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_compassion_num()
• nuxmv_module_get_compassion()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_compassion_num()

int nuxmv_model_get_compassion_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of compassions in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_compassion()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_define()

nuxmv_define_decl nuxmv_model_get_define	(	nuxmv_env	env,
		nuxmv_model	model,
		int	def_idx
	)

Get the i-th define declaration of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_define_num()
• nuxmv_module_get_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_define_num()

int nuxmv_model_get_define_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of define declarations in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_frozen_var()

nuxmv_var_decl nuxmv_model_get_frozen_var	(	nuxmv_env	env,
		nuxmv_model	model,
		int	var_idx
	)

Get the i-th frozen variable of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_frozen_var_num()
• nuxmv_module_get_frozen_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_frozen_var_num()

int nuxmv_model_get_frozen_var_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of frozen variables in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_frozen_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_function()

nuxmv_fun_decl nuxmv_model_get_function	(	nuxmv_env	env,
		nuxmv_model	model,
		int	fun_idx
	)

Get the i-th user-defined function declaration of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_function_num()
• nuxmv_module_get_function()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_model_get_function_num()

int nuxmv_model_get_function_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of user-defined function declarations in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_function()
• nuxmv_env_get_last_error_message()

Requirements: ??

nuxmv_model_get_init()

nuxmv_expr nuxmv_model_get_init	(	nuxmv_env	env,
		nuxmv_model	model,
		int	init_idx
	)

Get the i-th initial constraint of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_init_num()
• nuxmv_module_get_init()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_init_num()

int nuxmv_model_get_init_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of initial constraints in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_init()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_input_var()

nuxmv_var_decl nuxmv_model_get_input_var	(	nuxmv_env	env,
		nuxmv_model	model,
		int	var_idx
	)

Get the i-th input variable of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_input_var_num()
• nuxmv_module_get_input_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_input_var_num()

int nuxmv_model_get_input_var_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of input variables in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_input_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_invar()

nuxmv_expr nuxmv_model_get_invar	(	nuxmv_env	env,
		nuxmv_model	model,
		int	invar_idx
	)

Get the i-th invariant constraint of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_invar_num()
• nuxmv_module_get_invar()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_invar_num()

int nuxmv_model_get_invar_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of invariant constraints in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_invar()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_justice()

nuxmv_expr nuxmv_model_get_justice	(	nuxmv_env	env,
		nuxmv_model	model,
		int	just_idx
	)

Get the i-th justice constraint of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_justice_num()
• nuxmv_module_get_justice()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_justice_num()

int nuxmv_model_get_justice_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of justice constraints in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_justice()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_state_var()

nuxmv_var_decl nuxmv_model_get_state_var	(	nuxmv_env	env,
		nuxmv_model	model,
		int	var_idx
	)

Get the i-th state variable of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_state_var_num()
• nuxmv_module_get_state_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_state_var_num()

int nuxmv_model_get_state_var_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of state variables in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_state_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_trans()

nuxmv_expr nuxmv_model_get_trans	(	nuxmv_env	env,
		nuxmv_model	model,
		int	trans_idx
	)

Get the i-th transition constraint of a model.

Parameters

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

Returns

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

See also

• nuxmv_model_get_trans_num()
• nuxmv_module_get_trans()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02

nuxmv_model_get_trans_num()

int nuxmv_model_get_trans_num	(	nuxmv_env	env,
		nuxmv_model	model
	)

Get the number of transition constraints in a model.

Parameters

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

Returns

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

Note

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

See also

• nuxmv_model_get_trans()
• nuxmv_env_get_last_error_message()

Requirements: 03.004.02