source: vis_dev/vis-2.3/src/mc/mcDnC.c @ 45

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

vis2.3
File size: 35.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcDnC.c]
4
5  PackageName [mc]
6
7  Synopsis    [The Divide and Compose (D'n'C) Approach of SCC Enumeration.]
8
9  Description [This file contains the functions to compute the fair
10  Strongly Connected Components (SCCs) of the state translation graph
11  of an FSM by Divide and Compose.  Knowledge of the fair SCCs can be
12  used to decide language emptiness.  For more information, please
13  check the CONCUR'01 paper of Wang et al., "Divide and Compose: SCC
14  refinement for language emptiness." Other applications are also
15  possible.]
16
17  SeeAlso     []
18
19  Author      [Chao Wang]
20
21  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
22  All rights reserved.
23
24  Permission is hereby granted, without written agreement and without
25  license or royalty fees, to use, copy, modify, and distribute this
26  software and its documentation for any purpose, provided that the
27  above copyright notice and the following two paragraphs appear in
28  all copies of this software.]
29
30******************************************************************************/
31#include "mcInt.h"
32
33static char rcsid[] UNUSED = "$Id: mcDnC.c,v 1.9 2005/05/18 18:12:00 jinh Exp $";
34
35/*---------------------------------------------------------------------------*/
36/* Constant declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39/*---------------------------------------------------------------------------*/
40/* Structure declarations                                                    */
41/*---------------------------------------------------------------------------*/
42
43/*---------------------------------------------------------------------------*/
44/* Type declarations                                                         */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Macro declarations                                                        */
53/*---------------------------------------------------------------------------*/
54
55/**AutomaticStart*************************************************************/
56
57/*---------------------------------------------------------------------------*/
58/* Static function prototypes                                                */
59/*---------------------------------------------------------------------------*/
60static int SccIsStrong(mdd_manager *mddMgr, array_t *buechiFairness, mdd_t *SCC);
61static array_t * SortMddArrayBySize(Fsm_Fsm_t *fsm, array_t *mddArray);
62static int stringCompare(const void * s1, const void * s2);
63/**AutomaticEnd***************************************************************/
64
65
66/*---------------------------------------------------------------------------*/
67/* Definition of exported functions                                          */
68/*---------------------------------------------------------------------------*/
69
70/**Function********************************************************************
71
72  Synopsis [Compute all the states that lead to a fair cycle by
73  Compositional SCC analysis (DnC -- Divide and Compose).]
74
75  Comment [Used by LE/LTL/CTL* model checking. The Divide and Compose
76  (D'n'C) approach is used for the symbolic SCC enumeration, which
77  first creates SCC-closed sets on an abstract model and then
78  successively refines these sets on the refined abstract models,
79  until either no fair SCC exists or the concrete (original) model is
80  reached.
81
82  Strength reduction is also applied during the process -- as soon as
83  the SCC-closed sets become weak/terminal, special decision
84  procedures will be used to determine their language emptiness.
85
86  For more information, please check the CONCUR'01 paper of Wang et
87  al., "Divide and Compose: SCC refinement for language emptiness."
88 
89  Debugging information will be print out if dbgLevel is non-zero.
90
91  Return the set of initial states from where fair paths exist.]
92 
93  SideEffects []
94
95******************************************************************************/
96mdd_t *
97Mc_FsmCheckLanguageEmptinessByDnC(
98  Fsm_Fsm_t *modelFsm,
99  array_t *modelCareStates,
100  Mc_AutStrength_t automatonStrength,
101  int dcLevel,
102  int dbgLevel,
103  int printInputs,
104  int verbosity,
105  Mc_GSHScheduleType GSHschedule,
106  Mc_FwdBwdAnalysis GSHdirection,
107  int lockstep,
108  FILE *dbgFile,
109  int UseMore,
110  int SimValue,
111  char *driverName)
112{
113  Ntk_Network_t   *network = Fsm_FsmReadNetwork(modelFsm);
114  mdd_manager     *mddManager = Fsm_FsmReadMddManager(modelFsm);
115  Fsm_Fairness_t  *modelFairness = NIL(Fsm_Fairness_t);
116  array_t         *buechiFairness = NIL(array_t);
117  int             isExactReachableStatesAvailable = 0;
118  mdd_t           *reachableStates, *initialStates = NIL(mdd_t);
119  mdd_t           *fairStates, *fairInitialStates = NIL(mdd_t);
120  array_t         *onionRings = NIL(array_t);
121  array_t         *strongSccClosedSets = NIL(array_t);
122  array_t         *absLatchNameTableArray = NIL(array_t);
123  int             numOfAbstractModels, iter, i, exitFlag;
124  array_t         *arrayOfOnionRings = NIL(array_t);
125  array_t         *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
126  array_t         *modelCareStatesArray = mdd_array_duplicate(modelCareStates);
127  Mc_SccGen_t     *sccgen;
128  int             composeIncSize, numOfLatches, maxLatchesToCompose;
129
130  int             maxComposePercentage = 30;
131  int             maxSccsToEnum = 100;
132
133
134  /*
135   * Read fairness constraints.
136   */
137  modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
138  buechiFairness = array_alloc(mdd_t *, 0);
139  if (modelFairness != NIL(Fsm_Fairness_t)) {
140    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
141      (void) fprintf(vis_stdout, 
142                     "** non-Buechi fairness constraints not supported\n");
143      array_free(buechiFairness);
144      assert(0);
145    } else {
146      int j;
147      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
148      for (j = 0; j < numBuchi; j++) {
149        Ctlp_Formula_t *tmpFormula;
150        mdd_t *tempMdd;
151        tmpFormula = Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, j );
152        tempMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
153                                                  modelCareStatesArray, 
154                                                  (Mc_DcLevel) dcLevel);
155        array_insert_last(mdd_t *, buechiFairness, tempMdd);
156        array_insert_last( Ctlp_Formula_t *, ctlArray, 
157                           Ctlp_FormulaDup(tmpFormula));
158#if 1
159        fprintf(vis_stdout,"\nFairness[%d]:",j);
160        Ctlp_FormulaPrint(vis_stdout, tmpFormula);
161        fprintf(vis_stdout,"\n");
162#endif
163      }
164    }
165  } else {
166    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
167  }
168
169  /*
170   * If we need debugging information, arrayOfOnionRings != NIL(array_t),
171   */
172  if (dbgLevel != McDbgLevelNone_c)
173    arrayOfOnionRings = array_alloc(array_t *, 0);
174  else
175    arrayOfOnionRings = NIL(array_t);
176
177  /*
178   * If exact/approximate reachable states are available, use them.
179   */
180  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
181  reachableStates = Fsm_FsmReadReachableStates(modelFsm);
182  isExactReachableStatesAvailable = (reachableStates != NIL(mdd_t));
183  if (!isExactReachableStatesAvailable) 
184    reachableStates = McMddArrayAnd(modelCareStatesArray);
185  else
186    reachableStates = mdd_dup(reachableStates);
187  onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
188  if (onionRings == NIL(array_t)) {
189    onionRings = array_alloc(mdd_t *, 0);
190    array_insert(mdd_t *, onionRings, 0, mdd_dup(reachableStates));
191  }else
192    onionRings = mdd_array_duplicate(onionRings);
193
194  strongSccClosedSets = array_alloc(mdd_t *, 0);
195  array_insert(mdd_t *, strongSccClosedSets, 0, mdd_dup(reachableStates));
196
197  /*
198   * Compute a series of over-approximated abstract models
199   */
200  numOfLatches = array_n(Fsm_FsmReadPresentStateVars(modelFsm));
201  maxLatchesToCompose = (numOfLatches * maxComposePercentage/100);
202  maxLatchesToCompose = (maxLatchesToCompose > 20)? maxLatchesToCompose:20;
203  composeIncSize = maxLatchesToCompose/10;
204  composeIncSize = (composeIncSize > 4)? composeIncSize:4;
205
206  absLatchNameTableArray = 
207    Mc_CreateStaticRefinementScheduleArray(network,
208                                           ctlArray,
209                                           NIL(array_t),
210                                           NIL(array_t),
211                                           FALSE,
212                                           FALSE,
213                                           ((verbosity<McVerbosityMax_c)?
214                                            0:McVerbositySome_c),
215                                           composeIncSize,
216                                           Part_CorrelationWithSupport);
217  numOfAbstractModels = (array_n(absLatchNameTableArray) - 1);
218  if (verbosity >= McVerbosityLittle_c) {
219    fprintf(vis_stdout, 
220            "-- DnC: scheduled total %d abs models with %d latches\n",
221            numOfAbstractModels, numOfLatches);
222  }
223
224  if (verbosity >= McVerbositySome_c) {
225    fprintf(vis_stdout, "-- DnC:\n");
226    fprintf(vis_stdout, 
227            "-- DnC: maxComposePercentage = %d\n", maxComposePercentage);
228    fprintf(vis_stdout, 
229            "-- DnC: numOfLatches         = %d\n", numOfLatches);
230    fprintf(vis_stdout, 
231            "-- DnC: composeIncSize       = %d\n", composeIncSize);
232    fprintf(vis_stdout, 
233            "-- DnC: numOfAbstractModels  = %d\n", numOfAbstractModels);
234    fprintf(vis_stdout, 
235            "-- DnC: maxLatchesToCompose  = %d\n", maxLatchesToCompose);
236    fprintf(vis_stdout, 
237            "-- DnC: maxSccsToEnum        = %d\n", maxSccsToEnum);
238    fprintf(vis_stdout, "-- Dnc: \n");
239  }
240
241  exitFlag = 0;
242  for (iter=0; iter<numOfAbstractModels; iter++) {
243    Fsm_Fsm_t *absFsm = NIL(Fsm_Fsm_t);
244    st_table  *absLatchNameTable = NIL(st_table);
245    array_t   *absOnionRings;
246    array_t   *tempArray = NIL(array_t);
247    mdd_t     *sccClosedSet = NIL(mdd_t);
248    mdd_t     *tempMdd = NIL(mdd_t);
249    mdd_t     *absReachableStates = NIL(mdd_t);
250
251    absLatchNameTable = array_fetch(st_table *, absLatchNameTableArray, iter);
252    absFsm = Fsm_FsmCreateSubsystemFromNetwork(network, NIL(graph_t),
253                                               absLatchNameTable, TRUE, 1);
254
255    if (!isExactReachableStatesAvailable) {
256      absReachableStates = Fsm_FsmComputeReachableStates(absFsm, 0, 0, 0, 0,
257                                                         1, 0, 0,
258                                                         Fsm_Rch_Default_c, 
259                                                         0, 0,
260                                                         NIL(array_t), FALSE,
261                                                         NIL(array_t));
262      absOnionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
263      assert(absOnionRings);
264      absOnionRings = mdd_array_duplicate(absOnionRings);
265    }else {
266      absReachableStates = McComputeAbstractStates(absFsm, reachableStates);
267      absOnionRings = array_alloc(mdd_t *, array_n(onionRings));
268      arrayForEachItem(mdd_t *, onionRings, i, tempMdd) {
269        array_insert(mdd_t *, absOnionRings, i, 
270                     McComputeAbstractStates(absFsm, tempMdd) );
271      }
272    }
273
274    tempArray = strongSccClosedSets;
275    strongSccClosedSets = array_alloc(mdd_t *, 0);
276    arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
277      sccClosedSet = (iter == 0)? 
278        McComputeAbstractStates(absFsm, sccClosedSet): mdd_dup(sccClosedSet);
279      tempMdd = mdd_and(sccClosedSet, absReachableStates, 1, 1);
280      if (mdd_is_tautology(tempMdd, 0)) 
281        mdd_free(tempMdd);
282      else
283        array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
284      mdd_free(sccClosedSet);
285    }
286    mdd_array_free(tempArray);
287
288    /* Refine SCC-closed sets, but up to a certain number */
289    tempArray = strongSccClosedSets;
290    strongSccClosedSets = array_alloc(mdd_t *, 0);
291    Mc_FsmForEachFairScc(absFsm, sccgen, sccClosedSet, tempArray, 
292                         strongSccClosedSets, /* new scc-closed sets */
293                         buechiFairness, absOnionRings, FALSE,
294                         ((verbosity<McVerbosityMax_c)?
295                          McVerbosityNone_c:McVerbositySome_c),
296                         (Mc_DcLevel) dcLevel) {
297      if (SccIsStrong(mddManager, buechiFairness, sccClosedSet)) {
298        array_insert_last(mdd_t *, strongSccClosedSets, sccClosedSet);
299        if (maxSccsToEnum>0 && array_n(strongSccClosedSets)>maxSccsToEnum) {
300          Mc_FsmSccGenFree(sccgen, strongSccClosedSets);
301          break;
302        }
303
304      }else {
305        array_t  *newCareStatesArray;
306        newCareStatesArray = mdd_array_duplicate(modelCareStatesArray);
307        if (!isExactReachableStatesAvailable) 
308          array_insert_last(mdd_t *, newCareStatesArray, absReachableStates);
309
310        if (verbosity >= McVerbositySome_c) 
311          fprintf(vis_stdout, "-- DnC: search in a weak SCC-closed set\n");
312
313        fairStates = McFsmRefineWeakFairSCCs(modelFsm, sccClosedSet, 
314                                             newCareStatesArray, 
315                                             arrayOfOnionRings, FALSE, 
316                                             dcLevel, 
317                         ((verbosity<McVerbosityMax_c)? 0:McVerbositySome_c) );
318        fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
319        mdd_free(fairStates);
320        if (!mdd_is_tautology(fairInitialStates, 0)) { 
321          /* Done, find a reachable fair cycle */
322          exitFlag = 2; 
323          if (verbosity >= McVerbosityLittle_c) 
324            fprintf(vis_stdout, "-- DnC: find a weak SCC!\n");
325          Mc_FsmSccGenFree(sccgen, NIL(array_t));
326          break;
327        }else {
328          mdd_free(fairInitialStates); 
329        }
330      }
331
332    }/*Mc_FsmForEachFairScc( ) {*/ 
333    mdd_array_free(tempArray);
334
335    SortMddArrayBySize(absFsm, strongSccClosedSets);
336         
337    if (verbosity >= McVerbosityLittle_c && exitFlag != 2) {
338      fprintf(vis_stdout, 
339              "-- DnC: found %d SCC-closed sets in abs model %d with %d latches\n",
340              array_n(strongSccClosedSets), iter+1, 
341              st_count(absLatchNameTable));
342      if (verbosity >= McVerbositySome_c) {
343        array_t *absPSvars = Fsm_FsmReadPresentStateVars(absFsm);
344        array_t *PSvars = Fsm_FsmReadPresentStateVars(modelFsm);
345        arrayForEachItem(mdd_t *, strongSccClosedSets, i, tempMdd) {
346          fprintf(vis_stdout, "-- An SCC-closed set with %5g abs (%5g concrete) states\n",
347                  mdd_count_onset(mddManager, tempMdd, absPSvars),
348                  mdd_count_onset(mddManager, tempMdd, PSvars)
349                  );
350        }
351      }
352    }
353
354    if(exitFlag == 0 && array_n(strongSccClosedSets) == 0) {
355      /* Done, no reachable fair cycle exists */
356      exitFlag = 1; 
357    }
358
359    mdd_array_free(absOnionRings);
360    Fsm_FsmFree(absFsm);
361
362    /* existFlag: 0 --> unknown;  1 --> no fair SCC; 2 --> find a fair SCC */
363    if ( exitFlag != 0 || st_count(absLatchNameTable) > maxLatchesToCompose ) {
364      if (!isExactReachableStatesAvailable) {
365        array_insert_last(mdd_t *, modelCareStatesArray, absReachableStates);
366        tempMdd = reachableStates;
367        reachableStates = mdd_and(reachableStates, absReachableStates,1,1);
368        mdd_free(tempMdd);
369      }
370      break;
371    }
372
373    mdd_free(absReachableStates);
374       
375  }/*for (iter=0; iter<numOfAbstractModels; iter++) {*/
376
377  for (i=0; i<array_n(absLatchNameTableArray); i++) {
378    st_free_table( array_fetch(st_table *, absLatchNameTableArray, i) );
379  }
380  array_free(absLatchNameTableArray);
381
382
383  /*
384   * Compute fair SCCs on the concrete model if necessary
385   */
386  if (exitFlag == 0) {
387    array_t *tempArray;
388    mdd_t   *sccClosedSet = NIL(mdd_t);
389    mdd_t   *tempMdd = NIL(mdd_t);
390
391    if (verbosity >= McVerbosityLittle_c) 
392      fprintf(vis_stdout, "-- DnC: check the concrete model\n");
393
394    tempArray = strongSccClosedSets;
395    strongSccClosedSets = array_alloc(mdd_t *, 0);
396    arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
397      tempMdd = mdd_and(sccClosedSet, reachableStates, 1, 1);
398      if (mdd_is_tautology(tempMdd, 0)) 
399        mdd_free(tempMdd);
400      else
401        array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
402      mdd_free(sccClosedSet);
403    }
404    array_free(tempArray);
405
406    if (lockstep != MC_LOCKSTEP_OFF) {
407      tempArray = array_alloc(mdd_t *, 0);
408      fairStates = McFsmRefineFairSCCsByLockStep(modelFsm, lockstep,
409                                                 tempArray, 
410                                                 strongSccClosedSets,
411                                                 NIL(array_t),
412                                                 arrayOfOnionRings,
413                                                 (Mc_VerbosityLevel) verbosity,
414                                                 (Mc_DcLevel) dcLevel);
415      mdd_array_free(tempArray);
416    }else{
417      mdd_t   *fairStates0, *sccClosedSet;
418      array_t *EUonionRings;
419      mdd_t   *mddOne = mdd_one(mddManager);
420      Mc_EarlyTermination_t *earlyTermination;
421
422      sccClosedSet = McMddArrayOr(strongSccClosedSets);
423      fairStates0 = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet,
424                                            NIL(mdd_t), mddOne,
425                                            modelFairness,
426                                            modelCareStatesArray,
427                                            MC_NO_EARLY_TERMINATION,
428                                            NIL(array_t),
429                                            Mc_None_c, 
430                                            &arrayOfOnionRings,
431                                            (Mc_VerbosityLevel) verbosity,
432                                            (Mc_DcLevel) dcLevel,
433                                            NIL(boolean),
434                                            GSHschedule);
435      mdd_free(sccClosedSet);
436
437      EUonionRings = ( (arrayOfOnionRings == NIL(array_t))? 
438                       NIL(array_t):array_alloc(mdd_t *,0) );
439
440      earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
441      fairStates = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
442                                           fairStates0, NIL(mdd_t), mddOne,
443                                           modelCareStatesArray,
444                                           earlyTermination,
445                                           NIL(array_t), Mc_None_c,
446                                           EUonionRings,
447                                           (Mc_VerbosityLevel) verbosity,
448                                           (Mc_DcLevel) dcLevel,
449                                           NIL(boolean));
450      mdd_free(fairStates0);
451      mdd_free(mddOne);
452      Mc_EarlyTerminationFree(earlyTermination);
453
454      if (arrayOfOnionRings != NIL(array_t)) {
455        int j;
456        arrayForEachItem(array_t *, arrayOfOnionRings, i, tempArray) {
457#ifndef NDEBUG
458          mdd_t *mdd1 = array_fetch_last(mdd_t *, tempArray);
459#endif
460          arrayForEachItem(mdd_t *, EUonionRings, j, tempMdd) {
461            if (j != 0) 
462              array_insert_last(mdd_t *, tempArray, mdd_dup(tempMdd));
463            else   
464              assert( mdd_equal(tempMdd, mdd1) );
465          }
466        }
467        mdd_array_free(EUonionRings);
468      }
469    }
470
471    fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
472    mdd_free(fairStates);
473    exitFlag = mdd_is_tautology(fairInitialStates, 0)? 1:2;
474  }
475 
476  /* Clean-Ups */
477  mdd_array_free(modelCareStatesArray);
478  mdd_array_free(strongSccClosedSets);
479  mdd_array_free(onionRings);
480  mdd_free(reachableStates);
481  mdd_free(initialStates);
482
483  /*
484   * Print out the verification result (pass/fail, empty/non-empty)
485   */
486  if (exitFlag == 1) {
487    if (strcmp(driverName, "LE") == 0)
488      fprintf(vis_stdout, "# LE: language emptiness check passes\n");
489    else
490      fprintf(vis_stdout, "# %s: formula passed\n", driverName);
491    if (arrayOfOnionRings != NIL(array_t))
492      mdd_array_array_free(arrayOfOnionRings);
493    return fairInitialStates;
494
495  }else if (exitFlag == 2) {
496    if (strcmp(driverName, "LE") == 0)
497      fprintf(vis_stdout, "# LE: language is not empty\n");
498    else
499      fprintf(vis_stdout, "# %s: formula failed\n", driverName);
500 
501  }else {
502    fprintf(vis_stderr, "* DnC error, result is unknown!\n");
503    assert(0);
504  }
505
506  /*
507   * Print out the debugging information if requested
508   */
509  if (dbgLevel == McDbgLevelNone_c) {
510    if (arrayOfOnionRings != NIL(array_t)) 
511      mdd_array_array_free(arrayOfOnionRings);
512    return fairInitialStates;
513
514  }else {
515    mdd_t    *badStates, *aBadState, *mddOne;
516    McPath_t *fairPath, *normalPath;
517    array_t  *stemArray, *cycleArray;
518    FILE     *tmpFile = vis_stdout;
519    extern  FILE *vis_stdpipe;
520    fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);
521
522    /* Generate witness. */
523    badStates = mdd_dup(fairInitialStates);
524    aBadState = Mc_ComputeAState(badStates, modelFsm);
525    mdd_free(badStates);
526   
527    mddOne = mdd_one(mddManager);
528    fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
529                               modelCareStates, 
530                               (Mc_VerbosityLevel) verbosity,
531                               (Mc_DcLevel) dcLevel,
532                               McFwd_c);
533    mdd_free(mddOne);
534    mdd_free(aBadState);
535    mdd_array_array_free(arrayOfOnionRings);
536   
537    /* Print witness. */
538    normalPath = McPathNormalize(fairPath);
539    McPathFree(fairPath);
540   
541    stemArray = McPathReadStemArray(normalPath);
542    cycleArray = McPathReadCycleArray(normalPath);
543   
544    /* we should pass dbgFile/UseMore as parameters
545       dbgFile = McOptionsReadDebugFile(options);*/
546    if (dbgFile != NIL(FILE)) {
547      vis_stdpipe = dbgFile;
548    } else if (UseMore == TRUE) {
549      vis_stdpipe = popen("more","w");
550    } else {
551      vis_stdpipe = vis_stdout;
552    }
553    vis_stdout = vis_stdpipe;
554   
555    /* We should also pass SimValue as a parameter */
556    if (SimValue == FALSE) {
557      (void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
558      Mc_PrintPath(stemArray, modelFsm, printInputs);
559      fprintf (vis_stdout, "\n");
560     
561      (void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
562      Mc_PrintPath(cycleArray, modelFsm, printInputs);
563      fprintf (vis_stdout, "\n");
564    }else {
565      array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
566      (void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
567      McPrintSimPath(vis_stdout, completePath, modelFsm);
568      mdd_array_free(completePath);
569    }
570
571    if (dbgFile == NIL(FILE) && UseMore == TRUE) {
572      (void) pclose(vis_stdpipe);
573    } 
574    vis_stdout = tmpFile;
575   
576    McPathFree(normalPath);
577  }
578
579  return fairInitialStates;
580}
581
582/**Function********************************************************************
583
584  Synopsis           [Create a refinement schedule array.]
585
586  Description [If dynamicIncrease is true, the first element of return
587  array includes varibales appeared in formula. The size of the first
588  element should be less than or equal to incrementalSize. The second
589  element includes all variables in formula's cone of influence. When
590  dynamicIncrease is false, all variables in formula's cone of
591  influence (let's say n variables) are partitioned into
592  ceil(n/incrementalSize) elements. Then one more element which
593  includes all n variables are added to return array.]
594
595  SideEffects        []
596
597  SeeAlso            [Part_SubsystemInfo_t]
598
599******************************************************************************/
600array_t *
601Mc_CreateStaticRefinementScheduleArray(
602  Ntk_Network_t         *network,
603  array_t               *ctlArray,
604  array_t               *ltlArray,
605  array_t               *fairArray,
606  boolean               dynamicIncrease,
607  boolean               isLatchNameSort,
608  int                   verbosity,
609  int                   incrementalSize,
610  Part_CMethod          correlationMethod)
611{
612  array_t               *partitionArray;
613  Part_Subsystem_t      *partitionSubsystem;
614  Part_SubsystemInfo_t  *subsystemInfo; 
615  st_table              *latchNameTable;
616  st_table              *latchNameTableSum, *latchNameTableSumCopy;
617  char                  *flagValue;
618  st_generator          *stGen;
619  char                  *name;
620  double                affinityFactor;
621  array_t               *scheduleArray;
622  boolean               dynamicAndDependency = isLatchNameSort;
623  array_t               *tempArray, *tempArray2;
624  int                   i, count;
625
626  /* affinity factor to decompose state space */
627  flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
628  if(flagValue != NIL(char)){
629    affinityFactor = atof(flagValue); 
630  }
631  else{
632    /* default value */
633    affinityFactor = 0.5; 
634  }
635
636  /*
637   * Obtain submachines as array: The first sub-system includes
638   * variables in CTL/LTL/fair formulas and other latches are grouped
639   * in the same way as Part_PartCreateSubsystems()
640   */
641  subsystemInfo = Part_PartitionSubsystemInfoInit(network);
642  Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
643  Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
644  Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
645    correlationMethod); 
646  Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
647  partitionArray = Part_PartCreateSubsystemsWithCtlAndLtl(subsystemInfo,
648                   ctlArray, ltlArray, fairArray, 
649                   dynamicIncrease,dynamicAndDependency,FALSE);
650  Part_PartitionSubsystemInfoFree(subsystemInfo);
651
652  scheduleArray = array_alloc(st_table *, 0);
653
654
655  /*
656   * For each partitioned submachines build an FSM.
657   */
658  latchNameTableSum = st_init_table(strcmp, st_strhash);
659  if (!dynamicAndDependency){
660    for (i=0;i<array_n(partitionArray);i++){
661      partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
662      if (partitionSubsystem != NIL(Part_Subsystem_t)) {
663        latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
664        st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
665          if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
666            st_insert(latchNameTableSum, name, NIL(char));
667          }
668        }
669        Part_PartitionSubsystemFree(partitionSubsystem);
670      } 
671      latchNameTableSumCopy = st_copy(latchNameTableSum);
672      array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
673    }
674  }else{
675    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
676    latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
677    st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
678      st_insert(latchNameTableSum, name, NIL(char));
679    }
680    latchNameTableSumCopy = st_copy(latchNameTableSum);
681    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
682    Part_PartitionSubsystemFree(partitionSubsystem);
683   
684    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
685    tempArray = array_alloc(char *, 0);   
686    if (partitionSubsystem != NIL(Part_Subsystem_t)){
687      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
688      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
689        array_insert_last(char *, tempArray, name);
690      }
691      array_sort(tempArray, stringCompare);
692      Part_PartitionSubsystemFree(partitionSubsystem);
693    }
694   
695    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
696    tempArray2 = array_alloc(char *, 0);
697    if (partitionSubsystem != NIL(Part_Subsystem_t)) {
698      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
699      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
700        array_insert_last(char *, tempArray2, name);
701      }
702      array_sort(tempArray2, stringCompare);
703      Part_PartitionSubsystemFree(partitionSubsystem);
704    }
705
706    array_append(tempArray, tempArray2);
707    array_free(tempArray2);
708   
709    count = 0;
710    arrayForEachItem(char *, tempArray, i, name){   
711      if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
712        st_insert(latchNameTableSum, (char *)name, (char *)0);
713        count++;
714      }
715      if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
716        latchNameTableSumCopy = st_copy(latchNameTableSum);
717        array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
718        count = 0;
719      }
720    }
721    array_free(tempArray);
722    latchNameTableSumCopy = st_copy(latchNameTableSum);
723    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
724  }
725 
726  array_free(partitionArray);
727  st_free_table(latchNameTableSum);
728 
729  return (scheduleArray);
730}
731
732
733/*---------------------------------------------------------------------------*/
734/* Definition of internal functions                                          */
735/*---------------------------------------------------------------------------*/
736   
737/**Function********************************************************************
738
739  Synopsis [Compute the fair SCCs within the given weak SCC-closed
740  set.]
741
742  Description [Used by the Divide and Compose (D'n'C) approach for
743  language emptiness checking. Because it's a weak SCC-closed set,
744  fair states can be computed through the evaluation of EF EG
745  (sccClosedSet).
746 
747  Debugging information will be returned if arrayOfOnionRings is not NIL.
748
749  Return the fair states leading to a fair cycle within the given
750  SCC-closed set.]
751 
752  SideEffects [arrayOfOnionRings will be changed if it is not NIL and
753  the initial states intersect the fair states.]
754
755******************************************************************************/
756mdd_t *
757McFsmRefineWeakFairSCCs(
758  Fsm_Fsm_t *modelFsm, 
759  mdd_t *sccClosedSet, 
760  array_t *modelCareStatesArray, 
761  array_t *arrayOfOnionRings,
762  boolean isSccTerminal,
763  int dcLevel, 
764  int verbosity) 
765{
766  mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
767  mdd_t *initialStates;
768  mdd_t *mddOne, *mddEgFair, *mddEfEgFair, *fairInitStates, *mdd1;
769  array_t *EFonionRings, *EGArrayOfOnionRings, *EGonionRings;
770  array_t *newOnionRings;
771  int i, j;
772  Mc_EarlyTermination_t *earlyTermination;
773
774  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
775  mddOne = mdd_one(mddManager);
776
777  /* if debugging information is requested, arrayOfOnionRings!=NIL(array_t) */
778  if (arrayOfOnionRings != NIL(array_t)) {
779    EGArrayOfOnionRings = array_alloc(array_t *, 0);
780    EFonionRings = array_alloc(mdd_t *, 0);
781  }else {
782    EGArrayOfOnionRings = NIL(array_t);
783    EFonionRings = NIL(array_t);
784  }
785
786  if (isSccTerminal)
787    mddEgFair = mdd_dup(sccClosedSet);
788  else
789    mddEgFair = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet, 
790                                        NIL(mdd_t), mddOne, 
791                                        NIL(Fsm_Fairness_t),
792                                        modelCareStatesArray, 
793                                        NIL(Mc_EarlyTermination_t),
794                                        NIL(array_t), Mc_None_c,
795                                        &EGArrayOfOnionRings,
796                                        (Mc_VerbosityLevel) verbosity,
797                                        (Mc_DcLevel) dcLevel,
798                                        NIL(boolean), McGSH_EL_c);
799
800  earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
801  mddEfEgFair = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
802                                        mddEgFair, NIL(mdd_t), mddOne,
803                                        modelCareStatesArray,
804                                        earlyTermination,
805                                        NIL(array_t), Mc_None_c,
806                                        EFonionRings,
807                                        (Mc_VerbosityLevel) verbosity,
808                                        (Mc_DcLevel) dcLevel,
809                                        NIL(boolean));
810  mdd_free(mddEgFair);
811  Mc_EarlyTerminationFree(earlyTermination);
812
813  fairInitStates = mdd_and(mddEfEgFair, initialStates, 1, 1);
814
815  /* create the arrayOfOnionRings */
816  if (arrayOfOnionRings!=NIL(array_t) && !mdd_is_tautology(fairInitStates,0)) {
817    if (isSccTerminal) 
818      array_insert_last(array_t *, 
819                        arrayOfOnionRings, mdd_array_duplicate(EFonionRings));
820    else {
821      arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
822        newOnionRings = mdd_array_duplicate(EGonionRings);
823        arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
824          if (j != 0)
825            array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
826        }
827        array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
828      }
829    }
830  }
831  mdd_free(fairInitStates);
832 
833  if (arrayOfOnionRings != NIL(array_t)) {
834    mdd_array_free(EFonionRings);
835    mdd_array_array_free(EGArrayOfOnionRings);
836  }
837
838  mdd_free(initialStates);
839  mdd_free(mddOne);
840
841  return mddEfEgFair;
842}
843
844
845/**Function********************************************************************
846
847  Synopsis [Compute the abstract states from the concrete states.]
848
849  Description [By existentially quantify out the invisible
850  variables. Invisible variables are those state variables (or
851  latches) that are not in the supports of the abstract states---they
852  have been abstracted away.]
853
854  SideEffects []
855
856******************************************************************************/
857mdd_t * 
858McComputeAbstractStates(
859  Fsm_Fsm_t *absFsm, 
860  mdd_t *states)
861{
862  mdd_t       *result;
863  mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
864  array_t     *psVars = Fsm_FsmReadPresentStateVars(absFsm);
865  array_t     *supportVars;
866  array_t     *invisibleVars = array_alloc(long, 0);
867  st_table    *psVarTable = st_init_table(st_numcmp, st_numhash);
868  int         i;
869  long        mddId;
870
871  arrayForEachItem(long, psVars, i, mddId) {
872    st_insert(psVarTable, (char *)mddId, NIL(char));
873  }
874 
875  supportVars = mdd_get_support(mddManager, states);
876  arrayForEachItem(long, supportVars, i, mddId) {
877    if (!st_is_member(psVarTable, (char *)mddId)) 
878      array_insert_last(long, invisibleVars, mddId);
879  }
880  array_free(supportVars);
881  st_free_table(psVarTable);
882
883  result = mdd_smooth(mddManager, states, invisibleVars);
884
885  array_free(invisibleVars);
886
887  return result;
888}
889
890
891/**Function********************************************************************
892
893  Synopsis [Return true if the Divide and Compose (D'n'C) approach for
894  language emptiness checking is enabled.]
895
896  Description [Return true if the D'n'C approach for language emptiness
897  is enabled.]
898
899  SideEffects []
900
901******************************************************************************/
902boolean
903McGetDncEnabled(void)
904{
905  char *flagValue;
906  boolean result = FALSE;
907 
908  flagValue = Cmd_FlagReadByName("divide_and_compose");
909  if (flagValue != NIL(char)) {
910    if (strcmp(flagValue, "true") == 0)
911      result = TRUE;
912    else if (strcmp(flagValue, "false") == 0)
913      result = FALSE;
914    else {
915      fprintf(vis_stderr, "** dnc error: invalid dnc_enable flag %s, dnc is disabled. \n", flagValue);
916    }
917  }
918
919  return result;
920}
921
922
923/*---------------------------------------------------------------------------*/
924/* Definition of static functions                                            */
925/*---------------------------------------------------------------------------*/
926
927/**Function********************************************************************
928
929  Synopsis    [Return true if the given SCC is strong.]
930
931  Description [Return true if the given SCC is strong. Note that the
932  check is conservative -- for the purpose of efficiency -- When it
933  returns false, the SCC is definitely weak; when it returns true, the
934  SCC may be still be weak. For the language emptiness checking, this
935  is not going to hurt us.]
936
937  SideEffects []
938
939******************************************************************************/
940static boolean
941SccIsStrong(mdd_manager *mddMgr, array_t *buechiFairness, mdd_t *SCC)
942{
943  boolean strength;
944  mdd_t *LabeledAllFairness = mdd_dup(SCC);
945  mdd_t *NotLabeledAllFairness;
946  mdd_t *fairSet;
947  int i;
948   
949  /*
950   * check whether SCC intersects all the fairness constraints
951   * if yes, WEAK
952   * if no,  WEAK or STRONG
953   */
954  arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
955    mdd_t *tmpMdd = LabeledAllFairness;
956    LabeledAllFairness = mdd_and(LabeledAllFairness, fairSet, 1,1 );
957    mdd_free( tmpMdd );
958  }
959  NotLabeledAllFairness = mdd_and(SCC, LabeledAllFairness, 1, 0);
960  mdd_free(LabeledAllFairness);
961 
962  if(mdd_is_tautology(NotLabeledAllFairness, 0)) {
963    mdd_free(NotLabeledAllFairness);
964    strength = FALSE; /* WEAK*/
965  }
966  else {
967    mdd_free(NotLabeledAllFairness);
968    strength = TRUE;
969  }
970 
971  return strength;
972}
973
974/**Function********************************************************************
975
976  Synopsis    [Compare the size of two mdds.]
977
978  Description [Used to sort the array of mdds by their number of minterms.]
979
980  SideEffects [SortMddArrayBySize]
981
982******************************************************************************/
983static st_table *array_mdd_compare_table = NIL(st_table);
984static int 
985array_mdd_compare_size(
986  const void *obj1, 
987  const void *obj2) 
988{
989  double *val1, *val2;
990  int flag1, flag2;
991
992  flag1 = st_lookup(array_mdd_compare_table, *((char **)obj1), &val1);
993  flag2 = st_lookup(array_mdd_compare_table, *((char **)obj2), &val2);
994  assert(flag1 && flag2);
995
996  if (*val1 < *val2)
997    return -1;
998  else if (*val1> *val2)
999    return +1;
1000  else 
1001    return 0;
1002}
1003
1004/**Function********************************************************************
1005
1006  Synopsis    [Sort the array of mdds by their number of minterms.]
1007
1008  Description [Sort the array of mdds by their number of minterms. The
1009  present state variables of the given FSM is used to count the
1010  minterms. The sorting will be skipped if the number of present state
1011  variables is larger than 1024.]
1012
1013  SideEffects [array_mdd_compare_size]
1014
1015******************************************************************************/
1016static array_t *
1017SortMddArrayBySize(Fsm_Fsm_t *fsm, array_t *mddArray)
1018{
1019  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1020  array_t     *psVars = Fsm_FsmReadPresentStateVars(fsm);
1021 
1022  if (array_n(psVars) < 1024) {
1023    st_table    *mddToSizeTable =st_init_table(st_ptrcmp, st_ptrhash);
1024    double      *sizes = ALLOC(double, array_n(mddArray));
1025    mdd_t       *mdd1;
1026    int         i;
1027
1028    arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
1029      *(sizes+i) = mdd_count_onset(mddManager, mdd1, psVars);
1030      st_insert(mddToSizeTable, (char *)mdd1, (char *)(sizes+i));
1031    }
1032   
1033    array_mdd_compare_table = mddToSizeTable;
1034    array_sort(mddArray, array_mdd_compare_size);
1035
1036    FREE(sizes);
1037    st_free_table(mddToSizeTable);
1038  }
1039
1040  return mddArray;
1041}
1042
1043       
1044/**Function********************************************************************
1045
1046  Synopsis [Compare two strings]
1047
1048  SideEffects []
1049
1050******************************************************************************/
1051static int
1052stringCompare(
1053  const void * s1,
1054  const void * s2)
1055{
1056  return(strcmp(*(char **)s1, *(char **)s2));
1057}
1058
1059   
Note: See TracBrowser for help on using the repository browser.