VIS
|
00001 00017 #include "ltlInt.h" 00018 00019 static char rcsid[] UNUSED = "$Id: ltlTableau.c,v 1.15 2008/04/22 21:22:33 fabio Exp $"; 00020 00021 /*---------------------------------------------------------------------------*/ 00022 /* Constant declarations */ 00023 /*---------------------------------------------------------------------------*/ 00024 00025 /*---------------------------------------------------------------------------*/ 00026 /* Structure declarations */ 00027 /*---------------------------------------------------------------------------*/ 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Type declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 /*---------------------------------------------------------------------------*/ 00034 /* Variable declarations */ 00035 /*---------------------------------------------------------------------------*/ 00036 00037 /*---------------------------------------------------------------------------*/ 00038 /* Macro declarations */ 00039 /*---------------------------------------------------------------------------*/ 00040 00043 /*---------------------------------------------------------------------------*/ 00044 /* Static function prototypes */ 00045 /*---------------------------------------------------------------------------*/ 00046 00047 static void TableauClearMarks(LtlTableau_t *tableau); 00048 static int TableauRules(LtlTableau_t *tableau, Ctlsp_Formula_t *F); 00049 static void HashNextFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F); 00050 static void TableauLoadUntilSubFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F); 00051 00054 /*---------------------------------------------------------------------------*/ 00055 /* Definition of exported functions */ 00056 /*---------------------------------------------------------------------------*/ 00057 00070 LtlTableau_t * 00071 LtlTableauGenerateTableau( 00072 Ctlsp_Formula_t *formula) 00073 { 00074 Ctlsp_Formula_t *F, *notF, *tmpF; 00075 LtlTableau_t *tableau; 00076 int save_n; 00077 int i, j; 00078 00079 /* compute the NNF of (formula) and (its negation) */ 00080 F = Ctlsp_LtlFormulaNegationNormalForm(formula); 00081 tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula, NIL(Ctlsp_Formula_t)); 00082 notF = Ctlsp_LtlFormulaNegationNormalForm(tmpF); 00083 FREE(tmpF); 00084 00085 /* Create the 'tableau' for this LTL->AUT problem */ 00086 tableau = LtlTableauCreate(); 00087 00088 /* Hash F & notF into the unique table */ 00089 F = Ctlsp_LtlFormulaHashIntoUniqueTable(F,tableau->formulaUniqueTable); 00090 notF = Ctlsp_LtlFormulaHashIntoUniqueTable(notF,tableau->formulaUniqueTable); 00091 tableau->F = F; 00092 tableau->notF = notF; 00093 00094 /* tricky part:: for each U-formula/R-formula 'F', also hash 'XF' */ 00095 TableauClearMarks(tableau); 00096 HashNextFormulae(tableau, F); 00097 00098 /* Build the Alpha/Beta entry table */ 00099 tableau->abIndex = st_count(tableau->formulaUniqueTable); 00100 tableau->abTable = ALLOC(LtlTableauEntry_t, tableau->abIndex); 00101 tableau->labelTable = ALLOC(Ctlsp_Formula_t *, tableau->abIndex); 00102 00103 save_n = tableau->abIndex; 00104 tableau->abIndex = 0; 00105 TableauClearMarks(tableau); 00106 TableauRules(tableau,F); /* build the Alpha-Beta table */ 00107 TableauRules(tableau, notF); 00108 tableau->abIndex = save_n; 00109 00110 /* compute the negation field (.notF) for each Alpha-Beta entry */ 00111 for (i=0; i<tableau->abIndex; i++) { 00112 if (!tableau->abTable[i].notF) { 00113 Ctlsp_Formula_t *thisF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, 00114 tableau->abTable[i].F, 00115 NIL(Ctlsp_Formula_t)); 00116 Ctlsp_Formula_t *nnfF = Ctlsp_LtlFormulaNegationNormalForm(thisF); 00117 FREE(thisF); 00118 00119 tableau->abTable[i].notF = 00120 Ctlsp_LtlFormulaHashIntoUniqueTable(nnfF, tableau->formulaUniqueTable); 00121 for (j=0; j<tableau->abIndex; j++) { 00122 if (tableau->abTable[j].F == tableau->abTable[i].notF) { 00123 tableau->abTable[i].notF_idx = j; 00124 tableau->abTable[j].notF_idx = i; 00125 tableau->abTable[j].notF = tableau->abTable[i].F; 00126 break; 00127 } 00128 } 00129 assert(j < tableau->abIndex); 00130 } 00131 array_insert(int, tableau->abTableNegate, i, tableau->abTable[i].notF_idx); 00132 } 00133 00134 /* put all constant formulae (labels) into tableau->labelTable 00135 * includes: ID/NOT(ID) */ 00136 j = 0; 00137 for (i=0; i<tableau->abIndex; i++) { 00138 Ctlsp_Formula_t *holdF = tableau->abTable[i].F; 00139 if (Ctlsp_LtlFormulaIsPropositional(holdF) && 00140 Ctlsp_FormulaReadType(holdF) != Ctlsp_TRUE_c && 00141 Ctlsp_FormulaReadType(holdF) != Ctlsp_FALSE_c) { 00142 tableau->labelTable[j] = tableau->abTable[i].F; 00143 Ctlsp_FormulaSetLabelIndex(tableau->abTable[i].F, j); 00144 j++; 00145 } 00146 } 00147 tableau->labelIndex = j; 00148 00149 /* Create the Negate Method for abTable and labelTable */ 00150 for (i=0; i<tableau->abIndex; i++) { 00151 array_insert(int, tableau->abTableNegate, i, 00152 Ctlsp_FormulaReadABIndex(tableau->abTable[i].notF)); 00153 } 00154 for (i=0; i<tableau->labelIndex; i++) { 00155 int idx = Ctlsp_FormulaReadABIndex(tableau->labelTable[i]); 00156 array_insert(int, tableau->labelTableNegate, i, 00157 Ctlsp_FormulaReadLabelIndex(tableau->abTable[idx].notF)); 00158 } 00159 00160 /* put all the 'until sub-formulae' into tableau->untilUniqueTable */ 00161 TableauClearMarks(tableau); 00162 TableauLoadUntilSubFormulae(tableau, F); 00163 00164 return tableau; 00165 } 00166 00167 00177 LtlTableau_t * 00178 LtlTableauCreate( 00179 void) 00180 { 00181 LtlTableau_t *tableau = ALLOC(LtlTableau_t, 1); 00182 memset(tableau, 0, sizeof(LtlTableau_t)); 00183 00184 tableau->F = tableau->notF = NIL(Ctlsp_Formula_t); 00185 tableau->abIndex = 0; 00186 tableau->abTable = 0; 00187 tableau->abTableNegate = array_alloc(int, 0); 00188 tableau->labelTable = 0; 00189 tableau->labelTableNegate = array_alloc(int, 0); 00190 /* create empty hash tables */ 00191 tableau->formulaUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable(); 00192 tableau->untilUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable(); 00193 00194 return tableau; 00195 } 00196 00197 00207 void 00208 LtlTableauFree( 00209 LtlTableau_t *tableau) 00210 { 00211 int i; 00212 char *tmpstr; 00213 00214 /* free all the LTL formulae */ 00215 for (i=0; i<tableau->abIndex; i++) { 00216 if (Ctlsp_FormulaReadType(tableau->abTable[i].F) == Ctlsp_ID_c) { 00217 tmpstr = Ctlsp_FormulaReadVariableName(tableau->abTable[i].F); 00218 FREE(tmpstr); 00219 tmpstr = Ctlsp_FormulaReadValueName(tableau->abTable[i].F); 00220 FREE(tmpstr); 00221 } 00222 FREE(tableau->abTable[i].F); 00223 } 00224 00225 FREE(tableau->abTable); 00226 FREE(tableau->labelTable); 00227 array_free(tableau->abTableNegate); 00228 array_free(tableau->labelTableNegate); 00229 00230 st_free_table(tableau->formulaUniqueTable); 00231 st_free_table(tableau->untilUniqueTable); 00232 00233 FREE(tableau); 00234 } 00235 00236 00246 void 00247 LtlTableauPrint( 00248 FILE *fp, 00249 LtlTableau_t *tableau) 00250 { 00251 int i; 00252 00253 (void) fprintf(fp, "Tableau Rules for {"); 00254 Ctlsp_FormulaPrint(fp,tableau->F); 00255 (void) fprintf(fp, "} : # of sub-formulae = %d\n", tableau->abIndex); 00256 00257 for (i=0; i<tableau->abIndex; i++) { 00258 fprintf(fp, "%d [", i); 00259 Ctlsp_FormulaPrint(fp, tableau->abTable[i].F); 00260 fprintf(fp, "]\n\t"); 00261 fprintf(fp, "(%3d * %3d * X%3d) + (%3d * %3d * X%3d) -- notF= %3d\n", 00262 tableau->abTable[i].A[0].B[0], 00263 tableau->abTable[i].A[0].B[1], 00264 tableau->abTable[i].A[0].n, 00265 tableau->abTable[i].A[1].B[0], 00266 tableau->abTable[i].A[1].B[1], 00267 tableau->abTable[i].A[1].n, 00268 tableau->abTable[i].notF_idx); 00269 } 00270 } 00271 00272 00283 Ctlsp_Formula_t * 00284 LtlTableauGetUniqueXFormula( 00285 LtlTableau_t *tableau, 00286 Ctlsp_Formula_t *F) 00287 { 00288 Ctlsp_Formula_t *tmpF, *XF; 00289 00290 tmpF = Ctlsp_FormulaCreate(Ctlsp_X_c, F, NIL(Ctlsp_Formula_t)); 00291 XF = Ctlsp_LtlFormulaNegationNormalForm(tmpF); 00292 FREE(tmpF); 00293 XF = Ctlsp_LtlFormulaHashIntoUniqueTable(XF,tableau->formulaUniqueTable); 00294 00295 return XF; 00296 } 00297 00298 00299 /*---------------------------------------------------------------------------*/ 00300 /* Definition of static functions */ 00301 /*---------------------------------------------------------------------------*/ 00302 00303 00313 static void 00314 TableauClearMarks( 00315 LtlTableau_t *tableau) 00316 { 00317 st_table *tbl = tableau->formulaUniqueTable; 00318 st_generator *stgen; 00319 Ctlsp_Formula_t *F; 00320 00321 st_foreach_item(tbl, stgen, &F, NIL(char *)) { 00322 Ctlsp_FormulaResetMarked(F); 00323 } 00324 } 00325 00326 00337 static int 00338 TableauRules( 00339 LtlTableau_t *tableau, 00340 Ctlsp_Formula_t *F) 00341 { 00342 int index; 00343 int A0B0=-1, A0B1=-1, A0n=-1; 00344 int A1B0=-1, A1B1=-1, A1n=-1; 00345 Ctlsp_Formula_t *XF; 00346 Ctlsp_Formula_t *F_left, *F_right; 00347 Ctlsp_FormulaType F_type; 00348 00349 assert( F ); 00350 00351 if (Ctlsp_FormulaReadMarked(F)) 00352 return Ctlsp_FormulaReadABIndex(F); 00353 00354 Ctlsp_FormulaSetMarked(F); 00355 index = tableau->abIndex++; 00356 Ctlsp_FormulaSetABIndex(F, index); 00357 00358 F_type = Ctlsp_FormulaReadType(F); 00359 F_left = Ctlsp_FormulaReadLeftChild(F); 00360 F_right = Ctlsp_FormulaReadRightChild(F); 00361 00362 switch(F_type) { 00363 case Ctlsp_X_c: 00364 TableauRules(tableau, F_left); 00365 A0n = index; 00366 break; 00367 case Ctlsp_OR_c: 00368 A0B0 = TableauRules(tableau, F_left); 00369 A1B0 = TableauRules(tableau, F_right); 00370 break; 00371 case Ctlsp_AND_c: 00372 A0B0 = TableauRules(tableau, F_left); 00373 A0B1 = TableauRules(tableau, F_right); 00374 break; 00375 case Ctlsp_U_c: 00376 A0B0 = TableauRules(tableau, F_left); 00377 A1B0 = TableauRules(tableau, F_right); 00378 XF = LtlTableauGetUniqueXFormula(tableau, F); 00379 A0n = TableauRules(tableau, XF); 00380 break; 00381 case Ctlsp_R_c: 00382 A0B0 = TableauRules(tableau, F_right); 00383 A1B0 = TableauRules(tableau, F_right); 00384 A1B1 = TableauRules(tableau, F_left); 00385 XF = LtlTableauGetUniqueXFormula(tableau, F); 00386 A0n = TableauRules(tableau, XF); 00387 break; 00388 default: 00389 break; 00390 } 00391 00392 tableau->abTable[index].F = F; 00393 tableau->abTable[index].A[0].B[0] = A0B0; 00394 tableau->abTable[index].A[0].B[1] = A0B1; 00395 tableau->abTable[index].A[1].B[0] = A1B0; 00396 tableau->abTable[index].A[1].B[1] = A1B1; 00397 tableau->abTable[index].A[0].n = A0n; 00398 tableau->abTable[index].A[1].n = A1n; 00399 00400 tableau->abTable[index].notF_idx = -1; 00401 tableau->abTable[index].notF = NIL(Ctlsp_Formula_t); 00402 00403 return index; 00404 } 00405 00415 static void 00416 HashNextFormulae( 00417 LtlTableau_t *tableau, 00418 Ctlsp_Formula_t *F) 00419 { 00420 Ctlsp_Formula_t *XF, *NXF, *tmpF; 00421 Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F); 00422 Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F); 00423 Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F); 00424 00425 switch( F_type ) { 00426 case Ctlsp_X_c: 00427 HashNextFormulae(tableau, F_left); 00428 break; 00429 case Ctlsp_OR_c: 00430 case Ctlsp_AND_c: 00431 HashNextFormulae(tableau, F_left); 00432 HashNextFormulae(tableau, F_right); 00433 break; 00434 case Ctlsp_U_c: 00435 case Ctlsp_R_c: 00436 HashNextFormulae(tableau, F_left); 00437 HashNextFormulae(tableau, F_right); 00438 XF = LtlTableauGetUniqueXFormula(tableau, F); 00439 tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, XF, NIL(Ctlsp_Formula_t)); 00440 NXF = Ctlsp_LtlFormulaNegationNormalForm(tmpF); 00441 FREE(tmpF); 00442 Ctlsp_LtlFormulaHashIntoUniqueTable(NXF,tableau->formulaUniqueTable); 00443 break; 00444 default: 00445 break; 00446 } 00447 } 00448 00458 static void 00459 TableauLoadUntilSubFormulae( 00460 LtlTableau_t *tableau, 00461 Ctlsp_Formula_t *F) 00462 { 00463 char *list; 00464 st_table *uniqueTable = tableau->untilUniqueTable; 00465 Ctlsp_FormulaType F_type; 00466 00467 if (!F) 00468 return; 00469 00470 if (Ctlsp_FormulaReadMarked(F)) 00471 return; 00472 00473 00474 Ctlsp_FormulaSetMarked(F); 00475 F_type = Ctlsp_FormulaReadType(F); 00476 if (F_type == Ctlsp_U_c) { 00477 if(!st_is_member(uniqueTable, F)) { 00478 list = (char *) lsCreate(); 00479 st_insert(uniqueTable, F, list); 00480 } 00481 Ctlsp_FormulaSetRhs(Ctlsp_FormulaReadRightChild(F)); 00482 } 00483 if (F_type != Ctlsp_ID_c) { 00484 TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadLeftChild(F)); 00485 TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadRightChild(F)); 00486 } 00487 } 00488