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

Go to the documentation of this file.

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


  This file is part of the ``required'' package.
  %COPYRIGHT%
  

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

#ifndef __NUSMV_CORE_BMC_BMC_TEST_H__
#define __NUSMV_CORE_BMC_BMC_TEST_H__

#include "nusmv/core/cinit/NuSMVEnv.h"

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


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
/* user can generate a random wff based on a specified operator: */
typedef enum GenWffOperator_TAG {
  GWO_None, GWO_Globally, GWO_Future, GWO_Until, GWO_Releases,
  GWO_Historically, GWO_Once, GWO_Since, GWO_Triggered
} GenWffOperator;


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


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


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


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

int Bmc_Test_test_tableau(NuSMVEnv_ptr env,
                                 node_ptr wff,
                                 GenWffOperator wff_operator,
                                 int max_depth,
                                 int max_conns,
                                 boolean usePastOperators,
                                 boolean crossComparison,
                                 int k,
                                 int l);

#endif /* __NUSMV_CORE_BMC_BMC_TEST_H__ */

---