source: vis_dev/vis-2.3/src/abs/absEvaluate.c @ 23

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

vis2.3
File size: 32.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [absEvaluate.c]
4
5  PackageName [abs]
6
7  Synopsis [Evaluation procedures for the abstraction based mu-calculus model
8  checker.]
9
10  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
11
12  Copyright   [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "absInt.h"
19
20static char rcsid[] UNUSED = "$Id: absEvaluate.c,v 1.19 2002/09/19 05:25:00 fabio Exp $";
21
22
23/*---------------------------------------------------------------------------*/
24/* Macro declarations                                                        */
25/*---------------------------------------------------------------------------*/
26
27/*---------------------------------------------------------------------------*/
28/* Variable declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37static void EvaluateVariable(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
38static void EvaluateIdentifier(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
39static void EvaluateNot(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
40static void EvaluateAnd(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
41static void EvaluateFixedPoint(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
42static void EvaluatePreImage(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
43static mdd_t * OverApproximatePreImageWithSubFSM(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);
44static mdd_t * OverApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);
45static mdd_t * UnderApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);
46
47/**AutomaticEnd***************************************************************/
48
49
50/*---------------------------------------------------------------------------*/
51/* Definition of exported functions                                          */
52/*---------------------------------------------------------------------------*/
53
54
55/*---------------------------------------------------------------------------*/
56/* Definition of internal functions                                          */
57/*---------------------------------------------------------------------------*/
58
59/**Function********************************************************************
60
61  Synopsis [Procedure to evaluate a sub-formula]
62
63  Description [This procedure is simply a switch to call the apropriate
64  evaluation procedures depending on the type of formula]
65
66  SideEffects [EvaluateFixedPoint, EvaluateAnd, EvaluateNot, EvaluatePreImage,
67  EvaluateIdentifier, EvaluateVariable]
68
69******************************************************************************/
70void
71AbsSubFormulaVerify(
72  Abs_VerificationInfo_t *absInfo,
73  AbsVertexInfo_t *vertexPtr)
74{
75  AbsStats_t *stats;
76  mdd_manager *mddManager;
77  mdd_t *oldTmpCareSet = NIL(mdd_t);
78 
79  long verbosity;
80
81  stats = AbsVerificationInfoReadStats(absInfo);
82  mddManager = AbsVerificationInfoReadMddManager(absInfo);
83
84  /* If the current vertex has more than one parent, the temporary care set
85   * must be reset (because it depends on the path that led to this vertex */
86  if (lsLength(vertexPtr->parent) > 1) {
87    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
88    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
89  }
90
91  switch (AbsVertexReadType(vertexPtr)) {
92    case fixedPoint_c:
93      EvaluateFixedPoint(absInfo, vertexPtr);
94      AbsStatsReadEvalFixedPoint(stats)++;
95      break;
96    case and_c: 
97      EvaluateAnd(absInfo, vertexPtr);
98      AbsStatsReadEvalAnd(stats)++;
99      break;
100    case not_c:
101      EvaluateNot(absInfo, vertexPtr);
102      AbsStatsReadEvalNot(stats)++;
103      break;
104    case preImage_c:
105      EvaluatePreImage(absInfo, vertexPtr);
106      AbsStatsReadEvalPreImage(stats)++;
107      break;
108    case identifier_c:
109      EvaluateIdentifier(absInfo, vertexPtr);
110      AbsStatsReadEvalIdentifier(stats)++;
111      break;
112    case variable_c:
113      EvaluateVariable(absInfo, vertexPtr);
114      AbsStatsReadEvalVariable(stats)++;
115      break;
116    default: fail("Encountered unknown type of vertex\n");
117    }
118
119  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
120
121  /* Print the size of the care set */
122  if (verbosity & ABS_VB_CARESZ) {
123    (void) fprintf(vis_stdout, "ABS: Size of Care Set: ");
124    (void) fprintf(vis_stdout, "%d Nodes.\n", 
125                   mdd_size(AbsVerificationInfoReadCareSet(absInfo)));
126  }
127
128  /* Print the care set */
129  if (verbosity & ABS_VB_CARE) {
130    (void) fprintf(vis_stdout, "ABS: Care Set for Evaluation:\n");
131    AbsBddPrintMinterms(AbsVerificationInfoReadCareSet(absInfo));
132  }
133
134  /* Print the contents of the vertex */
135  if (verbosity & ABS_VB_VTXCNT) {
136    AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
137  }
138
139  if (lsLength(vertexPtr->parent) > 1) {
140    /* Restore the old temporary careset */
141    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
142    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
143  }
144
145} /* End of AbsSubFormulaVerify */
146
147/**Function********************************************************************
148
149  Synopsis [Traverse the operational graph and mark formulas for evaluation]
150
151  Description [This procedure receives two pointers and marks every formula in
152  between for later evaluation. The marking process is simply setting the field
153  served to 0]
154
155  SideEffects        []
156
157  SeeAlso            [AbsFixedPointIterate]
158
159******************************************************************************/
160void
161AbsFormulaScheduleEvaluation(
162  AbsVertexInfo_t *current,
163  AbsVertexInfo_t *limit)
164{
165  /* We reached the final case */
166  if (current == limit) {
167    return;
168  }
169  else {
170    AbsVertexInfo_t *parentPtr;
171    lsList          parentList;
172    lsGen           gen;
173
174    /* Set the re-evaluation flag for the current vertex */
175    AbsVertexSetServed(current, 0);
176
177    /* Recur over the parents */
178    parentList = AbsVertexReadParent(current);
179    lsForEachItem(parentList, gen, parentPtr) {
180      if (parentPtr != NIL(AbsVertexInfo_t)) {
181        AbsFormulaScheduleEvaluation(parentPtr, limit);
182      }
183    }
184  }
185
186  return;
187} /* End of AbsFormulaScheduleEvaluation */
188
189/**Function********************************************************************
190
191  Synopsis [Function to minimize the size of the BDD representing one iteration
192  of the fix-point]
193
194  Description [This function is simply to encapsulate the call to the minimize
195  procedure and have a simple place where to explore the different choices when
196  it comes to select upper and lower bounds for a function. In the case of
197  fix-point evaluation, there are several bounds that can be used to look for a
198  compact representation, this is the function in which that experimenting
199  should be included]
200
201  SideEffects        []
202
203  SeeAlso            [AbsFixedPointIterate]
204
205******************************************************************************/
206mdd_t *
207AbsComputeOptimalIterate(
208  Abs_VerificationInfo_t *absInfo,
209  AbsVertexInfo_t *vertexPtr,
210  mdd_t *lowerIterate,
211  mdd_t *upperIterate)
212{
213  mdd_t *tmp;
214  mdd_t *result;
215
216  if (AbsOptionsReadMinimizeIterate(AbsVerificationInfoReadOptions(absInfo))
217      && AbsVertexReadUseExtraCareSet(vertexPtr)) {
218
219    /*
220     * For this computation we have three ingredients and a handfull of
221     * choices. The ingredients are the sets newIterate, iterate and
222     * careSet. The goal is to compute an interval delimited by two boolean
223     * functions and then call the function bdd_between to try to obtain
224     * the best bdd in size inside that interval. To compute the extremes
225     * of the interval there are several choices. For example, the care set
226     * can be used in the lower bound of the interval or in both
227     * bounds. The bigger the interval the more choice the function
228     * bdd_between has to minimize, however, this does not turn into a
229     * better result.
230     *
231     * Current Choice: [newIterate * iterate', newIterate]
232     */
233    tmp = mdd_and(lowerIterate, upperIterate, 0, 1);
234    result = bdd_between(tmp, upperIterate);
235   
236    /* This line for debugging purposes, should be removed
237    (void) fprintf(vis_stdout,
238                   "newIterate : %d, Diff : %d, result %d\n",
239                   mdd_size(upperIterate), mdd_size(tmp),
240                   mdd_size(result)); */
241   
242    mdd_free(tmp);
243  }
244  else {
245    result = mdd_dup(upperIterate);
246  }
247
248  return result;
249} /* End of AbsComputeOptimalIterate */
250
251/**Function********************************************************************
252
253  Synopsis [Function to compute the iteration in a fix-point computation]
254
255  SideEffects        []
256
257  SeeAlso            [AbsSubFormulaVerify]
258
259******************************************************************************/
260boolean
261AbsFixedPointIterate(
262  Abs_VerificationInfo_t *absInfo,
263  AbsVertexInfo_t *vertexPtr,
264  int iterateIndex)
265{
266  AbsVertexInfo_t *subFormula;
267  boolean         keepIterating;
268  boolean         globalApprox;
269  int             stepCount;
270  long            verbosity;
271  mdd_t           *iterate;
272  mdd_t           *newIterate;
273  mdd_t           *careSet;
274   
275  /* Do not allow to iterate from the middle of a fixed point computation */
276  assert(iterateIndex == array_n(AbsVertexReadRings(vertexPtr)) - 1);
277
278  careSet = AbsVerificationInfoReadCareSet(absInfo);
279
280  /* Check if the set of iterates has already converged */
281  if (array_n(AbsVertexReadRings(vertexPtr)) > 1) {
282    mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateIndex);
283    mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
284    if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
285      return FALSE;
286    }
287    iterate = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
288  }
289  else {
290    iterate = AbsVertexFetchRing(vertexPtr, iterateIndex);
291  }
292  newIterate = AbsVertexFetchRing(vertexPtr, iterateIndex);
293
294  /* Variable initialization */
295  keepIterating = TRUE;
296  stepCount = iterateIndex;
297  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
298  subFormula = AbsVertexReadLeftKid(vertexPtr);
299  globalApprox = AbsVertexFetchSubApprox(vertexPtr, iterateIndex);
300 
301  /* Main loop for the fixed point computation */
302  while (keepIterating) {
303    mdd_t *best;
304   
305    /*
306     * Given newIterate, iterate and CareSet, if the use of extra care set is
307     * enabled, choose the best candidate as the value of the iterate.
308     */
309    best = AbsComputeOptimalIterate(absInfo, vertexPtr, iterate, newIterate);
310
311    /* Print the iterates */
312    if ((verbosity & ABS_VB_PITER) || (verbosity & ABS_VB_ITSIZ)) {
313      (void) fprintf(vis_stdout, "ABS: New Iterate: ");
314      if (verbosity & ABS_VB_ITSIZ) {
315        (void) fprintf(vis_stdout, "%d -> %d\n", mdd_size(newIterate),
316                       mdd_size(best));
317      }
318      else {
319        (void) fprintf(vis_stdout, "\n");
320      }
321      if (verbosity & ABS_VB_PITER) {
322        AbsBddPrintMinterms(newIterate);
323      }
324    }
325   
326    /* Store the value of the variable */
327    AbsVertexSetSat(AbsVertexReadFpVar(vertexPtr), best);
328   
329    /* Mark the proper sub-formulas for re-evaluation */
330    AbsFormulaScheduleEvaluation(AbsVertexReadFpVar(vertexPtr), vertexPtr);
331   
332    /* Evaluate the sub-formula */
333    AbsSubFormulaVerify(absInfo, subFormula);
334    mdd_free(best);
335    iterate = newIterate;
336   
337    /*
338     * Compute the new iterate. Due to the fact that don't cares are being
339     * used, it might be possible that the new iterate does not contain the
340     * previous one, in that case the or is taken
341     */
342    newIterate = mdd_or(iterate, AbsVertexReadSat(subFormula), 1, 1);
343   
344    assert(AbsMddLEqualModCareSet(iterate, newIterate, careSet));
345
346    /* Set the rings and the approximation flags */
347    AbsVertexInsertRing(vertexPtr, newIterate);
348    AbsVertexInsertRingApprox(vertexPtr, FALSE);
349    globalApprox = globalApprox || AbsVertexReadGlobalApprox(subFormula);
350    AbsVertexInsertSubApprox(vertexPtr, globalApprox);
351
352    keepIterating = !AbsMddEqualModCareSet(newIterate, iterate, careSet);
353   
354    stepCount++;
355  } /* End of main while loop */
356
357  return TRUE;
358} /* End of AbsFixedPointIterate */
359
360/*---------------------------------------------------------------------------*/
361/* Definition of static functions                                            */
362/*---------------------------------------------------------------------------*/
363
364/**Function********************************************************************
365
366  Synopsis [Function to evaluate a sub-formula representing the variable of a
367  fix-point computation]
368
369  SideEffects        []
370
371  SeeAlso            [AbsSubFormulaVerify]
372
373******************************************************************************/
374static void
375EvaluateVariable(
376  Abs_VerificationInfo_t *absInfo,
377  AbsVertexInfo_t *vertexPtr)
378{
379  /* Increase the number of times the result has been used */
380  AbsVertexReadServed(vertexPtr)++;
381
382  return;
383} /* End of EvaluateVariable */
384
385/**Function********************************************************************
386
387  Synopsis           [Evaluate a vertex storing an Id]
388
389  Description [This vertex represents a subformula with an atomic
390  proposition. No approximation is done on its evaluation. The assumption is
391  that this operation does not cause blow up in the memory requirements. This
392  situation might change though]
393
394  SideEffects        []
395
396  SeeAlso            [AbsSubFormulaVerify]
397
398******************************************************************************/
399static void
400EvaluateIdentifier(
401  Abs_VerificationInfo_t *absInfo,
402  AbsVertexInfo_t *vertexPtr)
403{
404  if (AbsVertexReadServed(vertexPtr) == 0) {
405    Ntk_Node_t     *node;
406    Var_Variable_t *nodeVar;
407    graph_t        *partition;
408    vertex_t       *partitionVertex;
409    Mvf_Function_t *nodeFunction;
410    mdd_t          *result;
411    char           *nodeNameString;
412    char           *nodeValueString;
413    int            nodeValue;
414
415    /* Clean up of previous result */
416    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
417      mdd_free(AbsVertexReadSat(vertexPtr));
418      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
419    }
420
421    /* Read the partition */
422    partition = AbsVerificationInfoReadPartition(absInfo);
423   
424    assert(partition != NIL(graph_t));
425   
426    /* Obtain the name and the value being used */
427    nodeNameString = AbsVertexReadName(vertexPtr);
428    nodeValueString = AbsVertexReadValue(vertexPtr);
429   
430    /* Obtain the the node in the network and the variable attached to it */
431    node = Ntk_NetworkFindNodeByName(AbsVerificationInfoReadNetwork(absInfo),
432                                     nodeNameString);
433    nodeVar = Ntk_NodeReadVariable(node);
434   
435    /* Obtain the real value of the multi-valued vairable */
436    if (Var_VariableTestIsSymbolic(nodeVar)) {
437      nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar,
438                                                         nodeValueString);
439    }
440    else {
441      nodeValue = atoi(nodeValueString);
442    }
443   
444    /* Read the partition, find the vertex in the partition and its function */
445    partitionVertex = Part_PartitionFindVertexByName(partition, 
446                                                     nodeNameString);
447   
448    /* If the vertex is not represented in the partition must be built */
449    if (partitionVertex == NIL(vertex_t)) { 
450      Ntk_Node_t *tmpNode;
451      lsGen      tmpGen;
452      array_t    *mvfArray;
453      array_t    *tmpRoots;
454      st_table   *tmpLeaves;
455     
456      /* Initialize the variables */
457      tmpRoots = array_alloc(Ntk_Node_t *, 0);
458      tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
459     
460      /* Insert the parameters in the array and table */
461      array_insert_last(Ntk_Node_t *, tmpRoots, node);
462      Ntk_NetworkForEachCombInput(AbsVerificationInfoReadNetwork(absInfo),
463                                  tmpGen, tmpNode) {
464        st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
465      }
466     
467      /* Effectively build the mdd for the given vertex */
468      mvfArray =  Ntm_NetworkBuildMvfs(AbsVerificationInfoReadNetwork(absInfo),
469                                       tmpRoots, tmpLeaves, NIL(mdd_t));
470      nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0);
471      array_free(tmpRoots);
472      st_free_table(tmpLeaves);
473      array_free(mvfArray);
474     
475      /* Store the result in the vertex */
476      result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
477      AbsVertexSetSat(vertexPtr, mdd_dup(result));
478      Mvf_FunctionFree(nodeFunction);
479    }
480    else {
481      /* Store the result in the vertex */
482      nodeFunction = Part_VertexReadFunction(partitionVertex);
483      result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
484      AbsVertexSetSat(vertexPtr, mdd_dup(result));
485    }
486   
487    /* Set the approximation flags */
488    AbsVertexSetLocalApprox(vertexPtr, FALSE);
489    AbsVertexSetGlobalApprox(vertexPtr, FALSE);
490  }
491
492  /* Increase the number of times the result has been used */
493  AbsVertexReadServed(vertexPtr)++;
494 
495  return;
496} /* End of EvaluateIdentifier */
497
498/**Function********************************************************************
499
500  Synopsis           [Evaluate a negation vertex]
501
502  SideEffects        []
503
504  SeeAlso            [AbsSubFormulaVerify]
505
506******************************************************************************/
507static void
508EvaluateNot(
509  Abs_VerificationInfo_t *absInfo,
510  AbsVertexInfo_t *vertexPtr)
511{
512  if (AbsVertexReadServed(vertexPtr) == 0) {
513    AbsVertexInfo_t *subFormula;
514   
515    /* Clean up of previous result */
516    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
517      mdd_free(AbsVertexReadSat(vertexPtr));
518      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
519    }
520
521    /* Recursively evaluate the sub-formula */
522    subFormula = AbsVertexReadLeftKid(vertexPtr);
523    AbsSubFormulaVerify(absInfo, subFormula);
524
525    /* Negate the result of the sub-formula */
526    AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));
527
528    /* Set the approximation flags */
529    AbsVertexSetLocalApprox(vertexPtr, FALSE);
530    AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));
531  }
532
533  /* Increase the number of times the result has been used */
534  AbsVertexReadServed(vertexPtr)++;
535
536  return;
537} /* End of EvaluateNot */
538
539/**Function********************************************************************
540
541  Synopsis           [Evaluate a conjunction vertex]
542
543  SideEffects        []
544
545  SeeAlso            [AbsSubFormulaVerify]
546
547******************************************************************************/
548static void
549EvaluateAnd(
550  Abs_VerificationInfo_t *absInfo,
551  AbsVertexInfo_t *vertexPtr)
552{
553  if (AbsVertexReadServed(vertexPtr) == 0) {
554    AbsVertexInfo_t *firstFormula;
555    AbsVertexInfo_t *secondFormula;
556    mdd_t *oldTmpCareSet;
557
558    /* Clean up of previous result */
559    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
560      mdd_free(AbsVertexReadSat(vertexPtr));
561      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
562    }
563
564    /* Obtain the subformulas to evaluate */
565    firstFormula = AbsVertexReadLeftKid(vertexPtr);
566    secondFormula = AbsVertexReadRightKid(vertexPtr);
567 
568    /* Recursively evaluate the first sub-formula */
569    AbsSubFormulaVerify(absInfo, firstFormula);
570
571    /* Store the temporary careset and set the new one */
572    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
573    AbsVerificationInfoSetTmpCareSet(absInfo, 
574                                     mdd_and(oldTmpCareSet, 
575                                             AbsVertexReadSat(firstFormula), 
576                                             1,1));
577
578    /* Recursively evaluate the second sub-formula */
579    AbsSubFormulaVerify(absInfo, secondFormula);
580
581    /* Restore the temporary careset */
582    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
583    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
584   
585    /* Compute result, so far no approximation is required */
586    AbsVertexSetSat(vertexPtr, mdd_and(AbsVertexReadSat(firstFormula),
587                                       AbsVertexReadSat(secondFormula), 
588                                       1, 1));
589
590    /* Set the approximation flags */
591    AbsVertexSetLocalApprox(vertexPtr, FALSE);
592    AbsVertexSetGlobalApprox(vertexPtr, 
593                             AbsVertexReadGlobalApprox(firstFormula) || 
594                             AbsVertexReadGlobalApprox(secondFormula));
595  }
596
597  /* Increase the number of times the result has been used */
598  AbsVertexReadServed(vertexPtr)++;
599
600  return;
601} /* End of EvaluateAnd */
602
603/**Function********************************************************************
604
605  Synopsis           [Evaluate a fix-point vertex]
606
607  SideEffects        []
608
609  SeeAlso            [AbsSubFormulaVerify]
610
611******************************************************************************/
612static void
613EvaluateFixedPoint(
614  Abs_VerificationInfo_t *absInfo,
615  AbsVertexInfo_t *vertexPtr)
616{
617  if (AbsVertexReadServed(vertexPtr) == 0) {
618    mdd_manager *mddManager;
619    mdd_t       *oldTmpCareSet;
620    mdd_t       *newTmpCareSet;
621
622    if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) {
623      mdd_t *ringUnit;
624      int i;
625
626      arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), i, ringUnit) {
627        mdd_free(ringUnit);
628      }
629      array_free(AbsVertexReadRings(vertexPtr));
630      array_free(AbsVertexReadRingApprox(vertexPtr));
631      array_free(AbsVertexReadSubApprox(vertexPtr));
632      mdd_free(AbsVertexReadSat(vertexPtr));
633    }
634
635    /* Re-allocation of the temporary structures */
636    AbsVertexSetRings(vertexPtr, array_alloc(mdd_t *, 0));
637    AbsVertexSetRingApprox(vertexPtr, array_alloc(boolean, 0));
638    AbsVertexSetSubApprox(vertexPtr, array_alloc(boolean, 0));
639   
640    /* Initial values of the fixed point */
641    mddManager = AbsVerificationInfoReadMddManager(absInfo);
642    AbsVertexInsertRing(vertexPtr, mdd_zero(mddManager));
643    AbsVertexInsertRingApprox(vertexPtr, FALSE);
644    AbsVertexInsertSubApprox(vertexPtr, FALSE);
645
646    /* Reset the temporary careset to the mdd one */
647    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
648    newTmpCareSet = mdd_one(mddManager);
649    AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);
650
651    /* Effectively iterate the body */
652    AbsFixedPointIterate(absInfo, vertexPtr, 0);
653
654    /* Restore the old temporary careset */
655    mdd_free(newTmpCareSet);
656    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
657   
658    /* Set the last result as the set sat*/
659    AbsVertexSetSat(vertexPtr, 
660                    mdd_dup(AbsVertexFetchRing(vertexPtr,
661                                        array_n(AbsVertexReadRings(vertexPtr))
662                                               - 1)));
663
664    /* Set the approximation flags */
665    AbsVertexSetLocalApprox(vertexPtr, FALSE);
666    AbsVertexSetGlobalApprox(vertexPtr, 
667                             AbsVertexFetchSubApprox(vertexPtr,
668                               array_n(AbsVertexReadSubApprox(vertexPtr)) - 1));
669  }
670
671  /* Increase the number of times the result has been used */
672  AbsVertexReadServed(vertexPtr)++;
673
674  return;
675}
676
677 /* End of EvaluateFixedPoint */
678
679/**Function********************************************************************
680
681  Synopsis           [Evaluate a pre-image vertex]
682
683  SideEffects        []
684
685  SeeAlso            [AbsSubFormulaVerify]
686
687******************************************************************************/
688static void
689EvaluatePreImage(
690  Abs_VerificationInfo_t *absInfo,
691  AbsVertexInfo_t *vertexPtr)
692{
693  AbsOptions_t *options;
694  AbsStats_t   *stats;
695  long         verbosity;
696
697  /* Variable initialization */
698  options = AbsVerificationInfoReadOptions(absInfo);
699  verbosity = AbsOptionsReadVerbosity(options);
700  stats = AbsVerificationInfoReadStats(absInfo);
701
702  if (AbsVertexReadServed(vertexPtr) == 0) {
703    AbsVertexInfo_t *subFormula;
704    mdd_manager     *mddManager;
705    mdd_t           *result;
706    mdd_t           *careSet;
707    mdd_t           *oldTmpCareSet;
708    mdd_t           *minimizedSet;
709
710    /* Variable initialization */
711    mddManager = AbsVerificationInfoReadMddManager(absInfo);
712    subFormula = AbsVertexReadLeftKid(vertexPtr);
713
714    /*
715     * Compute the care set as the conjunction of the given one and the
716     * temporary one
717     */
718    careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
719                      AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);
720
721    /* Clean up */
722    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
723      mdd_free(AbsVertexReadSat(vertexPtr));
724      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
725    }
726   
727    /* Reset the temporary careset to the mdd one */
728    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
729    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
730
731    /* Evaluate the sub-formula */
732    AbsSubFormulaVerify(absInfo, subFormula);
733
734    /* Restore the old temporary careset */
735    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
736    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
737   
738    /* Check for trivial cases */
739    if (mdd_is_tautology(AbsVertexReadSat(subFormula), 0) ||
740        mdd_is_tautology(AbsVertexReadSat(subFormula), 1)) {
741      AbsVertexSetSat(vertexPtr, mdd_dup(AbsVertexReadSat(subFormula)));
742      AbsVertexSetLocalApprox(vertexPtr, FALSE);
743      AbsVertexSetGlobalApprox(vertexPtr, 
744                               AbsVertexReadGlobalApprox(subFormula));
745      mdd_free(careSet);
746      return;
747    }
748
749    /* if (AbsOptionsReadMinimizeIterate(options)){ */
750    if (FALSE){
751      minimizedSet = bdd_minimize(AbsVertexReadSat(subFormula),
752                                  AbsVerificationInfoReadCareSet(absInfo));
753    }
754    else {
755      minimizedSet = mdd_dup(AbsVertexReadSat(subFormula));
756    }
757     
758    /* Look up in the cache if the result has been previously computed */
759    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
760      mdd_t   *unit;
761      boolean localFlag;
762      boolean exactness;
763     
764      exactness = AbsOptionsReadExact(options);
765      if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
766                             minimizedSet, careSet, !exactness,
767                             &unit, &localFlag)) {
768
769        /* Set the sat */
770        AbsVertexSetSat(vertexPtr, mdd_dup(unit));
771
772        /* Set the approximation flags */
773        AbsVertexSetLocalApprox(vertexPtr, localFlag & !exactness);
774        AbsVertexSetGlobalApprox(vertexPtr, 
775                                 AbsVertexReadGlobalApprox(subFormula) || 
776                                 AbsVertexReadLocalApprox(vertexPtr));
777        /* Increase the number of times the result has been used */
778        AbsVertexReadServed(vertexPtr)++;
779       
780        mdd_free(careSet);
781        mdd_free(minimizedSet);
782        return;
783      }
784    }
785    else {
786      /* Initialize the cache */
787      AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
788    }
789
790    /* Effectively compute preImage */
791    if (!AbsOptionsReadExact(options)) {
792      if (AbsVertexReadPolarity(vertexPtr)) {
793        if (AbsOptionsReadPartApprox(options)) {
794          result = OverApproximatePreImageWithSubFSM(absInfo, minimizedSet, 
795                                                     minimizedSet, careSet);
796        }
797        else {
798          result = OverApproximatePreImageWithBddSubsetting(absInfo, 
799                                                            minimizedSet, 
800                                                            minimizedSet, 
801                                                            careSet);
802        }
803        AbsVertexSetLocalApprox(vertexPtr, TRUE);
804      }
805      else {
806        result = UnderApproximatePreImageWithBddSubsetting(absInfo, 
807                                                           minimizedSet, 
808                                                           minimizedSet,
809                                                           careSet);
810        AbsVertexSetLocalApprox(vertexPtr, TRUE);
811      }
812      AbsStatsReadApproxPreImage(AbsVerificationInfoReadStats(absInfo))++;
813    }
814    else {
815      Fsm_Fsm_t       *system;
816      Img_ImageInfo_t *imageInfo;
817      long            cpuTime;
818
819      system = AbsVerificationInfoReadFsm(absInfo);
820      imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
821      cpuTime = util_cpu_time();
822      result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, minimizedSet,
823                                                     minimizedSet,careSet);
824      AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;
825
826      AbsStatsReadExactPreImage(stats)++;
827      AbsVertexSetLocalApprox(vertexPtr, FALSE);
828    }
829    AbsVertexSetSat(vertexPtr, result);
830
831    /* Set the value in the cache */
832    AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
833                       minimizedSet, AbsVertexReadSat(vertexPtr), careSet,
834                       AbsVertexReadLocalApprox(vertexPtr), FALSE);
835    AbsStatsReadPreImageCacheEntries(stats)++;
836    mdd_free(minimizedSet);
837
838    /* Set the approximation flags */
839    AbsVertexSetGlobalApprox(vertexPtr, 
840                             AbsVertexReadGlobalApprox(subFormula) || 
841                             AbsVertexReadLocalApprox(vertexPtr));
842
843    /* Print the number of states in the on set of Sat */
844    if (verbosity & ABS_VB_TSAT) {
845      Fsm_Fsm_t *globalSystem;
846      array_t *domainVars;
847      mdd_t *intersection;
848     
849      intersection = mdd_and(AbsVertexReadSat(vertexPtr), careSet, 1, 1);
850     
851      globalSystem = AbsVerificationInfoReadFsm(absInfo);
852      domainVars = Fsm_FsmReadPresentStateVars(globalSystem);
853      (void) fprintf(vis_stdout, "ABS: %.0f States satisfy the EX formula.\n",
854                     mdd_count_onset(AbsVerificationInfoReadMddManager(absInfo),
855                                     intersection, domainVars));
856      mdd_free(intersection);
857    }
858    mdd_free(careSet);
859  }
860 
861
862  /* Increase the number of times the result has been used */
863  AbsVertexReadServed(vertexPtr)++;
864
865  return;
866} /* End of EvaluatePreImage */
867
868/**Function********************************************************************
869
870  Synopsis           [Compute an over-approximation of the Preimage]
871
872  SideEffects [This overapproximation is computed by just ignoring some FSM
873  components]
874
875  SeeAlso            [AbsSubFormulaVerify]
876
877******************************************************************************/
878static mdd_t *
879OverApproximatePreImageWithSubFSM(
880  Abs_VerificationInfo_t *absInfo,
881  mdd_t *lowerBound,
882  mdd_t *upperBound,
883  mdd_t *careSet)
884{
885  Fsm_Fsm_t       *system;
886  Img_ImageInfo_t *imageInfo;
887  mdd_t           *result;
888  long            cpuTime;
889
890  /* Initialize some variables */
891  system = AbsVerificationInfoReadApproxFsm(absInfo);
892
893  if (system == NIL(Fsm_Fsm_t)) {
894    system = AbsVerificationInfoReadFsm(absInfo);
895  }
896
897  /* Obtain the image info */
898  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
899
900  cpuTime = util_cpu_time();
901  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, lowerBound,
902                                                 upperBound, careSet);
903  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
904    util_cpu_time() - cpuTime;
905
906  return result;
907} /* End of OverApproximatePreImageWithSubFSM */
908
909
910/**Function********************************************************************
911
912  Synopsis [A second procedure to compute an over-approximation of the
913  Preimage]
914
915  SideEffects        []
916
917  SeeAlso            [AbsSubFormulaVerify]
918
919******************************************************************************/
920static mdd_t *
921OverApproximatePreImageWithBddSubsetting(
922  Abs_VerificationInfo_t *absInfo,
923  mdd_t *lowerBound,
924  mdd_t *upperBound,
925  mdd_t *careSet)
926{
927  Fsm_Fsm_t       *system;
928  Img_ImageInfo_t *imageInfo;
929  mdd_t           *superSet;
930  mdd_t           *result;
931  long            cpuTime;
932
933  /* Initialize some variables */
934  system = AbsVerificationInfoReadFsm(absInfo);
935
936  /* Compute the subset of the restriction set */
937  superSet = bdd_approx_remap_ua(lowerBound,BDD_OVER_APPROX,
938                          AbsVerificationInfoReadNumStateVars(absInfo), 
939                          0,1);
940 
941  /* Obtain the image info */
942  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
943
944  cpuTime = util_cpu_time();
945  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, superSet,
946                                                 superSet, careSet);
947  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
948    util_cpu_time() - cpuTime;
949
950  mdd_free(superSet);
951
952  return result;
953} /* End of OverApproximatePreImageWithBddSubsetting */
954
955/**Function********************************************************************
956
957  Synopsis           [Compute an under-approximation of the preimage]
958
959  SideEffects        []
960
961  SeeAlso            [AbsSubFormulaVerify]
962
963******************************************************************************/
964static mdd_t *
965UnderApproximatePreImageWithBddSubsetting(
966  Abs_VerificationInfo_t *absInfo,
967  mdd_t *lowerBound,
968  mdd_t *upperBound,
969  mdd_t *careSet)
970{
971  Fsm_Fsm_t       *system;
972  Img_ImageInfo_t *imageInfo;
973  mdd_t           *subSet;
974  mdd_t           *result;
975  long            cpuTime;
976
977  /* Initialize some variables */
978  system = AbsVerificationInfoReadFsm(absInfo);
979
980  /* Compute the subset of the restriction set */
981  subSet = bdd_approx_remap_ua(lowerBound, BDD_UNDER_APPROX,
982                      AbsVerificationInfoReadNumStateVars(absInfo),
983                      0,1);
984
985  /* Obtain the image info */
986  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
987
988  cpuTime = util_cpu_time();
989  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, subSet, subSet, 
990                                                 careSet);
991  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
992    util_cpu_time() - cpuTime;
993
994  mdd_free(subSet);
995
996  return result;
997} /* End of UnderApproximatePreImageWithBddSubsetting */
Note: See TracBrowser for help on using the repository browser.