NuSMV/code/nusmv/core/bmc/bmcInt.h

Go to the documentation of this file.

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


  This file is part of the ``bmc'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by FBK-irst and University of Trento.

  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_BMC_BMC_INT_H__
#define __NUSMV_CORE_BMC_BMC_INT_H__


#include <time.h>
#include <limits.h>
#include <stdio.h>


#include "nusmv/core/enc/be/BeEnc.h"

#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/compile/compile.h"

#include "nusmv/core/be/be.h"

#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"

#include "nusmv/core/dd/dd.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/utils.h"

/* Uncomment the following line to print out benchmarking info */
/* #define BENCHMARKING */


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

#define BMC_DUMP_FILENAME_MAXLEN 4096

#define BMC_NO_PROPERTY_INDEX -1

#define BMC_BEXP_OUTPUT_SMV 0

#define BMC_BEXP_OUTPUT_LB 1

/* BMC Options  default values */

#define DEFAULT_DIMACS_FILENAME        "@f_k@k_l@l_n@n"

#define DEFAULT_INVAR_DIMACS_FILENAME  "@f_invar_n@n"

#define DEFAULT_BMC_PB_LENGTH     10

#define DEFAULT_BMC_PB_LOOP         Bmc_Utils_GetAllLoopbacksString()

#define DEFAULT_BMC_INVAR_ALG       "classic"

#define DEFAULT_BMC_INC_INVAR_ALG   "dual"

#define DEFAULT_BMC_OPTIMIZED_TABLEAU 1

#define DEFAULT_BMC_FORCE_PLTL_TABLEAU 0

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


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


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#define ST_BMC_CONV_BEXPR2BE_HASH "bcbh"

#define ST_BMC_TABLEAU_LTL_HASH "btlh"

extern cmp_struct_ptr cmps;
extern FsmBuilder_ptr global_fsm_builder;
extern TraceMgr_ptr global_trace_manager;



/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


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

node_ptr
bmc_tableau_memoization_get_key(NodeMgr_ptr nodemgr,
                                node_ptr wff, int time, int k, int l);

void bmc_tableau_memoization_insert(hash_ptr, node_ptr key, be_ptr be);

be_ptr bmc_tableau_memoization_lookup(hash_ptr, node_ptr key);

hash_ptr Bmc_Tableau_get_handled_hash(SymbTable_ptr symb_table,
                                             char* hash_str);

int
Bmc_TestTableau(NuSMVEnv_ptr env, int argc, char ** argv);

void Bmc_TestReset(void);

boolean
isPureFuture(const node_ptr pltl_wff);

be_ptr
Bmc_GetTestTableau(const BeEnc_ptr be_enc,
                   const node_ptr ltl_wff,
                   const int k, const int l);

be_ptr
BmcInt_Tableau_GetAtTime(const BeEnc_ptr be_enc,
                         const node_ptr ltl_wff,
                         const int time, const int k, const int l);

/* ================================================== */
/* Tableaux for an LTL formula:                       */

be_ptr
bmc_tableauGetNextAtTime(const BeEnc_ptr be_enc,
                         const node_ptr ltl_wff,
                         const int time, const int k, const int l);

be_ptr
bmc_tableauGetEventuallyAtTime(const BeEnc_ptr be_enc,
                               const node_ptr ltl_wff,
                               const int intime, const int k,
                               const int l);

be_ptr
bmc_tableauGetGloballyAtTime(const BeEnc_ptr be_enc,
                             const node_ptr ltl_wff,
                             const int intime, const int k,
                             const int l);

be_ptr
bmc_tableauGetUntilAtTime(const BeEnc_ptr be_enc,
                          const node_ptr p, const node_ptr q,
                          const int time, const int k, const int l);

be_ptr
bmc_tableauGetReleasesAtTime(const BeEnc_ptr be_enc,
                             const node_ptr p, const node_ptr q,
                             const int time, const int k, const int l);
/* ================================================== */


/* ================================================== */
/* Tableaux for a PLTL formula:                       */

be_ptr
Bmc_TableauPLTL_GetTableau(const BeEnc_ptr be_enc,
                           const node_ptr pltl_wff,
                           const int k, const int l);

be_ptr
Bmc_TableauPLTL_GetAllTimeTableau(const BeEnc_ptr be_enc,
                                  const node_ptr pltl_wff,
                                  const int k);
/* ================================================== */


/* ================================================== */
/* Utils module:                                      */

lsList
Bmc_Utils_get_vars_list_for_uniqueness(BeEnc_ptr be_enc,
                                       Prop_ptr invarprop);

lsList
Bmc_Utils_get_vars_list_for_uniqueness_fsm(BeEnc_ptr be_enc,
                                           SexpFsm_ptr bool_fsm);

/* ================================================== */
/* Simulation                                         */
void bmc_simulate_set_curr_sim_trace(const NuSMVEnv_ptr env, Trace_ptr trace, int idx);
Trace_ptr bmc_simulate_get_curr_sim_trace(const NuSMVEnv_ptr env);
int bmc_simulate_get_curr_sim_trace_index(const NuSMVEnv_ptr env);
/* ================================================== */

Trace_ptr
Bmc_create_trace_from_cnf_model(const BeEnc_ptr be_enc,
                                const NodeList_ptr symbols,
                                const char* desc,
                                const TraceType type,
                                const Slist_ptr cnf_model,
                                int k);

Trace_ptr
Bmc_fill_trace_from_cnf_model(const BeEnc_ptr be_enc,
                              const Slist_ptr cnf_model,
                              int k, Trace_ptr trace);

/* internal bmc/trace utils */

void
bmc_trace_utils_complete_trace(Trace_ptr trace,
                               const BoolEnc_ptr bool_enc);

void
bmc_trace_utils_append_input_state(Trace_ptr trace, BeEnc_ptr be_enc,
                                   const Slist_ptr cnf_model);

#endif /* __NUSMV_CORE_BMC_BMC_INT_H__ */

---