source: vis_dev/vis-2.3/src/ltl/ltlTableau.c @ 23

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

vis2.3
File size: 14.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltlTableau.c]
4
5  PackageName [ltl]
6
7  Synopsis    [Expand the LTL Formula by applying the Tableau Rules.]
8
9  Author      [Chao Wang<chao.wang@colorado.EDU>]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "ltlInt.h"
18
19static char rcsid[] UNUSED = "$Id: ltlTableau.c,v 1.15 2008/04/22 21:22:33 fabio Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Structure declarations                                                    */
27/*---------------------------------------------------------------------------*/
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Variable declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37/*---------------------------------------------------------------------------*/
38/* Macro declarations                                                        */
39/*---------------------------------------------------------------------------*/
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static void TableauClearMarks(LtlTableau_t *tableau);
48static int TableauRules(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
49static void HashNextFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
50static void TableauLoadUntilSubFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
51
52/**AutomaticEnd***************************************************************/
53
54/*---------------------------------------------------------------------------*/
55/* Definition of exported functions                                          */
56/*---------------------------------------------------------------------------*/
57
58/**Function********************************************************************
59
60  Synopsis    [Generate the 'Tableau' sturcture for the LTL->AUT problem.
61  It first computes the NNF of the input formula, then create the alpha/beta
62  entry table for both the input formula and its negation according the
63  tableau rules, and finally compute the list of 'Until formulae'.]
64
65  SideEffects []
66
67  SeeAlso     [LtlTableauGenerateRules]
68
69******************************************************************************/
70LtlTableau_t *
71LtlTableauGenerateTableau(
72  Ctlsp_Formula_t *formula)
73{
74  Ctlsp_Formula_t *F, *notF, *tmpF;
75  LtlTableau_t   *tableau;
76  int save_n;
77  int i, j;
78
79  /* compute the NNF of (formula) and (its negation) */
80  F = Ctlsp_LtlFormulaNegationNormalForm(formula);
81  tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula, NIL(Ctlsp_Formula_t));
82  notF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
83  FREE(tmpF);
84
85  /* Create the 'tableau' for this LTL->AUT problem */
86  tableau = LtlTableauCreate();
87 
88  /* Hash F & notF into the unique table */
89  F = Ctlsp_LtlFormulaHashIntoUniqueTable(F,tableau->formulaUniqueTable);
90  notF = Ctlsp_LtlFormulaHashIntoUniqueTable(notF,tableau->formulaUniqueTable);
91  tableau->F = F;
92  tableau->notF = notF;
93
94  /* tricky part:: for each U-formula/R-formula 'F', also hash 'XF' */
95  TableauClearMarks(tableau);
96  HashNextFormulae(tableau, F);
97 
98  /* Build the Alpha/Beta entry table */
99  tableau->abIndex = st_count(tableau->formulaUniqueTable);
100  tableau->abTable = ALLOC(LtlTableauEntry_t, tableau->abIndex);
101  tableau->labelTable = ALLOC(Ctlsp_Formula_t *, tableau->abIndex);
102
103  save_n = tableau->abIndex;
104  tableau->abIndex = 0;
105  TableauClearMarks(tableau);
106  TableauRules(tableau,F);      /* build the Alpha-Beta table */
107  TableauRules(tableau, notF);
108  tableau->abIndex = save_n;
109
110  /* compute the negation field (.notF) for each Alpha-Beta entry */
111  for (i=0; i<tableau->abIndex; i++) {
112    if (!tableau->abTable[i].notF) {
113      Ctlsp_Formula_t *thisF = Ctlsp_FormulaCreate(Ctlsp_NOT_c,
114                                                   tableau->abTable[i].F,
115                                                   NIL(Ctlsp_Formula_t));
116      Ctlsp_Formula_t *nnfF = Ctlsp_LtlFormulaNegationNormalForm(thisF);
117      FREE(thisF);
118                                                       
119      tableau->abTable[i].notF = 
120        Ctlsp_LtlFormulaHashIntoUniqueTable(nnfF, tableau->formulaUniqueTable);
121      for (j=0; j<tableau->abIndex; j++) {
122        if (tableau->abTable[j].F == tableau->abTable[i].notF) {
123          tableau->abTable[i].notF_idx = j;
124          tableau->abTable[j].notF_idx = i;
125          tableau->abTable[j].notF = tableau->abTable[i].F;
126          break;
127        }
128      }
129      assert(j < tableau->abIndex);
130    }
131    array_insert(int, tableau->abTableNegate, i, tableau->abTable[i].notF_idx);
132  }
133
134  /* put all constant formulae (labels) into tableau->labelTable
135   * includes: ID/NOT(ID) */
136  j = 0;
137  for (i=0; i<tableau->abIndex; i++) {
138    Ctlsp_Formula_t *holdF = tableau->abTable[i].F;
139    if (Ctlsp_LtlFormulaIsPropositional(holdF) &&
140        Ctlsp_FormulaReadType(holdF) != Ctlsp_TRUE_c &&
141        Ctlsp_FormulaReadType(holdF) != Ctlsp_FALSE_c) {
142      tableau->labelTable[j] = tableau->abTable[i].F;
143      Ctlsp_FormulaSetLabelIndex(tableau->abTable[i].F, j);
144      j++;
145    }
146  }
147  tableau->labelIndex = j;
148 
149  /* Create the Negate Method for abTable and labelTable */
150  for (i=0; i<tableau->abIndex; i++) {
151    array_insert(int, tableau->abTableNegate, i,
152                 Ctlsp_FormulaReadABIndex(tableau->abTable[i].notF));
153  }
154  for (i=0; i<tableau->labelIndex; i++) {
155    int idx = Ctlsp_FormulaReadABIndex(tableau->labelTable[i]);
156    array_insert(int, tableau->labelTableNegate, i,
157                 Ctlsp_FormulaReadLabelIndex(tableau->abTable[idx].notF));
158  }
159 
160  /* put all the 'until sub-formulae' into tableau->untilUniqueTable */
161  TableauClearMarks(tableau);
162  TableauLoadUntilSubFormulae(tableau, F);
163 
164  return tableau;
165}
166
167
168/**Function********************************************************************
169
170  Synopsis    [Allocate the data structure of tableau.]
171
172  Description []
173 
174  SideEffects []
175
176******************************************************************************/
177LtlTableau_t *
178LtlTableauCreate(
179  void)
180{
181  LtlTableau_t *tableau = ALLOC(LtlTableau_t, 1);
182  memset(tableau, 0, sizeof(LtlTableau_t));
183
184  tableau->F = tableau->notF = NIL(Ctlsp_Formula_t);
185  tableau->abIndex = 0;
186  tableau->abTable = 0;
187  tableau->abTableNegate = array_alloc(int, 0);
188  tableau->labelTable = 0;
189  tableau->labelTableNegate = array_alloc(int, 0);
190  /* create empty hash tables */
191  tableau->formulaUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
192  tableau->untilUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
193 
194  return tableau;
195} 
196
197
198/**Function********************************************************************
199
200  Synopsis    [Free the tableau data structure.]
201
202  SideEffects []
203
204  SeeAlso     [LtlTableauGenerateTableau]
205
206******************************************************************************/
207void
208LtlTableauFree(
209  LtlTableau_t *tableau)
210{
211  int i;
212  char *tmpstr;
213 
214  /* free all the LTL formulae */
215  for (i=0; i<tableau->abIndex; i++) {
216    if (Ctlsp_FormulaReadType(tableau->abTable[i].F) == Ctlsp_ID_c) {
217      tmpstr = Ctlsp_FormulaReadVariableName(tableau->abTable[i].F);
218      FREE(tmpstr);
219      tmpstr = Ctlsp_FormulaReadValueName(tableau->abTable[i].F);
220      FREE(tmpstr);
221    }
222    FREE(tableau->abTable[i].F);
223  }
224
225  FREE(tableau->abTable);
226  FREE(tableau->labelTable);
227  array_free(tableau->abTableNegate);
228  array_free(tableau->labelTableNegate);
229 
230  st_free_table(tableau->formulaUniqueTable);
231  st_free_table(tableau->untilUniqueTable);
232
233  FREE(tableau);
234}
235
236
237/**Function********************************************************************
238
239  Synopsis    [Print the content of the tableau.]
240
241  SideEffects []
242
243  SeeAlso     [LtlTableauGenerateTableau]
244
245******************************************************************************/
246void 
247LtlTableauPrint(
248  FILE *fp,
249  LtlTableau_t *tableau)
250{
251  int i;
252
253  (void) fprintf(fp, "Tableau Rules for {");
254  Ctlsp_FormulaPrint(fp,tableau->F);
255  (void) fprintf(fp, "} : # of sub-formulae = %d\n", tableau->abIndex);
256   
257  for (i=0; i<tableau->abIndex; i++) {
258    fprintf(fp, "%d   [", i);
259    Ctlsp_FormulaPrint(fp, tableau->abTable[i].F);
260    fprintf(fp, "]\n\t");
261    fprintf(fp, "(%3d * %3d * X%3d) + (%3d * %3d * X%3d) -- notF= %3d\n",
262            tableau->abTable[i].A[0].B[0],
263            tableau->abTable[i].A[0].B[1],
264            tableau->abTable[i].A[0].n,
265            tableau->abTable[i].A[1].B[0],
266            tableau->abTable[i].A[1].B[1],
267            tableau->abTable[i].A[1].n,
268            tableau->abTable[i].notF_idx);
269  }
270}
271
272
273/**Function********************************************************************
274
275  Synopsis    [Return the unique formula 'X F' in the tableu by giving 'F'.]
276
277  Description [If there does not exist, create and hash it into the unique
278  table.]
279 
280  SideEffects []
281
282******************************************************************************/
283Ctlsp_Formula_t *
284LtlTableauGetUniqueXFormula(
285  LtlTableau_t *tableau,
286  Ctlsp_Formula_t *F)
287{
288  Ctlsp_Formula_t *tmpF, *XF;
289 
290  tmpF = Ctlsp_FormulaCreate(Ctlsp_X_c, F, NIL(Ctlsp_Formula_t));
291  XF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
292  FREE(tmpF);
293  XF = Ctlsp_LtlFormulaHashIntoUniqueTable(XF,tableau->formulaUniqueTable);
294
295  return XF;
296}
297
298
299/*---------------------------------------------------------------------------*/
300/* Definition of static functions                                          */
301/*---------------------------------------------------------------------------*/
302
303
304/**Function********************************************************************
305
306  Synopsis    [Clear the marks of all the formula in the tableau.]
307
308  Description []
309 
310  SideEffects []
311
312******************************************************************************/
313static void
314TableauClearMarks(
315  LtlTableau_t *tableau)
316{
317  st_table *tbl = tableau->formulaUniqueTable;
318  st_generator *stgen;
319  Ctlsp_Formula_t *F;
320
321  st_foreach_item(tbl, stgen, &F, NIL(char *)) {
322    Ctlsp_FormulaResetMarked(F);
323  }
324}
325
326
327/**Function********************************************************************
328
329  Synopsis    [Fill out the Alpha-Beta entry table recursively.]
330
331  Description [1) assign each formula F an index and an entry;
332  2) build for each formula F a expansion  ( {A0B0 ^ A0B1} + {A1B0 ^ A1B1} )]
333 
334  SideEffects []
335
336******************************************************************************/
337static int
338TableauRules(
339  LtlTableau_t *tableau,
340  Ctlsp_Formula_t *F)
341{
342  int index;
343  int A0B0=-1, A0B1=-1, A0n=-1;
344  int A1B0=-1, A1B1=-1, A1n=-1;
345  Ctlsp_Formula_t *XF;
346  Ctlsp_Formula_t *F_left, *F_right;
347  Ctlsp_FormulaType F_type;
348 
349  assert( F );
350 
351  if (Ctlsp_FormulaReadMarked(F))
352    return Ctlsp_FormulaReadABIndex(F);
353
354  Ctlsp_FormulaSetMarked(F);
355  index = tableau->abIndex++;
356  Ctlsp_FormulaSetABIndex(F, index);
357
358  F_type = Ctlsp_FormulaReadType(F);
359  F_left = Ctlsp_FormulaReadLeftChild(F);
360  F_right = Ctlsp_FormulaReadRightChild(F);
361 
362  switch(F_type) {
363  case Ctlsp_X_c:
364    TableauRules(tableau, F_left); 
365    A0n = index;
366    break;
367  case Ctlsp_OR_c:
368    A0B0 = TableauRules(tableau, F_left);
369    A1B0 = TableauRules(tableau, F_right);
370    break;
371  case Ctlsp_AND_c:
372    A0B0 = TableauRules(tableau, F_left);
373    A0B1 = TableauRules(tableau, F_right);
374    break;
375  case Ctlsp_U_c:
376    A0B0 = TableauRules(tableau, F_left);
377    A1B0 = TableauRules(tableau, F_right);
378    XF = LtlTableauGetUniqueXFormula(tableau, F);
379    A0n = TableauRules(tableau, XF);
380    break;
381  case Ctlsp_R_c:
382    A0B0 = TableauRules(tableau, F_right);
383    A1B0 = TableauRules(tableau, F_right);
384    A1B1 = TableauRules(tableau, F_left);
385    XF = LtlTableauGetUniqueXFormula(tableau, F);
386    A0n = TableauRules(tableau, XF);
387    break;
388  default:
389    break;
390  }
391 
392  tableau->abTable[index].F = F;
393  tableau->abTable[index].A[0].B[0] = A0B0;
394  tableau->abTable[index].A[0].B[1] = A0B1;
395  tableau->abTable[index].A[1].B[0] = A1B0;
396  tableau->abTable[index].A[1].B[1] = A1B1;
397  tableau->abTable[index].A[0].n = A0n;
398  tableau->abTable[index].A[1].n = A1n;
399 
400  tableau->abTable[index].notF_idx = -1;
401  tableau->abTable[index].notF = NIL(Ctlsp_Formula_t);
402
403  return index;
404}
405
406/**Function********************************************************************
407
408  Synopsis    [Hash the formula 'X F' and its negation in the unique tableau.]
409
410  Description [Construct the 'X F' from the given 'F', and hash it.]
411 
412  SideEffects []
413
414******************************************************************************/
415static void
416HashNextFormulae(
417  LtlTableau_t *tableau,
418  Ctlsp_Formula_t *F)
419{
420  Ctlsp_Formula_t *XF, *NXF, *tmpF;
421  Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F);
422  Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
423  Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
424 
425  switch( F_type ) {
426  case Ctlsp_X_c:
427    HashNextFormulae(tableau, F_left);
428    break;
429  case Ctlsp_OR_c:
430  case Ctlsp_AND_c:
431    HashNextFormulae(tableau, F_left);
432    HashNextFormulae(tableau, F_right);
433    break;
434  case Ctlsp_U_c:
435  case Ctlsp_R_c:
436    HashNextFormulae(tableau, F_left);
437    HashNextFormulae(tableau, F_right);
438    XF = LtlTableauGetUniqueXFormula(tableau, F);     
439    tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, XF, NIL(Ctlsp_Formula_t));
440    NXF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
441    FREE(tmpF);
442    Ctlsp_LtlFormulaHashIntoUniqueTable(NXF,tableau->formulaUniqueTable);
443    break;
444  default:
445    break;
446  }
447}
448
449/**Function********************************************************************
450
451  Synopsis    [Put all the Until sub-formulae in a list.]
452
453  Description []
454 
455  SideEffects []
456
457******************************************************************************/
458static void
459TableauLoadUntilSubFormulae(
460  LtlTableau_t *tableau,
461  Ctlsp_Formula_t *F)
462{
463  char *list;
464  st_table *uniqueTable = tableau->untilUniqueTable;
465  Ctlsp_FormulaType F_type;
466 
467  if (!F)
468    return;
469
470  if (Ctlsp_FormulaReadMarked(F))
471    return;
472
473 
474  Ctlsp_FormulaSetMarked(F);
475  F_type = Ctlsp_FormulaReadType(F);
476  if (F_type == Ctlsp_U_c) {
477    if(!st_is_member(uniqueTable,  F)) {
478      list = (char *) lsCreate();
479      st_insert(uniqueTable,  F, list);
480    }
481    Ctlsp_FormulaSetRhs(Ctlsp_FormulaReadRightChild(F));
482  }
483  if (F_type != Ctlsp_ID_c) {
484    TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadLeftChild(F));
485    TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadRightChild(F));
486  }
487}     
488
Note: See TracBrowser for help on using the repository browser.