source: vis_dev/vis-2.3/src/img/imgMonolithic.c @ 31

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

vis2.3
File size: 22.7 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imgMonolithic.c]
4
5  PackageName [img]
6
7  Synopsis    [Routines for image computation using a monolithic transition
8  relation.]
9
10  Author      [Rajeev K. Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon]
11
12  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
13  All rights reserved.
14
15  Permission is hereby granted, without written agreement and without license
16  or royalty fees, to use, copy, modify, and distribute this software and its
17  documentation for any purpose, provided that the above copyright notice and
18  the following two paragraphs appear in all copies of this software.
19
20  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
21  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
22  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
23  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24
25  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
26  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
27  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
28  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
29  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
30
31******************************************************************************/
32
33#include "imgInt.h"
34
35static char rcsid[] UNUSED = "$Id: imgMonolithic.c,v 1.23 2002/08/27 08:43:12 fabio Exp $";
36
37/**AutomaticStart*************************************************************/
38
39/*---------------------------------------------------------------------------*/
40/* Static function prototypes                                                */
41/*---------------------------------------------------------------------------*/
42
43static mdd_t * ImageComputeMonolithic(mdd_t *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray, array_t *smoothVars, mdd_t *smoothCube);
44
45/**AutomaticEnd***************************************************************/
46
47
48/*---------------------------------------------------------------------------*/
49/* Definition of exported functions                                          */
50/*---------------------------------------------------------------------------*/
51
52
53   
54/*---------------------------------------------------------------------------*/
55/* Definition of internal functions                                          */
56/*---------------------------------------------------------------------------*/
57
58
59/**Function********************************************************************
60
61  Synopsis    [Initializes an image structure for image computation
62  using a monolithic transition relation.]
63
64  Description [This function computes the monolithic transition relation
65  characterizing the behavior of the system from the individual functions.]
66
67  SideEffects []
68
69  SeeAlso     [Img_MultiwayLinearAndSmooth]
70******************************************************************************/
71void *
72ImgImageInfoInitializeMono(void *methodData, ImgFunctionData_t * functionData,
73                           Img_DirectionType directionType)
74{
75  if (!methodData){ /* Need to compute */
76    int          i;
77    mdd_t       *monolithicT;
78    array_t     *rootRelations = array_alloc(mdd_t*, 0);
79    graph_t     *mddNetwork    = functionData->mddNetwork;
80    mdd_manager *mddManager    = Part_PartitionReadMddManager(mddNetwork);
81    array_t     *roots         = functionData->roots;
82    array_t     *leaves        = array_join(functionData->domainVars,
83                                            functionData->quantifyVars);
84    array_t     *rootFunctions = Part_PartitionBuildFunctions(mddNetwork, roots,
85                                                              leaves,
86                                                              NIL(mdd_t)); 
87   
88    array_free(leaves);
89   
90   
91    /*
92     * Take the product of the transition relation of all the root nodes
93     * and smooth out the quantify variables.
94     */
95   
96    /*
97     * Iterate over the function of all the root nodes.
98     */ 
99    for (i=0; i<array_n(rootFunctions); i++) {
100      Mvf_Function_t *rootFunction  = array_fetch(Mvf_Function_t*, rootFunctions, i);
101      int             rangeVarMddId = array_fetch(int, functionData->rangeVars, i);
102      mdd_t          *rootRelation =
103          Mvf_FunctionBuildRelationWithVariable(rootFunction,
104                                                rangeVarMddId); 
105      array_insert_last(mdd_t*, rootRelations, rootRelation);
106    }
107   
108    Mvf_FunctionArrayFree(rootFunctions);
109    monolithicT = Img_MultiwayLinearAndSmooth(mddManager, rootRelations,
110                                              functionData->quantifyVars,
111                                              functionData->domainVars,
112                                              Img_Iwls95_c, Img_Forward_c);
113    mdd_array_free(rootRelations);
114    return ((void *)monolithicT);
115  }
116  else {
117    return methodData;
118  }
119}
120
121
122
123/**Function********************************************************************
124
125  Synopsis    [Computes the forward image of a set of states between
126  fromLowerBound and fromUpperBound.]
127
128  Description [Computes the forward image of a set of states between
129  fromLowerBound and fromUpperBound.  First a set of states between
130  fromLowerBound and fromUpperBound is computed.  Then, the transition
131  relation is simplified by cofactoring it wrt to the set of states found in
132  the first step, and wrt the toCareSet.]
133
134  SideEffects []
135
136  SeeAlso     [ImgImageInfoComputeBwdMono, ImgImageInfoComputeFwdWithDomainVarsMono]
137******************************************************************************/
138mdd_t *
139ImgImageInfoComputeFwdMono(
140  ImgFunctionData_t * functionData,
141  Img_ImageInfo_t * imageInfo,
142  mdd_t *fromLowerBound,
143  mdd_t *fromUpperBound,
144  array_t * toCareSetArray)
145{
146  return  ImageComputeMonolithic((mdd_t *) imageInfo->methodData,
147                                 fromLowerBound, fromUpperBound,
148                                 toCareSetArray, functionData->domainBddVars,
149                                 functionData->domainCube); 
150}
151
152 
153/**Function********************************************************************
154
155  Synopsis    [Computes the forward image on domain variables of a set
156  of states between fromLowerBound and fromUpperBound.]
157
158  Description [Identical to ImgImageInfoComputeFwdMono except
159  1. toCareSet is in terms of domain vars and hence range vars are
160  substituted first. 2. Before returning the image, range vars are
161  substituted with domain vars.]
162
163  SideEffects []
164
165  SeeAlso     [ImgImageInfoComputeFwdMono]
166******************************************************************************/
167mdd_t *
168ImgImageInfoComputeFwdWithDomainVarsMono(
169  ImgFunctionData_t *functionData,
170  Img_ImageInfo_t *imageInfo,
171  mdd_t *fromLowerBound,
172  mdd_t *fromUpperBound,
173  array_t *toCareSetArray)
174{
175  array_t *toCareSetArrayRV = ImgSubstituteArray(toCareSetArray,
176                                                 functionData, Img_D2R_c);
177  mdd_t *imageRV = ImgImageInfoComputeFwdMono(functionData,
178                                              imageInfo,
179                                              fromLowerBound,
180                                              fromUpperBound,
181                                              toCareSetArrayRV);
182  mdd_t *imageDV = ImgSubstitute(imageRV, functionData, Img_R2D_c);
183
184  mdd_array_free(toCareSetArrayRV);
185  mdd_free(imageRV);
186  return imageDV;
187}
188
189/**Function********************************************************************
190
191  Synopsis    [Computes the backward image of a set of states between
192  fromLowerBound and fromUpperBound.]
193
194  Description [Computes the backward image of a set of states between
195  fromLowerBound and fromUpperBound.  First a set of states between
196  fromLowerBound and fromUpperBound is computed.  Then, the transition
197  relation is simplified by cofactoring it wrt to the set of states found in
198  the first step, and wrt the toCareSet.]
199
200  SideEffects []
201 
202  SeeAlso     [ImgImageInfoComputeFwdMono,ImgImageInfoComputeBwdWithDomainVarsMono]
203
204******************************************************************************/
205mdd_t *
206ImgImageInfoComputeBwdMono(
207  ImgFunctionData_t * functionData,
208  Img_ImageInfo_t *imageInfo,
209  mdd_t *fromLowerBound,
210  mdd_t *fromUpperBound,
211  array_t *toCareSetArray)
212{
213  return ImageComputeMonolithic((mdd_t*)imageInfo->methodData, fromLowerBound,
214                                fromUpperBound, toCareSetArray, 
215                                functionData->rangeBddVars,
216                                functionData->rangeCube); 
217}
218
219/**Function********************************************************************
220
221  Synopsis    [Computes the backward image of a set of states between
222  fromLowerBound and fromUpperBound.]
223
224  Description [Identical to ImgImageInfoComputeBwdMono except that
225  fromLowerBound and fromUpperBound and given in terms of domain
226  variables, hence we need to substitute the range variables first.]
227 
228  SideEffects []
229
230  SeeAlso [ImgImageInfoComputeBwdMono]
231
232******************************************************************************/
233mdd_t *
234ImgImageInfoComputeBwdWithDomainVarsMono(
235  ImgFunctionData_t * functionData,
236  Img_ImageInfo_t *imageInfo,
237  mdd_t *fromLowerBound,
238  mdd_t *fromUpperBound,
239  array_t *toCareSetArray)
240{
241  mdd_t *fromLowerBoundRV = ImgSubstitute(fromLowerBound,
242                                          functionData, Img_D2R_c);
243  mdd_t *fromUpperBoundRV = ImgSubstitute(fromUpperBound,
244                                          functionData, Img_D2R_c);
245  mdd_t *image = ImgImageInfoComputeBwdMono(functionData,
246                                            imageInfo,
247                                            fromLowerBoundRV,
248                                            fromUpperBoundRV,
249                                            toCareSetArray);
250  mdd_free(fromLowerBoundRV);
251  mdd_free(fromUpperBoundRV);
252  return image;
253}
254
255
256
257/**Function********************************************************************
258
259  Synopsis    [Frees the method data associated with the monolithic method.]
260
261  SideEffects []
262
263******************************************************************************/
264void
265ImgImageInfoFreeMono(void * methodData)
266{
267  mdd_free((mdd_t *)methodData);
268}
269
270/**Function********************************************************************
271
272  Synopsis    [Prints information about the IWLS95 method.]
273
274  Description [This function is used to obtain the information about
275  the parameters used to initialize the imageInfo.]
276
277  SideEffects []
278
279******************************************************************************/
280void
281ImgImageInfoPrintMethodParamsMono(void *methodData, FILE *fp)
282{
283  mdd_t *monolithicRelation = (mdd_t *)methodData;
284  (void) fprintf(fp,"Printing information about image method: Monolithic\n"); 
285  (void) fprintf(fp,"\tSize of monolithic relation = %10ld\n",
286                 (long) bdd_size(monolithicRelation));
287}
288
289/**Function********************************************************************
290
291  Synopsis    [Restores original transition relation from saved.]
292
293  Description [Restores original transition relation from saved.]
294
295  SideEffects []
296
297******************************************************************************/
298void
299ImgRestoreTransitionRelationMono(Img_ImageInfo_t *imageInfo,
300        Img_DirectionType directionType)
301{
302  mdd_free((mdd_t *) imageInfo->methodData);
303  imageInfo->methodData = (mdd_t *)imageInfo->savedRelation;
304  imageInfo->savedRelation = NIL(void);
305  return;
306}
307
308/**Function********************************************************************
309
310  Synopsis    [Duplicates transition relation.]
311
312  Description [Duplicates transition relation. Assumes that the
313  Transition Relation is a MDD.]
314
315  SideEffects []
316
317******************************************************************************/
318void
319ImgDuplicateTransitionRelationMono(Img_ImageInfo_t *imageInfo)
320{
321  imageInfo->savedRelation = (void *)mdd_dup((mdd_t *) imageInfo->methodData);
322  return;
323}
324
325/**Function********************************************************************
326
327  Synopsis    [Minimizes transition relation with given constraint.]
328
329  Description [Minimizes transition relation with given constraint.]
330
331  SideEffects []
332
333******************************************************************************/
334void
335ImgMinimizeTransitionRelationMono(Img_ImageInfo_t *imageInfo,
336        array_t *constrainArray, Img_MinimizeType minimizeMethod,
337        int printStatus)
338{
339  mdd_t *relation, *simplifiedRelation;
340  int i, size = 0;
341  mdd_t *constrain;
342
343  relation = (mdd_t *)imageInfo->methodData;
344
345  if (printStatus)
346    size = bdd_size(relation);
347
348  for (i = 0; i < array_n(constrainArray); i++) {
349    constrain = array_fetch(mdd_t *, constrainArray, i);
350    simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod,
351                                           TRUE);
352    if (printStatus) {
353      (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n",
354                     bdd_size(relation), bdd_size(constrain),
355                     bdd_size(simplifiedRelation));
356    }
357    mdd_free(relation);
358    relation = simplifiedRelation;
359  }
360  imageInfo->methodData = (void *)relation;
361
362  if (printStatus) {
363    (void) fprintf(vis_stdout,
364        "IMG Info: minimized relation [%d | %ld => %d]\n",
365                   size, bdd_size_multiple(constrainArray),
366                   bdd_size(relation));
367  }
368}
369
370/**Function********************************************************************
371
372  Synopsis    [Add dont care to transition relation.]
373
374  Description [Add dont care to transition relation. The constrain
375  array contains care sets.]
376
377  SideEffects []
378
379******************************************************************************/
380void
381ImgAddDontCareToTransitionRelationMono(Img_ImageInfo_t *imageInfo,
382        array_t *constrainArray, Img_MinimizeType minimizeMethod,
383        int printStatus)
384{
385  mdd_t *relation, *simplifiedRelation;
386  int i, size = 0;
387  mdd_t *constrain;
388
389  relation = (mdd_t *)imageInfo->methodData;
390
391  if (printStatus)
392    size = bdd_size(relation);
393
394  for (i = 0; i < array_n(constrainArray); i++) {
395    constrain = array_fetch(mdd_t *, constrainArray, i);
396    simplifiedRelation = Img_AddDontCareToImage(relation,
397                                             constrain, minimizeMethod);
398    if (printStatus) {
399      (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n",
400                     bdd_size(relation), bdd_size(constrain),
401                     bdd_size(simplifiedRelation));
402    }
403    mdd_free(relation);
404    relation = simplifiedRelation;
405  }
406  imageInfo->methodData = (void *)relation;
407
408  if (printStatus) {
409    (void) fprintf(vis_stdout,
410        "IMG Info: minimized relation [%d | %ld => %d]\n",
411                   size, bdd_size_multiple(constrainArray),
412                   bdd_size(relation));
413  }
414}
415
416
417/**Function********************************************************************
418
419  Synopsis    [Abstracts out given variables from transition relation.]
420
421  Description [Abstracts out given variables from transition relation.
422  abstractVars should be an array of bdd variables.]
423
424  SideEffects []
425
426******************************************************************************/
427void
428ImgAbstractTransitionRelationMono(Img_ImageInfo_t *imageInfo,
429        array_t *abstractVars, mdd_t *abstractCube, int printStatus)
430{
431  mdd_t *relation, *abstractedRelation;
432
433  relation = (mdd_t *)imageInfo->methodData;
434  if (abstractCube)
435    abstractedRelation = bdd_smooth_with_cube(relation, abstractCube);
436  else
437    abstractedRelation = bdd_smooth(relation, abstractVars);
438  if (printStatus) {
439    (void) fprintf(vis_stdout, "Info: abstracted relation %d => %d\n",
440                     bdd_size(relation), bdd_size(abstractedRelation));
441  }
442  mdd_free(relation);
443  imageInfo->methodData = (void *)abstractedRelation;
444}
445
446
447/**Function********************************************************************
448
449  Synopsis    [Approximates transition relation.]
450
451  Description [Approximates transition relation.]
452
453  SideEffects []
454
455******************************************************************************/
456int
457ImgApproximateTransitionRelationMono(mdd_manager *mgr,
458        Img_ImageInfo_t *imageInfo,
459        bdd_approx_dir_t approxDir,
460        bdd_approx_type_t approxMethod,
461        int approxThreshold,
462        double approxQuality,
463        double approxQualityBias,
464        mdd_t *bias)
465{
466  mdd_t *relation, *approxRelation;
467  int   unchanged;
468
469  relation = (mdd_t *)imageInfo->methodData;
470  approxRelation = Img_ApproximateImage(mgr, relation, approxDir, approxMethod,
471                                        approxThreshold, approxQuality,
472                                        approxQualityBias, bias);
473  if (bdd_is_tautology(approxRelation, 1)) {
474    fprintf(vis_stdout, "** img warning : bdd_one from subsetting.\n");
475    mdd_free(approxRelation);
476    unchanged = 1;
477  } else if (bdd_is_tautology(approxRelation, 0)) {
478    fprintf(vis_stdout, "** img warning : bdd_zero from subsetting.\n");
479    mdd_free(approxRelation);
480    unchanged = 1;
481  } else if (mdd_equal(approxRelation, relation)) {
482    mdd_free(approxRelation);
483    unchanged = 1;
484  } else {
485    mdd_free(relation);
486    imageInfo->methodData = (void *)approxRelation;
487    unchanged = 0;
488  }
489  return(unchanged);
490}
491
492/**Function********************************************************************
493
494  Synopsis [Constrains/adds dont-cares to the bit relation and creates
495  a new transition relation.]
496
497  Description [Constrains/adds dont-cares to the bit relation and
498  creates a new transition relation. First, the existing transition
499  relation is freed. The bit relation is created and constrained by
500  the given constraint (underapprox) or its complement is add to the
501  bit relation (overapprox) depending on the underApprox flag. Then
502  the modified bit relation is clustered. The code is similar to
503  ImgImageInfoInitializeMono. An over or under approximation of the
504  transition relation may be created. The underApprox flag should be
505  TRUE for an underapproximation and FALSE for an
506  overapproximation. Although Img_MinimizeImage is used the
507  minimizeMethod flag for underapproximations has to be passed by
508  Img_GuidedSearchReadUnderApproxMinimizeMethod. The cleanUp flag is
509  currently useless but is maintained for uniformity with other Image
510  computation methods incase methodData changes in the future to store
511  bitRelations. The flag ]
512
513  SideEffects [Current transition relation and quantification schedule
514  are freed. Bit relations are freed if indicated.]
515
516  SeeAlso [Img_MultiwayLinearAndSmooth ImgImageInfoInitializeMono
517  Img_MinimizeImage Img_AddDontCareToImage ]
518******************************************************************************/
519void 
520ImgImageConstrainAndClusterTransitionRelationMono(Img_ImageInfo_t *imageInfo,
521                                                  mdd_t *constrain,
522                                                  Img_MinimizeType minimizeMethod,
523                                                  boolean underApprox,
524                                                  boolean cleanUp,
525                                                  boolean forceReorder,
526                                                  int printStatus)
527{
528  ImgFunctionData_t *functionData = &(imageInfo->functionData);
529  mdd_t *methodData = (mdd_t *)imageInfo->methodData;
530  int          i;
531  mdd_t       *monolithicT;
532  array_t     *rootRelations = array_alloc(mdd_t*, 0);
533  graph_t     *mddNetwork    = functionData->mddNetwork;
534  mdd_manager *mddManager    = Part_PartitionReadMddManager(mddNetwork);
535  array_t     *roots         = functionData->roots;
536  array_t     *leaves        = array_join(functionData->domainVars,
537                                          functionData->quantifyVars);
538  array_t     *rootFunctions;
539  mdd_t       *relation;
540 
541  /*free existing  relation. */
542  if (!methodData) ImgImageInfoFreeMono(methodData);   
543  if (forceReorder) bdd_reorder(mddManager);
544  rootFunctions = Part_PartitionBuildFunctions(mddNetwork, roots,
545                                               leaves,
546                                               NIL(mdd_t)); 
547 
548  array_free(leaves);
549   
550  /*
551   * Take the product of the transition relation of all the root nodes
552   * and smooth out the quantify variables.
553   */
554 
555  /*
556   * Iterate over the function of all the root nodes.
557   */ 
558  for (i=0; i<array_n(rootFunctions); i++) {
559    Mvf_Function_t *rootFunction  = array_fetch(Mvf_Function_t*, rootFunctions, i);
560    int             rangeVarMddId = array_fetch(int, functionData->rangeVars, i);
561    mdd_t          *rootRelation =
562      Mvf_FunctionBuildRelationWithVariable(rootFunction,
563                                            rangeVarMddId); 
564    array_insert_last(mdd_t*, rootRelations, rootRelation);
565  }
566  Mvf_FunctionArrayFree(rootFunctions);
567
568  /* Constrain the bit relaitons */
569  if (constrain) {
570    arrayForEachItem(mdd_t *, rootRelations, i, relation) {
571      mdd_t *simplifiedRelation;
572      simplifiedRelation = Img_MinimizeImage(relation, constrain,
573                                             minimizeMethod, underApprox);
574      if (printStatus) {
575        (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n",
576                       bdd_size(relation), bdd_size(constrain),
577                       bdd_size(simplifiedRelation));
578      }
579      mdd_free(relation);
580      array_insert(mdd_t *, rootRelations, i, simplifiedRelation);
581    }
582  }
583
584  /* build the monolithic transition relation. */
585  monolithicT = Img_MultiwayLinearAndSmooth(mddManager, rootRelations,
586                                            functionData->quantifyVars,
587                                            functionData->domainVars,
588                                            Img_Iwls95_c, Img_Forward_c);
589  mdd_array_free(rootRelations);
590  imageInfo->methodData = (void *)monolithicT;
591  if (printStatus) {
592    ImgImageInfoPrintMethodParamsMono(monolithicT, vis_stdout);
593  }
594
595}
596
597
598
599/*---------------------------------------------------------------------------*/
600/* Definition of static functions                                            */
601/*---------------------------------------------------------------------------*/
602/**Function********************************************************************
603
604  Synopsis    [A generic routine for computing the image.]
605
606  Description [This is a routine for image computation which is called
607  by both forward image and backward image computation. The frontier
608  set (the set of states for which the image is computed) is obtained
609  by finding a small size BDD between lower and upper bounds.
610  The transition relation is simplified by cofactoring
611  it with the domainSubset (frontier set) and with the toCareSet. The
612  order in which this simplification is unimportant from functionality
613  point of view, but the order might effect the BDD size of the
614  optimizedRelation. smoothVars should be an array of bdd variables.]
615
616  SideEffects []
617
618******************************************************************************/
619static mdd_t *
620ImageComputeMonolithic(mdd_t *methodData, mdd_t *fromLowerBound, mdd_t
621                *fromUpperBound, array_t *toCareSetArray,
622                array_t *smoothVars, mdd_t *smoothCube)
623{
624  mdd_t       *domainSubset, *image;
625  mdd_t       *optimizedRelation, *subOptimizedRelation;
626  mdd_t       *monolithicT = (mdd_t *)methodData;
627 
628  assert(monolithicT != NIL(mdd_t));
629 
630  /*
631   * Optimization steps:
632   * Choose the domainSubset optimally.
633   * Reduce the transition relation wrt to care set and domainSubset.
634   */
635  domainSubset = bdd_between(fromLowerBound,fromUpperBound);
636  subOptimizedRelation = bdd_cofactor_array(monolithicT, toCareSetArray);
637  optimizedRelation = bdd_cofactor(subOptimizedRelation, domainSubset); 
638  mdd_free(domainSubset);
639  mdd_free(subOptimizedRelation);
640  /*optimizedRelation = bdd_and(fromLowerBound, monolithicT, 1, 1);*/
641  if (smoothCube)
642    image = bdd_smooth_with_cube(optimizedRelation, smoothCube);
643  else {
644    if (array_n(smoothVars) == 0)
645      image = mdd_dup(optimizedRelation);
646    else
647      image = bdd_smooth(optimizedRelation, smoothVars);
648  }
649
650  mdd_free(optimizedRelation);
651  return image;
652}
653
Note: See TracBrowser for help on using the repository browser.