NuSMV/code/nusmv/core/compile/compile.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


   This file is part of the ``compile'' package of NuSMV version 2.
   Copyright (C) 1998-2001 by CMU and FBK-irst.

   NuSMV version 2 is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2 of the License, or (at your option) any later version.

   NuSMV version 2 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with this library; if not, write to the Free Software
   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

   For more information on NuSMV see <http://nusmv.fbk.eu>
   or email to <nusmv-users@fbk.eu>.
   Please report bugs to <nusmv-users@fbk.eu>.

   To contact the NuSMV development board, email to <nusmv@fbk.eu>.

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_COMPILE_COMPILE_H__
#define __NUSMV_CORE_COMPILE_COMPILE_H__

#include "nusmv/core/be/be.h" /* the generic boolean expressions interface */
#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/compile/compileUtil.h"
#include "nusmv/core/compile/FlatHierarchy.h"
#include "nusmv/core/compile/PredicateExtractor.h"
#include "nusmv/core/compile/PredicateNormaliser.h"
#include "nusmv/core/compile/symb_table/SymbLayer.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/enc/bdd/BddEnc.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/fsm/sexp/BoolSexpFsm.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/hrc/HrcNode.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/utils/NodeList.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/node/anonymizers/NodeAnonymizerBase.h"

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

#define ENV_FLAG_FLATTENER_INITIALIZED "flattener_initialized"

#define ENV_PROC_SELECTOR_VNAME        "proc_selector_vname"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct cmp_struct* cmp_struct_ptr;

typedef enum {
  State_Variables_Instantiation_Mode,
  Frozen_Variables_Instantiation_Mode,
  Input_Variables_Instantiation_Mode
} Instantiation_Variables_Mode_Type;

typedef enum {
  State_Functions_Instantiation_Mode,
  Frozen_Functions_Instantiation_Mode
} Instantiation_Functions_Mode_Type;

typedef enum {ST_Notype, ST_Ctl, ST_Ltl, ST_Invar, ST_Compute} Spec_Type;

typedef enum {SS_Nostatus, SS_Unchecked, SS_True, SS_False, SS_Wrong, SS_Number} Spec_Status;

typedef struct _Fsm_SexpRec    Fsm_SexpRec;
typedef struct _Fsm_SexpRec  * Fsm_SexpPtr;






/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define MODEL_LAYER_NAME  "model"

#define DETERM_LAYER_NAME "determ"

#define INLINING_LAYER_NAME "inlining"

#define PROCESS_SELECTOR_VAR_NAME "_process_selector_"

#define RUNNING_SYMBOL "running"

#define MODEL_LAYERS_CLASS "Model Class"

#define ARTIFACTS_LAYERS_CLASS "Artifacts Class"

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

void Compile_init(NuSMVEnv_ptr env);

void Compile_quit(NuSMVEnv_ptr env);

void CompileFlatten_init_flattener(NuSMVEnv_ptr env);

void CompileFlatten_quit_flattener(NuSMVEnv_ptr env);

void CompileFlatten_hash_module(const NuSMVEnv_ptr env,
                                       node_ptr parsed_module);

FlatHierarchy_ptr
Compile_FlattenHierarchy(const NuSMVEnv_ptr env,
                         const SymbTable_ptr symb_table,
                         SymbLayer_ptr layer,
                         node_ptr, node_ptr, node_ptr,
                         boolean create_process_variable,
                         boolean calc_vars_constr,
                         boolean expand_bounded_arrays,
                         HrcNode_ptr hrc_result);

void Compile_CheckAssigns(const SymbTable_ptr, node_ptr);

void Compile_check_case(const SymbTable_ptr, node_ptr expr);

void Compile_check_next(const SymbTable_ptr st,
                               node_ptr expr, node_ptr context,
                               boolean is_one_next_allowed);

void Compile_check_input_next(const SymbTable_ptr st,
                                     node_ptr expr, node_ptr context);

node_ptr
CompileFlatten_concat_contexts(const NuSMVEnv_ptr env,
                               node_ptr ctx1, node_ptr ctx2);

node_ptr
CompileFlatten_expand_range(const NuSMVEnv_ptr env,
                            int a, int b);

node_ptr
CompileFlatten_resolve_number(SymbTable_ptr symb_table,
                              node_ptr n, node_ptr context);

node_ptr
CompileFlatten_resolve_define_chains(const SymbTable_ptr symb_table,
                                     node_ptr expr, node_ptr context);

void insert_module_hash(const NuSMVEnv_ptr env, node_ptr x,
                               node_ptr y);

node_ptr lookup_module_hash(const NuSMVEnv_ptr env, node_ptr x);

void compileCheckForInputVars(SymbTable_ptr, FlatHierarchy_ptr hierarchy);

int cmp_struct_get_read_model(cmp_struct_ptr cmp);

void cmp_struct_set_read_model(cmp_struct_ptr cmp);

void cmp_struct_unset_read_model(cmp_struct_ptr cmp);

int cmp_struct_get_hrc_built(cmp_struct_ptr cmp);

void cmp_struct_set_hrc_built(cmp_struct_ptr cmp);

int cmp_struct_get_flatten_hrc(cmp_struct_ptr cmp);

void cmp_struct_set_flatten_hrc(cmp_struct_ptr cmp);

int cmp_struct_get_encode_variables(cmp_struct_ptr cmp);

void cmp_struct_set_encode_variables(cmp_struct_ptr cmp);

int cmp_struct_get_process_selector(cmp_struct_ptr cmp);

void cmp_struct_set_process_selector(cmp_struct_ptr cmp);

int cmp_struct_get_build_frames(cmp_struct_ptr cmp);

void cmp_struct_set_build_frames(cmp_struct_ptr cmp);

int cmp_struct_get_build_model(cmp_struct_ptr cmp);

void cmp_struct_set_build_model(cmp_struct_ptr cmp);

int cmp_struct_get_build_flat_model(cmp_struct_ptr cmp);

void cmp_struct_set_build_flat_model(cmp_struct_ptr cmp);

int cmp_struct_get_build_bool_model(cmp_struct_ptr cmp);

void cmp_struct_set_build_bool_model(cmp_struct_ptr cmp);

int cmp_struct_get_fairness(cmp_struct_ptr cmp);

void cmp_struct_set_fairness(cmp_struct_ptr cmp);

int cmp_struct_get_coi(cmp_struct_ptr cmp);

void cmp_struct_set_coi(cmp_struct_ptr cmp);

int cmp_struct_get_bmc_init(cmp_struct_ptr cmp);

void cmp_struct_set_bmc_init(cmp_struct_ptr cmp);

void cmp_struct_unset_bmc_init(cmp_struct_ptr cmp);

int cmp_struct_get_bmc_setup(cmp_struct_ptr cmp);

void cmp_struct_set_bmc_setup(cmp_struct_ptr cmp);

void cmp_struct_unset_bmc_setup(cmp_struct_ptr cmp);

Expr_ptr
Compile_compile_simpwff_from_string(NuSMVEnv_ptr env,
                                    const SymbTable_ptr st,
                                    const char* str_formula);

Expr_ptr
Compile_compile_nextwff_from_string(NuSMVEnv_ptr,
                                    const SymbTable_ptr st,
                                    const char* str_formula);

Expr_ptr
Compile_compile_spec_from_string(NuSMVEnv_ptr env,
                                 const SymbTable_ptr st,
                                 const char* str_formula,
                                 const Prop_Type prop_type);

node_ptr
Compile_FlattenSexp(const SymbTable_ptr symb_table, node_ptr, node_ptr);

node_ptr
Compile_FlattenSexpExpandDefine(const SymbTable_ptr symb_table,
                                node_ptr, node_ptr);

void
Compile_WriteFlattenModel(const NuSMVEnv_ptr env,
                          FILE* out,
                          const SymbTable_ptr st,
                          const array_t* layer_names,
                          const char* fsm_name,
                          FlatHierarchy_ptr hierarchy,
                          boolean force_flattening);

void
Compile_WriteRestrictedFlattenModel(const NuSMVEnv_ptr env,
                                    FILE* out,
                                    const SymbTable_ptr st,
                                    const array_t* layer_names,
                                    const char* fsm_name,
                                    FlatHierarchy_ptr hierarchy,
                                    boolean force_flattening);

void
Compile_WriteObfuscatedFlattenModel(const NuSMVEnv_ptr env,
                                    FILE* out,
                                    const SymbTable_ptr st,
                                    const array_t* layer_names,
                                    const char* fsm_name,
                                    FlatHierarchy_ptr hierarchy,
                                    boolean print_map,
                                    boolean force_flattening,
                                    NodeAnonymizerBase_ptr anonymizer);

void
Compile_WriteFlattenFsm(const NuSMVEnv_ptr env,
                        FILE* out,
                        const SymbTable_ptr symb_table,
                        const array_t* layer_names,
                        const char* fsm_name,
                        FlatHierarchy_ptr hierarchy,
                        boolean force_flattening);

void
Compile_WriteFlattenModel_udg(const NuSMVEnv_ptr env,
                              FILE* out,
                              const SymbTable_ptr st,
                              const array_t* layer_names,
                              const char* fsm_name,
                              FlatHierarchy_ptr hierarchy);

void
Compile_WriteFlattenSpecs(const NuSMVEnv_ptr env,
                          FILE* out,
                          const SymbTable_ptr st,
                          FlatHierarchy_ptr hierarchy,
                          boolean force_flattening);

void
Compile_WriteBoolModel(const NuSMVEnv_ptr env,
                       FILE* out,
                       BddEnc_ptr enc,
                       NodeList_ptr layers,
                       const char* fsm_name,
                       BoolSexpFsm_ptr bool_sexp_fsm,
                       boolean force_flattening);

void
Compile_WriteBoolFsm(const NuSMVEnv_ptr env,
                     FILE* out,
                     const SymbTable_ptr symb_table,
                     NodeList_ptr layers,
                     const char* fsm_name,
                     BoolSexpFsm_ptr bool_sexp_fsm,
                     boolean force_flattening);

void
Compile_WriteBoolSpecs(const NuSMVEnv_ptr env,
                       FILE* out,
                       BddEnc_ptr enc,
                       FlatHierarchy_ptr hierarchy);

boolean Compile_is_expr_booleanizable(const SymbTable_ptr st,
                                             node_ptr expr,
                                             boolean word_booleanizable,
                                             hash_ptr cache);

Expr_ptr Compile_expr2bexpr(BddEnc_ptr enc,
                                   SymbLayer_ptr det_layer,
                                   Expr_ptr expr);

Expr_ptr Compile_detexpr2bexpr(BddEnc_ptr enc, Expr_ptr expr);

Expr_ptr
Compile_detexpr2bexpr_list(BddEnc_ptr enc, Expr_ptr expr);

Set_t
Formula_GetDependencies(const SymbTable_ptr, node_ptr, node_ptr);

Set_t
Formula_GetDependenciesByType(const SymbTable_ptr, node_ptr, node_ptr,
                              SymbFilterType, boolean);


Set_t
Formulae_GetDependenciesByType(const SymbTable_ptr, node_ptr, node_ptr, node_ptr,
                               SymbFilterType, boolean);

Set_t
Formula_GetConstants(const SymbTable_ptr symb_table,
                     node_ptr formula, node_ptr context);

Set_t
Formulae_GetDependencies(const SymbTable_ptr, node_ptr, node_ptr,
                         node_ptr);

Set_t ComputeCOIFixpoint(const SymbTable_ptr symb_table,
                                const FlatHierarchy_ptr hierarchy,
                                const Expr_ptr expression,
                                const int steps,
                                boolean* reached_fixpoint);

Set_t ComputeCOI(const SymbTable_ptr,
                        const FlatHierarchy_ptr, Set_t);

node_ptr
Flatten_GetDefinition(const SymbTable_ptr symb_table, node_ptr atom,
                      const boolean expand_defines);

void Flatten_remove_symbol_info(const NuSMVEnv_ptr env, node_ptr name);

node_ptr
CompileFlatten_normalise_value_list(const NuSMVEnv_ptr env,
                                    node_ptr old_value_list);

SymbType_ptr
Compile_InstantiateType(SymbTable_ptr st, SymbLayer_ptr layer,
                        node_ptr name, node_ptr type,
                        node_ptr context,
                        boolean expand_bounded_arrays);

boolean
Compile_DeclareVariable(SymbTable_ptr symb_table, SymbLayer_ptr layer,
                        node_ptr name, SymbType_ptr type,
                        node_ptr context,
                        Instantiation_Variables_Mode_Type mode);

boolean
Compile_DeclareFunction(SymbTable_ptr symb_table, SymbLayer_ptr layer,
                        node_ptr name, SymbType_ptr type,
                        node_ptr context,
                        Instantiation_Functions_Mode_Type mode);

node_ptr Compile_make_dag_info(const NuSMVEnv_ptr env,
                                      node_ptr expr, hash_ptr hash);

node_ptr Compile_convert_to_dag(const NuSMVEnv_ptr env,
                                       SymbTable_ptr symb_table,
                                       node_ptr expr,
                                       hash_ptr hash,
                                       hash_ptr defines);

void Compile_write_dag_defines(const NuSMVEnv_ptr env,
                               FILE* out, hash_ptr defines);

void Compile_declare_dag_defines_in_layer(SymbLayer_ptr layer,
                                          hash_ptr defines);


void Compile_destroy_dag_info(const NuSMVEnv_ptr env,
                                     hash_ptr dag_info, hash_ptr defines);

void Compile_print_array_define(const NuSMVEnv_ptr env, FILE* out, const node_ptr n);

HrcNode_ptr Compile_hrc_from_parse_tree(const NuSMVEnv_ptr env,
                                               NodeMgr_ptr nomgr,
                                               node_ptr mod_name,
                                               node_ptr parse_tree);

void Compile_fill_hrc_from_mod_body(const NuSMVEnv_ptr env,
                                           NodeMgr_ptr nomgr,
                                           node_ptr mod_body,
                                           HrcNode_ptr hrc_result,
                                           hash_ptr mod_defs);

/* directly or indirectly called by commmands */

int
CompileFlatten_flatten_smv(NuSMVEnv_ptr env,
                           boolean calc_vars_constrains,
                           boolean expand_bounded_arrays);

void
Compile_show_vars(const NuSMVEnv_ptr env, const boolean total_only,
                 const boolean defs_only, const boolean vars_only,
                 const boolean statevars, const boolean frozenvars,
                 const boolean inputvars, const OStream_ptr ostream,
                 const boolean verbose);

int Compile_write_model_flat_bool(const NuSMVEnv_ptr env,
                                         const char* output_file,
                                         FILE* ofileid);

void Compile_print_predicates(const NuSMVEnv_ptr env);

int Compile_create_flat_model(NuSMVEnv_ptr env);

int Compile_create_boolean_model(NuSMVEnv_ptr env);

/* For write_coi_model */

Expr_ptr
Compile_remove_assignments(const NuSMVEnv_ptr env, Expr_ptr expr);

void Compile_write_coi_prop_fsm(const NuSMVEnv_ptr env,
                                       FlatHierarchy_ptr fh,
                                       Set_t cone, Set_t props,
                                       OStream_ptr output_file);

void Compile_write_coi_prop(const NuSMVEnv_ptr env,
                                   Set_t cone, Set_t props,
                                   OStream_ptr output_file);

void Compile_print_summary(const NuSMVEnv_ptr env,
                                  OStream_ptr file, SymbTable_ptr st,
                                  NodeList_ptr list, const char * str,
                                  boolean limit_output);

int Compile_get_bits(const SymbTable_ptr st, const NodeList_ptr lst);

void Compile_write_global_coi_fsm(NuSMVEnv_ptr env,
                                         FlatHierarchy_ptr hierarchy,
                                         Prop_Type prop_type,
                                         OStream_ptr output_file);

int Compile_write_properties_coi(NuSMVEnv_ptr env,
                                        FlatHierarchy_ptr hierarchy,
                                        Prop_Type prop_type,
                                        boolean only_dump_coi,
                                        const char* file_name);

void Compile_print_type(const NuSMVEnv_ptr env,
                               OStream_ptr file, node_ptr ntype,
                               int threshold);

node_ptr Compile_get_var_type(const NuSMVEnv_ptr env,
                                     SymbType_ptr type);

void Compile_WriteFlattenFsm_udg(const NuSMVEnv_ptr env,
                                        FILE* out,
                                        const SymbTable_ptr st,
                                        const array_t* layer_names,
                                        const char* fsm_name,
                                        FlatHierarchy_ptr hierarchy);

void Compile_WriteFlattenSpecs_udg(const NuSMVEnv_ptr env,
                                          FILE* out,
                                          const SymbTable_ptr st,
                                          FlatHierarchy_ptr hierarchy);

void Compile_WriteBoolModel_udg(const NuSMVEnv_ptr env,
                                       FILE* out,
                                       BddEnc_ptr enc,
                                       NodeList_ptr layers,
                                       const char* fsm_name,
                                       BoolSexpFsm_ptr bool_sexp_fsm);

void Compile_WriteBoolFsm_udg(const NuSMVEnv_ptr env,
                                     FILE* out, const SymbTable_ptr st,
                                     NodeList_ptr layers, const char* fsm_name,
                                     BoolSexpFsm_ptr bool_sexp_fsm);

void Compile_WriteBoolSpecs_udg(const NuSMVEnv_ptr env, FILE* out,
                                       BddEnc_ptr enc,
                                       FlatHierarchy_ptr hierarchy);

node_ptr Compile_make_dag_info_udg(const NuSMVEnv_ptr env,
                                          node_ptr expr, hash_ptr hash);

node_ptr Compile_convert_to_dag_udg(const NuSMVEnv_ptr env,
                                           SymbTable_ptr symb_table,
                                           node_ptr expr,
                                           hash_ptr dag_hash,
                                           hash_ptr defines);

void Compile_print_array_define_udg(const NuSMVEnv_ptr env,
                                           FILE* out,
                                           const node_ptr n);

/* Moved here because it is called from Hycomp */

void Compile_ProcessHierarchy(const NuSMVEnv_ptr env,
                                     SymbTable_ptr symb_table,
                                     SymbLayer_ptr layer,
                                     FlatHierarchy_ptr hierachy,
                                     node_ptr name,
                                     boolean create_process_variables,
                                     boolean calc_vars_constr);

int Compile_print_usage(NuSMVEnv_ptr env, OStream_ptr file);

int Compile_print_fsm_stats(NuSMVEnv_ptr env,
                                   BddFsm_ptr fsm,
                                   FILE* outstream,
                                   boolean printPreds);

/* not declared b/c these are supposed to be used by the Python
   wrapper */
int Compile_encode_variables(NuSMVEnv_ptr env,
                             char* input_order_file_name,
                             boolean bdd_enc_enum_only);
int Compile_build_model(NuSMVEnv_ptr env,
                        TransType partition_method);

int Compile_check_if_flattening_was_built(const NuSMVEnv_ptr env,
                                                 FILE* err);

int Compile_check_if_encoding_was_built(const NuSMVEnv_ptr env,
                                               FILE* err);

int Compile_check_if_model_layer_is_in_bddenc(const NuSMVEnv_ptr env,
                                                     FILE* err);

int Compile_check_if_flat_model_was_built(const NuSMVEnv_ptr env,
                                                 FILE* err,
                                                 boolean forced);

int Compile_check_if_bool_model_was_built(const NuSMVEnv_ptr env,
                                                 FILE* err,
                                                 boolean forced);

int Compile_check_if_model_was_built(const NuSMVEnv_ptr env,
                                            FILE* err,
                                            boolean forced);

#endif /* __NUSMV_CORE_COMPILE_COMPILE_H__ */

---