VIS

src/abs/absTranslate.c

Go to the documentation of this file.
00001 
00018 #include "absInt.h" 
00019 
00020 static char rcsid[] UNUSED = "$Id: absTranslate.c,v 1.14 2002/09/04 14:58:18 fabio Exp $";
00021 
00022 
00023 /*---------------------------------------------------------------------------*/
00024 /* Macro declarations                                                        */
00025 /*---------------------------------------------------------------------------*/
00026 
00027 
00030 /*---------------------------------------------------------------------------*/
00031 /* Static function prototypes                                                */
00032 /*---------------------------------------------------------------------------*/
00033 
00034 static AbsVertexInfo_t * TranslateCtlSubFormula(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00035 static AbsVertexInfo_t * ComputeFairPredicate(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *atomicPredicate, array_t *fairArray, int polarity, int *uniqueIds);
00036 static AbsVertexInfo_t * TranslateCtlID(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity);
00037 static AbsVertexInfo_t * TranslateCtlEU(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00038 static AbsVertexInfo_t * TranslateCtlEG(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity, int *uniqueIds);
00039 static AbsVertexInfo_t * TranslateCtlEGFair(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00040 static AbsVertexInfo_t * TranslateCtlEX(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00041 static AbsVertexInfo_t * TranslateCtlNOT(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00042 static AbsVertexInfo_t * TranslateCtlTHEN(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00043 static AbsVertexInfo_t * TranslateCtlAND(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00044 static AbsVertexInfo_t * TranslateCtlOR(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
00045 static AbsVertexInfo_t * CreateConjunctionChain(AbsVertexCatalog_t *catalog, array_t *conjunctions, int polarity);
00046 
00050 /*---------------------------------------------------------------------------*/
00051 /* Definition of exported functions                                          */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Definition of internal functions                                          */
00056 /*---------------------------------------------------------------------------*/
00057 
00068 array_t *
00069 AbsCtlFormulaArrayTranslate(
00070   Abs_VerificationInfo_t *verInfo,
00071   array_t *formulaArray,
00072   array_t *fairArray)
00073 {
00074   AbsVertexCatalog_t *catalog;
00075   Ctlp_Formula_t  *formulaPtr;
00076   AbsVertexInfo_t *fairPositive;
00077   AbsVertexInfo_t *fairNegative;
00078   array_t         *result;
00079   boolean         initialPolarity;
00080   int             uniqueIds;
00081   int             i;
00082 
00083   if (formulaArray == NIL(array_t)) {
00084     return NIL(array_t);
00085   }
00086 
00087   /* Initialize certain variables */
00088   catalog = AbsVerificationInfoReadCatalog(verInfo);
00089   uniqueIds = 0;
00090 
00091   if (fairArray != NIL(array_t)) {
00092     fairPositive = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t),
00093                                         fairArray, TRUE, &uniqueIds);
00094 
00095     fairNegative = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t), 
00096                                         fairArray, FALSE, &uniqueIds);
00097   }
00098   else {
00099     fairPositive = NIL(AbsVertexInfo_t);
00100     fairNegative = NIL(AbsVertexInfo_t);
00101   }
00102 
00103   if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
00104     initialPolarity = TRUE;
00105   }
00106   else {
00107     initialPolarity = FALSE;
00108   }
00109 
00110   /* Create the result */
00111   result = array_alloc(AbsVertexInfo_t *, array_n(formulaArray));
00112 
00113   arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formulaPtr) {
00114     AbsVertexInfo_t *resultPtr;
00115 
00116     /* Translate the formula */
00117     resultPtr = TranslateCtlSubFormula(AbsVerificationInfoReadCatalog(verInfo),
00118                                        formulaPtr,      /* Formula */
00119                                        fairArray,       /* Fairness 
00120                                                            constraints */
00121                                        fairPositive,    /* Predicate fair 
00122                                                            with positive 
00123                                                            polarity */
00124                                        fairNegative,    /* Predicate fair
00125                                                            with negative
00126                                                            polarity */
00127                                        initialPolarity, /* Initial polarity */
00128                                        &uniqueIds);     /* Unique id counter */
00129 
00130     /* Negate the formula if needed */
00131     if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
00132       AbsVertexInfo_t *newResult;
00133 
00134       /* If the formula's top vertex is a negation, eliminate the redundancy */
00135       if (AbsVertexReadType(resultPtr) == not_c) {
00136         
00137         newResult = AbsVertexReadLeftKid(resultPtr);
00138         AbsVertexReadRefs(newResult)++;
00139         AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
00140         
00141         resultPtr =  newResult;
00142       }
00143       else {
00144         /* Create the not vertex */
00145         newResult = AbsVertexCatalogFindOrAdd(catalog, not_c, FALSE, 
00146                                               resultPtr,
00147                                               NIL(AbsVertexInfo_t), 0, 
00148                                               NIL(char), 
00149                                               NIL(char));
00150         if (AbsVertexReadType(newResult) == false_c) {
00151           AbsVertexSetPolarity(newResult, FALSE);
00152           AbsVertexSetDepth(newResult, AbsVertexReadDepth(resultPtr) + 1);
00153           AbsVertexSetType(newResult, not_c);
00154           AbsVertexSetLeftKid(newResult, resultPtr);
00155           AbsVertexSetParent(resultPtr, newResult);
00156         }
00157         else {
00158           AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
00159         }
00160         resultPtr = newResult;
00161       }
00162     } /* If the formula needs to be negated */
00163 
00164     /* Set the constant bit */
00165     AbsFormulaSetConstantBit(resultPtr);
00166 
00167     array_insert(AbsVertexInfo_t *, result, i, resultPtr);
00168   }
00169 
00170   /* Clean up */
00171   if (fairPositive != NIL(AbsVertexInfo_t)) {
00172     AbsVertexFree(catalog, fairPositive, NIL(AbsVertexInfo_t));
00173   }
00174   if (fairNegative != NIL(AbsVertexInfo_t)) {
00175     AbsVertexFree(catalog, fairNegative, NIL(AbsVertexInfo_t));
00176   }
00177 
00178 #ifndef NDEBUG
00179   {
00180     AbsVertexInfo_t *operationGraph;
00181     st_table *rootTable = st_init_table(st_ptrcmp, st_ptrhash);
00182     arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
00183       st_insert(rootTable, (char *) operationGraph, NIL(char));
00184     }
00185     arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
00186       assert(AbsFormulaSanityCheck(operationGraph, rootTable));
00187     }
00188     st_free_table(rootTable);
00189   }
00190 #endif
00191 
00192   return result;
00193 } /* End of AbsCtlFormulaArrayTranslate */
00194 
00195 
00196 /*---------------------------------------------------------------------------*/
00197 /* Definition of static functions                                            */
00198 /*---------------------------------------------------------------------------*/
00199 
00214 static AbsVertexInfo_t *
00215 TranslateCtlSubFormula(
00216   AbsVertexCatalog_t *catalog,
00217   Ctlp_Formula_t *formula,
00218   array_t *fairArray,
00219   AbsVertexInfo_t *fairPositive,
00220   AbsVertexInfo_t *fairNegative,
00221   int polarity,
00222   int *uniqueIds)
00223 {
00224   AbsVertexInfo_t *result;
00225 
00226   result = NIL(AbsVertexInfo_t);
00227 
00228   switch (Ctlp_FormulaReadType(formula)) {
00229     case Ctlp_TRUE_c:
00230     case Ctlp_FALSE_c: {
00231       (void) fprintf(vis_stderr, "** abs error: Error in TranslateCtlSubFormula. ");
00232       (void) fprintf(vis_stderr, "TRUE/FALSE constant found.\n");
00233       result = NIL(AbsVertexInfo_t);
00234       break;
00235     }
00236     case Ctlp_ID_c: {
00237       result = TranslateCtlID(catalog, formula, polarity);
00238       break;
00239     }
00240     case Ctlp_EG_c: {
00241       if (fairArray == NIL(array_t)) {
00242         result = TranslateCtlEG(catalog, formula, polarity, uniqueIds);
00243       }
00244       else {
00245         result = TranslateCtlEGFair(catalog, formula, fairArray, fairPositive, 
00246                                     fairNegative, polarity, uniqueIds);
00247       }
00248       break;
00249     }
00250     case Ctlp_EU_c: {
00251       result = TranslateCtlEU(catalog, formula, fairArray, fairPositive, 
00252                               fairNegative, polarity, uniqueIds);
00253       break;
00254     }
00255     case Ctlp_EX_c: {
00256       result = TranslateCtlEX(catalog, formula, fairArray, fairPositive, 
00257                               fairNegative, polarity, uniqueIds);
00258       break;
00259     }
00260     case Ctlp_NOT_c: {
00261       result = TranslateCtlNOT(catalog, formula, fairArray, fairPositive, 
00262                                fairNegative, polarity, uniqueIds);
00263       break;
00264     }
00265     case Ctlp_THEN_c:  {
00266       result = TranslateCtlTHEN(catalog, formula, fairArray, fairPositive, 
00267                                 fairNegative, polarity, uniqueIds);
00268       break;
00269     }
00270     case Ctlp_EQ_c:
00271     case Ctlp_XOR_c: {
00272       /* Non-monotonic operators should have been replaced before
00273        * reaching this point.
00274        */
00275       fail("Encountered unexpected type of CTL formula\n");
00276       break;
00277     }
00278     case Ctlp_AND_c: {
00279       result = TranslateCtlAND(catalog, formula, fairArray, fairPositive, 
00280                                fairNegative, polarity, uniqueIds);
00281       break;
00282     }
00283     case Ctlp_OR_c: {
00284       result = TranslateCtlOR(catalog, formula, fairArray, fairPositive, 
00285                               fairNegative, polarity, uniqueIds);
00286       break;
00287     }
00288     default: fail("Encountered unknown type of CTL formula\n");
00289   }
00290 
00291   return result;
00292 } /* End of TranslateCtlSubFormula */
00293 
00309 static AbsVertexInfo_t *
00310 ComputeFairPredicate(
00311   AbsVertexCatalog_t *catalog,
00312   AbsVertexInfo_t *atomicPredicate,
00313   array_t *fairArray,
00314   int polarity,
00315   int *uniqueIds)
00316 {
00317   Ctlp_Formula_t *ctlPtr;
00318   AbsVertexInfo_t *mainVarVertex;
00319   AbsVertexInfo_t *mainVarNotVertex;
00320   AbsVertexInfo_t *vertexPtr;
00321   AbsVertexInfo_t *aux1;
00322   AbsVertexInfo_t *aux2;
00323   AbsVertexInfo_t *aux3;
00324   array_t *conjunctions;
00325   array_t *constraintArray;
00326   int     mainVarId;
00327   int     i;
00328   
00329   /* Obtain the representation of the fairness predicates */
00330   constraintArray = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
00331   arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlPtr) {
00332     array_insert(AbsVertexInfo_t *, constraintArray, i, 
00333                  TranslateCtlSubFormula(catalog, ctlPtr, NIL(array_t), 
00334                                         NIL(AbsVertexInfo_t), 
00335                                         NIL(AbsVertexInfo_t), polarity,  
00336                                         uniqueIds));
00337   }
00338 
00339   /* Create the vertex representing the variable of the greatest fixed point */
00340   mainVarId = (*uniqueIds)++;
00341 
00342   aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity, 
00343                                    NIL(AbsVertexInfo_t), 
00344                                    NIL(AbsVertexInfo_t),
00345                                    mainVarId, NIL(char), NIL(char));
00346   if (AbsVertexReadType(aux1) == false_c) {
00347     AbsVertexSetPolarity(aux1, !polarity);
00348     AbsVertexSetDepth(aux1, 1);
00349     AbsVertexSetType(aux1, variable_c);
00350     AbsVertexSetVarId(aux1, mainVarId);
00351   }
00352   mainVarVertex = aux1;
00353 
00354   mainVarNotVertex = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
00355                                                NIL(AbsVertexInfo_t), 0, 
00356                                                NIL(char), NIL(char));
00357   if (AbsVertexReadType(mainVarNotVertex) == false_c) {
00358     AbsVertexSetPolarity(mainVarNotVertex, polarity);
00359     AbsVertexSetDepth(mainVarNotVertex, 2);
00360     AbsVertexSetType(mainVarNotVertex, not_c);
00361     AbsVertexSetLeftKid(mainVarNotVertex, aux1);
00362     AbsVertexSetParent(mainVarVertex, mainVarNotVertex);
00363   }
00364   else {
00365     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00366   }
00367 
00368   /* Create the predicates EX[E[f U z * f_i]] */
00369   conjunctions = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
00370   arrayForEachItem(AbsVertexInfo_t *, constraintArray, i, vertexPtr) {
00371     AbsVertexInfo_t *varVertex;
00372     int variableId;
00373 
00374     /* Create the conjunction between z and f_i */
00375     AbsVertexReadRefs(mainVarNotVertex)++;
00376     aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, vertexPtr, 
00377                                      mainVarNotVertex, 0, NIL(char), 
00378                                      NIL(char));
00379     if (AbsVertexReadType(aux1) == false_c) {
00380       AbsVertexSetPolarity(aux1, polarity);
00381       if (AbsVertexReadDepth(vertexPtr) > 2) {
00382         AbsVertexSetDepth(aux1, AbsVertexReadDepth(vertexPtr) + 1);
00383       }
00384       else {
00385         AbsVertexSetDepth(aux1, 3);
00386       }
00387       AbsVertexSetType(aux1, and_c);
00388       AbsVertexSetLeftKid(aux1, vertexPtr);
00389       AbsVertexSetRightKid(aux1, mainVarNotVertex);
00390       AbsVertexSetParent(vertexPtr, aux1);
00391       AbsVertexSetParent(mainVarNotVertex, aux1);
00392     }
00393     else {
00394       /* Cache hit */
00395       AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
00396       AbsVertexFree(catalog, mainVarNotVertex, NIL(AbsVertexInfo_t));
00397     }
00398 
00399     /* Create the vertex negating the previous conjunction */
00400     aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
00401                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
00402                                      NIL(char));
00403     if (AbsVertexReadType(aux2) == false_c) {
00404       AbsVertexSetPolarity(aux2, !polarity);
00405       AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00406       AbsVertexSetType(aux2, not_c);
00407       AbsVertexSetLeftKid(aux2, aux1);
00408       AbsVertexSetParent(aux1, aux2);
00409     }
00410     else {
00411       /* Cache hit */
00412       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00413     }
00414 
00415     /* Create the variable of the fixed point in the EU sub-formula*/
00416     variableId = (*uniqueIds)++;
00417     aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
00418                                      NIL(AbsVertexInfo_t), 
00419                                      NIL(AbsVertexInfo_t), variableId, 
00420                                      NIL(char), NIL(char));
00421     if (AbsVertexReadType(aux1) == false_c) {
00422       AbsVertexSetPolarity(aux1, polarity);
00423       AbsVertexSetDepth(aux1, 1);
00424       AbsVertexSetType(aux1, variable_c);
00425       AbsVertexSetVarId(aux1, variableId);
00426     }
00427     varVertex = aux1;
00428 
00429     /* Create the vertex storing the preimage sub-formula */
00430     aux3 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
00431                                      aux1, NIL(AbsVertexInfo_t),
00432                                      0, NIL(char), NIL(char));
00433     if (AbsVertexReadType(aux3) == false_c) {
00434       AbsVertexSetPolarity(aux3, polarity);
00435       AbsVertexSetDepth(aux3, 2);
00436       AbsVertexSetType(aux3, preImage_c);
00437       AbsVertexSetLeftKid(aux3, aux1);
00438       AbsVertexSetParent(aux1, aux3);
00439     }
00440     else {
00441       /* Cache hit */
00442       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00443     }
00444   
00445     if (atomicPredicate != NIL(AbsVertexInfo_t)) {
00446       AbsVertexReadRefs(atomicPredicate)++;
00447       /* Create the vertex representing the and */
00448       aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
00449                                        atomicPredicate, aux3, 0, NIL(char), 
00450                                        NIL(char));
00451       if (AbsVertexReadType(aux1) == false_c) {
00452         AbsVertexSetPolarity(aux1, polarity);
00453         if (AbsVertexReadDepth(atomicPredicate) > 2) {
00454           AbsVertexSetDepth(aux1, AbsVertexReadDepth(atomicPredicate) + 1);
00455         }
00456         else {
00457           AbsVertexSetDepth(aux1, 3);
00458         }
00459         AbsVertexSetType(aux1, and_c);
00460         AbsVertexSetLeftKid(aux1, atomicPredicate);
00461         AbsVertexSetRightKid(aux1, aux3);
00462         AbsVertexSetParent(atomicPredicate, aux1);
00463         AbsVertexSetParent(aux3, aux1);
00464       }
00465       else {
00466         /* Cache hit */
00467         AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
00468         AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
00469       }
00470     }
00471     else {
00472       aux1 = aux3;
00473     }
00474 
00475     /* Create the not vertex on top of the conjunction */
00476     aux3 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
00477                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
00478                                      NIL(char));
00479     if (AbsVertexReadType(aux3) == false_c) {
00480       AbsVertexSetPolarity(aux3, !polarity);
00481       AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
00482       AbsVertexSetType(aux3, not_c);
00483       AbsVertexSetLeftKid(aux3, aux1);
00484       AbsVertexSetParent(aux1, aux3);
00485     }
00486     else {
00487       /* Cache hit */
00488       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00489     }
00490     
00491     /* Vertex taking the conjunction */
00492     aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux2, aux3,
00493                                      0, NIL(char), NIL(char));
00494     if (AbsVertexReadType(aux1) == false_c) {
00495       AbsVertexSetPolarity(aux1, !polarity);
00496       if (AbsVertexReadDepth(aux2) > AbsVertexReadDepth(aux3)) {
00497         AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
00498       }
00499       else {
00500         AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
00501       }
00502       AbsVertexSetType(aux1, and_c);
00503       AbsVertexSetLeftKid(aux1, aux2);
00504       AbsVertexSetRightKid(aux1, aux3);
00505       AbsVertexSetParent(aux3, aux1);
00506       AbsVertexSetParent(aux2, aux1);
00507     }
00508     else {
00509       AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
00510       AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00511     }
00512     
00513     /* negation of the conjunction */
00514     aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
00515                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
00516                                      NIL(char));
00517     if (AbsVertexReadType(aux2) == false_c) {
00518       AbsVertexSetPolarity(aux2, polarity);
00519       AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00520       AbsVertexSetType(aux2, not_c);
00521       AbsVertexSetLeftKid(aux2, aux1);
00522       AbsVertexSetParent(aux1, aux2);
00523     }
00524     else {
00525       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00526     }
00527   
00528     /* Create the lfp vertex for the EU operator */
00529     aux1 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux2,
00530                                      NIL(AbsVertexInfo_t), 0, NIL(char),
00531                                      NIL(char));
00532     if (AbsVertexReadType(aux1) == false_c) {
00533       AbsVertexSetPolarity(aux1, polarity);
00534       AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
00535       AbsVertexSetType(aux1, fixedPoint_c);
00536       AbsVertexSetLeftKid(aux1, aux2);
00537       AbsVertexSetFpVar(aux1, varVertex);
00538       AbsVertexSetUseExtraCareSet(aux1, TRUE);
00539       AbsVertexSetParent(aux2, aux1);
00540     }
00541     else {
00542       AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00543     }
00544     
00545     /* Create the final EX vertex on top of the EU */
00546     aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
00547                                      aux1, NIL(AbsVertexInfo_t), 0, NIL(char),
00548                                      NIL(char));
00549     if (AbsVertexReadType(aux2) == false_c) {
00550       AbsVertexSetPolarity(aux2, polarity);
00551       AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00552       AbsVertexSetType(aux2, preImage_c);
00553       AbsVertexSetLeftKid(aux2, aux1);
00554       AbsVertexSetParent(aux1, aux2);
00555     }
00556     else {
00557       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00558     }
00559 
00560     array_insert(AbsVertexInfo_t *, conjunctions, i, aux2);
00561   } /* End of the loop iterating over the fairness constraints */
00562   AbsVertexReadRefs(mainVarNotVertex)--;
00563 
00564   /* Create the chain of ands for the conjunctions */
00565   aux1 = CreateConjunctionChain(catalog, conjunctions, polarity);
00566 
00567   /* Create the and with the atomic predicate if required */
00568   if (atomicPredicate != NIL(AbsVertexInfo_t)) {
00569     aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, atomicPredicate, 
00570                                      aux1, 0, NIL(char), NIL(char));
00571     if (AbsVertexReadType(aux2) == false_c) {
00572       AbsVertexSetPolarity(aux2, polarity);
00573       if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(atomicPredicate)) {
00574         AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00575       }
00576       else {
00577         AbsVertexSetDepth(aux2, AbsVertexReadDepth(atomicPredicate) + 1);
00578       }
00579       AbsVertexSetType(aux2, and_c);
00580       AbsVertexSetLeftKid(aux2, atomicPredicate);
00581       AbsVertexSetRightKid(aux2, aux1);
00582       AbsVertexSetParent(atomicPredicate, aux2);
00583       AbsVertexSetParent(aux1, aux2);
00584     }
00585     else {
00586       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00587       AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
00588     }
00589   }
00590   else {
00591     aux2 = aux1;
00592   }
00593 
00594   /* Create the not vertex on top of the conjunction */
00595   aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
00596                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
00597                                    NIL(char));
00598   if (AbsVertexReadType(aux1) == false_c) {
00599     AbsVertexSetPolarity(aux1, !polarity);
00600     AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
00601     AbsVertexSetType(aux1, not_c);
00602     AbsVertexSetLeftKid(aux1, aux2);
00603     AbsVertexSetParent(aux2, aux1);
00604   }
00605   else {
00606     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00607   }
00608   
00609   /* Create the top most fixed point vertex */
00610   aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
00611                                    NIL(AbsVertexInfo_t), mainVarId,
00612                                    NIL(char), NIL(char));
00613   if (AbsVertexReadType(aux2) == false_c) {
00614     AbsVertexSetPolarity(aux2, !polarity);
00615     AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00616     AbsVertexSetType(aux2, fixedPoint_c);
00617     AbsVertexSetVarId(aux2, mainVarId);
00618     AbsVertexSetLeftKid(aux2, aux1);
00619     AbsVertexSetFpVar(aux2, mainVarVertex);
00620     AbsVertexSetUseExtraCareSet(aux2, FALSE);
00621     AbsVertexSetParent(aux1, aux2);
00622   }
00623   else {
00624     AbsVertexSetUseExtraCareSet(aux2, FALSE);
00625     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00626   }
00627   
00628   /* Create the top most vertex */
00629   aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
00630                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
00631                                    NIL(char));
00632   if (AbsVertexReadType(aux1) == false_c) {
00633     AbsVertexSetPolarity(aux1, polarity);
00634     AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
00635     AbsVertexSetType(aux1, not_c);
00636     AbsVertexSetLeftKid(aux1, aux2);
00637     AbsVertexSetParent(aux2, aux1);
00638   }
00639   else {
00640     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00641   }
00642   
00643   /* Clean up */
00644   array_free(constraintArray);
00645   arrayForEachItem(AbsVertexInfo_t *, conjunctions, i, vertexPtr) {
00646     AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
00647   }
00648   array_free(conjunctions);
00649 
00650   return aux1;
00651 } /* End of ComputeFairPredicate */
00652 
00663 static AbsVertexInfo_t *
00664 TranslateCtlID(
00665   AbsVertexCatalog_t *catalog,
00666   Ctlp_Formula_t *formula,             
00667   int polarity)
00668 {
00669   AbsVertexInfo_t *result;
00670 
00671   result = AbsVertexCatalogFindOrAdd(catalog,
00672                                      identifier_c,
00673                                      polarity,
00674                                      NIL(AbsVertexInfo_t),
00675                                      NIL(AbsVertexInfo_t),
00676                                      0,
00677                                      Ctlp_FormulaReadVariableName(formula),
00678                                      Ctlp_FormulaReadValueName(formula));
00679   if (AbsVertexReadType(result) == false_c) {
00680     AbsVertexSetPolarity(result, polarity);
00681     AbsVertexSetDepth(result, 1);
00682     AbsVertexSetType(result, identifier_c);
00683     AbsVertexSetName(result, 
00684                      util_strsav(Ctlp_FormulaReadVariableName(formula)));
00685     AbsVertexSetValue(result,
00686                       util_strsav(Ctlp_FormulaReadValueName(formula)));
00687   }
00688   
00689   return result;
00690 } /* End of TranslateCtlID */
00691 
00702 static AbsVertexInfo_t *
00703 TranslateCtlEU(
00704   AbsVertexCatalog_t *catalog,
00705   Ctlp_Formula_t *formula,
00706   array_t *fairArray,
00707   AbsVertexInfo_t *fairPositive,
00708   AbsVertexInfo_t *fairNegative,
00709   int polarity,
00710   int *uniqueIds)
00711 {
00712   AbsVertexInfo_t *result;
00713   AbsVertexInfo_t *leftResult;
00714   AbsVertexInfo_t *rightResult;
00715   AbsVertexInfo_t *aux1;
00716   AbsVertexInfo_t *aux2;
00717   AbsVertexInfo_t *aux3;
00718   AbsVertexInfo_t *varVertex;
00719   int variableId;
00720   
00721   /* Allocate a unique id for the fixed point */
00722   variableId = (*uniqueIds)++;
00723   
00724   /* Create the vertex storing the fixed point variable */
00725   aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
00726                                    NIL(AbsVertexInfo_t), 
00727                                    NIL(AbsVertexInfo_t), variableId, 
00728                                    NIL(char), NIL(char));
00729   if (AbsVertexReadType(aux1) == false_c) {
00730     AbsVertexSetPolarity(aux1, polarity);
00731     AbsVertexSetDepth(aux1, 1);
00732     AbsVertexSetType(aux1, variable_c);
00733     AbsVertexSetVarId(aux1, variableId);
00734   }
00735   varVertex = aux1;
00736   
00737   /* Create the vertex storing the preimage sub-formula */
00738   aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
00739                                    aux1, NIL(AbsVertexInfo_t),
00740                                    0, NIL(char), NIL(char));
00741   if (AbsVertexReadType(aux2) == false_c) {
00742     AbsVertexSetPolarity(aux2, polarity);
00743     AbsVertexSetDepth(aux2, 2);
00744     AbsVertexSetType(aux2, preImage_c);
00745     AbsVertexSetLeftKid(aux2, aux1);
00746     AbsVertexSetParent(aux1, aux2);
00747   }
00748   else {
00749     /* Cache hit */
00750     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00751   }
00752   
00753   if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
00754     /* Compute the value of the sub-formula */
00755     leftResult = TranslateCtlSubFormula(catalog,
00756                                         Ctlp_FormulaReadLeftChild(formula),
00757                                         fairArray, fairPositive, fairNegative,
00758                                         polarity, uniqueIds);
00759     
00760     /* Create the vertex representing the and */
00761     aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, aux2,
00762                                      0, NIL(char), 
00763                                      NIL(char));
00764     if (AbsVertexReadType(aux1) == false_c) {
00765       AbsVertexSetPolarity(aux1, polarity);
00766       if (AbsVertexReadDepth(leftResult) > 2) {
00767         AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
00768       }
00769       else {
00770         AbsVertexSetDepth(aux1, 3);
00771       }
00772       AbsVertexSetType(aux1, and_c);
00773       AbsVertexSetLeftKid(aux1, leftResult);
00774       AbsVertexSetRightKid(aux1, aux2);
00775       AbsVertexSetParent(leftResult, aux1);
00776       AbsVertexSetParent(aux2, aux1);
00777     }
00778     else {
00779       /* Cache hit */
00780       AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00781       AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
00782     }
00783   } /* if type is TRUE */
00784   else {
00785     aux1 = aux2;
00786   }
00787   
00788   /* Create the not vertex on top of the conjunction */
00789   aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
00790                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
00791                                    NIL(char));
00792   if (AbsVertexReadType(aux2) == false_c) {
00793     AbsVertexSetPolarity(aux2, !polarity);
00794     AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
00795     AbsVertexSetType(aux2, not_c);
00796     AbsVertexSetLeftKid(aux2, aux1);
00797     AbsVertexSetParent(aux1, aux2);
00798   }
00799   else {
00800     /* Cache hit */
00801     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00802   }
00803   
00804   /* Evaluate the right operand of the EU */
00805   rightResult= TranslateCtlSubFormula(catalog,
00806                                       Ctlp_FormulaReadRightChild(formula),
00807                                       fairArray, fairPositive, fairNegative,
00808                                       polarity, uniqueIds);
00809   
00810   /* check if there are fairness constraints */
00811   if (fairPositive != NIL(AbsVertexInfo_t)) {
00812     AbsVertexInfo_t *fairness;
00813     AbsVertexInfo_t *conjunction;
00814 
00815     /* The negative polarity version of the fairness must be present as well */
00816     assert(fairNegative != NIL(AbsVertexInfo_t));
00817 
00818     /* Select the apropriate representation of the fairness constraint */
00819     if (polarity) {
00820       fairness = fairPositive;
00821     }
00822     else {
00823       fairness = fairNegative;
00824     }
00825     AbsVertexReadRefs(fairness)++;
00826 
00827     conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
00828                                             rightResult, fairness, 0, NIL(char),
00829                                             NIL(char));
00830 
00831     if (AbsVertexReadType(conjunction) == false_c) {
00832       int leftDepth;
00833       int rightDepth;
00834 
00835       leftDepth = AbsVertexReadDepth(rightResult);
00836       rightDepth = AbsVertexReadDepth(fairness);
00837 
00838       AbsVertexSetPolarity(conjunction, polarity);
00839       if (leftDepth > rightDepth) {
00840         AbsVertexSetDepth(conjunction, leftDepth + 1);
00841       }
00842       else {
00843         AbsVertexSetDepth(conjunction, rightDepth + 1);
00844       }
00845       AbsVertexSetType(conjunction, and_c);
00846       AbsVertexSetLeftKid(conjunction, rightResult);
00847       AbsVertexSetRightKid(conjunction, fairness);
00848       AbsVertexSetParent(rightResult, conjunction);
00849       AbsVertexSetParent(fairness, conjunction);
00850     }
00851     else {
00852       AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
00853       AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
00854     }
00855     rightResult = conjunction;
00856   }
00857 
00858   /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
00859   if (AbsVertexReadType(rightResult) == not_c) {
00860     AbsVertexInfo_t *newResult;
00861 
00862 
00863     newResult = AbsVertexReadLeftKid(rightResult);
00864     AbsVertexReadRefs(newResult)++;
00865     AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
00866     aux1 = newResult;
00867   }
00868   else {
00869     /* Vertex negating second operand */
00870     aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
00871                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
00872                                      NIL(char));
00873     if (AbsVertexReadType(aux1) == false_c) {
00874       AbsVertexSetPolarity(aux1, !polarity);
00875       AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
00876       AbsVertexSetType(aux1, not_c);
00877       AbsVertexSetLeftKid(aux1, rightResult);
00878       AbsVertexSetParent(rightResult, aux1);
00879     }
00880     else {
00881       AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
00882     }
00883   }
00884   
00885   /* Vertex taking the conjunction */
00886   aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
00887                                    0, NIL(char), NIL(char));
00888   if (AbsVertexReadType(aux3) == false_c) {
00889     AbsVertexSetPolarity(aux3, !polarity);
00890     if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
00891       AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
00892     }
00893     else {
00894       AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
00895     }
00896     AbsVertexSetType(aux3, and_c);
00897     AbsVertexSetLeftKid(aux3, aux1);
00898     AbsVertexSetRightKid(aux3, aux2);
00899     AbsVertexSetParent(aux1, aux3);
00900     AbsVertexSetParent(aux2, aux3);
00901   }
00902   else {
00903     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00904     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
00905   }
00906   
00907   /* negation of the conjunction */
00908   aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
00909                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
00910                                    NIL(char));
00911   if (AbsVertexReadType(aux1) == false_c) {
00912     AbsVertexSetPolarity(aux1, polarity);
00913     AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
00914     AbsVertexSetType(aux1, not_c);
00915     AbsVertexSetLeftKid(aux1, aux3);
00916     AbsVertexSetParent(aux3, aux1);
00917   }
00918   else {
00919     AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
00920   }
00921   
00922   /* Top vertex fixed point operator */
00923   result = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux1,
00924                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
00925                                      NIL(char));
00926   if (AbsVertexReadType(result) == false_c) {
00927     AbsVertexSetPolarity(result, polarity);
00928     AbsVertexSetDepth(result, AbsVertexReadDepth(aux1) + 1);
00929     AbsVertexSetType(result, fixedPoint_c);
00930     AbsVertexSetLeftKid(result, aux1);
00931     AbsVertexSetFpVar(result, varVertex);
00932     AbsVertexSetUseExtraCareSet(result, TRUE);
00933     AbsVertexSetParent(aux1, result);
00934   }
00935   else {
00936     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00937   }
00938   
00939   return result;
00940 } /* End of TranslateCtlEU */
00941 
00952 static AbsVertexInfo_t *
00953 TranslateCtlEG(
00954   AbsVertexCatalog_t *catalog,
00955   Ctlp_Formula_t *formula,
00956   int polarity,
00957   int *uniqueIds)
00958 {
00959   AbsVertexInfo_t *result;
00960   AbsVertexInfo_t *varVertex;
00961   AbsVertexInfo_t *aux1;
00962   AbsVertexInfo_t *aux2;
00963   AbsVertexInfo_t *childResult;
00964   int variableId;
00965   
00966   /* Allocate a unique id for the fixed point */
00967   variableId = (*uniqueIds)++;
00968   
00969   /* Create the vertex storing the fixed point variable */
00970   aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity,
00971                                    NIL(AbsVertexInfo_t), 
00972                                    NIL(AbsVertexInfo_t),
00973                                    variableId, NIL(char), NIL(char));
00974   if (AbsVertexReadType(aux1) == false_c) {
00975     AbsVertexSetPolarity(aux1, !polarity);
00976     AbsVertexSetDepth(aux1, 1);
00977     AbsVertexSetType(aux1, variable_c);
00978     AbsVertexSetVarId(aux1, variableId);
00979   }
00980   varVertex = aux1;
00981   
00982   /* Create the vertex to negate the variable of the fixed point */
00983   aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1, 
00984                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
00985                                    NIL(char));
00986   if (AbsVertexReadType(aux2) == false_c) {
00987     AbsVertexSetPolarity(aux2, polarity);
00988     AbsVertexSetDepth(aux2, 2);
00989     AbsVertexSetType(aux2, not_c);
00990     AbsVertexSetLeftKid(aux2, aux1);
00991     AbsVertexSetParent(aux1, aux2);
00992   }
00993   else {
00994     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
00995   }
00996 
00997   /* Create the vertex storing the preimage sub-formula */
00998   aux1 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
00999                                    aux1, NIL(AbsVertexInfo_t),
01000                                    0, NIL(char), NIL(char));
01001   if (AbsVertexReadType(aux1) == false_c) {
01002     AbsVertexSetPolarity(aux1, polarity);
01003     AbsVertexSetDepth(aux1, 3);
01004     AbsVertexSetType(aux1, preImage_c);
01005     AbsVertexSetLeftKid(aux1, aux2);
01006     AbsVertexSetParent(aux2, aux1);
01007   }
01008   else {
01009     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01010   }
01011   
01012   if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
01013     /* Create the vertex representing the sub-formula of EG */
01014     childResult = TranslateCtlSubFormula(catalog, 
01015                                          Ctlp_FormulaReadLeftChild(formula),
01016                                          NIL(array_t), NIL(AbsVertexInfo_t), 
01017                                          NIL(AbsVertexInfo_t), polarity, 
01018                                          uniqueIds);
01019     
01020     /* Create the vertex representing the and */
01021     aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, childResult, 
01022                                      aux1, 0, NIL(char), 
01023                                      NIL(char));
01024     if (AbsVertexReadType(aux2) == false_c) {
01025       AbsVertexSetPolarity(aux2, polarity);
01026       if (AbsVertexReadDepth(childResult) > 2) {
01027         AbsVertexSetDepth(aux2, AbsVertexReadDepth(childResult) + 1);
01028       }
01029       else {
01030         AbsVertexSetDepth(aux2, 4);
01031       }
01032       AbsVertexSetType(aux2, and_c);
01033       AbsVertexSetLeftKid(aux2, childResult);
01034       AbsVertexSetRightKid(aux2, aux1);
01035       AbsVertexSetParent(childResult, aux2);
01036       AbsVertexSetParent(aux1, aux2);
01037     }
01038     else {
01039       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01040       AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
01041     }
01042   }
01043   else {
01044     aux2 = aux1;
01045   }
01046   
01047   /* Create the not vertex on top of the conjunction */
01048   aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
01049                                    NIL(AbsVertexInfo_t), 0, NIL(char), 
01050                                    NIL(char));
01051   if (AbsVertexReadType(aux1) == false_c) {
01052     AbsVertexSetPolarity(aux1, !polarity);
01053     AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
01054     AbsVertexSetType(aux1, not_c);
01055     AbsVertexSetLeftKid(aux1, aux2);
01056     AbsVertexSetParent(aux2, aux1);
01057   }
01058   else {
01059     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
01060   }
01061   
01062   /* Create the fixedpoint_c vertex */
01063   aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
01064                                    NIL(AbsVertexInfo_t), variableId,
01065                                    NIL(char), NIL(char));
01066   if (AbsVertexReadType(aux2) == false_c) {
01067     AbsVertexSetPolarity(aux2, !polarity);
01068     AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
01069     AbsVertexSetType(aux2, fixedPoint_c);
01070     AbsVertexSetVarId(aux2, variableId);
01071     AbsVertexSetLeftKid(aux2, aux1);
01072     AbsVertexSetFpVar(aux2, varVertex);
01073     AbsVertexSetUseExtraCareSet(aux2, FALSE);
01074     AbsVertexSetParent(aux1, aux2);
01075   }
01076   else {
01077     AbsVertexSetUseExtraCareSet(aux2, FALSE);
01078     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01079   }
01080   
01081   /* Create the top most not vertex  */
01082   result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
01083                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01084                                      NIL(char));
01085   if (AbsVertexReadType(result) == false_c) {
01086     AbsVertexSetPolarity(result, polarity);
01087     AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
01088     AbsVertexSetType(result, not_c);
01089     AbsVertexSetLeftKid(result, aux2);
01090     AbsVertexSetParent(aux2, result);
01091   }
01092   else {
01093     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
01094   }
01095   
01096   return result;
01097 } /* End of TranslateCtlEG */
01098 
01109 static AbsVertexInfo_t *
01110 TranslateCtlEGFair(
01111   AbsVertexCatalog_t *catalog,
01112   Ctlp_Formula_t *formula,
01113   array_t *fairArray,
01114   AbsVertexInfo_t *fairPositive,
01115   AbsVertexInfo_t *fairNegative,
01116   int polarity,
01117   int *uniqueIds)
01118 {
01119   AbsVertexInfo_t *result;
01120   AbsVertexInfo_t *childResult;
01121 
01122   if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) == Ctlp_TRUE_c) {
01123     if (polarity) {
01124       result = fairPositive;
01125       AbsVertexReadRefs(fairPositive)++;
01126     }
01127     else {
01128       result = fairNegative;
01129       AbsVertexReadRefs(fairNegative)++;
01130     }
01131   }
01132   else {
01133     childResult = TranslateCtlSubFormula(catalog,
01134                                          Ctlp_FormulaReadLeftChild(formula),
01135                                          fairArray, fairPositive, fairNegative,
01136                                          polarity, uniqueIds);
01137 
01138     result = ComputeFairPredicate(catalog, childResult, fairArray, polarity,
01139                                   uniqueIds);
01140   }
01141 
01142   return result;
01143 } /* End of TranslateCtlEGFair */
01144 
01155 static AbsVertexInfo_t *
01156 TranslateCtlEX(
01157   AbsVertexCatalog_t *catalog,
01158   Ctlp_Formula_t *formula,
01159   array_t *fairArray,
01160   AbsVertexInfo_t *fairPositive,
01161   AbsVertexInfo_t *fairNegative,
01162   int polarity,
01163   int *uniqueIds)
01164 {
01165   AbsVertexInfo_t *result;
01166   AbsVertexInfo_t *childResult;
01167   
01168   /* Translate the sub-formula regardless */
01169   childResult = TranslateCtlSubFormula(catalog,
01170                                        Ctlp_FormulaReadLeftChild(formula),
01171                                        fairArray, fairPositive, fairNegative,
01172                                        polarity, uniqueIds);
01173   
01174   /* check if there are fairness constraints */
01175   if (fairPositive != NIL(AbsVertexInfo_t)) {
01176     AbsVertexInfo_t *fairness;
01177     AbsVertexInfo_t *conjunction;
01178 
01179     /* The negative polarity version of the fairness must be present as well */
01180     assert(fairNegative != NIL(AbsVertexInfo_t));
01181 
01182     /* Select the apropriate representation of the fairness constraint */
01183     if (polarity) {
01184       fairness = fairPositive;
01185     }
01186     else {
01187       fairness = fairNegative;
01188     }
01189     AbsVertexReadRefs(fairness)++;
01190 
01191     conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
01192                                             childResult, fairness, 0, NIL(char),
01193                                             NIL(char));
01194 
01195     if (AbsVertexReadType(conjunction) == false_c) {
01196       int leftDepth;
01197       int rightDepth;
01198 
01199       leftDepth = AbsVertexReadDepth(childResult);
01200       rightDepth = AbsVertexReadDepth(fairness);
01201 
01202       AbsVertexSetPolarity(conjunction, polarity);
01203       if (leftDepth > rightDepth) {
01204         AbsVertexSetDepth(conjunction, leftDepth + 1);
01205       }
01206       else {
01207         AbsVertexSetDepth(conjunction, rightDepth + 1);
01208       }
01209       AbsVertexSetType(conjunction, and_c);
01210       AbsVertexSetLeftKid(conjunction, childResult);
01211       AbsVertexSetRightKid(conjunction, fairness);
01212       AbsVertexSetParent(childResult, conjunction);
01213       AbsVertexSetParent(fairness, conjunction);
01214     }
01215     else {
01216       AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
01217       AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
01218     }
01219     childResult = conjunction;
01220   }
01221 
01222   /* Create the preImage vertex */
01223   result = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity, 
01224                                      childResult, NIL(AbsVertexInfo_t), 0, 
01225                                      NIL(char), NIL(char));
01226   if (AbsVertexReadType(result) == false_c) {
01227     AbsVertexSetPolarity(result, polarity);
01228     AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
01229     AbsVertexSetType(result, preImage_c);
01230     AbsVertexSetLeftKid(result, childResult);
01231     AbsVertexSetParent(childResult, result);
01232   }
01233   else {
01234     AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
01235   }
01236                                                            
01237   return result;
01238 } /* End of TranslateCtlEX */
01239 
01250 static AbsVertexInfo_t *
01251 TranslateCtlNOT(
01252   AbsVertexCatalog_t *catalog,
01253   Ctlp_Formula_t *formula,
01254   array_t *fairArray,
01255   AbsVertexInfo_t *fairPositive,
01256   AbsVertexInfo_t *fairNegative,
01257   int polarity,
01258   int *uniqueIds)
01259 {
01260   AbsVertexInfo_t *result;
01261   AbsVertexInfo_t *childResult;
01262   
01263   childResult = TranslateCtlSubFormula(catalog,
01264                                        Ctlp_FormulaReadLeftChild(formula),
01265                                        fairArray, fairPositive, fairNegative,
01266                                        !polarity, uniqueIds);
01267   
01268   /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
01269   if (AbsVertexReadType(childResult) == not_c) {
01270     AbsVertexInfo_t *newResult;
01271 
01272     newResult = AbsVertexReadLeftKid(childResult);
01273     AbsVertexReadRefs(newResult)++;
01274     AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
01275     
01276     return newResult;
01277   }
01278 
01279   /* Create the not vertex */
01280   result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, childResult,
01281                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01282                                      NIL(char));
01283   if (AbsVertexReadType(result) == false_c) {
01284     AbsVertexSetPolarity(result, polarity);
01285     AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
01286     AbsVertexSetType(result, not_c);
01287     AbsVertexSetLeftKid(result, childResult);
01288     AbsVertexSetParent(childResult, result);
01289   }
01290   else {
01291     AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
01292   }
01293   
01294   return result;
01295 } /* End of TranslateCtlNOT */
01296 
01307 static AbsVertexInfo_t *
01308 TranslateCtlTHEN(
01309   AbsVertexCatalog_t *catalog,
01310   Ctlp_Formula_t *formula,
01311   array_t *fairArray,
01312   AbsVertexInfo_t *fairPositive,
01313   AbsVertexInfo_t *fairNegative,
01314   int polarity,
01315   int *uniqueIds)
01316 {
01317   AbsVertexInfo_t *result;
01318   AbsVertexInfo_t *leftResult, *rightResult;
01319   AbsVertexInfo_t *aux1;
01320   AbsVertexInfo_t *aux2;
01321   
01322   leftResult = TranslateCtlSubFormula(catalog,
01323                                       Ctlp_FormulaReadLeftChild(formula),
01324                                       fairArray, fairPositive, fairNegative,
01325                                       !polarity, uniqueIds);
01326   rightResult= TranslateCtlSubFormula(catalog,
01327                                       Ctlp_FormulaReadRightChild(formula),
01328                                       fairArray, fairPositive, fairNegative,
01329                                       polarity, uniqueIds);
01330   
01331   /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
01332   if (AbsVertexReadType(rightResult) == not_c) {
01333     AbsVertexInfo_t *newResult;
01334 
01335     newResult = AbsVertexReadLeftKid(rightResult);
01336     AbsVertexReadRefs(newResult)++;
01337     AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
01338     aux1 = newResult;
01339   }
01340   else {
01341     /* Vertex negating first operand */
01342     aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
01343                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01344                                      NIL(char));
01345     if (AbsVertexReadType(aux1) == false_c) {
01346       AbsVertexSetPolarity(aux1, !polarity);
01347       AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
01348       AbsVertexSetType(aux1, not_c);
01349       AbsVertexSetLeftKid(aux1, rightResult);
01350       AbsVertexSetParent(rightResult, aux1);
01351     }
01352     else {
01353       AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
01354     }
01355   }
01356   
01357   /* Result node holding the and of both operands */
01358   aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, leftResult, 
01359                                    aux1, 0, NIL(char), NIL(char));
01360   if (AbsVertexReadType(aux2) == false_c) {
01361     AbsVertexSetPolarity(aux2, !polarity);
01362     if (AbsVertexReadDepth(leftResult) > AbsVertexReadDepth(aux1)) {
01363       AbsVertexSetDepth(aux2, AbsVertexReadDepth(leftResult) + 1);
01364     }
01365     else {
01366       AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
01367     }
01368     AbsVertexSetType(aux2, and_c);
01369     AbsVertexSetLeftKid(aux2, leftResult);
01370     AbsVertexSetRightKid(aux2, aux1);
01371     AbsVertexSetParent(aux1, aux2);
01372     AbsVertexSetParent(leftResult, aux2);
01373   }
01374   else {
01375     AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
01376     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01377   }
01378   
01379   /* Top vertex negation of the conjunction */
01380   result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
01381                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01382                                      NIL(char));
01383   if (AbsVertexReadType(result) == false_c) {
01384     AbsVertexSetPolarity(result, polarity);
01385     AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
01386     AbsVertexSetType(result, not_c);
01387     AbsVertexSetLeftKid(result, aux2);
01388     AbsVertexSetParent(aux2, result);
01389   }
01390   else {
01391     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
01392   }
01393   
01394   return result;
01395 } /* End of TranslateCtlTHEN */
01396 
01407 static AbsVertexInfo_t *
01408 TranslateCtlAND(
01409   AbsVertexCatalog_t *catalog,
01410   Ctlp_Formula_t *formula,
01411   array_t *fairArray,
01412   AbsVertexInfo_t *fairPositive,
01413   AbsVertexInfo_t *fairNegative,
01414   int polarity,
01415   int *uniqueIds)
01416 {
01417   AbsVertexInfo_t *result;
01418   AbsVertexInfo_t *leftResult, *rightResult;
01419   int leftDepth;
01420   int rightDepth;
01421   
01422   leftResult = TranslateCtlSubFormula(catalog,
01423                                       Ctlp_FormulaReadLeftChild(formula),
01424                                       fairArray, fairPositive, fairNegative,
01425                                       polarity, uniqueIds);
01426   rightResult= TranslateCtlSubFormula(catalog,
01427                                       Ctlp_FormulaReadRightChild(formula),
01428                                       fairArray, fairPositive, fairNegative,
01429                                       polarity, uniqueIds);
01430   
01431   /* Read the depths */
01432   leftDepth = AbsVertexReadDepth(leftResult);
01433   rightDepth = AbsVertexReadDepth(rightResult);
01434   
01435   result = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, 
01436                                      rightResult, 0, NIL(char), NIL(char));
01437   if (AbsVertexReadType(result) == false_c) {
01438     AbsVertexSetPolarity(result, polarity);
01439     if (leftDepth > rightDepth) {
01440       AbsVertexSetDepth(result, leftDepth + 1);
01441     }
01442     else {
01443       AbsVertexSetDepth(result, rightDepth + 1);
01444     }
01445     AbsVertexSetType(result, and_c);
01446     AbsVertexSetLeftKid(result, leftResult);
01447     AbsVertexSetRightKid(result, rightResult);
01448     AbsVertexSetParent(leftResult, result);
01449     AbsVertexSetParent(rightResult, result);
01450   }
01451   else {
01452     AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
01453     AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
01454   }
01455   
01456   return result;
01457 } /* End of TranslateCtlAND */
01458 
01469 static AbsVertexInfo_t *
01470 TranslateCtlOR(
01471   AbsVertexCatalog_t *catalog,
01472   Ctlp_Formula_t *formula,
01473   array_t *fairArray,
01474   AbsVertexInfo_t *fairPositive,
01475   AbsVertexInfo_t *fairNegative,
01476   int polarity,
01477   int *uniqueIds)
01478 {
01479   AbsVertexInfo_t *result;
01480   AbsVertexInfo_t *leftResult, *rightResult;
01481   AbsVertexInfo_t *aux1;
01482   AbsVertexInfo_t *aux2;
01483   AbsVertexInfo_t *aux3;
01484   
01485   leftResult = TranslateCtlSubFormula(catalog,
01486                                       Ctlp_FormulaReadLeftChild(formula),
01487                                       fairArray, fairPositive, fairNegative,
01488                                       polarity, uniqueIds);
01489   rightResult= TranslateCtlSubFormula(catalog,
01490                                       Ctlp_FormulaReadRightChild(formula),
01491                                       fairArray, fairPositive, fairNegative,
01492                                       polarity, uniqueIds);
01493   
01494   /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
01495   if (AbsVertexReadType(leftResult) == not_c) {
01496     AbsVertexInfo_t *newResult;
01497 
01498     newResult = AbsVertexReadLeftKid(leftResult);
01499     AbsVertexReadRefs(newResult)++;
01500     AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
01501     aux1 = newResult;
01502   }
01503   else {
01504     /* Vertex negating first operand */
01505     aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, leftResult, 
01506                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01507                                      NIL(char));
01508     if (AbsVertexReadType(aux1) == false_c) {
01509       AbsVertexSetPolarity(aux1, !polarity);
01510       AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
01511       AbsVertexSetType(aux1, not_c);
01512       AbsVertexSetLeftKid(aux1, leftResult);
01513       AbsVertexSetParent(leftResult, aux1);
01514     }
01515     else {
01516       AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
01517     }
01518   }
01519   
01520   if (AbsVertexReadType(rightResult) == not_c) {
01521     AbsVertexInfo_t *newResult;
01522 
01523     newResult = AbsVertexReadLeftKid(rightResult);
01524     AbsVertexReadRefs(newResult)++;
01525     AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
01526     aux2 = newResult;
01527   }
01528   else {
01529     /* Vertex negating second operand */
01530     aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
01531                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01532                                      NIL(char));
01533     if (AbsVertexReadType(aux2) == false_c) {
01534       AbsVertexSetPolarity(aux2, !polarity);
01535       AbsVertexSetDepth(aux2, AbsVertexReadDepth(rightResult) + 1);
01536       AbsVertexSetType(aux2, not_c);
01537       AbsVertexSetLeftKid(aux2, rightResult);
01538       AbsVertexSetParent(rightResult, aux2);
01539     }
01540     else {
01541       AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
01542     }
01543   }
01544   
01545   /* Vertex taking the conjunction */
01546   aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
01547                                    0, NIL(char), NIL(char));
01548   if (AbsVertexReadType(aux3) == false_c) {
01549     AbsVertexSetPolarity(aux3, !polarity);
01550     if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
01551       AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
01552     }
01553     else {
01554       AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
01555     }
01556     AbsVertexSetType(aux3, and_c);
01557     AbsVertexSetLeftKid(aux3, aux1);
01558     AbsVertexSetRightKid(aux3, aux2);
01559     AbsVertexSetParent(aux1, aux3);
01560     AbsVertexSetParent(aux2, aux3);
01561   }
01562   else {
01563     AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01564     AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
01565   }
01566   
01567   /* Top vertex negation of the conjunction */
01568   result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
01569                                      NIL(AbsVertexInfo_t), 0, NIL(char), 
01570                                      NIL(char));
01571   if (AbsVertexReadType(result) == false_c) {
01572     AbsVertexSetPolarity(result, polarity);
01573     AbsVertexSetDepth(result, AbsVertexReadDepth(aux3) + 1);
01574     AbsVertexSetType(result, not_c);
01575     AbsVertexSetLeftKid(result, aux3);
01576     AbsVertexSetParent(aux3, result);
01577   }
01578   else {
01579     AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
01580   }
01581   
01582   return result;
01583 } /* End of TranslateCtlOR */
01584 
01595 static AbsVertexInfo_t *
01596 CreateConjunctionChain(
01597   AbsVertexCatalog_t *catalog,
01598   array_t *conjunctions,
01599   int polarity)
01600 {
01601   AbsVertexInfo_t *aux1;
01602   AbsVertexInfo_t *aux2;
01603   AbsVertexInfo_t *aux3;
01604   int i;
01605 
01606   assert(conjunctions != NIL(array_t));
01607 
01608   aux1 = array_fetch(AbsVertexInfo_t *, conjunctions, 0);
01609   AbsVertexReadRefs(aux1)++;
01610 
01611   if (array_n(conjunctions) == 1) {
01612     return aux1;
01613   }
01614 
01615   for (i=1; i<array_n(conjunctions); i++) {
01616     aux2 = array_fetch(AbsVertexInfo_t *, conjunctions, i);
01617     AbsVertexReadRefs(aux2)++;
01618     
01619     aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, aux1, aux2, 0,
01620                                      NIL(char), NIL(char));
01621 
01622     if (AbsVertexReadType(aux3) == false_c) {
01623       AbsVertexSetPolarity(aux3, polarity);
01624       if (AbsVertexReadDepth(aux1) < AbsVertexReadDepth(aux2)) {
01625         AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
01626       }
01627       else {
01628         AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
01629       }
01630       AbsVertexSetType(aux3, and_c);
01631       AbsVertexSetLeftKid(aux3, aux1);
01632       AbsVertexSetRightKid(aux3, aux2);
01633       AbsVertexSetParent(aux1, aux3);
01634       AbsVertexSetParent(aux2, aux3);
01635     }
01636     else {
01637       AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
01638       AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
01639     }
01640 
01641     aux1 = aux3;
01642   }
01643 
01644   return aux1;
01645 } /* End of CreateConjunctionChain */