source: vis_dev/vis-2.3/src/abs/absTranslate.c @ 93

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

vis2.3
File size: 53.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [absTranslate.c]
4
5  PackageName [abs]
6
7  Synopsis    [Functions to translate CTL formulas to mu-calculus graphs.]
8
9  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
10
11  Copyright   [This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "absInt.h"
19
20static char rcsid[] UNUSED = "$Id: absTranslate.c,v 1.14 2002/09/04 14:58:18 fabio Exp $";
21
22
23/*---------------------------------------------------------------------------*/
24/* Macro declarations                                                        */
25/*---------------------------------------------------------------------------*/
26
27
28/**AutomaticStart*************************************************************/
29
30/*---------------------------------------------------------------------------*/
31/* Static function prototypes                                                */
32/*---------------------------------------------------------------------------*/
33
34static AbsVertexInfo_t * TranslateCtlSubFormula(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
35static AbsVertexInfo_t * ComputeFairPredicate(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *atomicPredicate, array_t *fairArray, int polarity, int *uniqueIds);
36static AbsVertexInfo_t * TranslateCtlID(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity);
37static AbsVertexInfo_t * TranslateCtlEU(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
38static AbsVertexInfo_t * TranslateCtlEG(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity, int *uniqueIds);
39static AbsVertexInfo_t * TranslateCtlEGFair(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
40static AbsVertexInfo_t * TranslateCtlEX(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
41static AbsVertexInfo_t * TranslateCtlNOT(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
42static AbsVertexInfo_t * TranslateCtlTHEN(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
43static AbsVertexInfo_t * TranslateCtlAND(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
44static AbsVertexInfo_t * TranslateCtlOR(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
45static AbsVertexInfo_t * CreateConjunctionChain(AbsVertexCatalog_t *catalog, array_t *conjunctions, int polarity);
46
47/**AutomaticEnd***************************************************************/
48
49
50/*---------------------------------------------------------------------------*/
51/* Definition of exported functions                                          */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Definition of internal functions                                          */
56/*---------------------------------------------------------------------------*/
57
58/**Function********************************************************************
59
60  Synopsis [Translate an array of CTL formulas to an array of labeled
61  operational graphs. The graphs may share vertices among them.]
62
63  SideEffects        []
64
65  SeeAlso            [TranslateCtlSubFormula]
66
67******************************************************************************/
68array_t *
69AbsCtlFormulaArrayTranslate(
70  Abs_VerificationInfo_t *verInfo,
71  array_t *formulaArray,
72  array_t *fairArray)
73{
74  AbsVertexCatalog_t *catalog;
75  Ctlp_Formula_t  *formulaPtr;
76  AbsVertexInfo_t *fairPositive;
77  AbsVertexInfo_t *fairNegative;
78  array_t         *result;
79  boolean         initialPolarity;
80  int             uniqueIds;
81  int             i;
82
83  if (formulaArray == NIL(array_t)) {
84    return NIL(array_t);
85  }
86
87  /* Initialize certain variables */
88  catalog = AbsVerificationInfoReadCatalog(verInfo);
89  uniqueIds = 0;
90
91  if (fairArray != NIL(array_t)) {
92    fairPositive = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t),
93                                        fairArray, TRUE, &uniqueIds);
94
95    fairNegative = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t), 
96                                        fairArray, FALSE, &uniqueIds);
97  }
98  else {
99    fairPositive = NIL(AbsVertexInfo_t);
100    fairNegative = NIL(AbsVertexInfo_t);
101  }
102
103  if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
104    initialPolarity = TRUE;
105  }
106  else {
107    initialPolarity = FALSE;
108  }
109
110  /* Create the result */
111  result = array_alloc(AbsVertexInfo_t *, array_n(formulaArray));
112
113  arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formulaPtr) {
114    AbsVertexInfo_t *resultPtr;
115
116    /* Translate the formula */
117    resultPtr = TranslateCtlSubFormula(AbsVerificationInfoReadCatalog(verInfo),
118                                       formulaPtr,      /* Formula */
119                                       fairArray,       /* Fairness
120                                                           constraints */
121                                       fairPositive,    /* Predicate fair
122                                                           with positive
123                                                           polarity */
124                                       fairNegative,    /* Predicate fair
125                                                           with negative
126                                                           polarity */
127                                       initialPolarity, /* Initial polarity */
128                                       &uniqueIds);     /* Unique id counter */
129
130    /* Negate the formula if needed */
131    if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
132      AbsVertexInfo_t *newResult;
133
134      /* If the formula's top vertex is a negation, eliminate the redundancy */
135      if (AbsVertexReadType(resultPtr) == not_c) {
136       
137        newResult = AbsVertexReadLeftKid(resultPtr);
138        AbsVertexReadRefs(newResult)++;
139        AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
140       
141        resultPtr =  newResult;
142      }
143      else {
144        /* Create the not vertex */
145        newResult = AbsVertexCatalogFindOrAdd(catalog, not_c, FALSE, 
146                                              resultPtr,
147                                              NIL(AbsVertexInfo_t), 0, 
148                                              NIL(char), 
149                                              NIL(char));
150        if (AbsVertexReadType(newResult) == false_c) {
151          AbsVertexSetPolarity(newResult, FALSE);
152          AbsVertexSetDepth(newResult, AbsVertexReadDepth(resultPtr) + 1);
153          AbsVertexSetType(newResult, not_c);
154          AbsVertexSetLeftKid(newResult, resultPtr);
155          AbsVertexSetParent(resultPtr, newResult);
156        }
157        else {
158          AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
159        }
160        resultPtr = newResult;
161      }
162    } /* If the formula needs to be negated */
163
164    /* Set the constant bit */
165    AbsFormulaSetConstantBit(resultPtr);
166
167    array_insert(AbsVertexInfo_t *, result, i, resultPtr);
168  }
169
170  /* Clean up */
171  if (fairPositive != NIL(AbsVertexInfo_t)) {
172    AbsVertexFree(catalog, fairPositive, NIL(AbsVertexInfo_t));
173  }
174  if (fairNegative != NIL(AbsVertexInfo_t)) {
175    AbsVertexFree(catalog, fairNegative, NIL(AbsVertexInfo_t));
176  }
177
178#ifndef NDEBUG
179  {
180    AbsVertexInfo_t *operationGraph;
181    st_table *rootTable = st_init_table(st_ptrcmp, st_ptrhash);
182    arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
183      st_insert(rootTable, (char *) operationGraph, NIL(char));
184    }
185    arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
186      assert(AbsFormulaSanityCheck(operationGraph, rootTable));
187    }
188    st_free_table(rootTable);
189  }
190#endif
191
192  return result;
193} /* End of AbsCtlFormulaArrayTranslate */
194
195
196/*---------------------------------------------------------------------------*/
197/* Definition of static functions                                            */
198/*---------------------------------------------------------------------------*/
199
200/**Function********************************************************************
201
202  Synopsis [Recursive formula to translate a formula to its operational graph]
203
204  Description [This function is just a case to call the specific translation
205  routines for the different types of sub-formulas]
206
207  SideEffects        []
208
209  SeeAlso [TranslateCtlId, TranslateCtlEG, TranslateCtlEGFair, TranslateCtlEU,
210  TranslateCtlEX, TranslateCtlNOT, TranslateCtlTHEN, TranslateCtlAND,
211  TranslateCtlOR]
212
213******************************************************************************/
214static AbsVertexInfo_t *
215TranslateCtlSubFormula(
216  AbsVertexCatalog_t *catalog,
217  Ctlp_Formula_t *formula,
218  array_t *fairArray,
219  AbsVertexInfo_t *fairPositive,
220  AbsVertexInfo_t *fairNegative,
221  int polarity,
222  int *uniqueIds)
223{
224  AbsVertexInfo_t *result;
225
226  result = NIL(AbsVertexInfo_t);
227
228  switch (Ctlp_FormulaReadType(formula)) {
229    case Ctlp_TRUE_c:
230    case Ctlp_FALSE_c: {
231      (void) fprintf(vis_stderr, "** abs error: Error in TranslateCtlSubFormula. ");
232      (void) fprintf(vis_stderr, "TRUE/FALSE constant found.\n");
233      result = NIL(AbsVertexInfo_t);
234      break;
235    }
236    case Ctlp_ID_c: {
237      result = TranslateCtlID(catalog, formula, polarity);
238      break;
239    }
240    case Ctlp_EG_c: {
241      if (fairArray == NIL(array_t)) {
242        result = TranslateCtlEG(catalog, formula, polarity, uniqueIds);
243      }
244      else {
245        result = TranslateCtlEGFair(catalog, formula, fairArray, fairPositive, 
246                                    fairNegative, polarity, uniqueIds);
247      }
248      break;
249    }
250    case Ctlp_EU_c: {
251      result = TranslateCtlEU(catalog, formula, fairArray, fairPositive, 
252                              fairNegative, polarity, uniqueIds);
253      break;
254    }
255    case Ctlp_EX_c: {
256      result = TranslateCtlEX(catalog, formula, fairArray, fairPositive, 
257                              fairNegative, polarity, uniqueIds);
258      break;
259    }
260    case Ctlp_NOT_c: {
261      result = TranslateCtlNOT(catalog, formula, fairArray, fairPositive, 
262                               fairNegative, polarity, uniqueIds);
263      break;
264    }
265    case Ctlp_THEN_c:  {
266      result = TranslateCtlTHEN(catalog, formula, fairArray, fairPositive, 
267                                fairNegative, polarity, uniqueIds);
268      break;
269    }
270    case Ctlp_EQ_c:
271    case Ctlp_XOR_c: {
272      /* Non-monotonic operators should have been replaced before
273       * reaching this point.
274       */
275      fail("Encountered unexpected type of CTL formula\n");
276      break;
277    }
278    case Ctlp_AND_c: {
279      result = TranslateCtlAND(catalog, formula, fairArray, fairPositive, 
280                               fairNegative, polarity, uniqueIds);
281      break;
282    }
283    case Ctlp_OR_c: {
284      result = TranslateCtlOR(catalog, formula, fairArray, fairPositive, 
285                              fairNegative, polarity, uniqueIds);
286      break;
287    }
288    default: fail("Encountered unknown type of CTL formula\n");
289  }
290
291  return result;
292} /* End of TranslateCtlSubFormula */
293
294/**Function********************************************************************
295
296  Synopsis [Computes the operational graph representation of the predicate
297  "fair"]
298
299  Description [Given a set of formulas f_1,...,f_n compute the predicate fair
300  which is computed as follows: fair(p) = nu(x).(p * Product(i=1,n)(EX[E[p U (x
301  * f_i)]])). The final graph will have in its top vertex the polarity given as
302  a parameter to the routine.]
303
304  SideEffects        []
305
306  SeeAlso            [AbsCtlFormulaArrayTranslate]
307
308******************************************************************************/
309static AbsVertexInfo_t *
310ComputeFairPredicate(
311  AbsVertexCatalog_t *catalog,
312  AbsVertexInfo_t *atomicPredicate,
313  array_t *fairArray,
314  int polarity,
315  int *uniqueIds)
316{
317  Ctlp_Formula_t *ctlPtr;
318  AbsVertexInfo_t *mainVarVertex;
319  AbsVertexInfo_t *mainVarNotVertex;
320  AbsVertexInfo_t *vertexPtr;
321  AbsVertexInfo_t *aux1;
322  AbsVertexInfo_t *aux2;
323  AbsVertexInfo_t *aux3;
324  array_t *conjunctions;
325  array_t *constraintArray;
326  int     mainVarId;
327  int     i;
328 
329  /* Obtain the representation of the fairness predicates */
330  constraintArray = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
331  arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlPtr) {
332    array_insert(AbsVertexInfo_t *, constraintArray, i, 
333                 TranslateCtlSubFormula(catalog, ctlPtr, NIL(array_t), 
334                                        NIL(AbsVertexInfo_t), 
335                                        NIL(AbsVertexInfo_t), polarity, 
336                                        uniqueIds));
337  }
338
339  /* Create the vertex representing the variable of the greatest fixed point */
340  mainVarId = (*uniqueIds)++;
341
342  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity, 
343                                   NIL(AbsVertexInfo_t), 
344                                   NIL(AbsVertexInfo_t),
345                                   mainVarId, NIL(char), NIL(char));
346  if (AbsVertexReadType(aux1) == false_c) {
347    AbsVertexSetPolarity(aux1, !polarity);
348    AbsVertexSetDepth(aux1, 1);
349    AbsVertexSetType(aux1, variable_c);
350    AbsVertexSetVarId(aux1, mainVarId);
351  }
352  mainVarVertex = aux1;
353
354  mainVarNotVertex = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
355                                               NIL(AbsVertexInfo_t), 0, 
356                                               NIL(char), NIL(char));
357  if (AbsVertexReadType(mainVarNotVertex) == false_c) {
358    AbsVertexSetPolarity(mainVarNotVertex, polarity);
359    AbsVertexSetDepth(mainVarNotVertex, 2);
360    AbsVertexSetType(mainVarNotVertex, not_c);
361    AbsVertexSetLeftKid(mainVarNotVertex, aux1);
362    AbsVertexSetParent(mainVarVertex, mainVarNotVertex);
363  }
364  else {
365    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
366  }
367
368  /* Create the predicates EX[E[f U z * f_i]] */
369  conjunctions = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
370  arrayForEachItem(AbsVertexInfo_t *, constraintArray, i, vertexPtr) {
371    AbsVertexInfo_t *varVertex;
372    int variableId;
373
374    /* Create the conjunction between z and f_i */
375    AbsVertexReadRefs(mainVarNotVertex)++;
376    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, vertexPtr, 
377                                     mainVarNotVertex, 0, NIL(char), 
378                                     NIL(char));
379    if (AbsVertexReadType(aux1) == false_c) {
380      AbsVertexSetPolarity(aux1, polarity);
381      if (AbsVertexReadDepth(vertexPtr) > 2) {
382        AbsVertexSetDepth(aux1, AbsVertexReadDepth(vertexPtr) + 1);
383      }
384      else {
385        AbsVertexSetDepth(aux1, 3);
386      }
387      AbsVertexSetType(aux1, and_c);
388      AbsVertexSetLeftKid(aux1, vertexPtr);
389      AbsVertexSetRightKid(aux1, mainVarNotVertex);
390      AbsVertexSetParent(vertexPtr, aux1);
391      AbsVertexSetParent(mainVarNotVertex, aux1);
392    }
393    else {
394      /* Cache hit */
395      AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
396      AbsVertexFree(catalog, mainVarNotVertex, NIL(AbsVertexInfo_t));
397    }
398
399    /* Create the vertex negating the previous conjunction */
400    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
401                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
402                                     NIL(char));
403    if (AbsVertexReadType(aux2) == false_c) {
404      AbsVertexSetPolarity(aux2, !polarity);
405      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
406      AbsVertexSetType(aux2, not_c);
407      AbsVertexSetLeftKid(aux2, aux1);
408      AbsVertexSetParent(aux1, aux2);
409    }
410    else {
411      /* Cache hit */
412      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
413    }
414
415    /* Create the variable of the fixed point in the EU sub-formula*/
416    variableId = (*uniqueIds)++;
417    aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
418                                     NIL(AbsVertexInfo_t), 
419                                     NIL(AbsVertexInfo_t), variableId, 
420                                     NIL(char), NIL(char));
421    if (AbsVertexReadType(aux1) == false_c) {
422      AbsVertexSetPolarity(aux1, polarity);
423      AbsVertexSetDepth(aux1, 1);
424      AbsVertexSetType(aux1, variable_c);
425      AbsVertexSetVarId(aux1, variableId);
426    }
427    varVertex = aux1;
428
429    /* Create the vertex storing the preimage sub-formula */
430    aux3 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
431                                     aux1, NIL(AbsVertexInfo_t),
432                                     0, NIL(char), NIL(char));
433    if (AbsVertexReadType(aux3) == false_c) {
434      AbsVertexSetPolarity(aux3, polarity);
435      AbsVertexSetDepth(aux3, 2);
436      AbsVertexSetType(aux3, preImage_c);
437      AbsVertexSetLeftKid(aux3, aux1);
438      AbsVertexSetParent(aux1, aux3);
439    }
440    else {
441      /* Cache hit */
442      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
443    }
444 
445    if (atomicPredicate != NIL(AbsVertexInfo_t)) {
446      AbsVertexReadRefs(atomicPredicate)++;
447      /* Create the vertex representing the and */
448      aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
449                                       atomicPredicate, aux3, 0, NIL(char), 
450                                       NIL(char));
451      if (AbsVertexReadType(aux1) == false_c) {
452        AbsVertexSetPolarity(aux1, polarity);
453        if (AbsVertexReadDepth(atomicPredicate) > 2) {
454          AbsVertexSetDepth(aux1, AbsVertexReadDepth(atomicPredicate) + 1);
455        }
456        else {
457          AbsVertexSetDepth(aux1, 3);
458        }
459        AbsVertexSetType(aux1, and_c);
460        AbsVertexSetLeftKid(aux1, atomicPredicate);
461        AbsVertexSetRightKid(aux1, aux3);
462        AbsVertexSetParent(atomicPredicate, aux1);
463        AbsVertexSetParent(aux3, aux1);
464      }
465      else {
466        /* Cache hit */
467        AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
468        AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
469      }
470    }
471    else {
472      aux1 = aux3;
473    }
474
475    /* Create the not vertex on top of the conjunction */
476    aux3 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
477                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
478                                     NIL(char));
479    if (AbsVertexReadType(aux3) == false_c) {
480      AbsVertexSetPolarity(aux3, !polarity);
481      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
482      AbsVertexSetType(aux3, not_c);
483      AbsVertexSetLeftKid(aux3, aux1);
484      AbsVertexSetParent(aux1, aux3);
485    }
486    else {
487      /* Cache hit */
488      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
489    }
490   
491    /* Vertex taking the conjunction */
492    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux2, aux3,
493                                     0, NIL(char), NIL(char));
494    if (AbsVertexReadType(aux1) == false_c) {
495      AbsVertexSetPolarity(aux1, !polarity);
496      if (AbsVertexReadDepth(aux2) > AbsVertexReadDepth(aux3)) {
497        AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
498      }
499      else {
500        AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
501      }
502      AbsVertexSetType(aux1, and_c);
503      AbsVertexSetLeftKid(aux1, aux2);
504      AbsVertexSetRightKid(aux1, aux3);
505      AbsVertexSetParent(aux3, aux1);
506      AbsVertexSetParent(aux2, aux1);
507    }
508    else {
509      AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
510      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
511    }
512   
513    /* negation of the conjunction */
514    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
515                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
516                                     NIL(char));
517    if (AbsVertexReadType(aux2) == false_c) {
518      AbsVertexSetPolarity(aux2, polarity);
519      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
520      AbsVertexSetType(aux2, not_c);
521      AbsVertexSetLeftKid(aux2, aux1);
522      AbsVertexSetParent(aux1, aux2);
523    }
524    else {
525      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
526    }
527 
528    /* Create the lfp vertex for the EU operator */
529    aux1 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux2,
530                                     NIL(AbsVertexInfo_t), 0, NIL(char),
531                                     NIL(char));
532    if (AbsVertexReadType(aux1) == false_c) {
533      AbsVertexSetPolarity(aux1, polarity);
534      AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
535      AbsVertexSetType(aux1, fixedPoint_c);
536      AbsVertexSetLeftKid(aux1, aux2);
537      AbsVertexSetFpVar(aux1, varVertex);
538      AbsVertexSetUseExtraCareSet(aux1, TRUE);
539      AbsVertexSetParent(aux2, aux1);
540    }
541    else {
542      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
543    }
544   
545    /* Create the final EX vertex on top of the EU */
546    aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
547                                     aux1, NIL(AbsVertexInfo_t), 0, NIL(char),
548                                     NIL(char));
549    if (AbsVertexReadType(aux2) == false_c) {
550      AbsVertexSetPolarity(aux2, polarity);
551      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
552      AbsVertexSetType(aux2, preImage_c);
553      AbsVertexSetLeftKid(aux2, aux1);
554      AbsVertexSetParent(aux1, aux2);
555    }
556    else {
557      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
558    }
559
560    array_insert(AbsVertexInfo_t *, conjunctions, i, aux2);
561  } /* End of the loop iterating over the fairness constraints */
562  AbsVertexReadRefs(mainVarNotVertex)--;
563
564  /* Create the chain of ands for the conjunctions */
565  aux1 = CreateConjunctionChain(catalog, conjunctions, polarity);
566
567  /* Create the and with the atomic predicate if required */
568  if (atomicPredicate != NIL(AbsVertexInfo_t)) {
569    aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, atomicPredicate, 
570                                     aux1, 0, NIL(char), NIL(char));
571    if (AbsVertexReadType(aux2) == false_c) {
572      AbsVertexSetPolarity(aux2, polarity);
573      if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(atomicPredicate)) {
574        AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
575      }
576      else {
577        AbsVertexSetDepth(aux2, AbsVertexReadDepth(atomicPredicate) + 1);
578      }
579      AbsVertexSetType(aux2, and_c);
580      AbsVertexSetLeftKid(aux2, atomicPredicate);
581      AbsVertexSetRightKid(aux2, aux1);
582      AbsVertexSetParent(atomicPredicate, aux2);
583      AbsVertexSetParent(aux1, aux2);
584    }
585    else {
586      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
587      AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
588    }
589  }
590  else {
591    aux2 = aux1;
592  }
593
594  /* Create the not vertex on top of the conjunction */
595  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
596                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
597                                   NIL(char));
598  if (AbsVertexReadType(aux1) == false_c) {
599    AbsVertexSetPolarity(aux1, !polarity);
600    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
601    AbsVertexSetType(aux1, not_c);
602    AbsVertexSetLeftKid(aux1, aux2);
603    AbsVertexSetParent(aux2, aux1);
604  }
605  else {
606    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
607  }
608 
609  /* Create the top most fixed point vertex */
610  aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
611                                   NIL(AbsVertexInfo_t), mainVarId,
612                                   NIL(char), NIL(char));
613  if (AbsVertexReadType(aux2) == false_c) {
614    AbsVertexSetPolarity(aux2, !polarity);
615    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
616    AbsVertexSetType(aux2, fixedPoint_c);
617    AbsVertexSetVarId(aux2, mainVarId);
618    AbsVertexSetLeftKid(aux2, aux1);
619    AbsVertexSetFpVar(aux2, mainVarVertex);
620    AbsVertexSetUseExtraCareSet(aux2, FALSE);
621    AbsVertexSetParent(aux1, aux2);
622  }
623  else {
624    AbsVertexSetUseExtraCareSet(aux2, FALSE);
625    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
626  }
627 
628  /* Create the top most vertex */
629  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
630                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
631                                   NIL(char));
632  if (AbsVertexReadType(aux1) == false_c) {
633    AbsVertexSetPolarity(aux1, polarity);
634    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
635    AbsVertexSetType(aux1, not_c);
636    AbsVertexSetLeftKid(aux1, aux2);
637    AbsVertexSetParent(aux2, aux1);
638  }
639  else {
640    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
641  }
642 
643  /* Clean up */
644  array_free(constraintArray);
645  arrayForEachItem(AbsVertexInfo_t *, conjunctions, i, vertexPtr) {
646    AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
647  }
648  array_free(conjunctions);
649
650  return aux1;
651} /* End of ComputeFairPredicate */
652
653/**Function********************************************************************
654
655  Synopsis [Computes the operational grarph representation of an atomic
656  predicate]
657
658  SideEffects        []
659
660  SeeAlso            [TranslateCtlSubFormula]
661
662******************************************************************************/
663static AbsVertexInfo_t *
664TranslateCtlID(
665  AbsVertexCatalog_t *catalog,
666  Ctlp_Formula_t *formula,             
667  int polarity)
668{
669  AbsVertexInfo_t *result;
670
671  result = AbsVertexCatalogFindOrAdd(catalog,
672                                     identifier_c,
673                                     polarity,
674                                     NIL(AbsVertexInfo_t),
675                                     NIL(AbsVertexInfo_t),
676                                     0,
677                                     Ctlp_FormulaReadVariableName(formula),
678                                     Ctlp_FormulaReadValueName(formula));
679  if (AbsVertexReadType(result) == false_c) {
680    AbsVertexSetPolarity(result, polarity);
681    AbsVertexSetDepth(result, 1);
682    AbsVertexSetType(result, identifier_c);
683    AbsVertexSetName(result, 
684                     util_strsav(Ctlp_FormulaReadVariableName(formula)));
685    AbsVertexSetValue(result,
686                      util_strsav(Ctlp_FormulaReadValueName(formula)));
687  }
688 
689  return result;
690} /* End of TranslateCtlID */
691
692/**Function********************************************************************
693
694  Synopsis [Computes the operational graph representation of a formula of the
695  form E(pUq)]
696
697  SideEffects        []
698
699  SeeAlso            [TranslateCtlSubFormula]
700
701******************************************************************************/
702static AbsVertexInfo_t *
703TranslateCtlEU(
704  AbsVertexCatalog_t *catalog,
705  Ctlp_Formula_t *formula,
706  array_t *fairArray,
707  AbsVertexInfo_t *fairPositive,
708  AbsVertexInfo_t *fairNegative,
709  int polarity,
710  int *uniqueIds)
711{
712  AbsVertexInfo_t *result;
713  AbsVertexInfo_t *leftResult;
714  AbsVertexInfo_t *rightResult;
715  AbsVertexInfo_t *aux1;
716  AbsVertexInfo_t *aux2;
717  AbsVertexInfo_t *aux3;
718  AbsVertexInfo_t *varVertex;
719  int variableId;
720 
721  /* Allocate a unique id for the fixed point */
722  variableId = (*uniqueIds)++;
723 
724  /* Create the vertex storing the fixed point variable */
725  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
726                                   NIL(AbsVertexInfo_t), 
727                                   NIL(AbsVertexInfo_t), variableId, 
728                                   NIL(char), NIL(char));
729  if (AbsVertexReadType(aux1) == false_c) {
730    AbsVertexSetPolarity(aux1, polarity);
731    AbsVertexSetDepth(aux1, 1);
732    AbsVertexSetType(aux1, variable_c);
733    AbsVertexSetVarId(aux1, variableId);
734  }
735  varVertex = aux1;
736 
737  /* Create the vertex storing the preimage sub-formula */
738  aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
739                                   aux1, NIL(AbsVertexInfo_t),
740                                   0, NIL(char), NIL(char));
741  if (AbsVertexReadType(aux2) == false_c) {
742    AbsVertexSetPolarity(aux2, polarity);
743    AbsVertexSetDepth(aux2, 2);
744    AbsVertexSetType(aux2, preImage_c);
745    AbsVertexSetLeftKid(aux2, aux1);
746    AbsVertexSetParent(aux1, aux2);
747  }
748  else {
749    /* Cache hit */
750    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
751  }
752 
753  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
754    /* Compute the value of the sub-formula */
755    leftResult = TranslateCtlSubFormula(catalog,
756                                        Ctlp_FormulaReadLeftChild(formula),
757                                        fairArray, fairPositive, fairNegative,
758                                        polarity, uniqueIds);
759   
760    /* Create the vertex representing the and */
761    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, aux2,
762                                     0, NIL(char), 
763                                     NIL(char));
764    if (AbsVertexReadType(aux1) == false_c) {
765      AbsVertexSetPolarity(aux1, polarity);
766      if (AbsVertexReadDepth(leftResult) > 2) {
767        AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
768      }
769      else {
770        AbsVertexSetDepth(aux1, 3);
771      }
772      AbsVertexSetType(aux1, and_c);
773      AbsVertexSetLeftKid(aux1, leftResult);
774      AbsVertexSetRightKid(aux1, aux2);
775      AbsVertexSetParent(leftResult, aux1);
776      AbsVertexSetParent(aux2, aux1);
777    }
778    else {
779      /* Cache hit */
780      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
781      AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
782    }
783  } /* if type is TRUE */
784  else {
785    aux1 = aux2;
786  }
787 
788  /* Create the not vertex on top of the conjunction */
789  aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
790                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
791                                   NIL(char));
792  if (AbsVertexReadType(aux2) == false_c) {
793    AbsVertexSetPolarity(aux2, !polarity);
794    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
795    AbsVertexSetType(aux2, not_c);
796    AbsVertexSetLeftKid(aux2, aux1);
797    AbsVertexSetParent(aux1, aux2);
798  }
799  else {
800    /* Cache hit */
801    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
802  }
803 
804  /* Evaluate the right operand of the EU */
805  rightResult= TranslateCtlSubFormula(catalog,
806                                      Ctlp_FormulaReadRightChild(formula),
807                                      fairArray, fairPositive, fairNegative,
808                                      polarity, uniqueIds);
809 
810  /* check if there are fairness constraints */
811  if (fairPositive != NIL(AbsVertexInfo_t)) {
812    AbsVertexInfo_t *fairness;
813    AbsVertexInfo_t *conjunction;
814
815    /* The negative polarity version of the fairness must be present as well */
816    assert(fairNegative != NIL(AbsVertexInfo_t));
817
818    /* Select the apropriate representation of the fairness constraint */
819    if (polarity) {
820      fairness = fairPositive;
821    }
822    else {
823      fairness = fairNegative;
824    }
825    AbsVertexReadRefs(fairness)++;
826
827    conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
828                                            rightResult, fairness, 0, NIL(char),
829                                            NIL(char));
830
831    if (AbsVertexReadType(conjunction) == false_c) {
832      int leftDepth;
833      int rightDepth;
834
835      leftDepth = AbsVertexReadDepth(rightResult);
836      rightDepth = AbsVertexReadDepth(fairness);
837
838      AbsVertexSetPolarity(conjunction, polarity);
839      if (leftDepth > rightDepth) {
840        AbsVertexSetDepth(conjunction, leftDepth + 1);
841      }
842      else {
843        AbsVertexSetDepth(conjunction, rightDepth + 1);
844      }
845      AbsVertexSetType(conjunction, and_c);
846      AbsVertexSetLeftKid(conjunction, rightResult);
847      AbsVertexSetRightKid(conjunction, fairness);
848      AbsVertexSetParent(rightResult, conjunction);
849      AbsVertexSetParent(fairness, conjunction);
850    }
851    else {
852      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
853      AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
854    }
855    rightResult = conjunction;
856  }
857
858  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
859  if (AbsVertexReadType(rightResult) == not_c) {
860    AbsVertexInfo_t *newResult;
861
862
863    newResult = AbsVertexReadLeftKid(rightResult);
864    AbsVertexReadRefs(newResult)++;
865    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
866    aux1 = newResult;
867  }
868  else {
869    /* Vertex negating second operand */
870    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
871                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
872                                     NIL(char));
873    if (AbsVertexReadType(aux1) == false_c) {
874      AbsVertexSetPolarity(aux1, !polarity);
875      AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
876      AbsVertexSetType(aux1, not_c);
877      AbsVertexSetLeftKid(aux1, rightResult);
878      AbsVertexSetParent(rightResult, aux1);
879    }
880    else {
881      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
882    }
883  }
884 
885  /* Vertex taking the conjunction */
886  aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
887                                   0, NIL(char), NIL(char));
888  if (AbsVertexReadType(aux3) == false_c) {
889    AbsVertexSetPolarity(aux3, !polarity);
890    if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
891      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
892    }
893    else {
894      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
895    }
896    AbsVertexSetType(aux3, and_c);
897    AbsVertexSetLeftKid(aux3, aux1);
898    AbsVertexSetRightKid(aux3, aux2);
899    AbsVertexSetParent(aux1, aux3);
900    AbsVertexSetParent(aux2, aux3);
901  }
902  else {
903    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
904    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
905  }
906 
907  /* negation of the conjunction */
908  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
909                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
910                                   NIL(char));
911  if (AbsVertexReadType(aux1) == false_c) {
912    AbsVertexSetPolarity(aux1, polarity);
913    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
914    AbsVertexSetType(aux1, not_c);
915    AbsVertexSetLeftKid(aux1, aux3);
916    AbsVertexSetParent(aux3, aux1);
917  }
918  else {
919    AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
920  }
921 
922  /* Top vertex fixed point operator */
923  result = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux1,
924                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
925                                     NIL(char));
926  if (AbsVertexReadType(result) == false_c) {
927    AbsVertexSetPolarity(result, polarity);
928    AbsVertexSetDepth(result, AbsVertexReadDepth(aux1) + 1);
929    AbsVertexSetType(result, fixedPoint_c);
930    AbsVertexSetLeftKid(result, aux1);
931    AbsVertexSetFpVar(result, varVertex);
932    AbsVertexSetUseExtraCareSet(result, TRUE);
933    AbsVertexSetParent(aux1, result);
934  }
935  else {
936    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
937  }
938 
939  return result;
940} /* End of TranslateCtlEU */
941
942/**Function********************************************************************
943
944  Synopsis [Computes the operational graph representation of a formula of the
945  form EG(p)]
946
947  SideEffects        []
948
949  SeeAlso            [TranslateCtlSubFormula]
950
951******************************************************************************/
952static AbsVertexInfo_t *
953TranslateCtlEG(
954  AbsVertexCatalog_t *catalog,
955  Ctlp_Formula_t *formula,
956  int polarity,
957  int *uniqueIds)
958{
959  AbsVertexInfo_t *result;
960  AbsVertexInfo_t *varVertex;
961  AbsVertexInfo_t *aux1;
962  AbsVertexInfo_t *aux2;
963  AbsVertexInfo_t *childResult;
964  int variableId;
965 
966  /* Allocate a unique id for the fixed point */
967  variableId = (*uniqueIds)++;
968 
969  /* Create the vertex storing the fixed point variable */
970  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity,
971                                   NIL(AbsVertexInfo_t), 
972                                   NIL(AbsVertexInfo_t),
973                                   variableId, NIL(char), NIL(char));
974  if (AbsVertexReadType(aux1) == false_c) {
975    AbsVertexSetPolarity(aux1, !polarity);
976    AbsVertexSetDepth(aux1, 1);
977    AbsVertexSetType(aux1, variable_c);
978    AbsVertexSetVarId(aux1, variableId);
979  }
980  varVertex = aux1;
981 
982  /* Create the vertex to negate the variable of the fixed point */
983  aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1, 
984                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
985                                   NIL(char));
986  if (AbsVertexReadType(aux2) == false_c) {
987    AbsVertexSetPolarity(aux2, polarity);
988    AbsVertexSetDepth(aux2, 2);
989    AbsVertexSetType(aux2, not_c);
990    AbsVertexSetLeftKid(aux2, aux1);
991    AbsVertexSetParent(aux1, aux2);
992  }
993  else {
994    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
995  }
996
997  /* Create the vertex storing the preimage sub-formula */
998  aux1 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
999                                   aux1, NIL(AbsVertexInfo_t),
1000                                   0, NIL(char), NIL(char));
1001  if (AbsVertexReadType(aux1) == false_c) {
1002    AbsVertexSetPolarity(aux1, polarity);
1003    AbsVertexSetDepth(aux1, 3);
1004    AbsVertexSetType(aux1, preImage_c);
1005    AbsVertexSetLeftKid(aux1, aux2);
1006    AbsVertexSetParent(aux2, aux1);
1007  }
1008  else {
1009    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1010  }
1011 
1012  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
1013    /* Create the vertex representing the sub-formula of EG */
1014    childResult = TranslateCtlSubFormula(catalog, 
1015                                         Ctlp_FormulaReadLeftChild(formula),
1016                                         NIL(array_t), NIL(AbsVertexInfo_t), 
1017                                         NIL(AbsVertexInfo_t), polarity, 
1018                                         uniqueIds);
1019   
1020    /* Create the vertex representing the and */
1021    aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, childResult, 
1022                                     aux1, 0, NIL(char), 
1023                                     NIL(char));
1024    if (AbsVertexReadType(aux2) == false_c) {
1025      AbsVertexSetPolarity(aux2, polarity);
1026      if (AbsVertexReadDepth(childResult) > 2) {
1027        AbsVertexSetDepth(aux2, AbsVertexReadDepth(childResult) + 1);
1028      }
1029      else {
1030        AbsVertexSetDepth(aux2, 4);
1031      }
1032      AbsVertexSetType(aux2, and_c);
1033      AbsVertexSetLeftKid(aux2, childResult);
1034      AbsVertexSetRightKid(aux2, aux1);
1035      AbsVertexSetParent(childResult, aux2);
1036      AbsVertexSetParent(aux1, aux2);
1037    }
1038    else {
1039      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1040      AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
1041    }
1042  }
1043  else {
1044    aux2 = aux1;
1045  }
1046 
1047  /* Create the not vertex on top of the conjunction */
1048  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
1049                                   NIL(AbsVertexInfo_t), 0, NIL(char), 
1050                                   NIL(char));
1051  if (AbsVertexReadType(aux1) == false_c) {
1052    AbsVertexSetPolarity(aux1, !polarity);
1053    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
1054    AbsVertexSetType(aux1, not_c);
1055    AbsVertexSetLeftKid(aux1, aux2);
1056    AbsVertexSetParent(aux2, aux1);
1057  }
1058  else {
1059    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
1060  }
1061 
1062  /* Create the fixedpoint_c vertex */
1063  aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
1064                                   NIL(AbsVertexInfo_t), variableId,
1065                                   NIL(char), NIL(char));
1066  if (AbsVertexReadType(aux2) == false_c) {
1067    AbsVertexSetPolarity(aux2, !polarity);
1068    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
1069    AbsVertexSetType(aux2, fixedPoint_c);
1070    AbsVertexSetVarId(aux2, variableId);
1071    AbsVertexSetLeftKid(aux2, aux1);
1072    AbsVertexSetFpVar(aux2, varVertex);
1073    AbsVertexSetUseExtraCareSet(aux2, FALSE);
1074    AbsVertexSetParent(aux1, aux2);
1075  }
1076  else {
1077    AbsVertexSetUseExtraCareSet(aux2, FALSE);
1078    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1079  }
1080 
1081  /* Create the top most not vertex  */
1082  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
1083                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1084                                     NIL(char));
1085  if (AbsVertexReadType(result) == false_c) {
1086    AbsVertexSetPolarity(result, polarity);
1087    AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
1088    AbsVertexSetType(result, not_c);
1089    AbsVertexSetLeftKid(result, aux2);
1090    AbsVertexSetParent(aux2, result);
1091  }
1092  else {
1093    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
1094  }
1095 
1096  return result;
1097} /* End of TranslateCtlEG */
1098
1099/**Function********************************************************************
1100
1101  Synopsis [Computes the operational graph representation of a predicate of the
1102  form EGfair(f)]
1103
1104  SideEffects        []
1105
1106  SeeAlso            [TranslateCtlSubFormula]
1107
1108******************************************************************************/
1109static AbsVertexInfo_t *
1110TranslateCtlEGFair(
1111  AbsVertexCatalog_t *catalog,
1112  Ctlp_Formula_t *formula,
1113  array_t *fairArray,
1114  AbsVertexInfo_t *fairPositive,
1115  AbsVertexInfo_t *fairNegative,
1116  int polarity,
1117  int *uniqueIds)
1118{
1119  AbsVertexInfo_t *result;
1120  AbsVertexInfo_t *childResult;
1121
1122  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) == Ctlp_TRUE_c) {
1123    if (polarity) {
1124      result = fairPositive;
1125      AbsVertexReadRefs(fairPositive)++;
1126    }
1127    else {
1128      result = fairNegative;
1129      AbsVertexReadRefs(fairNegative)++;
1130    }
1131  }
1132  else {
1133    childResult = TranslateCtlSubFormula(catalog,
1134                                         Ctlp_FormulaReadLeftChild(formula),
1135                                         fairArray, fairPositive, fairNegative,
1136                                         polarity, uniqueIds);
1137
1138    result = ComputeFairPredicate(catalog, childResult, fairArray, polarity,
1139                                  uniqueIds);
1140  }
1141
1142  return result;
1143} /* End of TranslateCtlEGFair */
1144
1145/**Function********************************************************************
1146
1147  Synopsis [Computes the operational graph representation of the predicate
1148  EX(p)]
1149
1150  SideEffects        []
1151
1152  SeeAlso            [TranslateCtlSubFormula]
1153
1154******************************************************************************/
1155static AbsVertexInfo_t *
1156TranslateCtlEX(
1157  AbsVertexCatalog_t *catalog,
1158  Ctlp_Formula_t *formula,
1159  array_t *fairArray,
1160  AbsVertexInfo_t *fairPositive,
1161  AbsVertexInfo_t *fairNegative,
1162  int polarity,
1163  int *uniqueIds)
1164{
1165  AbsVertexInfo_t *result;
1166  AbsVertexInfo_t *childResult;
1167 
1168  /* Translate the sub-formula regardless */
1169  childResult = TranslateCtlSubFormula(catalog,
1170                                       Ctlp_FormulaReadLeftChild(formula),
1171                                       fairArray, fairPositive, fairNegative,
1172                                       polarity, uniqueIds);
1173 
1174  /* check if there are fairness constraints */
1175  if (fairPositive != NIL(AbsVertexInfo_t)) {
1176    AbsVertexInfo_t *fairness;
1177    AbsVertexInfo_t *conjunction;
1178
1179    /* The negative polarity version of the fairness must be present as well */
1180    assert(fairNegative != NIL(AbsVertexInfo_t));
1181
1182    /* Select the apropriate representation of the fairness constraint */
1183    if (polarity) {
1184      fairness = fairPositive;
1185    }
1186    else {
1187      fairness = fairNegative;
1188    }
1189    AbsVertexReadRefs(fairness)++;
1190
1191    conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
1192                                            childResult, fairness, 0, NIL(char),
1193                                            NIL(char));
1194
1195    if (AbsVertexReadType(conjunction) == false_c) {
1196      int leftDepth;
1197      int rightDepth;
1198
1199      leftDepth = AbsVertexReadDepth(childResult);
1200      rightDepth = AbsVertexReadDepth(fairness);
1201
1202      AbsVertexSetPolarity(conjunction, polarity);
1203      if (leftDepth > rightDepth) {
1204        AbsVertexSetDepth(conjunction, leftDepth + 1);
1205      }
1206      else {
1207        AbsVertexSetDepth(conjunction, rightDepth + 1);
1208      }
1209      AbsVertexSetType(conjunction, and_c);
1210      AbsVertexSetLeftKid(conjunction, childResult);
1211      AbsVertexSetRightKid(conjunction, fairness);
1212      AbsVertexSetParent(childResult, conjunction);
1213      AbsVertexSetParent(fairness, conjunction);
1214    }
1215    else {
1216      AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
1217      AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
1218    }
1219    childResult = conjunction;
1220  }
1221
1222  /* Create the preImage vertex */
1223  result = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity, 
1224                                     childResult, NIL(AbsVertexInfo_t), 0, 
1225                                     NIL(char), NIL(char));
1226  if (AbsVertexReadType(result) == false_c) {
1227    AbsVertexSetPolarity(result, polarity);
1228    AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
1229    AbsVertexSetType(result, preImage_c);
1230    AbsVertexSetLeftKid(result, childResult);
1231    AbsVertexSetParent(childResult, result);
1232  }
1233  else {
1234    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
1235  }
1236                                                           
1237  return result;
1238} /* End of TranslateCtlEX */
1239
1240/**Function********************************************************************
1241
1242  Synopsis [Computes the operational graph representation of the predicate
1243  NOT(p)]
1244
1245  SideEffects        []
1246
1247  SeeAlso            [TranslateCtlSubFormula]
1248
1249******************************************************************************/
1250static AbsVertexInfo_t *
1251TranslateCtlNOT(
1252  AbsVertexCatalog_t *catalog,
1253  Ctlp_Formula_t *formula,
1254  array_t *fairArray,
1255  AbsVertexInfo_t *fairPositive,
1256  AbsVertexInfo_t *fairNegative,
1257  int polarity,
1258  int *uniqueIds)
1259{
1260  AbsVertexInfo_t *result;
1261  AbsVertexInfo_t *childResult;
1262 
1263  childResult = TranslateCtlSubFormula(catalog,
1264                                       Ctlp_FormulaReadLeftChild(formula),
1265                                       fairArray, fairPositive, fairNegative,
1266                                       !polarity, uniqueIds);
1267 
1268  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
1269  if (AbsVertexReadType(childResult) == not_c) {
1270    AbsVertexInfo_t *newResult;
1271
1272    newResult = AbsVertexReadLeftKid(childResult);
1273    AbsVertexReadRefs(newResult)++;
1274    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
1275   
1276    return newResult;
1277  }
1278
1279  /* Create the not vertex */
1280  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, childResult,
1281                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1282                                     NIL(char));
1283  if (AbsVertexReadType(result) == false_c) {
1284    AbsVertexSetPolarity(result, polarity);
1285    AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
1286    AbsVertexSetType(result, not_c);
1287    AbsVertexSetLeftKid(result, childResult);
1288    AbsVertexSetParent(childResult, result);
1289  }
1290  else {
1291    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
1292  }
1293 
1294  return result;
1295} /* End of TranslateCtlNOT */
1296
1297/**Function********************************************************************
1298
1299  Synopsis [Computes the operational graph representation of the predicate
1300  of the form p -> q]
1301
1302  SideEffects        []
1303
1304  SeeAlso            [TranslateCtlSubFormula]
1305
1306******************************************************************************/
1307static AbsVertexInfo_t *
1308TranslateCtlTHEN(
1309  AbsVertexCatalog_t *catalog,
1310  Ctlp_Formula_t *formula,
1311  array_t *fairArray,
1312  AbsVertexInfo_t *fairPositive,
1313  AbsVertexInfo_t *fairNegative,
1314  int polarity,
1315  int *uniqueIds)
1316{
1317  AbsVertexInfo_t *result;
1318  AbsVertexInfo_t *leftResult, *rightResult;
1319  AbsVertexInfo_t *aux1;
1320  AbsVertexInfo_t *aux2;
1321 
1322  leftResult = TranslateCtlSubFormula(catalog,
1323                                      Ctlp_FormulaReadLeftChild(formula),
1324                                      fairArray, fairPositive, fairNegative,
1325                                      !polarity, uniqueIds);
1326  rightResult= TranslateCtlSubFormula(catalog,
1327                                      Ctlp_FormulaReadRightChild(formula),
1328                                      fairArray, fairPositive, fairNegative,
1329                                      polarity, uniqueIds);
1330 
1331  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
1332  if (AbsVertexReadType(rightResult) == not_c) {
1333    AbsVertexInfo_t *newResult;
1334
1335    newResult = AbsVertexReadLeftKid(rightResult);
1336    AbsVertexReadRefs(newResult)++;
1337    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
1338    aux1 = newResult;
1339  }
1340  else {
1341    /* Vertex negating first operand */
1342    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
1343                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1344                                     NIL(char));
1345    if (AbsVertexReadType(aux1) == false_c) {
1346      AbsVertexSetPolarity(aux1, !polarity);
1347      AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
1348      AbsVertexSetType(aux1, not_c);
1349      AbsVertexSetLeftKid(aux1, rightResult);
1350      AbsVertexSetParent(rightResult, aux1);
1351    }
1352    else {
1353      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
1354    }
1355  }
1356 
1357  /* Result node holding the and of both operands */
1358  aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, leftResult, 
1359                                   aux1, 0, NIL(char), NIL(char));
1360  if (AbsVertexReadType(aux2) == false_c) {
1361    AbsVertexSetPolarity(aux2, !polarity);
1362    if (AbsVertexReadDepth(leftResult) > AbsVertexReadDepth(aux1)) {
1363      AbsVertexSetDepth(aux2, AbsVertexReadDepth(leftResult) + 1);
1364    }
1365    else {
1366      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
1367    }
1368    AbsVertexSetType(aux2, and_c);
1369    AbsVertexSetLeftKid(aux2, leftResult);
1370    AbsVertexSetRightKid(aux2, aux1);
1371    AbsVertexSetParent(aux1, aux2);
1372    AbsVertexSetParent(leftResult, aux2);
1373  }
1374  else {
1375    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
1376    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1377  }
1378 
1379  /* Top vertex negation of the conjunction */
1380  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
1381                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1382                                     NIL(char));
1383  if (AbsVertexReadType(result) == false_c) {
1384    AbsVertexSetPolarity(result, polarity);
1385    AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
1386    AbsVertexSetType(result, not_c);
1387    AbsVertexSetLeftKid(result, aux2);
1388    AbsVertexSetParent(aux2, result);
1389  }
1390  else {
1391    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
1392  }
1393 
1394  return result;
1395} /* End of TranslateCtlTHEN */
1396
1397/**Function********************************************************************
1398
1399  Synopsis [Computes the operational graph representation of the predicate of
1400  the form p AND q]
1401
1402  SideEffects        []
1403
1404  SeeAlso            [TranslateCtlSubFormula]
1405
1406******************************************************************************/
1407static AbsVertexInfo_t *
1408TranslateCtlAND(
1409  AbsVertexCatalog_t *catalog,
1410  Ctlp_Formula_t *formula,
1411  array_t *fairArray,
1412  AbsVertexInfo_t *fairPositive,
1413  AbsVertexInfo_t *fairNegative,
1414  int polarity,
1415  int *uniqueIds)
1416{
1417  AbsVertexInfo_t *result;
1418  AbsVertexInfo_t *leftResult, *rightResult;
1419  int leftDepth;
1420  int rightDepth;
1421 
1422  leftResult = TranslateCtlSubFormula(catalog,
1423                                      Ctlp_FormulaReadLeftChild(formula),
1424                                      fairArray, fairPositive, fairNegative,
1425                                      polarity, uniqueIds);
1426  rightResult= TranslateCtlSubFormula(catalog,
1427                                      Ctlp_FormulaReadRightChild(formula),
1428                                      fairArray, fairPositive, fairNegative,
1429                                      polarity, uniqueIds);
1430 
1431  /* Read the depths */
1432  leftDepth = AbsVertexReadDepth(leftResult);
1433  rightDepth = AbsVertexReadDepth(rightResult);
1434 
1435  result = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, 
1436                                     rightResult, 0, NIL(char), NIL(char));
1437  if (AbsVertexReadType(result) == false_c) {
1438    AbsVertexSetPolarity(result, polarity);
1439    if (leftDepth > rightDepth) {
1440      AbsVertexSetDepth(result, leftDepth + 1);
1441    }
1442    else {
1443      AbsVertexSetDepth(result, rightDepth + 1);
1444    }
1445    AbsVertexSetType(result, and_c);
1446    AbsVertexSetLeftKid(result, leftResult);
1447    AbsVertexSetRightKid(result, rightResult);
1448    AbsVertexSetParent(leftResult, result);
1449    AbsVertexSetParent(rightResult, result);
1450  }
1451  else {
1452    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
1453    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
1454  }
1455 
1456  return result;
1457} /* End of TranslateCtlAND */
1458
1459/**Function********************************************************************
1460
1461  Synopsis [Computes the operational graph representation of the predicate of
1462   the for p OR q]
1463
1464  SideEffects        []
1465
1466  SeeAlso            [TranslateCtlSubFormula]
1467
1468******************************************************************************/
1469static AbsVertexInfo_t *
1470TranslateCtlOR(
1471  AbsVertexCatalog_t *catalog,
1472  Ctlp_Formula_t *formula,
1473  array_t *fairArray,
1474  AbsVertexInfo_t *fairPositive,
1475  AbsVertexInfo_t *fairNegative,
1476  int polarity,
1477  int *uniqueIds)
1478{
1479  AbsVertexInfo_t *result;
1480  AbsVertexInfo_t *leftResult, *rightResult;
1481  AbsVertexInfo_t *aux1;
1482  AbsVertexInfo_t *aux2;
1483  AbsVertexInfo_t *aux3;
1484 
1485  leftResult = TranslateCtlSubFormula(catalog,
1486                                      Ctlp_FormulaReadLeftChild(formula),
1487                                      fairArray, fairPositive, fairNegative,
1488                                      polarity, uniqueIds);
1489  rightResult= TranslateCtlSubFormula(catalog,
1490                                      Ctlp_FormulaReadRightChild(formula),
1491                                      fairArray, fairPositive, fairNegative,
1492                                      polarity, uniqueIds);
1493 
1494  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
1495  if (AbsVertexReadType(leftResult) == not_c) {
1496    AbsVertexInfo_t *newResult;
1497
1498    newResult = AbsVertexReadLeftKid(leftResult);
1499    AbsVertexReadRefs(newResult)++;
1500    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
1501    aux1 = newResult;
1502  }
1503  else {
1504    /* Vertex negating first operand */
1505    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, leftResult, 
1506                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1507                                     NIL(char));
1508    if (AbsVertexReadType(aux1) == false_c) {
1509      AbsVertexSetPolarity(aux1, !polarity);
1510      AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
1511      AbsVertexSetType(aux1, not_c);
1512      AbsVertexSetLeftKid(aux1, leftResult);
1513      AbsVertexSetParent(leftResult, aux1);
1514    }
1515    else {
1516      AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
1517    }
1518  }
1519 
1520  if (AbsVertexReadType(rightResult) == not_c) {
1521    AbsVertexInfo_t *newResult;
1522
1523    newResult = AbsVertexReadLeftKid(rightResult);
1524    AbsVertexReadRefs(newResult)++;
1525    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
1526    aux2 = newResult;
1527  }
1528  else {
1529    /* Vertex negating second operand */
1530    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
1531                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1532                                     NIL(char));
1533    if (AbsVertexReadType(aux2) == false_c) {
1534      AbsVertexSetPolarity(aux2, !polarity);
1535      AbsVertexSetDepth(aux2, AbsVertexReadDepth(rightResult) + 1);
1536      AbsVertexSetType(aux2, not_c);
1537      AbsVertexSetLeftKid(aux2, rightResult);
1538      AbsVertexSetParent(rightResult, aux2);
1539    }
1540    else {
1541      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
1542    }
1543  }
1544 
1545  /* Vertex taking the conjunction */
1546  aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
1547                                   0, NIL(char), NIL(char));
1548  if (AbsVertexReadType(aux3) == false_c) {
1549    AbsVertexSetPolarity(aux3, !polarity);
1550    if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
1551      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
1552    }
1553    else {
1554      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
1555    }
1556    AbsVertexSetType(aux3, and_c);
1557    AbsVertexSetLeftKid(aux3, aux1);
1558    AbsVertexSetRightKid(aux3, aux2);
1559    AbsVertexSetParent(aux1, aux3);
1560    AbsVertexSetParent(aux2, aux3);
1561  }
1562  else {
1563    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1564    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
1565  }
1566 
1567  /* Top vertex negation of the conjunction */
1568  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
1569                                     NIL(AbsVertexInfo_t), 0, NIL(char), 
1570                                     NIL(char));
1571  if (AbsVertexReadType(result) == false_c) {
1572    AbsVertexSetPolarity(result, polarity);
1573    AbsVertexSetDepth(result, AbsVertexReadDepth(aux3) + 1);
1574    AbsVertexSetType(result, not_c);
1575    AbsVertexSetLeftKid(result, aux3);
1576    AbsVertexSetParent(aux3, result);
1577  }
1578  else {
1579    AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
1580  }
1581 
1582  return result;
1583} /* End of TranslateCtlOR */
1584
1585/**Function********************************************************************
1586
1587  Synopsis [Given an array containing vertices, creates the conjunction of all
1588  of them.]
1589
1590  SideEffects        []
1591
1592  SeeAlso            [ComputeFairPredicate]
1593
1594******************************************************************************/
1595static AbsVertexInfo_t *
1596CreateConjunctionChain(
1597  AbsVertexCatalog_t *catalog,
1598  array_t *conjunctions,
1599  int polarity)
1600{
1601  AbsVertexInfo_t *aux1;
1602  AbsVertexInfo_t *aux2;
1603  AbsVertexInfo_t *aux3;
1604  int i;
1605
1606  assert(conjunctions != NIL(array_t));
1607
1608  aux1 = array_fetch(AbsVertexInfo_t *, conjunctions, 0);
1609  AbsVertexReadRefs(aux1)++;
1610
1611  if (array_n(conjunctions) == 1) {
1612    return aux1;
1613  }
1614
1615  for (i=1; i<array_n(conjunctions); i++) {
1616    aux2 = array_fetch(AbsVertexInfo_t *, conjunctions, i);
1617    AbsVertexReadRefs(aux2)++;
1618   
1619    aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, aux1, aux2, 0,
1620                                     NIL(char), NIL(char));
1621
1622    if (AbsVertexReadType(aux3) == false_c) {
1623      AbsVertexSetPolarity(aux3, polarity);
1624      if (AbsVertexReadDepth(aux1) < AbsVertexReadDepth(aux2)) {
1625        AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
1626      }
1627      else {
1628        AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
1629      }
1630      AbsVertexSetType(aux3, and_c);
1631      AbsVertexSetLeftKid(aux3, aux1);
1632      AbsVertexSetRightKid(aux3, aux2);
1633      AbsVertexSetParent(aux1, aux3);
1634      AbsVertexSetParent(aux2, aux3);
1635    }
1636    else {
1637      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
1638      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
1639    }
1640
1641    aux1 = aux3;
1642  }
1643
1644  return aux1;
1645} /* End of CreateConjunctionChain */
Note: See TracBrowser for help on using the repository browser.