source: vis_dev/vis-2.3/src/mc/mcInt.h @ 31

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

vis2.3
File size: 22.4 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [mcInt.h]
4
5  PackageName [mc]
6
7  Synopsis    [Internal declarations.]
8
9  Author      [Adnan Aziz and Tom Shiple, In-Ho Moon]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30  Revision    [$Id: mcInt.h,v 1.51 2008/04/22 21:24:49 fabio Exp $]
31
32******************************************************************************/
33
34#ifndef _MCINT
35#define _MCINT
36
37/*---------------------------------------------------------------------------*/
38/* Nested includes                                                           */
39/*---------------------------------------------------------------------------*/
40#include "heap.h"
41#include "ntm.h"
42#include "part.h"
43#include "mc.h"
44#include <string.h>
45
46
47/*---------------------------------------------------------------------------*/
48/* Constant declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51#define McMaxStringLength_c 1000
52
53
54/**Enum************************************************************************
55
56  Synopsis    [Level to which debugging of CTL formulae is performed.]
57
58******************************************************************************/
59
60typedef enum {
61  McDbgLevelNone_c,
62  McDbgLevelMin_c,
63  McDbgLevelMinVerbose_c,
64  McDbgLevelMax_c,
65  McDbgLevelInteractive_c
66} McDbgLevel;
67
68/**Enum************************************************************************
69
70  Synopsis    [Trimming mode for the enqueued sets of states.]
71
72  Description []
73
74******************************************************************************/
75
76typedef enum {
77  McLS_none_c, /* do not apply any trimming */
78  McLS_G_c,    /* apply EG to set of states */
79  McLS_H_c,    /* apply EH to set of states */
80  McLS_GH_c    /* apply both EG and EH to set of states */
81} McLockstepMode;
82
83
84/**Enum************************************************************************
85
86  Synopsis    [SCC generator status.]
87
88  Description [SCC generator status.  Empty means that there are no more
89  fair SCCs to be enumerated.]
90
91******************************************************************************/
92
93typedef enum {
94  McSccGenEmpty_c,
95  McSccGenNonEmpty_c
96} McSccGenStatus;
97
98
99/*---------------------------------------------------------------------------*/
100/* Structure declarations                                                    */
101/*---------------------------------------------------------------------------*/
102
103
104/**Struct**********************************************************************
105
106  Synopsis    [A struct for representing a paths.]
107
108  Description [Structure consists of two arrays of mdd's - the stem,
109  and the cycle (possibley empty if we are dealing with finite paths)]
110
111******************************************************************************/
112
113struct McPathStruct {
114  array_t *stemArray; /* represents a sequence of mdd's each corresponding to
115                       * a state, for the finite segment of the path
116                       */
117
118  array_t *cycleArray; /* represents a sequence of mdd's each corresponding to
119                        * a state, for the cycle of the path
120                        */
121};
122
123/**Struct**********************************************************************
124
125  Synopsis    [A struct for keeping the command line options.]
126
127******************************************************************************/
128
129struct McOptionsStruct {
130  boolean useMore;      /* use more as pipe for debug output */
131  boolean reduceFsm;
132  boolean printInputs;
133  boolean useFormulaTree;
134  boolean vd;   
135  boolean beer;   
136  boolean simFormat;
137  boolean FAFWFlag;
138  FILE *ctlFile;
139  FILE *guideFile;      /* file with hints (null if no guided search) */
140  FILE *systemFile;      /* file with system controlled variable for FAFW */
141  FILE *debugFile;
142  Mc_FwdBwdAnalysis fwdBwd;
143  Mc_LeMethod_t leMethod;
144  Mc_DcLevel dcLevel;
145  McDbgLevel dbgLevel;
146  Mc_GSHScheduleType schedule;
147  int lockstep;
148  Mc_VerbosityLevel verbosityLevel;
149  int timeOutPeriod;
150  boolean doCoverageHoskote;
151  boolean doCoverageImproved;
152  /* The following options are related with ARDC */
153  Fsm_ArdcOptions_t *ardcOptions;
154  Fsm_RchType_t invarApproxFlag; /* the type of reachability analysis for
155                                    invariant checking */
156  boolean invarOnionRingsFlag; /* flag to indicate whether onion rings should
157                                  be kept during reahability analysis */
158  /* The following option is for forward traversal */
159  Mc_FwdBwdAnalysis traversalDirection;
160  boolean incre; /* flag for incremental SAT solver in PureSAT*/
161  boolean sss; /* flag for SSS/Interpolation, 0 for ip, 1 for SSS*/
162  boolean flatIP; /* flag for flat interpolation algorithm*/
163  int IPspeed; /*enable various speed up techniques for PureSat+IP algorithm*/
164};
165
166/**Struct**********************************************************************
167
168  Synopsis [Keeps info on early termination: you can stop model
169  checking if you have some or all of the states]
170
171******************************************************************************/
172
173struct McEarlyTerminationStruct {
174  Mc_EarlyTerminationType mode;
175  mdd_t *states;
176};
177
178/**Struct**********************************************************************
179
180  Synopsis    [Fair SCC generator.]
181
182  Description []
183
184******************************************************************************/
185
186struct McSccGenStruct {
187  McSccGenStatus status;
188  Fsm_Fsm_t *fsm;
189  Heap_t *heap;
190  array_t *rings;               /* of mdd_t */
191  array_t *buechiFairness;      /* of mdd_t */
192  boolean earlyTermination;
193  Mc_VerbosityLevel verbosity;
194  Mc_DcLevel dcLevel;
195  int fairSccsFound;
196  int totalExamined;
197  int nImgComps;
198  int nPreComps;
199};
200
201/*---------------------------------------------------------------------------*/
202/* Type declarations                                                         */
203/*---------------------------------------------------------------------------*/
204
205typedef struct McPathStruct McPath_t;
206typedef struct McOptionsStruct McOptions_t;
207
208/*---------------------------------------------------------------------------*/
209/* Macro declarations                                                        */
210/*---------------------------------------------------------------------------*/
211
212#define GET_NORMAL_PT(_pt) ((mdd_t *)((unsigned long)(_pt) & ~01L))
213
214/**AutomaticStart*************************************************************/
215
216/*---------------------------------------------------------------------------*/
217/* Function prototypes                                                       */
218/*---------------------------------------------------------------------------*/
219
220EXTERN int McFsmDebugFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
221EXTERN void McFsmStateDebugFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
222EXTERN McPath_t * McBuildFairPath(mdd_t *startState, mdd_t *invariantStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis fwdBwd);
223EXTERN mdd_t* McFsmEvaluateEGFormulaUsingGSH(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType schedule);
224EXTERN mdd_t* McFsmEvaluateEHFormulaUsingGSH(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType schedule);
225EXTERN mdd_t * McEvaluateEUFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
226EXTERN mdd_t * McEvaluateAUFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
227EXTERN mdd_t * McEvaluateESFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
228EXTERN mdd_t * McEvaluateEGFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
229EXTERN mdd_t * McEvaluateEHFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
230EXTERN mdd_t * McEvaluateESFormulaWithGivenTRWithTarget( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
231EXTERN mdd_t * McEvaluateESFormulaWithGivenTRFAFW( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, mdd_t *Swin);
232EXTERN void McFormulaFreeDebugData(Ctlp_Formula_t *formula);
233EXTERN void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm);
234EXTERN mdd_t * McFsmComputeFairSCCsByLockStep(Fsm_Fsm_t *fsm, int maxNumberOfSCCs, array_t *SCCs, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
235EXTERN mdd_t * McFsmRefineFairSCCsByLockStep(Fsm_Fsm_t *fsm, int maxNumberOfSCCs, array_t *SCCs, array_t *sccClosedSets, array_t *careStates, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
236EXTERN mdd_t * McFsmRefineWeakFairSCCs(Fsm_Fsm_t *modelFsm, mdd_t *sccClosedSet, array_t *modelCareStatesArray, array_t *arrayOfOnionRings,boolean isSccTerminal,int dcLevel, int verbosity);
237EXTERN mdd_t * McFsmComputeOneFairSccByLinearStep(Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined);
238EXTERN mdd_t * McFsmComputeOneFairSccByLockStep(Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined);
239EXTERN array_t * McCompletePathFwd(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
240EXTERN array_t * McCompletePathBwd(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
241EXTERN int McCommandInitState(Hrc_Manager_t **hmgr, int argc, char **argv);
242EXTERN char * McStatePrintAsFormula(mdd_t *aMinterm, array_t *aSupport, Fsm_Fsm_t *modelFsm);
243EXTERN int McComputeOnionRingsWithClosestCore(mdd_t *aState, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm);
244EXTERN array_t * McRemoveIndexedOnionRings(int index, array_t *arrayOfOnionRings);
245EXTERN array_t * McConvertMintermToValueArray(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
246EXTERN void McPrintTransition(mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber);
247EXTERN void McPrintTransitionAiger(mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber);
248EXTERN void McStatePassesFormula(mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
249EXTERN void McStateFailsFormula(mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
250EXTERN void McStatePassesOrFailsFormula(mdd_t *aState, Ctlp_Formula_t *formula, int pass, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
251EXTERN McPath_t * McPathNormalize(McPath_t *aPath);
252EXTERN array_t * McCreateMergedPath(array_t *aPath, array_t *bPath);
253EXTERN array_t * McCreateJoinedPath(array_t *aPath, array_t *bPath);
254EXTERN boolean McStateSatisfiesFormula(Ctlp_Formula_t *aFormula, mdd_t *aState);
255EXTERN boolean McStateTestMembership(mdd_t *aState, mdd_t *setOfStates);
256EXTERN mdd_t * McGetSuccessorInTarget(mdd_t *aState, mdd_t *targetStates, Fsm_Fsm_t *modelFsm);
257EXTERN mdd_t * McGetSuccessorInTargetAmongFairStates(mdd_t *aState, mdd_t *targetStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm);
258EXTERN array_t * McPathReadStemArray(McPath_t *aPath);
259EXTERN array_t * McPathReadCycleArray(McPath_t *aPath);
260EXTERN void McPathSetStemArray(McPath_t *aPath, array_t *stemArray);
261EXTERN void McPathSetCycleArray(McPath_t *aPath, array_t *cycleArray);
262EXTERN McPath_t * McPathAlloc(void);
263EXTERN void McPathFree(McPath_t * aPath);
264EXTERN McOptions_t * McOptionsAlloc(void);
265EXTERN void McOptionsFree(McOptions_t *options);
266EXTERN Mc_LeMethod_t McOptionsReadLeMethod(McOptions_t *options);
267EXTERN McDbgLevel McOptionsReadDbgLevel(McOptions_t *options);
268EXTERN FILE * McOptionsReadGuideFile(McOptions_t *options);
269EXTERN FILE * McOptionsReadSystemFile(McOptions_t *options);
270EXTERN int McOptionsReadTimeOutPeriod(McOptions_t *options);
271EXTERN Mc_VerbosityLevel McOptionsReadVerbosityLevel(McOptions_t *options);
272EXTERN Mc_DcLevel McOptionsReadDcLevel(McOptions_t *options);
273EXTERN FILE * McOptionsReadCtlFile(McOptions_t *options);
274EXTERN FILE * McOptionsReadDebugFile(McOptions_t *options);
275EXTERN int McOptionsReadSimValue(McOptions_t *options);
276EXTERN int McOptionsReadUseMore(McOptions_t *options);
277EXTERN int McOptionsReadReduceFsm(McOptions_t *options);
278EXTERN int McOptionsReadPrintInputs(McOptions_t *options);
279EXTERN boolean McOptionsReadUseFormulaTree(McOptions_t *options);
280EXTERN Mc_GSHScheduleType McOptionsReadSchedule(McOptions_t *options);
281EXTERN int McOptionsReadLockstep(McOptions_t *options);
282EXTERN Fsm_RchType_t McOptionsReadInvarApproxFlag(McOptions_t *options);
283EXTERN boolean McOptionsReadInvarOnionRingsFlag(McOptions_t *options);
284EXTERN Mc_FwdBwdAnalysis McOptionsReadFwdBwd(McOptions_t *options);
285EXTERN Mc_FwdBwdAnalysis McOptionsReadTraversalDirection(McOptions_t *options);
286EXTERN Fsm_ArdcOptions_t * McOptionsReadArdcOptions(McOptions_t *options);
287EXTERN int McOptionsReadCoverageHoskote(McOptions_t *options);
288EXTERN int McOptionsReadCoverageImproved(McOptions_t *options);
289EXTERN void McOptionsSetFwdBwd(McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd);
290EXTERN void McOptionsSetGuideFile(McOptions_t *options, FILE *guideFile);
291EXTERN void McOptionsSetTraversalDirection(McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd);
292EXTERN void McOptionsSetUseMore(McOptions_t *options, boolean useMore);
293EXTERN void McOptionsSetReduceFsm(McOptions_t *options, boolean reduceFsm);
294EXTERN void McOptionsSetPrintInputs(McOptions_t *options, boolean printInputs);
295EXTERN void McOptionsSetUseFormulaTree(McOptions_t *options, boolean useFormulaTree);
296EXTERN void McOptionsSetSchedule(McOptions_t *options, Mc_GSHScheduleType schedule);
297EXTERN void McOptionsSetLockstep(McOptions_t *options, int lockstep);
298EXTERN void McOptionsSetSimValue(McOptions_t *options, boolean simValue);
299EXTERN void McOptionsSetDbgLevel(McOptions_t *options, McDbgLevel dbgLevel);
300EXTERN void McOptionsSetVerbosityLevel(McOptions_t *options, Mc_VerbosityLevel verbosityLevel);
301EXTERN void McOptionsSetLeMethod(McOptions_t *options, Mc_LeMethod_t leMethod);
302EXTERN void McOptionsSetDcLevel(McOptions_t *options, Mc_DcLevel dcLevel);
303EXTERN void McOptionsSetArdcOptions(McOptions_t *options, Fsm_ArdcOptions_t *ardcOptions);
304EXTERN void McOptionsSetInvarOnionRingsFlag(McOptions_t *options, int shellFlag);
305EXTERN void McOptionsSetCtlFile(McOptions_t *options, FILE *file);
306EXTERN void McOptionsSetDebugFile(McOptions_t *options, FILE *file);
307EXTERN void McOptionsSetTimeOutPeriod(McOptions_t *options, int timeOutPeriod);
308EXTERN void McOptionsSetInvarApproxFlag(McOptions_t *options, Fsm_RchType_t approxFlag);
309EXTERN void McOptionsSetCoverageHoskote(McOptions_t *options, boolean doCoverageHoskote);
310EXTERN void McOptionsSetCoverageImproved(McOptions_t *options, boolean doCoverageImproved);
311EXTERN void McOptionsSetVacuityDetect(McOptions_t *options, boolean vd);
312EXTERN boolean McOptionsReadVacuityDetect(McOptions_t *options);
313EXTERN void McOptionsSetBeerMethod(McOptions_t *options, boolean beer);
314EXTERN int McOptionsReadBeerMethod(McOptions_t *options);
315EXTERN void McOptionsSetFAFWFlag(McOptions_t *options, boolean FAFWFlag);
316EXTERN void McOptionsSetVariablesForSystem(McOptions_t *options, FILE  *systemFile);
317EXTERN boolean McQueryContinue(char *query);
318EXTERN void McPrintSupport(mdd_t *aMdd, mdd_manager *mddMgr, Ntk_Network_t *aNetwork);
319EXTERN int McPrintSimPath(FILE *outputFile, array_t *aPath, Fsm_Fsm_t *modelFsm);
320EXTERN Fsm_Fsm_t * McConstructReducedFsm(Ntk_Network_t *network, array_t *ctlFormulaArray);
321EXTERN Mc_EarlyTermination_t * McObtainUpdatedEarlyTerminationCondition(Mc_EarlyTermination_t *earlyTermination, mdd_t *careStates, Ctlp_FormulaType formulaType);
322EXTERN boolean McCheckEarlyTerminationForUnderapprox(Mc_EarlyTermination_t *earlyTermination, mdd_t *underApprox, array_t *careStatesArray);
323EXTERN boolean McCheckEarlyTerminationForOverapprox(Mc_EarlyTermination_t *earlyTermination, mdd_t *overApprox, array_t *careStatesArray);
324EXTERN mdd_t * McComputeACloseMinterm(mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr);
325EXTERN mdd_t * McComputeACloseState(mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm);
326EXTERN Mc_GSHScheduleType McStringConvertToScheduleType(char *string);
327EXTERN int McStringConvertToLockstepMode(char *string);
328EXTERN array_t *McMddArrayDuplicateFAFW(array_t *aPath);
329EXTERN void McNormalizeBddPointer(array_t *bddArray);
330
331EXTERN mdd_t *McMddArrayAnd(array_t *mddArray);
332EXTERN mdd_t *McMddArrayOr(array_t *mddArray);
333EXTERN mdd_t *McComputeAbstractStates(Fsm_Fsm_t *absFsm, mdd_t *reachableStates);
334EXTERN boolean McGetDncEnabled(void);
335EXTERN array_t * Mc_BuildForwardRings(mdd_t *S, Fsm_Fsm_t *fsm, array_t *onionRings); 
336EXTERN void Mc_CheckPathToCore(Fsm_Fsm_t *fsm, array_t *pathToCore);
337EXTERN void Mc_CheckPathFromCore(Fsm_Fsm_t *fsm, array_t *pathFromCore);
338EXTERN void Mc_PrintStates( Fsm_Fsm_t *modelFsm, mdd_t *states);
339EXTERN void Mc_PrintNumStates( Fsm_Fsm_t *modelFsm, mdd_t *states);
340EXTERN void Mc_PrintRings( Fsm_Fsm_t *modelFsm, array_t *onionRings);
341EXTERN void Mc_PrintNumRings( Fsm_Fsm_t *modelFsm, array_t *onionRings);
342EXTERN boolean McPrintPassFail(mdd_manager *mddMgr, Fsm_Fsm_t *modelFsm, Mc_FwdBwdAnalysis traversalDirection, Ctlp_Formula_t *ctlFormula, mdd_t *ctlFormulaStates, mdd_t *modelInitialStates, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity);
343EXTERN mdd_t * McModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula);
344EXTERN void InvarPrintDebugInformation(Fsm_Fsm_t *modelFsm, array_t *invarFormulaArray, array_t *invarStatesArray, int *resultArray, McOptions_t *options, array_t *hintsStatesArray);
345EXTERN array_t * SortFormulasByFsm(Fsm_Fsm_t *totalFsm, array_t *invarFormulaArray, array_t *fsmArray, McOptions_t *options);
346EXTERN int TestInvariantsInTotalFsm(Fsm_Fsm_t *totalFsm, array_t *invarStatesArray, int shellFlag);
347EXTERN void McEstimateCoverage(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis traversalDirection, mdd_t *modelInitialStates, mdd_t *ctlFormulaStates, mdd_t **totalcoveredstates, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList, boolean performCoverageHoskote, boolean performCoverageImproved);
348EXTERN void McPrintCoverageSummary(Fsm_Fsm_t *modelFsm, Mc_DcLevel dcLevel, McOptions_t *options, array_t *modelCareStatesArray, mdd_t *modelCareStates, mdd_t *totalcoveredstates, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, boolean performCoverageHoskote, boolean performCoverageImproved);
349EXTERN Ctlp_Approx_t ComputeResultingApproximation(Ctlp_FormulaType formulaType, Ctlp_Approx_t leftApproxType, Ctlp_Approx_t rightApproxType, Ctlp_Approx_t TRMinimization, Mc_EarlyTermination_t *earlyTermination, boolean fixpoint);
350EXTERN void McVacuityDetection(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options);
351
352/**AutomaticEnd***************************************************************/
353
354#endif /* _MCINT */
Note: See TracBrowser for help on using the repository browser.