source: vis_dev/vis-2.3/src/amc/amc.h @ 17

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

vis2.3
File size: 9.5 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [amc.h]
4
5  PackageName [amc]
6
7  Synopsis    [Model Check using over(under)-approximation of the transition
8  relation.]
9
10  Description [The package implements the approximate_model_check command.
11  The command is designed as a wrapper around the model_check command.
12  The command contains dual algorithms.  Predefined abstraction of the
13  transition relation is performed in a controlled way to ensure that the result
14  is reliable. By default, the command makes its effort to prove whether
15  the given ACTL formula is positive. User must set an environment variable
16  "amc_prove_false" when he/she wishes to prove whether the given ACTL formula
17  is negative.  When the formula is proven FALSE, then the error trace is
18  returned as in the model_check command.
19  Currently, one predefined approximation method, namely a "block-tearing"
20  method, is implemented. The package manipulate the internal data structure
21  of FSM to obtain over(under)-approximation of a given system. The algorithm
22  begin with coarse approximation in which the degree of initial approximation
23  is set by the user. Initial degree of approximation can be set by using
24  "amc_sizeof_group" environment. When the initial attempt using the coarse
25  approximation fails, the algorithm automatically combine subsystems(take
26  synchronous product) to obtain refined approximations. The procedure is
27  repeated until the approximation is good enough so that the result is
28  reliable.
29  ]
30
31
32  Author      [Woohyuk Lee]
33
34  Copyright [This file was created at the University of Colorado at Boulder.
35  The University of Colorado at Boulder makes no warranty about the suitability
36  of this software for any purpose.  It is presented on an AS IS basis.]
37
38  Revision    [$Id: amc.h,v 1.17 2002/09/08 23:15:15 fabio Exp $]
39
40******************************************************************************/
41
42#ifndef _AMC
43#define _AMC
44
45#include "part.h"
46
47/*---------------------------------------------------------------------------*/
48/* Constant declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Structure declarations                                                    */
54/*---------------------------------------------------------------------------*/
55
56/**Enum************************************************************************
57
58  Synopsis    [Methods for Approximation.]
59
60  Description [Currently, only Amc_Block_c is used. Amc_Block_c method
61  implements the abstraction method called "block tearing". The blocks of
62  subsystem is created by grouping the subset of vertices of the partition.
63  Based on the initial grouping into blocks of subsystems, over(under)-
64  approximation of the transition relation is created. The approximations of
65  the transition relation is used to conservatively verify either true
66  positive or true negative of a given ACTL formula.]
67
68******************************************************************************/
69typedef enum {
70  Amc_Variable_c,
71  Amc_Block_c,
72  Amc_Default_c
73} Amc_MethodType;
74
75/**Enum************************************************************************
76
77  Synopsis    [Verbosity Levels.]
78
79******************************************************************************/
80typedef enum {
81  Amc_VerbosityNone_c,
82  Amc_VerbositySpit_c,
83  Amc_VerbosityVomit_c
84} Amc_VerbosityLevel;
85
86/**Enum************************************************************************
87
88  Synopsis    [Quantification Mode.]
89
90******************************************************************************/
91typedef enum {
92  Amc_PresentVars_c,
93  Amc_NextVars_c,
94  Amc_InputVars_c,
95  Amc_User_c
96} Amc_QuantificationMode;
97
98/**Enum************************************************************************
99
100  Synopsis    [Verification Results.]
101
102******************************************************************************/
103typedef enum {
104  Amc_Verified_Unknown_c,
105  Amc_Verified_True_c,
106  Amc_Verified_False_c
107} Amc_Verified_Answer;
108
109/*---------------------------------------------------------------------------*/
110/* Type declarations                                                         */
111/*---------------------------------------------------------------------------*/
112
113typedef struct AmcSubsystemInfo Amc_SubsystemInfo_t;
114typedef struct AmcInfoStruct Amc_Info_t;
115
116#include "mc.h"
117
118/*---------------------------------------------------------------------------*/
119/* Variable declarations                                                     */
120/*---------------------------------------------------------------------------*/
121
122
123/*---------------------------------------------------------------------------*/
124/* Macro declarations                                                        */
125/*---------------------------------------------------------------------------*/
126
127
128/**AutomaticStart*************************************************************/
129
130/*---------------------------------------------------------------------------*/
131/* Function prototypes                                                       */
132/*---------------------------------------------------------------------------*/
133
134EXTERN void Amc_AmcEvaluateFormula(Ntk_Network_t *network, Ctlp_Formula_t *formula, int verbosity);
135EXTERN Amc_Info_t * Amc_AmcInfoInitialize(Ntk_Network_t *network, Ctlp_Formula_t *formula, Amc_MethodType methodType, int verbosity);
136EXTERN mdd_t * Amc_AmcExistentialQuantifySubsystem(Amc_SubsystemInfo_t *subSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode);
137EXTERN array_t * Amc_AmcExistentialQuantifySubsystemArray(array_t *subSystemArray, Amc_SubsystemInfo_t *currentSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode);
138EXTERN Fsm_Fsm_t * Amc_AmcSubsystemReadFsm(Amc_SubsystemInfo_t *system);
139EXTERN void Amc_AmcSubsystemSetFsm(Amc_SubsystemInfo_t *system, Fsm_Fsm_t *info);
140EXTERN array_t * Amc_AmcSubsystemReadRelationArray(Amc_SubsystemInfo_t *system);
141EXTERN void Amc_AmcSubsystemSetRelationArray(Amc_SubsystemInfo_t *system, array_t *info);
142EXTERN mdd_t * Amc_AmcSubsystemReadNextStateVarSmoothen(Amc_SubsystemInfo_t *system);
143EXTERN void Amc_AmcSubsystemSetNextStateVarSmoothen(Amc_SubsystemInfo_t *system, mdd_t *info);
144EXTERN mdd_t * Amc_AmcSubsystemReadSatisfy(Amc_SubsystemInfo_t *system);
145EXTERN void Amc_AmcSubsystemSetSatisfy(Amc_SubsystemInfo_t *system, mdd_t *data);
146EXTERN st_table * Amc_AmcSubsystemReadVertexTable(Amc_SubsystemInfo_t *system);
147EXTERN void Amc_AmcSubsystemSetVertexTable(Amc_SubsystemInfo_t *system, st_table *data);
148EXTERN st_table * Amc_AmcSubsystemReadFanInTable(Amc_SubsystemInfo_t *system);
149EXTERN void Amc_AmcSubsystemSetFanInTable(Amc_SubsystemInfo_t *system, st_table *data);
150EXTERN st_table * Amc_AmcSubsystemReadFanOutTable(Amc_SubsystemInfo_t *system);
151EXTERN void Amc_AmcSubsystemSetFanOutTable(Amc_SubsystemInfo_t *system, st_table *data);
152EXTERN char * Amc_AmcSubsystemReadMethodSpecificData(Amc_SubsystemInfo_t *system);
153EXTERN void Amc_AmcSubsystemSetMethodSpecificData(Amc_SubsystemInfo_t *system, char *data);
154EXTERN mdd_t * Amc_AmcReadInitialStates(Amc_Info_t *system);
155EXTERN void Amc_AmcSetInitialStates(Amc_Info_t *system, mdd_t *data);
156EXTERN Amc_SubsystemInfo_t * Amc_AmcReadOptimalSystem(Amc_Info_t *system);
157EXTERN void Amc_AmcSetOptimalSystem(Amc_Info_t *system, Amc_SubsystemInfo_t *data);
158EXTERN void * Amc_AmcReadMethodData(Amc_Info_t *system);
159EXTERN void Amc_AmcSetMethodData(Amc_Info_t *system, void *data);
160EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemAllocate(void);
161EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemCreate(Fsm_Fsm_t *fsm, mdd_t *satisfyStates, st_table *vertexTable, st_table *fanInTable, st_table *fanOutTable);
162EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemDuplicate(Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem);
163EXTERN void Amc_AmcSubsystemFree(Amc_SubsystemInfo_t *subSystem);
164EXTERN void Amc_AmcSubsystemFreeAlsoPartition(Amc_SubsystemInfo_t *subSystem);
165EXTERN Amc_SubsystemInfo_t * Amc_CombineSubsystems(Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem1, Amc_SubsystemInfo_t *subSystem2);
166EXTERN Img_ImageInfo_t * Amc_AmcReadOrCreateImageInfo(Fsm_Fsm_t *fsm);
167EXTERN mdd_t * Amc_AmcEvaluateCTLFormula(Amc_SubsystemInfo_t *subSystem, array_t *subSystemArray, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, mdd_t *modelCareStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
168EXTERN mdd_t * Amc_AmcEvaluateEXFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
169EXTERN mdd_t * Amc_AmcEvaluateEUFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, array_t *onionRings, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
170EXTERN mdd_t * Amc_AmcEvaluateEGFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, mdd_t *careStates, array_t *onionRingsArrayForDbg, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
171EXTERN void Amc_Init(void);
172EXTERN void Amc_End(void);
173
174/**AutomaticEnd***************************************************************/
175
176#endif /* _AMC */
Note: See TracBrowser for help on using the repository browser.