source: vis_dev/vis-2.3/src/mc/mcDbg.c @ 104

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

vis2.3
File size: 59.0 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [mcDbg.c]
4
5  PackageName [mc]
6
7  Synopsis    [Debugger for Fair CTL models]
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
34static char rcsid[] UNUSED = "$Id: mcDbg.c,v 1.43 2005/04/23 04:40:54 fabio Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Macro declarations                                                        */
38/*---------------------------------------------------------------------------*/
39
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static void DebugID(McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm);
48static void DebugTrueFalse(Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm);
49static void DebugBoolean(McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
50static McPath_t * DebugEX(Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
51static McPath_t * DebugEU(Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
52static McPath_t * DebugEG(Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, McOptions_t *options);
53static void FsmStateDebugConvertedFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
54static void FsmPathDebugFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray);
55static void FsmPathDebugEXFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray);
56static void FsmPathDebugEUFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray);
57static void FsmPathDebugEGFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray);
58static void FsmPathDebugEFFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray);
59static void FsmPathDebugAXFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray);
60static void FsmPathDebugAFFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray);
61static void FsmPathDebugAGFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray);
62static void FsmPathDebugAUFormula(McOptions_t *options, mdd_t *aState, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
63
64/**AutomaticEnd***************************************************************/
65
66
67/*---------------------------------------------------------------------------*/
68/* Definition of exported functions                                          */
69/*---------------------------------------------------------------------------*/
70
71/*---------------------------------------------------------------------------*/
72/* Definition of internal functions                                          */
73/*---------------------------------------------------------------------------*/
74
75/**Function********************************************************************
76
77  Synopsis [Debug CTL formula in existential normal form]
78
79  Description [Debug CTL formula in existential normal form. The extent to
80  which debug information is generated is a function of options settings.
81
82  The debugger works with ctlFormula, but uses the pointers back to
83  the original formula that it was converted from, to give the user
84  more sensible feedback.  To do this, it relies on a specific
85  translation: only EF, AU, AF, AG, and AX are converted.  Hence, the
86  only times that the converted bit is set, we have a conversion of
87  one of these formulas, and the operator is either EU, or negation.
88  in the latter case, we can conclude from the child of the negation
89  what formula we converted from: EX means AX, EG means AF, EU means AG,
90  and OR means AU.
91  ]
92
93  SideEffects [Affects vis_stdpipe]
94
95  SeeAlso     [Ctlp_FormulaConvertToExistentialForm]
96
97******************************************************************************/
98int
99McFsmDebugFormula(
100  McOptions_t *options,
101  Ctlp_Formula_t *ctlFormula,
102  Fsm_Fsm_t *modelFsm,
103  array_t *careSetArray)
104{
105  mdd_t *modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
106  mdd_t *goodStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
107  mdd_t *badStates = mdd_and(modelInitialStates, goodStates, 1, 0);
108  mdd_t *witnessSuccState;
109  FILE *debugFile = McOptionsReadDebugFile(options);
110  FILE *oldStdOut;
111  FILE *oldStdErr;
112  extern FILE *vis_stdpipe;
113  char *nrOfTracesString;
114  int nrOfTraces;   /* nr of debug traces that we output */
115  int i;            /* counts debug traces               */
116
117  mdd_free(modelInitialStates);
118
119  oldStdOut = vis_stdout;
120  oldStdErr = vis_stderr;
121 
122  nrOfTracesString = Cmd_FlagReadByName("nr_counterexamples");
123  if(nrOfTracesString == NIL(char))
124    nrOfTraces = 1;
125  else
126    nrOfTraces = atoi(nrOfTracesString);
127 
128  if (debugFile) {
129    vis_stdpipe = debugFile;
130    vis_stdout = vis_stdpipe;
131   (void)fprintf(vis_stdpipe, "# MC: formula failed --- ");
132    Ctlp_FormulaPrint(vis_stdpipe,Ctlp_FormulaReadOriginalFormula(ctlFormula));
133    (void)fprintf(vis_stdpipe, "\n");
134  } else if (McOptionsReadUseMore(options)){
135    vis_stdpipe = popen("more", "w");
136    vis_stdout = vis_stdpipe;
137    vis_stderr = vis_stdpipe;
138  }
139  else
140    vis_stdpipe = vis_stdout;
141
142  for(i = 0; i < nrOfTraces; i++){
143    (void)fprintf(vis_stdout, "# MC: Calling debugger for trace %d\n",
144                  i+1);
145    witnessSuccState = McComputeACloseState(badStates, goodStates, modelFsm);
146    McFsmStateDebugFormula(options, ctlFormula, witnessSuccState, modelFsm,
147                           careSetArray);
148    (void)fprintf(vis_stdout, "\n");
149
150    mdd_free(witnessSuccState);
151  }
152  mdd_free(badStates);
153  mdd_free(goodStates);
154
155  if (vis_stdout != oldStdOut && vis_stdout != debugFile)
156    (void)pclose(vis_stdpipe);
157
158  vis_stdout = oldStdOut;
159  vis_stderr = oldStdErr;
160
161  return 1;
162}
163
164/**Function********************************************************************
165
166  Synopsis [Debug CTL formula in existential normal form at state aState]
167
168  Description [Debug CTL formula in existential normal form at state
169  aState. Formula is assumed to have been CONVERTED to existential normal
170  form.]
171
172  SideEffects []
173
174******************************************************************************/
175void
176McFsmStateDebugFormula(
177  McOptions_t *options,
178  Ctlp_Formula_t *ctlFormula,
179  mdd_t *aState,
180  Fsm_Fsm_t *modelFsm,
181  array_t *careSetArray)
182{
183  Ctlp_Formula_t *originalFormula;
184  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
185
186  if ( ctlFormula == NIL(Ctlp_Formula_t) )
187    return;
188
189  if ( Ctlp_FormulaTestIsConverted( ctlFormula ) ) {
190    FsmStateDebugConvertedFormula(options, ctlFormula, aState, modelFsm,
191                                  careSetArray);
192    return;
193  }
194
195  originalFormula = Ctlp_FormulaReadOriginalFormula( ctlFormula );
196
197  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
198
199    case Ctlp_ID_c :
200      DebugID( options, ctlFormula, aState, modelFsm );
201      break;
202
203    case Ctlp_TRUE_c:
204    case Ctlp_FALSE_c:
205      DebugTrueFalse( ctlFormula, aState, modelFsm );
206      break;
207
208    case Ctlp_EQ_c:
209    case Ctlp_XOR_c:
210    case Ctlp_THEN_c:
211    case Ctlp_NOT_c:
212    case Ctlp_AND_c:
213    case Ctlp_OR_c:
214      DebugBoolean(options, ctlFormula, aState, modelFsm, careSetArray);
215      break;
216
217    case Ctlp_EX_c:
218    case Ctlp_EU_c:
219    case Ctlp_EG_c:
220      if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) {
221        mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
222        mdd_t *closeState;
223        Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm);
224        array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
225        McStateFailsFormula(aState, originalFormula, debugLevel, modelFsm);
226        if (mdd_is_tautology(passStates, 0)) {
227          fprintf(vis_stdout,
228                  "--No state satisfies the formula\n");
229          mdd_free(passStates);
230          break;
231        }
232        fprintf(vis_stdout,
233                "--A simple counter example does not exist since it\n");
234        fprintf(vis_stdout,
235                "  requires generating all paths from the state\n");
236        fprintf(vis_stdout,
237                "--A state at minimum distance satisfying the formula is\n");
238        closeState = McComputeACloseState(passStates, aState, modelFsm);
239        mdd_free(passStates);
240        Mc_MintermPrint(closeState, PSVars, modelNetwork);
241        mdd_free(closeState);
242        break;
243      }
244      else {
245        McPath_t *witnessPath = NIL(McPath_t);
246        if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EX_c ) {
247          witnessPath = DebugEX(ctlFormula, aState, modelFsm, careSetArray);
248        }
249        else if  ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) {
250          witnessPath = DebugEU(ctlFormula, aState, modelFsm, careSetArray);
251        }
252        else {
253          witnessPath = DebugEG(ctlFormula, aState, modelFsm, careSetArray,
254                                options);
255        }
256
257        FsmPathDebugFormula(options, ctlFormula, modelFsm, witnessPath,
258                            careSetArray);
259        McPathFree( witnessPath );
260      }
261      break;
262
263    case Ctlp_Cmp_c:
264    case Ctlp_Init_c:
265    case Ctlp_FwdU_c:
266    case Ctlp_FwdG_c:
267    case Ctlp_EY_c:
268    case Ctlp_EH_c:
269      break;
270
271    default: {
272      fail("Bad switch in debugging normal formula\n");
273    }
274  }
275}
276
277
278
279
280/**Function********************************************************************
281
282  Synopsis [Build fair path starting from aState, using given debug information.]
283
284  Description [Build fair path starting from aState, using given array of
285  onion rings.  Each member of this array of onion rings is an array of rings
286  of states leading to a fairness constraint. Function returns an McPath_t,
287  which consists of a stem array which is a sequence of states, and a path
288  array which is a sequence of states starting from the last state in stem
289  array, leading back to a state existing in stem array. In this sense, it is
290  confusing, since the "cycle" is not a true cycle (it just completes a
291  cycle).]
292
293  Comment [Proceed by building a path which passes through each fairness
294  constraint.  Then attempt to complete a cycle by seeing if a path can be
295  found from the last state to the first state satisfying the first fairness
296  constraint.]
297
298  SideEffects []
299
300******************************************************************************/
301McPath_t *
302McBuildFairPath(
303  mdd_t *startState,
304  mdd_t *invariantStates,
305  array_t *arrayOfOnionRings,
306  Fsm_Fsm_t *modelFsm,
307  array_t *careSetArray,
308  Mc_VerbosityLevel verbosity,
309  Mc_DcLevel dcLevel,
310  Mc_FwdBwdAnalysis fwdBwd )
311{
312  mdd_t *tmpState;
313  mdd_t *lastState;
314  mdd_t *rootState = mdd_dup( startState );
315  mdd_t *currentState = mdd_dup( rootState );
316  mdd_t *stemState = NIL(mdd_t);
317
318  array_t *tmpStemArray;
319  array_t *dupArrayOfOnionRings = array_dup( arrayOfOnionRings );
320  array_t *stemArray = array_alloc(mdd_t *, 0 );
321  array_t *cycleArray = NIL(array_t);
322  McPath_t *fairPath;
323
324  array_insert_last( mdd_t *, stemArray, currentState );
325
326  while ( array_n( dupArrayOfOnionRings ) > 0 ) {
327    int index = McComputeOnionRingsWithClosestCore(currentState,
328                        dupArrayOfOnionRings, modelFsm);
329    array_t *onionRingsWithClosestFairness = array_fetch(array_t *,
330                        dupArrayOfOnionRings, index);
331    array_t *tmpArray = Mc_BuildPathToCore(currentState,
332                                onionRingsWithClosestFairness,
333                                modelFsm, McGreaterOrEqualZero_c);
334
335    if ( stemState == NIL(mdd_t) ) {
336      tmpState = array_fetch_last( mdd_t *, tmpArray );
337      stemState = mdd_dup( tmpState );
338    }
339
340    tmpStemArray = McCreateMergedPath( stemArray, tmpArray );
341    McNormalizeBddPointer(stemArray);
342    McNormalizeBddPointer(tmpArray);
343    mdd_array_free( stemArray );
344    mdd_array_free( tmpArray );
345    stemArray = tmpStemArray;
346
347    currentState = array_fetch_last( mdd_t *, stemArray );
348
349    tmpArray = McRemoveIndexedOnionRings( index, dupArrayOfOnionRings );
350    array_free( dupArrayOfOnionRings );
351    dupArrayOfOnionRings = tmpArray;
352  } /* while onionrings left */
353    array_free( dupArrayOfOnionRings );
354
355  tmpState = GET_NORMAL_PT(array_fetch_last( mdd_t *, stemArray ));
356  lastState = mdd_dup( tmpState );
357
358  cycleArray = Mc_CompletePath(lastState, stemState, invariantStates, modelFsm,
359                               careSetArray, verbosity, dcLevel, fwdBwd);
360
361  if ( cycleArray != NIL(array_t) ) {
362    mdd_free( lastState );
363  }
364  else {
365    McPath_t *tmpFairPath;
366    array_t *tmpStemArray;
367
368    /*
369     * Get shortest path to lastState
370     */
371    McNormalizeBddPointer(stemArray);
372    mdd_array_free( stemArray );
373    if ( !mdd_equal( rootState, lastState ) ) {
374      stemArray = Mc_CompletePath(rootState, lastState, invariantStates,
375                                  modelFsm, careSetArray, verbosity, dcLevel,
376                                  fwdBwd);
377    }
378    else {
379      stemArray = array_alloc( mdd_t *, 0 );
380      tmpState = mdd_dup( rootState );
381      array_insert_last( mdd_t *, stemArray, tmpState );
382    }
383    mdd_free( lastState );
384
385    tmpState = GET_NORMAL_PT(array_fetch_last( mdd_t *, stemArray ));
386    lastState = mdd_dup( tmpState );
387
388    if ( mdd_equal( lastState, rootState ) ) {
389      /*
390       * Force a descent in the SCC DAG
391      mdd_t *descendantState = McGetSuccessorInTarget(lastState,
392                                                invariantStates, modelFsm);
393       */
394      mdd_t *descendantState = McGetSuccessorInTargetAmongFairStates(lastState,
395                                                invariantStates, arrayOfOnionRings, modelFsm);
396      tmpFairPath = McBuildFairPath(descendantState, invariantStates,
397                                    arrayOfOnionRings, modelFsm,
398                                    careSetArray,
399                                    verbosity, dcLevel, fwdBwd);
400      tmpStemArray = McCreateJoinedPath(stemArray,
401                                        McPathReadStemArray(tmpFairPath));
402      mdd_free( descendantState );
403    }
404    else {
405      tmpFairPath = McBuildFairPath(lastState, invariantStates,
406                                    arrayOfOnionRings, modelFsm,
407                                    careSetArray, 
408                                    verbosity, dcLevel, fwdBwd);
409      tmpStemArray = McCreateMergedPath(stemArray,
410                                        McPathReadStemArray(tmpFairPath));
411    }
412    mdd_free( lastState );
413    McNormalizeBddPointer(stemArray);
414    mdd_array_free( stemArray );
415    stemArray = tmpStemArray;
416
417    cycleArray = McMddArrayDuplicateFAFW( McPathReadCycleArray( tmpFairPath ) );
418
419    McPathFree( tmpFairPath );
420
421    if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
422       mdd_t *S = GET_NORMAL_PT(array_fetch(mdd_t *, stemArray, 0));
423       mdd_t *T = GET_NORMAL_PT(array_fetch(mdd_t *, stemArray, array_n(stemArray)-1));
424       array_t *forwardRings = Mc_BuildForwardRingsWithInvariants(
425                                S, T, invariantStates, modelFsm);
426       tmpStemArray = Mc_BuildPathFromCoreFAFW(
427                                T, forwardRings, modelFsm, McGreaterOrEqualZero_c);
428       McNormalizeBddPointer(stemArray);
429       mdd_array_free(stemArray);
430       mdd_array_free(forwardRings);
431       stemArray = tmpStemArray;
432    }
433  }
434
435  mdd_free( rootState );
436  mdd_free( stemState );
437
438  fairPath = McPathAlloc();
439  McPathSetStemArray( fairPath, stemArray );
440  McPathSetCycleArray( fairPath, cycleArray );
441
442  return fairPath;
443}
444
445
446/*---------------------------------------------------------------------------*/
447/* Definition of static functions                                            */
448/*---------------------------------------------------------------------------*/
449
450
451/**Function********************************************************************
452
453  Synopsis    [Debug an Atomic Formula]
454
455  Description [Debug an Atomic Formula. As per the semantics of fair CTL, a
456  state satisfies an Atomic Formula just in case the given wire computes the
457  appropriate Boolean function on that state as input. The state has to be
458  fair; however we do NOT justify the fairness by printing a path to a fair
459  cycle.  THe user can achieve this effect by adding ANDing in a formula EG
460  TRUE.]
461
462  SideEffects []
463
464******************************************************************************/
465static void
466DebugID(
467  McOptions_t *options,
468  Ctlp_Formula_t *aFormula,
469  mdd_t *aState,
470  Fsm_Fsm_t *modelFsm)
471{
472  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula); 
473  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
474
475  if ( McStateSatisfiesFormula( aFormula, aState ) ) {
476    McStatePassesFormula( aState, originalFormula, debugLevel, modelFsm );
477  }
478  else {
479    McStateFailsFormula( aState, originalFormula, debugLevel, modelFsm );
480  }
481}
482
483/**Function********************************************************************
484
485  Synopsis    [Debug a TRUE/FALSE formula]
486
487  SideEffects []
488
489******************************************************************************/
490static void
491DebugTrueFalse(
492  Ctlp_Formula_t *aFormula,
493  mdd_t *aState,
494  Fsm_Fsm_t *modelFsm)
495{
496  fprintf(vis_stdout, "--Nothing to debug for %s\n",
497    ((Ctlp_FormulaReadType(aFormula) == Ctlp_TRUE_c) ? "TRUE\n" : "FALSE\n"));
498}
499
500/**Function********************************************************************
501
502  Synopsis    [Debug a Boolean formula]
503
504  Desciption  [Debug a Boolean formula. For Boolean formula built out of binary
505  connective, we may debug only one branch, if say the formula is an AND and
506  the left branch is fails.]
507
508  SideEffects []
509
510******************************************************************************/
511static void
512DebugBoolean(
513  McOptions_t *options,
514  Ctlp_Formula_t *aFormula,
515  mdd_t *aState,
516  Fsm_Fsm_t *modelFsm,
517  array_t *careSetArray)
518{
519  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula);
520  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( aFormula );
521  Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( aFormula );
522  McDbgLevel debugLevel = McOptionsReadDbgLevel(options);
523
524  if (McStateSatisfiesFormula(aFormula, aState)) {
525    McStatePassesFormula(aState, originalFormula, debugLevel, modelFsm);
526  } else {
527    McStateFailsFormula(aState, originalFormula, debugLevel, modelFsm);
528  }
529
530  /* We always debug the first (left) child. */
531  McFsmStateDebugFormula(options, lFormula, aState, modelFsm, careSetArray);
532
533  /* What we do for the second child depends on the type of the formula.
534   * For Ctlp_AND_c, Ctlp_OR_c, Ctlp_THEN_c the right child may not be
535   * needed.  With early termination, the right child may not have the
536   * information required to produce a counterexample;  hence, its debugging
537   * is not optional.  (We may get incorrect answers.)
538   */
539  if (Ctlp_FormulaReadType(aFormula) == Ctlp_AND_c) {
540    /* If aFormula fails and aState does not satisfy lFormula
541     * 1. The information about aState at the right child is not
542     *    necessarilty correct.  (aState was a don't care state.)
543     * 2. A counterexample to lFormula is a counterexample to
544     *    aFormula.
545     * So, if aFormula fails, we should debug the right child only if
546     * aState satisfies lFormula.
547     * If, on the other hand, aFormula passes, then aState must satisfy
548     * lFormula, and we need to witness both lFormula and rFormula.
549     */
550    if (McStateSatisfiesFormula(lFormula, aState)) {
551      McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
552                             careSetArray);
553    }
554  } else if (Ctlp_FormulaReadType(aFormula) == Ctlp_OR_c) {
555    /* if aFormula passes, we should debug the right child only if
556     * aState does not satisfy lFormula.
557     * If, on the other hand, aFormula fails, then aState may not satisfy
558     * lFormula, and we need to produce counterexamples for both lFormula
559     * and rFormula.
560     */
561    if (!McStateSatisfiesFormula(lFormula, aState)) {
562      McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
563                             careSetArray);
564    }
565  } else if (Ctlp_FormulaReadType(aFormula) == Ctlp_THEN_c) {
566    /* This case is like the OR, with the polarity of the left
567     * left child reversed.
568     */
569    if (McStateSatisfiesFormula(lFormula, aState)) {
570      McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
571                             careSetArray);
572    }
573  } else if (Ctlp_FormulaReadType(aFormula) != Ctlp_NOT_c) {
574    /* For Ctlp_EQ_c and Ctlp_XOR_c both children must be debugged. */
575    McFsmStateDebugFormula(options, rFormula, aState, modelFsm, careSetArray);
576  }
577}
578
579/**Function********************************************************************
580
581  Synopsis    [Debug a formula of type EX.]
582
583  Description [Debug a formula of type EX at specified state. It is assumed
584  that aState satisfies the EX formula.]
585
586  SideEffects []
587
588******************************************************************************/
589static McPath_t *
590DebugEX(
591  Ctlp_Formula_t *aFormula,
592  mdd_t *aState,
593  Fsm_Fsm_t *modelFsm,
594  array_t *careSetArray)
595{
596  mdd_t *aDupState = mdd_dup( aState );
597  mdd_t *aStateSuccs;
598  mdd_t *statesSatisfyingLeftFormula;
599  mdd_t *targetStates;
600  mdd_t *witnessSuccState;
601  Ctlp_Formula_t *lFormula;
602  McPath_t *witnessPath = McPathAlloc();
603  array_t *stemArray = array_alloc( mdd_t *, 0 );
604  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
605
606  /*
607   * By using careSet here, can end up with unreachable successors
608   */
609  aStateSuccs = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
610                        aState, aState, careSetArray);
611
612  lFormula = Ctlp_FormulaReadLeftChild( aFormula );
613  statesSatisfyingLeftFormula = Ctlp_FormulaObtainLatestApprox( lFormula );
614
615  targetStates = mdd_and( aStateSuccs, statesSatisfyingLeftFormula, 1, 1 );
616  mdd_free( aStateSuccs ); mdd_free( statesSatisfyingLeftFormula );
617
618  witnessSuccState = Mc_ComputeACloseState( targetStates, aState, modelFsm );
619  mdd_free( targetStates );
620
621  array_insert_last( mdd_t *, stemArray, aDupState );
622  array_insert_last( mdd_t *, stemArray, witnessSuccState );
623
624  McPathSetStemArray( witnessPath, stemArray );
625
626  return witnessPath;
627}
628
629/**Function********************************************************************
630
631  Synopsis    [Debug a formula of type EU.]
632
633  Description [Debug a formula of type EU at specified state. It is assumed that
634  state fails formula.]
635
636  SideEffects []
637
638******************************************************************************/
639static McPath_t *
640DebugEU(
641  Ctlp_Formula_t *aFormula,
642  mdd_t *aState,
643  Fsm_Fsm_t *modelFsm,
644  array_t *careSetArray)
645{
646  McPath_t *witnessPath = McPathAlloc();
647  array_t *OnionRings = (array_t *) Ctlp_FormulaReadDebugData( aFormula );
648  array_t *pathToCore = Mc_BuildPathToCore(aState, OnionRings, 
649                                           modelFsm,
650                                           McGreaterOrEqualZero_c );
651
652  McPathSetStemArray( witnessPath, pathToCore );
653
654  return witnessPath;
655}
656
657/**Function********************************************************************
658
659  Synopsis    [Debug a formula of type EG.]
660
661  Description [Debug a formula of type EG at specified state. It is assumed
662  that state fails formula. Refer to Clarke et al DAC 1995 for details of the
663  algorithm.]
664
665  SideEffects []
666
667******************************************************************************/
668static McPath_t *
669DebugEG(
670  Ctlp_Formula_t *aFormula,
671  mdd_t *aState,
672  Fsm_Fsm_t *modelFsm,
673  array_t *careSetArray,
674  McOptions_t *options)
675{
676  array_t *arrayOfOnionRings = (array_t *) Ctlp_FormulaReadDebugData(aFormula);
677  mdd_t *invariantMdd = Ctlp_FormulaObtainLatestApprox( aFormula );
678  McPath_t *fairPath = McBuildFairPath(aState, invariantMdd, arrayOfOnionRings,
679                                        modelFsm, careSetArray,
680                                        McOptionsReadVerbosityLevel(options),
681                                        McOptionsReadDcLevel(options),
682                                        McOptionsReadFwdBwd(options));
683  mdd_free( invariantMdd );
684
685  return fairPath;
686}
687
688
689/**Function********************************************************************
690
691  Synopsis    [Debug a converted formula]
692
693  Comment [There are five kinds of formula that are converted: EF, AU, AF, AG,
694  AX.  The Ctlp_Formula_t structure has a pointer back to the original formula
695  (where one exists). For the non-trivial cases (AU, AF, AG, AX) if the
696  formula is false, we create a counter example, i.e. a fair path which fails
697  the property. The AG, AX, AF cases are simple; the AU case is tricky because
698  this can be failed on two ways.]
699
700  SideEffects []
701
702******************************************************************************/
703static void
704FsmStateDebugConvertedFormula(
705  McOptions_t *options,
706  Ctlp_Formula_t *ctlFormula,
707  mdd_t *aState,
708  Fsm_Fsm_t *modelFsm,
709  array_t *careSetArray)
710{
711  McPath_t *witnessPath;
712  McPath_t *counterExamplePath;
713
714  Ctlp_Formula_t *originalFormula =Ctlp_FormulaReadOriginalFormula(ctlFormula);
715  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
716  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
717
718  if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) {
719    if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) {
720      mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
721      mdd_t *closeState;
722      Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm);
723      array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
724      McStateFailsFormula( aState, originalFormula, debugLevel, modelFsm );
725      if (mdd_is_tautology(passStates, 0)) {
726          fprintf(vis_stdout,
727                  "--No state satisfies the formula\n");
728      } else {
729        fprintf(vis_stdout,
730                "\n--A simple counter example does not exist since it\n");
731        fprintf(vis_stdout,
732                "  requires generating all paths from the state\n");
733        fprintf(vis_stdout,
734                "--A state at minimum distance satisfying the formula is\n");
735        closeState = McComputeACloseState(passStates, aState, modelFsm);
736        Mc_MintermPrint(closeState, PSVars, modelNetwork);
737        mdd_free(closeState);
738      }
739      mdd_free(passStates);
740    }
741    else {
742      witnessPath = DebugEU(ctlFormula, aState, modelFsm, careSetArray);
743      FsmPathDebugEFFormula(options, ctlFormula, modelFsm, witnessPath,
744                            careSetArray);
745      McPathFree( witnessPath );
746    }
747    return;
748  }
749
750  /*
751   * The original formula must be an AX,AF,AG, or AU formula
752   */
753  if ( McStateSatisfiesFormula( ctlFormula, aState ) ) {
754    McStatePassesFormula( aState, originalFormula, debugLevel, modelFsm );
755    fprintf(vis_stdout,
756            "--A simple witness does not exist since it requires\n");
757    fprintf(vis_stdout, "  generating all paths from the state\n");
758    return;
759  }
760
761  switch ( Ctlp_FormulaReadType( lFormula ) ) {
762    case Ctlp_EX_c: {
763      counterExamplePath = DebugEX(lFormula, aState, modelFsm, careSetArray);
764      FsmPathDebugAXFormula(options, ctlFormula, modelFsm, counterExamplePath,
765                            careSetArray);
766      McPathFree( counterExamplePath );
767      break;
768    }
769
770    case Ctlp_EG_c: {
771      counterExamplePath = DebugEG(lFormula, aState, modelFsm, careSetArray,
772                                   options);
773      FsmPathDebugAFFormula(options, ctlFormula, modelFsm, counterExamplePath,
774                            careSetArray);
775      McPathFree( counterExamplePath );
776      break;
777    }
778
779    case Ctlp_EU_c: {
780      counterExamplePath = DebugEU(lFormula, aState, modelFsm, careSetArray);
781      FsmPathDebugAGFormula(options, ctlFormula, modelFsm, counterExamplePath,
782                            careSetArray);
783      McPathFree( counterExamplePath );
784      break;
785    }
786
787    case Ctlp_OR_c: {
788      /*
789       * need special functions bcoz of two possibilities
790       */
791      FsmPathDebugAUFormula(options, aState, ctlFormula, modelFsm,
792                            careSetArray);
793      break;
794    }
795
796    default: fail("Bad formula type in handling converted operator\n");
797  }
798}
799
800
801/**Function********************************************************************
802
803  Synopsis [Debug a formula of the form EX, EG, EU, EF.]
804
805  SideEffects []
806
807******************************************************************************/
808static void
809FsmPathDebugFormula(
810  McOptions_t *options,
811  Ctlp_Formula_t *ctlFormula,
812  Fsm_Fsm_t *modelFsm,
813  McPath_t *witnessPath,
814  array_t *careSetArray)
815{
816  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
817    case Ctlp_EX_c: {
818      FsmPathDebugEXFormula(options, ctlFormula, modelFsm, witnessPath,
819                            careSetArray);
820      break;
821    }
822
823    case Ctlp_EU_c: {
824      FsmPathDebugEUFormula(options, ctlFormula, modelFsm, witnessPath,
825                            careSetArray);
826      break;
827    }
828
829    case Ctlp_EG_c: {
830      FsmPathDebugEGFormula(options, ctlFormula, modelFsm, witnessPath,
831                            careSetArray);
832      break;
833    }
834    default: {
835      fail("bad switch in converting converted formula\n");
836    }
837  }
838}
839
840/**Function********************************************************************
841
842  Synopsis [Debug a path for EX type formula.]
843
844  SideEffects []
845
846******************************************************************************/
847static void
848FsmPathDebugEXFormula(
849  McOptions_t *options,
850  Ctlp_Formula_t *ctlFormula,
851  Fsm_Fsm_t *modelFsm,
852  McPath_t *witnessPath,
853  array_t *careSetArray)
854{
855  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
856  array_t *witnessArray = McPathReadStemArray( witnessPath );
857  mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
858  char *firstStateName = Mc_MintermToString(firstState, PSVars,
859                                Fsm_FsmReadNetwork(modelFsm));
860  Ctlp_Formula_t *lChild = Ctlp_FormulaReadLeftChild( ctlFormula );
861  char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
862  boolean printInputs = McOptionsReadPrintInputs( options );
863  mdd_t *secondlastState;
864  if(array_n(witnessArray)<2)
865    {
866      fprintf(vis_stdout,"witnessArray has less than two elements, return\n");
867      return;
868    }
869  secondlastState= array_fetch( mdd_t *, witnessArray, (array_n(witnessArray)-1) );
870
871  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
872    fprintf(vis_stdout, "--State\n%spasses EX formula\n\n",
873            firstStateName); 
874  else
875    fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
876            ctlFormulaText );
877 
878  FREE(firstStateName);
879  FREE(ctlFormulaText);
880 
881 
882  switch ( McOptionsReadDbgLevel( options ) ) {
883  case McDbgLevelMin_c:
884  case McDbgLevelMinVerbose_c:
885  case McDbgLevelMax_c:
886    fprintf(vis_stdout, " --Counter example begins\n");
887    Mc_PrintPath( witnessArray, modelFsm, printInputs );
888    fprintf(vis_stdout, " --Counter example ends\n\n");
889    McFsmStateDebugFormula(options, lChild, secondlastState, modelFsm,
890                           careSetArray);
891    break;
892  case McDbgLevelInteractive_c:
893    fprintf(vis_stdout, " --Counter example begins\n");
894    Mc_PrintPath( witnessArray, modelFsm, printInputs );
895    fprintf(vis_stdout, " --Counter example ends\n\n");
896    if (McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n")) 
897    McFsmStateDebugFormula(options, lChild, secondlastState, modelFsm,
898                             careSetArray);
899    break;
900  default: 
901    fail("Reached bad switch in FsmPathDebugEXFormula\n");
902  }
903}
904
905/**Function********************************************************************
906
907  Synopsis [Debug a path for EU type formula.]
908
909  SideEffects []
910
911******************************************************************************/
912static void
913FsmPathDebugEUFormula(
914  McOptions_t *options,
915  Ctlp_Formula_t *ctlFormula,
916  Fsm_Fsm_t *modelFsm,
917  McPath_t *witnessPath,
918  array_t *careSetArray)
919{
920  char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
921  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
922  Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula );
923  char *lFormulaText = Ctlp_FormulaConvertToString( lFormula );
924  char *rFormulaText = Ctlp_FormulaConvertToString( rFormula );
925  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
926  array_t *witnessArray = McPathReadStemArray( witnessPath );
927  mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
928  mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray ));
929  char *firstStateName = Mc_MintermToString(firstState, PSVars,
930                                            Fsm_FsmReadNetwork(modelFsm));
931  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
932  boolean printInputs = McOptionsReadPrintInputs( options );
933
934 if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
935   fprintf(vis_stdout, "--State\n%spasses EU formula\n\n",
936           firstStateName); 
937 else
938   fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
939           ctlFormulaText );
940
941 FREE(firstStateName);
942 FREE(ctlFormulaText);
943 
944  switch ( debugLevel ) {
945  case McDbgLevelMin_c:
946  case McDbgLevelMinVerbose_c:
947      if ( array_n(witnessArray ) == 1 ) {
948        if( debugLevel != McDbgLevelMin_c )
949          fprintf(vis_stdout, "since %s is true at this state", rFormulaText);
950        McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
951                               careSetArray);
952      }
953      else {
954        if( debugLevel != McDbgLevelMin_c )
955          fprintf(vis_stdout, "--Path on which %s is true till %s is true\n",
956                  lFormulaText, rFormulaText);
957        fprintf(vis_stdout, " --Counter example begins\n");
958        Mc_PrintPath(witnessArray, modelFsm, printInputs);
959        fprintf(vis_stdout, " --Counter example ends\n\n");
960        McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
961                               careSetArray);
962      }
963    break;
964  case McDbgLevelMax_c:
965  case McDbgLevelInteractive_c: 
966    if ( array_n(witnessArray ) == 1 ) {
967      fprintf(vis_stdout, "since %s is true at this state", rFormulaText);
968      McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
969                             careSetArray); 
970    }
971    else {
972      int i;
973      fprintf(vis_stdout, "--Path on which %s is true till %s is true\n",
974                  lFormulaText, rFormulaText);
975      fprintf(vis_stdout, " --Counter example begins\n");
976      Mc_PrintPath(witnessArray,modelFsm,printInputs);
977      fprintf(vis_stdout, " --Counter example ends\n\n");
978      for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) {
979        mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
980     
981        if (debugLevel == McDbgLevelMax_c ||
982            (debugLevel == McDbgLevelInteractive_c &&
983             McQueryContinue(
984               "Continue debugging EU formula? (1-yes,0-no)\n"))) {
985          McFsmStateDebugFormula(options, lFormula, aState, modelFsm,
986                                 careSetArray);
987        }
988    }
989      McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
990                             careSetArray);
991    }
992    break;
993  default: 
994    fail("Should not be here - bad switch in debugging EU formula\n");
995  }
996  FREE(lFormulaText);
997  FREE(rFormulaText);
998}
999/**Function********************************************************************
1000
1001  Synopsis [Debug a path for EG type formula.]
1002
1003  SideEffects []
1004
1005******************************************************************************/
1006static void
1007FsmPathDebugEGFormula(
1008  McOptions_t *options,
1009  Ctlp_Formula_t *ctlFormula,
1010  Fsm_Fsm_t *modelFsm,
1011  McPath_t *witnessPath,
1012  array_t *careSetArray)
1013{
1014  mdd_t *firstState;
1015  char *firstStateName;
1016  array_t *witnessArray;
1017  char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
1018  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1019  array_t *stemArray = McPathReadStemArray( witnessPath );
1020  array_t *cycleArray = McPathReadCycleArray( witnessPath );
1021  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
1022  char *lFormulaText = Ctlp_FormulaConvertToString( lFormula );
1023  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
1024  boolean printInputs = McOptionsReadPrintInputs( options );
1025
1026  witnessArray = McCreateMergedPath( stemArray, cycleArray );
1027  firstState = array_fetch( mdd_t *, witnessArray, 0 );
1028  firstStateName = Mc_MintermToString(firstState, PSVars,Fsm_FsmReadNetwork(modelFsm));
1029 
1030  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1031    fprintf(vis_stdout, "--State\n%spasses EG formula\n\n",
1032            firstStateName); 
1033  else
1034    fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
1035            ctlFormulaText );
1036 
1037  FREE(firstStateName);
1038  FREE(ctlFormulaText);
1039
1040  switch ( debugLevel ) {
1041  case McDbgLevelMin_c:
1042  case McDbgLevelMinVerbose_c: {
1043    McPath_t *normalPath = McPathNormalize( witnessPath );
1044    array_t *stem = McPathReadStemArray( normalPath );
1045    array_t *cycle = McPathReadCycleArray( normalPath );
1046
1047    if(debugLevel != McDbgLevelMin_c)
1048      fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n",
1049              lFormulaText);
1050   
1051    FREE( lFormulaText );
1052    fprintf(vis_stdout, " --Counter example begins\n");
1053    (void) fprintf( vis_stdout, "--Fair path stem:\n");
1054    Mc_PrintPath( stem, modelFsm, printInputs );
1055   
1056    (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1057    Mc_PrintPath( cycle, modelFsm, printInputs );
1058    fprintf(vis_stdout, "\n");
1059    fprintf(vis_stdout, " --Counter example ends\n\n");
1060    McPathFree( normalPath );
1061    break;
1062  }
1063  case McDbgLevelMax_c:
1064  case McDbgLevelInteractive_c: {
1065    McPath_t *normalPath = McPathNormalize( witnessPath );
1066    array_t *stem = McPathReadStemArray( normalPath );
1067    array_t *cycle = McPathReadCycleArray( normalPath );
1068    int i;
1069    fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n",
1070              lFormulaText);
1071    fprintf(vis_stdout, " --Counter example begins\n");
1072    (void) fprintf( vis_stdout, "--Fair path stem:\n");
1073    Mc_PrintPath( stem, modelFsm, printInputs );
1074    (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1075    Mc_PrintPath( cycle, modelFsm, printInputs );
1076    fprintf(vis_stdout, " --Counter example ends\n\n");
1077    for( i=0 ; i < ( array_n( witnessArray )-1  ); i++ ) {
1078      mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
1079   
1080      if (debugLevel == McDbgLevelMax_c ||
1081          (debugLevel == McDbgLevelInteractive_c &&
1082           McQueryContinue(
1083             "--Continue debugging EG formula? (1-yes,0-no)\n"))) {
1084        McFsmStateDebugFormula(options, lFormula, aState, modelFsm,
1085                               careSetArray);
1086      }
1087    }
1088    break;
1089  }
1090  default:
1091    fail("Bad switch in FsmPathDebugEGFormula\n");
1092  }
1093  McNormalizeBddPointer(witnessArray);
1094  mdd_array_free( witnessArray );
1095}
1096
1097/**Function********************************************************************
1098
1099  Synopsis    [Debug a EF  formula]
1100
1101  SideEffects []
1102
1103******************************************************************************/
1104static void
1105FsmPathDebugEFFormula(
1106  McOptions_t *options,
1107  Ctlp_Formula_t *ctlFormula,
1108  Fsm_Fsm_t *modelFsm,
1109  McPath_t *witnessPath,
1110  array_t *careSetArray)
1111{
1112  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
1113  char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
1114
1115  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1116  array_t *witnessArray = McPathReadStemArray( witnessPath );
1117
1118  mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
1119  mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray );
1120  char *firstStateName = Mc_MintermToString(firstState, PSVars,
1121                                        Fsm_FsmReadNetwork(modelFsm));
1122
1123  Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula );
1124  Ctlp_Formula_t *rOriginalFormula = Ctlp_FormulaReadOriginalFormula(rFormula);
1125  char *rOriginalFormulaText = Ctlp_FormulaConvertToString( rOriginalFormula );
1126  char *rFormulaText = Ctlp_FormulaConvertToString( rFormula );
1127  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
1128  boolean printInputs = McOptionsReadPrintInputs( options );
1129
1130  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1131    fprintf(vis_stdout, "--State\n%spasses EF formula\n\n",
1132            firstStateName); 
1133  else
1134    fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
1135          originalFormulaText );
1136 
1137  FREE(firstStateName);
1138  FREE(originalFormulaText);
1139
1140  switch ( debugLevel ) {
1141  case McDbgLevelMin_c:
1142  case McDbgLevelMinVerbose_c:
1143    if ( array_n(witnessArray ) == 1 ) {
1144      if( debugLevel !=  McDbgLevelMin_c)
1145        fprintf(vis_stdout, "since %s is true at this state\n",
1146                rOriginalFormulaText);
1147     
1148      FREE( rOriginalFormulaText );
1149      McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
1150                             careSetArray);
1151    }
1152    else {
1153      if( debugLevel !=  McDbgLevelMin_c)
1154        fprintf(vis_stdout,
1155                "--Witness is a path to a state where %s is finally true\n",
1156                rOriginalFormulaText);
1157      (void) fprintf( vis_stdout, "\n--Fair path stem:\n");
1158      FREE( rOriginalFormulaText );
1159      fprintf(vis_stdout, " --Counter example begins\n");
1160      Mc_PrintPath( witnessArray, modelFsm, printInputs );
1161      fprintf(vis_stdout, " --Counter example ends\n\n");
1162    }
1163    break;
1164  case McDbgLevelMax_c:
1165  case McDbgLevelInteractive_c:
1166    if ( array_n(witnessArray ) == 1 ) {
1167      McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
1168                             careSetArray);
1169    }
1170    else
1171      {
1172        fprintf(vis_stdout,
1173                "--Witness is a path to a state where %s is finally true\n",
1174                rOriginalFormulaText);
1175        fprintf(vis_stdout, " --Counter example begins\n");
1176      Mc_PrintPath( witnessArray, modelFsm, printInputs);
1177      fprintf(vis_stdout, " --Counter example ends\n\n");
1178      if (debugLevel == McDbgLevelMax_c ||
1179          (debugLevel == McDbgLevelInteractive_c &&
1180           McQueryContinue(
1181             "--Continue debugging EF formula? (1-yes,0-no)\n")))
1182        {
1183        McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
1184                               careSetArray);
1185        }
1186      }
1187    break;
1188  default:
1189    fail("bad switch in debugging EF\n");
1190  }
1191  FREE(rFormulaText);
1192}
1193
1194/**Function********************************************************************
1195
1196  Synopsis    [Debug a AX formula]
1197
1198  SideEffects []
1199
1200******************************************************************************/
1201static void
1202FsmPathDebugAXFormula(
1203  McOptions_t *options,
1204  Ctlp_Formula_t *ctlFormula,
1205  Fsm_Fsm_t *modelFsm,
1206  McPath_t *counterExamplePath,
1207  array_t *careSetArray)
1208{
1209  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
1210  char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
1211  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
1212  Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
1213  Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula );
1214
1215  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1216  array_t *witnessArray = McPathReadStemArray( counterExamplePath );
1217  mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
1218  mdd_t *lastState = array_fetch( mdd_t *, witnessArray, 1 );
1219  char *firstStateName = Mc_MintermToString(firstState, PSVars,
1220                                            Fsm_FsmReadNetwork(modelFsm));
1221  boolean printInputs = McOptionsReadPrintInputs( options );
1222
1223 
1224  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1225    fprintf(vis_stdout, "--State\n%sfails AX formula\n\n",
1226            firstStateName); 
1227  else
1228      fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
1229          originalFormulaText );
1230
1231  FREE(firstStateName);
1232  FREE(originalFormulaText);
1233
1234  switch ( McOptionsReadDbgLevel( options ) ) {
1235  case McDbgLevelMin_c:
1236  case McDbgLevelMinVerbose_c:
1237  case McDbgLevelMax_c:
1238    fprintf(vis_stdout, " --Counter example begins\n"); 
1239    Mc_PrintPath( witnessArray, modelFsm, printInputs );
1240    fprintf(vis_stdout, " --Counter example ends\n\n");
1241    fprintf(vis_stdout, "\n");
1242    McFsmStateDebugFormula(options, lllFormula, lastState, modelFsm,
1243                           careSetArray);
1244    break;
1245  case McDbgLevelInteractive_c:
1246    fprintf(vis_stdout, " --Counter example begins\n");
1247    Mc_PrintPath( witnessArray, modelFsm, printInputs );
1248    fprintf(vis_stdout, " --Counter example ends\n\n");
1249    if ( McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n") ) {
1250      McFsmStateDebugFormula(options, lllFormula, lastState, modelFsm,
1251                             careSetArray);
1252    }
1253    break;
1254  default: 
1255    fail("Bad switch in FsmPathDebugAXFormula\n");
1256  }
1257}
1258
1259/**Function********************************************************************
1260
1261  Synopsis    [Debug a AF formula]
1262
1263  SideEffects []
1264
1265******************************************************************************/
1266static void
1267FsmPathDebugAFFormula(
1268  McOptions_t *options,
1269  Ctlp_Formula_t *ctlFormula,
1270  Fsm_Fsm_t *modelFsm,
1271  McPath_t *counterExamplePath,
1272  array_t *careSetArray)
1273{
1274  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
1275  char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
1276  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
1277  Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
1278  Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula );
1279  Ctlp_Formula_t *lllOriginalFormula = Ctlp_FormulaReadOriginalFormula(
1280                                        lllFormula);
1281  char *lllOriginalFormulaText = Ctlp_FormulaConvertToString(
1282                                        lllOriginalFormula);
1283
1284  mdd_t *firstState;
1285  array_t *witnessArray;
1286  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1287  array_t *stemArray = McPathReadStemArray( counterExamplePath );
1288  array_t *cycleArray = McPathReadCycleArray( counterExamplePath );
1289  char *firstStateName;
1290  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
1291  boolean printInputs = McOptionsReadPrintInputs( options );
1292
1293  witnessArray = McCreateMergedPath( stemArray, cycleArray );
1294  firstState = array_fetch( mdd_t *, witnessArray, 0 );
1295  firstStateName = Mc_MintermToString(firstState, PSVars,
1296                                        Fsm_FsmReadNetwork(modelFsm));
1297
1298  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1299    fprintf(vis_stdout, "--State\n%sfails AF formula\n\n",
1300            firstStateName); 
1301  else
1302    fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
1303            originalFormulaText );
1304  FREE(firstStateName);
1305  FREE(originalFormulaText);
1306
1307  switch ( debugLevel ) {
1308  case McDbgLevelMin_c:
1309  case McDbgLevelMinVerbose_c: {
1310    McPath_t *normalPath = McPathNormalize( counterExamplePath );
1311    array_t *stem = McPathReadStemArray( normalPath );
1312    array_t *cycle = McPathReadCycleArray( normalPath );
1313    if( debugLevel !=  McDbgLevelMin_c)
1314      fprintf(vis_stdout, "--A fair path on which %s is always false:\n",
1315              lllOriginalFormulaText );
1316   
1317    fprintf(vis_stdout, " --Counter example begins\n");
1318    (void) fprintf( vis_stdout, "--Fair path stem:\n");
1319    Mc_PrintPath( stem, modelFsm, printInputs );
1320   
1321    (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1322    Mc_PrintPath( cycle, modelFsm, printInputs );
1323    fprintf(vis_stdout, "\n");
1324    fprintf(vis_stdout, " --Counter example ends\n\n");
1325    McPathFree( normalPath );
1326    break;
1327  }
1328  case McDbgLevelMax_c:
1329  case McDbgLevelInteractive_c: {
1330    int i;
1331    McPath_t *normalPath = McPathNormalize( counterExamplePath );
1332    array_t *stem = McPathReadStemArray( normalPath );
1333    array_t *cycle = McPathReadCycleArray( normalPath );
1334    fprintf(vis_stdout, "--A fair path on which %s is always false:\n",
1335              lllOriginalFormulaText ); 
1336    fprintf(vis_stdout, " --Counter example begins\n");
1337    (void) fprintf( vis_stdout, "--Fair path stem:\n");
1338    Mc_PrintPath( stem, modelFsm, printInputs );
1339   
1340    (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1341    Mc_PrintPath( cycle, modelFsm, printInputs );
1342    fprintf(vis_stdout, "\n");
1343    fprintf(vis_stdout, " --Counter example ends\n\n");
1344    McPathFree( normalPath );
1345    for( i=0 ; i < ( array_n( witnessArray )-1  ); i++ ) {
1346      mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
1347   
1348      if (debugLevel == McDbgLevelMax_c ||
1349          (debugLevel == McDbgLevelInteractive_c &&
1350           McQueryContinue(
1351             "--Continue debugging AF formula? (1-yes,0-no)\n"))) {
1352        McFsmStateDebugFormula(options, lllFormula, aState, modelFsm,
1353                               careSetArray);
1354      }
1355    }
1356
1357    break;
1358  }
1359  default: {
1360    fail("Bad case in switch for debugging AF formula\n");
1361  }
1362  }
1363  McNormalizeBddPointer(witnessArray);
1364  mdd_array_free( witnessArray );
1365  FREE(lllOriginalFormulaText);
1366}
1367
1368/**Function********************************************************************
1369
1370  Synopsis    [Debug an AG formula.]
1371 
1372  Description [Debugs an AG formula.  What it really wants is a formula of the
1373  form !EF! phi, that was converted from the formula AG phi, with all the
1374  converted pointers set as required: the top ! points to the original AG
1375  formula, and top node of phi points to the original phi.]
1376
1377  SideEffects []
1378
1379******************************************************************************/
1380static void
1381FsmPathDebugAGFormula(
1382  McOptions_t *options,
1383  Ctlp_Formula_t *ctlFormula,
1384  Fsm_Fsm_t *modelFsm,
1385  McPath_t *counterExamplePath,
1386  array_t *careSetArray)
1387{
1388  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
1389  char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
1390  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
1391  Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula );
1392  Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula );
1393  Ctlp_Formula_t *lrlOriginalFormula = Ctlp_FormulaReadOriginalFormula(
1394                                        lrlFormula);
1395  char *lrlOriginalFormulaText = Ctlp_FormulaConvertToString(
1396                                        lrlOriginalFormula);
1397
1398  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1399  array_t *witnessArray = McPathReadStemArray( counterExamplePath );
1400  mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
1401  mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray ));
1402  char *firstStateName = Mc_MintermToString(firstState, PSVars,
1403                                            Fsm_FsmReadNetwork(modelFsm));
1404  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
1405  boolean printInputs = McOptionsReadPrintInputs( options );
1406
1407  assert( Ctlp_FormulaReadType(ctlFormula) == Ctlp_NOT_c );
1408  assert( Ctlp_FormulaTestIsConverted(ctlFormula) );
1409  assert( Ctlp_FormulaReadType(originalFormula) == Ctlp_AG_c );
1410  assert( originalFormulaText != NIL(char) );
1411  assert( Ctlp_FormulaReadType(lFormula) == Ctlp_EU_c );
1412  assert( Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(lFormula)) ==
1413          Ctlp_TRUE_c );
1414  assert( Ctlp_FormulaReadType(lrFormula) == Ctlp_NOT_c  );
1415  assert( lrlOriginalFormula != NIL(Ctlp_Formula_t) );
1416 
1417  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1418    fprintf(vis_stdout, "--State\n%sfails AG formula\n\n",
1419            firstStateName); 
1420  else
1421    fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
1422            originalFormulaText );
1423  FREE(firstStateName);
1424  FREE(originalFormulaText);
1425
1426  switch ( debugLevel ) {
1427  case McDbgLevelMin_c:
1428  case McDbgLevelMinVerbose_c:{
1429    if ( array_n(witnessArray ) == 1 ) {
1430      if( debugLevel !=  McDbgLevelMin_c)
1431        fprintf(vis_stdout, "since %s is false at this state\n",
1432                lrlOriginalFormulaText );
1433      McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
1434                             careSetArray);
1435    }
1436    else {
1437      if( debugLevel !=  McDbgLevelMin_c)
1438        fprintf(vis_stdout,
1439                "--Counter example is a path to a state where %s is false\n",
1440                lrlOriginalFormulaText);
1441      fprintf(vis_stdout, " --Counter example begins\n");
1442      Mc_PrintPath(witnessArray, modelFsm, printInputs);
1443      fprintf(vis_stdout, " --Counter example ends\n\n");
1444      McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
1445                             careSetArray);
1446    }
1447    break;
1448  }
1449  case McDbgLevelMax_c:
1450  case McDbgLevelInteractive_c: {
1451    if ( array_n(witnessArray ) == 1 ) {
1452      if( debugLevel !=  McDbgLevelMin_c)
1453        fprintf(vis_stdout, "since %s is false at this state\n",
1454                lrlOriginalFormulaText );
1455      McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
1456                             careSetArray);
1457    }
1458    else {
1459      fprintf(vis_stdout,
1460                "--Counter example is a path to a state where %s is false\n",
1461                lrlOriginalFormulaText);
1462      fprintf(vis_stdout, " --Counter example begins\n");
1463      Mc_PrintPath( witnessArray, modelFsm, printInputs);
1464      fprintf(vis_stdout, " --Counter example ends\n\n");
1465      if (debugLevel == McDbgLevelMax_c ||
1466          (debugLevel == McDbgLevelInteractive_c &&
1467           McQueryContinue(
1468             "--Continue debugging AG formula? (1-yes,0-no)\n")))
1469        {
1470        McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
1471                               careSetArray);
1472        }
1473      }
1474    break;
1475  }
1476  default: {
1477    fail("bad switch in debugging AG\n");
1478  }
1479  }
1480  FREE(lrlOriginalFormulaText);
1481}
1482
1483/**Function********************************************************************
1484
1485  Synopsis    [Debug a AU formula]
1486
1487  SideEffects []
1488
1489******************************************************************************/
1490static void
1491FsmPathDebugAUFormula(
1492  McOptions_t *options,
1493  mdd_t *aState,
1494  Ctlp_Formula_t *ctlFormula,
1495  Fsm_Fsm_t *modelFsm,
1496  array_t *careSetArray)
1497{
1498  Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
1499  char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
1500  Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
1501  Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula );
1502  Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula );
1503  Ctlp_Formula_t *lrllFormula = Ctlp_FormulaReadLeftChild( lrlFormula );
1504  Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
1505  Ctlp_Formula_t *llrFormula = Ctlp_FormulaReadRightChild( llFormula );
1506  Ctlp_Formula_t *llrlFormula = Ctlp_FormulaReadLeftChild( llrFormula );
1507  Ctlp_Formula_t *llrllFormula = Ctlp_FormulaReadLeftChild( llrlFormula );
1508  Ctlp_Formula_t *fFormula = llrllFormula;
1509  Ctlp_Formula_t *gFormula = lrllFormula;
1510  Ctlp_Formula_t *fOriginalFormula = Ctlp_FormulaReadOriginalFormula(fFormula);
1511  Ctlp_Formula_t *gOriginalFormula = Ctlp_FormulaReadOriginalFormula(gFormula);
1512  char *fText = Ctlp_FormulaConvertToString( fOriginalFormula );
1513  char *gText = Ctlp_FormulaConvertToString( gOriginalFormula );
1514
1515  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
1516  char *firstStateName = Mc_MintermToString(aState, PSVars,
1517                                        Fsm_FsmReadNetwork(modelFsm));
1518  McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
1519  boolean printInputs = McOptionsReadPrintInputs( options );
1520
1521  if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
1522    fprintf(vis_stdout, "--State\n%sfails AU formula\n\n",
1523            firstStateName); 
1524  else
1525    fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
1526            originalFormulaText );
1527  FREE(firstStateName);
1528  FREE(originalFormulaText);
1529
1530  /* orginal formula is A(fUg) => converted is !((E[!g U (!f*!g)]) + (EG!g)) */
1531
1532  if ( McStateSatisfiesFormula( llFormula, aState ) ) {
1533    /*
1534     * the case E[!g U (!f*!g)] is true
1535     */
1536    McPath_t *counterExamplePath = DebugEU(llFormula, aState, modelFsm,
1537                                           careSetArray);
1538   
1539    array_t *stemArray = McPathReadStemArray( counterExamplePath );
1540    array_t *witnessArray = stemArray;
1541    mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
1542    mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray );
1543    char *firstStateName = Mc_MintermToString(firstState, PSVars,
1544                                Fsm_FsmReadNetwork(modelFsm));
1545
1546    switch ( debugLevel ) {
1547    case McDbgLevelMinVerbose_c: 
1548      fprintf(vis_stdout,
1549              "--Counter example is a fair path where %s is false until %s is also false\n",
1550              gText, fText);
1551    case McDbgLevelMin_c:
1552      fprintf(vis_stdout, " --Counter example begins\n");
1553      Mc_PrintPath(witnessArray, modelFsm, printInputs);
1554      fprintf(vis_stdout, " --Counter example ends\n\n");
1555      McFsmStateDebugFormula(options, llrFormula, lastState, modelFsm,
1556                             careSetArray);
1557      break;
1558       
1559    case McDbgLevelMax_c:
1560    case McDbgLevelInteractive_c: {
1561      if ( array_n(witnessArray ) == 1 ) {
1562        fprintf(vis_stdout,
1563                "--At state %s\nformula %s is false and\nformula %s is also false\n",
1564                firstStateName, fText, gText);
1565        if (debugLevel == McDbgLevelMax_c ||
1566            (debugLevel == McDbgLevelInteractive_c &&
1567             McQueryContinue(
1568               "Continue debugging AU formula? (1-yes,0-no)\n"))) {
1569          McFsmStateDebugFormula(options, fFormula, aState, modelFsm,
1570                                 careSetArray);
1571          McFsmStateDebugFormula(options, gFormula, aState, modelFsm,
1572                                 careSetArray);
1573        }
1574      }
1575      else {
1576        int i;
1577        fprintf(vis_stdout, " --Counter example begins\n");
1578        Mc_PrintPath(witnessArray,modelFsm,printInputs);
1579        fprintf(vis_stdout, " --Counter example ends\n\n");
1580        for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) {
1581          mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
1582         
1583          if (debugLevel == McDbgLevelMax_c ||
1584              (debugLevel == McDbgLevelInteractive_c &&
1585               McQueryContinue(
1586                 "Continue debugging AU formula? (1-yes,0-no)\n"))) {
1587            McFsmStateDebugFormula(options, gFormula, aState, modelFsm,
1588                                   careSetArray);
1589          }
1590        }
1591       
1592        if (debugLevel == McDbgLevelMax_c ||
1593            (debugLevel == McDbgLevelInteractive_c &&
1594             McQueryContinue(
1595               "Continue debugging AU formula? (1-yes,0-no)\n"))) {
1596          McFsmStateDebugFormula(options, fFormula, lastState, modelFsm,
1597                                 careSetArray);
1598          McFsmStateDebugFormula(options, gFormula, lastState, modelFsm,
1599                                 careSetArray);
1600        }
1601      }
1602      break;
1603    }
1604   
1605    default: {
1606      fail("Unknown case in debugging AU\n");
1607    }
1608    }/* case */
1609    McPathFree( counterExamplePath );
1610  }
1611  else {
1612    /*
1613     * must be the case that EG!g
1614     */
1615    McPath_t *counterExamplePath = DebugEG(lrFormula, aState, modelFsm,
1616                                           careSetArray, 
1617                                           options);
1618
1619    assert( McStateSatisfiesFormula( lrFormula, aState ) );
1620
1621    if( debugLevel !=  McDbgLevelMin_c)
1622      fprintf(vis_stdout,
1623              "--Counter example is a fair path where %s is always false\n",
1624              gText);
1625
1626    switch ( debugLevel ) {
1627    case McDbgLevelMin_c:
1628    case McDbgLevelMinVerbose_c:{
1629      McPath_t *normalPath = McPathNormalize( counterExamplePath );
1630      array_t *stem = McPathReadStemArray( normalPath );
1631      array_t *cycle = McPathReadCycleArray( normalPath );
1632     
1633      fprintf(vis_stdout, " --Counter example begins\n");
1634      (void) fprintf( vis_stdout, "--Fair path stem:\n");
1635      Mc_PrintPath( stem, modelFsm, printInputs );
1636     
1637      (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1638      Mc_PrintPath( cycle, modelFsm, printInputs );
1639      fprintf(vis_stdout, " --Counter example ends\n\n");
1640      McPathFree( normalPath );
1641      break;
1642    }
1643   
1644    case McDbgLevelMax_c:
1645    case McDbgLevelInteractive_c:
1646      {
1647    int i;
1648    array_t *stemArray = McPathReadStemArray( counterExamplePath );
1649    array_t *cycleArray = McPathReadCycleArray( counterExamplePath );
1650    array_t *witnessArray = McCreateMergedPath( stemArray, cycleArray );
1651    McPath_t *normalPath = McPathNormalize( counterExamplePath );
1652    array_t *stem = McPathReadStemArray( normalPath );
1653    array_t *cycle = McPathReadCycleArray( normalPath );
1654   
1655    fprintf(vis_stdout, " --Counter example begins\n");
1656    (void) fprintf( vis_stdout, "--Fair path stem:\n");
1657    Mc_PrintPath( stem, modelFsm, printInputs );
1658   
1659    (void) fprintf( vis_stdout, "--Fair path cycle:\n");
1660    Mc_PrintPath( cycle, modelFsm, printInputs );
1661    fprintf(vis_stdout, " --Counter example ends\n\n");
1662    McPathFree( normalPath );
1663    for( i=0 ; i < ( array_n( witnessArray )-1  ); i++ ) {
1664      mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
1665   
1666      if (debugLevel == McDbgLevelMax_c ||
1667          (debugLevel == McDbgLevelInteractive_c &&
1668           McQueryContinue(
1669             "--Continue debugging AU formula? (1-yes,0-no)\n"))) {
1670        McFsmStateDebugFormula(options, lrllFormula, aState, modelFsm,
1671                               careSetArray);
1672      }
1673    }
1674    break;
1675  }
1676
1677    default: {
1678      fail("Bad switch in debugging AU formula\n");
1679    }
1680    }/* case */
1681    McPathFree( counterExamplePath );
1682  }
1683 
1684  FREE( fText );
1685  FREE( gText );
1686}
Note: See TracBrowser for help on using the repository browser.