NuSMV/code/nusmv/core/bmc/bmcBmc.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_BMC_H__
#define __NUSMV_CORE_BMC_BMC_BMC_H__

#include "nusmv/core/bmc/bmcDump.h"
#include "nusmv/core/bmc/bmc.h"

#include "nusmv/core/fsm/be/BeFsm.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/trace/Trace.h"

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"


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

typedef enum {BMC_TRUE, BMC_FALSE, BMC_UNKNOWN, BMC_ERROR} Bmc_result;

typedef enum {
  BMC_INVAR_BACKWARD_CLOSURE,
  BMC_INVAR_FORWARD_CLOSURE
} bmc_invar_closure_strategy;


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


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


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

int Bmc_GenSolveLtl(NuSMVEnv_ptr env, Prop_ptr ltlprop,
                           const int k, const int relative_loop,
                           const boolean must_inc_length,
                           const boolean must_solve,
                           const Bmc_DumpType dump_type,
                           const char* dump_fname_template);

int Bmc_GenSolveInvar(NuSMVEnv_ptr env,
                             Prop_ptr invarprop,
                             const boolean must_solve,
                             const Bmc_DumpType dump_type,
                             const char* dump_fname_template);

Bmc_result Bmc_induction_algorithm(const NuSMVEnv_ptr env,
                                          BeFsm_ptr be_fsm,
                                          node_ptr binvarspec,
                                          Trace_ptr* trace_index,
                                          NodeList_ptr symbols);

Bmc_result
Bmc_een_sorensson_algorithm(const NuSMVEnv_ptr env,
                            BeFsm_ptr be_fsm,
                            BoolSexpFsm_ptr bool_fsm,
                            node_ptr binvarspec,
                            int max_k,
                            const Bmc_DumpType dump_type,
                            const char* dump_fname_template,
                            Prop_ptr pp,
                            Prop_ptr oldprop,
                            boolean print_steps,
                            boolean use_extra_step,
                            Trace_ptr* trace);

Bmc_result
Bmc_een_sorensson_algorithm_without_dump(const NuSMVEnv_ptr env,
                                         BeFsm_ptr be_fsm,
                                         BoolSexpFsm_ptr bool_fsm,
                                         node_ptr binvarspec,
                                         int max_k,
                                         boolean use_extra_step,
                                         Trace_ptr* trace);

int
Bmc_GenSolveInvar_EenSorensson(NuSMVEnv_ptr env,
                               Prop_ptr invarprop,
                               const int max_k,
                               const Bmc_DumpType dump_type,
                               const char* dump_fname_template,
                               boolean use_extra_step);

/* incremental algorithms */

int Bmc_GenSolveLtlInc(NuSMVEnv_ptr env, Prop_ptr ltlprop,
                              const int k, const int relative_loop,
                              const boolean must_inc_length);

int Bmc_GenSolveInvarZigzag(NuSMVEnv_ptr env,
                                   Prop_ptr invarprop, const int max_k);

int Bmc_GenSolveInvarDual(NuSMVEnv_ptr env,
                                 Prop_ptr invarprop, const int max_k,
                                 bmc_invar_closure_strategy strategy);

int Bmc_GenSolveInvarFalsification(NuSMVEnv_ptr env, Prop_ptr invarprop,
                                   const int max_k, int step_k);

#endif /* __NUSMV_CORE_BMC_BMC_BMC_H__ */

---