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

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

vis2.3
File size: 19.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [mc.h]
4
5  PackageName [mc]
6
7  Synopsis    [Fair CTL model checker and debugger.]
8
9  Description [Fair CTL model checker and debugger.  Works on a flattened
10  network.]
11
12  Author      [Adnan Aziz, Tom Shiple, In-Ho Moon]
13
14  Comment     []
15 
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: mc.h,v 1.54 2007/04/17 00:01:22 sohail Exp $]
36
37******************************************************************************/
38
39#ifndef _MC
40#define _MC
41
42/*---------------------------------------------------------------------------*/
43/* Nested includes                                                           */
44/*---------------------------------------------------------------------------*/
45#include "cmd.h"
46#include "ctlp.h"
47#include "ctlsp.h"
48#include "ntk.h"
49
50/*---------------------------------------------------------------------------*/
51/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/* Use this if you don't want early termination */
55#define MC_NO_EARLY_TERMINATION (NIL(Mc_EarlyTermination_t))
56
57/* Constants for lockstep mode. */
58#define MC_LOCKSTEP_UNASSIGNED          -3
59#define MC_LOCKSTEP_OFF                 -2
60#define MC_LOCKSTEP_EARLY_TERMINATION   -1
61#define MC_LOCKSTEP_ALL_SCCS            0
62
63/*---------------------------------------------------------------------------*/
64/* Structure declarations                                                    */
65/*---------------------------------------------------------------------------*/
66
67/**Enum************************************************************************
68
69  Synopsis    [Use forward or backward analysis]
70
71******************************************************************************/
72
73typedef enum {
74  McFwd_c,
75  McBwd_c /* someday there may be a mixed method */
76} Mc_FwdBwdAnalysis;
77
78/**Enum************************************************************************
79
80  Synopsis    [Extent to which Mc functions provide feedback/stats.]
81
82******************************************************************************/
83
84typedef enum {
85  McVerbosityNone_c,
86  McVerbosityLittle_c,
87  McVerbositySome_c,
88  McVerbosityMax_c
89} Mc_VerbosityLevel;
90
91/**Enum************************************************************************
92
93  Synopsis    [Extent to which don't cares are used in Mc functions.]
94
95******************************************************************************/
96
97typedef enum {
98  McDcLevelNone_c,
99  McDcLevelRch_c,
100  McDcLevelRchFrontier_c,
101  McDcLevelArdc_c
102} Mc_DcLevel;
103
104
105/**Enum************************************************************************
106
107  Synopsis [When creating a path from aState to bState, make it non trivial
108  (ie a cycle) when aState == bState and McPathLengthType is McGreaterZero_c.]
109
110******************************************************************************/
111
112typedef enum {
113  McGreaterZero_c,
114  McGreaterOrEqualZero_c
115} Mc_PathLengthType;
116
117
118/**Enum************************************************************************
119
120  Synopsis    [Some,all or care, for Mc_EarlyTermination_t]
121
122******************************************************************************/
123
124typedef enum {
125  McSome_c,
126  McAll_c,
127  McCare_c
128} Mc_EarlyTerminationType;
129
130/**Enum************************************************************************
131
132  Synopsis [What kind of hints?]
133
134  Description [Would you like that with no hints, global hints or
135  local hints?  Paper or plastic?]
136
137  SideEffects []
138
139  SeeAlso []
140 
141******************************************************************************/
142typedef enum {
143  Mc_None_c,
144  Mc_Global_c,
145  Mc_Local_c
146} Mc_GuidedSearch_t;
147
148/**Enum************************************************************************
149
150  Synopsis [Specifies the method for language emptiness checking]
151
152  Description [Specifies the method used by command ltl and le for
153  checking the language emptiness.]
154
155  SideEffects []
156
157  SeeAlso []
158 
159******************************************************************************/
160typedef enum {
161  Mc_Le_Default_c,
162  Mc_Le_Dnc_c
163} Mc_LeMethod_t;
164
165/**Enum************************************************************************
166
167  Synopsis [Specifies the automaton strength]
168
169  Description [Specifies the automaton strength]
170
171  SideEffects []
172
173  SeeAlso []
174 
175******************************************************************************/
176typedef enum {
177    Mc_Aut_Terminal_c,
178    Mc_Aut_Weak_c,
179    Mc_Aut_Strong_c
180} Mc_AutStrength_t;
181
182/**Enum************************************************************************
183
184  Synopsis    [Type of GSH schedule.]
185
186  Description [The GSH schedule is the policy followed by the GSH
187  algorithm in applying the EU and EX operators.  If there are
188  <code>n</code> fairness constraints, the operators are
189  <code>EU1,...,EUn,EX</code>.  Currently, three schedules are
190  supported: EL, EL1, EL2, budget, and random.
191  <ul>
192  <li> EL: <code>EU1 EX ... EUn EX EU1 EX ... EUn EX ...</code>.
193  <li> EL1: <code>EU1 ... EUn EX EU1 ... EUn EX ...</code>.
194  <li> EL2: <code>EU1 ... EUn EX EX ... EU1 ... EUn EX EX ... ...</code>.
195  <li> budget: like EL2, but <code>EX</code> not allowed more times than
196       number of <code>EXs</code> performed inside <code>EUs</code>.
197  <li> random: operators are chosen in a pseudorandom fashion with 0.5
198       probability assigned to <code>EX</code> (as in EL).
199  </ul>]
200
201******************************************************************************/
202
203typedef enum {
204  McGSH_old_c,       /* do not use GSH */
205  McGSH_EL_c,        /* Emerson-Lei schedule */
206  McGSH_EL1_c,       /* modified Emerson-Lei schedule */
207  McGSH_EL2_c,       /* Hojati's EL2 schedule (a.k.a. OWCTY) */
208  McGSH_Budget_c,    /* EL2 with EX budget */
209  McGSH_Random_c,    /* Random schedule */
210  McGSH_Unassigned_c /* invalid schedule */
211} Mc_GSHScheduleType;
212
213/*---------------------------------------------------------------------------*/
214/* Type declarations                                                         */
215/*---------------------------------------------------------------------------*/
216
217/*-----------------------------------------------------------------------------
218
219  Synopsis    [The type of the onion rings]
220
221  Description [Onion rings are arrays of mdd_t*s, decribes in onionRings.c]
222
223-----------------------------------------------------------------------------*/
224typedef array_t OnionRing_t;
225
226typedef struct McEarlyTerminationStruct Mc_EarlyTermination_t;
227typedef struct McSccGenStruct Mc_SccGen_t;
228
229
230/*---------------------------------------------------------------------------*/
231/* Macro declarations                                                        */
232/*---------------------------------------------------------------------------*/
233
234
235/**Macro***********************************************************************
236
237  Synopsis     [Iterates over the fair SCCs of a FSM.]
238
239  Description  [Iterates over the fair SCCs of a FSM.  The parameters are:
240  <ul>
241  <li> Fsm_Fsm_t *fsm,
242  <li> Mc_SccGen_t *gen,
243  <li> mdd_t *scc,
244  <li> array_t *sccClosedSetArray, ( of mdd_t * )
245  <li> array_t *leftover,          ( of mdd_t *, can be NULL )
246  <li> array_t *buechiFairness,    ( of mdd_t * )
247  <li> array_t *onionRings,        ( of mdd_t * )
248  <li> boolean earlyTermination,
249  <li> Mc_VerbosityLevel verbosity,
250  <li> Mc_DcLevel dcLevel.
251  </ul>
252  Mc_FsmForEachFairScc allocates and frees the generator.  Therefore the
253  application should not try to do that unless it breaks out of the
254  loop, in which case it must call Mc_FsmSccGenFree explicitly.  If
255  earlyTermination is TRUE, at most one fair SCC is enumerated.
256  Setting earlyTermination to TRUE differs from breaking out of hte
257  loop after the first fair SCC is enumerated in three respects.
258  <ul>
259  <li> The set of states returned in scc is guaranteed to contain a fair
260       SCC, but it may also contain states not belonging to that SCC.
261  <li> early termination is typically faster, however,
262  <li> one cannot retrive the sets of states not yet processed.  Even if
263       leftover is non NIL, nothing is added to it.
264  </ul>]
265
266  SideEffects  [none]
267
268  SeeAlso      [Mc_FsmFirstScc Mc_FsmNextScc Mc_FsmIsSccGenEmpty
269  Mc_FsmSccGenFree]
270
271******************************************************************************/
272#define Mc_FsmForEachFairScc(fsm, gen, scc, sccClosedSetArray, leftover,\
273                             buechiFairness, onionRings, earlyTermination,\
274                             verbosity, dcLevel)\
275  for((gen) = Mc_FsmFirstScc(fsm, &scc, sccClosedSetArray, buechiFairness,\
276                             onionRings, earlyTermination,\
277                             verbosity, dcLevel);\
278    Mc_FsmIsSccGenEmpty(gen) ? Mc_FsmSccGenFree(gen, leftover) : TRUE;\
279    (void) Mc_FsmNextScc(gen, &scc))
280
281/*---------------------------------------------------------------------------*/
282/* Nested includes                                                           */
283/*---------------------------------------------------------------------------*/
284#include "fsm.h"
285#include "part.h"
286
287/**AutomaticStart*************************************************************/
288
289/*---------------------------------------------------------------------------*/
290/* Function prototypes                                                       */
291/*---------------------------------------------------------------------------*/
292
293EXTERN void Mc_Init(void);
294EXTERN void Mc_End(void);
295EXTERN mdd_t * Mc_FsmCheckLanguageEmptiness(Fsm_Fsm_t *modelFsm, array_t *modelCareStatesArray, Mc_AutStrength_t automatonStrength, Mc_LeMethod_t leMethod, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName);
296EXTERN mdd_t * Mc_FsmEvaluateFormula(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule);
297EXTERN mdd_t * Mc_FsmEvaluateEXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
298EXTERN mdd_t * Mc_FsmEvaluateMXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
299EXTERN mdd_t * Mc_FsmEvaluateAXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
300EXTERN mdd_t * Mc_FsmEvaluateEYFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
301EXTERN mdd_t * Mc_FsmEvaluateEUFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
302EXTERN mdd_t * Mc_FsmEvaluateAUFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
303EXTERN mdd_t * Mc_FsmEvaluateESFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *source, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
304EXTERN mdd_t * Mc_FsmEvaluateEGFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule);
305EXTERN mdd_t * Mc_FsmEvaluateEHFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule);
306EXTERN mdd_t * Mc_FsmEvaluateFwdUFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
307EXTERN mdd_t * Mc_FsmEvaluateFwdGFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
308EXTERN mdd_t * Mc_FsmEvaluateFwdEHFormula(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
309EXTERN void Mc_FsmEvaluateFormulaForVacuity(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates);
310EXTERN mdd_t *Mc_QuantifyInputFAFW(Fsm_Fsm_t *fsm, bdd_t *result);
311EXTERN Mc_SccGen_t * Mc_FsmFirstScc(Fsm_Fsm_t *fsm, mdd_t **scc, array_t *sccClosedSetArray, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
312EXTERN boolean Mc_FsmNextScc(Mc_SccGen_t *gen, mdd_t **scc);
313EXTERN boolean Mc_FsmIsSccGenEmpty(Mc_SccGen_t *gen);
314EXTERN boolean Mc_FsmSccGenFree(Mc_SccGen_t *gen, array_t *leftover);
315EXTERN int Mc_FsmComputeStatesReachingToSet(Fsm_Fsm_t *modelFsm, mdd_t *targetStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
316EXTERN int Mc_FsmComputeStatesReachableFromSet(Fsm_Fsm_t *modelFsm, mdd_t *initialStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
317EXTERN boolean Mc_FormulaStaticSemanticCheckOnNetwork(Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
318EXTERN array_t * Mc_BuildPathToCore(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType);
319EXTERN array_t * Mc_BuildPathToCoreFAFW(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType);
320EXTERN array_t * Mc_BuildPathFromCore(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType);
321EXTERN array_t * Mc_BuildPathFromCoreFAFW(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType);
322EXTERN array_t * Mc_CompletePath(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis dirn);
323EXTERN mdd_t * Mc_ComputeAMinterm(mdd_t *aSet, array_t *Support, mdd_manager *mddMgr);
324EXTERN mdd_t * Mc_ComputeACloseMinterm(mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr);
325EXTERN char * Mc_MintermToString(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork);
326EXTERN char * Mc_MintermToStringAiger(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork);
327EXTERN char * Mc_MintermToStringAigerInput(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork);
328EXTERN int Mc_PrintPath(array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput);
329EXTERN int Mc_PrintPathAiger(array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput);
330EXTERN mdd_t * Mc_FsmComputeDrivingInputMinterms(Fsm_Fsm_t *fsm, mdd_t *aState, mdd_t *bState);
331EXTERN mdd_t * Mc_ComputeAState(mdd_t *states, Fsm_Fsm_t *modelFsm);
332EXTERN mdd_t * Mc_ComputeACloseState(mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm);
333EXTERN void Mc_MintermPrint(mdd_t *aMinterm, array_t *support, Ntk_Network_t *aNetwork);
334EXTERN void Mc_NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable);
335EXTERN void Mc_NodeTableAddLtlFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable);
336EXTERN Fsm_Fsm_t * Mc_ConstructReducedFsm(Ntk_Network_t *network, array_t *ctlFormulaArray);
337EXTERN Mc_GSHScheduleType Mc_StringConvertToScheduleType(char *string);
338EXTERN int Mc_StringConvertToLockstepMode(char *string);
339EXTERN Mc_EarlyTermination_t * Mc_EarlyTerminationAlloc(Mc_EarlyTerminationType mode, mdd_t *states);
340EXTERN void Mc_EarlyTerminationFree(Mc_EarlyTermination_t *earlyTermination);
341EXTERN boolean Mc_EarlyTerminationIsSkip(Mc_EarlyTermination_t *earlyTermination);
342EXTERN array_t * Mc_ReadHints(FILE *guideFP);
343EXTERN st_table * Mc_ReadSystemVariablesFAFW(Fsm_Fsm_t *fsm, FILE *systemFP);
344EXTERN array_t * Mc_EvaluateHints(Fsm_Fsm_t *fsm, Ctlp_FormulaArray_t *invarArray);
345EXTERN array_t * Mc_ComputeGuideArray(Fsm_Fsm_t *fsm, FILE *guideFP);
346EXTERN Mc_GuidedSearch_t Mc_ReadGuidedSearchType(void);
347EXTERN array_t *
348Mc_BuildShortestPathFAFW(mdd_t *win, mdd_t *S, mdd_t *T, array_t *rings, mdd_manager *mgr, Fsm_Fsm_t *fsm, int prevFlag);
349EXTERN st_table *Mc_SetAllInputToSystem(Fsm_Fsm_t *fsm);
350EXTERN array_t * Mc_BuildFAFWLayer(Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H);
351EXTERN array_t * MC_BuildCounterExampleFAFWGeneral( Fsm_Fsm_t *modelFsm, mdd_t *I, mdd_t *T, mdd_t *H, array_t *L);
352EXTERN array_t * Mc_BuildPathFromCoreFAFWGeneral( mdd_t *T, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType);
353EXTERN array_t * Mc_BuildForwardRingsWithInvariants( mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm);
354EXTERN array_t * Mc_CreateStaticRefinementScheduleArray(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, boolean dynamicIncrease, boolean isLatchNameSort, int verbosity, int incrementalSize, Part_CMethod correlationMethod);
355EXTERN mdd_t * Mc_FsmCheckLanguageEmptinessByDnC(Fsm_Fsm_t *modelFsm, array_t *modelCareStatesArray, Mc_AutStrength_t automatonStrength, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName);
356
357
358
359/**AutomaticEnd***************************************************************/
360
361#endif /* _MC */
Note: See TracBrowser for help on using the repository browser.