Data Structures

All data types used by the API. More...

Collaboration diagram for Data Structures:

Modules
	Options
	Environment options.

Data Structures
struct	nuxmv_env
	Environment object. More...
struct	nuxmv_opt
	Option object as key-value pair. More...
struct	nuxmv_expr_type
	Expression type object. More...
struct	nuxmv_var_type
	Variable type object. More...
struct	nuxmv_symbol
	Symbol object. More...
struct	nuxmv_expr
	Expression object. More...
struct	nuxmv_module
	Module object. More...
struct	nuxmv_var_decl
	Variable declaration. More...
struct	nuxmv_trace_value
	Symbol value. More...
struct	nuxmv_fun_decl
	Function declaration. More...
struct	nuxmv_assign
	Assignment. More...
struct	nuxmv_compassion
	Compassion constraint. More...
struct	nuxmv_define_decl
	Define declaration. More...
struct	nuxmv_model
	Model object. More...
struct	nuxmv_property
	Property object. More...
struct	nuxmv_result
	Result code object. More...
struct	nuxmv_trace
	Trace object. More...
struct	nuxmv_simulation
	Simulation object. More...
struct	nuxmv_simulation_constraint
	Simulation constraint object. More...

Typedefs
typedef struct nuxmv_env	nuxmv_env
	Environment object.
typedef struct nuxmv_opt	nuxmv_opt
	Option object as key-value pair.
typedef struct nuxmv_expr_type	nuxmv_expr_type
	Expression type object.
typedef enum nuxmv_expr_type_tag	nuxmv_expr_type_tag
	Tags for expression types.
typedef struct nuxmv_var_type	nuxmv_var_type
	Variable type object.
typedef enum nuxmv_var_type_tag	nuxmv_var_type_tag
typedef struct nuxmv_symbol	nuxmv_symbol
	Symbol object.
typedef struct nuxmv_expr	nuxmv_expr
	Expression object.
typedef enum nuxmv_op_tag	nuxmv_op_tag
	Operators.
typedef enum nuxmv_expr_visit_order	nuxmv_expr_visit_order
	Visiting order.
typedef enum nuxmv_expr_visit_status	nuxmv_expr_visit_status
	States when visiting an expression.
typedef nuxmv_expr_visit_status(*	nuxmv_expr_visit_callback) (nuxmv_env env, nuxmv_expr expr, void *user_data)
	Type for user-defined callback functions when visiting an expression.
typedef struct nuxmv_module	nuxmv_module
	Module object.
typedef struct nuxmv_var_decl	nuxmv_var_decl
	Variable declaration.
typedef struct nuxmv_trace_value	nuxmv_trace_value
	Symbol value.
typedef struct nuxmv_fun_decl	nuxmv_fun_decl
	Function declaration.
typedef struct nuxmv_assign	nuxmv_assign
	Assignment.
typedef struct nuxmv_compassion	nuxmv_compassion
	Compassion constraint.
typedef struct nuxmv_define_decl	nuxmv_define_decl
	Define declaration.
typedef enum nuxmv_model_format	nuxmv_model_format
	Model formats.
typedef struct nuxmv_model	nuxmv_model
	Model object.
typedef enum nuxmv_property_type	nuxmv_property_type
	Property types.
typedef struct nuxmv_property	nuxmv_property
	Property object.
typedef enum nuxmv_result_code	nuxmv_result_code
	Result codes.
typedef struct nuxmv_result	nuxmv_result
	Result code object.
typedef enum nuxmv_trace_format	nuxmv_trace_format
	Trace formats.
typedef struct nuxmv_trace	nuxmv_trace
	Trace object.
typedef struct nuxmv_simulation	nuxmv_simulation
	Simulation object.
typedef struct nuxmv_simulation_constraint	nuxmv_simulation_constraint
	Simulation constraint object.
typedef bool(*	nuxmv_serialized_chunk_callback) (char *chunk, size_t chunk_size, void *user_data)
	Type for callback function when processing serialized streams.

Enumerations
enum	nuxmv_expr_type_tag {   NUXMV_TYPE_INVALID = -1 , NUXMV_TYPE_BOOL , NUXMV_TYPE_INT , NUXMV_TYPE_REAL ,   NUXMV_TYPE_ENUM , NUXMV_TYPE_SET , NUXMV_TYPE_SIGNED_WORD , NUXMV_TYPE_UNSIGNED_WORD ,   NUXMV_TYPE_ARRAY , NUXMV_TYPE_FUNCTION , NUXMV_TYPE_LAST_ }
	Tags for expression types. More...
enum	nuxmv_var_type_tag {   NUXMV_VAR_TYPE_INVALID = -1 , NUXMV_VAR_TYPE_BOOL , NUXMV_VAR_TYPE_INT , NUXMV_VAR_TYPE_REAL ,   NUXMV_VAR_TYPE_ENUM , NUXMV_VAR_TYPE_INT_ENUM , NUXMV_VAR_TYPE_INT_RANGE , NUXMV_VAR_TYPE_SIGNED_WORD ,   NUXMV_VAR_TYPE_UNSIGNED_WORD , NUXMV_VAR_TYPE_ARRAY , NUXMV_VAR_TYPE_FUNCTION , NUXMV_VAR_TYPE_LAST_ }
enum	nuxmv_op_tag {   NUXMV_OP_INVALID = -1 , NUXMV_OP_AND , NUXMV_OP_OR , NUXMV_OP_NOT ,   NUXMV_OP_XOR , NUXMV_OP_XNOR , NUXMV_OP_IMPLIES , NUXMV_OP_IFF ,   NUXMV_OP_EQ , NUXMV_OP_NEQ , NUXMV_OP_GT , NUXMV_OP_GTE ,   NUXMV_OP_LT , NUXMV_OP_LTE , NUXMV_OP_NEGATIVE_NUM , NUXMV_OP_PLUS ,   NUXMV_OP_MINUS , NUXMV_OP_TIMES , NUXMV_OP_DIV , NUXMV_OP_MOD ,   NUXMV_OP_LSHIFT , NUXMV_OP_RSHIFT , NUXMV_OP_ABS , NUXMV_OP_ACOS ,   NUXMV_OP_ASIN , NUXMV_OP_ATAN , NUXMV_OP_COS , NUXMV_OP_EXP ,   NUXMV_OP_FLOOR , NUXMV_OP_LN , NUXMV_OP_MAX , NUXMV_OP_MIN ,   NUXMV_OP_PI , NUXMV_OP_POW , NUXMV_OP_SIN , NUXMV_OP_SQRT ,   NUXMV_OP_TAN , NUXMV_OP_NEXT_FUNCTION , NUXMV_OP_GLOBALLY , NUXMV_OP_FINALLY ,   NUXMV_OP_NEXT , NUXMV_OP_UNTIL , NUXMV_OP_RELEASE , NUXMV_OP_HISTORICALLY ,   NUXMV_OP_ONCE , NUXMV_OP_YESTERDAY , NUXMV_OP_SINCE , NUXMV_OP_TRIGGERED ,   NUXMV_OP_INDEX_ACCESS , NUXMV_OP_ARRAY_READ , NUXMV_OP_ARRAY_WRITE , NUXMV_OP_BIT_SELECTION ,   NUXMV_OP_WORD_CONCAT , NUXMV_OP_CAST_WORD1 , NUXMV_OP_CAST_BOOL , NUXMV_OP_CAST_TOINT ,   NUXMV_OP_CAST_SIGNED , NUXMV_OP_CAST_UNSIGNED , NUXMV_OP_CAST_SIGNED_WORD , NUXMV_OP_CAST_UNSIGNED_WORD ,   NUXMV_OP_EXTEND , NUXMV_OP_RESIZE , NUXMV_OP_SET_UNION , NUXMV_OP_SET_IN ,   NUXMV_OP_IFTHENELSE , NUXMV_OP_UF , NUXMV_OP_LAST_ }
	Operators. More...
enum	nuxmv_expr_visit_order { NUXMV_EXPR_VISIT_PRE_ORDER , NUXMV_EXPR_VISIT_POST_ORDER }
	Visiting order. More...
enum	nuxmv_expr_visit_status { NUXMV_EXPR_VISIT_PROCESS , NUXMV_EXPR_VISIT_SKIP , NUXMV_EXPR_VISIT_ABORT }
	States when visiting an expression. More...
enum	nuxmv_model_format { NUXMV_MODEL_FORMAT_SMV , NUXMV_MODEL_FORMAT_VMT , NUXMV_MODEL_FORMAT_AIG }
	Model formats. More...
enum	nuxmv_property_type { NUXMV_PROPERTY_INVALID = -1 , NUXMV_PROPERTY_INVARSPEC , NUXMV_PROPERTY_LTLSPEC }
	Property types. More...
enum	nuxmv_result_code { NUXMV_RESULT_INVALID = -1 , NUXMV_RESULT_FALSE , NUXMV_RESULT_TRUE , NUXMV_RESULT_UNKNOWN }
	Result codes. More...
enum	nuxmv_trace_format { NUXMV_TRACE_FORMAT_XML }
	Trace formats. More...

Detailed Description

All data types used by the API.

---

This section lists all data types.

Typedef Documentation

nuxmv_assign

typedef struct nuxmv_assign nuxmv_assign

Assignment.

An assignment consists of a pair of expressions: the left- and the right-hand sides of the equal sign.

See also

• NUXMV_VALID_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_compassion

typedef struct nuxmv_compassion nuxmv_compassion

Compassion constraint.

A compassion constraint consists of a pair of formulas (p, q); if property p is true infinitely often in a fair path, then also formula q has to be true infinitely often in the fair path.

See also

• NUXMV_VALID_COMPASSION()
• nuxmv_module_get_compassion()
• nuxmv_model_get_compassion()

nuxmv_define_decl

typedef struct nuxmv_define_decl nuxmv_define_decl

Define declaration.

A define declaration is a pair of identifier (expression) and body associating the expression to the body.

Note

Heterogeneous defines are not supported. Types of body and identifier must be equal.

See also

• NUXMV_VALID_DEFINE_DECL()
• nuxmv_module_get_define()
• nuxmv_model_get_define()

nuxmv_env

typedef struct nuxmv_env nuxmv_env

Environment object.

See also

• nuxmv_create_env()

nuxmv_expr

typedef struct nuxmv_expr nuxmv_expr

Expression object.

See also

• nuxmv_make_identifier()
• nuxmv_make_value()
• nuxmv_make_op()
• nuxmv_make_expr_from_string()
• nuxmv_simplify_expr()

nuxmv_expr_type

typedef struct nuxmv_expr_type nuxmv_expr_type

Expression type object.

See also

• nuxmv_make_boolean_type()
• nuxmv_make_integer_type()
• nuxmv_make_real_type()
• nuxmv_make_enum_type()
• nuxmv_make_set_type()
• nuxmv_make_signed_word_type()
• nuxmv_make_unsigned_word_type()
• nuxmv_make_array_type()
• nuxmv_make_function_type()

nuxmv_expr_type_tag

typedef enum nuxmv_expr_type_tag nuxmv_expr_type_tag

Tags for expression types.

See also

• nuxmv_expr_type
• nuxmv_expr_type_get_tag()

nuxmv_expr_visit_callback

typedef nuxmv_expr_visit_status(* nuxmv_expr_visit_callback) (nuxmv_env env, nuxmv_expr expr, void *user_data)

Type for user-defined callback functions when visiting an expression.

This function pointer type defines the signature for callbacks that are invoked when visiting an expression.

Parameters

[in]	env	Environment of the expression being visited.
[in]	expr	Currently visited expression.
[in]	user_data	Any user-defined context data passed via nuxmv_visit_expr().

See also

• nuxmv_visit_expr()

nuxmv_expr_visit_order

typedef enum nuxmv_expr_visit_order nuxmv_expr_visit_order

Visiting order.

See also

• nuxmv_visit_expr()

nuxmv_expr_visit_status

typedef enum nuxmv_expr_visit_status nuxmv_expr_visit_status

States when visiting an expression.

User-defined callback functions shall return one of the following code in order to instruct the visiting routine what to do next.

See also

• nuxmv_expr_visit_callback
• nuxmv_visit_expr()

nuxmv_fun_decl

typedef struct nuxmv_fun_decl nuxmv_fun_decl

Function declaration.

A function declaration is a pair of identifier and nuxmv_expr_type associating the identifier to the function type.

See also

• NUXMV_MAKE_FUN_DECL()
• nuxmv_module_add_function()
• nuxmv_module_get_function()

nuxmv_model

typedef struct nuxmv_model nuxmv_model

Model object.

See also

• nuxmv_create_model()
• nuxmv_create_model_from_string()

nuxmv_model_format

typedef enum nuxmv_model_format nuxmv_model_format

Model formats.

See also

• nuxmv_create_model_from_string()
• nuxmv_serialize_model_to_string()

nuxmv_module

typedef struct nuxmv_module nuxmv_module

Module object.

See also

• nuxmv_create_module()
• nuxmv_create_module_from_property()

nuxmv_op_tag

typedef enum nuxmv_op_tag nuxmv_op_tag

Operators.

See also

• nuxmv_expr_get_op_tag()
• nuxmv_expr_contains_temporal_operators()

nuxmv_opt

typedef struct nuxmv_opt nuxmv_opt

Option object as key-value pair.

nuxmv_property

typedef struct nuxmv_property nuxmv_property

Property object.

See also

• nuxmv_make_property()
• nuxmv_make_property_from_string()

nuxmv_property_type

typedef enum nuxmv_property_type nuxmv_property_type

Property types.

See also

• nuxmv_make_property()
• nuxmv_make_property_from_string()

nuxmv_result

typedef struct nuxmv_result nuxmv_result

Result code object.

See also

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

nuxmv_result_code

typedef enum nuxmv_result_code nuxmv_result_code

Result codes.

These codes are general and their interpretation depends on the checking context.

See also

• nuxmv_result_get_code()

nuxmv_serialized_chunk_callback

typedef bool(* nuxmv_serialized_chunk_callback) (char *chunk, size_t chunk_size, void *user_data)

Type for callback function when processing serialized streams.

This function pointer type defines the signature for callbacks that are invoked by a serialization routine whenever a chunk of serialized data becomes available. The user can implement this callback to process the data in a stream-like fashion.

Parameters

[in]	chunk	Pointer to the current chunk of serialized data.
[in]	chunk_size	Size of the data chunk in bytes.
[in]	user_data	Any user-defined context data, passed via serialization functions.

Returns

true to signal to the serialization function to continue processing subsequent chunks, false to instruct it to stop the process.

See also

• nuxmv_serialize_model_to_string()
• nuxmv_serialize_trace_to_string()

Requirements: 03.002

nuxmv_simulation

typedef struct nuxmv_simulation nuxmv_simulation

Simulation object.

See also

• nuxmv_create_simulation()

nuxmv_simulation_constraint

typedef struct nuxmv_simulation_constraint nuxmv_simulation_constraint

Simulation constraint object.

See also

• NUXMV_MAKE_SIMULATION_CONSTRAINT()
• NUXMV_MAKE_INVALID_EXPR()
• nuxmv_create_simulation()
• nuxmv_extend_simulation()

nuxmv_symbol

typedef struct nuxmv_symbol nuxmv_symbol

Symbol object.

See also

• nuxmv_make_symbol()
• nuxmv_make_scoped_symbol()

nuxmv_trace

typedef struct nuxmv_trace nuxmv_trace

Trace object.

See also

• nuxmv_result_get_trace()
• nuxmv_make_trace_from_string()

nuxmv_trace_format

typedef enum nuxmv_trace_format nuxmv_trace_format

Trace formats.

See also

• nuxmv_make_trace_from_string()
• nuxmv_serialize_trace_to_string()

nuxmv_trace_value

typedef struct nuxmv_trace_value nuxmv_trace_value

Symbol value.

A symbol value is a pair of identifier and value associating the symbol identifier to the symbol value.

See also

• NUXMV_VALID_TRACE_VALUE()
• nuxmv_trace_get_step_state()
• nuxmv_trace_get_step_input()
• nuxmv_trace_get_step_define()
• nuxmv_trace_get_function()

nuxmv_var_decl

typedef struct nuxmv_var_decl nuxmv_var_decl

Variable declaration.

A variable declaration is a pair of identifier and var_type associating the identifier to the variable type.

See also

• NUXMV_MAKE_VAR_DECL()
• nuxmv_module_add_state_var()
• nuxmv_model_get_state_var()

nuxmv_var_type

typedef struct nuxmv_var_type nuxmv_var_type

Variable type object.

See also

• nuxmv_make_simple_var_type()
• nuxmv_make_var_type_with_domain()
• nuxmv_make_var_type_with_integer_range()
• nuxmv_make_var_type_array()

nuxmv_var_type_tag

typedef enum nuxmv_var_type_tag nuxmv_var_type_tag

Enumeration Type Documentation

nuxmv_expr_type_tag

enum nuxmv_expr_type_tag

Tags for expression types.

See also

• nuxmv_expr_type
• nuxmv_expr_type_get_tag()

Enumerator
NUXMV_TYPE_INVALID	Not a valid type.
NUXMV_TYPE_BOOL	Boolean type.
NUXMV_TYPE_INT	Unbound integer type.
NUXMV_TYPE_REAL	Real type.
NUXMV_TYPE_ENUM	Symbolic enumerative type
NUXMV_TYPE_SET	Set type.
NUXMV_TYPE_SIGNED_WORD	Signed word type.
NUXMV_TYPE_UNSIGNED_WORD	Unsigned word type.
NUXMV_TYPE_ARRAY	Array type.
NUXMV_TYPE_FUNCTION	Function type.
NUXMV_TYPE_LAST_	(List terminator.)

nuxmv_expr_visit_order

enum nuxmv_expr_visit_order

Visiting order.

See also

• nuxmv_visit_expr()

Enumerator
NUXMV_EXPR_VISIT_PRE_ORDER	Each node is traversed before its children.
NUXMV_EXPR_VISIT_POST_ORDER	Each node is traversed after its children.

nuxmv_expr_visit_status

enum nuxmv_expr_visit_status

States when visiting an expression.

User-defined callback functions shall return one of the following code in order to instruct the visiting routine what to do next.

See also

• nuxmv_expr_visit_callback
• nuxmv_visit_expr()

Enumerator
NUXMV_EXPR_VISIT_PROCESS	Process current node's children.
NUXMV_EXPR_VISIT_SKIP	Skip current node's children.
NUXMV_EXPR_VISIT_ABORT	Abort the visiting process.

nuxmv_model_format

enum nuxmv_model_format

Model formats.

See also

• nuxmv_create_model_from_string()
• nuxmv_serialize_model_to_string()

Enumerator
NUXMV_MODEL_FORMAT_SMV	Model follows Symbolic Model Verifier format
NUXMV_MODEL_FORMAT_VMT	Model follows Verification Modulo Theories format
NUXMV_MODEL_FORMAT_AIG	Model follows AIG Model Checker format

nuxmv_op_tag

enum nuxmv_op_tag

Operators.

See also

• nuxmv_expr_get_op_tag()
• nuxmv_expr_contains_temporal_operators()

Enumerator
NUXMV_OP_INVALID	Not a valid operator.
NUXMV_OP_AND	Logical conjunction operator.
NUXMV_OP_OR	Logical disjunction operator.
NUXMV_OP_NOT	Logical negation operator.
NUXMV_OP_XOR	Logical exclusive disjunction operator.
NUXMV_OP_XNOR	Logical exclusive NOR operator.
NUXMV_OP_IMPLIES	Logical conditional operator.
NUXMV_OP_IFF	Logical biconditional operator.
NUXMV_OP_EQ	Equal to operator.
NUXMV_OP_NEQ	Not equal to operator.
NUXMV_OP_GT	Greater than operator.
NUXMV_OP_GTE	Greater than or equal to operator.
NUXMV_OP_LT	Less than operator.
NUXMV_OP_LTE	Less than or equal to operator.
NUXMV_OP_NEGATIVE_NUM	Negative number sign. (car(n) is the number)
NUXMV_OP_PLUS	Addition operator.
NUXMV_OP_MINUS	Subtraction operator.
NUXMV_OP_TIMES	Multiplication operator.
NUXMV_OP_DIV	Division operator.
NUXMV_OP_MOD	Modulo operator.
NUXMV_OP_LSHIFT	Left shift operator.
NUXMV_OP_RSHIFT	Right shift operator.
NUXMV_OP_ABS	Absolute operator.
NUXMV_OP_ACOS	Arccosine function (acos(x)).
NUXMV_OP_ASIN	Arcsine function (asin(x)).
NUXMV_OP_ATAN	Arctangent function (atan(x)).
NUXMV_OP_COS	Cosine operator.
NUXMV_OP_EXP	Euler's number exponentiation operator.
NUXMV_OP_FLOOR	Floor operator.
NUXMV_OP_LN	Natural logarithm operator.
NUXMV_OP_MAX	Maximum operator.
NUXMV_OP_MIN	Minimum operator.
NUXMV_OP_PI	Pi constant.
NUXMV_OP_POW	Exponentiation operator.
NUXMV_OP_SIN	Sine operator.
NUXMV_OP_SQRT	Square root function (sqrt(x)).
NUXMV_OP_TAN	Tangent operator.
NUXMV_OP_NEXT_FUNCTION	next function.
NUXMV_OP_GLOBALLY	Globally temporal operator.
NUXMV_OP_FINALLY	Finally temporal operator.
NUXMV_OP_NEXT	Next temporal operator.
NUXMV_OP_UNTIL	Until temporal operator.
NUXMV_OP_RELEASE	Release temporal operator.
NUXMV_OP_HISTORICALLY	Historically temporal operator.
NUXMV_OP_ONCE	Once temporal operator.
NUXMV_OP_YESTERDAY	Yesterday temporal operator.
NUXMV_OP_SINCE	Since temporal operator.
NUXMV_OP_TRIGGERED	Triggered temporal operator.
NUXMV_OP_INDEX_ACCESS	array[index] access operator.
NUXMV_OP_ARRAY_READ	array read operator.
NUXMV_OP_ARRAY_WRITE	array write operator.
NUXMV_OP_BIT_SELECTION	word[j:i] bit selection operator.
NUXMV_OP_WORD_CONCAT	Word concatenation (w1 :: w2) operator.
NUXMV_OP_CAST_WORD1	Cast boolean to unsigned word[1].
NUXMV_OP_CAST_BOOL	Cast int or unsigned word[1] to boolean
NUXMV_OP_CAST_TOINT	Cast boolean word to integer
NUXMV_OP_CAST_SIGNED	Cast unsigned to signed word operator.
NUXMV_OP_CAST_UNSIGNED	Cast signed to unsigned word operator.
NUXMV_OP_CAST_SIGNED_WORD	Cast integer to signed word.
NUXMV_OP_CAST_UNSIGNED_WORD	Cast integer to unsigned word.
NUXMV_OP_EXTEND	Word extension function (extend(word, n)).
NUXMV_OP_RESIZE	Word resize function (resize(word, n)).
NUXMV_OP_SET_UNION	Set union (s1 union s2) operator.
NUXMV_OP_SET_IN	Set inclusion check (e in s) operator.
NUXMV_OP_IFTHENELSE	Ternary if-then-else operator.
NUXMV_OP_UF	Apply a generic symbol to a list of arguments.
NUXMV_OP_LAST_	(List terminator.)

nuxmv_property_type

enum nuxmv_property_type

Property types.

See also

• nuxmv_make_property()
• nuxmv_make_property_from_string()

Enumerator
NUXMV_PROPERTY_INVALID	Not a valid property.
NUXMV_PROPERTY_INVARSPEC	Property is an invariant.
NUXMV_PROPERTY_LTLSPEC	Generic property with temporal operators.

nuxmv_result_code

enum nuxmv_result_code

Result codes.

These codes are general and their interpretation depends on the checking context.

See also

• nuxmv_result_get_code()

Enumerator
NUXMV_RESULT_INVALID	Not a valid result.
NUXMV_RESULT_FALSE	The property checked was false.
NUXMV_RESULT_TRUE	The property checked was true.
NUXMV_RESULT_UNKNOWN	The check result is still not known.

nuxmv_trace_format

enum nuxmv_trace_format

Trace formats.

See also

• nuxmv_make_trace_from_string()
• nuxmv_serialize_trace_to_string()

Enumerator
NUXMV_TRACE_FORMAT_XML	Trace follows the Extensible Markup Language syntax.

nuxmv_var_type_tag

enum nuxmv_var_type_tag

Enumerator
NUXMV_VAR_TYPE_INVALID
NUXMV_VAR_TYPE_BOOL	Boolean type.
NUXMV_VAR_TYPE_INT	Unbound integer type.
NUXMV_VAR_TYPE_REAL	Real type.
NUXMV_VAR_TYPE_ENUM	Symbolic enumerative type
NUXMV_VAR_TYPE_INT_ENUM	Integer enumerative type
NUXMV_VAR_TYPE_INT_RANGE	Bound integer type.
NUXMV_VAR_TYPE_SIGNED_WORD	Signed word type.
NUXMV_VAR_TYPE_UNSIGNED_WORD	Unsigned word type.
NUXMV_VAR_TYPE_ARRAY	Array type.
NUXMV_VAR_TYPE_FUNCTION	Function type.
NUXMV_VAR_TYPE_LAST_