Module Adders

Functions for adding objects to a Module. More...

Collaboration diagram for Module Adders:

Macros
#define	NUXMV_MAKE_VAR_DECL(identifier_, var_type_)    ((nuxmv_var_decl){.identifier = identifier_, .var_type = var_type_})
	Helper macro for making variable declarations.
#define	NUXMV_VALID_VAR_DECL(var_decl_)
	Valid variable declaration.
#define	NUXMV_MAKE_FUN_DECL(identifier_, fun_type_)    ((nuxmv_fun_decl){.identifier = identifier_, .fun_type = fun_type_})
	Helper macro for making function declarations.
#define	NUXMV_VALID_FUN_DECL(fun_decl_)
	Valid function declaration.
#define	NUXMV_MAKE_ASSIGN(lhs_, rhs_)   ((nuxmv_assign){.lhs = lhs_, .rhs = rhs_})
	Helper macro for making an assignment.
#define	NUXMV_VALID_ASSIGN(assign_)    (NUXMV_VALID_EXPR((assign_).lhs) && NUXMV_VALID_EXPR((assign_).rhs))
	Valid assignment.
#define	NUXMV_MAKE_COMPASSION(p_, q_)   ((nuxmv_compassion){.p = p_, .q = q_})
	Helper macro for making compassions.
#define	NUXMV_VALID_COMPASSION(comp_)    (NUXMV_VALID_EXPR((comp_).p) && NUXMV_VALID_EXPR((comp_).q))
	Valid compassion constraint.
#define	NUXMV_MAKE_DEFINE_DECL(identifier_, body_)    ((nuxmv_define_decl){.identifier = identifier_, .body = body_})
	Helper macro for making define declarations.
#define	NUXMV_VALID_DEFINE_DECL(define_decl_)
	Valid define declaration.

Functions
nuxmv_status_code	nuxmv_module_add_params (nuxmv_env env, nuxmv_module module, const nuxmv_expr *params, size_t param_num)
	Add parameters to a module.
nuxmv_status_code	nuxmv_module_add_state_var (nuxmv_env env, nuxmv_module module, nuxmv_var_decl var)
	Add a state variable to a module.
nuxmv_status_code	nuxmv_module_add_input_var (nuxmv_env env, nuxmv_module module, nuxmv_var_decl var)
	Add an input variable to a module.
nuxmv_status_code	nuxmv_module_add_frozen_var (nuxmv_env env, nuxmv_module module, nuxmv_var_decl var)
	Adds a frozen variable to a module.
nuxmv_status_code	nuxmv_module_add_function (nuxmv_env env, nuxmv_module module, nuxmv_fun_decl fun_decl)
	Add an uninterpreted function declaration to a module.
nuxmv_status_code	nuxmv_module_add_init (nuxmv_env env, nuxmv_module module, nuxmv_expr init)
	Add an initial constraint to a module.
nuxmv_status_code	nuxmv_module_add_trans (nuxmv_env env, nuxmv_module module, nuxmv_expr trans)
	Add a transition constraint to a module.
nuxmv_status_code	nuxmv_module_add_invar (nuxmv_env env, nuxmv_module module, nuxmv_expr invar)
	Add an invariant constraint to a module.
nuxmv_status_code	nuxmv_module_add_justice (nuxmv_env env, nuxmv_module module, nuxmv_expr justice)
	Add a justice constraint to a module.
nuxmv_status_code	nuxmv_module_add_compassion (nuxmv_env env, nuxmv_module module, nuxmv_compassion comp)
	Add a compassion constraint to a module.
nuxmv_status_code	nuxmv_module_add_define (nuxmv_env env, nuxmv_module module, nuxmv_define_decl decl)
	Add a define declaration to a module.
nuxmv_status_code	nuxmv_module_add_init_assign (nuxmv_env env, nuxmv_module module, nuxmv_assign assign)
	Add an initial assignment to a module.
nuxmv_status_code	nuxmv_module_add_next_assign (nuxmv_env env, nuxmv_module module, nuxmv_assign assign)
	Add a next assignment to a module.
nuxmv_status_code	nuxmv_module_add_invar_assign (nuxmv_env env, nuxmv_module module, nuxmv_assign assign)
	Add an invariant assignment to a module.
nuxmv_status_code	nuxmv_module_add_property (nuxmv_env env, nuxmv_module module, nuxmv_property property)
	Add a property to a module.
nuxmv_status_code	nuxmv_module_add_submodule (nuxmv_env env, nuxmv_module module, const char *name, nuxmv_module sub, const nuxmv_expr *params, size_t param_num)
	Add a submodule to a module.

Detailed Description

Functions for adding objects to a Module.

---

Macro Definition Documentation

NUXMV_MAKE_ASSIGN

#define NUXMV_MAKE_ASSIGN	(		lhs_,
			rhs_
	)		((nuxmv_assign){.lhs = lhs_, .rhs = rhs_})

Helper macro for making an assignment.

Parameters

[in]	lhs_	A nuxmv_expr as the left-hand side of the assignment.
[in]	rhs_	A nuxmv_expr as the right-hand side of the assignment.

Returns

A new nuxmv_assign object.

See also

• NUXMV_VALID_ASSIGN()

NUXMV_MAKE_COMPASSION

#define NUXMV_MAKE_COMPASSION	(		p_,
			q_
	)		((nuxmv_compassion){.p = p_, .q = q_})

Helper macro for making compassions.

Parameters

[in]	p_	A nuxmv_expr as the first formula of the compassion constraint.
[in]	q_	A nuxmv_expr as the second formula of the compassion constraint.

Returns

A new nuxmv_compassion object.

See also

• NUXMV_VALID_COMPASSION()

NUXMV_MAKE_DEFINE_DECL

#define NUXMV_MAKE_DEFINE_DECL	(		identifier_,
			body_
	)		((nuxmv_define_decl){.identifier = identifier_, .body = body_})

Helper macro for making define declarations.

Parameters

[in]	identifier_	A nuxmv_expr as the identifier of the define.
[in]	body_	A nuxmv_expr as the type of the define.

Returns

A new nuxmv_define_decl object.

See also

• NUXMV_VALID_DEFINE_DECL()
• nuxmv_module_add_define()

NUXMV_MAKE_FUN_DECL

#define NUXMV_MAKE_FUN_DECL	(		identifier_,
			fun_type_
	)		((nuxmv_fun_decl){.identifier = identifier_, .fun_type = fun_type_})

Helper macro for making function declarations.

Parameters

[in]	identifier_	A nuxmv_symbol as the identifier of the function.
[in]	fun_type_	A nuxmv_expr_type as the type of the function.

Returns

A new nuxmv_fun_decl object.

NUXMV_MAKE_VAR_DECL

#define NUXMV_MAKE_VAR_DECL	(		identifier_,
			var_type_
	)		((nuxmv_var_decl){.identifier = identifier_, .var_type = var_type_})

Helper macro for making variable declarations.

Parameters

[in]	identifier_	A nuxmv_symbol as the identifier of the variable.
[in]	var_type_	A nuxmv_var_type as the type of the variable.

Returns

A new nuxmv_var_decl object.

See also

• NUXMV_VALID_VAR_DECL()

NUXMV_VALID_ASSIGN

#define NUXMV_VALID_ASSIGN

(

assign_

)

(NUXMV_VALID_EXPR((assign_).lhs) && NUXMV_VALID_EXPR((assign_).rhs))

Valid assignment.

This macro checks whether assign is a valid nuxmv_assign.

Parameters

[in]

assign_

The assignment to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_ASSIGN()
• nuxmv_module_get_init_assign()
• nuxmv_module_get_next_assign()
• nuxmv_module_get_invar_assign()
• nuxmv_model_get_init_assign()
• nuxmv_model_get_next_assign()
• nuxmv_model_get_invar_assign()

NUXMV_VALID_COMPASSION

#define NUXMV_VALID_COMPASSION

(

comp_

)

(NUXMV_VALID_EXPR((comp_).p) && NUXMV_VALID_EXPR((comp_).q))

Valid compassion constraint.

This macro checks whether comp is a valid nuxmv_compassion.

Parameters

[in]

comp_

The compassion constraint to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_COMPASSION()
• nuxmv_module_get_compassion()

NUXMV_VALID_DEFINE_DECL

#define NUXMV_VALID_DEFINE_DECL

(

define_decl_

)

Value:

    (NUXMV_VALID_EXPR((define_decl_).identifier) &&                            \
     NUXMV_VALID_EXPR((define_decl_).body))

Valid define declaration.

This macro checks whether define_decl is a valid nuxmv_define_decl.

Parameters

[in]

define_decl_

The define declaration to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_DEFINE_DECL()
• nuxmv_model_get_define()
• nuxmv_module_get_define()

NUXMV_VALID_FUN_DECL

#define NUXMV_VALID_FUN_DECL

(

fun_decl_

)

Value:

    (NUXMV_VALID_SYMBOL((fun_decl_).identifier) &&                             \
     NUXMV_VALID_VAR_TYPE((fun_decl_).fun_type))

Valid function declaration.

This macro checks whether fun_decl is a valid nuxmv_fun_decl.

Parameters

[in]

fun_decl_

The function declaration to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_FUN_DECL()
• nuxmv_module_get_function()
• nuxmv_model_get_function()

NUXMV_VALID_VAR_DECL

#define NUXMV_VALID_VAR_DECL

(

var_decl_

)

Value:

    (NUXMV_VALID_SYMBOL((var_decl_).identifier) &&                             \
     NUXMV_VALID_VAR_TYPE((var_decl_).var_type))

Valid variable declaration.

This macro checks whether var_decl is a valid nuxmv_var_decl.

Parameters

[in]

var_decl_

The variable declaration to inspect.

Returns

true if the option is valid, false otherwise.

See also

• NUXMV_MAKE_VAR_DECL()
• nuxmv_module_get_state_var()
• nuxmv_module_get_input_var()
• nuxmv_module_get_frozen_var()

Function Documentation

nuxmv_module_add_compassion()

nuxmv_status_code nuxmv_module_add_compassion	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_compassion	comp
	)

Add a compassion constraint to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	comp	A compassion constraint.

Returns

NUXMV_SUCCESS if the compassion assignment was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_COMPASSION()
• nuxmv_module_get_compassion()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_define()

nuxmv_status_code nuxmv_module_add_define	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_define_decl	decl
	)

Add a define declaration to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	decl	A unique define declaration to add.

Returns

NUXMV_SUCCESS if the define declaration was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_DEFINE_DECL()
• nuxmv_module_get_define()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_frozen_var()

nuxmv_status_code nuxmv_module_add_frozen_var	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_var_decl	var
	)

Adds a frozen variable to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to add a frozen variable to.
[in]	var	A unique frozen variable to add.

Returns

NUXMV_SUCCESS when the frozen variable was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_VAR_DECL()
• nuxmv_module_get_frozen_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_function()

nuxmv_status_code nuxmv_module_add_function	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_fun_decl	fun_decl
	)

Add an uninterpreted function declaration to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to add the uninterpreted function declaration to.
[in]	fun_decl	An uninterpreted function declaration to add.

Returns

NUXMV_SUCCESS when the uninterpreted function declaration was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_FUN_DECL()
• nuxmv_module_get_function()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_init()

nuxmv_status_code nuxmv_module_add_init	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_expr	init
	)

Add an initial constraint to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	init	An initial constraint to add.

Returns

NUXMV_SUCCESS if the initial constraint was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_init()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_init_assign()

nuxmv_status_code nuxmv_module_add_init_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_assign	assign
	)

Add an initial assignment to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	assign	An assignment to add.

Returns

NUXMV_SUCCESS if the initial assignment was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_init_assign()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_input_var()

nuxmv_status_code nuxmv_module_add_input_var	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_var_decl	var
	)

Add an input variable to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to add an input variable to.
[in]	var	A unique input variable to add.

Returns

NUXMV_SUCCESS when the input variable was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_VAR_DECL()
• nuxmv_module_get_input_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_invar()

nuxmv_status_code nuxmv_module_add_invar	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_expr	invar
	)

Add an invariant constraint to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	invar	An invariant constraint to add.

Returns

NUXMV_SUCCESS if the invariant constraint was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_invar()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_invar_assign()

nuxmv_status_code nuxmv_module_add_invar_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_assign	assign
	)

Add an invariant assignment to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	assign	An assignment to add.

Returns

NUXMV_SUCCESS if the invariant assignment was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_invar_assign()
• nuxmv_env_get_last_error_message()

nuxmv_module_add_justice()

nuxmv_status_code nuxmv_module_add_justice	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_expr	justice
	)

Add a justice constraint to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	justice	A justice constraint to add.

Returns

NUXMV_SUCCESS if the justice constraint was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_justice()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_next_assign()

nuxmv_status_code nuxmv_module_add_next_assign	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_assign	assign
	)

Add a next assignment to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	assign	An assignment to add.

Returns

NUXMV_SUCCESS if the next assignment was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_next_assign()
• nuxmv_env_get_last_error_message()

nuxmv_module_add_params()

nuxmv_status_code nuxmv_module_add_params	(	nuxmv_env	env,
		nuxmv_module	module,
		const nuxmv_expr *	params,
		size_t	param_num
	)

Add parameters to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to add parameters to.
[in]	params	A list of parameters to add.
[in]	param_num	The number of parameters in the list.

Returns

NUXMV_SUCCESS when parameters were added, NUXMV_FAILURE in case of error.

See also

• NUXMV_COUNT_OF()
• nuxmv_module_get_param()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_property()

nuxmv_status_code nuxmv_module_add_property	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_property	property
	)

Add a property to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	property	A property to add to the module.

Returns

NUXMV_SUCCESS if the invariant assignment was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_make_property()
• nuxmv_env_get_last_error_message()

Requirements: 03.008

nuxmv_module_add_state_var()

nuxmv_status_code nuxmv_module_add_state_var	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_var_decl	var
	)

Add a state variable to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to add a state variable to.
[in]	var	A unique state variable to add.

Returns

NUXMV_SUCCESS when the state variable was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_MAKE_VAR_DECL()
• nuxmv_module_get_state_var()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01

nuxmv_module_add_submodule()

nuxmv_status_code nuxmv_module_add_submodule	(	nuxmv_env	env,
		nuxmv_module	module,
		const char *	name,
		nuxmv_module	sub,
		const nuxmv_expr *	params,
		size_t	param_num
	)

Add a submodule to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	name	An unique name for the submodule instantiation as a null-terminated string.
[in]	sub	The submodule to add. The submodule must not be destroyed if the module is still in use.
[in]	params	A list of parameters for the submodule instantiation. If no list shall be used it is safe to use NULL or the result of malloc(0), provided that param_num=0.
[in]	param_num	The number of parameters in the list. If no list shall be passed, use 0 as actual value of param_num.

Returns

NUXMV_SUCCESS if the invariant assignment was added, NUXMV_FAILURE in case of error.

See also

• NUXMV_COUNT_OF()
• nuxmv_module_get_submodule_num()
• nuxmv_module_get_submodule_name()
• nuxmv_module_get_submodule()
• nuxmv_module_get_submodule_param()
• nuxmv_env_get_last_error_message()
• nuxmv_destroy_module()

Requirements: 03.009.01

nuxmv_module_add_trans()

nuxmv_status_code nuxmv_module_add_trans	(	nuxmv_env	env,
		nuxmv_module	module,
		nuxmv_expr	trans
	)

Add a transition constraint to a module.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to modify.
[in]	trans	A transition constraint to add.

Returns

NUXMV_SUCCESS if the transition constraint was added, NUXMV_FAILURE in case of error.

See also

• nuxmv_module_get_trans()
• nuxmv_env_get_last_error_message()

Requirements: 03.009.01