/**CHeaderFile*****************************************************************

  FileName    [abs.h]

  PackageName [abs]

  Synopsis    [Incremental CTL model checker.]

  Description [This package provides the command "incremental_ctl_verification",
  an algorithm to verify CTL formulas starting from an initial abstraction and
  applying refinements to increment the level of accuracy in the verification.
  The theory behind this work can be found in:

  @InCollection{Pardo97,
    author =       {Abelardo Pardo and Gary Hachtel},
    title =        {Automatic Abstraction Techniques for Propositional
                    $\mu$-calculus Model Checking},
    booktitle =    {9th Conference on Computer Aided Verification (CAV'97)},
    publisher =    {Springer-Verlag},
    year =         1997,
    editor =       {O. Grumberg},
    month =        jun,
    pages =        {12-23},
    note =         {LNCS-1254}
    }] 

  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

  Revision    [$Id: abs.h,v 1.5 2002/09/08 22:14:03 fabio Exp $]

******************************************************************************/

#ifndef _ABSINC
#define _ABSINC

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "fsm.h"

typedef struct AbsVerificationInfo Abs_VerificationInfo_t;

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

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

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

EXTERN void Abs_Init(void);
EXTERN void Abs_End(void);
EXTERN Abs_VerificationInfo_t * Abs_VerificationComputeInfo(Ntk_Network_t *network);
EXTERN array_t * Abs_FileParseFormulaArray(FILE *fp);

/**AutomaticEnd***************************************************************/

#endif /* _ABSINC */