VIS
|
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 */