source: vis_dev/vis-2.3/src/amc/amcAmc.c @ 36

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

vis2.3
File size: 79.4 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [amcAmc.c]
4
5  PackageName [amc]
6
7  Synopsis    [Approximate Model Checker.]
8
9  Author      [Woohyuk Lee <woohyuk@duke.colorado.edu>]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "amcInt.h"
18#include "mcInt.h"
19
20static char rcsid[] UNUSED = "$Id: amcAmc.c,v 1.57 2005/04/16 04:22:41 fabio Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26
27/*---------------------------------------------------------------------------*/
28/* Type declarations                                                         */
29/*---------------------------------------------------------------------------*/
30
31
32/*---------------------------------------------------------------------------*/
33/* Structure declarations                                                    */
34/*---------------------------------------------------------------------------*/
35
36
37/*---------------------------------------------------------------------------*/
38/* Variable declarations                                                     */
39/*---------------------------------------------------------------------------*/
40
41
42/*---------------------------------------------------------------------------*/
43/* Macro declarations                                                        */
44/*---------------------------------------------------------------------------*/
45
46
47/**AutomaticStart*************************************************************/
48
49/*---------------------------------------------------------------------------*/
50/* Static function prototypes                                                */
51/*---------------------------------------------------------------------------*/
52static int stringCompare(const void *s1, const void *s2);
53
54/**AutomaticEnd***************************************************************/
55
56
57/*---------------------------------------------------------------------------*/
58/* Definition of exported functions                                          */
59/*---------------------------------------------------------------------------*/
60
61/**Function********************************************************************
62
63  Synopsis [Evaluate formula with approximations.]
64
65  Description [Starting from an initial coarse approximation, find an
66  approximation that produces reliable result. The degree of approximation
67  is determined by the number of vertices contained in a subsystem. The initial
68  number of vertices in a subsystem is set by "amc_sizeof_group" environment.
69  The algorithm searches a virtual lattice of approximations in which the
70  level of the lattice is defined as the degree of approximations. Once the
71  approximations in a certain level fails to prove the formula, the algorithm
72  automatically refines the approximation by combining(taking the synchronous
73  product) of subsystems. It repeats the process until the approximation is
74  refined enough to produce a reliable result. The procedure may also be
75  viewed as finding a pseudo-optimal path starting from the coarse
76  approximations(in level 1 of the lattice of approximations) to the
77  approximations that produce reliable result. One can draw a virtual contour
78  separating the approximations that produce faulty results and the reliable
79  results. We call this virtual placement of the approximations and the
80  contour separting the two regions, a lattice of approximations.
81  The algorithms are dual. Each algorithm makes its effort to prove whether the
82  formula is positive or negative respectively. When proving true positive of
83  given ACTL formula we use over-approximation  of the transition relation,
84  and to prove true negative, we use under-approximation of the transition
85  relation.]
86
87
88  SideEffects []
89
90  SeeAlso []
91 
92******************************************************************************/
93void
94Amc_AmcEvaluateFormula(
95  Ntk_Network_t         *network,
96  Ctlp_Formula_t        *formula,
97  int                   verbosity)
98{
99  Amc_Info_t            *amcInfo;
100  int                   levelOfLattice;
101  char                  *flagValue;
102
103  long initialTime = 0;
104  long finalTime;
105
106
107  /*
108   * If the partition was not created, get out.  We are assuming we were able to
109   * construct BDD for each combinational outputs.
110   */
111
112  graph_t       *partition = Part_NetworkReadPartition(network);
113  if (partition == NIL(graph_t)) {
114    error_append("** amc error: Network has no partition. Cannot apply approximate model checking.");
115    return;
116  }
117
118
119  /*
120   * Initialize data structures.
121   */
122  amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);
123
124
125
126  /*
127   * Check every possible environment variables that user may have set.
128   * And give user some assurance by reporting the flag values.
129   * Explanation of possible environment variables are discussed in the
130   * man page of the package.
131   */
132  amcInfo->isMBM = 0;
133
134  flagValue = Cmd_FlagReadByName("amc_prove_false");
135  if (flagValue == NIL(char)){
136    amcInfo->lowerBound = 0;
137    fprintf(vis_stdout, "\n#AMC: Proving whether the formula is true.\n");
138  }
139  else {
140    amcInfo->lowerBound = 1;
141    fprintf(vis_stdout, "\n#AMC: Proving whether the formula is false.\n");
142  }
143
144  if(verbosity) {
145    flagValue = Cmd_FlagReadByName("amc_grouping_method");
146    if (flagValue == NIL(char)){
147      amcInfo->groupingMethod = 0;
148      fprintf(vis_stdout, "\n#AMC: No grouping method has been set."); 
149    }
150    else {
151      amcInfo->groupingMethod = 1;
152      fprintf(vis_stdout, "\n#AMC: Using latch dependency method for grouping latches into subsystems.");
153    }
154  }
155
156
157
158  /*
159   * The lattice of approximation algorithm.
160   */
161
162  levelOfLattice = array_n(amcInfo->subSystemArray);
163  amcInfo->currentLevel = 1;
164
165  while(levelOfLattice >= amcInfo->currentLevel) {
166    if(verbosity) {
167      (void)fprintf(vis_stdout, "\n\n##AMC: Entering level %d(%d) of the lattice of approximations\n", 
168                                   amcInfo->currentLevel, levelOfLattice);
169      fflush(vis_stdout);
170    }
171
172
173    initialTime = util_cpu_time();
174
175    if( (!(*amcInfo->amcBoundProc)(amcInfo, formula, verbosity)) && !(amcInfo->isVerified) ) {
176
177      /* Automatically switches to lattice of lowerbound approximations */
178      if(verbosity)
179        (void)fprintf(vis_stdout, "Abandoning upper bound approximations.\n");
180
181      /* Free all */
182      (*amcInfo->amcFreeProc)(amcInfo);
183
184      amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);
185      amcInfo->lowerBound = TRUE;
186      amcInfo->currentLevel = 0;
187
188    }
189    else if(amcInfo->isVerified) {
190      finalTime = util_cpu_time();
191      if(verbosity == Amc_VerbosityVomit_c) {
192        (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =", 
193                                    (finalTime - initialTime) / 1000);
194      }
195
196      if(amcInfo->amcAnswer == Amc_Verified_True_c) {
197        (void) fprintf(vis_stdout, "\n# AMC: Verified formula TRUE at level %d of %d : ",
198                       amcInfo->currentLevel, levelOfLattice);
199      }else if(amcInfo->amcAnswer == Amc_Verified_False_c) {
200        (void) fprintf(vis_stdout, "\n# AMC: Verified formula FALSE at level %d of %d : ",
201                       amcInfo->currentLevel, levelOfLattice);
202      }else{
203        fprintf(vis_stdout, "\n# AMC: formula unknown --- ");
204        Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
205        (void) fprintf(vis_stdout, "\n# AMC: Verified formula UNKNOWN at level %d of %d : ",
206                       amcInfo->currentLevel, levelOfLattice);
207      }
208      (void) fprintf(vis_stdout, "\n# AMC: ");
209      Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
210      AmcPrintOptimalSystem(vis_stdout, amcInfo);
211      (*amcInfo->amcFreeProc)(amcInfo);
212      return;
213    } /* end of else if(amcInfo->isVerified) */
214   
215    amcInfo->currentLevel++;
216  } /* end of while(levelOfLattice >= amcInfo->currentLevel) */
217 
218  finalTime = util_cpu_time();
219  if(verbosity == Amc_VerbosityVomit_c) {
220    (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
221                   (finalTime - initialTime) / 1000);
222  }
223 
224  /*
225  ** Now, spec was not verified becase there was an error in computation.
226  */ 
227  (void) fprintf(vis_stdout, "\n# AMC: The spec was not able to be verified.\n# AMC: ");
228  Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
229  (*amcInfo->amcFreeProc)(amcInfo);
230 
231}
232
233
234/**Function********************************************************************
235
236  Synopsis    [Initializes an amcInfo structure for the given method.]
237
238  Description [Regardless of the method type, the initialization procedure
239  starts from constructing set of subsystems. A subsystem contains a subset
240  of vertices of the partition. Based on the subset of vertices, subFSM is
241  created. The subsystems are stored as an array. After the creation of
242  the subsystem array, the function initializes remaining field of
243  (Amc_Info_t *) amcInfo.
244  The function returns initialized (Amc_Info_t *) amcInfo.]
245
246  SideEffects        []
247
248  SeeAlso     []
249
250******************************************************************************/
251Amc_Info_t *
252Amc_AmcInfoInitialize(
253  Ntk_Network_t         *network,
254  Ctlp_Formula_t        *formula,
255  Amc_MethodType        methodType,
256  int                   verbosity)
257{
258  Amc_Info_t            *amcInfo;
259  char                  *userSpecifiedMethod;
260
261  amcInfo = ALLOC(Amc_Info_t, 1);
262  amcInfo->network = network;
263
264  /*
265   * AmcCreateSubsystems creates fsm for each subsystem and returns subSystemArray.
266   */
267  amcInfo->subSystemArray = AmcCreateSubsystemArray(network, formula);
268
269#ifdef AMC_DEBUG
270AmcCheckSupportAndOutputFunctions(amcInfo->subSystemArray);
271#endif
272
273  /*
274   * Initialize optimalSystem, isVerified;
275   */
276  amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
277  amcInfo->isVerified = 0;
278  amcInfo->amcAnswer = Amc_Verified_Unknown_c;
279
280  /*
281   * If methodType is default, use user-specified method.
282   */
283  if (methodType == Amc_Default_c) {
284    userSpecifiedMethod = Cmd_FlagReadByName("amc_method");
285    if (userSpecifiedMethod == NIL(char)) {
286      methodType = Amc_Block_c;
287    }
288    else {
289      if (strcmp(userSpecifiedMethod, "block") == 0) {
290        methodType = Amc_Block_c;
291      }
292      else if (strcmp(userSpecifiedMethod, "variable") == 0) {
293        methodType = Amc_Variable_c;
294      }
295      else {
296        (void) fprintf(vis_stderr, "** amc error: Unrecognized amc_method %s: using Block method.\n",
297                       userSpecifiedMethod);
298        methodType = Amc_Block_c;
299      }
300    }
301  }
302 
303  amcInfo->methodType = methodType;
304
305
306  /*
307   * Every subsystem shares identical initial states.
308   * We do not abstract the state space. Only the transition relation is over or
309   * under approximated.
310   */
311  {
312    mdd_t               *sampleInitialStates;
313    Amc_SubsystemInfo_t *sampleSystem;
314
315    /*
316     * Fsm routines always returns duplicate copy.
317     */
318
319    sampleSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 0);
320    sampleInitialStates = Fsm_FsmComputeInitialStates(sampleSystem->fsm); 
321    amcInfo->initialStates = sampleInitialStates; 
322  }
323
324
325  /*
326   * Fill in the rest of amcInfo according to methodType.
327   */
328  switch(methodType) {
329    case Amc_Block_c:
330      amcInfo->methodData = NIL(void);
331      amcInfo->amcBoundProc = AmcBlockTearingProc;
332      amcInfo->amcFreeProc  = AmcFreeBlock;
333      break;
334/*
335 ;;The variable tearing method has not been implemented yet;;
336    case Amc_Variable_c:
337      amcInfo->methodData = AmcInfoInitializeVariable(amcInfo);
338      amcInfo->amcUpperBoundProc = AmcUpperBoundProcVariable;
339      amcInfo->amcLowerBoundProc = AmcLowerBoundProcVariable;
340      amcInfo->amcFreeProc = AmcFreeVariable;
341      break;
342*/
343    default:
344      fail("Invalid methodtype when initalizing amc method"); 
345  }
346
347  amcInfo->currentLevel = 0;
348
349  return(amcInfo);
350}
351
352
353/**Function********************************************************************
354
355  Synopsis    [Apply existential quantification over a subsystem.]
356
357  Description [Given a subsystem, the routine existentially quantify
358  the MDD variables from the transition relation of the subsystem.   
359  The return value is the resulting MDD. There are four quantification
360  modes;   
361  <dl>
362  <dt> Amc_PresentVars_c
363  <dd> Existentially quantify present state variables. <p>
364
365  <dt> Amc_NextVars_c
366  <dd> Existentially quantify next state variables. <p>
367 
368  <dt> Amc_InputVars_c
369  <dd> Existentially quantify input variables. <p>
370
371  <dt> Amc_User_c
372  <dd> Existentially quantify variables provide by the user. In this
373       mode user has to provide the array of MDD IDs to the function. If
374       the user does not provide the array of MDD IDs, the function just
375       returns the transition relation of the subsystem. <p>
376  </dl>]
377
378  SideEffects []
379
380  SeeAlso     [Amc_SubsystemInfo, AmcInitializeQuantifyVars]
381
382******************************************************************************/
383mdd_t *
384Amc_AmcExistentialQuantifySubsystem(
385  Amc_SubsystemInfo_t   *subSystem,
386  array_t               *quantifyVars,
387Amc_QuantificationMode  quantificationMode)
388{
389  Fsm_Fsm_t     *subSystemFsm   = AmcSubsystemReadFsm(subSystem);       
390  Ntk_Network_t *network        = Fsm_FsmReadNetwork(subSystemFsm);
391  mdd_manager   *mddManager     = Ntk_NetworkReadMddManager(network);
392  graph_t       *partition      = Part_NetworkReadPartition(network);
393
394  mdd_t         *result;
395
396  array_t       *transitionRelationArray = Amc_AmcSubsystemReadRelationArray(subSystem);
397
398  if( transitionRelationArray == NIL(array_t) ) { 
399    /* Build the transition relation of this subsystem. */
400    st_table    *vertexTable    = AmcSubsystemReadVertexTable(subSystem);
401    st_generator                *stGen;
402    char                        *latchName;
403
404    transitionRelationArray     = array_alloc(mdd_t *, 0);   
405    st_foreach_item(vertexTable, stGen, &latchName, NIL(char *)) {
406
407      Ntk_Node_t        *latch          = Ntk_NetworkFindNodeByName(network, latchName);
408      int               functionMddId   = Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch));
409
410      char      *nameLatchDataInput     = Ntk_NodeReadName(Ntk_LatchReadDataInput(latch));
411      vertex_t  *ptrVertex      = Part_PartitionFindVertexByName(partition, nameLatchDataInput);
412
413      Mvf_Function_t    *nextStateFunction;
414      mdd_t             *transitionRelation;
415      nextStateFunction         = Part_VertexReadFunction(ptrVertex);
416      transitionRelation        = Mvf_FunctionBuildRelationWithVariable(nextStateFunction,
417                                                                functionMddId);
418#ifdef AMC_DEBUG
419    {
420      int y, mddId; array_t *supportOfRelation;
421      fprintf(vis_stdout, "\nThe transition relation of the output function of the node : %s", latchName);
422      supportOfRelation = mdd_get_support(mddManager, transitionRelation);
423      arrayForEachItem(int, supportOfRelation, y, mddId) {
424        Ntk_Node_t *supportNode = Ntk_NetworkFindNodeByMddId(network, mddId);
425        fprintf(vis_stdout, "\n\tThe node in the support : %s", 
426                                       Ntk_NodeReadName(supportNode));
427      }
428    }
429#endif
430
431      if( nextStateFunction == NIL(Mvf_Function_t) ) {
432         error_append("** amc error: Build partition before running approximate model checker.");
433         return NIL(mdd_t);
434      }
435
436      array_insert_last(mdd_t *, transitionRelationArray, transitionRelation);
437    } /* end of st_foreach_item */
438
439    /* Cache the transition relation of the subsystem. */
440    Amc_AmcSubsystemSetRelationArray(subSystem, transitionRelationArray);
441
442  } /* end of transition relation construction. */
443
444
445  /*
446   * Notice : The present and next state variable of a subsystem is identical
447   * to that of the original system. The subsystem carries the subset of the
448   * output functions of the original system.
449   */
450  if( quantificationMode == Amc_User_c ) {
451    /* result = Img_MultiwayLinearAndSmooth(mddManager, transitionRelationArray, quantifyVars,
452                                         NIL(array_t)); */
453    if( AmcSubsystemReadNextStateVarSmoothen(subSystem) == NIL(mdd_t) ) {
454      result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, quantifyVars);
455      AmcSubsystemSetNextStateVarSmoothen(subSystem, result);
456    }
457    else {
458      result = AmcSubsystemReadNextStateVarSmoothen(subSystem);
459    }
460  }
461  else if( quantificationMode == Amc_PresentVars_c ) {
462    array_t     *presentVars    = Fsm_FsmReadPresentStateVars(subSystemFsm);
463    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, presentVars);
464  }
465  else if( quantificationMode == Amc_NextVars_c ) {
466    array_t     *nextVars       = Fsm_FsmReadNextStateVars(subSystemFsm);
467    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, nextVars);
468  }
469  else if( quantificationMode == Amc_InputVars_c ) {
470    array_t     *inputVars      = Fsm_FsmReadInputVars(subSystemFsm);
471    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, inputVars);
472  }
473  else {
474    error_append("** amc error: Invalid quantification mode.");
475    return NIL(mdd_t);
476  }
477
478
479  return(result);
480
481}
482
483/**Function********************************************************************
484
485  Synopsis    [Apply existential quantification to the array of subsystems.]
486
487  Description [Given an array of subsystems, the routine existentially
488  quantifies the MDD variables from the transition relations of the subsystems.
489  The existential quantification is applied to the subsystems that hasn't
490  yet been taken into the optimal system. The optimal system is the group
491  of subsystems that has been synchronously combined.
492  There are four quantification modes;
493  <dl>
494  <dt> Amc_PresentVars_c
495  <dd> Existentially quantify present state variables. <p>
496
497  <dt> Amc_NextVars_c
498  <dd> Existentially quantify next state variables. <p>
499 
500  <dt> Amc_InputVars_c
501  <dd> Existentially quantify input variables. <p>
502
503  <dt> Amc_User_c
504  <dd> Existentially quantify variables provide by the user. In this
505       mode user has to provide the array of MDD IDs to the function. If
506       the user does not provide the array of MDD IDs, the function just
507       returns the transition relation of the subsystem. <p>
508  </dl>
509  The return value is the array of quantified result of the MDD
510  representation of the transition relation.  ]
511 
512  SideEffects []
513
514  SeeAlso     [Amc_SubsystemInfo, Amc_AmcExistentialQuantifySubsystem]
515
516******************************************************************************/
517array_t *
518Amc_AmcExistentialQuantifySubsystemArray(
519  array_t                       *subSystemArray,
520  Amc_SubsystemInfo_t           *currentSystem,
521  array_t                       *quantifyVars,
522  Amc_QuantificationMode        quantificationMode)
523{
524  int i;
525  Amc_SubsystemInfo_t   *subSystem; 
526  mdd_t                 *quantifiedSystemMdd;
527  array_t               *quantifiedSystemMddArray = array_alloc(mdd_t *, 0);
528
529  if( (quantificationMode == Amc_User_c) && (quantifyVars == NIL(array_t)) ) {
530    error_append("** amc error: Subsystem has no output functions.");
531    return NIL(array_t);
532  }
533
534  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
535    if( (!subSystem->takenIntoOptimal) && (i != currentSystem->takenIntoOptimal) ) {
536
537      quantifiedSystemMdd =
538        Amc_AmcExistentialQuantifySubsystem(subSystem, quantifyVars, 
539                                            quantificationMode);
540      array_insert_last(mdd_t *, quantifiedSystemMddArray, quantifiedSystemMdd);
541    }
542  }
543
544  return(quantifiedSystemMddArray);
545
546}
547
548
549/**Function********************************************************************
550
551  Synopsis           [Read the fsm field of a Amc_SubsystemInfo]
552
553  SideEffects        []
554
555  SeeAlso            [Amc_SubsystemInfo]
556
557******************************************************************************/
558Fsm_Fsm_t *
559Amc_AmcSubsystemReadFsm(
560  Amc_SubsystemInfo_t *system)
561{
562  return AmcSubsystemReadFsm(system);
563} /* End of Amc_AmcSubsystemReadFsm */
564
565/**Function********************************************************************
566
567  Synopsis           [Set the fsm field of a Amc_SubsystemInfo]
568
569  SideEffects        []
570
571  SeeAlso            [Amc_SubsystemInfo_t]
572
573******************************************************************************/
574void
575Amc_AmcSubsystemSetFsm(
576  Amc_SubsystemInfo_t *system,
577  Fsm_Fsm_t *info)
578{
579  AmcSubsystemSetFsm(system, info);
580} /* End of Amc_AmcSubsystemReadFsm */
581
582
583/**Function********************************************************************
584
585  Synopsis           [Read the transition relation field of the
586  Amc_SubsystemInfo]
587
588  SideEffects        []
589
590  SeeAlso            [Amc_SubsystemInfo]
591
592******************************************************************************/
593array_t *
594Amc_AmcSubsystemReadRelationArray(
595  Amc_SubsystemInfo_t *system)
596{
597  return AmcSubsystemReadRelationArray(system);
598} /* End of Amc_AmcSubsystemReadTransitionRelation */
599
600/**Function********************************************************************
601
602  Synopsis           [Set the transition relation field of the
603  Amc_SubsystemInfo]
604
605  SideEffects        []
606
607  SeeAlso            [Amc_SubsystemInfo_t]
608
609******************************************************************************/
610void
611Amc_AmcSubsystemSetRelationArray(
612  Amc_SubsystemInfo_t   *system,
613  array_t               *info)
614{
615  AmcSubsystemSetRelationArray(system, info);
616} /* End of Amc_AmcSubsystemSetTransitionRelation */
617
618
619/**Function********************************************************************
620
621  Synopsis           [Read the nextStateVarSmoothen field of the
622  Amc_SubsystemInfo]
623
624  Description        [nextStateVarSmoothen field contains the MDD of the
625  transition relation with the next state variable existentially quantified.]
626
627  SideEffects        []
628
629  SeeAlso            [Amc_SubsystemInfo]
630
631******************************************************************************/
632mdd_t *
633Amc_AmcSubsystemReadNextStateVarSmoothen(
634  Amc_SubsystemInfo_t *system)
635{
636  return AmcSubsystemReadNextStateVarSmoothen(system);
637} /* End of Amc_AmcSubsystemReadNextStateVarSmooth */
638
639/**Function********************************************************************
640
641  Synopsis           [Set the nextStateVarSmoothen field of the
642  Amc_SubsystemInfo]
643
644  SideEffects        []
645
646  SeeAlso            [Amc_SubsystemInfo_t]
647
648******************************************************************************/
649void
650Amc_AmcSubsystemSetNextStateVarSmoothen(
651  Amc_SubsystemInfo_t   *system,
652  mdd_t                 *info)
653{
654  AmcSubsystemSetNextStateVarSmoothen(system, info);
655} /* End of Amc_AmcSubsystemSetNextStateVarSmooth */
656
657/**Function********************************************************************
658
659  Synopsis      [Read the satisfyStates field of the Amc_SubsystemInfo_t]
660
661  SideEffects   []
662
663  SeeAlso       [Amc_SubsystemInfo_t]
664
665******************************************************************************/
666mdd_t *
667Amc_AmcSubsystemReadSatisfy(
668  Amc_SubsystemInfo_t *system)
669{
670  return AmcSubsystemReadSatisfy(system);
671} /* End of Amc_AmcSubsystemReadSatisfy */
672
673/**Function********************************************************************
674
675  Synopsis      [Set the satisfyStates field of Amc_SubsystemInfo_t ]
676
677  Description   [satisfyStates field contains the MDD representation of the
678  super(sub)set of states satisfying given formula. The super(sub)set of states
679  satisfying given formula is obtained by utilizing the information of
680  the subsystem.]
681
682  SideEffects   []
683
684  SeeAlso       [Amc_SubsystemInfo_t]
685
686******************************************************************************/
687void
688Amc_AmcSubsystemSetSatisfy(
689  Amc_SubsystemInfo_t *system,
690  mdd_t *data)
691{
692  AmcSubsystemSetSatisfy(system, data);
693} /* End of Amc_AmcSubsystemSetSatisfy */
694
695/**Function********************************************************************
696
697  Synopsis      [Read the vertexTable field of the Amc_SubsystemInfo_t]
698
699  Description   [The vertexTable field of the subsystem is the hash table
700  of vertex names. Only the vertices contained in the subsystem is stored
701  in this table.]
702
703  SideEffects   []
704
705  SeeAlso       [Amc_SubsystemInfo_t]
706
707******************************************************************************/
708st_table *
709Amc_AmcSubsystemReadVertexTable(
710  Amc_SubsystemInfo_t *system)
711{
712  return AmcSubsystemReadVertexTable(system);
713} /* End of Amc_AmcSubsystemReadVertexTable */
714
715/**Function********************************************************************
716
717  Synopsis      [Set the vertexTable field of Amc_SubsystemInfo_t ]
718
719  SideEffects   []
720
721  SeeAlso       [Amc_SubsystemInfo_t]
722
723******************************************************************************/
724void
725Amc_AmcSubsystemSetVertexTable(
726  Amc_SubsystemInfo_t *system,
727  st_table *data)
728{
729  AmcSubsystemSetVertexTable(system, data);
730} /* End of Amc_AmcSubsystemSetVertexTable */
731
732/**Function********************************************************************
733
734  Synopsis      [Read the fanInTable field of the Amc_SubsystemInfo_t]
735
736  Description   [The fanInTable is the hash table of the subsystem index.
737  The subsystem index is the pointer value uniquely distinguishing subsystems.
738  The table contains the index of the subsystems whose component vertex
739  is one of the transitive fan-ins of the vertex in this subsystem.]
740
741  SideEffects   []
742
743  SeeAlso       [Amc_SubsystemInfo_t]
744
745******************************************************************************/
746st_table *
747Amc_AmcSubsystemReadFanInTable(
748  Amc_SubsystemInfo_t *system)
749{
750  return AmcSubsystemReadFanInTable(system);
751} /* End of Amc_AmcSubsystemReadFanInTable */
752
753/**Function********************************************************************
754
755  Synopsis      [Set the fanInTable field of Amc_SubsystemInfo_t ]
756
757  SideEffects   []
758
759  SeeAlso       [Amc_SubsystemInfo_t]
760
761******************************************************************************/
762void
763Amc_AmcSubsystemSetFanInTable(
764  Amc_SubsystemInfo_t *system,
765  st_table *data)
766{
767  AmcSubsystemSetFanInTable(system, data);
768} /* End of Amc_AmcSubsystemSetFanInTable */
769
770/**Function********************************************************************
771
772  Synopsis      [Read the fanOutTable field of the Amc_SubsystemInfo_t]
773
774  Description   [The fanOutTable is the hash table of the subsystem index.
775  The subsystem index is the pointer value uniquely distinguishing subsystems.
776  The table contains the index of the subsystems whose component vertex
777  is one of the transitive fan-outs of the vertex in this subsystem.]
778
779  SideEffects   []
780
781  SeeAlso       [Amc_SubsystemInfo_t]
782
783******************************************************************************/
784st_table *
785Amc_AmcSubsystemReadFanOutTable(
786  Amc_SubsystemInfo_t *system)
787{
788  return AmcSubsystemReadFanOutTable(system);
789} /* End of Amc_AmcSubsystemReadFanOutTable */
790
791/**Function********************************************************************
792
793  Synopsis      [Set the fanOutTable field of Amc_SubsystemInfo_t ]
794
795  SideEffects   []
796
797  SeeAlso       [Amc_SubsystemInfo_t]
798
799******************************************************************************/
800void
801Amc_AmcSubsystemSetFanOutTable(
802  Amc_SubsystemInfo_t *system,
803  st_table *data)
804{
805  AmcSubsystemSetFanOutTable(system, data);
806} /* End of Amc_AmcSubsystemSetFanOutTable */
807
808
809/**Function********************************************************************
810
811  Synopsis           [Read the MethodSpecific field of Amc_SubsystemInfo_t]
812
813  Description        [The method specific field may hold any value(s) that are
814  specific to the various methods.]
815
816  SideEffects        []
817
818  SeeAlso            [Amc_SubsystemInfo_t]
819
820******************************************************************************/
821char *
822Amc_AmcSubsystemReadMethodSpecificData(
823  Amc_SubsystemInfo_t *system)
824{
825  return AmcSubsystemReadMethodSpecificData(system);
826} /* End of Amc_AmcSubsystemReadMethodSpecificData */
827
828/**Function********************************************************************
829
830  Synopsis           [Set the MethodSpecific field of Amc_SubsystemInfo_t]
831
832  SideEffects        []
833
834  SeeAlso            [Amc_SubsystemInfo_t]
835
836******************************************************************************/
837void 
838Amc_AmcSubsystemSetMethodSpecificData(
839  Amc_SubsystemInfo_t *system,
840  char                *data)
841{
842  AmcSubsystemSetMethodSpecificData(system, data);
843} /* End of Amc_AmcSubsystemSetMethodSpecificData */
844
845
846
847/**Function********************************************************************
848
849  Synopsis      [Read the initial states from Amc_Info_t]
850
851  SideEffects   []
852
853  SeeAlso       [Amc_Info_t]
854
855******************************************************************************/
856mdd_t *
857Amc_AmcReadInitialStates(
858  Amc_Info_t *system)
859{
860  return AmcReadInitialStates(system);
861} /* End of Amc_AmcReadInitialStates */
862
863/**Function********************************************************************
864
865  Synopsis      [Sets the initial states from Amc_Info_t]
866
867  SideEffects   []
868
869  SeeAlso       [Amc_Info_t]
870
871******************************************************************************/
872void
873Amc_AmcSetInitialStates(
874  Amc_Info_t    *system,
875  mdd_t         *data)
876{
877  AmcSetInitialStates(system, data);
878} /* End of Amc_AmcSetInitialStates */
879
880/**Function********************************************************************
881
882  Synopsis      [Read the optimal system from Amc_Info_t]
883
884  SideEffects   []
885
886  SeeAlso       [Amc_Info_t]
887
888******************************************************************************/
889Amc_SubsystemInfo_t *
890Amc_AmcReadOptimalSystem(
891  Amc_Info_t *system)
892{
893  return AmcReadOptimalSystem(system);
894} /* End of Amc_AmcReadOptimalSystem */
895
896/**Function********************************************************************
897
898  Synopsis      [Sets the optimal system from Amc_Info_t]
899
900  SideEffects   []
901
902  SeeAlso       [Amc_Info_t]
903
904******************************************************************************/
905void
906Amc_AmcSetOptimalSystem(
907  Amc_Info_t *system,
908  Amc_SubsystemInfo_t    *data)
909{
910  AmcSetOptimalSystem(system, data);
911} /* End of Amc_AmcSetOptimalSystem */
912
913/**Function********************************************************************
914
915  Synopsis      [Read the MethodData from Amc_Info_t]
916
917  SideEffects   []
918
919  SeeAlso       [Amc_Info_t]
920
921******************************************************************************/
922void *
923Amc_AmcReadMethodData(
924  Amc_Info_t *system)
925{
926  return AmcReadMethodData(system);
927} /* End of Amc_AmcReadMethodData */
928
929/**Function********************************************************************
930
931  Synopsis      [Sets the MethodData from Amc_Info_t]
932
933  SideEffects   []
934
935  SeeAlso       [Amc_Info_t]
936
937******************************************************************************/
938void
939Amc_AmcSetMethodData(
940  Amc_Info_t    *system,
941  void          *data)
942{
943  AmcSetMethodData(system, data);
944} /* End of Amc_AmcSetMethodData */
945
946
947
948/**Function********************************************************************
949
950  Synopsis           [Allocate and initialize a Amc_SubsystemInfo_t]
951
952  SideEffects        []
953
954  SeeAlso            [Amc_AmcSubsystemFree]
955
956******************************************************************************/
957Amc_SubsystemInfo_t *
958Amc_AmcSubsystemAllocate(void)
959{
960  Amc_SubsystemInfo_t *result;
961
962  result = ALLOC(Amc_SubsystemInfo_t, 1);
963
964  return result;
965} /* End of Amc_SubsystemAllocate */
966
967
968/**Function********************************************************************
969
970  Synopsis           [Create a subsystem.]
971
972  Description        [Create and initialize a subsystem.]
973
974  SideEffects        []
975
976  SeeAlso            []
977
978******************************************************************************/
979Amc_SubsystemInfo_t *
980Amc_AmcSubsystemCreate(
981  Fsm_Fsm_t             *fsm,
982  mdd_t                 *satisfyStates,
983  st_table              *vertexTable,
984  st_table              *fanInTable,
985  st_table              *fanOutTable)
986{
987  Amc_SubsystemInfo_t *result;
988
989  result                        = ALLOC(Amc_SubsystemInfo_t, 1);
990  result->fsm                   = fsm;
991  result->relationArray         = NIL(array_t);
992  result->nextStateVarSmoothen  = NIL(mdd_t);
993  result->satisfyStates         = satisfyStates;
994  result->vertexTable           = vertexTable;
995  result->fanInTable            = fanInTable;
996  result->fanOutTable           = fanOutTable;
997  result->takenIntoOptimal      = 0;  /* Initialize to 0 */
998  result->methodSpecificData    = NIL(char);
999
1000  return result;
1001} 
1002
1003/**Function********************************************************************
1004
1005  Synopsis           [Duplicate a subsystem.]
1006
1007  SideEffects        []
1008
1009  SeeAlso            [Amc_AmcSubsystemAllocate]
1010
1011******************************************************************************/
1012Amc_SubsystemInfo_t *
1013Amc_AmcSubsystemDuplicate(
1014  Ntk_Network_t       *network, 
1015  Amc_SubsystemInfo_t *subSystem)
1016{
1017  Fsm_Fsm_t     *fsm;
1018  mdd_t         *satisfyStates  = NIL(mdd_t);
1019  st_table      *vertexTable    = NIL(st_table);
1020  st_table      *fanInTable     = NIL(st_table);
1021  st_table      *fanOutTable    = NIL(st_table);
1022  graph_t       *partition      = Part_NetworkReadPartition(network);
1023
1024  if(subSystem->satisfyStates != NIL(mdd_t)) {
1025    satisfyStates = mdd_dup(subSystem->satisfyStates);
1026  }
1027  if(subSystem->vertexTable != NIL(st_table)) {
1028    vertexTable = st_copy(subSystem->vertexTable);
1029  }
1030  if(subSystem->fanInTable != NIL(st_table)) {
1031    fanInTable = st_copy(subSystem->fanInTable);
1032  }
1033  if(subSystem->fanOutTable != NIL(st_table)) {
1034    fanOutTable = st_copy(subSystem->fanOutTable);
1035  }
1036
1037  fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
1038        FALSE, 0);
1039
1040  return(Amc_AmcSubsystemCreate(fsm, satisfyStates, vertexTable, fanInTable, fanOutTable));
1041}
1042
1043
1044
1045/**Function********************************************************************
1046
1047  Synopsis           [Free a subsystem.]
1048
1049  Description        [Frees a subsystem plus associated fields except the
1050  partition. This is to reuse the partition without recreating it.]
1051
1052  SideEffects        []
1053
1054  SeeAlso            [Amc_AmcSubsystemAllocate]
1055
1056******************************************************************************/
1057void
1058Amc_AmcSubsystemFree(
1059  Amc_SubsystemInfo_t *subSystem)
1060{
1061  st_table      *vertexTable;
1062  st_table      *fanInTable, *fanOutTable;
1063
1064  /* Do not free partition associated to this fsm */
1065  if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
1066    Fsm_FsmSubsystemFree(AmcSubsystemReadFsm(subSystem));
1067  } 
1068
1069  if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
1070    array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
1071    mdd_t   *transitionRelation;
1072    int         i;
1073    arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
1074      mdd_free(transitionRelation); 
1075    } 
1076    array_free(transitionRelationArray);
1077  }
1078
1079  if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
1080    mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
1081  }
1082
1083  if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
1084    mdd_free(AmcSubsystemReadSatisfy(subSystem));
1085  } 
1086
1087  /* Do not free vertex!! */
1088  vertexTable = AmcSubsystemReadVertexTable(subSystem);
1089  if (vertexTable != NIL(st_table)) {
1090    st_free_table(vertexTable);
1091  }
1092
1093  fanInTable = AmcSubsystemReadFanInTable(subSystem);
1094  if (fanInTable != NIL(st_table)) {
1095    st_free_table(fanInTable);
1096  }
1097
1098  fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
1099  if (fanOutTable != NIL(st_table)) {
1100    st_free_table(fanOutTable);
1101  }
1102
1103
1104  FREE(subSystem);
1105} 
1106
1107/**Function********************************************************************
1108
1109  Synopsis           [Free a subsystem.]
1110
1111  Description        [Frees a subsystem including the associated partition.]
1112
1113  SideEffects        []
1114
1115  SeeAlso            [Amc_AmcSubsystemAllocate]
1116
1117******************************************************************************/
1118void
1119Amc_AmcSubsystemFreeAlsoPartition(
1120  Amc_SubsystemInfo_t *subSystem)
1121{
1122  st_table      *vertexTable;
1123  st_table      *fanInTable, *fanOutTable;
1124
1125  /* Do not free partition associated to this fsm */
1126  if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
1127    Fsm_FsmFree(AmcSubsystemReadFsm(subSystem));
1128  } 
1129
1130  if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
1131    array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
1132    mdd_t   *transitionRelation;
1133    int         i;
1134    arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
1135      mdd_free(transitionRelation); 
1136    } 
1137    array_free(transitionRelationArray);
1138  }
1139
1140  if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
1141    mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
1142  }
1143
1144  if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
1145    mdd_free(AmcSubsystemReadSatisfy(subSystem));
1146  } 
1147
1148  /* Do not free vertex!! */
1149  vertexTable = AmcSubsystemReadVertexTable(subSystem);
1150  if (vertexTable != NIL(st_table)) {
1151    st_free_table(vertexTable);
1152  }
1153
1154  fanInTable = AmcSubsystemReadFanInTable(subSystem);
1155  if (fanInTable != NIL(st_table)) {
1156    st_free_table(fanInTable);
1157  }
1158
1159  fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
1160  if (fanOutTable != NIL(st_table)) {
1161    st_free_table(fanOutTable);
1162  }
1163
1164
1165  FREE(subSystem);
1166} 
1167
1168
1169
1170
1171/**Function********************************************************************
1172
1173  Synopsis           [Combine two subsystems and return the resulting
1174  subsystem.]
1175
1176  Description        [Take the synchronous product of two subsystems. The routine
1177  returns resulting subsystem. If either one of the subsystem is NIL return
1178  the other. It is an error to pass two NIL pointers. Either one has to be
1179  a subsystem.]
1180
1181  SideEffects        []
1182
1183  SeeAlso            []
1184
1185******************************************************************************/
1186Amc_SubsystemInfo_t *
1187Amc_CombineSubsystems(
1188  Ntk_Network_t         *network,
1189  Amc_SubsystemInfo_t   *subSystem1,
1190  Amc_SubsystemInfo_t   *subSystem2)
1191{
1192  Amc_SubsystemInfo_t   *subSystemInfo;
1193  Amc_SubsystemInfo_t   *subSystem;
1194  st_table              *vertexTable, *vertexTable1, *vertexTable2;
1195  st_table              *fanInTable = NIL(st_table);
1196  st_table              *fanOutTable = NIL(st_table);
1197  st_table              *fanInTable1, *fanInTable2;
1198  st_table              *fanOutTable1, *fanOutTable2;
1199  Ntk_Node_t            *latch; 
1200  graph_t               *partition = Part_NetworkReadPartition(network);
1201  Fsm_Fsm_t             *fsm;
1202  lsGen                 gen;
1203  st_generator          *stGen;
1204
1205  /* If two subsystem are identical return error */
1206  if(subSystem1 == subSystem2) {
1207    error_append("** amc error: illegal subsystem combination");
1208    return NIL(Amc_SubsystemInfo_t);
1209  }
1210  /* If two subsystem are NIL return error */
1211  if( (subSystem1 == NIL(Amc_SubsystemInfo_t)) && 
1212      (subSystem2 == NIL(Amc_SubsystemInfo_t)) ) {
1213    error_append("** amc error: illegal subsystem combination");
1214    return NIL(Amc_SubsystemInfo_t);
1215  }
1216
1217  /* If either of two subsystem is NIL return copy of the other */
1218  if(subSystem1 == NIL(Amc_SubsystemInfo_t)) {
1219    return Amc_AmcSubsystemDuplicate(network, subSystem2);
1220  }
1221  if(subSystem2 == NIL(Amc_SubsystemInfo_t)) {
1222    return Amc_AmcSubsystemDuplicate(network, subSystem1);
1223  }
1224
1225  vertexTable  = st_init_table(strcmp, st_strhash); 
1226  vertexTable1 = AmcSubsystemReadVertexTable(subSystem1);
1227  vertexTable2 = AmcSubsystemReadVertexTable(subSystem2);
1228
1229  Ntk_NetworkForEachLatch(network, gen, latch) {
1230    char *latchName = Ntk_NodeReadName(latch);
1231    if( st_lookup(vertexTable1, latchName, (char **)0) || 
1232        st_lookup(vertexTable2, latchName, (char **)0) ) {
1233
1234      st_insert(vertexTable, latchName, (char *)0);
1235
1236    }
1237  } /* end of Ntk_NetworkForEachLatch */
1238
1239
1240  fanInTable1 = AmcSubsystemReadFanInTable(subSystem1);
1241  fanInTable2 = AmcSubsystemReadFanInTable(subSystem2);
1242  if( (fanInTable1 != NIL(st_table)) && (fanInTable2 != NIL(st_table)) ) { 
1243
1244    fanInTable  = st_init_table(st_ptrcmp, st_ptrhash); 
1245
1246    st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
1247      st_insert(fanInTable, (char *)subSystem, (char *)0);
1248    }
1249    st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
1250      st_insert(fanInTable, (char *)subSystem, (char *)0);
1251    }
1252  }
1253
1254
1255  fanOutTable1 = AmcSubsystemReadFanOutTable(subSystem1);
1256  fanOutTable2 = AmcSubsystemReadFanOutTable(subSystem2);
1257
1258  if( (fanOutTable1 != NIL(st_table)) && (fanOutTable2 != NIL(st_table)) ) { 
1259
1260    fanOutTable  = st_init_table(st_ptrcmp, st_ptrhash); 
1261
1262    st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
1263      st_insert(fanOutTable, subSystem, (char *)0);
1264    }
1265    st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
1266      st_insert(fanOutTable, subSystem, (char *)0);
1267    }
1268  }
1269
1270
1271  fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
1272        FALSE, 0);
1273
1274  subSystemInfo = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable, 
1275                                            fanInTable, fanOutTable);
1276
1277  /* Does not free tables */
1278
1279  return(subSystemInfo);
1280}
1281
1282#ifdef AMC_DEBUG_
1283/**Function********************************************************************
1284
1285  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
1286  necessary.]
1287
1288  Description [_Obsolete_]
1289
1290  SideEffects []
1291
1292  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]
1293
1294******************************************************************************/
1295Img_ImageInfo_t *
1296Amc_AmcReadOrCreateImageInfo(
1297  Fsm_Fsm_t *fsm)
1298{
1299  Img_ImageInfo_t *imageInfo;
1300  if( Fsm_FsmReadImageInfo(fsm) == NIL(Img_ImageInfo_t)) {
1301    array_t *dummyInputVars     = array_alloc(int, 0);
1302    imageInfo = Img_ImageInfoInitialize(Fsm_FsmReadPartition(fsm),
1303                                        Fsm_FsmReadNextStateFunctions(fsm),
1304                                        Fsm_FsmReadPresentStateVars(fsm),
1305                                        Fsm_FsmReadNextStateVars(fsm),
1306                                        dummyInputVars,
1307                                        Fsm_FsmReadNetwork(fsm),
1308                                        Img_Default_c, Img_Both_c);
1309    Fsm_FsmSetImageInfo(fsm, imageInfo);
1310    array_free(dummyInputVars);
1311  }
1312  return (imageInfo);
1313}
1314#endif
1315
1316/**Function********************************************************************
1317
1318  Synopsis    [Model check formula with approxmiations.]
1319
1320  Description [The routine evaluates given formula with approximations.]
1321 
1322  Comment     []
1323
1324  SideEffects []
1325
1326******************************************************************************/
1327mdd_t * 
1328Amc_AmcEvaluateCTLFormula(
1329  Amc_SubsystemInfo_t   *subSystem,
1330  array_t               *subSystemArray,
1331  Ctlp_Formula_t        *ctlFormula, 
1332  mdd_t                 *fairStates, 
1333  Fsm_Fairness_t        *fairCondition, 
1334  mdd_t                 *modelCareStates,
1335  boolean               lowerBound,
1336  array_t               *quantifyVars,
1337  Mc_VerbosityLevel     verbosity,
1338  Mc_DcLevel            dcLevel )
1339{
1340  Fsm_Fsm_t     *modelFsm = Amc_AmcSubsystemReadFsm(subSystem);
1341
1342  mdd_t  *leftMdd  = NIL(mdd_t);
1343  mdd_t  *rightMdd = NIL(mdd_t);
1344  mdd_t  *result   = NIL(mdd_t);
1345  mdd_t  *tmpResult = NIL(mdd_t);
1346
1347  mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates(ctlFormula );
1348  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
1349  mdd_t *careStates = NIL(mdd_t);
1350 
1351
1352  if (ctlFormulaStates) {
1353    return ctlFormulaStates;
1354  }
1355 
1356  { 
1357    Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
1358    if (leftChild) {
1359      leftMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, leftChild, fairStates, fairCondition, 
1360                                   modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel); 
1361      if (!leftMdd) 
1362        return NIL(mdd_t);
1363    }
1364  }
1365
1366  {
1367    Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
1368    if (rightChild) {
1369      rightMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, rightChild, fairStates, fairCondition, 
1370                                    modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel);
1371      if (!rightMdd ) 
1372        return NIL(mdd_t);
1373    }
1374  }
1375
1376  careStates = (modelCareStates != NIL(mdd_t)) ?  mdd_dup(modelCareStates) : mdd_one(mddMgr);
1377  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
1378
1379    case Ctlp_ID_c : tmpResult = AmcModelCheckAtomicFormula( modelFsm, ctlFormula ); 
1380
1381       /* #AMC : Obtain lowerbound of the constraint set. */
1382      if(0 && lowerBound) { /*Chao: this is not correct! consider !EF(!p) */
1383        array_t *quantifyPresentVars     = array_fetch(array_t *, quantifyVars, 0);
1384        int     numOfPresentQuantifyVars = array_n(quantifyPresentVars);
1385        /*
1386         * Currently VIS does not allow primary input as the variable of
1387         * the atomic propositions.
1388         */
1389        if(numOfPresentQuantifyVars > 0) {
1390           result = mdd_consensus(mddMgr, tmpResult, quantifyPresentVars); 
1391           mdd_free(tmpResult);
1392        }
1393        else
1394           result = tmpResult;
1395        }
1396      else
1397        result = tmpResult;
1398
1399      break;
1400
1401    case Ctlp_TRUE_c : result = mdd_one( mddMgr ); break;
1402    case Ctlp_FALSE_c : result = mdd_zero( mddMgr ); break;
1403
1404    case Ctlp_NOT_c : result = mdd_not( leftMdd ); break;
1405    case Ctlp_EQ_c : result = mdd_xnor( leftMdd, rightMdd ); break;
1406    case Ctlp_XOR_c : result = mdd_xor( leftMdd, rightMdd ); break;
1407    case Ctlp_THEN_c : result = mdd_or( leftMdd, rightMdd, 0, 1 ); break;
1408    case Ctlp_AND_c: result = mdd_and( leftMdd, rightMdd, 1, 1 ); break;
1409    case Ctlp_OR_c: result = mdd_or( leftMdd, rightMdd, 1, 1 ); break;
1410
1411    case Ctlp_EX_c: 
1412      result = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, leftMdd, fairStates, 
1413                                        careStates, lowerBound, quantifyVars, verbosity, dcLevel );
1414      break;
1415
1416    case Ctlp_EU_c: {
1417      array_t *onionRings = array_alloc( mdd_t *, 0 );
1418      result = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, leftMdd, rightMdd, fairStates, 
1419                                    careStates, onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
1420      Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) onionRings, McFormulaFreeDebugData); 
1421      break;
1422    }
1423
1424    case Ctlp_EG_c: {
1425      array_t *arrayOfOnionRings = array_alloc( array_t *, 0 );
1426      result = Amc_AmcEvaluateEGFormula( modelFsm, subSystemArray, subSystem, leftMdd, 
1427                                        fairStates, fairCondition, careStates, 
1428                                        arrayOfOnionRings, lowerBound, quantifyVars, verbosity, dcLevel );
1429      Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) arrayOfOnionRings, McFormulaFreeDebugData); 
1430      break;
1431    }
1432
1433    default: fail("Encountered unknown type of CTL formula\n");
1434  }
1435
1436
1437  Ctlp_FormulaSetStates( ctlFormula, result );
1438
1439  mdd_free( careStates );
1440  return result;
1441}
1442
1443/**Function********************************************************************
1444
1445  Synopsis      [Evaluate EX formula with approximations.]
1446
1447  Description   [The routine evaluates EX formula with approximations. The
1448  routine is used both to obtain lower- and upper- bound of the exact preimage.
1449
1450  Chao: Let's use the following symbols to represent the present-state vars,
1451  next-state vars, and the input vars:
1452    s        -- Present-State Vars
1453    t        -- Next-State Vars
1454    x        -- Input Vars
1455    s_A,t_A  -- PS or NS vars in the abstract model
1456    s_R,t_R  -- PS or NS vars in the remaining models
1457    T        -- Transition Relation of the concrete model, T = T_A * T_R
1458    T_A,T_R  -- TR of the abstract model or the remaining models
1459 
1460  The upper-bound EX computation is
1461    \exist  (s_R) ( \exist (t,x)   (T_A(s,x,t_A)  * C(t))                )
1462
1463  The lower-bound EX computation is
1464    \forall (s_R) ( \exist (t_A,x) ( T_A(s,x,t_A) * (\forall (t_R) C(t)) )
1465  ]
1466
1467  SideEffects   []
1468
1469  SeeAlso       [AmcInitializeQuantifyVars]
1470
1471******************************************************************************/
1472
1473mdd_t *
1474Amc_AmcEvaluateEXFormula(
1475  Fsm_Fsm_t             *modelFsm,
1476  array_t               *subSystemArray, 
1477  Amc_SubsystemInfo_t   *subSystem,
1478  mdd_t                 *targetMdd,
1479  mdd_t                 *fairStates,
1480  mdd_t                 *careStates,
1481  boolean               lowerBound,
1482  array_t               *quantifyVars,
1483  Mc_VerbosityLevel     verbosity,
1484  Mc_DcLevel            dcLevel )
1485{
1486  /*
1487   * The care set consists of the passed careStates
1488   */
1489  mdd_t *toCareSet = mdd_dup( careStates );
1490
1491  mdd_t *fromLowerBound;
1492  mdd_t *fromUpperBound;
1493  mdd_t *result = NIL(mdd_t);
1494  mdd_t *tmpResult;
1495  mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
1496  array_t *quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
1497 
1498  Img_ImageInfo_t * imageInfo;
1499
1500  assert(quantifyPresentVars != NIL(array_t));
1501
1502  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 1);
1503
1504  if ( dcLevel == McDcLevelRchFrontier_c ) {
1505    /*
1506     * The lower bound is the conjunction of the fair states,
1507     * the target states, and the care states.
1508     */
1509    mdd_t *tmpMdd = mdd_and( targetMdd, fairStates, 1, 1 );
1510    fromLowerBound = mdd_and( tmpMdd, careStates, 1, 1 );
1511    mdd_free( tmpMdd );
1512    /*
1513     * The upper bound is the OR of the lower bound with the
1514     * complement of the care states.
1515     */
1516    fromUpperBound = mdd_or( fromLowerBound, careStates, 1, 0 );
1517  }
1518  else {
1519    /*
1520     * The lower bound is the conjunction of the fair states,
1521     * and the target states.
1522     */
1523    fromLowerBound = mdd_and( targetMdd, fairStates, 1, 1 );
1524    /*
1525     * The upper bound is the same as the lower bound.
1526     */
1527    fromUpperBound = mdd_dup( fromLowerBound );
1528  }
1529
1530
1531  /***************************************************************************
1532   * compute C1(s) =
1533   *    C(s)                         for upper-bound EX computation
1534   *    ( \forall (s_R) C(s) )       for lower-bound EX computation
1535   ***************************************************************************/
1536  if (lowerBound) {
1537      mdd_t *mdd1, *mdd2;
1538      mdd1 = fromLowerBound;
1539      mdd2 = fromUpperBound;
1540      if (array_n(quantifyPresentVars) > 0) {
1541        fromLowerBound = mdd_consensus(mddManager, fromLowerBound,
1542                                       quantifyPresentVars);
1543      } else {
1544        fromLowerBound = mdd_dup(fromLowerBound);
1545      }
1546      if (mdd_equal(mdd1, mdd2)) {
1547        fromUpperBound = mdd_dup(fromLowerBound);
1548      }else {
1549        if (array_n(quantifyPresentVars) > 0) {
1550          fromUpperBound = mdd_consensus(mddManager, fromUpperBound,
1551                                         quantifyPresentVars);
1552        } else {
1553          fromUpperBound = mdd_dup(fromUpperBound);
1554        }
1555      }
1556      mdd_free(mdd1);
1557      mdd_free(mdd2);
1558  }
1559
1560  /***************************************************************************
1561   * Compute \exist (t,x) ( T_A(s,x,t_A) * C1(t) ), where
1562   *    C1(t) = C(t)                      for upper-bound EX
1563   *    C1(t) = (\forall (t_R) C(t) )     for lower-bound EX
1564   ***************************************************************************/
1565  tmpResult = Img_ImageInfoComputeBwdWithDomainVars( imageInfo,
1566                                                     fromLowerBound,
1567                                                     fromUpperBound,
1568                                                     toCareSet );
1569
1570  /***************************************************************************
1571   * Compute the final result
1572   *    \exist  (s_R)  (tmpResult(s))      for upper-bound EX
1573   *    \forall (s_R)  (tmpResult(s))      for lower-bound EX
1574   **************************************************************************/
1575  if (lowerBound) {
1576    if (array_n(quantifyPresentVars) > 0) {
1577      result = mdd_consensus(mddManager, tmpResult, quantifyPresentVars);
1578    } else {
1579      result = mdd_dup(tmpResult);
1580    }
1581  }else {
1582    result = mdd_dup(tmpResult);
1583    /*  result = mdd_smooth(mddManager, tmpResult, quantifyPresentVars);*/
1584  } 
1585  mdd_free(tmpResult);
1586 
1587  mdd_free( fromLowerBound );
1588  mdd_free( fromUpperBound );
1589  mdd_free( toCareSet );
1590
1591  if ( verbosity == McVerbosityMax_c ) {
1592    static int refCount = 0;
1593    mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
1594    array_t *psVars     = Fsm_FsmReadPresentStateVars( modelFsm );
1595    mdd_t *tmpMdd = careStates ? mdd_and( result, careStates, 1, 1 ) : mdd_dup( result );
1596    fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount, mdd_size( result ) );
1597    fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n", 
1598            mdd_count_onset(  mddMgr, tmpMdd, psVars ) ); 
1599    mdd_free(tmpMdd);
1600  }
1601
1602  return result;
1603}
1604
1605#if 0
1606/* this is the original (buggy) version */
1607mdd_t *
1608Amc_AmcEvaluateEXFormula_Old(
1609  Fsm_Fsm_t             *modelFsm,
1610  array_t               *subSystemArray,
1611  Amc_SubsystemInfo_t   *subSystem,
1612  mdd_t                 *targetMdd,
1613  mdd_t                 *fairStates,
1614  mdd_t                 *careStates,
1615  boolean               lowerBound,
1616  array_t               *quantifyVars,
1617  Mc_VerbosityLevel     verbosity,
1618  Mc_DcLevel            dcLevel )
1619{
1620  /*
1621   * The care set consists of the passed careStates
1622   */
1623  mdd_t *toCareSet = mdd_dup( careStates );
1624
1625  mdd_t *fromLowerBound;
1626  mdd_t *fromUpperBound;
1627  mdd_t *result = NIL(mdd_t);
1628  mdd_t *tmpResult;
1629
1630  Img_ImageInfo_t * imageInfo;
1631
1632  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 1);
1633
1634  /*
1635   * this condition will never  be true; we didnt find it to be
1636   * especially effective, are avoiding using it for now. later
1637   * we may add a McDcLevelMax+1 field which will allow us to use it
1638   *
1639   */
1640  if ( dcLevel > McDcLevelRchFrontier_c ) {
1641    /*
1642     * The lower bound is the conjunction of the fair states,
1643     * the target states, and the care states.
1644     */
1645    mdd_t *tmpMdd = mdd_and( targetMdd, fairStates, 1, 1 );
1646    fromLowerBound = mdd_and( tmpMdd, careStates, 1, 1 );
1647    mdd_free( tmpMdd );
1648    /*
1649     * The upper bound is the OR of the lower bound with the
1650     * complement of the care states.
1651     */
1652    fromUpperBound = mdd_or( fromLowerBound, careStates, 1, 0 );
1653  }
1654  else {
1655    /*
1656     * The lower bound is the conjunction of the fair states,
1657     * and the target states.
1658     */
1659    fromLowerBound = mdd_and( targetMdd, fairStates, 1, 1 );
1660    /*
1661     * The upper bound is the same as the lower bound.
1662     */
1663    fromUpperBound = mdd_dup( fromLowerBound );
1664  }
1665
1666  /* #AMC : */
1667#ifdef AMC_DEBUG
1668  if(lowerBound) {
1669    /*
1670     * Sanity check. The set to compute a preimage from should only contain the present
1671     * state variables of the subsystem.
1672     */
1673    {
1674      mdd_manager       *mddManager     = Fsm_FsmReadMddManager( modelFsm );
1675      Ntk_Network_t     *network        = Fsm_FsmReadNetwork(modelFsm);
1676      array_t           *supportArray   = mdd_get_support(mddManager, fromLowerBound);
1677      st_table          *vertexTable    = Amc_AmcSubsystemReadVertexTable(subSystem);
1678      int               i, varId;
1679
1680      fprintf(vis_stdout, "\n#AMC : Sanity check of the support of the constraint set");
1681      arrayForEachItem(int, supportArray, i, varId) {
1682        Ntk_Node_t  *node = Ntk_NetworkFindNodeByMddId(network, varId);
1683        char *latchName = Ntk_NodeReadName(node);
1684        fprintf(vis_stdout, "\n#  fromLowerBound -- Node : %s", latchName);
1685      }
1686
1687      arrayForEachItem(int, supportArray, i, varId) {
1688        char *latchName = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(network, varId));
1689        if( !st_lookup(vertexTable, latchName, (char **)0 )) {
1690          fprintf(vis_stdout, "\n** amc error : Whoops!! Something's wrong in lowerbound routine.");
1691          fflush(vis_stdout);
1692        }
1693      } /* end of arrayForEachItem */
1694    }
1695  } /* end of if(lowerBound) */
1696#endif
1697
1698  tmpResult = Img_ImageInfoComputeBwdWithDomainVars( imageInfo,
1699                                                     fromLowerBound,
1700                                                     fromUpperBound,
1701                                                     toCareSet );
1702#ifdef AMC_DEBUG
1703    {
1704      Ntk_Network_t     *network        = Fsm_FsmReadNetwork(modelFsm);
1705      mdd_manager       *mddManager     = Fsm_FsmReadMddManager( modelFsm );
1706      array_t           *supportArray   = mdd_get_support(mddManager, tmpResult);
1707      int               i, varId;
1708
1709      fprintf(vis_stdout, "\n#AMC : Sanity check of the support of the preimage");
1710      arrayForEachItem(int, supportArray, i, varId) {
1711        Ntk_Node_t  *node = Ntk_NetworkFindNodeByMddId(network, varId);
1712        char *latchName = Ntk_NodeReadName(node);
1713        fprintf(vis_stdout, "\n## The preimage contains the node : %s", latchName);
1714        if( Ntk_NodeTestIsLatch(node) )
1715          fprintf(vis_stdout, "\n##  The node is a latch");
1716        else
1717          fprintf(vis_stdout, "\n##  The node is not a latch");
1718
1719      } /* end of arrayForEachItem */
1720    }
1721#endif
1722
1723  /* #AMC : */
1724  if(lowerBound) {
1725    mdd_manager *mddManager       = Fsm_FsmReadMddManager( modelFsm );
1726    array_t     *quantifyNextVars = array_fetch(array_t *, quantifyVars, 1);
1727    array_t     *exQuantifiedSystemMddArray;
1728
1729    /*
1730     * Existential abstraction of next state variables from subsystems that are
1731     * not currently in consideration. Each subsystem has disjoint next state
1732     * functions, hence we distribute existential abstraction over subsystems.
1733     */
1734
1735    exQuantifiedSystemMddArray =
1736      Amc_AmcExistentialQuantifySubsystemArray(subSystemArray, subSystem,
1737                                               quantifyNextVars, Amc_User_c);
1738
1739    /*
1740     * Universal abstraction of present state and input variables from
1741     * subsystems that are not currently in consideration.
1742     */
1743    {
1744      array_t   *quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
1745      array_t   *quantifyInputVars   = array_fetch(array_t *, quantifyVars, 2);
1746      array_t   *consensusVarArray   = array_join(quantifyPresentVars,
1747                                                  quantifyInputVars);
1748      mdd_t     *interResult         = mdd_one( mddManager );
1749      mdd_t     *subMdd;
1750      int       i;
1751
1752      array_insert_last(mdd_t *, exQuantifiedSystemMddArray, tmpResult);
1753      arrayForEachItem(mdd_t *, exQuantifiedSystemMddArray, i, subMdd) {
1754        mdd_t *cResult = mdd_consensus(mddManager, subMdd, consensusVarArray);
1755        result = mdd_and(cResult, interResult, 1, 1);
1756        mdd_free(cResult); mdd_free(interResult);
1757        interResult = result;
1758
1759        if( mdd_is_tautology(result, 0) ) break;
1760      }
1761
1762      mdd_free(tmpResult);
1763      /* Do not free Mdds. These are cached. */
1764      array_free(exQuantifiedSystemMddArray);
1765      array_free(consensusVarArray);
1766    }
1767
1768
1769  } /* end of if(lowerBound) */
1770  else {
1771   result = tmpResult;
1772  } /* end of #AMC insertion */
1773
1774  mdd_free( fromLowerBound );
1775  mdd_free( fromUpperBound );
1776  mdd_free( toCareSet );
1777
1778  if ( verbosity == McVerbosityMax_c ) {
1779    static int refCount = 0;
1780    mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
1781    array_t *psVars     = Fsm_FsmReadPresentStateVars( modelFsm );
1782    mdd_t *tmpMdd = careStates ? mdd_and( result, careStates, 1, 1 ) : mdd_dup( result );
1783    fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount, mdd_size( result ) );
1784    fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n",
1785            mdd_count_onset(  mddMgr, tmpMdd, psVars ) );
1786    mdd_free(tmpMdd);
1787  }
1788
1789  return result;
1790}
1791#endif
1792
1793/**Function********************************************************************
1794
1795  Synopsis    [Evaluate EU formula with approximations.]
1796
1797  Description []
1798
1799  Comment     []
1800
1801  SideEffects []
1802
1803******************************************************************************/
1804mdd_t *
1805Amc_AmcEvaluateEUFormula( 
1806  Fsm_Fsm_t *modelFsm,
1807  array_t   *subSystemArray, 
1808  Amc_SubsystemInfo_t   *subSystem,
1809  mdd_t *invariantMdd,
1810  mdd_t *targetMdd,
1811  mdd_t *fairStates,
1812  mdd_t *careStates,
1813  array_t *onionRings,
1814  boolean lowerBound,
1815  array_t *quantifyVars,
1816  Mc_VerbosityLevel verbosity,
1817  Mc_DcLevel dcLevel )
1818{
1819  mdd_t *aMdd;
1820  mdd_t *bMdd;
1821  mdd_t *cMdd;
1822  mdd_t *resultMdd = mdd_and( targetMdd, fairStates, 1, 1 );
1823  mdd_t *ringMdd   = mdd_dup( resultMdd ); 
1824
1825  while (TRUE) { 
1826
1827    if ( onionRings ) {
1828      array_insert_last( mdd_t *, onionRings, mdd_dup( resultMdd ) );
1829    }
1830
1831    /*
1832     * When trying to use dont cares to the hilt,
1833     * use a bdd between succ iterations -> ringMdd
1834     */
1835    aMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, ringMdd, fairStates, careStates,
1836                                    lowerBound, quantifyVars, verbosity, dcLevel ); 
1837    mdd_free( ringMdd );
1838    bMdd = mdd_and( aMdd, invariantMdd, 1, 1 ); 
1839    cMdd = mdd_or( resultMdd, bMdd, 1, 1 ); 
1840
1841    mdd_free( aMdd );
1842    mdd_free( bMdd );
1843
1844    if ( mdd_equal_mod_care_set( cMdd, resultMdd, careStates ) ) {
1845      mdd_free( cMdd );
1846      break;
1847    }
1848
1849    if ( dcLevel >= McDcLevelRchFrontier_c ) {
1850      mdd_t *tmpMdd = mdd_and( resultMdd, cMdd, 0, 1 );
1851      ringMdd = bdd_between( tmpMdd, cMdd );
1852      if ( verbosity == McVerbosityMax_c ) {
1853        fprintf(vis_stdout, "-- EU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n", 
1854                mdd_size( tmpMdd ), mdd_size( resultMdd ), mdd_size( ringMdd ) );
1855      }
1856      mdd_free( tmpMdd );
1857    }
1858    else {
1859      ringMdd = mdd_dup( cMdd );
1860      if ( verbosity == McVerbosityMax_c ) {
1861        fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size( ringMdd ) );
1862      }
1863    }
1864
1865    mdd_free( resultMdd );
1866    resultMdd = cMdd;
1867
1868  }
1869
1870  if ( ( verbosity == McVerbosityMax_c ) ) {
1871    static int refCount=0;
1872    mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
1873    array_t *psVars     = Fsm_FsmReadPresentStateVars( modelFsm );
1874    mdd_t *tmpMdd = careStates ? mdd_and( resultMdd, careStates, 1, 1 ) : mdd_dup( resultMdd );
1875    fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount, mdd_size( resultMdd ) );
1876    fprintf(vis_stdout, "--There are %.0f care states satisfying EU formula\n", 
1877            mdd_count_onset(  mddMgr, tmpMdd, psVars ) );
1878    mdd_free(tmpMdd);
1879  }
1880
1881  return resultMdd;
1882}
1883
1884/**Function********************************************************************
1885
1886  Synopsis    [Evaluate EG formula with approximations.]
1887
1888  Description []
1889
1890  SideEffects []
1891
1892******************************************************************************/
1893
1894mdd_t *
1895Amc_AmcEvaluateEGFormula( 
1896  Fsm_Fsm_t *modelFsm,
1897  array_t   *subSystemArray,
1898  Amc_SubsystemInfo_t   *subSystem,
1899  mdd_t *invariantMdd,
1900  mdd_t *fairStates,
1901  Fsm_Fairness_t *modelFairness,
1902  mdd_t *careStates,
1903  array_t *onionRingsArrayForDbg,
1904  boolean lowerBound,
1905  array_t *quantifyVars,
1906  Mc_VerbosityLevel verbosity,
1907  Mc_DcLevel dcLevel )
1908{
1909  int i;
1910  array_t *onionRings = NIL(array_t);
1911  array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
1912  mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
1913  mdd_t *mddOne = mdd_one( mddManager );
1914  mdd_t *Zmdd;
1915
1916 
1917  array_t *buchiFairness = array_alloc( mdd_t *, 0 );
1918  if (modelFairness) {
1919    if ( !Fsm_FairnessTestIsBuchi( modelFairness ) ) {
1920      (void) fprintf(vis_stdout, "#** mc error: non Buchi fairness constraints not supported\n");
1921      return NIL(mdd_t);
1922    }
1923    else {
1924      int j;
1925      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( modelFairness, 0 );
1926      array_t   *careStatesArray = array_alloc(mdd_t *, 0);
1927
1928      array_insert(mdd_t *, careStatesArray, 0, careStates);
1929      for( j = 0 ; j < numBuchi; j++ ) {
1930        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness,
1931                                                        0, j, careStatesArray,
1932                                                        dcLevel);
1933        array_insert_last( mdd_t *, buchiFairness, tmpMdd );
1934      }
1935      array_free(careStatesArray);
1936    }
1937  }
1938  else {
1939    array_insert_last( mdd_t *, buchiFairness, mdd_one(mddManager) );
1940  }
1941
1942  if ( onionRingsArrayForDbg !=NIL(array_t) ) {
1943    tmpOnionRingsArrayForDbg = array_alloc( array_t *, 0 );
1944  }
1945
1946
1947  Zmdd = mdd_dup( invariantMdd );
1948  while (TRUE) {
1949
1950    mdd_t *ZprimeMdd = mdd_dup(Zmdd);
1951    mdd_t *conjunctsMdd = NIL(mdd_t);
1952    mdd_t *AAmdd = mdd_dup(Zmdd);
1953
1954    for ( i = 0 ; i < array_n( buchiFairness ) ; i++ ) {
1955
1956      mdd_t *aMdd, *bMdd, *cMdd;
1957      mdd_t *FiMdd = array_fetch( mdd_t *, buchiFairness, i );
1958
1959      if ( tmpOnionRingsArrayForDbg ) {
1960        onionRings = array_alloc( mdd_t *, 0 );
1961        array_insert_last( array_t *, tmpOnionRingsArrayForDbg, onionRings );
1962      }
1963
1964      /* aMdd = mdd_and( FiMdd, Zmdd, 1, 1); */
1965      aMdd = mdd_and( FiMdd, AAmdd, 1, 1);
1966
1967      bMdd = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, AAmdd, aMdd, mddOne, careStates, 
1968                                      onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
1969      mdd_free(aMdd);
1970      cMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, bMdd, mddOne, careStates,
1971                                      lowerBound, quantifyVars, verbosity, dcLevel ); 
1972      mdd_free(bMdd);
1973
1974      if ( conjunctsMdd == NIL(mdd_t) ) {
1975        conjunctsMdd = mdd_dup( cMdd );
1976        mdd_free( AAmdd ); AAmdd = mdd_and( conjunctsMdd, invariantMdd,1 ,1 ); 
1977      }
1978      else {
1979        mdd_t *tmpMdd = mdd_and( cMdd, conjunctsMdd, 1, 1 );
1980        mdd_free( conjunctsMdd );
1981        conjunctsMdd = tmpMdd;
1982        mdd_free( AAmdd ); AAmdd = mdd_and( conjunctsMdd, invariantMdd,1 ,1 );
1983      }
1984      mdd_free( cMdd );
1985    }
1986    mdd_free(AAmdd);
1987
1988    mdd_free(ZprimeMdd);
1989    ZprimeMdd = mdd_and( invariantMdd, conjunctsMdd, 1, 1 );
1990    mdd_free( conjunctsMdd );
1991
1992    if ( mdd_equal_mod_care_set( ZprimeMdd, Zmdd, careStates ) ) {
1993      mdd_free( ZprimeMdd );
1994      break;
1995    }
1996
1997    mdd_free( Zmdd );
1998    Zmdd = ZprimeMdd;
1999
2000    if ( tmpOnionRingsArrayForDbg ) {
2001      arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings ) {
2002        mdd_array_free( onionRings );
2003      }
2004      array_free( tmpOnionRingsArrayForDbg );
2005      tmpOnionRingsArrayForDbg = array_alloc( array_t *, 0 );
2006    }
2007  }
2008
2009  if ( onionRingsArrayForDbg != NIL(array_t) ) {
2010    arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings ) {
2011      array_insert_last( array_t *, onionRingsArrayForDbg, onionRings );
2012    }
2013    array_free( tmpOnionRingsArrayForDbg );
2014  }
2015
2016  if ( ( verbosity == McVerbositySome_c ) || ( verbosity == McVerbosityMax_c ) ) {
2017    { 
2018      for ( i = 0 ; i < array_n( onionRingsArrayForDbg ); i++ ) {
2019        int j;
2020        mdd_t *Fi = array_fetch( mdd_t *,  buchiFairness, i );
2021        array_t *onionRings = array_fetch( array_t *, onionRingsArrayForDbg, i );
2022        for( j = 0 ; j < array_n( onionRings ) ; j++ ) {
2023          mdd_t *ring = array_fetch( mdd_t *, onionRings, j );
2024          if ( j == 0 ) {
2025            if ( ! mdd_lequal( ring, Fi, 1, 1 ) ) {
2026              fprintf( vis_stderr, "Problem w/ dbg - inner most ring not in Fi\n");
2027            }
2028          }
2029          if ( ! mdd_lequal( ring, Zmdd, 1, 1 ) ) {
2030            fprintf( vis_stderr, "Problem w/ dbg - onion ring fails invariant\n");
2031          }
2032        }
2033      }
2034    }
2035
2036    { 
2037      mdd_t *tmpMdd = careStates ? mdd_and( Zmdd, careStates, 1, 1 ) : mdd_dup( Zmdd );
2038      fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n", 
2039              mdd_count_onset(  Fsm_FsmReadMddManager( modelFsm ), tmpMdd,
2040                                Fsm_FsmReadPresentStateVars( modelFsm ) ) );
2041      mdd_free( tmpMdd );
2042    }
2043  }
2044
2045  mdd_array_free( buchiFairness );
2046  mdd_free( mddOne );
2047
2048  return Zmdd;
2049}
2050
2051
2052/*---------------------------------------------------------------------------*/
2053/* Definition of internal functions                                          */
2054/*---------------------------------------------------------------------------*/
2055
2056/**Function********************************************************************
2057
2058  Synopsis           [Create an array of subsystems.]
2059
2060  Description        [Based on the array of set of vertices, create an
2061  array of subsystems. Depending on the grouping method, different function
2062  call is made to obtain an array of structure typed Part_SubsystemInfo_t.
2063  From this information, the vertex table, fan-in table, and the fan-out
2064  table is obtained to create an array of subFSMs and the subsystems.
2065  ]
2066
2067  SideEffects        []
2068
2069  SeeAlso            [Part_SubsystemInfo_t]
2070
2071******************************************************************************/
2072array_t *
2073AmcCreateSubsystemArray(
2074  Ntk_Network_t         *network,
2075  Ctlp_Formula_t        *formula)
2076{
2077  array_t               *partitionArray, *subSystemArray;
2078  Part_Subsystem_t      *partitionSubsystem;
2079  Part_SubsystemInfo_t *subsystemInfo; 
2080  st_table              *vertexTable;
2081  array_t               *fanInIndexArray, *fanOutIndexArray;
2082  st_table              *fanInSystemTable, *fanOutSystemTable;
2083  Amc_SubsystemInfo_t   *subSystem; 
2084  graph_t               *partition = Part_NetworkReadPartition(network);
2085  int                   i, j;
2086  int                   fanInIndex, fanOutIndex, numOfVertex;
2087  Amc_SubsystemInfo_t   *fanInSubsystem, *fanOutSubsystem;
2088  char                  *flagValue, *numberOfVertexInGroup;
2089  array_t               *ctlArray;
2090
2091  /* Obtain the size of the subsystem */
2092  numberOfVertexInGroup = Cmd_FlagReadByName("amc_sizeof_group");
2093  if(numberOfVertexInGroup != NIL(char)){
2094    numOfVertex = atoi(numberOfVertexInGroup); 
2095  }
2096  else{
2097    /* default value */
2098    numOfVertex = 8; 
2099  }
2100
2101  /*
2102   * Obtain subsystem partitioned as submachines.
2103   */
2104  flagValue = Cmd_FlagReadByName("amc_grouping_method");
2105  if( (flagValue != NIL(char)) && 
2106           (strcmp(flagValue, "latch_dependency")) == 0){
2107
2108    subsystemInfo = Part_PartitionSubsystemInfoInit(network);
2109    Part_PartitionSubsystemInfoSetBound(subsystemInfo, numOfVertex);
2110    partitionArray = Part_PartCreateSubsystems(subsystemInfo, NIL(array_t),
2111        NIL(array_t));
2112   
2113    Part_PartitionSubsystemInfoFree(subsystemInfo); 
2114
2115  }
2116  else{
2117    /*
2118     * Latches which have dependency relation with given formulae
2119     * are computed and grouped into sub-systems.
2120     */
2121    lsGen  gen;
2122    Ntk_Node_t *node;
2123    char *name;
2124    array_t *arrayOfDataInputName;
2125    lsList latchInputList = lsCreate();
2126
2127    if (latchInputList == (lsList)0){
2128      return NIL(array_t);
2129    }
2130
2131    ctlArray = array_alloc(Ctlp_Formula_t *, 1);
2132    array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);
2133
2134    if (!Part_PartitionGetLatchInputListFromCTL(network, ctlArray,
2135                                                NIL(array_t),
2136                                                latchInputList)) {
2137      array_free(ctlArray);
2138      return NIL(array_t);
2139    }
2140    arrayOfDataInputName = array_alloc(Ntk_Node_t *, lsLength(latchInputList));
2141    lsForEachItem(latchInputList, gen, node){
2142      name = Ntk_NodeReadName(node);
2143      array_insert_last(char *, arrayOfDataInputName, name);
2144    }
2145    lsDestroy(latchInputList, (void (*)(lsGeneric))0);
2146    array_sort(arrayOfDataInputName, stringCompare);
2147
2148    partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network,
2149                     arrayOfDataInputName);
2150    array_free(arrayOfDataInputName);
2151    array_free(ctlArray);
2152  }
2153
2154  subSystemArray = array_alloc(Amc_SubsystemInfo_t *, array_n(partitionArray));
2155
2156
2157  /*
2158   * For each partitioned submachines build an FSM.
2159   */
2160  arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
2161    Fsm_Fsm_t *fsm;
2162
2163    vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
2164    fanInIndexArray  = Part_PartitionSubsystemReadFanIn(partitionSubsystem);
2165    fanOutIndexArray = Part_PartitionSubsystemReadFanOut(partitionSubsystem); 
2166
2167    FREE(partitionSubsystem);
2168
2169    fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
2170        FALSE, 0);
2171
2172    subSystem = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable, 
2173                                    /*   NIL(st_table), NIL(st_table) ); */
2174                                       (st_table *)fanInIndexArray, 
2175                                       (st_table *)fanOutIndexArray); 
2176    array_insert_last(Amc_SubsystemInfo_t *, subSystemArray, subSystem);
2177  } /* end of arrayForEachItem(partitionArray) */
2178
2179  array_free(partitionArray);
2180
2181  /*
2182   * Convert fanInIndexTable to fanInSystemTable
2183   * Convert fanOutIndexTable to fanOutSystemTable
2184   */
2185  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
2186
2187    fanInIndexArray = (array_t *) AmcSubsystemReadFanInTable(subSystem);
2188    fanInSystemTable = st_init_table(st_ptrcmp, st_ptrhash);
2189
2190    if( fanInIndexArray != NIL(array_t) ) {
2191      arrayForEachItem(int, fanInIndexArray, j, fanInIndex) {
2192     
2193        fanInSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
2194                                     fanInIndex);
2195        st_insert(fanInSystemTable, (char *)fanInSubsystem, NIL(char));
2196
2197      }
2198      array_free(fanInIndexArray);
2199    }
2200
2201    AmcSubsystemSetFanInTable(subSystem, fanInSystemTable);
2202
2203
2204    fanOutIndexArray = (array_t *) AmcSubsystemReadFanOutTable(subSystem);
2205    fanOutSystemTable = st_init_table(st_ptrcmp, st_ptrhash);
2206
2207    if( fanOutIndexArray != NIL(array_t) ) {
2208      arrayForEachItem(int, fanOutIndexArray, j, fanOutIndex) {
2209     
2210        fanOutSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
2211                                      fanOutIndex);
2212        st_insert(fanOutSystemTable, (char *)fanOutSubsystem, NIL(char));
2213
2214      }
2215      array_free(fanOutIndexArray);
2216    }
2217
2218    AmcSubsystemSetFanOutTable(subSystem, fanOutSystemTable);
2219
2220  }
2221
2222
2223  return subSystemArray;
2224}
2225
2226/**Function********************************************************************
2227
2228  Synopsis           [Print subsystem(s) taken into the optimal system.]
2229
2230  SideEffects        [From the array of subsystems, prints the subsystems
2231  that has been added(combined) to form a optimal system.]
2232
2233  SeeAlso            []
2234
2235******************************************************************************/
2236void
2237AmcPrintOptimalSystem(
2238  FILE *fp,
2239  Amc_Info_t *amcInfo)
2240{
2241  int i;
2242  Amc_SubsystemInfo_t *subSystem;
2243
2244  fprintf(fp, "\nSubsystems in optimal path : ");
2245
2246  arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, subSystem) {
2247   
2248    if(subSystem->takenIntoOptimal)
2249      fprintf(fp, " %d ", i); 
2250 
2251  }
2252
2253}
2254
2255#ifdef AMC_DEBUG
2256/**Function********************************************************************
2257
2258  Synopsis           [Only for the debugging purpose.]
2259
2260  SideEffects        []
2261
2262  SeeAlso            []
2263
2264******************************************************************************/
2265void
2266AmcCheckSupportAndOutputFunctions(
2267  array_t *subSystemArray)
2268{
2269  int i;
2270  Amc_SubsystemInfo_t *subSystem;
2271  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
2272    Fsm_Fsm_t   *subSystemFsm   = AmcSubsystemReadFsm(subSystem);       
2273    Ntk_Network_t *network      = Fsm_FsmReadNetwork(subSystemFsm);
2274    mdd_manager *mddManager     = Ntk_NetworkReadMddManager(network);
2275    graph_t     *partition      = Part_NetworkReadPartition(network);
2276
2277    st_table    *vertexTable    = AmcSubsystemReadVertexTable(subSystem);
2278    st_generator                *stGen;
2279    char                        *latchName;
2280
2281    st_foreach_item(vertexTable, stGen, &latchName, NIL(char *)) {
2282
2283      Ntk_Node_t        *latch          = Ntk_NetworkFindNodeByName(network, latchName);
2284      int               functionMddId   = Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch));
2285
2286      char      *nameLatchDataInput     = Ntk_NodeReadName(Ntk_LatchReadDataInput(latch));
2287      vertex_t  *ptrVertex      = Part_PartitionFindVertexByName(partition, nameLatchDataInput);
2288      Mvf_Function_t    *nextStateFunction;
2289      st_table          *supportTable;
2290
2291      nextStateFunction = Part_VertexReadFunction(ptrVertex);
2292      supportTable      = AmcCreateFunctionSupportTable(nextStateFunction);
2293
2294      /* print the name of the latch vars and its mddId in this subsystem*/
2295      fprintf(vis_stdout, "\nSubsystem %d : Has latch : %s MddId : %d", 
2296                                             i, latchName, Ntk_NodeReadMddId(latch));
2297      fprintf(vis_stdout, "\n\tIts corresponding next state var : %s MddId : %d", 
2298                                             Ntk_NodeReadName(Ntk_NodeReadShadow(latch)),
2299                                             Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)) );
2300
2301      /* print the name of the output function and its mddId */
2302      {
2303        int outputMddId = Ntk_NodeReadMddId(Ntk_LatchReadDataInput(latch));
2304        fprintf(vis_stdout, "\n\tIts output function  Output Function : %s  MddId : %d", 
2305                                              nameLatchDataInput, outputMddId); 
2306      }
2307
2308      /* print the support of its output function */
2309      {
2310        st_generator            *stGen2;
2311        long                    supportId;
2312        st_foreach_item(supportTable, stGen2, (char **)&supportId, NIL(char *)) {
2313          Ntk_Node_t  *supportNode = Ntk_NetworkFindNodeByMddId(network, (int) supportId);
2314          char          *supportName = Ntk_NodeReadName(supportNode);
2315          fprintf(vis_stdout, "\n\tOutput function's support : %s MddId : %d",
2316                                                supportName, (int) supportId); 
2317          fflush(vis_stdout);
2318        } 
2319      }
2320
2321
2322    } /* end of st_foreach_item */
2323
2324  } /* end of ArrayForEachItem */
2325
2326
2327  /* Print the name of the present state vars and its mddId */
2328  /* Print the name of the next state vars and its mddId */
2329  /* Print the input vars */
2330  {
2331    Amc_SubsystemInfo_t *subSystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray, 0);
2332    Fsm_Fsm_t   *subSystemFsm      = AmcSubsystemReadFsm(subSystem);
2333    Ntk_Network_t *network         = Fsm_FsmReadNetwork(subSystemFsm);
2334    lsGen gen; Ntk_Node_t *inputNode;
2335    Ntk_NetworkForEachPrimaryInput(network, gen, inputNode) {
2336      fprintf(vis_stdout, "\nPrimary Input : %s MddId : %d", 
2337                             Ntk_NodeReadName(inputNode), Ntk_NodeReadMddId(inputNode));
2338    }
2339  }
2340
2341  /* Print the pseudo input vars */
2342  {
2343    Amc_SubsystemInfo_t *subSystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray, 0); 
2344    Fsm_Fsm_t   *subSystemFsm      = AmcSubsystemReadFsm(subSystem);
2345    Ntk_Network_t *network         = Fsm_FsmReadNetwork(subSystemFsm);
2346    lsGen gen; Ntk_Node_t *inputNode;
2347    Ntk_NetworkForEachPseudoInput(network, gen, inputNode) {
2348      fprintf(vis_stdout, "\nPseudo Input : %s MddId : %d", 
2349                             Ntk_NodeReadName(inputNode), Ntk_NodeReadMddId(inputNode));
2350      fflush(vis_stdout);
2351    }
2352  }
2353
2354}
2355
2356/**Function********************************************************************
2357
2358  Synopsis           [Only for debugging.]
2359
2360  SideEffects        []
2361
2362  SeeAlso            [Amc_SubsystemInfo]
2363
2364******************************************************************************/
2365st_table *
2366AmcCreateFunctionSupportTable(
2367  Mvf_Function_t *mvf)
2368{
2369  mdd_manager  *mddManager;        /* Manager for the MDDs */
2370  array_t      *support;
2371  st_table     *mddSupport = st_init_table(st_numcmp, st_numhash);
2372  int          numComponents = Mvf_FunctionReadNumComponents(mvf);
2373  int          j, k;
2374  mdd_t        *unit;
2375
2376  assert(numComponents!= 0);
2377 
2378  mddManager = Mvf_FunctionReadMddManager(mvf);
2379
2380  /*
2381   * compute the support of an mdd as the union of supports of every
2382   * function component
2383   */
2384  for(j = 0; j < numComponents; j++) {
2385    unit = Mvf_FunctionReadComponent(mvf, j);
2386    support = mdd_get_support(mddManager, unit);
2387   
2388    /* For every element of its support */
2389    for(k = 0; k < array_n(support); k++) {
2390      st_insert(mddSupport, (char *)(long)array_fetch(int, support, k), (char *)0);
2391    } /* End of for */
2392    array_free(support);
2393  } /* End of for */
2394
2395  return mddSupport;
2396} /* End of */
2397#endif
2398
2399
2400/**Function********************************************************************
2401
2402  Synopsis    [Find Mdd for states satisfying Atomic Formula.]
2403
2404  Description [This is a duplicate copy of static function,
2405  ModelCheckAtomicFormula(). ]
2406
2407  SideEffects []
2408
2409******************************************************************************/
2410mdd_t *
2411AmcModelCheckAtomicFormula( 
2412  Fsm_Fsm_t *modelFsm,
2413  Ctlp_Formula_t *ctlFormula)
2414{
2415  mdd_t * resultMdd;
2416  mdd_t *tmpMdd;
2417  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
2418  char *nodeNameString = Ctlp_FormulaReadVariableName( ctlFormula );
2419  char *nodeValueString = Ctlp_FormulaReadValueName( ctlFormula );
2420  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
2421
2422  Var_Variable_t *nodeVar;
2423  int nodeValue;
2424
2425  graph_t *modelPartition;
2426  vertex_t *partitionVertex;
2427  Mvf_Function_t *MVF;
2428
2429  nodeVar = Ntk_NodeReadVariable( node );
2430  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
2431    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
2432  }
2433  else {
2434    nodeValue = atoi( nodeValueString );
2435  } 
2436
2437  modelPartition = Part_NetworkReadPartition( network );
2438  if ( !( partitionVertex = Part_PartitionFindVertexByName( modelPartition,
2439                                                            nodeNameString ) )) { 
2440    lsGen tmpGen;
2441    Ntk_Node_t *tmpNode;
2442    array_t *mvfArray;
2443    array_t *tmpRoots = array_alloc( Ntk_Node_t *, 0 );
2444    st_table *tmpLeaves = st_init_table( st_ptrcmp, st_ptrhash );
2445    array_insert_last( Ntk_Node_t *, tmpRoots, node );
2446
2447    Ntk_NetworkForEachCombInput( network, tmpGen, tmpNode ) {
2448      st_insert( tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED );
2449    }
2450
2451    mvfArray =  Ntm_NetworkBuildMvfs( network, tmpRoots, tmpLeaves,
2452                                      NIL(mdd_t) );
2453    MVF = array_fetch( Mvf_Function_t *, mvfArray, 0 );
2454    array_free( tmpRoots );
2455    st_free_table( tmpLeaves );
2456    array_free( mvfArray );
2457
2458    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
2459    resultMdd = mdd_dup( tmpMdd );
2460    Mvf_FunctionFree( MVF );
2461    return resultMdd;
2462  }
2463  else {
2464    MVF = Part_VertexReadFunction( partitionVertex );
2465    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
2466    resultMdd = mdd_dup( tmpMdd );
2467    return resultMdd;
2468  }
2469}
2470
2471
2472/*---------------------------------------------------------------------------*/
2473/* Definition of static functions                                            */
2474/*---------------------------------------------------------------------------*/
2475/**Function********************************************************************
2476
2477  Synopsis [Compare two strings]
2478
2479  SideEffects []
2480
2481******************************************************************************/
2482static int
2483stringCompare(
2484  const void * s1,
2485  const void * s2)
2486{
2487  return(strcmp(*(char **)s1, *(char **)s2));
2488}
Note: See TracBrowser for help on using the repository browser.