source: vis_dev/vis-2.3/src/abs/abs.h @ 43

Last change on this file since 43 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 2.8 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [abs.h]
4
5  PackageName [abs]
6
7  Synopsis    [Incremental CTL model checker.]
8
9  Description [This package provides the command "incremental_ctl_verification",
10  an algorithm to verify CTL formulas starting from an initial abstraction and
11  applying refinements to increment the level of accuracy in the verification.
12  The theory behind this work can be found in:
13
14  @InCollection{Pardo97,
15    author =       {Abelardo Pardo and Gary Hachtel},
16    title =        {Automatic Abstraction Techniques for Propositional
17                    $\mu$-calculus Model Checking},
18    booktitle =    {9th Conference on Computer Aided Verification (CAV'97)},
19    publisher =    {Springer-Verlag},
20    year =         1997,
21    editor =       {O. Grumberg},
22    month =        jun,
23    pages =        {12-23},
24    note =         {LNCS-1254}
25    }]
26
27  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
28
29  Copyright   [This file was created at the University of Colorado at
30  Boulder.  The University of Colorado at Boulder makes no warranty
31  about the suitability of this software for any purpose.  It is
32  presented on an AS IS basis.]
33
34  Revision    [$Id: abs.h,v 1.5 2002/09/08 22:14:03 fabio Exp $]
35
36******************************************************************************/
37
38#ifndef _ABSINC
39#define _ABSINC
40
41/*---------------------------------------------------------------------------*/
42/* Nested includes                                                           */
43/*---------------------------------------------------------------------------*/
44#include "fsm.h"
45
46typedef struct AbsVerificationInfo Abs_VerificationInfo_t;
47
48/*---------------------------------------------------------------------------*/
49/* Structure declarations                                                    */
50/*---------------------------------------------------------------------------*/
51
52/*---------------------------------------------------------------------------*/
53/* Nested includes                                                           */
54/*---------------------------------------------------------------------------*/
55
56/**AutomaticStart*************************************************************/
57
58/*---------------------------------------------------------------------------*/
59/* Function prototypes                                                       */
60/*---------------------------------------------------------------------------*/
61
62EXTERN void Abs_Init(void);
63EXTERN void Abs_End(void);
64EXTERN Abs_VerificationInfo_t * Abs_VerificationComputeInfo(Ntk_Network_t *network);
65EXTERN array_t * Abs_FileParseFormulaArray(FILE *fp);
66
67/**AutomaticEnd***************************************************************/
68
69#endif /* _ABSINC */
70
Note: See TracBrowser for help on using the repository browser.