VIS

src/ltl/ltlTableau.c

Go to the documentation of this file.
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