|
| nuxmv_env | nuxmv_create_env (void) |
| | Create a new environment.
|
| |
| nuxmv_status_code | nuxmv_destroy_env (nuxmv_env env) |
| | Destroy an environment.
|
| |
| const char * | nuxmv_env_get_last_error_message (nuxmv_env env) |
| | Get the last error message and clear it.
|
| |
| nuxmv_status_code | nuxmv_env_set_options (nuxmv_env env, const nuxmv_opt *opts, size_t opt_num) |
| | Set a list of options for the environment.
|
| |
| int | nuxmv_env_get_option_num (nuxmv_env env) |
| | Get the number of options for the environment.
|
| |
| nuxmv_opt | nuxmv_env_get_option (nuxmv_env env, int opt_idx) |
| | Get an option of the environment.
|
| |
| nuxmv_expr_type | nuxmv_make_boolean_type (nuxmv_env env) |
| | Create a Boolean type.
|
| |
| nuxmv_expr_type | nuxmv_make_integer_type (nuxmv_env env) |
| | Create an integer type.
|
| |
| nuxmv_expr_type | nuxmv_make_real_type (nuxmv_env env) |
| | Create a real type.
|
| |
| nuxmv_expr_type | nuxmv_make_enum_type (nuxmv_env env) |
| | Create an enumerative type whose variants are symbolic tags.
|
| |
| nuxmv_expr_type | nuxmv_make_set_type (nuxmv_env env, nuxmv_expr_type elem) |
| | Create a set type.
|
| |
| nuxmv_expr_type | nuxmv_make_signed_word_type (nuxmv_env env, size_t width) |
| | Create a signed word type.
|
| |
| nuxmv_expr_type | nuxmv_make_unsigned_word_type (nuxmv_env env, size_t width) |
| | Create an unsigned word type.
|
| |
| nuxmv_expr_type | nuxmv_make_array_type (nuxmv_env env, nuxmv_expr_type idx, nuxmv_expr_type elem) |
| | Create an array type.
|
| |
| nuxmv_expr_type | nuxmv_make_function_type (nuxmv_env env, const nuxmv_expr_type *args, size_t arg_num, nuxmv_expr_type result) |
| | Create a new (uninterpreted) function type.
|
| |
| nuxmv_expr_type_tag | nuxmv_expr_type_get_tag (nuxmv_env env, nuxmv_expr_type type) |
| | Get the tag of a type.
|
| |
| size_t | nuxmv_expr_type_get_id (nuxmv_env env, nuxmv_expr_type type) |
| | Get the ID of a type.
|
| |
| int | nuxmv_word_type_get_width (nuxmv_env env, nuxmv_expr_type type) |
| | Get the width of a (un)signed word type.
|
| |
| nuxmv_expr_type | nuxmv_array_type_get_index (nuxmv_env env, nuxmv_expr_type type) |
| | Get the type of the index of an array type.
|
| |
| nuxmv_expr_type | nuxmv_array_type_get_element (nuxmv_env env, nuxmv_expr_type type) |
| | Get the type of the elements of an array type.
|
| |
| int | nuxmv_function_type_get_argument_num (nuxmv_env env, nuxmv_expr_type type) |
| | Get the number of arguments of a function type.
|
| |
| nuxmv_expr_type | nuxmv_function_type_get_argument (nuxmv_env env, nuxmv_expr_type type, int arg_idx) |
| | Get the i-th argument type of a function type.
|
| |
| nuxmv_expr_type | nuxmv_function_type_get_result (nuxmv_env env, nuxmv_expr_type type) |
| | Get the type of the result of a function type.
|
| |
| nuxmv_expr_type | nuxmv_set_type_get_element (nuxmv_env env, nuxmv_expr_type type) |
| | Get the type of the elements of a set type.
|
| |
| nuxmv_var_type | nuxmv_make_simple_var_type (nuxmv_env env, nuxmv_expr_type type) |
| | Get the variable type corresponding to a type.
|
| |
| nuxmv_var_type | nuxmv_make_var_type_with_domain (nuxmv_env env, const nuxmv_expr *domain, size_t domain_num) |
| | Get the variable type corresponding to an enumerative.
|
| |
| nuxmv_var_type | nuxmv_make_var_type_with_integer_range (nuxmv_env env, int min, int max) |
| | Returns the var_type corresponding to the selected bounded int type.
|
| |
| nuxmv_var_type | nuxmv_make_var_type_array (nuxmv_env env, nuxmv_var_type idx, nuxmv_var_type elem) |
| | Builds an array var_type.
|
| |
| nuxmv_expr_type | nuxmv_var_type_get_expr_type (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the expression type corresponding to a variable type.
|
| |
| nuxmv_var_type_tag | nuxmv_var_type_get_tag (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the tag of a var_type.
|
| |
| size_t | nuxmv_var_type_get_id (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the ID of a var type.
|
| |
| nuxmv_var_type | nuxmv_var_type_array_get_index (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the var type of the index of an array var type.
|
| |
| nuxmv_var_type | nuxmv_var_type_array_get_element (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the var type of the element of an array var type.
|
| |
| int | nuxmv_var_type_integer_range_get_min (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the min value an integer range var type.
|
| |
| int | nuxmv_var_type_integer_range_get_max (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the max value an integer range var type.
|
| |
| int | nuxmv_var_type_get_domain_num (nuxmv_env env, nuxmv_var_type var_type) |
| | Get the number of elements of a var type with domain.
|
| |
| nuxmv_expr | nuxmv_var_type_get_domain_element (nuxmv_env env, nuxmv_var_type var_type, int elem_idx) |
| | Get the domain element at the given index of a var type with domain.
|
| |
| nuxmv_symbol | nuxmv_make_symbol (nuxmv_env env, const char *name) |
| | Create a new symbol.
|
| |
| nuxmv_symbol | nuxmv_make_scoped_symbol (nuxmv_env env, const char *name, nuxmv_symbol scope) |
| | Create a new symbol with the given name and context.
|
| |
| size_t | nuxmv_symbol_get_id (nuxmv_env env, nuxmv_symbol sym) |
| | Get the ID of a symbol.
|
| |
| const char * | nuxmv_symbol_get_name (nuxmv_env env, nuxmv_symbol symbol) |
| | Get the name of a symbol.
|
| |
| int | nuxmv_symbol_is_scoped (nuxmv_env env, nuxmv_symbol symbol) |
| | Test whether a symbol is scoped.
|
| |
| nuxmv_symbol | nuxmv_symbol_get_scope (nuxmv_env env, nuxmv_symbol symbol) |
| | Get the scope of a symbol.
|
| |
| nuxmv_expr | nuxmv_make_identifier (nuxmv_env env, nuxmv_symbol symbol, nuxmv_expr_type type) |
| | Create a new identifier for a symbol.
|
| |
| nuxmv_expr | nuxmv_make_value (nuxmv_env env, nuxmv_symbol val, nuxmv_expr_type type) |
| | Create a new value for a symbol.
|
| |
| nuxmv_expr | nuxmv_make_op (nuxmv_env env, nuxmv_op_tag op, const nuxmv_expr *args, size_t arg_num) |
| | Create a structured expression for an operator.
|
| |
| nuxmv_expr | nuxmv_make_parametric_op (nuxmv_env env, nuxmv_op_tag op, const nuxmv_expr *args, size_t arg_num, const int *params, size_t param_num) |
| | Create a structured parametric expression for an operator.
|
| |
| nuxmv_expr | nuxmv_make_un_op (nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg) |
| | Create a structured expression for a unary operator.
|
| |
| nuxmv_expr | nuxmv_make_bin_op (nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg1, nuxmv_expr arg2) |
| | Create a structured expression for a binary operator.
|
| |
| nuxmv_expr | nuxmv_make_expr_from_string (nuxmv_env env, const char *data, nuxmv_module scope) |
| | Make an expression from a string.
|
| |
| nuxmv_expr_type | nuxmv_expr_get_type (nuxmv_env env, nuxmv_expr expr) |
| | Get the type of an expression.
|
| |
| nuxmv_symbol | nuxmv_expr_get_symbol (nuxmv_env env, nuxmv_expr identifier) |
| | Get the symbol associated to an identifier.
|
| |
| size_t | nuxmv_expr_get_id (nuxmv_env env, nuxmv_expr expr) |
| | Get the ID of a type.
|
| |
| int | nuxmv_serialize_expr_to_string (nuxmv_env env, nuxmv_expr expr, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size) |
| | Serialize a expr to a string.
|
| |
| int | nuxmv_expr_contains_temporal_operators (nuxmv_env env, nuxmv_expr expr) |
| | Test whether an expression contains temporal operators.
|
| |
| int | nuxmv_expr_is_identifier (nuxmv_env env, nuxmv_expr expr) |
| | Test whether an expression corresponds to an identifier.
|
| |
| int | nuxmv_expr_is_value (nuxmv_env env, nuxmv_expr expr) |
| | Test whether an expression corresponds to a value.
|
| |
| int | nuxmv_expr_is_op (nuxmv_env env, nuxmv_expr expr) |
| | Test whether an expression corresponds to an operator.
|
| |
| nuxmv_op_tag | nuxmv_expr_get_op_tag (nuxmv_env env, nuxmv_expr expr) |
| | Get the tag of an operator.
|
| |
| int | nuxmv_expr_get_argument_num (nuxmv_env env, nuxmv_expr expr) |
| | Get the number of arguments in an expression.
|
| |
| nuxmv_expr | nuxmv_expr_get_argument (nuxmv_env env, nuxmv_expr expr, int arg_idx) |
| | Get the i-th argument of a structured expression.
|
| |
| int | nuxmv_expr_is_parametric (nuxmv_env env, nuxmv_expr expr) |
| | Test whether an expression is parametric.
|
| |
| int | nuxmv_expr_get_parameter_num (nuxmv_env env, nuxmv_expr expr) |
| | Get the number of parameters in a parametric expression.
|
| |
| int | nuxmv_expr_get_parameter (nuxmv_env env, nuxmv_expr expr, int param_idx) |
| | Get the i-th parameter value of a structured parametric expression.
|
| |
| int | nuxmv_visit_expr (nuxmv_env env, nuxmv_expr expr, nuxmv_expr_visit_callback callback, nuxmv_expr_visit_order order, void *user_data) |
| | Visit an expression.
|
| |
| nuxmv_expr | nuxmv_simplify_expr (nuxmv_env env, nuxmv_expr expr) |
| | Simplify an expression.
|
| |
| nuxmv_module | nuxmv_create_module (nuxmv_env env, const char *name) |
| | Create a new module.
|
| |
| nuxmv_module | nuxmv_create_module_from_property (nuxmv_env env, const char *name, nuxmv_property property, const nuxmv_opt *opts, size_t opt_num) |
| | Create a new module out of a property.
|
| |
| nuxmv_status_code | nuxmv_destroy_module (nuxmv_env env, nuxmv_module module) |
| | Destroy a module.
|
| |
| nuxmv_module | nuxmv_copy_module (nuxmv_env env, nuxmv_module module, const char *name) |
| | Copy a module.
|
| |
| 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.
|
| |
| const char * | nuxmv_module_get_name (nuxmv_env env, nuxmv_module module) |
| | Get the name of a module.
|
| |
| int | nuxmv_module_get_param_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of parameters of a module.
|
| |
| nuxmv_expr | nuxmv_module_get_param (nuxmv_env env, nuxmv_module module, int param_idx) |
| | Get the i-th parameter of a module.
|
| |
| int | nuxmv_module_get_state_var_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of state variables in a module.
|
| |
| nuxmv_var_decl | nuxmv_module_get_state_var (nuxmv_env env, nuxmv_module module, int var_idx) |
| | Get the i-th state variable of a module.
|
| |
| int | nuxmv_module_get_input_var_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of input variables in a module.
|
| |
| nuxmv_var_decl | nuxmv_module_get_input_var (nuxmv_env env, nuxmv_module module, int var_idx) |
| | Get the i-th input variable of a module.
|
| |
| int | nuxmv_module_get_frozen_var_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of frozen variables in a module.
|
| |
| nuxmv_var_decl | nuxmv_module_get_frozen_var (nuxmv_env env, nuxmv_module module, int var_idx) |
| | Get the i-th frozen variable of a module.
|
| |
| int | nuxmv_module_get_function_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of uninterpreted function declarations in a module.
|
| |
| nuxmv_fun_decl | nuxmv_module_get_function (nuxmv_env env, nuxmv_module module, int fun_idx) |
| | Get the i-th uninterpreted function declaration of a module.
|
| |
| int | nuxmv_module_get_init_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of initial constraints in a module.
|
| |
| nuxmv_expr | nuxmv_module_get_init (nuxmv_env env, nuxmv_module module, int init_idx) |
| | Get the i-th initial constraint of a module.
|
| |
| int | nuxmv_module_get_trans_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of transition constraints in a module.
|
| |
| nuxmv_expr | nuxmv_module_get_trans (nuxmv_env env, nuxmv_module module, int trans_idx) |
| | Get the i-th transition constraint of a module.
|
| |
| int | nuxmv_module_get_invar_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of invariant constraints in a module.
|
| |
| nuxmv_expr | nuxmv_module_get_invar (nuxmv_env env, nuxmv_module module, int invar_idx) |
| | Get the i-th invariant constraint of a module.
|
| |
| int | nuxmv_module_get_justice_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of justice constraints in a module.
|
| |
| nuxmv_expr | nuxmv_module_get_justice (nuxmv_env env, nuxmv_module module, int just_idx) |
| | Get the i-th justice constraint of a module.
|
| |
| int | nuxmv_module_get_compassion_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of compassions in a module.
|
| |
| nuxmv_compassion | nuxmv_module_get_compassion (nuxmv_env env, nuxmv_module module, int comp_idx) |
| | Get the i-th compassion of a module.
|
| |
| int | nuxmv_module_get_define_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of define declarations in a module.
|
| |
| nuxmv_define_decl | nuxmv_module_get_define (nuxmv_env env, nuxmv_module module, int def_idx) |
| | Get the i-th define declaration of a module.
|
| |
| int | nuxmv_module_get_init_assign_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of initial assignments in a module.
|
| |
| nuxmv_assign | nuxmv_module_get_init_assign (nuxmv_env env, nuxmv_module module, int assign_idx) |
| | Get the i-th initial assignment of a module.
|
| |
| int | nuxmv_module_get_next_assign_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of next assignments in a module.
|
| |
| nuxmv_assign | nuxmv_module_get_next_assign (nuxmv_env env, nuxmv_module module, int assign_idx) |
| | Get the i-th next assignment of a module.
|
| |
| int | nuxmv_module_get_invar_assign_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of invariant assignments in a module.
|
| |
| nuxmv_assign | nuxmv_module_get_invar_assign (nuxmv_env env, nuxmv_module module, int assign_idx) |
| | Get the i-th invariant assignment of a module.
|
| |
| int | nuxmv_module_get_property_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of properties in a module.
|
| |
| nuxmv_property | nuxmv_module_get_property (nuxmv_env env, nuxmv_module module, int prop_idx) |
| | Get the i-th property of a module.
|
| |
| int | nuxmv_module_get_submodule_num (nuxmv_env env, nuxmv_module module) |
| | Get the number of submodules in a module.
|
| |
| const char * | nuxmv_module_get_submodule_name (nuxmv_env env, nuxmv_module module, int sub_idx) |
| | Get the name of the i-th submodule of a module.
|
| |
| nuxmv_module | nuxmv_module_get_submodule (nuxmv_env env, nuxmv_module module, int sub_idx) |
| | Get the i-th submodule of a module.
|
| |
| int | nuxmv_module_get_submodule_param_num (nuxmv_env env, nuxmv_module module, int sub_idx) |
| | Get the number of parameters in a submodule.
|
| |
| nuxmv_expr | nuxmv_module_get_submodule_param (nuxmv_env env, nuxmv_module module, int sub_idx, int param_idx) |
| | Get the i-th parameter of a submodule.
|
| |
| int | nuxmv_serialize_module_to_string (nuxmv_env env, nuxmv_module module, bool with_submodules, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size) |
| | Serialize a module to a string in SMV format.
|
| |
| 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.
|
| |
| nuxmv_module | nuxmv_model_get_root_module (nuxmv_env env, nuxmv_model model) |
| | Get the root module of a model.
|
| |
| 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.
|
| |
| int | nuxmv_model_get_init_assign_num (nuxmv_env env, nuxmv_model model) |
| | Get the number of initial assignments in a model.
|
| |
| nuxmv_assign | nuxmv_model_get_init_assign (nuxmv_env env, nuxmv_model model, int assign_idx) |
| | Get the i-th initial assignment of a model.
|
| |
| int | nuxmv_model_get_next_assign_num (nuxmv_env env, nuxmv_model model) |
| | Get the number of next assignments in a model.
|
| |
| nuxmv_assign | nuxmv_model_get_next_assign (nuxmv_env env, nuxmv_model model, int assign_idx) |
| | Get the i-th next assignment of a model.
|
| |
| int | nuxmv_model_get_invar_assign_num (nuxmv_env env, nuxmv_model model) |
| | Get the number of invariant assignments in a model.
|
| |
| nuxmv_assign | nuxmv_model_get_invar_assign (nuxmv_env env, nuxmv_model model, int assign_idx) |
| | Get the i-th invariant assignment of a model.
|
| |
| int | nuxmv_model_get_property_num (nuxmv_env env, nuxmv_model model) |
| | Get the number of properties in a model.
|
| |
| nuxmv_property | nuxmv_model_get_property (nuxmv_env env, nuxmv_model model, int prop_idx) |
| | Get the i-th property of a model.
|
| |
| nuxmv_property | nuxmv_model_get_property_by_name (nuxmv_env env, nuxmv_model model, const char *name) |
| | Get the property of a model by name.
|
| |
| nuxmv_status_code | nuxmv_model_add_property (nuxmv_env env, nuxmv_model model, nuxmv_property property) |
| | Add a property to the model.
|
| |
| 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.
|
| |
| nuxmv_simulation | nuxmv_create_simulation (nuxmv_env env, nuxmv_model model, nuxmv_simulation_constraint constraint, const nuxmv_opt *opts, size_t opt_num) |
| | Create a new simulation for a model.
|
| |
| nuxmv_status_code | nuxmv_destroy_simulation (nuxmv_env env, nuxmv_simulation simulation) |
| | Destroy a simulation.
|
| |
| nuxmv_status_code | nuxmv_extend_simulation (nuxmv_env env, nuxmv_simulation simulation, size_t k, nuxmv_simulation_constraint constraint) |
| | Extend the simulation by k steps.
|
| |
| nuxmv_result | nuxmv_simulation_get_result (nuxmv_env env, nuxmv_simulation simulation) |
| | Get the result out of a simulation.
|
| |
| nuxmv_result_code | nuxmv_result_get_code (nuxmv_env env, nuxmv_result result) |
| | Get the code out of a result.
|
| |
| nuxmv_trace | nuxmv_result_get_trace (nuxmv_env env, nuxmv_result result) |
| | Get the trace stored in a nuxmv_result.
|
| |
| nuxmv_trace | nuxmv_make_trace_from_string (nuxmv_env env, nuxmv_trace_format fmt, const char *data, nuxmv_model model) |
| | Make a trace from string.
|
| |
| int | nuxmv_serialize_trace_to_string (nuxmv_env env, nuxmv_trace trace, nuxmv_trace_format fmt, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size) |
| | Serialize a trace to a string.
|
| |
| nuxmv_result | nuxmv_trace_check_property (nuxmv_env env, nuxmv_trace trace, nuxmv_property property, nuxmv_model model, const nuxmv_opt *opts, size_t opt_num) |
| | Check a property on a trace.
|
| |
| int | nuxmv_trace_get_step_num (nuxmv_env env, nuxmv_trace trace) |
| | Get the number of steps in a trace.
|
| |
| int | nuxmv_trace_get_step_state_num (nuxmv_env env, nuxmv_trace trace, int step_idx) |
| | Get the number of state variables in a trace.
|
| |
| nuxmv_trace_value | nuxmv_trace_get_step_state (nuxmv_env env, nuxmv_trace trace, int step_idx, int var_idx) |
| | Get the value of a state variable from the i-th step of a trace.
|
| |
| int | nuxmv_trace_get_step_input_num (nuxmv_env env, nuxmv_trace trace, int step_idx) |
| | Get the number of input variables in a trace.
|
| |
| nuxmv_trace_value | nuxmv_trace_get_step_input (nuxmv_env env, nuxmv_trace trace, int step_idx, int var_idx) |
| | Get the value of an input variable from the i-th step of a trace.
|
| |
| int | nuxmv_trace_get_step_define_num (nuxmv_env env, nuxmv_trace trace, int step_idx) |
| | Get the number of defines in a trace.
|
| |
| nuxmv_trace_value | nuxmv_trace_get_step_define (nuxmv_env env, nuxmv_trace trace, int step_idx, int def_idx) |
| | Get the value of a define from the i-th step of a trace.
|
| |
| int | nuxmv_trace_get_function_num (nuxmv_env env, nuxmv_trace trace) |
| | Get the number of uninterpreted functions in a trace.
|
| |
| nuxmv_trace_value | nuxmv_trace_get_function (nuxmv_env env, nuxmv_trace trace, int fun_idx) |
| | Get the value of a uninterpreted function from a trace.
|
| |
| int | nuxmv_trace_get_loopback (nuxmv_env env, nuxmv_trace trace) |
| | Get the the step the trace loops back, if any.
|
| |
