Functions for handling Models. More...

Collaboration diagram for Models:

Modules
	Model Variable Getters
	Functions for getting Variables from a Model.

	Model Assign Getters
	Functions for getting Assigns from a Model.

	Model Property Getters
	Functions for getting Properties from a Model.

	Add property to Model
	Functions for adding Properties to a Model.

Macros
#define	NUXMV_VALID_MODEL(model) ((model).repr != NULL)
	Valid model.

Functions
nuxmv_model	nuxmv_create_model (nuxmv_env env, nuxmv_module module, const nuxmv_expr *params, size_t param_num)
	Create a new model instantiating a module with the desired parameters.

nuxmv_model	nuxmv_create_model_from_string (nuxmv_env env, nuxmv_model_format fmt, const char *data)
	Create a model from a string.

int	nuxmv_serialize_model_to_string (nuxmv_env env, nuxmv_model model, nuxmv_model_format fmt, nuxmv_serialized_chunk_callback callback, void user_data, char data, size_t data_size)
	Serialize a model to a string.

nuxmv_result	nuxmv_model_check_property (nuxmv_env env, nuxmv_model model, nuxmv_property property, const nuxmv_opt *opts, size_t opt_num)
	Check the given property on a model.

nuxmv_result	nuxmv_model_check_deadlock (nuxmv_env env, nuxmv_model model, const nuxmv_opt *opts, size_t opt_num)
	Check for deadlock freedom.

nuxmv_result	nuxmv_model_check_receptiveness (nuxmv_env env, nuxmv_model model, const nuxmv_opt *opts, size_t opt_num)
	Check for receptiveness to inputs.

nuxmv_status_code	nuxmv_destroy_model (nuxmv_env env, nuxmv_model model)
	Destroy a model.

Detailed Description

Functions for handling Models.

Macro Definition Documentation

◆ NUXMV_VALID_MODEL

#define NUXMV_VALID_MODEL ( model ) ((model).repr != NULL)

Valid model.

This macro checks whether model is a valid nuxmv_model.

Parameters

[in] model The model to inspect.

Returns: true if the option is valid, false otherwise.

Function Documentation

◆ nuxmv_create_model()

nuxmv_model nuxmv_create_model	(	nuxmv_env	env,
		nuxmv_module	module,
		const nuxmv_expr *	params,
		size_t	param_num
	)

Create a new model instantiating a module with the desired parameters.

Parameters

[in]	env	The environment to modify.
[in]	module	The module to instantiate into a model. The module must not be destroyed while the model is still in use.
[in]	params	A list of parameters for the model. 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: The newly created model. In case of error, NUXMV_VALID_MODEL() evaluates to false.

See also

Requirements: 03.009.03

◆ nuxmv_create_model_from_string()

nuxmv_model nuxmv_create_model_from_string	(	nuxmv_env	env,
		nuxmv_model_format	fmt,
		const char *	data
	)

Create a model from a string.

Parameters

[in]	env	The environment to modify.
[in]	fmt	The format of the input string.
[in]	data	A null-terminated string containing the model data.

Returns: The newly created model corresponding to the string. In case of error, NUXMV_VALID_MODEL() evaluates to false.

Note: A current limitation of this function is that it always returns a flattened model, consisting only of a single root module, even if the input string contains submodules. We plan to remove this limitation in future releases.

See also

Requirements: 03.005

◆ nuxmv_destroy_model()

nuxmv_status_code nuxmv_destroy_model	(	nuxmv_env	env,
		nuxmv_model	model
	)

Destroy a model.

With this function, the user notifies the environment that the selected model is no more needed.

Parameters

[in]	env	The environment to modify.
[in]	model	A model to destroy.

Returns: NUXMV_SUCCESS if the module was destroyed, NUXMV_FAILURE in case of error.

See also

Requirements: 03.004.01

◆ nuxmv_model_check_deadlock()

nuxmv_result nuxmv_model_check_deadlock	(	nuxmv_env	env,
		nuxmv_model	model,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Check for deadlock freedom.

Parameters

[in]	env	The environment to inspect.
[in]	model	A model to check the deadlock on.
[in]	opts	A list of options for the check.
[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 checking. In case of error, NUXMV_VALID_RESULT() evaluates to false.

See also

Requirements: 02.005

Attention: This function has not been implemented, yet.

◆ nuxmv_model_check_property()

nuxmv_result nuxmv_model_check_property	(	nuxmv_env	env,
		nuxmv_model	model,
		nuxmv_property	property,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Check the given property on a model.

Parameters

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

See also

Requirements: 02.001

◆ nuxmv_model_check_receptiveness()

nuxmv_result nuxmv_model_check_receptiveness	(	nuxmv_env	env,
		nuxmv_model	model,
		const nuxmv_opt *	opts,
		size_t	opt_num
	)

Check for receptiveness to inputs.

Parameters

[in]	env	The environment to inspect.
[in]	model	A model to check the deadlock on.
[in]	opts	A list of options for the check. 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 checking. In case of error, NUXMV_VALID_RESULT() evaluates to false.

See also

Requirements: ??

Attention: This function has not been implemented, yet.

◆ nuxmv_serialize_model_to_string()

int nuxmv_serialize_model_to_string	(	nuxmv_env	env,
		nuxmv_model	model,
		nuxmv_model_format	fmt,
		nuxmv_serialized_chunk_callback	callback,
		void *	user_data,
		char *	data,
		size_t	data_size
	)

Serialize a model to a string.

This function converts the given model into a string representation using the specified 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]	model	The model to serialize.
[in]	fmt	The format to use for serialization.
[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

Requirements: 03.002

Modules

Macros

Functions

Detailed Description

Macro Definition Documentation

◆ NUXMV_VALID_MODEL

Function Documentation

◆ nuxmv_create_model()

◆ nuxmv_create_model_from_string()

◆ nuxmv_destroy_model()

◆ nuxmv_model_check_deadlock()

◆ nuxmv_model_check_property()

◆ nuxmv_model_check_receptiveness()

◆ nuxmv_serialize_model_to_string()