source: vis_dev/vis-2.3/src/mc/mcUtil.c @ 82

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

vis2.3
File size: 168.2 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [mcUtil.c]
4
5  PackageName [mc]
6
7  Synopsis    [Utilities for Fair CTL model checker and debugger]
8
9  Author      [Adnan Aziz, Tom Shiple, In-Ho Moon]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "mcInt.h"
33#include "mdd.h"
34#include "cmd.h"
35#include "fsm.h"
36#include "img.h"
37#include "sat.h"
38#include "baig.h"
39#include <errno.h>
40
41static char rcsid[] UNUSED = "$Id: mcUtil.c,v 1.113 2009/04/11 18:26:10 fabio Exp $";
42
43/*---------------------------------------------------------------------------*/
44/* Macro declarations                                                        */
45/*---------------------------------------------------------------------------*/
46
47
48/**AutomaticStart*************************************************************/
49
50/*---------------------------------------------------------------------------*/
51/* Static function prototypes                                                */
52/*---------------------------------------------------------------------------*/
53
54static void PrintNodes(array_t *mddIdArray, Ntk_Network_t *network);
55static array_t * SortMddIds(array_t *mddIdArray, Ntk_Network_t *network);
56static void PrintDeck(array_t *mddValues, array_t *mddIdArray, Ntk_Network_t *network);
57static int cmp(const void * s1, const void * s2);
58static boolean AtomicFormulaCheckSemantics(Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
59static void NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable);
60static void NodeTableAddLtlFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable);
61static boolean MintermCheckWellFormed(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
62static boolean SetCheckSupport(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
63static mdd_t * Mc_ComputeRangeOfPseudoInputs(Ntk_Network_t *network);
64static array_t *Mc_BuildBackwardRingsWithInvariants(mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm);
65
66/**AutomaticEnd***************************************************************/
67
68
69/*---------------------------------------------------------------------------*/
70/* Definition of exported functions                                          */
71/*---------------------------------------------------------------------------*/
72
73/**Function********************************************************************
74
75  Synopsis [Return Boolean TRUE/FALSE depending on whether states in
76  specialStates can reach states in targetStates.]
77
78  Description [Return Boolean TRUE/FALSE depending on whether states in
79  specialStates can reach states in targetStates. If true, onionRings is set
80  to results of fixed point computation going back from targetStates to
81  specialStates.]
82
83  SideEffects []
84
85******************************************************************************/
86int
87Mc_FsmComputeStatesReachingToSet(
88  Fsm_Fsm_t *modelFsm,
89  mdd_t *targetStates,
90  array_t *careStatesArray,
91  mdd_t *specialStates,
92  array_t *onionRings,
93  Mc_VerbosityLevel verbosity,
94  Mc_DcLevel dcLevel)
95{
96  mdd_t *fromUpperBound;
97  mdd_t *toCareSet;
98  array_t *toCareSetArray = array_alloc(mdd_t *, 0);
99  mdd_t *image;
100  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
101
102  mdd_t *reachingStates = mdd_dup( targetStates );
103  mdd_t *fromLowerBound = mdd_dup( targetStates );
104
105  /* Iterate until fromLowerBound is empty. */
106  while (mdd_is_tautology(fromLowerBound, 0) == 0){
107    /* fromLowerBound is the "onion shell" of states just examined. */
108    array_insert_last(mdd_t*, onionRings,
109                      mdd_dup(fromLowerBound));
110    if ( !mdd_lequal(  fromLowerBound, specialStates, 1, 0 ) ) {
111      mdd_free( fromLowerBound );
112      mdd_free( reachingStates );
113      return TRUE;
114    }
115
116    /* fromUpperBound is the set of all states reaching targets thus far. */
117    fromUpperBound = mdd_dup( reachingStates );
118
119    /* toCareSet is the set of all states not reached so far. */
120    toCareSet = mdd_not(reachingStates);
121    array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
122
123    /*
124     * Pre-Image of some set between lower and upper, where we care
125     * about the image only on unreaching states.
126     */
127    image = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
128                fromLowerBound, fromUpperBound, toCareSetArray);
129    mdd_free(toCareSet);
130    mdd_free(fromLowerBound);
131
132    /* New set of reaching states is old set plus new image. */
133    mdd_free( reachingStates );
134    reachingStates = mdd_or(fromUpperBound, image, 1, 1);
135    mdd_free(image);
136
137    /*
138     * New lower bound is the states just reached (note not on
139     * fromUpperBound).
140     */
141    fromLowerBound = mdd_and(reachingStates, fromUpperBound, 1, 0);
142
143    mdd_free(fromUpperBound);
144  }
145  mdd_array_free( onionRings );
146  mdd_free( reachingStates );
147  mdd_free(fromLowerBound);
148  array_free(toCareSetArray);
149
150  return FALSE;
151}
152
153/**Function********************************************************************
154
155  Synopsis [Return Boolean TRUE/FALSE depending on whether states in
156  specialStates are reachable from  initialStates.]
157
158  Description [Return Boolean TRUE/FALSE depending on whether states in
159  specialStates are reachable from  initialStates.If true, onionRings is set
160  to results of fixed point computation going forward from initialStates to
161  specialStates.  Otherwise onionRings is freed.]
162
163  SideEffects []
164
165******************************************************************************/
166int
167Mc_FsmComputeStatesReachableFromSet(
168  Fsm_Fsm_t *modelFsm,
169  mdd_t *initialStates,
170  array_t *careStatesArray,
171  mdd_t *specialStates,
172  array_t *onionRings,
173  Mc_VerbosityLevel verbosity,
174  Mc_DcLevel dcLevel)
175{
176  boolean reachable=FALSE;
177  mdd_t *fromUpperBound;
178  mdd_t *toCareSet;
179  array_t *toCareSetArray = array_alloc(mdd_t *, 0);
180  mdd_t *image;
181  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
182
183  mdd_t *reachableStates = mdd_dup( initialStates );
184  mdd_t *fromLowerBound = mdd_dup( initialStates );
185
186  /* Iterate until fromLowerBound is empty. */
187  while (mdd_is_tautology(fromLowerBound, 0) == 0){
188    /* fromLowerBound is the "onion shell" of states just reached. */
189    array_insert_last(mdd_t*, onionRings,
190                      mdd_dup(fromLowerBound));
191    if (!mdd_lequal(  fromLowerBound, specialStates, 1, 0 ) ) {
192      mdd_free( fromLowerBound );
193      mdd_free( reachableStates );
194      return TRUE;
195    }
196
197    /* fromUpperBound is the set of all states reached thus far. */
198    fromUpperBound = mdd_dup( reachableStates );
199
200    /* toCareSet is the set of all states not reached so far. */
201    toCareSet = mdd_not(reachableStates);
202    array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
203
204    /*
205     * Image of some set between lower and upper, where we care
206     * about the image only on unreached states.
207     */
208    image = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
209                fromLowerBound, fromUpperBound, toCareSetArray);
210    mdd_free(toCareSet);
211    mdd_free(fromLowerBound);
212
213    /* New set of reachable states is old set plus new image. */
214    mdd_free( reachableStates );
215    reachableStates = mdd_or(fromUpperBound, image, 1, 1);
216    mdd_free(image);
217
218    /*
219     * New lower bound is the states just reached (note not on
220     * fromUpperBound).
221     */
222    fromLowerBound = mdd_and(reachableStates, fromUpperBound, 1, 0);
223    mdd_free(fromUpperBound);
224  }
225  mdd_array_free( onionRings );
226  mdd_free( reachableStates );
227  mdd_free(fromLowerBound);
228  array_free(toCareSetArray);
229
230  return reachable;
231
232}
233
234/**Function********************************************************************
235
236  Synopsis [Perform static semantic check of ctl formula on network.]
237
238  Description [Perform static semantic check of ctl formula on network.
239  Specifically, given an atomic formula of the form LHS=RHS, check that the LHS
240  is the name of a latch/wire in the network, and that RHS is of appropriate
241  type (enum/integer) and is lies in the range of the latch/wire values. If LHS
242  is a wire, and inputsAllowed is false, check to see that the algebraic
243  support of the wire consists of only latches and constants.]
244
245  SideEffects []
246
247******************************************************************************/
248boolean
249Mc_FormulaStaticSemanticCheckOnNetwork(
250  Ctlp_Formula_t *formula,
251  Ntk_Network_t *network,
252  boolean inputsAllowed
253  )
254{
255  boolean lCheck;
256  boolean rCheck;
257  Ctlp_Formula_t *leftChild;
258  Ctlp_Formula_t *rightChild;
259
260  if(formula == NIL(Ctlp_Formula_t)){
261    return TRUE;
262  }
263
264  if(Ctlp_FormulaReadType(formula) == Ctlp_ID_c){
265    return AtomicFormulaCheckSemantics(formula, network, inputsAllowed);
266  }
267
268  leftChild = Ctlp_FormulaReadLeftChild(formula);
269  rightChild = Ctlp_FormulaReadRightChild(formula);
270
271  lCheck = Mc_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
272                                                  inputsAllowed);
273  if(!lCheck)
274    return FALSE;
275
276  rCheck = Mc_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
277                                                  inputsAllowed);
278  if (!rCheck)
279      return FALSE;
280
281  return TRUE;
282}
283
284/**Function********************************************************************
285
286  Synopsis [Build Path to Core starting at aState.]
287
288  Description [Build Path to Core (the first onion ring) starting at aState.
289
290  <p> For the onion rings should be built in such a way that for every state v
291  in ring i+1 there is a state v' in ring i such that there is an edge from v
292  to v'.  This function will also works for non-BFS rings, where we just
293  require that for every state v in a ring i > 0, there is a state in a ring 0
294  <= j < i that is a successor of v.
295
296  <p>For paths of length at least one, set PathLengthType to McGreaterZero_c.
297  Otherwise, use McGreaterOrEqualZero_c.  The function returns a sequence of
298  states to a state in the core of onionRings, starting at aState. It is the
299  users responsibility to free the array returned as well as its members.]
300
301  SideEffects []
302
303******************************************************************************/
304array_t *
305Mc_BuildPathToCore(
306  mdd_t *aState,
307  array_t *onionRings,
308  Fsm_Fsm_t *modelFsm,
309  Mc_PathLengthType PathLengthType)
310{
311  int i;  /* index into the onionRings */
312  int startingPoint;
313  mdd_t *currentState;
314  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
315  array_t *pathToCore;
316  mdd_manager *mddMgr         = Fsm_FsmReadMddManager(modelFsm);
317  array_t *toCareSetArray;
318
319  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
320    return(Mc_BuildPathToCoreFAFW(
321                            aState, onionRings, modelFsm, PathLengthType));
322  }
323
324  pathToCore         = array_alloc( mdd_t * , 0 );
325  toCareSetArray     = array_alloc(mdd_t *, 0);
326  array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));
327
328  if ( PathLengthType == McGreaterZero_c )
329    startingPoint = 1;
330  else if ( PathLengthType == McGreaterOrEqualZero_c )
331    startingPoint = 0;
332  else
333    fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");
334
335  /* RB: How do you guarantee that aState is in one of the onion rings [1,n]?*/
336
337  /*Find the lowest ring that holds aState*/
338  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
339    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
340    if ( McStateTestMembership( aState, ring ) )
341      break;
342  }
343  if ( i == array_n( onionRings ) )
344    return NIL(array_t);
345
346  currentState = mdd_dup( aState );
347  array_insert_last( mdd_t *, pathToCore, currentState );
348
349  /* until we get to ring 0, keep finding successors for currentState */
350  while( i > 0 ) {
351    mdd_t *currentStateSuccs;
352    mdd_t *innerRing;
353    mdd_t *currentStateSuccsInInnerRing;
354    mdd_t *witnessSuccState;
355
356    i--;
357
358    currentStateSuccs =
359      Img_ImageInfoComputeImageWithDomainVars(imageInfo, currentState,
360                                              currentState, toCareSetArray);
361    currentStateSuccsInInnerRing = mdd_zero(mddMgr);
362
363    /* find the highest ring that contains a successor, starting with i */
364    while(mdd_is_tautology(currentStateSuccsInInnerRing, 0)){
365      assert(i >= 0);
366      if(i < 0) return NIL(array_t);
367
368      innerRing = array_fetch( mdd_t *, onionRings, i );
369      mdd_free(currentStateSuccsInInnerRing);
370      currentStateSuccsInInnerRing = mdd_and(currentStateSuccs, innerRing,
371                                             1, 1 );
372      i--;
373    }
374
375    i++;
376
377    witnessSuccState = Mc_ComputeACloseState(currentStateSuccsInInnerRing,
378                                             currentState,
379                                             modelFsm );
380    array_insert_last( mdd_t *, pathToCore, witnessSuccState );
381    currentState = witnessSuccState;
382
383    mdd_free( currentStateSuccs );
384    mdd_free( currentStateSuccsInInnerRing );
385
386    /* next, see if we cannot move a few more rings down.  We have to do this,
387     * since a nontrivial path is not guaranteed to exist from a node in ring i
388     * to a node in a lower ring.  In fact a state in ring i may also be in
389     * ring 0. */
390    {
391      boolean contained = TRUE;
392      while(contained && i > 0){
393        i--;
394        innerRing = array_fetch( mdd_t *, onionRings, i );
395        contained = mdd_lequal(witnessSuccState, innerRing, 1, 1);
396      }
397      /* i is highest ring not containing witnessSuccState, or i = 0 */
398
399      if(!contained){
400        i++;
401      }
402      /* i is lowest ring containing witnessSuccState */
403    }
404  }
405
406  mdd_array_free(toCareSetArray);
407
408  return pathToCore;
409}
410
411/**Function********************************************************************
412
413  Synopsis [Build a onion ring from initial state.]
414
415  Description [Build a onion ring from initial state.
416               This is function for FateAndFreeWill counterexample generation.]
417
418  SideEffects []
419
420******************************************************************************/
421array_t *
422Mc_BuildForwardRings(
423  mdd_t *S,
424  Fsm_Fsm_t *fsm,
425  array_t *onionRings)
426{
427  mdd_t *nextStates;
428  mdd_t *states, *nStates, *oneMdd;
429  array_t *toCareSetArray, *forwardRings;
430  int i;
431  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
432
433  states = mdd_zero(mddMgr);
434  oneMdd = mdd_one(mddMgr);
435  for(i=0; i<array_n(onionRings); i++) {
436    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
437    nStates = mdd_or(ring, states, 1, 1);
438    mdd_free(states);
439    states = nStates;
440  }
441  forwardRings = array_alloc(mdd_t *, 0);
442  toCareSetArray = array_alloc(mdd_t *, 0);
443  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
444  nextStates = Mc_FsmEvaluateESFormula(fsm, states, S,
445                                       NIL(mdd_t), oneMdd, toCareSetArray,
446                                       MC_NO_EARLY_TERMINATION, NIL(array_t),
447                                       Mc_None_c, forwardRings,
448                                       McVerbosityNone_c, McDcLevelNone_c,
449                                       NIL(boolean));
450  mdd_free(nextStates);
451  mdd_free(states);
452  mdd_array_free(toCareSetArray);
453
454  return(forwardRings);
455}
456
457/**Function********************************************************************
458
459  Synopsis [Build a onion ring to target under invariants.]
460
461  Description [Build a onion ring to target under invariants.
462               This is function for FateAndFreeWill counterexample generation.]
463
464  SideEffects []
465
466******************************************************************************/
467array_t *
468Mc_BuildForwardRingsWithInvariants(mdd_t *S,
469                                   mdd_t *T,
470                                   mdd_t *invariants,
471                                   Fsm_Fsm_t *fsm)
472{
473  mdd_t *oneMdd, *nextStates, *fairStates;
474  array_t *toCareSetArray, *forwardRings;
475  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
476
477  oneMdd = mdd_one(mddMgr);
478  forwardRings = array_alloc(mdd_t *, 0);
479  toCareSetArray = array_alloc(mdd_t *, 0);
480  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
481  fairStates = Fsm_FsmReadFairnessStates(fsm);
482  if(fairStates == 0)   fairStates = oneMdd;
483  nextStates = McEvaluateESFormulaWithGivenTRWithTarget(fsm, invariants, S, T,
484                                   NIL(mdd_t), fairStates, toCareSetArray,
485                                   MC_NO_EARLY_TERMINATION,
486                                   forwardRings, McVerbosityNone_c,
487                                   McDcLevelNone_c, NIL(boolean));
488  mdd_free(nextStates);
489  mdd_array_free(toCareSetArray);
490
491  return(forwardRings);
492}
493
494/**Function********************************************************************
495
496  Synopsis [Build a onion ring from target under invariants.]
497
498  Description [Build a onion ring from target under invariants.
499               This is function for FateAndFreeWill counterexample generation.]
500
501  SideEffects []
502
503******************************************************************************/
504static array_t *
505Mc_BuildBackwardRingsWithInvariants(
506  mdd_t *S,
507  mdd_t *T,
508  mdd_t *invariants,
509  Fsm_Fsm_t *fsm)
510{
511  mdd_t *oneMdd, *nextStates, *fairStates;
512  array_t *toCareSetArray, *backwardRings;
513  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
514
515  oneMdd = mdd_one(mddMgr);
516  backwardRings = array_alloc(mdd_t *, 0);
517  toCareSetArray = array_alloc(mdd_t *, 0);
518  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
519  fairStates = Fsm_FsmReadFairnessStates(fsm);
520  if(fairStates == 0)   fairStates = oneMdd;
521  nextStates = McEvaluateEUFormulaWithGivenTR(fsm, invariants, T,
522                                   NIL(mdd_t), fairStates, toCareSetArray,
523                                   MC_NO_EARLY_TERMINATION,
524                                   backwardRings, McVerbosityNone_c,
525                                   McDcLevelNone_c, NIL(boolean));
526  mdd_free(nextStates);
527  mdd_array_free(toCareSetArray);
528
529  return(backwardRings);
530}
531
532/**Function********************************************************************
533
534  Synopsis [Build Path from Core to aState.]
535
536  Description [Build Path starting at a Core state (a state in the first onion
537  ring) to aState.  For paths of length at least one, set PathLengthType to
538  McGreaterZero_c; otherwise, use McGreaterOrEqualZero_c.  The function returns
539  a sequence of states from the core of onionRings to a aState.
540
541  <p>In the case of BFS search, the onion rings are built forward, so that any
542  state in ring i+1 has at least one predecessor in ring i-1.  In non-BFS
543  search that may not be true, but we will have that every state in ring i+1
544  has a predecessor in ring i or less.  The fsm is checked to see if the search
545  was BFS. If not, every ring from the beginning is searched to find the
546  shortest path. This is a greedy heuristic and the shortest path is not
547  guaranteed to be found.  McBuildPathToCore takes a different approach.
548
549  <p>It is the users responsibility to free the array returned as well as its
550  members.]
551
552  SideEffects []
553
554  SeeAlso[Mc_BuildPathToCore]
555
556******************************************************************************/
557array_t *
558Mc_BuildPathFromCore(
559  mdd_t *aStates,
560  array_t *onionRings,
561  Fsm_Fsm_t *modelFsm,
562  Mc_PathLengthType PathLengthType)
563{
564  int i, j;
565  int startingPoint;
566  mdd_t *currentState, *aState;
567  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
568  array_t *pathToCore;
569  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
570  array_t *toCareSetArray;
571  array_t *pathFromCore;
572  mdd_t *currentStatePreds, *currentStatePredsInInnerRing;
573  mdd_t *innerRing = NIL(mdd_t), *witnessPredState;
574  boolean shortestDist =
575        (Fsm_FsmReadReachabilityOnionRingsMode(modelFsm) == Fsm_Rch_Bfs_c);
576
577
578  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
579    pathFromCore = Mc_BuildPathFromCoreFAFW(
580                            aStates, onionRings,
581                            modelFsm, PathLengthType);
582    return(pathFromCore);
583  }
584  aState = Mc_ComputeAState(aStates, modelFsm);
585
586  pathToCore = array_alloc( mdd_t * , 0 );
587  toCareSetArray = NIL(array_t);
588
589  if ( PathLengthType == McGreaterZero_c ) {
590    startingPoint = 1;
591  }
592  else if ( PathLengthType == McGreaterOrEqualZero_c ) {
593    startingPoint = 0;
594  }
595  else {
596    fail("Called Mc_BuildPathFromCore with ill formed PathLengthType\n");
597  }
598
599  /* check that the state occurs in an onion ring. */
600  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
601    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
602    if ( McStateTestMembership( aState, ring ) )
603      break;
604  }
605  if ( i == array_n( onionRings ) ) {
606    mdd_free(aState);
607    return NIL(array_t);
608  }
609
610  /* insert the state in the path to the core */
611  currentState = aState;
612  array_insert_last( mdd_t *, pathToCore, currentState );
613
614  /* initialize */
615  toCareSetArray = array_alloc(mdd_t *, 0);
616  array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));
617
618  /* loop until a path is found to the core */
619  while( i-- > 0 ) {
620    if (shortestDist) {
621      /* a predecessor is guaranteed to be in the previous ring */
622      mdd_array_free(toCareSetArray);
623      toCareSetArray = array_alloc(mdd_t *, 0);
624      innerRing = array_fetch( mdd_t *, onionRings, i );
625      array_insert(mdd_t *, toCareSetArray, 0, mdd_dup(innerRing));
626      currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
627                                imageInfo, currentState,
628                                currentState, toCareSetArray);
629    } else {
630      /* compute the predecessors */
631      currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
632                                imageInfo, currentState,
633                                currentState, toCareSetArray );
634      /* search for a predecessor in the earliest onion ring */
635      for (j = 0; j <= i; j++) {
636        innerRing = array_fetch( mdd_t *, onionRings, j );
637        if (!mdd_lequal(currentStatePreds, innerRing, 1, 0)) {
638          i = j;
639          break;
640        }
641      }
642    }
643    /* compute the set of predecessors in the chosen ring. */
644    currentStatePredsInInnerRing = mdd_and(currentStatePreds, innerRing, 1, 1);
645    mdd_free( currentStatePreds );
646    /* find a state in the predecessor */
647    witnessPredState = Mc_ComputeACloseState(currentStatePredsInInnerRing,
648                                             currentState, modelFsm);
649    mdd_free( currentStatePredsInInnerRing );
650    /* insert predecessor in the path */
651    array_insert_last( mdd_t *, pathToCore, witnessPredState );
652    currentState = witnessPredState;
653  }
654
655  mdd_array_free(toCareSetArray);
656
657  /* flip the path to a path from the core */
658  {
659    int i;
660    pathFromCore = array_alloc( mdd_t *, 0 );
661
662    for( i=0; i < array_n( pathToCore ); i++ ) {
663      mdd_t *tmpMdd = array_fetch(mdd_t *, pathToCore,
664                                  (array_n(pathToCore) - (i+1)));
665      array_insert_last( mdd_t *, pathFromCore, tmpMdd );
666    }
667    array_free( pathToCore );
668    return pathFromCore;
669  }
670}
671
672/**Function********************************************************************
673
674  Synopsis [Build a path from initial state to target.]
675
676  Description [Build a path from initial state to target.
677               This is function for FateAndFreeWill counterexample generation.]
678
679  SideEffects []
680
681******************************************************************************/
682array_t *
683Mc_BuildPathToCoreFAFW(
684  mdd_t *aStates,
685  array_t *onionRings,
686  Fsm_Fsm_t *modelFsm,
687  Mc_PathLengthType PathLengthType)
688{
689  int i, startingPoint;
690  array_t *pathFromCore, *pathToCore;
691  array_t *reachableOnionRings;
692  mdd_t *currentStates;
693
694  if ( PathLengthType == McGreaterZero_c ) {
695    startingPoint = 1;
696  }
697  else if ( PathLengthType == McGreaterOrEqualZero_c ) {
698    startingPoint = 0;
699  }
700  else {
701    fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");
702  }
703
704  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
705    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
706    if ( McStateTestMembership( aStates, ring ) )
707      break;
708  }
709  if(i==0) {
710    pathToCore = array_alloc( mdd_t * , 0 );
711    array_insert_last( mdd_t *, pathToCore, mdd_dup(aStates) );
712    return pathToCore;
713  }
714
715  reachableOnionRings = Mc_BuildForwardRings(aStates, modelFsm, onionRings);
716  currentStates = array_fetch(mdd_t *, onionRings, 0);
717  pathFromCore = Mc_BuildPathFromCoreFAFW(
718                                currentStates,
719                                reachableOnionRings, modelFsm, PathLengthType);
720  mdd_array_free(reachableOnionRings);
721
722  return(pathFromCore);
723}
724
725
726/**Function********************************************************************
727
728  Synopsis [Build a path from target to initial state with general algorithm.]
729
730  Description [Build a path from target to initial state with general algorithm.
731               This is function for FateAndFreeWill counterexample generation.]
732
733  SideEffects []
734
735******************************************************************************/
736array_t *
737Mc_BuildPathFromCoreFAFWGeneral(
738  mdd_t *T,
739  array_t *rings,
740  Fsm_Fsm_t *modelFsm,
741  Mc_PathLengthType PathLengthType)
742{
743  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
744  mdd_t *S, *H, *nH, *ring;
745  int i;
746  array_t *L;
747  array_t *pathFromCore;
748  array_t *npathFromCore;
749
750  H = mdd_zero(mgr);
751  for(i=0; i<array_n(rings); i++) {
752    ring = array_fetch(mdd_t *, rings, i);
753    nH = mdd_or(ring, H, 1, 1);
754    mdd_free(H);
755    H = nH;
756  }
757
758  nH = mdd_and(H, T, 1, 1);
759  T = nH;
760
761  L = Mc_BuildFAFWLayer(modelFsm, mdd_dup(T), mdd_dup(H));
762
763  if ( PathLengthType == McGreaterZero_c ) {
764    S = mdd_dup(array_fetch(mdd_t *, rings, 1));
765  }
766  else if( PathLengthType == McGreaterOrEqualZero_c ) {
767    S = mdd_dup(array_fetch(mdd_t *, rings, 0));
768  }
769  else {
770    fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
771  }
772  pathFromCore =
773      MC_BuildCounterExampleFAFWGeneral(modelFsm, mdd_dup(S), mdd_dup(T), H, L);
774
775  if(PathLengthType == McGreaterZero_c ) {
776    S = array_fetch(mdd_t *, rings, 0);
777    npathFromCore = array_alloc(mdd_t *, 0);
778    array_insert_last(mdd_t *, npathFromCore, mdd_dup(S));
779    for(i=0; i<array_n(pathFromCore); i++) {
780      S = array_fetch(mdd_t *, pathFromCore, i);
781      array_insert_last(mdd_t *, npathFromCore, S);
782    }
783    array_free(pathFromCore);
784    pathFromCore = npathFromCore;
785  }
786  mdd_free(T);
787  return(pathFromCore);
788}
789
790
791/**Function********************************************************************
792
793  Synopsis [Build a counterexample path with general algorithm.]
794
795  Description [Build a counterexample path with general algorithm
796               This is function for FateAndFreeWill counterexample generation.]
797
798  SideEffects []
799
800******************************************************************************/
801array_t *
802MC_BuildCounterExampleFAFWGeneral(
803        Fsm_Fsm_t *modelFsm,
804        mdd_t *I,
805        mdd_t *T,
806        mdd_t *H,
807        array_t *L)
808{
809  mdd_t *oneMdd, *zeroMdd;
810  mdd_t *T_I, *P, *Li, *Q_Li, *Q_T, *nLi;
811  mdd_t *ring, *ring_Q, *Q;
812  mdd_t *layer, *Lm, *nLayer;
813  mdd_t *extCube;
814  mdd_t *invariantStates, *nInvariantStates;
815  int m, q, free, i;
816  array_t *path, *R;
817  array_t *careStatesArray;
818  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
819  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
820
821  oneMdd = mdd_one(mgr);
822  zeroMdd = mdd_zero(mgr);
823  path = array_alloc(mdd_t *, 0);
824
825  T_I = mdd_and(T, I, 1, 1);
826  if(!mdd_equal(T_I, zeroMdd)) {
827    mdd_free(oneMdd);
828    mdd_free(zeroMdd);
829    P = Mc_ComputeACloseState(T_I, T, modelFsm);
830    mdd_free(T_I);
831    array_insert_last(mdd_t *, path, P);
832    return(path);
833  }
834  mdd_free(T_I);
835
836  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
837  invariantStates = mdd_zero(mgr);
838  layer = NULL;
839  Lm = NULL;
840  for(m=0; m<array_n(L); m++) {
841    layer = array_fetch(mdd_t *, L, m);
842    nLayer = bdd_smooth_with_cube(layer, extCube);
843    nInvariantStates = mdd_or(invariantStates, nLayer, 1, 1);
844    mdd_free(nLayer);
845    mdd_free(invariantStates);
846    invariantStates = nInvariantStates;
847    Lm = mdd_and(I, layer, 1, 1);
848    if(!mdd_equal(Lm, zeroMdd)) {
849      break;
850    }
851    mdd_free(Lm);
852  }
853
854  R = Mc_BuildBackwardRingsWithInvariants(Lm, T, invariantStates, modelFsm);
855
856  imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
857  Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
858  /**
859  Img_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, layer);
860  **/
861
862  i = m;
863  Q = mdd_and(I, Lm, 1, 1);
864  ring_Q = NULL;
865  for(q=0; q<array_n(R); q++) {
866    ring = array_fetch(mdd_t *, R, q);
867    ring_Q = mdd_and(ring, Q, 1, 1);
868    if(!mdd_equal(ring_Q, zeroMdd)) {
869      break;
870    }
871    mdd_free(ring_Q);
872  }
873  mdd_free(Q);
874  P = Mc_ComputeACloseState(ring_Q, T, modelFsm);
875  mdd_free(ring_Q);
876
877  free = 0;
878  careStatesArray = array_alloc(mdd_t *, 0);
879  array_insert_last(mdd_t *, careStatesArray, oneMdd);
880  while(1) {
881    Q = Img_ImageInfoComputeImageWithDomainVars(
882                               imageInfo, P, P, careStatesArray);
883    Q_T = mdd_and(Q, P, 1, 0);
884    mdd_free(Q);
885    Q = Q_T;
886
887    if(i>0) {
888      Li = array_fetch(mdd_t *, L, i-1);
889      nLi = bdd_smooth_with_cube(Li, extCube);
890      Q_Li = mdd_and(Q, nLi, 1, 1);
891      mdd_free(nLi);
892      if(!mdd_equal(Q_Li, zeroMdd)) {
893        i--;
894        mdd_free(Q);
895        Q = Q_Li;
896        free = 1;
897        imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
898        Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
899        Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
900        /**
901        Fsm_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
902        Fsm_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, Li);
903        **/
904      }
905    }
906
907    ring_Q = NULL;
908    for(q=0; q<array_n(R); q++) {
909      ring = array_fetch(mdd_t *, R, q);
910      ring_Q = mdd_and(ring, Q, 1, 1);
911      if(!mdd_equal(ring_Q, zeroMdd)) {
912          break;
913      }
914      mdd_free(ring_Q);
915    }
916    mdd_free(Q);
917
918    if(q >= array_n(R)) {
919      imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
920      Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
921      /**
922      Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
923      **/
924      continue;
925    }
926
927    Q = Mc_ComputeACloseState(ring_Q, T, modelFsm);
928    mdd_free(ring_Q);
929
930    if(free == 0) {
931      array_insert_last(mdd_t *, path, (mdd_t *)((long)P+1));
932    }
933    else if(free ==1) {
934      array_insert_last(mdd_t *, path, P);
935      free = 0;
936    }
937
938    Q_T = mdd_and(Q, T, 1, 1);
939    if(!mdd_equal(Q_T, zeroMdd)) {
940      array_insert_last(mdd_t *, path, (mdd_t *)((long)Q+1));
941      mdd_free(Q_T);
942      break;
943    }
944    mdd_free(Q_T);
945
946    P = Q;
947  }
948
949  array_free(careStatesArray);
950  mdd_free(oneMdd);
951  mdd_free(zeroMdd);
952
953  imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
954  Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
955  /**
956  Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
957  **/
958  return(path);
959}
960
961/**Function********************************************************************
962
963  Synopsis [Build a fate and free will layer.]
964
965  Description [Build a fate and free will layer.
966               This is function for FateAndFreeWill counterexample generation.]
967
968  SideEffects []
969
970******************************************************************************/
971array_t *
972Mc_BuildFAFWLayer(Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H)
973{
974  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
975  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
976  mdd_t *zeroMdd, *oneMdd;
977  mdd_t *S, *nH, *EX_S, *extCube, *S_new;
978  array_t *L;
979  array_t *careStatesArray;
980
981  zeroMdd = mdd_zero(mgr);
982  oneMdd = mdd_one(mgr);
983  L = array_alloc(mdd_t *, 0);
984
985  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
986  careStatesArray = array_alloc(mdd_t *, 0);
987  array_insert_last(mdd_t *, careStatesArray, oneMdd);
988  while(!mdd_equal(H, zeroMdd)) {
989      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
990      S = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
991                                   NIL(mdd_t), oneMdd, careStatesArray,
992                                   MC_NO_EARLY_TERMINATION, NIL(array_t),
993                                   Mc_None_c, 0, McVerbosityNone_c,
994                                   McDcLevelNone_c, NIL(boolean));
995      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);
996      array_insert_last(mdd_t *, L, S);
997
998      S_new = bdd_smooth_with_cube(S, extCube);
999      mdd_free(S);
1000      nH = mdd_and(H, S_new, 1, 0);
1001
1002      if(mdd_equal(H, nH)) {
1003        mdd_free(nH);
1004        mdd_free(S_new);
1005        break;
1006      }
1007      mdd_free(H);
1008      H = nH;
1009      mdd_free(T);
1010      EX_S = Img_ImageInfoComputePreImageWithDomainVars(
1011                                imageInfo, S_new, S_new, careStatesArray);
1012      mdd_free(S_new);
1013      T = mdd_and(EX_S, H, 1, 1);
1014  }
1015  array_free(careStatesArray);
1016  mdd_free(zeroMdd);
1017  mdd_free(oneMdd);
1018  mdd_free(T);
1019  mdd_free(H);
1020
1021  return(L);
1022}
1023
1024/**Function********************************************************************
1025
1026  Synopsis [Build a path from target to initial state.]
1027
1028  Description [Build a path from target to initial state.
1029               This is function for FateAndFreeWill counterexample generation.]
1030
1031  SideEffects []
1032
1033******************************************************************************/
1034array_t *
1035Mc_BuildPathFromCoreFAFW(
1036  mdd_t *Ts,
1037  array_t *rings,
1038  Fsm_Fsm_t *modelFsm,
1039  Mc_PathLengthType PathLengthType)
1040{
1041  int startingPoint, prevFlag;
1042  int i, p, dist, forced;
1043  bdd_t *T, *S, *H, *nH, *Hp, *S1, *Swin;
1044  bdd_t *ring, *oneMdd, *zeroMdd;
1045  array_t *C, *newC, *AUrings, *segment;
1046  array_t *R, *ESrings;
1047  array_t *careStatesArray;
1048  array_t *pathFromCore;
1049  bdd_t *T_wedge_ring, *S1_wedge_ring, *Hp_wedge_S1;
1050  bdd_t *T_wedge_S, *C_T_wedge_S, *ESresult, *EX_T;
1051  bdd_t *EX_T_wedge_ring, *Hp_wedge_EX_T, *lastR;
1052  bdd_t *C_T_wedge_ring, *new_, *extCube;
1053  bdd_t *bundle, *single, *preSingle;
1054  Img_ImageInfo_t *imageInfo;
1055  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
1056
1057  if(Fsm_FsmReadFAFWFlag(modelFsm) == 2) {
1058      pathFromCore = Mc_BuildPathFromCoreFAFWGeneral(
1059                            Ts, rings,
1060                            modelFsm, PathLengthType);
1061      return(pathFromCore);
1062  }
1063
1064  T = mdd_dup(Ts);
1065  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
1066  if ( PathLengthType == McGreaterZero_c ) {
1067    startingPoint = 1;
1068  }
1069  else if( PathLengthType == McGreaterOrEqualZero_c ) {
1070    startingPoint = 0;
1071  }
1072  else {
1073    fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
1074  }
1075
1076  oneMdd = mdd_one(mgr);
1077  zeroMdd = mdd_zero(mgr);
1078  S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));
1079  prevFlag = 0; /** free **/
1080
1081  H = mdd_zero(mgr);
1082  for(i=startingPoint; i<array_n(rings); i++) {
1083    ring = array_fetch(mdd_t *, rings, i);
1084    new_ = mdd_and(ring, H, 1, 0);
1085    mdd_free(ring);
1086    nH = mdd_or(new_, H, 1, 1);
1087    mdd_free(H);
1088    H = nH;
1089    array_insert(mdd_t *, rings, i, new_);
1090  }
1091
1092  C = array_alloc(mdd_t *, 0);
1093  T_wedge_S = mdd_and(T, S, 1, 1);
1094  if(!mdd_equal(T_wedge_S, zeroMdd)) {
1095    if(startingPoint == 1) {
1096      mdd_free(T);
1097      T = array_fetch(mdd_t *, rings, 0);
1098      array_insert_last(mdd_t *, C, bdd_dup(T));
1099    }
1100    C_T_wedge_S = bdd_closest_cube(T_wedge_S, S, &dist);
1101    array_insert_last(mdd_t *, C, C_T_wedge_S);
1102    mdd_free(S);
1103    mdd_free(oneMdd);
1104    mdd_free(zeroMdd);
1105    mdd_free(H);
1106    mdd_free(T_wedge_S);
1107
1108    return(C);
1109  }
1110  mdd_free(T_wedge_S);
1111
1112  T_wedge_ring = NULL;
1113  for(p=startingPoint; p<array_n(rings); p++) {
1114    ring = array_fetch(mdd_t *, rings, p);
1115    T_wedge_ring = mdd_and(T, ring, 1, 1);
1116    if(!mdd_equal(T_wedge_ring, zeroMdd)) {
1117      break;
1118    }
1119    mdd_free(T_wedge_ring);
1120  }
1121  mdd_free(T);
1122
1123  C_T_wedge_ring = bdd_closest_cube(T_wedge_ring, S, &dist);
1124  mdd_free(T_wedge_ring);
1125  array_insert_last(mdd_t *, C, C_T_wedge_ring);
1126  T = C_T_wedge_ring;
1127
1128  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
1129  careStatesArray = array_alloc(mdd_t *, 0);
1130  array_insert_last(mdd_t *, careStatesArray, oneMdd);
1131  while(1) {
1132    if(prevFlag == 0) { /* free segement */
1133      prevFlag = 1; /* force segment */
1134
1135      for(i=array_n(rings)-1; i>p; i--) {
1136        ring = array_fetch(mdd_t *, rings, i);
1137        nH = mdd_and(H, ring, 1, 0);
1138        mdd_free(H);
1139        H = nH;
1140      }
1141
1142      AUrings = array_alloc(mdd_t *, 0);
1143      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
1144      Swin = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
1145                                   NIL(mdd_t), oneMdd, careStatesArray,
1146                                   MC_NO_EARLY_TERMINATION, NIL(array_t),
1147                                   Mc_None_c, AUrings, McVerbosityNone_c,
1148                                   McDcLevelNone_c, NIL(boolean));
1149      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);
1150
1151
1152      S1 = bdd_smooth_with_cube(Swin, extCube);
1153      mdd_array_free(AUrings);
1154      if(mdd_equal(S1, T)) {
1155        mdd_free(S1);
1156        mdd_free(Swin);
1157        continue;
1158      }
1159
1160      for(i=p-1; i>=startingPoint; i--) {
1161        ring = array_fetch(mdd_t *, rings, i);
1162        S1_wedge_ring = mdd_and(S1, ring, 1, 1);
1163        if(mdd_equal(S1_wedge_ring, zeroMdd)) {
1164          mdd_free(S1_wedge_ring);
1165          break;
1166        }
1167        mdd_free(S1_wedge_ring);
1168      }
1169      p = i+1;
1170      Hp = array_fetch(mdd_t *, rings, p);
1171
1172      ESrings = array_alloc(mdd_t *, 0);
1173      Hp_wedge_S1 = mdd_and(Hp, S1, 1, 1);
1174
1175      ESresult = McEvaluateESFormulaWithGivenTRFAFW( modelFsm, S1, Hp_wedge_S1,
1176                                       NIL(mdd_t), oneMdd, careStatesArray,
1177                                       MC_NO_EARLY_TERMINATION, ESrings,
1178                                       McVerbosityNone_c, McDcLevelNone_c,
1179                                       NIL(boolean), Swin);
1180      mdd_free(ESresult);
1181      mdd_free(Hp_wedge_S1);
1182      mdd_free(S1);
1183      R = ESrings;
1184      if(array_n(R) <= 1) {
1185        mdd_array_free(R);
1186        mdd_free(Swin);
1187        continue;
1188      }
1189    }
1190    else { /* force segment */
1191      Swin = 0;
1192      prevFlag = 0; /* free segment */
1193      EX_T = Img_ImageInfoComputePreImageWithDomainVars(
1194                                imageInfo, T, T, careStatesArray);
1195
1196      for(i=p-1; i>=startingPoint; i--) {
1197        ring = array_fetch(mdd_t *, rings, i);
1198        EX_T_wedge_ring = mdd_and(EX_T, ring, 1, 1);
1199        if(mdd_equal(EX_T_wedge_ring, zeroMdd)) {
1200          mdd_free(EX_T_wedge_ring);
1201          break;
1202        }
1203        mdd_free(EX_T_wedge_ring);
1204      }
1205      p = i+1;
1206
1207      Hp = array_fetch(mdd_t *, rings, p);
1208      R = array_alloc(mdd_t *, 0);
1209      Hp_wedge_EX_T = mdd_and(Hp, EX_T, 1, 1);
1210      array_insert_last(mdd_t *, R, Hp_wedge_EX_T);
1211      /**array_insert_last(mdd_t *, R, T); **/
1212      array_insert_last(mdd_t *, R, mdd_dup(T));
1213      mdd_free(EX_T);
1214    }
1215
1216    lastR = array_fetch(mdd_t *, R, 0);
1217    segment = Mc_BuildShortestPathFAFW(Swin, lastR, T, R, mgr, modelFsm, prevFlag);
1218    if(Swin)    {
1219      mdd_free(Swin);
1220      Swin = 0;
1221    }
1222    mdd_array_free(R);
1223
1224    newC = array_join(C, segment);
1225    array_free(C);
1226    C = newC;
1227
1228    T = array_fetch(mdd_t *, segment, array_n(segment)-1);
1229    if((long)T %2) T = (mdd_t *)((long)T - 1);
1230/**    T = mdd_dup(T); **/
1231    array_free(segment);
1232
1233    T_wedge_S = mdd_and(T, S, 1, 1);
1234    if(!mdd_equal(T_wedge_S, zeroMdd)) {
1235      mdd_free(T_wedge_S);
1236/**      mdd_free(T);  **/
1237      mdd_free(S);
1238      mdd_free(H);
1239      break;
1240    }
1241    mdd_free(T_wedge_S);
1242
1243    startingPoint = 0;
1244    mdd_free(S);
1245    S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));
1246
1247  }
1248
1249  array_free(careStatesArray);
1250  mdd_free(oneMdd);
1251  mdd_free(zeroMdd);
1252
1253  {
1254    int i;
1255    pathFromCore = array_alloc( mdd_t *, 0 );
1256
1257    if(startingPoint == 1) {
1258      T = array_fetch(mdd_t *, rings, 0);
1259      array_insert_last(mdd_t *, pathFromCore, bdd_dup(T));
1260    }
1261
1262    preSingle = NULL;
1263    for( i=0; i < array_n( C ); i++ ) {
1264      bundle = array_fetch(mdd_t *, C, (array_n(C) - (i+1)));
1265      forced = 0;
1266      if((long)bundle%2) {
1267        bundle = (mdd_t *)((long)bundle -1);
1268        forced++;
1269      }
1270      if(i==0)
1271        single = Mc_ComputeAState(bundle, modelFsm);
1272      else
1273        single = Mc_ComputeACloseState(bundle, preSingle, modelFsm);
1274      array_insert_last( mdd_t *, pathFromCore,
1275              (mdd_t *)((long)(single) + forced) );
1276      preSingle = single;
1277    }
1278    McNormalizeBddPointer(C);
1279    mdd_array_free(C);
1280    return pathFromCore;
1281  }
1282}
1283
1284/**Function********************************************************************
1285
1286  Synopsis [Build a shortest path from T to S.]
1287
1288  Description [Make a shortest path from T to S which only passes through
1289               states in rings. There is always a path from T to S.
1290               Returns a sequence of states starting from T, leading to S.
1291               It is the users responsibility to free the returned
1292               array as well as its members.
1293               This is function for FateAndFreeWill counterexample generation.]
1294
1295  SideEffects []
1296
1297******************************************************************************/
1298array_t *
1299Mc_BuildShortestPathFAFW(mdd_t *win,
1300                         mdd_t *S,
1301                         mdd_t *T,
1302                         array_t *rings,
1303                         mdd_manager *mgr,
1304                         Fsm_Fsm_t *fsm,
1305                         int prevFlag)
1306{
1307  int q, dist;
1308  mdd_t *zeroMdd, *oneMdd;
1309  mdd_t *inputCube;
1310  mdd_t *ring, *ring_wedge_T, *Cn, *Cs;
1311  mdd_t *K, *realK, *range;
1312  mdd_t *preimage_of_Cn;
1313  array_t *C, *stateVars, *inputVars;
1314  array_t *toCareSetArray;
1315  Img_ImageInfo_t *imageInfo;
1316
1317  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 1, 0);
1318  stateVars = Fsm_FsmReadPresentStateVars(fsm);
1319  inputVars = Fsm_FsmReadInputVars(fsm);
1320  inputCube = mdd_id_array_to_bdd_cube(mgr, inputVars);
1321  zeroMdd = mdd_zero(mgr);
1322  oneMdd = mdd_one(mgr);
1323  ring_wedge_T = NULL;
1324  for (q = 0; q < array_n(rings); q++){
1325    ring = array_fetch(mdd_t *, rings, q);
1326    ring_wedge_T = mdd_and(T, ring, 1, 1);
1327    if(!mdd_equal(ring_wedge_T, zeroMdd))
1328      break;
1329    mdd_free(ring_wedge_T);
1330    ring_wedge_T = 0;
1331  }
1332  if(ring_wedge_T) {
1333    mdd_free(ring_wedge_T);
1334  }
1335  else {
1336    fprintf(stdout, "We cannot find T\n");
1337  }
1338
1339  C = array_alloc(mdd_t *, 0);
1340  Cn = (T);
1341  toCareSetArray = array_alloc(mdd_t *, 0);
1342  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
1343  range = mdd_range_mdd(mgr, stateVars);
1344  while(q > 0) {
1345    preimage_of_Cn = Img_ImageInfoComputePreImageWithDomainVars(
1346                                imageInfo, Cn, Cn, toCareSetArray);
1347
1348    K = NULL;
1349    for (q = 0; q < array_n(rings); q++){
1350      ring = array_fetch(mdd_t *, rings, q);
1351      K = mdd_and(preimage_of_Cn, ring, 1, 1);
1352      if(!mdd_equal(K, zeroMdd))
1353        break;
1354      mdd_free(K);
1355      K = 0;
1356    }
1357
1358    mdd_free(preimage_of_Cn);
1359    realK = mdd_and(K, range, 1, 1);
1360    mdd_free(K);
1361    Cs = bdd_closest_cube(realK, Cn, &dist);
1362    mdd_free(realK);
1363
1364
1365    Cn = bdd_smooth_with_cube(Cs, inputCube);
1366    mdd_free(Cs);
1367    if(!prevFlag) /** free segment **/
1368      array_insert_last(mdd_t *, C, Cn);
1369    else          /** fated segment **/
1370      array_insert_last(mdd_t *, C, (mdd_t *)((long)Cn+1));
1371  }
1372  array_free(toCareSetArray);
1373  mdd_free(zeroMdd);
1374  mdd_free(oneMdd);
1375  mdd_free(range);
1376  mdd_free(inputCube);
1377  return(C);
1378}
1379
1380
1381
1382/**Function********************************************************************
1383
1384  Synopsis [Make a path from aState to bState.]
1385
1386  Description [Make a path from aState to bState which only passes through
1387  invariantStates; it is assumed that aState and bState lie in invariantStates.
1388  Returns a sequence of states starting from aState, leading to bState. If
1389  aState == bState, a non trivial path is returned (ie a cycle). If no
1390  path exists, return NIL. It is the users responsibility to free the returned
1391  array as well as its members.]
1392
1393  SideEffects []
1394
1395******************************************************************************/
1396array_t *
1397Mc_CompletePath(
1398  mdd_t *aState,
1399  mdd_t *bState,
1400  mdd_t *invariantStates,
1401  Fsm_Fsm_t *modelFsm,
1402  array_t *careSetArray,
1403  Mc_VerbosityLevel verbosity,
1404  Mc_DcLevel dcLevel,
1405  Mc_FwdBwdAnalysis dirn)
1406{
1407
1408  if ( dirn == McFwd_c )  {
1409    return McCompletePathFwd(aState, bState, invariantStates, modelFsm,
1410                             careSetArray, verbosity, dcLevel );
1411  }
1412  else {
1413    return McCompletePathBwd(aState, bState, invariantStates, modelFsm,
1414                             careSetArray, verbosity, dcLevel );
1415  }
1416}
1417
1418/**Function********************************************************************
1419
1420  Synopsis [Pick an arbitrary minterm from the given set.]
1421
1422  Description [Pick an arbitrary minterm from the given set. Support is an
1423  array of mddids representing the total support; that is, all the variables
1424  on which aSet may depend.]
1425
1426  SideEffects []
1427
1428******************************************************************************/
1429mdd_t *
1430Mc_ComputeAMinterm(
1431  mdd_t *aSet,
1432  array_t *Support,
1433  mdd_manager *mddMgr)
1434{
1435  /* check that support of set is contained in Support */
1436  assert( SetCheckSupport( aSet, Support, mddMgr ));
1437  assert(!mdd_is_tautology(aSet, 0));
1438
1439  if(bdd_get_package_name() == CUDD){
1440    mdd_t *range;             /* range of Support             */
1441    mdd_t *legalSet;          /* aSet without the don't cares */
1442    array_t *bddSupport;      /* Support in terms of bdd vars */
1443    mdd_t *minterm;           /* a random minterm             */
1444
1445    range      = mdd_range_mdd(mddMgr, Support);
1446    legalSet   = bdd_intersects(aSet, range);
1447    mdd_free(range);
1448    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
1449    minterm    = bdd_pick_one_minterm(legalSet, bddSupport);
1450
1451    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
1452    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
1453    assert(mdd_lequal(minterm,legalSet,1,1));
1454
1455    mdd_array_free(bddSupport);
1456    mdd_free(legalSet);
1457
1458    return minterm;
1459  }else{
1460    int i, j;
1461    mdd_t *aSetDup;
1462    mdd_t *resultMdd;
1463    array_t *resultMddArray = array_alloc( mdd_t *, 0 );
1464
1465    aSetDup = mdd_dup( aSet );
1466    for( i = 0 ; i < array_n( Support ); i++ ) {
1467
1468      int aSupportVar = array_fetch( int, Support, i );
1469
1470      for( j = 0 ;;) {
1471        mdd_t *faceMdd, *tmpMdd;
1472        array_t *tmpArray = array_alloc( int, 0 );
1473        array_insert_last( int, tmpArray, j );
1474
1475        /* this call will crash if have run through range of mvar */
1476        faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
1477        array_free( tmpArray );
1478        tmpMdd = mdd_and( faceMdd, aSetDup, 1, 1 );
1479
1480        if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
1481          array_insert_last( mdd_t *, resultMddArray, faceMdd );
1482          mdd_free( aSetDup );
1483          aSetDup = tmpMdd;
1484          break;
1485        }
1486        mdd_free( faceMdd );
1487        mdd_free( tmpMdd );
1488        j++;
1489      }
1490    }
1491    mdd_free( aSetDup );
1492
1493    resultMdd = mdd_one( mddMgr );
1494    for ( i = 0 ; i < array_n( resultMddArray ); i++ ) {
1495      mdd_t *faceMdd = array_fetch( mdd_t *, resultMddArray, i );
1496      mdd_t *tmpMdd = mdd_and( faceMdd, resultMdd, 1, 1 );
1497      mdd_free( resultMdd ); mdd_free( faceMdd );
1498      resultMdd = tmpMdd;
1499    }
1500    array_free( resultMddArray );
1501
1502    return resultMdd;
1503  }/* IF CUDD */
1504}
1505
1506
1507/**Function********************************************************************
1508
1509  Synopsis [Pick a minterm from the given set close to target. Support
1510  is an array of mddids representing the total support; that is, all
1511  the variables on which aSet may depend.]
1512
1513  SideEffects []
1514
1515******************************************************************************/
1516mdd_t *
1517Mc_ComputeACloseMinterm(
1518  mdd_t *aSet,
1519  mdd_t *target,
1520  array_t *Support,
1521  mdd_manager *mddMgr)
1522{
1523  if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
1524    mdd_t *range;             /* range of Support             */
1525    mdd_t *legalSet;          /* aSet without the don't cares */
1526    mdd_t *closeCube;
1527    int dist;
1528    array_t *bddSupport;      /* Support in terms of bdd vars */
1529    mdd_t *minterm;           /* a random minterm             */
1530
1531    /* Check that support of set is contained in Support. */
1532    assert(SetCheckSupport(aSet, Support, mddMgr));
1533    assert(!mdd_is_tautology(aSet, 0));
1534    range      = mdd_range_mdd(mddMgr, Support);
1535    legalSet   = bdd_and(aSet, range, 1, 1);
1536    mdd_free(range);
1537    closeCube = mdd_closest_cube(legalSet, target, &dist);
1538    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
1539    minterm    = bdd_pick_one_minterm(closeCube, bddSupport);
1540
1541    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
1542    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
1543    assert(mdd_lequal(minterm,legalSet,1,1));
1544
1545    mdd_array_free(bddSupport);
1546    mdd_free(legalSet);
1547    mdd_free(closeCube);
1548
1549    return minterm;
1550  } else {
1551    return Mc_ComputeAMinterm(aSet, Support, mddMgr);
1552  }/* if CUDD */
1553
1554} /* McComputeACloseMinterm */
1555
1556
1557
1558
1559/**Function********************************************************************
1560
1561  Synopsis [Return a string for a minterm.]
1562
1563  SideEffects []
1564
1565******************************************************************************/
1566char *
1567Mc_MintermToStringAiger(
1568  mdd_t *aMinterm,
1569  array_t *aSupport,
1570  Ntk_Network_t *aNetwork)
1571{
1572  int i;
1573  char *tmp1String;
1574  char *tmp2String;
1575  char bodyString[McMaxStringLength_c];
1576  char *mintermString = NIL(char);
1577  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
1578  array_t *valueArray;
1579  array_t *stringArray = array_alloc( char *, 0 );
1580
1581  aMinterm = GET_NORMAL_PT(aMinterm);
1582  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
1583  for ( i = 0 ; i < array_n( aSupport ); i++ ) {
1584
1585    int mddId = array_fetch( int, aSupport, i );
1586    int value = array_fetch( int, valueArray, i );
1587    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
1588    char *nodeName = Ntk_NodeReadName( node );
1589    if(!((nodeName[0] == '$') && (nodeName[1] == '_')))
1590    {
1591      Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
1592
1593      if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
1594        char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
1595                                                                   value );
1596        sprintf( bodyString, "%s", symbolicValue );
1597      }
1598      else {
1599        sprintf( bodyString, "%d", value );
1600      }
1601      tmp1String = util_strsav( bodyString );
1602      array_insert_last( char *, stringArray, tmp1String );
1603    }
1604  }
1605  array_free(valueArray);
1606
1607  array_sort( stringArray, cmp);
1608
1609  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
1610    tmp1String = array_fetch( char *, stringArray, i );
1611    if( i == 0 )  {
1612      mintermString = util_strcat3(tmp1String, "", "" );
1613    }
1614    else {
1615      tmp2String = util_strcat3(mintermString, "", tmp1String );
1616      FREE(mintermString);
1617      mintermString = tmp2String;
1618    }
1619    FREE(tmp1String);
1620  }
1621  array_free( stringArray );
1622
1623  tmp1String = util_strcat3(mintermString, " ", "");
1624  FREE(mintermString);
1625  mintermString = tmp1String;
1626
1627  return mintermString;
1628}
1629
1630
1631/**Function********************************************************************
1632
1633  Synopsis [Return a string for a minterm.]
1634
1635  SideEffects []
1636
1637******************************************************************************/
1638char *
1639Mc_MintermToStringAigerInput(
1640  mdd_t *aMinterm,
1641  array_t *aSupport,
1642  Ntk_Network_t *aNetwork)
1643{
1644  int i;
1645  char *tmp1String;
1646  char *tmp2String;
1647  char bodyString[McMaxStringLength_c];
1648  char *mintermString = NIL(char);
1649  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
1650  array_t *valueArray;
1651  array_t *stringArray = array_alloc( char *, 0 );
1652
1653  aMinterm = GET_NORMAL_PT(aMinterm);
1654  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
1655  for ( i = 0 ; i < array_n( aSupport ); i++ ) {
1656
1657    int mddId = array_fetch( int, aSupport, i );
1658    int value = array_fetch( int, valueArray, i );
1659    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
1660    char *nodeName = Ntk_NodeReadName( node );
1661    if((nodeName[0] == '$') && (nodeName[1] == '_'))
1662    {
1663      Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
1664
1665      if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
1666        char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
1667                                                                   value );
1668        sprintf( bodyString, "%s", symbolicValue );
1669      }
1670      else {
1671        sprintf( bodyString, "%d", value );
1672      }
1673      tmp1String = util_strsav( bodyString );
1674      array_insert_last( char *, stringArray, tmp1String );
1675    }
1676  }
1677  array_free(valueArray);
1678
1679  array_sort( stringArray, cmp);
1680
1681  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
1682    tmp1String = array_fetch( char *, stringArray, i );
1683    if( i == 0 )  {
1684      mintermString = util_strcat3(tmp1String, "", "" );
1685    }
1686    else {
1687      tmp2String = util_strcat3(mintermString, "", tmp1String );
1688      FREE(mintermString);
1689      mintermString = tmp2String;
1690    }
1691    FREE(tmp1String);
1692  }
1693  array_free( stringArray );
1694
1695  tmp1String = util_strcat3(mintermString, " ", "");
1696  FREE(mintermString);
1697  mintermString = tmp1String;
1698
1699  return mintermString;
1700}
1701
1702/**Function********************************************************************
1703
1704  Synopsis [Return a string for a minterm.]
1705
1706  SideEffects []
1707
1708******************************************************************************/
1709char *
1710Mc_MintermToString(
1711  mdd_t *aMinterm,
1712  array_t *aSupport,
1713  Ntk_Network_t *aNetwork)
1714{
1715  int i;
1716  char *tmp1String;
1717  char *tmp2String;
1718  char bodyString[McMaxStringLength_c];
1719  char *mintermString = NIL(char);
1720  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
1721  array_t *valueArray;
1722  array_t *stringArray = array_alloc( char *, 0 );
1723
1724  aMinterm = GET_NORMAL_PT(aMinterm);
1725  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
1726  for ( i = 0 ; i < array_n( aSupport ); i++ ) {
1727
1728    int mddId = array_fetch( int, aSupport, i );
1729    int value = array_fetch( int, valueArray, i );
1730    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
1731    char *nodeName = Ntk_NodeReadName( node );
1732    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
1733
1734    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
1735      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
1736                                                                   value );
1737      sprintf( bodyString, "%s:%s", nodeName, symbolicValue );
1738    }
1739    else {
1740      sprintf( bodyString, "%s:%d", nodeName, value );
1741    }
1742    tmp1String = util_strsav( bodyString );
1743    array_insert_last( char *, stringArray, tmp1String );
1744  }
1745  array_free(valueArray);
1746
1747  array_sort( stringArray, cmp);
1748
1749  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
1750    tmp1String = array_fetch( char *, stringArray, i );
1751    if( i == 0 )  {
1752      mintermString = util_strcat3(tmp1String, "", "" );
1753    }
1754    else {
1755      tmp2String = util_strcat3(mintermString, "\n", tmp1String );
1756      FREE(mintermString);
1757      mintermString = tmp2String;
1758    }
1759    FREE(tmp1String);
1760  }
1761  array_free( stringArray );
1762
1763  tmp1String = util_strcat3(mintermString, "\n", "");
1764  FREE(mintermString);
1765  mintermString = tmp1String;
1766
1767  return mintermString;
1768}
1769
1770/**Function********************************************************************
1771
1772  Synopsis [Utility function - prints states on path, inputs for transitions]
1773
1774  SideEffects []
1775
1776******************************************************************************/
1777int
1778Mc_PrintPath(
1779  array_t *aPath,
1780  Fsm_Fsm_t *modelFsm,
1781  boolean printInput)
1782{
1783  int check, forced, i;
1784  int numForced;
1785  mdd_t *inputSet=NIL(mdd_t);
1786  mdd_t *uInput = NIL(mdd_t);
1787  mdd_t *vInput = NIL(mdd_t);
1788
1789  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
1790  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
1791  mdd_manager *mddMgr =  Fsm_FsmReadMddManager( modelFsm );
1792
1793  forced = 0;
1794  check = 1;
1795  numForced = 0;
1796
1797
1798  for( i = -1 ; i < (array_n( aPath )-1); i++ ) {
1799
1800    mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
1801    mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );
1802
1803    if((long)aState%2) {
1804      aState = (mdd_t *)((long)aState -1);
1805      forced++;
1806    }
1807    else        forced = 0;
1808
1809    if((long)bState%2) {
1810      bState = (mdd_t *)((long)bState -1);
1811    }
1812
1813    if ( printInput == TRUE && i != -1) {
1814      inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, aState, bState );
1815      vInput = Mc_ComputeACloseMinterm( inputSet, uInput, inputVars, mddMgr );
1816    }
1817    if(forced)  {
1818      fprintf(vis_stdout, "---- Forced %d\n", forced);
1819      numForced ++;
1820    }
1821    McPrintTransition( aState, bState, uInput, vInput, psVars, inputVars,
1822                       printInput, modelFsm, (i+1) );
1823
1824
1825    if ( uInput != NIL(mdd_t) ) {
1826      mdd_free(uInput);
1827    }
1828    uInput = vInput;
1829
1830    if ( inputSet != NIL(mdd_t) ) {
1831      mdd_free(inputSet);
1832    }
1833  }
1834
1835  if ( vInput != NIL(mdd_t) ) {
1836    mdd_free(uInput);
1837  }
1838
1839  if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
1840    fprintf(vis_stdout,
1841        "# MC: the number of non-trivial forced segments %d\n",
1842        numForced);
1843  }
1844
1845  return 1;
1846}
1847
1848/**Function********************************************************************
1849
1850  Synopsis [Utility function - prints states on path, inputs for transitions]
1851
1852  SideEffects []
1853
1854******************************************************************************/
1855int
1856Mc_PrintPathAiger(
1857  array_t *aPath,
1858  Fsm_Fsm_t *modelFsm,
1859  boolean printInput)
1860{
1861  int check, forced, i;
1862  int numForced;
1863  mdd_t *inputSet=NIL(mdd_t);
1864  mdd_t *uInput = NIL(mdd_t);
1865  mdd_t *vInput = NIL(mdd_t);
1866
1867  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
1868  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
1869
1870  forced = 0;
1871  check = 1;
1872  numForced = 0;
1873
1874  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
1875
1876  FILE *psO = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
1877  for(i=0; i<array_n(psVars); i++)
1878  {
1879    int mddId = array_fetch( int, psVars, i );
1880    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
1881    char *nodeName = Ntk_NodeReadName( node );
1882    if((nodeName[0] == '$') && (nodeName[1] == '_'))
1883    {
1884      fprintf(psO, "%s\n", &nodeName[2]);
1885    }
1886  }
1887  fclose(psO);
1888
1889  for( i = -1 ; i < (array_n( aPath )-1); i++ ) {
1890
1891    mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
1892    mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );
1893
1894    if((long)aState%2) {
1895      aState = (mdd_t *)((long)aState -1);
1896      forced++;
1897    }
1898    else        forced = 0;
1899
1900    if((long)bState%2) {
1901      bState = (mdd_t *)((long)bState -1);
1902    }
1903
1904    if(forced)  {
1905      fprintf(vis_stdout, "---- Forced %d\n", forced);
1906      numForced ++;
1907    }
1908
1909    /* The following fix is only for Sat-competition 2007 and will need to be fixed for future */
1910
1911    if(i == (array_n(aPath)-2))
1912    {
1913      McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
1914                       printInput, modelFsm, 1 );
1915    }
1916    else
1917    {
1918      McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
1919                       printInput, modelFsm, 0 );
1920    }
1921
1922
1923    if ( uInput != NIL(mdd_t) ) {
1924      mdd_free(uInput);
1925    }
1926    uInput = vInput;
1927
1928    if ( inputSet != NIL(mdd_t) ) {
1929      mdd_free(inputSet);
1930    }
1931  }
1932
1933  if ( vInput != NIL(mdd_t) ) {
1934    mdd_free(uInput);
1935  }
1936
1937  if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
1938    fprintf(vis_stdout,
1939        "# MC: the number of non-trivial forced segments %d\n",
1940        numForced);
1941  }
1942
1943  return 1;
1944}
1945
1946
1947/**Function********************************************************************
1948
1949  Synopsis    [Builds MVF for a node that is a pseudo input.]
1950
1951  Description [Builds MVF for a node that is a pseudo input.  This node has a
1952  single output and no inputs. Its table has several row entries.  We build an
1953  MVF whose components correspond exactly to possible table outputs.]
1954
1955  SideEffects []
1956
1957  Comment [Although pseudo inputs, constants, and internal nodes all have
1958  tables, a single procedure cannot be used to build their MVF.  A pseudo
1959  input MVF is built in terms of its mddId, whereas a constant or internal is
1960  not.  A constant or pseudo input doesn't have any inputs, whereas an
1961  internal does.]
1962
1963  SeeAlso     [Tbl_TableBuildMvfForNonDetConstant]
1964
1965******************************************************************************/
1966static Mvf_Function_t *
1967NodeBuildPseudoInputMvf(
1968  Ntk_Node_t * node,
1969  mdd_manager * mddMgr)
1970{
1971  Mvf_Function_t *mvf;
1972  int             columnIndex = Ntk_NodeReadOutputIndex(node);
1973  Tbl_Table_t    *table       = Ntk_NodeReadTable(node);
1974  int             mddId       = Ntk_NodeReadMddId(node);
1975
1976  assert(mddId != NTK_UNASSIGNED_MDD_ID);
1977  mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex, mddId, mddMgr);
1978  return mvf;
1979}
1980
1981/**Function********************************************************************
1982
1983  Synopsis [Return the range of pseudo inputs if they are defined by subsets of range.]
1984
1985  Description [The result can be used to extract correct input conditions.]
1986
1987  SideEffects []
1988
1989******************************************************************************/
1990static mdd_t *
1991Mc_ComputeRangeOfPseudoInputs(
1992  Ntk_Network_t *network)
1993{
1994  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( network );
1995  Mvf_Function_t *nodeMvf;
1996  mdd_t *tmpMdd, *zeroMdd;
1997  mdd_t *restrictMdd, *sumMdd;
1998  int restrictFlag;
1999  lsGen gen;
2000  Ntk_Node_t *node;
2001  int i;
2002
2003  zeroMdd = mdd_zero(mddMgr);
2004  restrictMdd = mdd_one(mddMgr);
2005  restrictFlag = 0;
2006  Ntk_NetworkForEachPseudoInput(network, gen, node) {
2007    nodeMvf = NodeBuildPseudoInputMvf(node, mddMgr);
2008    for(i=0; i<nodeMvf->num; i++) {
2009      tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
2010      if(mdd_equal(tmpMdd, zeroMdd)) {
2011        restrictFlag = 1;
2012        break;
2013      }
2014    }
2015    if(restrictFlag) {
2016      sumMdd = mdd_zero(mddMgr);
2017      for(i=0; i<nodeMvf->num; i++) {
2018        tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
2019        if(!mdd_equal(tmpMdd, zeroMdd)) {
2020          tmpMdd = mdd_or( sumMdd, tmpMdd, 1, 1 );
2021          mdd_free(sumMdd);
2022          sumMdd = tmpMdd;
2023        }
2024      }
2025      tmpMdd = mdd_and( sumMdd, restrictMdd, 1, 1 );
2026      mdd_free(sumMdd);
2027      mdd_free(restrictMdd);
2028      restrictMdd = tmpMdd;
2029    }
2030    Mvf_FunctionFree(nodeMvf);
2031  }
2032  mdd_free(zeroMdd);
2033
2034  return(restrictMdd);
2035}
2036
2037
2038/**Function********************************************************************
2039
2040  Synopsis [Return all inputs which cause a transition from aState to bState.]
2041
2042  Description [Return all inputs which cause a transition from aState to bState.
2043  It is assumed that aState,bState are truly minterms over the PS variables.]
2044
2045  SideEffects []
2046
2047******************************************************************************/
2048mdd_t *
2049Mc_FsmComputeDrivingInputMinterms(
2050  Fsm_Fsm_t *fsm,
2051  mdd_t *aState,
2052  mdd_t *bState )
2053{
2054  int i;
2055  int psMddId;
2056  int inputMddId;
2057  mdd_gen *mddGen;
2058  Ntk_Node_t *latch, *node, *dataNode;
2059  array_t *aMinterm, *bMinterm;
2060  mdd_t *resultMdd;
2061  array_t *resultMvfs;
2062  array_t *inputArray = Fsm_FsmReadInputVars( fsm );
2063  array_t *psArray = Fsm_FsmReadPresentStateVars( fsm );
2064  Ntk_Network_t *network = Fsm_FsmReadNetwork( fsm );
2065  st_table *leaves = st_init_table(st_ptrcmp, st_ptrhash);
2066  array_t *roots = array_alloc( Ntk_Node_t *, 0 );
2067  array_t *latches = array_alloc( Ntk_Node_t *, 0 );
2068  array_t *support = array_alloc( int, 0 );
2069  mdd_t *rangeOfPseudoInputs, *tmpMdd;
2070
2071  arrayForEachItem(int , psArray, i, psMddId ) {
2072    latch = Ntk_NetworkFindNodeByMddId( network, psMddId );
2073    dataNode = Ntk_LatchReadDataInput( latch );
2074    array_insert_last( int, support, psMddId );
2075    array_insert_last( Ntk_Node_t *, roots, dataNode );
2076    array_insert_last( Ntk_Node_t *, latches, latch );
2077  }
2078
2079  /* Convert the  minterm to an array of assignments to support vars. */
2080  foreach_mdd_minterm(aState, mddGen, aMinterm, support) {
2081    mdd_gen_free(mddGen);
2082    break;
2083    /* NOT REACHED */
2084  }
2085
2086  foreach_mdd_minterm(bState, mddGen, bMinterm, support) {
2087    mdd_gen_free(mddGen);
2088    break;
2089     /* NOT REACHED */
2090  }
2091  array_free( support );
2092
2093  arrayForEachItem(int , inputArray, i, inputMddId ) {
2094    node = Ntk_NetworkFindNodeByMddId( network, inputMddId );
2095    st_insert(leaves, (char *) node, (char *) NTM_UNUSED );
2096  }
2097
2098  for ( i = 0 ; i < array_n( roots ); i++ ) {
2099    int value = array_fetch( int, aMinterm, i );
2100    latch = array_fetch( Ntk_Node_t *, latches, i );
2101    st_insert( leaves, (char *) latch, (char *) (long) value );
2102  }
2103
2104  resultMvfs = Ntm_NetworkBuildMvfs( network, roots, leaves, NIL(mdd_t) );
2105
2106  array_free( roots );
2107  array_free( latches );
2108  st_free_table( leaves );
2109
2110  rangeOfPseudoInputs = Mc_ComputeRangeOfPseudoInputs(network);
2111
2112  resultMdd = rangeOfPseudoInputs;
2113  for ( i = 0 ; i < array_n( resultMvfs ) ; i++ ) {
2114    Mvf_Function_t *mvf = array_fetch( Mvf_Function_t *, resultMvfs, i );
2115    int value = array_fetch( int, bMinterm, i );
2116    mdd_t *activeMdd = Mvf_FunctionReadComponent( mvf, value );
2117    tmpMdd = mdd_and( activeMdd, resultMdd, 1, 1 );
2118    if(mdd_is_tautology(tmpMdd, 0)) {
2119        fprintf(stdout, "current error\n");
2120    }
2121    mdd_free( resultMdd );
2122    resultMdd = tmpMdd;
2123    Mvf_FunctionFree( mvf );
2124  }
2125  array_free( resultMvfs);
2126  array_free( aMinterm );
2127  array_free( bMinterm );
2128
2129  return resultMdd;
2130}
2131
2132
2133/**Function********************************************************************
2134
2135  Synopsis [Select an arbitrary  state from the given set]
2136
2137  SideEffects []
2138
2139******************************************************************************/
2140mdd_t *
2141Mc_ComputeAState(
2142  mdd_t *states,
2143  Fsm_Fsm_t *modelFsm)
2144{
2145  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
2146  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
2147  mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );
2148
2149  return result;
2150}
2151
2152
2153/**Function********************************************************************
2154
2155  Synopsis [Select a state from the given set close to target.]
2156
2157  SideEffects []
2158
2159******************************************************************************/
2160mdd_t *
2161Mc_ComputeACloseState(
2162  mdd_t *states,
2163  mdd_t *target,
2164  Fsm_Fsm_t *modelFsm)
2165{
2166  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
2167  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
2168  mdd_t *result = Mc_ComputeACloseMinterm( states, target, PSVars, mddMgr );
2169
2170  return result;
2171}
2172
2173
2174/**Function********************************************************************
2175
2176  Synopsis [Print a minterm.]
2177
2178  SideEffects []
2179
2180******************************************************************************/
2181void
2182Mc_MintermPrint(
2183  mdd_t *aMinterm,
2184  array_t *support,
2185  Ntk_Network_t *aNetwork)
2186{
2187  char *tmpString = Mc_MintermToString( aMinterm, support, aNetwork );
2188  fprintf( vis_stdout, "%s", tmpString );
2189  FREE(tmpString);
2190}
2191
2192/**Function********************************************************************
2193
2194  Synopsis [Add nodes for wires referred to in formula to nodesTable.]
2195
2196  SideEffects []
2197
2198******************************************************************************/
2199void
2200Mc_NodeTableAddCtlFormulaNodes(
2201  Ntk_Network_t *network,
2202  Ctlp_Formula_t *formula,
2203  st_table * nodesTable )
2204{
2205  NodeTableAddCtlFormulaNodes( network, formula, nodesTable );
2206}
2207
2208/**Function********************************************************************
2209
2210  Synopsis [Add nodes for wires referred to in formula to nodesTable.]
2211
2212  Description [Add nodes for wires referred to in formula to nodesTable.]
2213
2214  SideEffects []
2215
2216******************************************************************************/
2217void
2218Mc_NodeTableAddLtlFormulaNodes(
2219  Ntk_Network_t *network,
2220  Ctlsp_Formula_t *formula,
2221  st_table * nodesTable )
2222{
2223  NodeTableAddLtlFormulaNodes(network, formula, nodesTable);
2224}
2225
2226/**Function********************************************************************
2227
2228  Synopsis [Form an FSM reduced with respect to the specified formula]
2229
2230  Description [Form an FSM reduced with respect to the CTL formula array.
2231  All latches and inputs which affect the given formula AND the fairness
2232  conditions of the system are included in this reduced fsm.]
2233
2234  SideEffects []
2235
2236******************************************************************************/
2237Fsm_Fsm_t *
2238Mc_ConstructReducedFsm(
2239  Ntk_Network_t *network,
2240  array_t *ctlFormulaArray)
2241{
2242  return(McConstructReducedFsm(network, ctlFormulaArray));
2243}
2244
2245
2246/**Function********************************************************************
2247
2248  Synopsis    [Converts a string to a schedule type.]
2249
2250  Description [Converts a string to a schedule type.  If string does
2251  not refer to one of the allowed schedule types, then returns
2252  McGSH_Unassigned_c.]
2253
2254  SideEffects []
2255
2256******************************************************************************/
2257Mc_GSHScheduleType
2258Mc_StringConvertToScheduleType(
2259  char *string)
2260{
2261  return McStringConvertToScheduleType(string);
2262}
2263
2264/**Function********************************************************************
2265
2266  Synopsis    [Converts a string to a lockstep mode.]
2267
2268  Description [Converts a string to a lockstep mode.  If string does
2269  not refer to one of the allowed lockstep modes, it returns
2270  MC_LOCKSTEP_UNASSIGNED.  The allowed values are: MC_LOCKSTEP_OFF,
2271  MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive
2272  integer n (lockstep enumerates up to n fair SCCs).]
2273
2274  SideEffects []
2275
2276******************************************************************************/
2277int
2278Mc_StringConvertToLockstepMode(
2279  char *string)
2280{
2281  return McStringConvertToLockstepMode(string);
2282}
2283
2284
2285/**Function********************************************************************
2286
2287  Synopsis [Allocate an earlytermination struct and initialize with arguments]
2288
2289  SideEffects []
2290******************************************************************************/
2291Mc_EarlyTermination_t *
2292Mc_EarlyTerminationAlloc(
2293  Mc_EarlyTerminationType mode,
2294  mdd_t *states)
2295{
2296  Mc_EarlyTermination_t *result = ALLOC(Mc_EarlyTermination_t, 1);
2297
2298  result->mode   = mode;
2299  if (states != NIL(mdd_t)) {
2300    result->states = mdd_dup(states);
2301  } else {
2302    result->states = NIL(mdd_t);
2303  }
2304
2305  return result;
2306}
2307
2308/**Function********************************************************************
2309
2310  Synopsis [Free an earlytermination struct (you are allowed to pass
2311  MC_NO_EARLY_TERMINATION, or NULL, and it will have no effect. ]
2312
2313  SideEffects []
2314******************************************************************************/
2315void
2316Mc_EarlyTerminationFree(Mc_EarlyTermination_t *earlyTermination)
2317{
2318  if(earlyTermination == NIL(Mc_EarlyTermination_t) ||
2319     earlyTermination == MC_NO_EARLY_TERMINATION)
2320    return;
2321
2322  if(earlyTermination->states != NIL(mdd_t))
2323    mdd_free(earlyTermination->states);
2324
2325  free(earlyTermination);
2326
2327  return;
2328}
2329
2330/**Function********************************************************************
2331
2332  Synopsis [Return TRUE iff the early termination condition specifies that
2333  the computation can be entirely skipped.]
2334
2335  SideEffects [none]
2336******************************************************************************/
2337boolean
2338Mc_EarlyTerminationIsSkip(Mc_EarlyTermination_t *earlyTermination)
2339{
2340  if (earlyTermination == NIL(Mc_EarlyTermination_t) ||
2341     earlyTermination == MC_NO_EARLY_TERMINATION)
2342    return FALSE;
2343
2344  return (earlyTermination->mode == McCare_c &&
2345          earlyTermination->states == NIL(mdd_t));
2346
2347}
2348
2349/*---------------------------------------------------------------------------*/
2350/* Definition of internal functions                                          */
2351/*---------------------------------------------------------------------------*/
2352
2353/**Function********************************************************************
2354
2355  Synopsis [Make a path from aState to bState using fwd reachability.]
2356
2357  Description [Make a path from aState to bState which only passes through
2358  invariantStates; it is assumed that aState and bState lie in invariantStates.
2359  Returns a sequence of states starting from aState, leading to bState. If
2360  aState == bState, a non trivial path is returned (ie a cycle). If no
2361  path exists, return NIL. It is the users responsibility to free the returned
2362  array as well as its members. This function starts from aState and does
2363  forward reachability till it hits bState or a fixed point.]
2364
2365  SideEffects []
2366
2367******************************************************************************/
2368array_t *
2369McCompletePathFwd(
2370  mdd_t *aState,
2371  mdd_t *bState,
2372  mdd_t *invariantStates,
2373  Fsm_Fsm_t *modelFsm,
2374  array_t *careSetArray,
2375  Mc_VerbosityLevel verbosity,
2376  Mc_DcLevel dcLevel)
2377{
2378  mdd_t *tmp1Mdd;
2379  array_t *result;
2380  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
2381  mdd_t *zeroMdd = mdd_zero( mddMgr );
2382  array_t *onionRings = array_alloc( mdd_t *, 0 );
2383  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
2384  mdd_t *c0, *c1;
2385
2386  assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
2387  assert( mdd_lequal( bState, invariantStates, 1, 1 ) );
2388
2389  if ( mdd_equal( aState, bState ) ) {
2390
2391    /*
2392     * Alter the starting point to force routine to produce cycle if exists
2393     * Question: would it be quicker to do simultaneous backward/forward
2394     * analysis?
2395     */
2396
2397    c0 = mdd_dup( aState );
2398    array_insert_last( mdd_t *, onionRings, c0 );
2399
2400    tmp1Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
2401                aState, aState, careSetArray);
2402    c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
2403    mdd_free(tmp1Mdd);
2404    array_insert_last( mdd_t *, onionRings, c1 );
2405  }
2406  else {
2407    c0 = zeroMdd;
2408    c1 = mdd_dup( aState );
2409    array_insert_last( mdd_t *, onionRings, c1 );
2410  }
2411
2412  while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {
2413
2414    mdd_t *tmp2Mdd;
2415
2416    if ( McStateTestMembership( bState, c1 ) ) {
2417      break;
2418    }
2419
2420    /*
2421     *  performance gain from using dc's in this fp computation.
2422     *  use only when dclevel >= max
2423     */
2424    if ( dcLevel >= McDcLevelRchFrontier_c ) {
2425      mdd_t *annulusMdd = mdd_and(  c0, c1, 0, 1 );
2426      mdd_t *discMdd = mdd_dup( c1 );
2427      mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );
2428
2429      tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
2430                        annulusMdd, discMdd, careSetArray);
2431
2432      if ( verbosity > McVerbosityNone_c ) {
2433        fprintf(vis_stdout,
2434                "--Fwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
2435                mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
2436      }
2437
2438      mdd_free( annulusMdd );
2439      mdd_free( discMdd );
2440      mdd_free( dcMdd );
2441    }
2442    else {
2443      tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, c1, c1,
2444                                                        careSetArray);
2445    }
2446
2447    tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
2448    mdd_free(tmp2Mdd);
2449
2450    c0 = c1;
2451    c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
2452    mdd_free( tmp1Mdd );
2453
2454    array_insert_last( mdd_t *, onionRings, c1 );
2455  }
2456
2457  if ( McStateTestMembership( bState, c1 ) )  {
2458    result = Mc_BuildPathFromCore(bState, onionRings, modelFsm,
2459                                  McGreaterZero_c );
2460  }
2461  else {
2462    result = NIL(array_t);
2463  }
2464
2465  mdd_free( zeroMdd );
2466  mdd_array_free( onionRings);
2467
2468  return result;
2469}
2470
2471/**Function********************************************************************
2472
2473  Synopsis [Make a path from aState to bState using bwd reachability.]
2474
2475  Description [Make a path from aState to bState which only passes through
2476  invariantStates; it is assumed that aState and bState lie in invariantStates.
2477  Returns a sequence of states starting from aState, leading to bState. If
2478  aState == bState, a non trivial path is returned (ie a cycle). If no
2479  path exists, return NIL. It is the users responsibility to free the returned
2480  array as well as its members. This function starts from bState and does
2481  backward reachability till it hits aState or a fixed point.]
2482
2483  SideEffects []
2484
2485******************************************************************************/
2486array_t *
2487McCompletePathBwd(
2488  mdd_t *aState,
2489  mdd_t *bState,
2490  mdd_t *invariantStates,
2491  Fsm_Fsm_t *modelFsm,
2492  array_t *careSetArray,
2493  Mc_VerbosityLevel verbosity,
2494  Mc_DcLevel dcLevel)
2495{
2496  mdd_t *tmp1Mdd;
2497  array_t *result;
2498  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
2499  mdd_t *zeroMdd = mdd_zero( mddMgr );
2500  array_t *onionRings = array_alloc( mdd_t *, 0 );
2501  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
2502  mdd_t *c0, *c1;
2503
2504
2505  assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
2506  assert( mdd_lequal( bState, invariantStates, 1, 1 ) );
2507
2508  if ( mdd_equal( aState, bState ) ) {
2509
2510    /*
2511     * Alter the starting point to force routine to produce cycle if exists
2512     * Question: would it be quicker to do simultaneous backward/forward
2513     * analysis?
2514     */
2515
2516    c0 = mdd_dup( bState );
2517    array_insert_last( mdd_t *, onionRings, c0 );
2518
2519    tmp1Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, bState,
2520                                                         bState, careSetArray);
2521    c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
2522    mdd_free(tmp1Mdd);
2523    array_insert_last( mdd_t *, onionRings, c1 );
2524  }
2525  else {
2526    c0 = zeroMdd;
2527    c1 = mdd_dup( bState );
2528    array_insert_last( mdd_t *, onionRings, c1 );
2529  }
2530
2531  while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {
2532
2533    mdd_t *tmp2Mdd;
2534
2535    if ( McStateTestMembership( aState, c1 ) ) {
2536      break;
2537    }
2538
2539    /*
2540     *  performance gain from using dc's in this fp computation.
2541     *  use only when dclevel >= max
2542     */
2543    if ( dcLevel >= McDcLevelRchFrontier_c ) {
2544      mdd_t *annulusMdd = mdd_and(  c0, c1, 0, 1 );
2545      mdd_t *discMdd = mdd_dup( c1 );
2546      mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );
2547
2548      tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
2549                        annulusMdd, discMdd, careSetArray);
2550
2551      if ( verbosity > McVerbosityNone_c ) {
2552        fprintf(vis_stdout,
2553                "--Bwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
2554                mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
2555      }
2556
2557      mdd_free( annulusMdd );
2558      mdd_free( discMdd );
2559      mdd_free( dcMdd );
2560    }
2561    else {
2562      tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, c1, c1,
2563                                                           careSetArray);
2564    }
2565
2566    tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
2567    mdd_free(tmp2Mdd);
2568
2569    c0 = c1;
2570    c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
2571    mdd_free( tmp1Mdd );
2572
2573    array_insert_last( mdd_t *, onionRings, c1 );
2574  }
2575
2576  if ( McStateTestMembership( aState, c1 ) )  {
2577    result = Mc_BuildPathToCore(aState, onionRings, modelFsm, McGreaterZero_c);
2578  }
2579  else {
2580    result = NIL(array_t);
2581  }
2582
2583  mdd_free( zeroMdd );
2584  mdd_array_free( onionRings);
2585
2586  return result;
2587}
2588
2589/**Function********************************************************************
2590
2591  Synopsis [Write resettability condition as a CTL formula]
2592
2593  CommandName      [_init_state_formula]
2594
2595  CommandSynopsis [write resettability condition as a CTL formula]
2596
2597  CommandArguments [ \[-h\] \[&lt;init_file&gt;\] ]
2598
2599  CommandDescription [Write resettability condition as a CTL formula. Writes to
2600  <code>init_file</code> is specified, else stdout.]
2601
2602  SideEffects []
2603
2604******************************************************************************/
2605int
2606McCommandInitState(
2607  Hrc_Manager_t **hmgr,
2608  int argc,
2609  char **argv)
2610{
2611  mdd_t *modelInitialStates;
2612  mdd_t *anInitialState;
2613  Fsm_Fsm_t *modelFsm;
2614  char *formulaTxt;
2615  array_t *stateVars;
2616  FILE *ctlFile;
2617
2618  if ( argc == 1 ) {
2619    ctlFile = vis_stdout;
2620  }
2621  else {
2622    if ( !strcmp( "-h", argv[1] ) || ( argc > 2 ) ) {
2623      fprintf( vis_stdout, "Usage: _init_state_formula [-h] init_file\n\tinit_file - file to write init state formula to (default is stdout)\n");
2624      return 1;
2625    }
2626    ctlFile = Cmd_FileOpen( argv[1], "w", NIL(char *), 0 );
2627  }
2628
2629  modelFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
2630  if (modelFsm == NIL(Fsm_Fsm_t)) {
2631    if ( argc != 1 ) {
2632      fclose( ctlFile );
2633    }
2634    return 1;
2635  }
2636  stateVars = Fsm_FsmReadPresentStateVars( modelFsm );
2637
2638  modelInitialStates = Fsm_FsmComputeInitialStates( modelFsm );
2639  if ( modelInitialStates == NIL(mdd_t) ) {
2640    (void) fprintf( vis_stdout, "** mc error: - cant build init states (mutual latch dependancy?)\n%s\n",
2641                    error_string() );
2642    if ( argc != 1 ) {
2643      fclose( ctlFile );
2644    }
2645    return 1;
2646  }
2647  anInitialState = Mc_ComputeAState( modelInitialStates, modelFsm );
2648  mdd_free(modelInitialStates);
2649
2650  formulaTxt = McStatePrintAsFormula( anInitialState, stateVars, modelFsm );
2651  mdd_free(anInitialState);
2652
2653  fprintf( ctlFile, "AG EF %s;\n", formulaTxt );
2654  FREE(formulaTxt);
2655
2656  if ( argc != 1 ) {
2657    fclose(ctlFile);
2658  }
2659
2660  return 0;
2661}
2662
2663
2664
2665/**Function********************************************************************
2666
2667  Synopsis [Return a CTL formula for a minterm.]
2668
2669  SideEffects []
2670
2671******************************************************************************/
2672char *
2673McStatePrintAsFormula(
2674  mdd_t *aMinterm,
2675  array_t *aSupport,
2676  Fsm_Fsm_t *modelFsm)
2677{
2678  int i;
2679  char *tmp1String;
2680  char *tmp2String;
2681  char *tmp3String;
2682  char bodyString[McMaxStringLength_c];
2683  char *mintermString = NIL(char);
2684  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
2685  Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
2686  array_t *valueArray = McConvertMintermToValueArray( aMinterm, aSupport, mddMgr );
2687  array_t *stringArray = array_alloc( char *, 0 );
2688
2689  for ( i = 0 ; i < array_n( aSupport ); i++ ) {
2690
2691    int mddId = array_fetch( int, aSupport, i );
2692    int value = array_fetch( int, valueArray, i );
2693    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
2694    char *nodeName = Ntk_NodeReadName( node );
2695    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
2696
2697    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
2698      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
2699      sprintf( bodyString, "%s=%s", nodeName, symbolicValue );
2700    }
2701    else {
2702      sprintf( bodyString, "%s=%d", nodeName, value );
2703    }
2704    tmp1String = util_strsav( bodyString );
2705    array_insert_last( char *, stringArray, tmp1String );
2706  }
2707  array_free(valueArray);
2708
2709  array_sort( stringArray, cmp);
2710
2711  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
2712    tmp1String = array_fetch( char *, stringArray, i );
2713    if( i == 0 )  {
2714      mintermString = util_strcat3("(", tmp1String, ")" );
2715    }
2716    else {
2717      tmp2String = util_strcat3( mintermString, " * (", tmp1String );
2718      FREE(mintermString);
2719      tmp3String = util_strcat3( tmp2String, ")", "" );
2720      FREE(tmp2String);
2721      mintermString = tmp3String;
2722    }
2723    FREE(tmp1String);
2724  }
2725  array_free( stringArray );
2726
2727  tmp1String = util_strcat3( "( ", mintermString, " )" );
2728  FREE(mintermString);
2729  mintermString = tmp1String;
2730
2731  return mintermString;
2732}
2733
2734/**Function********************************************************************
2735
2736  Synopsis [Search the given array of "Onion Rings" for the Onion Rings
2737  with the clore closest to specified state.]
2738
2739  Description [Search the given array of "Onion Rings" for the Onion Rings with
2740  the core closest to specified state. By "Onion Rings" we refer to an array of
2741  sets of states (so arrayOfOnionRings is an array of arrays of states).  The
2742  first member of a set of onion rings is referred to as the "core". The "Onion
2743  Rings" array has the property that the first set is all states that can reach
2744  the core (this may be mod a care set like the reached states).  The succesive
2745  sets are those which can reach the core in successively fewer iterations.
2746
2747  We find the i with the smallest index j for which arrayOfOnionRings[i][j]
2748  contains aState.]
2749
2750  SideEffects []
2751
2752******************************************************************************/
2753int
2754McComputeOnionRingsWithClosestCore(
2755  mdd_t *aState,
2756  array_t *arrayOfOnionRings,
2757  Fsm_Fsm_t *modelFsm)
2758{
2759  int index;
2760  int distance = 0;
2761
2762  while( TRUE ) {
2763    for( index = 0 ; index < array_n( arrayOfOnionRings ) ; index++ ) {
2764      array_t *iOnionRings = array_fetch( array_t *, arrayOfOnionRings, index );
2765
2766      /* will crash if run out of rings -> if not in there */
2767      mdd_t *stateSet = array_fetch( mdd_t *, iOnionRings, distance );
2768
2769      if ( McStateTestMembership( aState, stateSet ) )
2770        return index;
2771    }
2772    distance++;
2773  }
2774  assert(0);
2775}
2776
2777
2778
2779/**Function********************************************************************
2780
2781  Synopsis [Remove array indexed by index from array of arrays.]
2782
2783  Description [Remove array indexed by index from array of arrays. Does NOT
2784  free the input arrayOfOnionRings.]
2785
2786  SideEffects []
2787
2788******************************************************************************/
2789array_t *
2790McRemoveIndexedOnionRings(
2791  int index,
2792  array_t *arrayOfOnionRings)
2793{
2794  int i;
2795  array_t *dupArrayOfOnionRings = array_alloc( array_t *, 0 );
2796  array_t *OnionRings;
2797
2798  for ( i = 0 ; i < array_n( arrayOfOnionRings ) ; i++ ) {
2799    if ( i == index ) {
2800      continue;
2801    }
2802    OnionRings = array_fetch( array_t *, arrayOfOnionRings, i );
2803    array_insert_last( array_t *, dupArrayOfOnionRings, OnionRings );
2804  }
2805
2806  return dupArrayOfOnionRings;
2807}
2808
2809
2810
2811
2812
2813
2814
2815/**Function********************************************************************
2816
2817  Synopsis [Convert a minterm to an array of integers]
2818
2819  SideEffects []
2820
2821******************************************************************************/
2822array_t *
2823McConvertMintermToValueArray(
2824  mdd_t *aMinterm,
2825  array_t *aSupport,
2826  mdd_manager *mddMgr)
2827{
2828  array_t *resultValueArray;
2829
2830  /* this will be performed only in v0s-g executables */
2831  assert( MintermCheckWellFormed( aMinterm, aSupport, mddMgr ));
2832
2833  resultValueArray = array_alloc( int, 0 );
2834  {
2835    int i;
2836    for( i = 0 ; i < array_n( aSupport ); i++ ) {
2837      int aSupportVar = array_fetch( int, aSupport, i );
2838      int j;
2839      for( j = 0 ; TRUE ; j++) {
2840
2841        mdd_t *faceMdd, *tmpMdd;
2842        array_t *tmpArray = array_alloc( int, 0 );
2843
2844        array_insert_last( int, tmpArray, j );
2845        faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
2846        array_free( tmpArray );
2847
2848        tmpMdd = mdd_and( faceMdd, aMinterm, 1, 1 );
2849        mdd_free( faceMdd );
2850        if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
2851          mdd_free( tmpMdd );
2852          array_insert_last( int, resultValueArray, j );
2853          break;
2854        }
2855        mdd_free( tmpMdd );
2856      }
2857    }
2858  }
2859
2860  return resultValueArray;
2861}
2862
2863
2864
2865
2866
2867/**Function********************************************************************
2868
2869  Synopsis [Print a transition to vis_stdout.]
2870
2871  Description [Print a transition to vis_stdout. The transition is supposed to be
2872  from aState to bState on input vInput. If uInput is not NIL, instead of
2873  printing vInput, we only print the places where it differs from uInput. If there
2874  is no difference anywhere, we print "-Unchanged-". Similarly, we print only the
2875  incremental difference from aState to bState; if there is none, we print "-Unchanged-".
2876  If aState is NIL we simply print bState and return.]
2877
2878  SideEffects []
2879
2880******************************************************************************/
2881void
2882McPrintTransitionAiger(
2883  mdd_t *aState,
2884  mdd_t *bState,
2885  mdd_t *uInput,
2886  mdd_t *vInput,
2887  array_t *stateSupport,
2888  array_t *inputSupport,
2889  boolean printInputs,
2890  Fsm_Fsm_t *modelFsm,
2891  int seqNumber)
2892{
2893  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
2894  char *aString = aState ? Mc_MintermToStringAiger( aState, stateSupport, modelNetwork ) : NIL(char);
2895  char *bString = Mc_MintermToStringAiger( bState, stateSupport, modelNetwork );
2896  char *inpString = aState ? Mc_MintermToStringAigerInput( aState, stateSupport, modelNetwork ) : NIL(char);
2897
2898  st_table   *node2MvfAigTable;
2899
2900  node2MvfAigTable =
2901        (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);
2902
2903  if ( aState == NIL(mdd_t) ) {
2904    FREE(bString);
2905    return;
2906  }
2907
2908  fprintf(vis_stdout, "%s", aString);
2909  fprintf(vis_stdout, "%s", inpString);
2910
2911
2912   /* first test that there are inputs */
2913  /* if ( array_n( inputSupport ) > 0 ) {
2914    if ( uInput == NIL(mdd_t) ) {
2915      char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
2916      FREE(vString);
2917    }
2918    else {
2919      boolean unchanged=TRUE;
2920      char *uString = Mc_MintermToStringAiger( uInput, inputSupport, modelNetwork );
2921      char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
2922      FREE(uString);
2923      FREE(vString);
2924    }
2925  } */
2926
2927  if(seqNumber == 1)
2928  {
2929    fprintf(vis_stdout, "1 ");
2930  }
2931  else
2932  {
2933    fprintf(vis_stdout, "0 ");
2934  }
2935
2936
2937  fprintf(vis_stdout, "%s", bString);
2938
2939  FREE( aString );
2940  FREE( bString );
2941  fprintf (vis_stdout, "\n");
2942  return;
2943}
2944
2945
2946
2947
2948/**Function********************************************************************
2949
2950  Synopsis [Print a transition to vis_stdout.]
2951
2952  Description [Print a transition to vis_stdout. The transition is supposed to be
2953  from aState to bState on input vInput. If uInput is not NIL, instead of
2954  printing vInput, we only print the places where it differs from uInput. If there
2955  is no difference anywhere, we print "-Unchanged-". Similarly, we print only the
2956  incremental difference from aState to bState; if there is none, we print "-Unchanged-".
2957  If aState is NIL we simply print bState and return.]
2958
2959  SideEffects []
2960
2961******************************************************************************/
2962void
2963McPrintTransition(
2964  mdd_t *aState,
2965  mdd_t *bState,
2966  mdd_t *uInput,
2967  mdd_t *vInput,
2968  array_t *stateSupport,
2969  array_t *inputSupport,
2970  boolean printInputs,
2971  Fsm_Fsm_t *modelFsm,
2972  int seqNumber)
2973{
2974  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
2975  char *aString = aState ? Mc_MintermToString( aState, stateSupport, modelNetwork ) : NIL(char);
2976  char *bString = Mc_MintermToString( bState, stateSupport, modelNetwork );
2977
2978  char *tmp1String = aString;
2979  char *tmp2String = bString;
2980  char *ptr1;
2981  char *ptr2;
2982  st_table   *node2MvfAigTable;
2983
2984  node2MvfAigTable =
2985        (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);
2986
2987  if ( aState == NIL(mdd_t) ) {
2988    fprintf( vis_stdout, "--State %d:\n%s\n", seqNumber, bString );
2989    FREE(bString);
2990    return;
2991  }
2992
2993  fprintf(vis_stdout, "--Goes to state %d:\n", seqNumber );
2994
2995  {
2996    boolean unchanged=TRUE;
2997    while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
2998      ptr2 = strchr( tmp2String, '\n' );
2999      *ptr1 = 0;
3000      *ptr2 = 0;
3001      if ( (strcmp( tmp1String, tmp2String ) ) ) {
3002        fprintf( vis_stdout, "%s\n", tmp2String );
3003        unchanged = FALSE;
3004      }
3005      tmp1String = & (ptr1[1]);
3006      tmp2String = & (ptr2[1]);
3007    }
3008    if (unchanged == TRUE) {
3009      fprintf( vis_stdout, "<Unchanged>\n");
3010    }
3011  }
3012
3013
3014  if ( printInputs == TRUE ) {
3015    /* first test that there are inputs */
3016    if ( array_n( inputSupport ) > 0 ) {
3017      fprintf(vis_stdout, "--On input:\n");
3018      if ( uInput == NIL(mdd_t) ) {
3019        char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
3020        fprintf(vis_stdout, "%s", vString );
3021        FREE(vString);
3022      }
3023      else {
3024        boolean unchanged=TRUE;
3025        char *uString = Mc_MintermToString( uInput, inputSupport, modelNetwork );
3026        char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
3027        tmp1String = uString;
3028        tmp2String = vString;
3029        while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
3030          ptr2 = strchr( tmp2String, '\n' );
3031          *ptr1 = 0;
3032          *ptr2 = 0;
3033          if ( (strcmp( tmp1String, tmp2String ) ) ) {
3034            fprintf( vis_stdout, "%s\n", tmp2String );
3035            unchanged = FALSE;
3036          }
3037          tmp1String = & (ptr1[1]);
3038          tmp2String = & (ptr2[1]);
3039        }
3040        if (unchanged == TRUE) {
3041          fprintf( vis_stdout, "<Unchanged>\n");
3042        }
3043        FREE(uString);
3044        FREE(vString);
3045      }
3046    }
3047  }
3048
3049  FREE( aString );
3050  FREE( bString );
3051  fprintf (vis_stdout, "\n");
3052}
3053
3054
3055/**Function********************************************************************
3056
3057  Synopsis [Print message saying given state passes formula.]
3058
3059  SideEffects []
3060
3061******************************************************************************/
3062void
3063McStatePassesFormula(
3064  mdd_t *aState,
3065  Ctlp_Formula_t *formula,
3066  McDbgLevel debugLevel,
3067 Fsm_Fsm_t *modelFsm)
3068{
3069  McStatePassesOrFailsFormula( aState, formula, 1, debugLevel,  modelFsm );
3070}
3071
3072
3073/**Function********************************************************************
3074
3075  Synopsis [Print message saying given state fails formula.]
3076
3077  SideEffects []
3078
3079******************************************************************************/
3080void
3081McStateFailsFormula(
3082  mdd_t *aState,
3083  Ctlp_Formula_t *formula,
3084  McDbgLevel debugLevel,
3085  Fsm_Fsm_t *modelFsm)
3086{
3087  McStatePassesOrFailsFormula( aState, formula, 0,  debugLevel, modelFsm );
3088}
3089
3090
3091/**Function********************************************************************
3092
3093  Synopsis [Utility function - prints state passes or fails formula]
3094
3095  SideEffects []
3096
3097******************************************************************************/
3098void
3099McStatePassesOrFailsFormula(
3100  mdd_t *aState,
3101  Ctlp_Formula_t *formula,
3102  int pass,
3103  McDbgLevel debugLevel,
3104  Fsm_Fsm_t *modelFsm)
3105{
3106  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
3107  char *formulaText = Ctlp_FormulaConvertToString( formula );
3108  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
3109
3110  /* Nodes created in converting formulae like AU may not have text
3111   * attached to them. */
3112  if (formulaText == NIL(char))
3113    return;
3114
3115  fprintf( vis_stdout, "--State\n");
3116  Mc_MintermPrint( aState, PSVars, modelNetwork );
3117  if ( pass )
3118    fprintf( vis_stdout, "passes ");
3119  else
3120    fprintf( vis_stdout, "fails ");
3121
3122  if( debugLevel > McDbgLevelMin_c)
3123    fprintf(vis_stdout, "%s.\n\n", formulaText);
3124  else
3125    fprintf(vis_stdout, "\n\n");
3126
3127  FREE(formulaText);
3128}
3129
3130
3131
3132/**Function********************************************************************
3133
3134  Synopsis [Utility function - convert McPath_t to normal form.]
3135
3136  Description [Utility function - convert McPath_t to normal form.
3137  A normal McPath_t is one where the stem leads to a state, which then returns
3138  it self in the cycle.]
3139
3140  SideEffects []
3141
3142******************************************************************************/
3143
3144McPath_t *
3145McPathNormalize(
3146  McPath_t *aPath)
3147{
3148  int i, j;
3149  int forced;
3150
3151  array_t *stemArray = McPathReadStemArray( aPath );
3152  array_t *cycleArray = McPathReadCycleArray( aPath );
3153
3154  McPath_t *result = McPathAlloc();
3155  array_t *newStem = array_alloc( mdd_t *, 0 );
3156  array_t *newCycle = array_alloc( mdd_t *, 0 );
3157
3158  mdd_t *lastState = GET_NORMAL_PT(array_fetch_last(mdd_t *, cycleArray));
3159
3160  McPathSetStemArray( result, newStem );
3161  McPathSetCycleArray( result, newCycle );
3162
3163  for( i = 0 ; i < array_n( stemArray ) ; i++ ) {
3164    mdd_t *tmpState = array_fetch( mdd_t *, stemArray, i );
3165    forced = 0;
3166    if((long)tmpState % 2) {
3167       forced = 1;
3168       tmpState = (mdd_t *)((long)tmpState - 1);
3169    }
3170    array_insert_last(mdd_t *, newStem,
3171            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
3172
3173    if ( mdd_equal( lastState, tmpState ) ) {
3174      break;
3175    }
3176  }
3177
3178  for( j = i; j < array_n( stemArray ); j++ ) {
3179    mdd_t *tmpState = array_fetch( mdd_t *, stemArray, j );
3180    forced = 0;
3181    if((long)tmpState % 2) {
3182       forced = 1;
3183       tmpState = (mdd_t *)((long)tmpState - 1);
3184    }
3185
3186    array_insert_last(mdd_t *, newCycle,
3187            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
3188
3189  }
3190
3191  /* first state of cycle array == last state of stem array => start from j=1 */
3192  for( j = 1; j < array_n( cycleArray ); j++ ) {
3193    mdd_t *tmpState = array_fetch( mdd_t *, cycleArray, j );
3194    forced = 0;
3195    if((long)tmpState % 2) {
3196       forced = 1;
3197       tmpState = (mdd_t *)((long)tmpState - 1);
3198    }
3199    array_insert_last(mdd_t *, newCycle,
3200            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
3201
3202  }
3203
3204  return result;
3205
3206}
3207
3208
3209
3210/**Function********************************************************************
3211
3212  Synopsis [Utility function - merges two paths.]
3213
3214  Description [Utility function - merges two paths. Note that the merge is done
3215  by adding the elements of the second array starting from the second element onwards.
3216  This is because we often have to merge paths where the end point of the first is the
3217  starting point of the second.]
3218
3219  SideEffects []
3220
3221******************************************************************************/
3222array_t *
3223McCreateMergedPath(
3224  array_t *aPath,
3225  array_t *bPath)
3226{
3227  int i, pos, forced;
3228  mdd_t *tmpState, *endOfAPath;
3229  array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
3230  array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );
3231
3232  for( i = 1 ; i < array_n( bPathDup ) ; i++ ) {
3233    tmpState = array_fetch( mdd_t *, bPathDup, i );
3234    array_insert_last( mdd_t *, aPathDup, tmpState );
3235  }
3236  pos = array_n(aPathDup) - array_n(bPathDup);
3237  endOfAPath = array_fetch(mdd_t *, aPathDup, pos);
3238
3239  tmpState = array_fetch( mdd_t *, bPathDup, 0 );
3240  forced = 0;
3241  if((long)tmpState % 2) {
3242    forced = 1;
3243    tmpState = (mdd_t *)((long)tmpState - 1);
3244  }
3245  if(forced && mdd_equal(tmpState, endOfAPath)) {
3246    array_insert(mdd_t *, aPathDup, pos, (mdd_t *)((long)endOfAPath + forced) );
3247  }
3248
3249  mdd_free( tmpState );
3250  array_free( bPathDup );
3251
3252  return aPathDup;
3253}
3254
3255/**Function********************************************************************
3256
3257  Synopsis [Utility function - duplicate bdd array.]
3258
3259  Description [To represent the forced segment, the mdd_t is complemented.
3260               Therefore one cannot use mdd_array_duplicate.
3261               This is function for FateAndFreeWill counterexample generation.]
3262
3263  SideEffects []
3264
3265******************************************************************************/
3266array_t *
3267McMddArrayDuplicateFAFW(array_t *mddArray)
3268{
3269  int   i, forced;
3270  mdd_t *newTempMdd;
3271  int      length = array_n(mddArray);
3272  array_t *result = array_alloc(mdd_t *, length);
3273
3274  for (i = 0; i < length; i++) {
3275    mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i);
3276    forced = 0;
3277    if((long)tempMdd % 2) {
3278      forced = 1;
3279      tempMdd = (mdd_t *)((long)tempMdd - 1);
3280    }
3281
3282    newTempMdd = mdd_dup(tempMdd);
3283    array_insert(mdd_t *, result, i, (mdd_t *)((long)newTempMdd + forced));
3284  }
3285
3286  return (result);
3287}
3288
3289/**Function********************************************************************
3290
3291  Synopsis [Utility function - compute the intersection of the elements.]
3292
3293  Description [Utility function - compute the intersection of the elements.]
3294
3295  SideEffects []
3296
3297******************************************************************************/
3298mdd_t *
3299McMddArrayAnd(array_t *mddArray)
3300{
3301  mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
3302  int i;
3303
3304  result = NIL(mdd_t);
3305  arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
3306    if (result == NIL(mdd_t))
3307      result = mdd_dup(mdd1);
3308    else {
3309      mdd2 = result;
3310      result = mdd_and(result, mdd1, 1, 1);
3311      mdd_free(mdd2);
3312    }
3313  }
3314
3315  return (result);
3316}
3317
3318/**Function********************************************************************
3319
3320  Synopsis [Utility function - compute the union of the elements.]
3321
3322  Description [Utility function - compute the union of the elements.]
3323
3324  SideEffects []
3325
3326******************************************************************************/
3327mdd_t *
3328McMddArrayOr(array_t *mddArray)
3329{
3330  mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
3331  int i;
3332
3333  result = NIL(mdd_t);
3334  arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
3335    if (result == NIL(mdd_t))
3336      result = mdd_dup(mdd1);
3337    else {
3338      mdd2 = result;
3339      result = mdd_or(result, mdd1, 1, 1);
3340      mdd_free(mdd2);
3341    }
3342  }
3343
3344  return (result);
3345}
3346
3347/**Function********************************************************************
3348
3349  Synopsis [Utility function - joins two paths.]
3350
3351  Description [Utility function - joins two paths. Note that the joins is done
3352  by adding the elements of the second array starting from the first element onwards.]
3353
3354  SeeAlso [McCreateMergedPath]
3355
3356  SideEffects []
3357
3358******************************************************************************/
3359array_t *
3360McCreateJoinedPath(
3361  array_t *aPath,
3362  array_t *bPath)
3363{
3364  int i;
3365  mdd_t *tmpState;
3366  array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
3367  array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );
3368
3369  for( i = 0 ; i < array_n( bPathDup ) ; i++ ) {
3370    tmpState = array_fetch( mdd_t *, bPathDup, i );
3371    array_insert_last( mdd_t *, aPathDup, tmpState );
3372  }
3373  array_free( bPathDup );
3374
3375  return aPathDup;
3376}
3377
3378
3379/**Function********************************************************************
3380
3381  Synopsis [ Check to see if aState lies in set of states satisfying aFormula ]
3382
3383  SideEffects []
3384
3385******************************************************************************/
3386boolean
3387McStateSatisfiesFormula(
3388  Ctlp_Formula_t *aFormula,
3389  mdd_t *aState )
3390{
3391  mdd_t *passStates = Ctlp_FormulaObtainLatestApprox( aFormula );
3392
3393  if ( mdd_lequal( aState, passStates, 1, 1 ) ) {
3394    mdd_free( passStates );
3395    return TRUE;
3396  }
3397  else {
3398    mdd_free( passStates );
3399    return FALSE;
3400  }
3401}
3402
3403
3404
3405/**Function********************************************************************
3406
3407  Synopsis [ Tests aState is a member of setOfStates ]
3408
3409  SideEffects []
3410
3411******************************************************************************/
3412boolean
3413McStateTestMembership(
3414  mdd_t *aState,
3415  mdd_t *setOfStates )
3416{
3417  return mdd_lequal( aState, setOfStates, 1, 1 );
3418}
3419
3420/**Function********************************************************************
3421
3422  Synopsis [Obtain a successor of aState which is in targetStates]
3423
3424  SideEffects []
3425
3426******************************************************************************/
3427mdd_t *
3428McGetSuccessorInTarget(
3429  mdd_t *aState,
3430  mdd_t *targetStates,
3431  Fsm_Fsm_t *modelFsm )
3432{
3433  mdd_t *tmpMdd, *succsInTarget, *result;
3434  array_t *careSetArray = array_alloc(mdd_t *, 0);
3435  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
3436
3437  array_insert_last(mdd_t *, careSetArray, targetStates);
3438  tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
3439                                                   aState, careSetArray);
3440  array_free(careSetArray);
3441  succsInTarget = mdd_and(tmpMdd, targetStates, 1, 1);
3442#if 1
3443  result = Mc_ComputeAState(succsInTarget, modelFsm);
3444#else
3445  result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);
3446#endif
3447
3448  mdd_free( tmpMdd );
3449  mdd_free( succsInTarget );
3450
3451  return result;
3452}
3453
3454/**Function********************************************************************
3455
3456  Synopsis [Obtain a successor of aState which is in targetStates]
3457
3458  SideEffects []
3459
3460******************************************************************************/
3461mdd_t *
3462McGetSuccessorInTargetAmongFairStates(
3463  mdd_t *aState,
3464  mdd_t *targetStates,
3465  array_t *arrayOfOnionRings,
3466  Fsm_Fsm_t *modelFsm )
3467{
3468  mdd_t *tmpMdd, *succsInTarget, *result;
3469  mdd_t *fairStates, *newFairStates, *onionRing;
3470  mdd_t *targetStatesInFairStates;
3471  array_t *onionRings;
3472  int i, j;
3473  array_t *careSetArray = array_alloc(mdd_t *, 0);
3474
3475  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
3476
3477
3478  fairStates = 0;
3479  for(i=0; i<array_n(arrayOfOnionRings); i++) {
3480    onionRings = array_fetch(array_t *, arrayOfOnionRings, i);
3481    for(j=0; j<array_n(onionRings); j++) {
3482      onionRing = array_fetch(mdd_t *,onionRings, j);
3483
3484      if(fairStates) {
3485        newFairStates = mdd_or(fairStates, onionRing, 1, 1);
3486        mdd_free(fairStates);
3487        fairStates = newFairStates;
3488      }
3489      else {
3490        fairStates = mdd_dup(onionRing);
3491      }
3492    }
3493  }
3494  targetStatesInFairStates = mdd_and(fairStates, targetStates, 1, 1);
3495  mdd_free(fairStates);
3496
3497  array_insert_last(mdd_t *, careSetArray, targetStatesInFairStates);
3498  tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
3499                                                   aState, careSetArray);
3500  succsInTarget = mdd_and(tmpMdd, targetStatesInFairStates, 1, 1);
3501  mdd_array_free(careSetArray);
3502  result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);
3503
3504  mdd_free( tmpMdd );
3505  mdd_free( succsInTarget );
3506
3507  return result;
3508}
3509
3510
3511/**Function********************************************************************
3512
3513  Synopsis [Obtain stem of fair path]
3514
3515  SideEffects []
3516
3517******************************************************************************/
3518array_t *
3519McPathReadStemArray(
3520  McPath_t *aPath )
3521{
3522  return aPath->stemArray;
3523}
3524
3525/**Function********************************************************************
3526
3527  Synopsis [Obtain cycle of fair path]
3528
3529  SideEffects []
3530
3531******************************************************************************/
3532array_t *
3533McPathReadCycleArray(
3534  McPath_t *aPath )
3535{
3536  return aPath->cycleArray;
3537}
3538
3539/**Function********************************************************************
3540
3541  Synopsis [Set stem of fair path]
3542
3543  SideEffects []
3544
3545******************************************************************************/
3546void
3547McPathSetStemArray(
3548  McPath_t *aPath,
3549  array_t *stemArray)
3550{
3551  aPath->stemArray = stemArray;
3552}
3553
3554/**Function********************************************************************
3555
3556  Synopsis [Set cycle of fair path]
3557
3558  SideEffects []
3559
3560******************************************************************************/
3561void
3562McPathSetCycleArray(
3563  McPath_t *aPath,
3564  array_t *cycleArray )
3565{
3566  aPath->cycleArray = cycleArray;
3567}
3568
3569/**Function********************************************************************
3570
3571  Synopsis [Allocate a  Path Struct]
3572
3573  SideEffects []
3574
3575******************************************************************************/
3576McPath_t *
3577McPathAlloc(void)
3578{
3579  McPath_t *tmpPath = ( McPath_t * ) malloc( sizeof( McPath_t ) );
3580
3581  tmpPath->stemArray = NIL(array_t);
3582  tmpPath->cycleArray = NIL(array_t);
3583
3584  return tmpPath;
3585}
3586
3587/**Function********************************************************************
3588
3589  Synopsis [Free a  Path Struct]
3590
3591  SideEffects []
3592
3593******************************************************************************/
3594void
3595McNormalizeBddPointer(array_t *bddArray)
3596{
3597  int i;
3598  bdd_t *p;
3599
3600  for(i=0; i<array_n(bddArray); i++) {
3601    p = array_fetch(bdd_t *, bddArray, i);
3602    if((long)p%2) p = (mdd_t *)( (long)p -1 );
3603    array_insert(bdd_t *, bddArray, i, p);
3604  }
3605}
3606
3607void
3608McPathFree(
3609  McPath_t * aPath )
3610{
3611  if ( aPath->stemArray ) {
3612    McNormalizeBddPointer(aPath->stemArray);
3613    mdd_array_free( aPath->stemArray );
3614  }
3615
3616  if ( aPath->cycleArray ) {
3617    McNormalizeBddPointer(aPath->cycleArray);
3618    mdd_array_free( aPath->cycleArray );
3619  }
3620
3621  FREE( aPath );
3622}
3623
3624/**Function********************************************************************
3625
3626  Synopsis [Allocate an McOptions_t struct.]
3627
3628  SideEffects []
3629
3630******************************************************************************/
3631McOptions_t *
3632McOptionsAlloc(void)
3633{
3634  McOptions_t *result = ALLOC(McOptions_t, 1);
3635
3636  memset(result, 0, sizeof(McOptions_t));
3637
3638  result->useMore = FALSE;
3639  result->reduceFsm = FALSE;
3640  result->printInputs = FALSE;
3641  result->useFormulaTree = FALSE;
3642  result->simFormat = FALSE;
3643  result->ctlFile = NIL(FILE);
3644  result->guideFile = NIL(FILE);
3645  result->debugFile = NIL(FILE);
3646  result->fwdBwd = McFwd_c;
3647  result->dcLevel = McDcLevelNone_c;
3648  result->dbgLevel = McDbgLevelMin_c;
3649  result->schedule = McGSH_EL_c;
3650  result->lockstep = MC_LOCKSTEP_OFF;
3651  result->verbosityLevel = McVerbosityNone_c;
3652  result->timeOutPeriod = 0;
3653  result->ardcOptions = NIL(Fsm_ArdcOptions_t);
3654  result->invarApproxFlag = Fsm_Rch_Default_c;
3655  result->invarOnionRingsFlag = FALSE;
3656  result->traversalDirection = McBwd_c;
3657  result->doCoverageHoskote = FALSE;
3658  result->doCoverageImproved = FALSE;
3659  result->incre = TRUE;
3660
3661
3662  return result;
3663}
3664
3665/**Function********************************************************************
3666
3667  Synopsis [Free an McOptions_t struct.]
3668
3669  SideEffects []
3670
3671******************************************************************************/
3672void
3673McOptionsFree(
3674  McOptions_t *options)
3675{
3676  if (options->debugFile != NIL(FILE)){
3677    fclose(options->debugFile);
3678  }
3679  if (options->ardcOptions != NIL(Fsm_ArdcOptions_t)){
3680    FREE(options->ardcOptions);
3681  }
3682  FREE(options);
3683}
3684
3685
3686/**Function********************************************************************
3687
3688  Synopsis [Return Dbg level set at options.]
3689
3690  SideEffects []
3691
3692******************************************************************************/
3693McDbgLevel
3694McOptionsReadDbgLevel(
3695  McOptions_t *options )
3696{
3697  return options->dbgLevel;
3698}
3699
3700/**Function********************************************************************
3701
3702  Synopsis [Return filepointer for guide file (NULL if guided search
3703  is disabled)]
3704
3705  SideEffects []
3706
3707******************************************************************************/
3708FILE *
3709McOptionsReadGuideFile(
3710  McOptions_t *options )
3711{
3712  return options->guideFile;
3713}
3714
3715/**Function********************************************************************
3716
3717  Synopsis [Return filepointer for system variables file for FAFW ]
3718
3719  SideEffects []
3720
3721******************************************************************************/
3722FILE *
3723McOptionsReadSystemFile(
3724  McOptions_t *options )
3725{
3726  return options->systemFile;
3727}
3728
3729/**Function********************************************************************
3730
3731  Synopsis [Return time out period set at options.]
3732
3733  SideEffects []
3734
3735******************************************************************************/
3736int
3737McOptionsReadTimeOutPeriod(
3738  McOptions_t *options )
3739{
3740  return options->timeOutPeriod;
3741}
3742
3743/**Function********************************************************************
3744
3745  Synopsis [Return Verbosity level of options.]
3746
3747  SideEffects []
3748
3749******************************************************************************/
3750Mc_VerbosityLevel
3751McOptionsReadVerbosityLevel(
3752  McOptions_t *options )
3753{
3754  return options->verbosityLevel;
3755}
3756
3757/**Function********************************************************************
3758
3759  Synopsis [Return the language emptiness checking method of options.]
3760
3761  SideEffects []
3762
3763******************************************************************************/
3764Mc_LeMethod_t
3765McOptionsReadLeMethod(
3766  McOptions_t *options )
3767{
3768  return options->leMethod;
3769}
3770
3771/**Function********************************************************************
3772
3773  Synopsis [Return Dbg level of options.]
3774
3775  SideEffects []
3776
3777******************************************************************************/
3778Mc_DcLevel
3779McOptionsReadDcLevel(
3780  McOptions_t *options )
3781{
3782  return options->dcLevel;
3783}
3784
3785/**Function********************************************************************
3786
3787  Synopsis [Return ctl file set at options.]
3788
3789  SideEffects []
3790
3791******************************************************************************/
3792FILE *
3793McOptionsReadCtlFile(
3794  McOptions_t *options )
3795{
3796  return options->ctlFile;
3797}
3798
3799/**Function********************************************************************
3800
3801  Synopsis [Return debug file set at options.]
3802
3803  SideEffects []
3804
3805******************************************************************************/
3806FILE *
3807McOptionsReadDebugFile(
3808  McOptions_t *options )
3809{
3810  return options->debugFile;
3811}
3812
3813/**Function********************************************************************
3814
3815  Synopsis [Read sim flag at options.]
3816
3817  SideEffects []
3818
3819******************************************************************************/
3820int
3821McOptionsReadSimValue(
3822  McOptions_t *options)
3823{
3824  return options->simFormat;
3825}
3826
3827/**Function********************************************************************
3828
3829  Synopsis [Read use more as pipe at options.]
3830
3831  SideEffects []
3832
3833******************************************************************************/
3834int
3835McOptionsReadUseMore(
3836  McOptions_t *options)
3837{
3838  return options->useMore;
3839}
3840
3841/**Function********************************************************************
3842
3843  Synopsis [Returns the value of Vacuity Detection option.]
3844
3845  SideEffects []
3846
3847******************************************************************************/
3848boolean
3849McOptionsReadVacuityDetect(
3850  McOptions_t *options)
3851{
3852  return options->vd ;
3853}
3854
3855/**Function********************************************************************
3856
3857  Synopsis [Returns the value of the option for the Beer method.]
3858
3859  SideEffects []
3860
3861******************************************************************************/
3862int
3863McOptionsReadBeerMethod(
3864  McOptions_t *options)
3865{
3866  return options->beer ;
3867}
3868
3869
3870/**Function********************************************************************
3871
3872  Synopsis [Read use CTL formula specific reduction.]
3873
3874  SideEffects []
3875
3876******************************************************************************/
3877int
3878McOptionsReadReduceFsm(
3879  McOptions_t *options)
3880{
3881  return options->reduceFsm;
3882}
3883
3884/**Function********************************************************************
3885
3886  Synopsis [Read print inputs in debug trace.]
3887
3888  SideEffects []
3889
3890******************************************************************************/
3891int
3892McOptionsReadPrintInputs(
3893  McOptions_t *options)
3894{
3895  return options->printInputs;
3896}
3897
3898/**Function********************************************************************
3899
3900  Synopsis [Read use of CTL formula tree.]
3901
3902  SideEffects []
3903
3904******************************************************************************/
3905boolean
3906McOptionsReadUseFormulaTree(
3907  McOptions_t *options)
3908{
3909  return options->useFormulaTree;
3910}
3911
3912/**Function********************************************************************
3913
3914  Synopsis [Read schedule for GSH.]
3915
3916  SideEffects []
3917
3918******************************************************************************/
3919Mc_GSHScheduleType
3920McOptionsReadSchedule(
3921  McOptions_t *options)
3922{
3923  return options->schedule;
3924}
3925
3926/**Function********************************************************************
3927
3928  Synopsis [Read lockstep option.]
3929
3930  SideEffects []
3931
3932******************************************************************************/
3933int
3934McOptionsReadLockstep(
3935  McOptions_t *options)
3936{
3937  return options->lockstep;
3938}
3939
3940/**Function********************************************************************
3941
3942  Synopsis [Read reachability analysis type for check_invariant]
3943
3944  SideEffects []
3945
3946******************************************************************************/
3947Fsm_RchType_t
3948McOptionsReadInvarApproxFlag(
3949  McOptions_t *options)
3950{
3951  return (options->invarApproxFlag);
3952}
3953
3954/**Function********************************************************************
3955
3956  Synopsis [Read onion rings flag for check_invariant]
3957
3958  SideEffects []
3959
3960******************************************************************************/
3961boolean
3962McOptionsReadInvarOnionRingsFlag(
3963  McOptions_t *options)
3964{
3965  return (options->invarOnionRingsFlag);
3966}
3967
3968/**Function********************************************************************
3969
3970  Synopsis [Read whether to use forward or backward analysis]
3971
3972  SideEffects []
3973
3974******************************************************************************/
3975Mc_FwdBwdAnalysis
3976McOptionsReadFwdBwd(
3977  McOptions_t *options)
3978{
3979  return options->fwdBwd;
3980}
3981
3982/**Function********************************************************************
3983
3984  Synopsis [Read whether to use forward or backward traversal.]
3985
3986  SideEffects []
3987
3988******************************************************************************/
3989Mc_FwdBwdAnalysis
3990McOptionsReadTraversalDirection(
3991  McOptions_t *options)
3992{
3993  return options->traversalDirection;
3994}
3995
3996/**Function********************************************************************
3997
3998  Synopsis [Read ARDC options.]
3999
4000  SideEffects []
4001
4002******************************************************************************/
4003Fsm_ArdcOptions_t *
4004McOptionsReadArdcOptions(
4005  McOptions_t *options)
4006{
4007  return options->ardcOptions;
4008}
4009
4010
4011/**Function********************************************************************
4012
4013  Synopsis [Read whether to do coverage computation using Hoskote et.al's algorithm]
4014
4015  SideEffects []
4016
4017******************************************************************************/
4018int
4019McOptionsReadCoverageHoskote(
4020  McOptions_t *options)
4021{
4022  return options->doCoverageHoskote;
4023}
4024
4025/**Function********************************************************************
4026
4027  Synopsis [Read whether to do coverage computation using the improved algorithm]
4028
4029  SideEffects []
4030
4031******************************************************************************/
4032int
4033McOptionsReadCoverageImproved(
4034  McOptions_t *options)
4035{
4036  return options->doCoverageImproved;
4037}
4038
4039/**Function********************************************************************
4040
4041  Synopsis [Set use forward or backward analysis]
4042
4043  SideEffects []
4044
4045******************************************************************************/
4046void
4047McOptionsSetFwdBwd(
4048  McOptions_t *options,
4049  Mc_FwdBwdAnalysis fwdBwd )
4050{
4051  options->fwdBwd = fwdBwd;
4052}
4053
4054/**Function********************************************************************
4055
4056  Synopsis [Set guided search file (set to NULL if no guided search)]
4057
4058  SideEffects []
4059
4060******************************************************************************/
4061void
4062McOptionsSetGuideFile(
4063  McOptions_t *options,
4064  FILE  *guideFile )
4065{
4066  options->guideFile = guideFile;
4067}
4068
4069/**Function********************************************************************
4070
4071  Synopsis [Set varibles for system file for FAFW]
4072
4073  SideEffects []
4074
4075******************************************************************************/
4076void
4077McOptionsSetVariablesForSystem(
4078  McOptions_t *options,
4079  FILE  *systemFile )
4080{
4081  options->systemFile = systemFile;
4082}
4083/**Function********************************************************************
4084
4085  Synopsis [Set use forward or backward traversal]
4086
4087  SideEffects []
4088
4089******************************************************************************/
4090void
4091McOptionsSetTraversalDirection(
4092  McOptions_t *options,
4093  Mc_FwdBwdAnalysis fwdBwd )
4094{
4095  options->traversalDirection = fwdBwd;
4096}
4097
4098/**Function********************************************************************
4099
4100  Synopsis [Set use more pipe flag at options.]
4101
4102  SideEffects []
4103
4104******************************************************************************/
4105void
4106McOptionsSetUseMore(
4107  McOptions_t *options,
4108  boolean useMore )
4109{
4110  options->useMore = useMore;
4111}
4112
4113/**Function********************************************************************
4114
4115  Synopsis [Set reduce fsm flag]
4116
4117  SideEffects []
4118
4119******************************************************************************/
4120void
4121McOptionsSetReduceFsm(
4122  McOptions_t *options,
4123  boolean reduceFsm )
4124{
4125  options->reduceFsm = reduceFsm;
4126}
4127
4128/**Function********************************************************************
4129
4130  Synopsis [Set Vacuity Detect flag]
4131
4132  SideEffects []
4133
4134******************************************************************************/
4135void
4136McOptionsSetVacuityDetect(
4137  McOptions_t *options,
4138  boolean vd )
4139{
4140  options->vd = vd;
4141}
4142
4143/**Function********************************************************************
4144
4145  Synopsis [Set Beer Method for vacuity detection flag]
4146
4147  SideEffects []
4148
4149******************************************************************************/
4150void
4151McOptionsSetBeerMethod(
4152  McOptions_t *options,
4153  boolean beer )
4154{
4155  options->beer = beer;
4156}
4157
4158/**Function********************************************************************
4159
4160  Synopsis [Set flag for fate and free will algorithm]
4161
4162  SideEffects []
4163
4164******************************************************************************/
4165void
4166McOptionsSetFAFWFlag(
4167  McOptions_t *options,
4168  boolean FAFWFlag )
4169{
4170  options->FAFWFlag = FAFWFlag;
4171}
4172/**Function********************************************************************
4173
4174  Synopsis [Set print inputs flag]
4175
4176  SideEffects []
4177
4178******************************************************************************/
4179void
4180McOptionsSetPrintInputs(
4181  McOptions_t *options,
4182  boolean printInputs )
4183{
4184  options->printInputs = printInputs;
4185}
4186
4187/**Function********************************************************************
4188
4189  Synopsis [Set use formula tree flag]
4190
4191  SideEffects []
4192
4193******************************************************************************/
4194void
4195McOptionsSetUseFormulaTree(
4196  McOptions_t *options,
4197  boolean useFormulaTree )
4198{
4199  options->useFormulaTree = useFormulaTree;
4200}
4201
4202/**Function********************************************************************
4203
4204  Synopsis [Set GSH schedule]
4205
4206  SideEffects []
4207
4208******************************************************************************/
4209void
4210McOptionsSetSchedule(
4211  McOptions_t *options,
4212  Mc_GSHScheduleType schedule )
4213{
4214  options->schedule = schedule;
4215}
4216
4217/**Function********************************************************************
4218
4219  Synopsis [Set lockstep option]
4220
4221  SideEffects []
4222
4223******************************************************************************/
4224void
4225McOptionsSetLockstep(
4226  McOptions_t *options,
4227  int lockstep )
4228{
4229  options->lockstep = lockstep;
4230}
4231
4232/**Function********************************************************************
4233
4234  Synopsis [Set sim flag at options.]
4235
4236  SideEffects []
4237
4238******************************************************************************/
4239void
4240McOptionsSetSimValue(
4241  McOptions_t *options,
4242  boolean simValue )
4243{
4244  options->simFormat = simValue;
4245}
4246
4247/**Function********************************************************************
4248
4249  Synopsis [Set Dbg level at options.]
4250
4251  SideEffects []
4252
4253******************************************************************************/
4254void
4255McOptionsSetDbgLevel(
4256  McOptions_t *options,
4257  McDbgLevel dbgLevel )
4258{
4259  options->dbgLevel = dbgLevel;
4260}
4261
4262/**Function********************************************************************
4263
4264  Synopsis [Set Verbosity at options.]
4265
4266  SideEffects []
4267
4268******************************************************************************/
4269void
4270McOptionsSetVerbosityLevel(
4271  McOptions_t *options,
4272  Mc_VerbosityLevel verbosityLevel )
4273{
4274  options->verbosityLevel = verbosityLevel;
4275}
4276
4277/**Function********************************************************************
4278
4279  Synopsis [Set language emptiness checking method at options.]
4280
4281  SideEffects []
4282
4283******************************************************************************/
4284void
4285McOptionsSetLeMethod(
4286  McOptions_t *options,
4287  Mc_LeMethod_t leMethod)
4288{
4289  options->leMethod = leMethod;
4290}
4291
4292/**Function********************************************************************
4293
4294  Synopsis [Set Dc level at options.]
4295
4296  SideEffects []
4297
4298******************************************************************************/
4299void
4300McOptionsSetDcLevel(
4301  McOptions_t *options,
4302  Mc_DcLevel dcLevel)
4303{
4304  options->dcLevel = dcLevel;
4305}
4306
4307/**Function********************************************************************
4308
4309  Synopsis [Set ARDC options.]
4310
4311  SideEffects []
4312
4313******************************************************************************/
4314void
4315McOptionsSetArdcOptions(
4316  McOptions_t *options,
4317  Fsm_ArdcOptions_t *ardcOptions)
4318{
4319  options->ardcOptions = ardcOptions;
4320}
4321
4322/**Function********************************************************************
4323
4324  Synopsis [Set a flag to store onion rings during invariant checking.]
4325
4326  SideEffects []
4327
4328******************************************************************************/
4329void
4330McOptionsSetInvarOnionRingsFlag(
4331  McOptions_t *options, int shellFlag)
4332{
4333  if (shellFlag) options->invarOnionRingsFlag = TRUE;
4334  else options->invarOnionRingsFlag = FALSE;
4335}
4336
4337
4338/**Function********************************************************************
4339
4340  Synopsis [Set CTL File at options.]
4341
4342  SideEffects []
4343
4344******************************************************************************/
4345void
4346McOptionsSetCtlFile(
4347  McOptions_t *options,
4348  FILE *file)
4349{
4350  options->ctlFile = file;
4351}
4352
4353/**Function********************************************************************
4354
4355  Synopsis [Set Debug File at options.]
4356
4357  SideEffects []
4358
4359******************************************************************************/
4360void
4361McOptionsSetDebugFile(
4362  McOptions_t *options,
4363  FILE *file)
4364{
4365  options->debugFile = file;
4366}
4367
4368/**Function********************************************************************
4369
4370  Synopsis [Set ime out periopd at options.]
4371
4372  SideEffects []
4373
4374******************************************************************************/
4375void
4376McOptionsSetTimeOutPeriod(
4377  McOptions_t *options,
4378  int timeOutPeriod)
4379{
4380  options->timeOutPeriod = timeOutPeriod;
4381}
4382
4383/**Function********************************************************************
4384
4385  Synopsis [Set reachability analysis type]
4386
4387  SideEffects []
4388
4389******************************************************************************/
4390void
4391McOptionsSetInvarApproxFlag(
4392  McOptions_t *options,
4393  Fsm_RchType_t approxFlag)
4394{
4395  options->invarApproxFlag = approxFlag;
4396}
4397
4398
4399
4400/**Function********************************************************************
4401
4402  Synopsis [Set do Coverage-Hoskote flag]
4403
4404  SideEffects []
4405
4406******************************************************************************/
4407void
4408McOptionsSetCoverageHoskote(
4409  McOptions_t *options,
4410  boolean doCoverageHoskote )
4411{
4412  options->doCoverageHoskote = doCoverageHoskote;
4413}
4414
4415/**Function********************************************************************
4416
4417  Synopsis [Set do Coverage-Improved flag]
4418
4419  SideEffects []
4420
4421******************************************************************************/
4422void
4423McOptionsSetCoverageImproved(
4424  McOptions_t *options,
4425  boolean doCoverageImproved )
4426{
4427  options->doCoverageImproved = doCoverageImproved;
4428}
4429
4430
4431/**Function********************************************************************
4432
4433  Synopsis [Query user to continue.]
4434
4435  SideEffects []
4436
4437******************************************************************************/
4438boolean
4439McQueryContinue(char *query)
4440{
4441  char result[2];
4442
4443  fprintf(vis_stdout, "%s", query);
4444  if (fgets(result, 2, stdin) == NULL) return FALSE;
4445
4446  if(!strcmp(result,"1"))
4447    return TRUE;
4448  else if(!strcmp(result,"0"))
4449    return FALSE;
4450  else {
4451    fprintf(vis_stdout, "-- Must enter 0/1\n");
4452    return McQueryContinue(query);
4453  }
4454}
4455
4456
4457/**Function********************************************************************
4458
4459  Synopsis [Print Support of Function]
4460
4461  SideEffects []
4462
4463******************************************************************************/
4464
4465void
4466McPrintSupport(
4467  mdd_t *aMdd,
4468  mdd_manager *mddMgr,
4469  Ntk_Network_t *aNetwork )
4470{
4471  int i;
4472  char *tmp1String, *tmp2String;
4473  char *mintermString = NIL(char);
4474  char bodyString[McMaxStringLength_c];
4475  array_t *aSupport = mdd_get_support( mddMgr, aMdd );
4476  array_t *stringArray = array_alloc( char *, 0 );
4477
4478  for ( i = 0 ; i < array_n( aSupport ); i++ ) {
4479
4480    int mddId = array_fetch( int, aSupport, i );
4481    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
4482    char *nodeName = Ntk_NodeReadName( node );
4483    sprintf( bodyString, "%s", nodeName );
4484    tmp1String = util_strsav( bodyString );
4485    array_insert_last( char *, stringArray, tmp1String );
4486  }
4487
4488  array_sort( stringArray, cmp);
4489
4490  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
4491    tmp1String = array_fetch( char *, stringArray, i );
4492    if( i == 0 )  {
4493      mintermString = util_strcat3(tmp1String, "", "" );
4494    }
4495    else {
4496      tmp2String = util_strcat3(mintermString, "\n", tmp1String );
4497      FREE(mintermString);
4498      mintermString = tmp2String;
4499    }
4500    FREE(tmp1String);
4501  }
4502  fprintf(vis_stdout, "%s\n", mintermString );
4503}
4504
4505
4506
4507/**Function********************************************************************
4508
4509  Synopsis [Print path as sim trace]
4510
4511  SideEffects []
4512
4513******************************************************************************/
4514
4515
4516
4517int
4518McPrintSimPath(
4519  FILE *outputFile,
4520  array_t *aPath,
4521  Fsm_Fsm_t *modelFsm)
4522{
4523  int i;
4524
4525  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
4526  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
4527
4528  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
4529  mdd_manager *mddMgr =  Fsm_FsmReadMddManager( modelFsm );
4530
4531  array_t *inputSortedVars = SortMddIds( inputVars, network );
4532  array_t *psSortedVars = SortMddIds( psVars, network );
4533
4534  fprintf(outputFile, "# UC Berkeley, VIS Release 1.3\n");
4535  fprintf(outputFile, "# Network: %s\n", Ntk_NetworkReadName( network ) );
4536  fprintf(outputFile, "# Simulation vectors have been generated to show language non-empty\n\n");
4537
4538  fprintf( outputFile, ".inputs " );
4539  PrintNodes( inputSortedVars, network );
4540  fprintf( outputFile, "\n" );
4541
4542  fprintf( outputFile, ".latches " );
4543  PrintNodes( psSortedVars, network );
4544  fprintf( outputFile, "\n" );
4545
4546  fprintf( outputFile, ".outputs\n" );
4547
4548  for( i = -1 ; i < (array_n( aPath ) - 1); i++ ) {
4549
4550    if ( i == -1 ) {
4551      mdd_t *initState = array_fetch( mdd_t *, aPath, (i+1) );
4552      array_t *initValues = McConvertMintermToValueArray( initState, psSortedVars, mddMgr );
4553
4554      fprintf( outputFile, ".initial ");
4555      PrintDeck( initValues, psSortedVars, network );
4556      array_free( initValues );
4557
4558      fprintf( outputFile, "\n" );
4559      fprintf( outputFile, ".start_vectors\n");
4560    }
4561    else {
4562      array_t *psValues;
4563      array_t *nsValues;
4564      array_t *inputValues;
4565
4566      mdd_t *psState = array_fetch( mdd_t *, aPath, i );
4567      mdd_t *nsState = array_fetch( mdd_t *, aPath, (i+1) );
4568      mdd_t *inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, psState, nsState );
4569      mdd_t *input = Mc_ComputeAMinterm( inputSet, inputVars, mddMgr );
4570
4571      inputValues = McConvertMintermToValueArray( input, inputSortedVars, mddMgr );
4572      PrintDeck( inputValues, inputSortedVars, network );
4573      array_free( inputValues );
4574      fprintf( outputFile, " ;");
4575
4576      psValues = McConvertMintermToValueArray( psState, psSortedVars, mddMgr );
4577      PrintDeck( psValues, psSortedVars, network );
4578      array_free( psValues );
4579      fprintf( outputFile, " ;");
4580
4581      nsValues = McConvertMintermToValueArray( nsState, psSortedVars, mddMgr );
4582      PrintDeck( nsValues, psSortedVars, network );
4583      array_free( nsValues );
4584      fprintf( outputFile, " ;\n");
4585
4586      mdd_free( inputSet );
4587      mdd_free( input );
4588    }
4589  }
4590  array_free( psSortedVars );
4591  array_free( inputSortedVars );
4592
4593  return 1;
4594}
4595
4596
4597/**Function********************************************************************
4598
4599  Synopsis [Form an FSM reduced with respect to the specified formula]
4600
4601  Description [Form an FSM reduced with respect to the CTL formula array. All latches
4602  and inputs which affect the given formula AND the fairness conditions of the
4603  system are included in this reduced fsm.]
4604
4605  SideEffects []
4606
4607******************************************************************************/
4608Fsm_Fsm_t *
4609McConstructReducedFsm(
4610  Ntk_Network_t *network,
4611  array_t *ctlFormulaArray )
4612{
4613  int i;
4614  Ntk_Node_t *node;
4615  array_t *nodeArray;
4616  st_table *formulaNodes;
4617  Ctlp_Formula_t *fairnessCondition;
4618  Ctlp_Formula_t *ctlFormula;
4619  array_t *formulaCombNodes;
4620  Fsm_Fsm_t *netFsm =  Fsm_NetworkReadFsm( network );
4621  Fsm_Fsm_t *reducedFsm;
4622  Fsm_Fairness_t *netFairness = Fsm_FsmReadFairnessConstraint( netFsm );
4623  array_t *reducedFsmFairness = array_alloc( Ctlp_Formula_t *, 0 );
4624
4625  if (netFairness) {
4626    if ( !Fsm_FairnessTestIsBuchi( netFairness ) ) {
4627      (void) fprintf(vis_stderr, "** mc error: non Buchi fairness constraints not supported\n");
4628      (void) fprintf(vis_stderr, "** mc error: ignoring fairness constraints\n");
4629    }
4630    else {
4631      int j;
4632      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( netFairness, 0 );
4633      for( j = 0 ; j < numBuchi; j++ ) {
4634        Ctlp_Formula_t *tmpFormula = Fsm_FairnessReadFinallyInfFormula( netFairness, 0, j );
4635        Ctlp_Formula_t *reducedFsmCondition = Ctlp_FormulaDup( tmpFormula );
4636        array_insert_last( Ctlp_Formula_t *, reducedFsmFairness, reducedFsmCondition );
4637      }
4638    }
4639  }
4640
4641  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );
4642  arrayForEachItem( Ctlp_Formula_t *, ctlFormulaArray, i, ctlFormula ) {
4643    NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
4644  }
4645
4646  arrayForEachItem( Ctlp_Formula_t *, reducedFsmFairness, i, fairnessCondition ) {
4647    NodeTableAddCtlFormulaNodes( network, fairnessCondition, formulaNodes );
4648  }
4649
4650  {
4651    st_generator *stGen;
4652    nodeArray = array_alloc( Ntk_Node_t *, 0 );
4653    st_foreach_item( formulaNodes, stGen, &node, NIL(char *) ) {
4654      array_insert_last( Ntk_Node_t *, nodeArray, node );
4655    }
4656  }
4657  st_free_table( formulaNodes );
4658
4659  formulaCombNodes  = Ntk_NodeComputeCombinationalSupport( network, nodeArray, FALSE );
4660  array_free( nodeArray );
4661  if(array_n(formulaCombNodes) == 0) {
4662
4663    /* Free the fairness constraint array (if any) */
4664    for (i=0; i<array_n(reducedFsmFairness); i++){
4665      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
4666                                            reducedFsmFairness, i);
4667      Ctlp_FormulaFree(formula);
4668    }
4669    array_free(reducedFsmFairness);
4670    /* Free the formulaCombNodes */
4671    array_free(formulaCombNodes);
4672    /* We should return a NIL fsm */
4673    return NIL(Fsm_Fsm_t);
4674  }
4675  {
4676    graph_t *dupPart;
4677    graph_t *origPart = Part_NetworkReadPartition( network );
4678    array_t *reducedFsmLatches = array_alloc( Ntk_Node_t *, 0 );
4679    array_t *reducedFsmInputs = array_alloc( Ntk_Node_t *, 0 );
4680    int i;
4681    arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
4682      if ( Ntk_NodeTestIsInput( node ) == TRUE ) {
4683        array_insert_last( Ntk_Node_t *, reducedFsmInputs, node );
4684      }
4685      else {
4686        assert( Ntk_NodeTestIsLatch( node ) == TRUE );
4687        array_insert_last( Ntk_Node_t *, reducedFsmLatches, node );
4688      }
4689    }
4690    if ((array_n(reducedFsmInputs) ==
4691         Ntk_NetworkReadNumInputs(network)) &&
4692        (array_n(reducedFsmLatches) ==
4693         Ntk_NetworkReadNumLatches(network))){
4694      /* We did not observe any reduction. Return a NIL fsm. */
4695      /* After freeing appropriate stuff */
4696
4697      /* Free the fairness constraint array (if any) */
4698      for (i=0; i<array_n(reducedFsmFairness); i++){
4699        Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
4700                                              reducedFsmFairness, i);
4701        Ctlp_FormulaFree(formula);
4702      }
4703      array_free(reducedFsmFairness);
4704      array_free(formulaCombNodes);
4705      array_free(reducedFsmLatches);
4706      array_free(reducedFsmInputs);
4707      return NIL(Fsm_Fsm_t);
4708    }
4709    dupPart = Part_PartitionDuplicate( origPart );
4710    array_free( formulaCombNodes );
4711    reducedFsm = Fsm_FsmCreateReducedFsm( network, dupPart, reducedFsmLatches,
4712                                          reducedFsmInputs, reducedFsmFairness );
4713    array_free( reducedFsmLatches );
4714    array_free( reducedFsmInputs );
4715    array_free( reducedFsmFairness );
4716  }
4717
4718  return reducedFsm;
4719
4720}
4721
4722/**Function********************************************************************
4723
4724  Synopsis [Update the early termination condition.]
4725
4726  Description [Update the early termination condition.
4727
4728  MC_NO_EARLY_TERMINATION is equivalent to mode=CARE and
4729  states=mdd_one.  careStates=NIL is equivalent to either
4730  careStates=mdd_zero (for disjunction) or careStates=mdd_one (in the
4731  other cases).  With these provisions, the propagation algorithm can
4732  be summarized thus.
4733
4734  <p> For negation, ALL becomes SOME and vice versa, while CARE is
4735  passed unchanged.
4736
4737  <p> For conjunction, disjunction, and implication: if the current
4738  node has a termination condition of type ALL or SOME, this is
4739  refined and propagated.  Otherwise, the returned early termination
4740  condition is of type CARE.  The care states are the conjunction of
4741  earlyTermination->states and either careStates (for conjunction and
4742  implication) or the complement of careStates (for disjunction).
4743
4744  <p> In some cases, one can immediately determine that the goal
4745  cannot be reached, or has already been reached.  In these cases, the
4746  termination condition has mode=CARE and states=mdd_zero.
4747
4748  <p> The other types of formulae produce no early termination
4749  condition for their children.  That is, they declare that all states
4750  are care states.]
4751
4752  SideEffects []
4753
4754******************************************************************************/
4755Mc_EarlyTermination_t *
4756McObtainUpdatedEarlyTerminationCondition(
4757  Mc_EarlyTermination_t *earlyTermination,
4758  mdd_t *careStates,
4759  Ctlp_FormulaType formulaType)
4760{
4761  Mc_EarlyTermination_t *result;
4762
4763  switch (formulaType) {
4764  case Ctlp_NOT_c:
4765    if (earlyTermination == MC_NO_EARLY_TERMINATION)
4766      return MC_NO_EARLY_TERMINATION;
4767    result = Mc_EarlyTerminationAlloc(earlyTermination->mode,
4768                                      earlyTermination->states);
4769    switch (result->mode) {
4770    case McAll_c:
4771      result->mode = McSome_c;
4772      break;
4773    case McSome_c:
4774      result->mode = McAll_c;
4775      break;
4776    case McCare_c:
4777      break;
4778    default:
4779      assert(0);
4780    }
4781    break;
4782  case Ctlp_AND_c:
4783    if (careStates == NIL(mdd_t)) {
4784      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
4785        result = MC_NO_EARLY_TERMINATION;
4786      } else if (earlyTermination->mode == McAll_c) {
4787        result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
4788      } else {
4789        /* Here mode is CARE or SOME: inherit care states from parent. */
4790        result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
4791      }
4792    } else {
4793      /* There are care states from sibling. */
4794      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
4795        /* No early termination from parent: just use sibling's care states. */
4796        result = Mc_EarlyTerminationAlloc(McCare_c, careStates);
4797      } else if (earlyTermination->mode == McAll_c) {
4798        /* If some goal states are not in care set, we know we cannot achieve
4799         * the goal; otherwise, we just propagate the parent's condition.
4800         */
4801        if (mdd_lequal(earlyTermination->states, careStates, 1, 1)) {
4802          result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
4803        } else {
4804          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
4805        }
4806      } else if (earlyTermination->mode == McSome_c) {
4807        /* If no goal states are in the care set, we have failed; otherwise
4808         * we refine the goal set to those states also in the care set.
4809         */
4810        if (mdd_lequal(earlyTermination->states, careStates, 1, 0)) {
4811          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
4812        } else {
4813          mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
4814          result = Mc_EarlyTerminationAlloc(McSome_c, andMdd);
4815          mdd_free(andMdd);
4816        }
4817      } else { /* if (earlyTermination->mode == McCare_c) */
4818        /* Intersect care states from parent and sibling. */
4819        mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
4820        result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
4821        mdd_free(andMdd);
4822      }
4823    }
4824    break;
4825  case Ctlp_THEN_c:
4826  case Ctlp_OR_c:
4827    if (careStates == NIL(mdd_t)) {
4828      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
4829        result = MC_NO_EARLY_TERMINATION;
4830      } else if (earlyTermination->mode == McSome_c) {
4831        if (formulaType == Ctlp_OR_c) {
4832          result = Mc_EarlyTerminationAlloc(McSome_c,
4833                                            earlyTermination->states);
4834        } else {
4835          result = Mc_EarlyTerminationAlloc(McAll_c,
4836                                            earlyTermination->states);
4837        }
4838      } else {
4839        /* Here mode is CARE or ALL: inherit care states from parent. */
4840        result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
4841      }
4842    } else {
4843      /* There are care states from sibling.
4844       * Since f->g is !f+g, we treat the THEN and OR cases together by
4845       * complementing the care set in the latter case. */
4846      mdd_t *mask = (formulaType == Ctlp_OR_c) ?
4847        bdd_not(careStates) : bdd_dup(careStates);
4848      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
4849        /* No early termination from parent: just use sibling's care states. */
4850        result = Mc_EarlyTerminationAlloc(McCare_c, mask);
4851      } else if (earlyTermination->mode == McAll_c) {
4852        /* Remove the goal states already attained from the goal set. */
4853        mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
4854        result = Mc_EarlyTerminationAlloc(McAll_c, andMdd);
4855        mdd_free(andMdd);
4856      } else if (earlyTermination->mode == McSome_c) {
4857        /* If some goal states were already attained, declare success;
4858         * otherwise just propagate the parent's condition.
4859         */
4860        if (mdd_lequal(earlyTermination->states, mask, 1, 1)) {
4861          result = Mc_EarlyTerminationAlloc(McSome_c,
4862                                            earlyTermination->states);
4863        } else {
4864          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* success */
4865        }
4866      } else { /* if (earlyTermination->mode == McCare_c) */
4867        /* Intersect care states from parent and sibling. */
4868        mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
4869        result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
4870        mdd_free(andMdd);
4871      }
4872      mdd_free(mask);
4873    }
4874    break;
4875  default:
4876    result = MC_NO_EARLY_TERMINATION;
4877  }
4878  return result;
4879
4880} /* McObtainUpdatedEarlyTerminationCondition */
4881
4882
4883/**Function********************************************************************
4884
4885  Synopsis [Check if an underapproximation of the evaluation
4886  guarantees that the early termination conditions hold.]
4887
4888  Description [Check if an underapproximation of the evaluation
4889  guarantees that the early termination conditions hold , modulo a
4890  care set modeled by an implicitly conjoined array of bdds.
4891
4892  If we are looking for ALL of ETstates, or we are are given a set of
4893  CARE states, then we are done if ETstates \subseteq underapprox,
4894  because that implies ETstates \subseteq exactset.
4895
4896  If we are looking for SOME of ETstates, we are done if underapprox and
4897  ETstates overlap, because that means that the exact set and ETstates also
4898  overlap.
4899
4900  If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the
4901  function is false.]
4902
4903  SideEffects []
4904
4905******************************************************************************/
4906boolean
4907McCheckEarlyTerminationForUnderapprox(
4908  Mc_EarlyTermination_t *earlyTermination,
4909  mdd_t *underApprox,
4910  array_t *careStatesArray)
4911{
4912  if(earlyTermination == MC_NO_EARLY_TERMINATION)
4913    return FALSE;
4914
4915  /* for an underapproximation and McAll_c (McSome_c), you just check
4916     whether all states (some states) are already reached */
4917  return(((earlyTermination->mode != McSome_c) &&
4918          (mdd_lequal_mod_care_set_array(earlyTermination->states, underApprox,
4919                                         1, 1, careStatesArray)))
4920         ||
4921         (
4922           (earlyTermination->mode == McSome_c) &&
4923           (!mdd_lequal_mod_care_set_array(underApprox,
4924                                           earlyTermination->states, 1,
4925                                           0, careStatesArray))));
4926}
4927
4928
4929/**Function********************************************************************
4930
4931  Synopsis [Check if an overapproximation of the evaluation guarantees
4932  that the early termination conditions hold.]
4933
4934  Description [Check if an overapproximation of the evaluation
4935  guarantees that the early termination conditions hold, modulo a care
4936  set modeled by an implicitly conjoined array of bdds.
4937
4938  If we are looking for ALL of ETstates, then we are done if we have
4939  overapprox is not a superset of ETstates, because the exact set will
4940  not hold all of ETstates.
4941
4942  If we are looking for SOME of ETstates, or we are given a set of
4943  CARE states, we are done if overapprox is disjoint from ETstates,
4944  because that means that the exact set is also disjoint from
4945  ETstates.
4946
4947  If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the
4948  function is false.]
4949
4950  SideEffects []
4951
4952******************************************************************************/
4953boolean
4954McCheckEarlyTerminationForOverapprox(
4955  Mc_EarlyTermination_t *earlyTermination,
4956  mdd_t *overApprox,
4957  array_t *careStatesArray)
4958{
4959  if(earlyTermination == MC_NO_EARLY_TERMINATION)
4960    return FALSE;
4961
4962  /* For an overapproximation and McAll_c (McSome_c), you check
4963     whether some state (all states) are already missing */
4964  return(((earlyTermination->mode == McAll_c) &&
4965          (!mdd_lequal_mod_care_set_array(earlyTermination->states,
4966                                          overApprox, 1, 1, careStatesArray)))
4967         ||
4968         ((earlyTermination->mode != McAll_c) &&
4969          (mdd_lequal_mod_care_set_array(earlyTermination->states,
4970                                          overApprox, 1, 0,
4971                                          careStatesArray))));
4972}
4973
4974
4975/**Function********************************************************************
4976
4977  Synopsis [Return an array of formulae representing the hints]
4978
4979  Description [Read the guide file and store the hint formulae in an
4980  array. Adds the 1 hint to the end of the array.
4981
4982  Returns NIL if something goes wrong: parse error in the file or temporal
4983  operators in the hints]
4984
4985  SideEffects []
4986
4987******************************************************************************/
4988array_t *
4989Mc_ReadHints(
4990  FILE *guideFP
4991  )
4992{
4993  Ctlp_FormulaArray_t *invarArray;   /* formulae representing hints */
4994  int i;                      /* to iterate over formulae        */
4995  Ctlp_Formula_t *formula;    /* idem                            */
4996
4997  if (guideFP == NIL(FILE)){
4998    fprintf(vis_stderr,
4999            "** mc error: can't read hint file.\n");
5000    return NIL(array_t);
5001  }
5002
5003  invarArray = Ctlp_FileParseFormulaArray( guideFP );
5004
5005  if (invarArray == NIL(array_t)){
5006    fprintf(vis_stderr,
5007            "** mc error: parse error in hints file.\n");
5008    return NIL(array_t);
5009  }
5010
5011  if (array_n(invarArray) == 0){
5012    fprintf(vis_stdout, "** mc error: File contained no hints.\n");
5013    Ctlp_FormulaArrayFree(invarArray);
5014    return NIL(array_t);
5015  }
5016
5017
5018  array_insert_last(Ctlp_Formula_t *, invarArray,
5019                    Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void)));
5020
5021  /* some checks */
5022  arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
5023    if(!Ctlp_FormulaTestIsQuantifierFree(formula)){
5024      (void) fprintf(vis_stdout,
5025                     "** mc error: Hints contain temporal operators\n");
5026
5027      Ctlp_FormulaArrayFree(invarArray);
5028      return NIL(array_t);
5029    } /* quantifier free */
5030
5031  }/* checks */
5032
5033
5034  return invarArray;
5035}/* Mc_ReadHints */
5036
5037/**Function********************************************************************
5038
5039  Synopsis [Return an array of variables controlled by system ]
5040
5041  Description [Read the system variables file and store the variables controlled by system in an array.
5042
5043  Returns NIL if something goes wrong: parse error in the file or variables that  are not contained in model.]
5044
5045  SideEffects []
5046
5047******************************************************************************/
5048st_table *
5049Mc_ReadSystemVariablesFAFW(
5050  Fsm_Fsm_t *fsm,
5051  FILE *systemFP
5052  )
5053{
5054  st_table *variablesTable;
5055  array_t *bddIdArray;
5056  char line[1024], nodeName[1024], *next;
5057  int mddId, bddId;
5058  int i, j, len, index;
5059  int errorFlag;
5060  Ntk_Node_t *node;
5061  Ntk_Network_t *network;
5062  mdd_manager *mgr;
5063
5064  errorFlag = 0;
5065  if (systemFP == NIL(FILE)){
5066    fprintf(vis_stderr,
5067            "** mc error: can't read system file.\n");
5068    return NIL(st_table);
5069  }
5070
5071  network = Fsm_FsmReadNetwork(fsm);
5072  mgr = Fsm_FsmReadMddManager(fsm);
5073  variablesTable = st_init_table(st_numcmp, st_numhash);
5074  while(fgets(line, 1024, systemFP)) {
5075    len = strlen(line);
5076    for(i=0; i<len; i++) {
5077      if(line[i] == ' ')        continue;
5078      if(line[i] == '\t')       continue;
5079      break;
5080    }
5081    next = &(line[i]);
5082    if(next[0] == '\n') continue;
5083    if(next[0] == '#')  continue;
5084    len = strlen(next);
5085    index = 0;
5086    nodeName[0] = '\0';
5087    for(i=0; i<len; i++) {
5088      if(next[i] == ' ') break;
5089      if(next[i] == '\t') break;
5090      if(next[i] == '\n') break;
5091      nodeName[index] = next[i];
5092      index++;
5093    }
5094    nodeName[index] = '\0';
5095    node = Ntk_NetworkFindNodeByName(network, nodeName);
5096    if(node == NIL(Ntk_Node_t)) {
5097      fprintf(vis_stderr, "Error : Can't find node '%s'\n", nodeName);
5098      errorFlag = 1;
5099      continue;
5100    }
5101    mddId = Ntk_NodeReadMddId(node);
5102    bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
5103    for(j=0; j<array_n(bddIdArray); j++) {
5104      bddId = array_fetch(int, bddIdArray, j);
5105      st_insert(variablesTable, (char *)(long)bddId, (char *)(long)bddId);
5106    }
5107    array_free(bddIdArray);
5108  }
5109
5110  if(variablesTable->num_entries == 0)  {
5111    st_free_table(variablesTable);
5112    variablesTable = 0;
5113  }
5114  if(errorFlag) {
5115    if(variablesTable)
5116      st_free_table(variablesTable);
5117    variablesTable = 0;
5118    return((st_table *)-1);
5119  }
5120  return variablesTable;
5121}/* Mc_ReadSystemVariablesFAFW */
5122
5123
5124/**Function********************************************************************
5125
5126  Synopsis []
5127
5128  Description []
5129
5130  SideEffects []
5131
5132******************************************************************************/
5133st_table *
5134Mc_SetAllInputToSystem(Fsm_Fsm_t *fsm)
5135{
5136  mdd_manager *mgr;
5137  array_t *inputVars, *bddIdArray;
5138  int i, j;
5139  int mddId, bddId;
5140  st_table *idTable;
5141
5142  idTable = st_init_table(st_numcmp, st_numhash);
5143  mgr = Fsm_FsmReadMddManager(fsm);
5144  /* inputVars = Fsm_FsmReadPrimaryInputVars(fsm); */
5145  inputVars = Fsm_FsmReadInputVars(fsm);
5146
5147  if(inputVars) {
5148    for(i=0; i<array_n(inputVars); i++) {
5149      mddId = array_fetch(int, inputVars, i);
5150      bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
5151      for(j=0; j<array_n(bddIdArray); j++) {
5152        bddId = array_fetch(int, bddIdArray, j);
5153        st_insert(idTable, (char *)(long)bddId, (char *)(long)bddId);
5154      }
5155    }
5156  }
5157  return(idTable);
5158
5159}
5160
5161/**Function********************************************************************
5162
5163  Synopsis [Return an array of states corresponding to the hints]
5164
5165  Description [Flushes the states associated with the hints,and reevaluates
5166  them in the current fsm. Quantifies out variables in the hint that are not in
5167  present state or primary input set of the current FSM.
5168
5169  Returns NIL if something goes wrong (the hint does not fit the fsm).]
5170
5171  SideEffects []
5172
5173******************************************************************************/
5174array_t *
5175Mc_EvaluateHints(
5176  Fsm_Fsm_t *fsm,
5177  Ctlp_FormulaArray_t *invarArray
5178  )
5179{
5180  array_t *invarStatesArray = NIL(array_t);/* array of sets of states: hints*/
5181  int i, j;                                       /* to iterate over formulae  */
5182  Ctlp_Formula_t *formula= NIL(Ctlp_Formula_t);/* idem                      */
5183  mdd_t *invarFormulaStates = NIL(mdd_t);/* states in which formula is true */
5184  mdd_t *one = NIL(mdd_t);
5185  array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
5186  array_t *inputVars = Fsm_FsmReadInputVars(fsm);
5187  array_t *psInputVars = array_join(psVars, inputVars);
5188  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
5189
5190  invarStatesArray = array_alloc(mdd_t *, 0);
5191
5192  one = mdd_one(Fsm_FsmReadMddManager(fsm));
5193
5194  arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
5195    /* semantic checks */
5196    if(!Mc_FormulaStaticSemanticCheckOnNetwork(formula,
5197                                               Fsm_FsmReadNetwork(fsm),
5198                                               TRUE)){
5199      (void) fprintf(vis_stdout,
5200                     "** mc error: Error evaluating hint:\n%s\n",
5201                     error_string());
5202
5203      mdd_free(one);
5204      mdd_array_free(invarStatesArray);
5205      return NIL(array_t);
5206    }/* if semantic error */
5207
5208    assert(Ctlp_FormulaTestIsQuantifierFree(formula));
5209
5210    Ctlp_FlushStates(formula);
5211
5212
5213    /* compute the set of states represented by the invariant. */
5214    invarFormulaStates =
5215      Mc_FsmEvaluateFormula(fsm, formula, one,
5216                            NIL(Fsm_Fairness_t), NIL(array_t),
5217                            MC_NO_EARLY_TERMINATION,
5218                            NIL(Fsm_HintsArray_t), Mc_None_c,
5219                            McVerbosityNone_c, McDcLevelNone_c, 0,
5220                            McGSH_EL_c);
5221
5222
5223    if (!mdd_check_support(mddMgr, invarFormulaStates, psInputVars)) {
5224      mdd_t *temp;
5225      int mddId;
5226      array_t *supportArray = mdd_get_support(mddMgr, invarFormulaStates);
5227      array_t *leftOverVars = array_alloc(int, 0);
5228      /* store the PS and the Input Vars of this FSM */
5229      st_table *supportTable = st_init_table(st_numcmp, st_numhash);
5230
5231      arrayForEachItem(int, psInputVars, j, mddId) {
5232        (void) st_insert(supportTable, (char *) (long) mddId, NIL(char));
5233      }
5234
5235      /* isolate the vars outside this FSM */
5236      arrayForEachItem(int, supportArray, j, mddId) {
5237        if (st_is_member(supportTable, (char *)(long)mddId) == 0) {
5238          array_insert_last(int, leftOverVars, mddId);
5239        }
5240      }
5241
5242      /* Quantify them out */
5243      if (array_n(leftOverVars) > 0) {
5244        fprintf(vis_stdout, "GS warning ** Quantifying out variables not relevant to the reduced FSM in hint %d. \n", i+1);
5245        arrayForEachItem(int, leftOverVars, j, mddId) {
5246          fprintf(vis_stdout, "%s\n", (mdd_get_var_by_id(mddMgr, mddId)).name);
5247        }
5248        temp = mdd_smooth(mddMgr,  invarFormulaStates, leftOverVars);
5249        mdd_free(invarFormulaStates);
5250        invarFormulaStates = temp;
5251      }
5252      array_free(leftOverVars);
5253      st_free_table(supportTable);
5254      array_free(supportArray);
5255    }
5256
5257    array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
5258  }/* for each formula */
5259
5260  array_free(psInputVars);
5261  mdd_free(one);
5262  return invarStatesArray;
5263}/* Mc_EvaluateHints */
5264
5265/**Function********************************************************************
5266
5267  Synopsis [Return an array of hints]
5268
5269  Description [Read the guide file and compute the BDDs of the hints
5270  and store in an array. Adds the 1 hint to the end of the array.
5271
5272  Closes the guideFP.
5273
5274  Returns NIL if something goes wrong.]
5275
5276  SideEffects []
5277
5278******************************************************************************/
5279array_t *
5280Mc_ComputeGuideArray(
5281  Fsm_Fsm_t *fsm,
5282  FILE *guideFP
5283  )
5284{
5285  Ctlp_FormulaArray_t *hintFormulae;
5286  array_t             * hintSets;
5287
5288  hintFormulae = Mc_ReadHints(guideFP);
5289  fclose(guideFP);
5290
5291  if( hintFormulae == NIL(Ctlp_FormulaArray_t))
5292    return NIL(array_t);
5293
5294  hintSets = Mc_EvaluateHints(fsm, hintFormulae);
5295
5296  Ctlp_FormulaArrayFree(hintFormulae);
5297
5298  return hintSets;
5299}/* Mc_ComputeGuideArray */
5300
5301
5302/**Function********************************************************************
5303
5304  Synopsis [Read and parse the hints_type set flag]
5305
5306  Description [Read and parse the hints_type set flag.  If it is not
5307  set return the default: local.  Return Mc_None_c if there is an
5308  error.]
5309
5310  SideEffects []
5311
5312******************************************************************************/
5313Mc_GuidedSearch_t Mc_ReadGuidedSearchType(void)
5314{
5315  char *string =  Cmd_FlagReadByName("guided_search_hint_type");
5316
5317  if(string == NIL(char))  /* default */
5318    return Mc_Local_c;
5319  if(!strcmp(string, "global"))
5320    return Mc_Global_c;
5321  if(!strcmp(string, "local"))
5322    return Mc_Local_c;
5323  else
5324    return Mc_None_c;
5325}
5326
5327
5328/**Function********************************************************************
5329
5330  Synopsis [Debug function to check if there exists a proper input value]
5331
5332  Description [Check the existence of path by extracting input condition.]
5333
5334  SideEffects []
5335
5336******************************************************************************/
5337void
5338Mc_CheckPathToCore(Fsm_Fsm_t *fsm, array_t *pathToCore)
5339{
5340  array_t *inputVars;
5341  int i;
5342  mdd_t *fromState, *toState, *inputSet;
5343  mdd_manager   *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
5344
5345  inputVars = Fsm_FsmReadInputVars( fsm );
5346  for(i=-1; i<array_n(pathToCore)-1; i++) {
5347    fromState = (i==-1) ? 0 : array_fetch(mdd_t *, pathToCore, i);
5348    toState = array_fetch(mdd_t *, pathToCore, i+1);
5349    if((long)fromState % 2)     fromState = (mdd_t *)((long)fromState - 1);
5350    if((long)toState % 2)       toState = (mdd_t *)((long)toState - 1);
5351    inputSet = ( i == -1) ? 0 :
5352                 Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );
5353
5354    if(inputSet)
5355      Mc_ComputeAMinterm( inputSet, inputVars, mgr );
5356    else if(i != -1)
5357      fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
5358  }
5359
5360}
5361
5362/**Function********************************************************************
5363
5364  Synopsis [Debug function to check if there exists a proper input value]
5365
5366  Description [Check the existence of path by extracting input condition.]
5367
5368  SideEffects []
5369
5370******************************************************************************/
5371void
5372Mc_CheckPathFromCore(Fsm_Fsm_t *fsm, array_t *pathFromCore)
5373{
5374  array_t *inputVars;
5375  int i;
5376  mdd_t *fromState, *toState, *inputSet;
5377  mdd_manager   *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
5378
5379  inputVars = Fsm_FsmReadInputVars( fsm );
5380  for(i=array_n(pathFromCore); i>0; i--) {
5381    fromState = (i==array_n(pathFromCore)) ? 0 : array_fetch(mdd_t *, pathFromCore, i);
5382    toState = array_fetch(mdd_t *, pathFromCore, i-1);
5383    if((long)fromState % 2)     fromState = (mdd_t *)((long)fromState - 1);
5384    if((long)toState % 2)       toState = (mdd_t *)((long)toState - 1);
5385    inputSet = ( i == array_n(pathFromCore)) ? 0 :
5386      Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );
5387
5388    if(inputSet)
5389      Mc_ComputeAMinterm( inputSet, inputVars, mgr );
5390    else if(i != array_n(pathFromCore))
5391      fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
5392  }
5393}
5394
5395/**Function********************************************************************
5396
5397  Synopsis [Print states in terms of state variables]
5398
5399  Description [Print states in terms of state variables]
5400
5401  SideEffects []
5402
5403******************************************************************************/
5404void
5405Mc_PrintStates(
5406  Fsm_Fsm_t *modelFsm,
5407  mdd_t *states)
5408{
5409  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
5410  Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
5411  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
5412  mdd_t *zeroMdd, *new_states;
5413  char  *tmpString;
5414  double   size;
5415
5416 /*
5417  *  sometimes, this function will be constrained by number of minterm
5418  *     in the given set of states.
5419  *     num_minterm = mdd_num_of_mintern(states);
5420  *     if(num_minterm > MAX_MINTERM)   {
5421  *       fprintf( stdout, "Too many minterms in given states\n" );
5422  *       return;
5423  *     }
5424  */
5425  if((long)states % 2) {
5426    states = (mdd_t *)((long)states - 1);
5427  }
5428  zeroMdd = mdd_zero( mddMgr );
5429  states = mdd_dup(states);
5430  if(mdd_equal(states, zeroMdd)) {
5431    fprintf(stdout, "ZERO mdd\n");
5432    mdd_free(zeroMdd);
5433    return;
5434  }
5435  size = mdd_count_onset(mddMgr, states, PSVars);
5436  if(size > 40.0) {
5437    fprintf(stdout, "Too many minterms in given states %.0f\n", size);
5438    return;
5439  }
5440  fprintf( stdout, "    " );
5441  while(1) {
5442    mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );
5443
5444    new_states = mdd_and( states, result, 1, 0 );
5445    mdd_free( states );
5446    states = new_states;
5447
5448    tmpString = Mc_MintermToString( result, PSVars, aNetwork );
5449    fprintf( stdout, "%s ", tmpString );
5450    FREE(tmpString);
5451    mdd_free( result );
5452
5453    if(mdd_equal(states, zeroMdd)) {
5454      mdd_free(zeroMdd);
5455      mdd_free(states);
5456      break;
5457    }
5458  }
5459  fprintf(stdout, "\n");
5460}
5461
5462/**Function********************************************************************
5463
5464  Synopsis [Print the number of states]
5465
5466  Description [Print the number of states.]
5467
5468  SideEffects []
5469
5470******************************************************************************/
5471void
5472Mc_PrintNumStates(
5473  Fsm_Fsm_t *modelFsm,
5474  mdd_t *states)
5475{
5476  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
5477  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
5478  mdd_t *zeroMdd;
5479  double size;
5480
5481 /*
5482  *  sometimes, this function will be constrained by number of minterm
5483  *     in the given set of states.
5484  *     num_minterm = mdd_num_of_mintern(states);
5485  *     if(num_minterm > MAX_MINTERM)   {
5486  *       fprintf( stdout, "Too many minterms in given states\n" );
5487  *       return;
5488  *     }
5489  */
5490  if((long)states % 2) {
5491    states = (mdd_t *)((long)states - 1);
5492  }
5493  zeroMdd = mdd_zero( mddMgr );
5494  states = mdd_dup(states);
5495  if(mdd_equal(states, zeroMdd)) {
5496    fprintf(stdout, "ZERO mdd\n");
5497    mdd_free(zeroMdd);
5498    mdd_free(states);
5499    return;
5500  }
5501  size = mdd_count_onset(mddMgr, states, PSVars);
5502  fprintf(stdout, "num states : %.0f\n", size);
5503  mdd_free(zeroMdd);
5504  mdd_free(states);
5505}
5506
5507/**Function********************************************************************
5508
5509  Synopsis [Print the states of each ring]
5510
5511  Description [Print the states of each ring]
5512
5513  SideEffects []
5514
5515******************************************************************************/
5516void
5517Mc_PrintRings(
5518  Fsm_Fsm_t *modelFsm,
5519  array_t *onionRings)
5520{
5521  int j;
5522  mdd_t *innerRing;
5523
5524  if(array_n(onionRings) > 0) {
5525    for(j=0; j<array_n(onionRings); j++) {
5526      innerRing = array_fetch(mdd_t *, onionRings, j);
5527      fprintf(vis_stdout, "%d'th ring : ", j);
5528      if(innerRing)
5529        Mc_PrintStates(modelFsm, innerRing);
5530      else
5531        fprintf(vis_stdout, "\n");
5532    }
5533  }
5534}
5535
5536/**Function********************************************************************
5537
5538  Synopsis [Print the number of states of each ring]
5539
5540  Description [Print the number of states of each ring]
5541
5542  SideEffects []
5543
5544******************************************************************************/
5545void
5546Mc_PrintNumRings(
5547  Fsm_Fsm_t *modelFsm,
5548  array_t *onionRings)
5549{
5550  int j;
5551  mdd_t *innerRing;
5552
5553  if(array_n(onionRings) > 0) {
5554    for(j=0; j<array_n(onionRings); j++) {
5555      innerRing = array_fetch(mdd_t *, onionRings, j);
5556      fprintf(vis_stdout, "%d'th ring : ", j);
5557      if(innerRing)
5558        Mc_PrintNumStates(modelFsm, innerRing);
5559      else
5560        fprintf(vis_stdout, "\n");
5561    }
5562  }
5563}
5564
5565
5566/**Function********************************************************************
5567
5568  Synopsis [Pick a minterm from the given set close to target. Support
5569  is an array of mddids representing the total support; that is, all
5570  the variables on which aSet may depend.]
5571
5572  SideEffects []
5573
5574******************************************************************************/
5575mdd_t *
5576McComputeACloseMinterm(
5577  mdd_t *aSet,
5578  mdd_t *target,
5579  array_t *Support,
5580  mdd_manager *mddMgr)
5581{
5582  if (bdd_get_package_name() == CUDD) {
5583    mdd_t *range;             /* range of Support             */
5584    mdd_t *legalSet;          /* aSet without the don't cares */
5585    mdd_t *closeCube;
5586    int dist;
5587    array_t *bddSupport;      /* Support in terms of bdd vars */
5588    mdd_t *minterm;           /* a random minterm             */
5589
5590    /* Check that support of set is contained in Support. */
5591    assert(SetCheckSupport(aSet, Support, mddMgr));
5592    assert(!mdd_is_tautology(aSet, 0));
5593    range      = mdd_range_mdd(mddMgr, Support);
5594    legalSet   = bdd_and(aSet, range, 1, 1);
5595    mdd_free(range);
5596    closeCube = mdd_closest_cube(legalSet, target, &dist);
5597    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
5598    minterm    = bdd_pick_one_minterm(closeCube, bddSupport);
5599
5600    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
5601    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
5602    assert(mdd_lequal(minterm,legalSet,1,1));
5603
5604    mdd_array_free(bddSupport);
5605    mdd_free(legalSet);
5606    mdd_free(closeCube);
5607
5608    return minterm;
5609  } else {
5610    return Mc_ComputeAMinterm(aSet, Support, mddMgr);
5611  }/* if CUDD */
5612
5613} /* McComputeACloseMinterm */
5614
5615/**Function********************************************************************
5616
5617  Synopsis [Select a state from the given set]
5618
5619  SideEffects []
5620
5621******************************************************************************/
5622mdd_t *
5623McComputeACloseState(
5624  mdd_t *states,
5625  mdd_t *target,
5626  Fsm_Fsm_t *modelFsm)
5627{
5628  array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
5629  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(
5630    Fsm_FsmReadNetwork(modelFsm));
5631  mdd_t *result;
5632
5633  if (mdd_is_tautology(target, 0)) {
5634    result = Mc_ComputeAMinterm(states, PSVars, mddMgr);
5635  } else {
5636    result = McComputeACloseMinterm(states, target, PSVars, mddMgr);
5637  }
5638
5639  return result;
5640
5641} /* McComputeACloseState */
5642
5643
5644/**Function********************************************************************
5645
5646  Synopsis    [Converts a string to a schedule type.]
5647
5648  Description [Converts a string to a schedule type.  If string does
5649  not refer to one of the allowed schedule types, then returns
5650  McGSH_Unassigned_c.]
5651
5652  SideEffects []
5653
5654******************************************************************************/
5655Mc_GSHScheduleType
5656McStringConvertToScheduleType(
5657  char *string)
5658{
5659  if (strcmp("off", string) == 0) {
5660    return McGSH_old_c;
5661  } else if (strcmp("EL", string) == 0) {
5662    return McGSH_EL_c;
5663  } else if (strcmp("EL1", string) == 0) {
5664    return McGSH_EL1_c;
5665  } else if (strcmp("EL2", string) == 0) {
5666    return McGSH_EL2_c;
5667  } else if (strcmp("random", string) == 0) {
5668    return McGSH_Random_c;
5669  } else if (strcmp("budget", string) == 0) {
5670    return McGSH_Budget_c;
5671  } else {
5672    return McGSH_Unassigned_c;
5673  }
5674
5675} /* McStringConvertToScheduleType */
5676
5677
5678/**Function********************************************************************
5679
5680  Synopsis    [Converts a string to a lockstep mode.]
5681
5682  Description [Converts a string to a lockstep mode.  If string does
5683  not refer to one of the allowed lockstep modes, it returns
5684  MC_LOCKSTEP_UNASSIGNED.  The allowed values are: MC_LOCKSTEP_OFF,
5685  MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive
5686  integer n (lockstep enumerates up to n fair SCCs).]
5687
5688  SideEffects []
5689
5690******************************************************************************/
5691int
5692McStringConvertToLockstepMode(
5693  char *string)
5694{
5695  int n;
5696
5697  if (strcmp("off", string) == 0) {
5698    return MC_LOCKSTEP_OFF;
5699  } else if (strcmp("on", string) == 0) {
5700    return MC_LOCKSTEP_EARLY_TERMINATION;
5701  } else if (strcmp("all", string) == 0) {
5702    return MC_LOCKSTEP_ALL_SCCS;
5703  } else if (Cmd_StringCheckIsInteger(string, &n) == 2) {
5704    return n;
5705  } else {
5706    return MC_LOCKSTEP_UNASSIGNED;
5707  }
5708
5709} /* McStringConvertToLockstepMode */
5710
5711
5712/*---------------------------------------------------------------------------*/
5713/* Definition of static functions                                            */
5714/*---------------------------------------------------------------------------*/
5715
5716/**Function********************************************************************
5717
5718  Synopsis [Print  an array of nodes]
5719
5720  SideEffects []
5721
5722******************************************************************************/
5723
5724static void
5725PrintNodes(
5726  array_t *mddIdArray,
5727  Ntk_Network_t *network )
5728{
5729  int i;
5730  int mddId;
5731
5732  arrayForEachItem(int , mddIdArray, i, mddId) {
5733    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
5734    char *nodeName = Ntk_NodeReadName( node );
5735    fprintf(vis_stdout, " %s ", nodeName );
5736  }
5737}
5738
5739
5740/**Function********************************************************************
5741
5742  Synopsis [Print  an array of nodes]
5743
5744  SideEffects []
5745
5746******************************************************************************/
5747
5748static array_t *
5749SortMddIds(
5750  array_t *mddIdArray,
5751  Ntk_Network_t *network )
5752{
5753  int i;
5754  int mddId;
5755  char *nodeName;
5756  st_table *nameToIndex = st_init_table( strcmp, st_strhash );
5757  array_t *nodeNameArray = array_alloc( char *, 0 );
5758  array_t *result = array_alloc( int, 0 );
5759
5760  arrayForEachItem(int, mddIdArray, i, mddId) {
5761    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
5762    nodeName = Ntk_NodeReadName( node );
5763    st_insert( nameToIndex, nodeName, (char *) (long) i );
5764    array_insert_last(  char *, nodeNameArray, nodeName );
5765  }
5766  array_sort( nodeNameArray, cmp);
5767
5768  arrayForEachItem(char *, nodeNameArray, i, nodeName ) {
5769    int index;
5770    st_lookup_int( nameToIndex, nodeName, & index );
5771    mddId = array_fetch( int, mddIdArray, index );
5772    array_insert_last( int, result, mddId );
5773  }
5774  st_free_table( nameToIndex );
5775  array_free( nodeNameArray );
5776
5777  return result;
5778}
5779
5780/**Function********************************************************************
5781
5782  Synopsis [Print  an array of nodes]
5783
5784  SideEffects []
5785
5786******************************************************************************/
5787
5788
5789static void
5790PrintDeck(
5791  array_t *mddValues,
5792  array_t *mddIdArray,
5793  Ntk_Network_t *network )
5794{
5795  int i;
5796  int mddId;
5797
5798  arrayForEachItem(int, mddIdArray, i, mddId) {
5799    int value = array_fetch( int, mddValues, i );
5800    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
5801    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
5802    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
5803      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
5804      fprintf( vis_stdout, "%s ", symbolicValue );
5805    }
5806    else {
5807      fprintf( vis_stdout, "%d ", value );
5808    }
5809  }
5810}
5811
5812/**Function********************************************************************
5813
5814  Synopsis [Compare two strings in the from of char **]
5815
5816  SideEffects []
5817
5818******************************************************************************/
5819static int
5820cmp(
5821  const void * s1,
5822  const void * s2)
5823{
5824  return(strcmp(*(char **)s1, *(char **)s2));
5825}
5826
5827/**Function********************************************************************
5828
5829  Synopsis [Perform simple static semantic checks on formula.]
5830
5831  SideEffects []
5832
5833  SeeAlso [Mc_FormulaStaticSemanticCheckOnNetwork]
5834******************************************************************************/
5835static boolean
5836AtomicFormulaCheckSemantics(
5837  Ctlp_Formula_t *formula,
5838  Ntk_Network_t *network,
5839  boolean inputsAllowed)
5840{
5841
5842  char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
5843  char *nodeValueString = Ctlp_FormulaReadValueName( formula );
5844  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
5845
5846  Var_Variable_t *nodeVar;
5847  int nodeValue;
5848
5849  if ( !node ) {
5850    error_append("Could not find node corresponding to the name\n\t- ");
5851    error_append( nodeNameString );
5852    error_append("\n(Wire for this name may have been removed by synthesis)");
5853    return FALSE;
5854  }
5855
5856  nodeVar = Ntk_NodeReadVariable( node );
5857  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
5858
5859    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
5860    if ( nodeValue == -1 ) {
5861      error_append("Value specified in RHS is not in domain of variable\n");
5862      error_append( Ctlp_FormulaReadVariableName( formula ) );
5863      error_append("=");
5864      error_append( Ctlp_FormulaReadValueName( formula ) );
5865      return FALSE;
5866    }
5867  }
5868  else {
5869    int check;
5870
5871    check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
5872    if( check==0 ) {
5873      error_append("Value in the RHS is illegal\n");
5874      error_append( Ctlp_FormulaReadVariableName( formula ) );
5875      error_append("=");
5876      error_append( Ctlp_FormulaReadValueName( formula ) );
5877      return FALSE;
5878    }
5879    if( check==1 ) {
5880      error_append("Value in the RHS is out of range of int\n");
5881      error_append( Ctlp_FormulaReadVariableName( formula ) );
5882      error_append("=");
5883      error_append( Ctlp_FormulaReadValueName( formula ) );
5884      return FALSE;
5885    }
5886    if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
5887      error_append("Value specified in RHS is not in domain of variable\n");
5888      error_append( Ctlp_FormulaReadVariableName( formula ) );
5889      error_append("=");
5890      error_append( Ctlp_FormulaReadValueName( formula ) );
5891      return FALSE;
5892    }
5893  }
5894
5895  if(!inputsAllowed){
5896    boolean coverSupport;
5897    lsGen tmpGen;
5898    Ntk_Node_t *tmpNode;
5899    st_table *supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
5900    array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);
5901
5902    array_insert_last( Ntk_Node_t *, thisNodeArray, node );
5903    Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
5904      if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
5905        st_insert(supportNodes, (char *) tmpNode, NIL(char));
5906      }
5907    }
5908
5909    coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
5910                                                            thisNodeArray,
5911                                                            supportNodes);
5912    array_free(thisNodeArray);
5913    st_free_table(supportNodes);
5914
5915    if ( coverSupport == FALSE ) {
5916      char *tmpString =
5917        util_strcat3( "\nNode ", nodeNameString,
5918                      " is not driven only by latches and constants.\n");
5919      error_append(tmpString);
5920      return FALSE;
5921    }
5922  }
5923
5924  return TRUE;
5925}
5926
5927/**Function********************************************************************
5928
5929  Synopsis [Add nodes for wires referred to in formula to nodesTable.]
5930
5931  SideEffects []
5932
5933******************************************************************************/
5934static void
5935NodeTableAddCtlFormulaNodes(
5936  Ntk_Network_t *network,
5937  Ctlp_Formula_t *formula,
5938  st_table * nodesTable )
5939{
5940  if ( formula == NIL(Ctlp_Formula_t) ) {
5941        return;
5942  }
5943
5944  if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
5945    char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
5946    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
5947    if( node )
5948      st_insert( nodesTable, ( char *) node, NIL(char) );
5949    return;
5950  }
5951
5952  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
5953  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );
5954
5955  return;
5956}
5957
5958/**Function********************************************************************
5959
5960  Synopsis [Add nodes for wires referred to in formula to nodesTable.]
5961
5962  SideEffects []
5963
5964******************************************************************************/
5965static void
5966NodeTableAddLtlFormulaNodes(
5967  Ntk_Network_t *network,
5968  Ctlsp_Formula_t *formula,
5969  st_table * nodesTable )
5970{
5971  if ( formula == NIL(Ctlsp_Formula_t) ) {
5972        return;
5973  }
5974
5975  if ( Ctlsp_FormulaReadType( formula ) == Ctlsp_ID_c ) {
5976    char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
5977    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
5978    if( node )
5979      st_insert( nodesTable, ( char *) node, NIL(char) );
5980    return;
5981  }
5982
5983  NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadRightChild( formula ), nodesTable );
5984  NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadLeftChild( formula ), nodesTable );
5985
5986  return;
5987}
5988
5989/**Function********************************************************************
5990
5991  Synopsis [Test that given mdd is a minterm.]
5992
5993  SideEffects []
5994
5995******************************************************************************/
5996static boolean
5997MintermCheckWellFormed(
5998  mdd_t *aMinterm,
5999  array_t *aSupport,
6000  mdd_manager *mddMgr)
6001{
6002
6003  /* first check its support */
6004  if (!SetCheckSupport(aMinterm, aSupport, mddMgr)) {
6005    return FALSE;
6006  }
6007
6008  /* now check its a minterm */
6009  {
6010    float cardinality = mdd_count_onset( mddMgr, aMinterm, aSupport );
6011    if ( cardinality != 1 ) {
6012      fprintf( vis_stderr, "-- onset is not one\n");
6013      return FALSE;
6014    }
6015  }
6016  return TRUE;
6017}
6018
6019
6020/**Function********************************************************************
6021
6022  Synopsis [Test that given mdd is a minterm.]
6023
6024  SideEffects []
6025
6026******************************************************************************/
6027static boolean
6028SetCheckSupport(
6029  mdd_t *aMinterm,
6030  array_t *aSupport,
6031  mdd_manager *mddMgr)
6032{
6033  if (!mdd_check_support(mddMgr, aMinterm, aSupport)) {
6034    fprintf(vis_stderr,
6035      "** mc error: support of minterm is not contained in claimed support\n");
6036    return FALSE;
6037  }
6038  return TRUE;
6039}
Note: See TracBrowser for help on using the repository browser.