Properties

Functions for handling Properties. More...

Macros
#define	NUXMV_VALID_PROPERTY(property)   ((property).repr != NULL)
	Valid property.

Functions
nuxmv_property	nuxmv_make_property (nuxmv_env env, nuxmv_property_type type, nuxmv_expr expr, const char *name)
	Create a new property.
nuxmv_property	nuxmv_make_property_from_string (nuxmv_env env, nuxmv_property_type type, const char *data, nuxmv_module scope, const char *name)
	Create a property from string.
nuxmv_result	nuxmv_property_check_satisfiability (nuxmv_env env, nuxmv_property property, const nuxmv_opt *opts, size_t opt_num)
	Create the satisfiability of a property.
nuxmv_expr	nuxmv_property_get_expr (nuxmv_env env, nuxmv_property property)
	Get the expression of a property.
const char *	nuxmv_property_get_name (nuxmv_env env, nuxmv_property property)
	Get the name of a property.
nuxmv_property_type	nuxmv_property_get_type (nuxmv_env env, nuxmv_property property)
	Get the type of a property.

Detailed Description

Functions for handling Properties.

---

Macro Definition Documentation

NUXMV_VALID_PROPERTY

#define NUXMV_VALID_PROPERTY

(

property

)

((property).repr != NULL)

Valid property.

This macro checks whether property is a valid nuxmv_property.

Parameters

[in]

property

The property to inspect.

Returns

true if the option is valid, false otherwise.

Function Documentation

nuxmv_make_property()

nuxmv_property nuxmv_make_property	(	nuxmv_env	env,
		nuxmv_property_type	type,
		nuxmv_expr	expr,
		const char *	name
	)

Create a new property.

Parameters

[in]	env	The environment to modify.
[in]	type	The type of the property to create.
[in]	expr	An expression to attach the property to.
[in]	name	The name of the property as a null-terminated string. name is optional, use NULL as no-value.

Returns

The newly created property. In case of error, NUXMV_VALID_PROPERTY() evaluates to false.

See also

• nuxmv_make_property_from_string()
• nuxmv_module_add_property()
• nuxmv_env_get_last_error_message()

Requirements: 03.008

nuxmv_make_property_from_string()

nuxmv_property nuxmv_make_property_from_string	(	nuxmv_env	env,
		nuxmv_property_type	type,
		const char *	data,
		nuxmv_module	scope,
		const char *	name
	)

Create a property from string.

Parameters

[in]	env	The environment to modify.
[in]	name	The name of the property as a null-terminated string. name is optional, use NULL as no-value.
[in]	type	The type of the property to create.
[in]	data	A null-terminated string containing the property data.
[in]	scope	A context symbols belongs to.

Returns

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

See also

• nuxmv_make_property()
• nuxmv_env_get_last_error_message()

Requirements: 03.005

nuxmv_property_check_satisfiability()

nuxmv_result nuxmv_property_check_satisfiability	(	nuxmv_env	env,
		nuxmv_property	property,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Create the satisfiability of a property.

Parameters

[in]	env	The environment to inspect.
[in]	property	The property to check the satisfiability of.
[in]	opts	A list of options to apply. 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 simulation. In case of error, NUXMV_VALID_RESULT() evaluates to false.

See also

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

Requirements: 02.003

Attention

This function has not been implemented, yet.

nuxmv_property_get_expr()

nuxmv_expr nuxmv_property_get_expr	(	nuxmv_env	env,
		nuxmv_property	property
	)

Get the expression of a property.

Parameters

[in]	env	The environment to inspect.
[in]	property	The property to check the satisfiability of.

Returns

The expression of the property

Requirements: 02.003

nuxmv_property_get_name()

const char * nuxmv_property_get_name	(	nuxmv_env	env,
		nuxmv_property	property
	)

Get the name of a property.

Parameters

[in]	env	The environment to inspect.
[in]	property	The property to check the satisfiability of.

Returns

The name of the property, NULL if the property doesn't have a name.

Requirements: 02.003

nuxmv_property_get_type()

nuxmv_property_type nuxmv_property_get_type	(	nuxmv_env	env,
		nuxmv_property	property
	)

Get the type of a property.

Parameters

[in]	env	The environment to inspect.
[in]	property	The property to check the satisfiability of.

Returns

The type of the property

Requirements: 02.003