nuxmv.h

Go to the documentation of this file.

 
#pragma once
 
#ifdef __cplusplus
extern "C" {
#endif
 
#include <stdbool.h>
#include <stddef.h>
#include <stdio.h>
 
#define NUXMV_COUNT_OF(array) (sizeof(array) / sizeof(array[0]))
 
typedef enum nuxmv_status_code {
    NUXMV_FAILURE = 0,
    NUXMV_SUCCESS
} nuxmv_status_code;
 
 
typedef struct nuxmv_env {
    void *repr;
} nuxmv_env;
 
typedef struct nuxmv_opt {
    const char *key;
    const char *value;
} nuxmv_opt;
 
typedef struct nuxmv_expr_type {
    void *repr;
} nuxmv_expr_type;
 
typedef 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_          
} nuxmv_expr_type_tag;
 
typedef struct nuxmv_var_type {
    void *repr;
} nuxmv_var_type;
 
typedef 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_
} nuxmv_var_type_tag;
 
typedef struct nuxmv_symbol {
    void *repr;
} nuxmv_symbol;
 
typedef struct nuxmv_expr {
    void *repr;
} nuxmv_expr;
 
typedef 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_ 
} nuxmv_op_tag;
 
typedef enum nuxmv_expr_visit_order {
    NUXMV_EXPR_VISIT_PRE_ORDER,
    NUXMV_EXPR_VISIT_POST_ORDER
} nuxmv_expr_visit_order;
 
typedef enum nuxmv_expr_visit_status {
    NUXMV_EXPR_VISIT_PROCESS, 
    NUXMV_EXPR_VISIT_SKIP,    
    NUXMV_EXPR_VISIT_ABORT    
} nuxmv_expr_visit_status;
 
typedef nuxmv_expr_visit_status (*nuxmv_expr_visit_callback)(nuxmv_env env,
                                                             nuxmv_expr expr,
                                                             void *user_data);
 
typedef struct nuxmv_module {
    void *repr;
} nuxmv_module;
 
typedef struct nuxmv_var_decl {
    nuxmv_symbol identifier;
    nuxmv_var_type var_type;
} nuxmv_var_decl;
 
typedef struct nuxmv_trace_value {
    nuxmv_expr identifier;
    nuxmv_expr value;
} nuxmv_trace_value;
 
typedef struct nuxmv_fun_decl {
    nuxmv_symbol identifier;
    nuxmv_var_type fun_type;
} nuxmv_fun_decl;
 
typedef struct nuxmv_assign {
    nuxmv_expr lhs;
    nuxmv_expr rhs;
} nuxmv_assign;
 
typedef struct nuxmv_compassion {
    nuxmv_expr p;
    nuxmv_expr q;
} nuxmv_compassion;
 
typedef struct nuxmv_define_decl {
    nuxmv_expr identifier;
    nuxmv_expr body;
} nuxmv_define_decl;
 
typedef enum nuxmv_model_format {
    NUXMV_MODEL_FORMAT_SMV,
    NUXMV_MODEL_FORMAT_VMT,
    NUXMV_MODEL_FORMAT_AIG
} nuxmv_model_format;
 
typedef struct nuxmv_model {
    void *repr;
} nuxmv_model;
 
typedef enum nuxmv_property_type {
    NUXMV_PROPERTY_INVALID = -1,
    NUXMV_PROPERTY_INVARSPEC,
    NUXMV_PROPERTY_LTLSPEC
} nuxmv_property_type;
 
typedef struct nuxmv_property {
    void *repr;
} nuxmv_property;
 
typedef enum nuxmv_result_code {
    NUXMV_RESULT_INVALID = -1,
    NUXMV_RESULT_FALSE,
    NUXMV_RESULT_TRUE,
    NUXMV_RESULT_UNKNOWN
} nuxmv_result_code;
 
typedef struct nuxmv_result {
    void *repr;
} nuxmv_result;
 
typedef enum nuxmv_trace_format {
    NUXMV_TRACE_FORMAT_XML
} nuxmv_trace_format;
 
typedef struct nuxmv_trace {
    void *repr;
} nuxmv_trace;
 
typedef struct nuxmv_simulation {
    void *repr;
} nuxmv_simulation;
 
typedef struct nuxmv_simulation_constraint {
    nuxmv_expr simple_constraint;
    nuxmv_expr trans_constraint;
    nuxmv_trace trace;
    size_t trace_start;
    nuxmv_expr ltl_formula;
} nuxmv_simulation_constraint;
 
typedef bool (*nuxmv_serialized_chunk_callback)(char *chunk, size_t chunk_size,
                                                void *user_data);
 
 
 
#define NUXMV_MAKE_OPT(k, v) ((nuxmv_opt){.key = k, .value = v})
 
#define NUXMV_VALID_OPT(opt) ((opt).key != NULL && (opt).value != NULL)
 
 
 
#define NUXMV_VALID_ENV(env) ((env).repr != NULL)
 
nuxmv_env nuxmv_create_env(void);
 
nuxmv_status_code nuxmv_destroy_env(nuxmv_env env);
 
const char *nuxmv_env_get_last_error_message(nuxmv_env env);
 
nuxmv_status_code nuxmv_env_set_options(nuxmv_env env, const nuxmv_opt *opts,
                                        size_t opt_num);
 
int nuxmv_env_get_option_num(nuxmv_env env);
 
nuxmv_opt nuxmv_env_get_option(nuxmv_env env, int opt_idx);
 
 
 
#define NUXMV_VALID_EXPR_TYPE(expr_type) ((expr_type).repr != NULL)
 
nuxmv_expr_type nuxmv_make_boolean_type(nuxmv_env env);
 
nuxmv_expr_type nuxmv_make_integer_type(nuxmv_env env);
 
nuxmv_expr_type nuxmv_make_real_type(nuxmv_env env);
 
nuxmv_expr_type nuxmv_make_enum_type(nuxmv_env env);
 
nuxmv_expr_type nuxmv_make_set_type(nuxmv_env env, nuxmv_expr_type elem);
 
nuxmv_expr_type nuxmv_make_signed_word_type(nuxmv_env env, size_t width);
 
nuxmv_expr_type nuxmv_make_unsigned_word_type(nuxmv_env env, size_t width);
 
nuxmv_expr_type nuxmv_make_array_type(nuxmv_env env, nuxmv_expr_type idx,
                                      nuxmv_expr_type elem);
 
nuxmv_expr_type nuxmv_make_function_type(nuxmv_env env,
                                         const nuxmv_expr_type *args,
                                         size_t arg_num,
                                         nuxmv_expr_type result);
 
nuxmv_expr_type_tag nuxmv_expr_type_get_tag(nuxmv_env env,
                                            nuxmv_expr_type type);
 
size_t nuxmv_expr_type_get_id(nuxmv_env env, nuxmv_expr_type type);
 
int nuxmv_word_type_get_width(nuxmv_env env, nuxmv_expr_type type);
 
nuxmv_expr_type nuxmv_array_type_get_index(nuxmv_env env, nuxmv_expr_type type);
 
nuxmv_expr_type nuxmv_array_type_get_element(nuxmv_env env,
                                             nuxmv_expr_type type);
 
int nuxmv_function_type_get_argument_num(nuxmv_env env, nuxmv_expr_type type);
 
nuxmv_expr_type nuxmv_function_type_get_argument(nuxmv_env env,
                                                 nuxmv_expr_type type,
                                                 int arg_idx);
 
nuxmv_expr_type nuxmv_function_type_get_result(nuxmv_env env,
                                               nuxmv_expr_type type);
 
nuxmv_expr_type nuxmv_set_type_get_element(nuxmv_env env, nuxmv_expr_type type);
 
 
 
#define NUXMV_VALID_VAR_TYPE(var_type) ((var_type).repr != NULL)
 
nuxmv_var_type nuxmv_make_simple_var_type(nuxmv_env env, nuxmv_expr_type type);
 
nuxmv_var_type nuxmv_make_var_type_with_domain(nuxmv_env env,
                                               const nuxmv_expr *domain,
                                               size_t domain_num);
 
nuxmv_var_type nuxmv_make_var_type_with_integer_range(nuxmv_env env, int min,
                                                      int max);
 
nuxmv_var_type nuxmv_make_var_type_array(nuxmv_env env, nuxmv_var_type idx,
                                         nuxmv_var_type elem);
 
nuxmv_expr_type nuxmv_var_type_get_expr_type(nuxmv_env env,
                                             nuxmv_var_type var_type);
 
nuxmv_var_type_tag nuxmv_var_type_get_tag(nuxmv_env env,
                                          nuxmv_var_type var_type);
 
size_t nuxmv_var_type_get_id(nuxmv_env env, nuxmv_var_type var_type);
 
nuxmv_var_type nuxmv_var_type_array_get_index(nuxmv_env env,
                                              nuxmv_var_type var_type);
 
nuxmv_var_type nuxmv_var_type_array_get_element(nuxmv_env env,
                                                nuxmv_var_type var_type);
 
int nuxmv_var_type_integer_range_get_min(nuxmv_env env,
                                         nuxmv_var_type var_type);
 
int nuxmv_var_type_integer_range_get_max(nuxmv_env env,
                                         nuxmv_var_type var_type);
 
int nuxmv_var_type_get_domain_num(nuxmv_env env, nuxmv_var_type var_type);
 
nuxmv_expr nuxmv_var_type_get_domain_element(nuxmv_env env,
                                             nuxmv_var_type var_type,
                                             int elem_idx);
 
 
 
#define NUXMV_VALID_SYMBOL(symbol) ((symbol).repr != NULL)
 
nuxmv_symbol nuxmv_make_symbol(nuxmv_env env, const char *name);
 
nuxmv_symbol nuxmv_make_scoped_symbol(nuxmv_env env, const char *name,
                                      nuxmv_symbol scope);
 
size_t nuxmv_symbol_get_id(nuxmv_env env, nuxmv_symbol sym);
 
const char *nuxmv_symbol_get_name(nuxmv_env env, nuxmv_symbol symbol);
 
int nuxmv_symbol_is_scoped(nuxmv_env env, nuxmv_symbol symbol);
 
nuxmv_symbol nuxmv_symbol_get_scope(nuxmv_env env, nuxmv_symbol symbol);
 
 
 
#define NUXMV_MAKE_INVALID_EXPR() ((nuxmv_expr){.repr = NULL})
 
#define NUXMV_VALID_EXPR(expr) ((expr).repr != NULL)
 
nuxmv_expr nuxmv_make_identifier(nuxmv_env env, nuxmv_symbol symbol,
                                 nuxmv_expr_type type);
 
nuxmv_expr nuxmv_make_value(nuxmv_env env, nuxmv_symbol val,
                            nuxmv_expr_type type);
 
nuxmv_expr nuxmv_make_op(nuxmv_env env, nuxmv_op_tag op, const nuxmv_expr *args,
                         size_t arg_num);
 
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);
 
nuxmv_expr nuxmv_make_un_op(nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg);
 
nuxmv_expr nuxmv_make_bin_op(nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg1,
                             nuxmv_expr arg2);
 
nuxmv_expr nuxmv_make_expr_from_string(nuxmv_env env, const char *data,
                                       nuxmv_module scope);
 
nuxmv_expr_type nuxmv_expr_get_type(nuxmv_env env, nuxmv_expr expr);
 
nuxmv_symbol nuxmv_expr_get_symbol(nuxmv_env env, nuxmv_expr identifier);
 
size_t nuxmv_expr_get_id(nuxmv_env env, nuxmv_expr expr);
 
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);
 
int nuxmv_expr_contains_temporal_operators(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_is_identifier(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_is_value(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_is_op(nuxmv_env env, nuxmv_expr expr);
 
nuxmv_op_tag nuxmv_expr_get_op_tag(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_get_argument_num(nuxmv_env env, nuxmv_expr expr);
 
nuxmv_expr nuxmv_expr_get_argument(nuxmv_env env, nuxmv_expr expr, int arg_idx);
 
int nuxmv_expr_is_parametric(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_get_parameter_num(nuxmv_env env, nuxmv_expr expr);
 
int nuxmv_expr_get_parameter(nuxmv_env env, nuxmv_expr expr, int param_idx);
 
int nuxmv_visit_expr(nuxmv_env env, nuxmv_expr expr,
                     nuxmv_expr_visit_callback callback,
                     nuxmv_expr_visit_order order, void *user_data);
 
nuxmv_expr nuxmv_simplify_expr(nuxmv_env env, nuxmv_expr expr);
 
 
 
#define NUXMV_MAKE_INVALID_MODULE() ((nuxmv_module){.repr = NULL})
 
#define NUXMV_VALID_MODULE(module) ((module).repr != NULL)
 
nuxmv_module nuxmv_create_module(nuxmv_env env, const char *name);
 
nuxmv_module nuxmv_create_module_from_property(nuxmv_env env, const char *name,
                                               nuxmv_property property,
                                               const nuxmv_opt *opts,
                                               size_t opt_num);
 
nuxmv_status_code nuxmv_destroy_module(nuxmv_env env, nuxmv_module module);
 
nuxmv_module nuxmv_copy_module(nuxmv_env env, nuxmv_module module,
                               const char *name);
 
 
 
#define NUXMV_MAKE_VAR_DECL(identifier_, var_type_)                            \
    ((nuxmv_var_decl){.identifier = identifier_, .var_type = var_type_})
 
#define NUXMV_VALID_VAR_DECL(var_decl_)                                        \
    (NUXMV_VALID_SYMBOL((var_decl_).identifier) &&                             \
     NUXMV_VALID_VAR_TYPE((var_decl_).var_type))
 
#define NUXMV_MAKE_FUN_DECL(identifier_, fun_type_)                            \
    ((nuxmv_fun_decl){.identifier = identifier_, .fun_type = fun_type_})
 
#define NUXMV_VALID_FUN_DECL(fun_decl_)                                        \
    (NUXMV_VALID_SYMBOL((fun_decl_).identifier) &&                             \
     NUXMV_VALID_VAR_TYPE((fun_decl_).fun_type))
 
#define NUXMV_MAKE_ASSIGN(lhs_, rhs_) ((nuxmv_assign){.lhs = lhs_, .rhs = rhs_})
 
#define NUXMV_VALID_ASSIGN(assign_)                                            \
    (NUXMV_VALID_EXPR((assign_).lhs) && NUXMV_VALID_EXPR((assign_).rhs))
 
#define NUXMV_MAKE_COMPASSION(p_, q_) ((nuxmv_compassion){.p = p_, .q = q_})
 
#define NUXMV_VALID_COMPASSION(comp_)                                          \
    (NUXMV_VALID_EXPR((comp_).p) && NUXMV_VALID_EXPR((comp_).q))
 
#define NUXMV_MAKE_DEFINE_DECL(identifier_, body_)                             \
    ((nuxmv_define_decl){.identifier = identifier_, .body = body_})
 
#define NUXMV_VALID_DEFINE_DECL(define_decl_)                                  \
    (NUXMV_VALID_EXPR((define_decl_).identifier) &&                            \
     NUXMV_VALID_EXPR((define_decl_).body))
 
nuxmv_status_code nuxmv_module_add_params(nuxmv_env env, nuxmv_module module,
                                          const nuxmv_expr *params,
                                          size_t param_num);
 
nuxmv_status_code nuxmv_module_add_state_var(nuxmv_env env, nuxmv_module module,
                                             nuxmv_var_decl var);
 
nuxmv_status_code nuxmv_module_add_input_var(nuxmv_env env, nuxmv_module module,
                                             nuxmv_var_decl var);
 
nuxmv_status_code nuxmv_module_add_frozen_var(nuxmv_env env,
                                              nuxmv_module module,
                                              nuxmv_var_decl var);
 
nuxmv_status_code nuxmv_module_add_function(nuxmv_env env, nuxmv_module module,
                                            nuxmv_fun_decl fun_decl);
 
nuxmv_status_code nuxmv_module_add_init(nuxmv_env env, nuxmv_module module,
                                        nuxmv_expr init);
 
nuxmv_status_code nuxmv_module_add_trans(nuxmv_env env, nuxmv_module module,
                                         nuxmv_expr trans);
 
nuxmv_status_code nuxmv_module_add_invar(nuxmv_env env, nuxmv_module module,
                                         nuxmv_expr invar);
 
nuxmv_status_code nuxmv_module_add_justice(nuxmv_env env, nuxmv_module module,
                                           nuxmv_expr justice);
 
nuxmv_status_code nuxmv_module_add_compassion(nuxmv_env env,
                                              nuxmv_module module,
                                              nuxmv_compassion comp);
 
nuxmv_status_code nuxmv_module_add_define(nuxmv_env env, nuxmv_module module,
                                          nuxmv_define_decl decl);
 
nuxmv_status_code nuxmv_module_add_init_assign(nuxmv_env env,
                                               nuxmv_module module,
                                               nuxmv_assign assign);
 
nuxmv_status_code nuxmv_module_add_next_assign(nuxmv_env env,
                                               nuxmv_module module,
                                               nuxmv_assign assign);
 
nuxmv_status_code nuxmv_module_add_invar_assign(nuxmv_env env,
                                                nuxmv_module module,
                                                nuxmv_assign assign);
 
nuxmv_status_code nuxmv_module_add_property(nuxmv_env env, nuxmv_module module,
                                            nuxmv_property property);
 
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);
 
 
 
const char *nuxmv_module_get_name(nuxmv_env env, nuxmv_module module);
 
int nuxmv_module_get_param_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_expr nuxmv_module_get_param(nuxmv_env env, nuxmv_module module,
                                  int param_idx);
 
int nuxmv_module_get_state_var_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_var_decl nuxmv_module_get_state_var(nuxmv_env env, nuxmv_module module,
                                          int var_idx);
 
int nuxmv_module_get_input_var_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_var_decl nuxmv_module_get_input_var(nuxmv_env env, nuxmv_module module,
                                          int var_idx);
 
int nuxmv_module_get_frozen_var_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_var_decl nuxmv_module_get_frozen_var(nuxmv_env env, nuxmv_module module,
                                           int var_idx);
 
int nuxmv_module_get_function_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_fun_decl nuxmv_module_get_function(nuxmv_env env, nuxmv_module module,
                                         int fun_idx);
 
int nuxmv_module_get_init_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_expr nuxmv_module_get_init(nuxmv_env env, nuxmv_module module,
                                 int init_idx);
 
int nuxmv_module_get_trans_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_expr nuxmv_module_get_trans(nuxmv_env env, nuxmv_module module,
                                  int trans_idx);
 
int nuxmv_module_get_invar_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_expr nuxmv_module_get_invar(nuxmv_env env, nuxmv_module module,
                                  int invar_idx);
 
int nuxmv_module_get_justice_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_expr nuxmv_module_get_justice(nuxmv_env env, nuxmv_module module,
                                    int just_idx);
 
int nuxmv_module_get_compassion_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_compassion nuxmv_module_get_compassion(nuxmv_env env, nuxmv_module module,
                                             int comp_idx);
 
int nuxmv_module_get_define_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_define_decl nuxmv_module_get_define(nuxmv_env env, nuxmv_module module,
                                          int def_idx);
 
int nuxmv_module_get_init_assign_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_assign nuxmv_module_get_init_assign(nuxmv_env env, nuxmv_module module,
                                          int assign_idx);
 
int nuxmv_module_get_next_assign_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_assign nuxmv_module_get_next_assign(nuxmv_env env, nuxmv_module module,
                                          int assign_idx);
 
int nuxmv_module_get_invar_assign_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_assign nuxmv_module_get_invar_assign(nuxmv_env env, nuxmv_module module,
                                           int assign_idx);
 
int nuxmv_module_get_property_num(nuxmv_env env, nuxmv_module module);
 
nuxmv_property nuxmv_module_get_property(nuxmv_env env, nuxmv_module module,
                                         int prop_idx);
 
int nuxmv_module_get_submodule_num(nuxmv_env env, nuxmv_module module);
 
const char *nuxmv_module_get_submodule_name(nuxmv_env env, nuxmv_module module,
                                            int sub_idx);
 
nuxmv_module nuxmv_module_get_submodule(nuxmv_env env, nuxmv_module module,
                                        int sub_idx);
 
int nuxmv_module_get_submodule_param_num(nuxmv_env env, nuxmv_module module,
                                         int sub_idx);
 
nuxmv_expr nuxmv_module_get_submodule_param(nuxmv_env env, nuxmv_module module,
                                            int sub_idx, int param_idx);
 
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);
 
 
 
#define NUXMV_VALID_MODEL(model) ((model).repr != NULL)
 
nuxmv_model nuxmv_create_model(nuxmv_env env, nuxmv_module module,
                               const nuxmv_expr *params, size_t param_num);
 
nuxmv_model nuxmv_create_model_from_string(nuxmv_env env,
                                           nuxmv_model_format fmt,
                                           const char *data);
 
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);
 
nuxmv_result nuxmv_model_check_property(nuxmv_env env, nuxmv_model model,
                                        nuxmv_property property,
                                        const nuxmv_opt *opts, size_t opt_num);
 
nuxmv_result nuxmv_model_check_deadlock(nuxmv_env env, nuxmv_model model,
                                        const nuxmv_opt *opts, size_t opt_num);
 
nuxmv_result nuxmv_model_check_receptiveness(nuxmv_env env, nuxmv_model model,
                                             const nuxmv_opt *opts,
                                             size_t opt_num);
 
nuxmv_status_code nuxmv_destroy_model(nuxmv_env env, nuxmv_model model);
 
 
nuxmv_module nuxmv_model_get_root_module(nuxmv_env env, nuxmv_model model);
 
 
int nuxmv_model_get_state_var_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_var_decl nuxmv_model_get_state_var(nuxmv_env env, nuxmv_model model,
                                         int var_idx);
 
int nuxmv_model_get_input_var_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_var_decl nuxmv_model_get_input_var(nuxmv_env env, nuxmv_model model,
                                         int var_idx);
 
int nuxmv_model_get_frozen_var_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_var_decl nuxmv_model_get_frozen_var(nuxmv_env env, nuxmv_model model,
                                          int var_idx);
 
int nuxmv_model_get_function_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_fun_decl nuxmv_model_get_function(nuxmv_env env, nuxmv_model model,
                                        int fun_idx);
 
int nuxmv_model_get_init_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_expr nuxmv_model_get_init(nuxmv_env env, nuxmv_model model, int init_idx);
 
int nuxmv_model_get_trans_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_expr nuxmv_model_get_trans(nuxmv_env env, nuxmv_model model,
                                 int trans_idx);
 
int nuxmv_model_get_invar_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_expr nuxmv_model_get_invar(nuxmv_env env, nuxmv_model model,
                                 int invar_idx);
 
int nuxmv_model_get_justice_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_expr nuxmv_model_get_justice(nuxmv_env env, nuxmv_model model,
                                   int just_idx);
 
int nuxmv_model_get_compassion_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_compassion nuxmv_model_get_compassion(nuxmv_env env, nuxmv_model model,
                                            int comp_idx);
 
int nuxmv_model_get_define_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_define_decl nuxmv_model_get_define(nuxmv_env env, nuxmv_model model,
                                         int def_idx);
 
 
 
int nuxmv_model_get_init_assign_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_assign nuxmv_model_get_init_assign(nuxmv_env env, nuxmv_model model,
                                         int assign_idx);
 
int nuxmv_model_get_next_assign_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_assign nuxmv_model_get_next_assign(nuxmv_env env, nuxmv_model model,
                                         int assign_idx);
 
int nuxmv_model_get_invar_assign_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_assign nuxmv_model_get_invar_assign(nuxmv_env env, nuxmv_model model,
                                          int assign_idx);
 
 
 
int nuxmv_model_get_property_num(nuxmv_env env, nuxmv_model model);
 
nuxmv_property nuxmv_model_get_property(nuxmv_env env, nuxmv_model model,
                                        int prop_idx);
 
nuxmv_property nuxmv_model_get_property_by_name(nuxmv_env env,
                                                nuxmv_model model,
                                                const char *name);
 
 
 
nuxmv_status_code nuxmv_model_add_property(nuxmv_env env, nuxmv_model model,
                                           nuxmv_property property);
 
 
 
#define NUXMV_VALID_PROPERTY(property) ((property).repr != NULL)
 
nuxmv_property nuxmv_make_property(nuxmv_env env, nuxmv_property_type type,
                                   nuxmv_expr expr, const char *name);
 
nuxmv_property nuxmv_make_property_from_string(nuxmv_env env,
                                               nuxmv_property_type type,
                                               const char *data,
                                               nuxmv_module scope,
                                               const char *name);
 
nuxmv_result nuxmv_property_check_satisfiability(nuxmv_env env,
                                                 nuxmv_property property,
                                                 const nuxmv_opt *opts,
                                                 size_t opt_num);
nuxmv_expr nuxmv_property_get_expr(nuxmv_env env, nuxmv_property property);
 
const char *nuxmv_property_get_name(nuxmv_env env, nuxmv_property property);
 
nuxmv_property_type nuxmv_property_get_type(nuxmv_env env,
                                            nuxmv_property property);
 
 
 
#define NUXMV_VALID_SIMULATION(simulation) ((simulation).repr != NULL)
 
#define NUXMV_MAKE_SIMULATION_CONSTRAINT(                                      \
    simple_constraint_, trans_constraint_, trace_, trace_start_, ltl_formula_) \
    ((nuxmv_simulation_constraint){.simple_constraint = (simple_constraint_),  \
                                   .trans_constraint = (trans_constraint_),    \
                                   .trace = (trace_),                          \
                                   .trace_start = (trace_start_),              \
                                   .ltl_formula = (ltl_formula_)})
 
nuxmv_simulation nuxmv_create_simulation(nuxmv_env env, nuxmv_model model,
                                         nuxmv_simulation_constraint constraint,
                                         const nuxmv_opt *opts, size_t opt_num);
 
nuxmv_status_code nuxmv_destroy_simulation(nuxmv_env env,
                                           nuxmv_simulation simulation);
 
nuxmv_status_code
nuxmv_extend_simulation(nuxmv_env env, nuxmv_simulation simulation, size_t k,
                        nuxmv_simulation_constraint constraint);
 
nuxmv_result nuxmv_simulation_get_result(nuxmv_env env,
                                         nuxmv_simulation simulation);
 
 
 
#define NUXMV_VALID_RESULT(result) ((result).repr != NULL)
 
nuxmv_result_code nuxmv_result_get_code(nuxmv_env env, nuxmv_result result);
 
nuxmv_trace nuxmv_result_get_trace(nuxmv_env env, nuxmv_result result);
 
 
 
#define NUXMV_VALID_TRACE(trace) ((trace).repr != NULL)
 
nuxmv_trace nuxmv_make_trace_from_string(nuxmv_env env, nuxmv_trace_format fmt,
                                         const char *data, nuxmv_model model);
 
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);
 
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);
 
 
 
#define NUXMV_VALID_TRACE_VALUE(symb_val)                                      \
    (NUXMV_VALID_EXPR((symb_val).identifier) &&                                \
     NUXMV_VALID_EXPR((symb_val).value))
 
int nuxmv_trace_get_step_num(nuxmv_env env, nuxmv_trace trace);
 
int nuxmv_trace_get_step_state_num(nuxmv_env env, nuxmv_trace trace,
                                   int step_idx);
 
nuxmv_trace_value nuxmv_trace_get_step_state(nuxmv_env env, nuxmv_trace trace,
                                             int step_idx, int var_idx);
 
int nuxmv_trace_get_step_input_num(nuxmv_env env, nuxmv_trace trace,
                                   int step_idx);
 
nuxmv_trace_value nuxmv_trace_get_step_input(nuxmv_env env, nuxmv_trace trace,
                                             int step_idx, int var_idx);
 
int nuxmv_trace_get_step_define_num(nuxmv_env env, nuxmv_trace trace,
                                    int step_idx);
 
nuxmv_trace_value nuxmv_trace_get_step_define(nuxmv_env env, nuxmv_trace trace,
                                              int step_idx, int def_idx);
 
int nuxmv_trace_get_function_num(nuxmv_env env, nuxmv_trace trace);
 
nuxmv_trace_value nuxmv_trace_get_function(nuxmv_env env, nuxmv_trace trace,
                                           int fun_idx);
 
int nuxmv_trace_get_loopback(nuxmv_env env, nuxmv_trace trace);
 
#ifdef __cplusplus
}
#endif