#include "ltlInt.h"
Include dependency graph for ltlTableau.c:
Go to the source code of this file.
Functions | |
| static void | TableauClearMarks (LtlTableau_t *tableau) |
| static int | TableauRules (LtlTableau_t *tableau, Ctlsp_Formula_t *F) |
| static void | HashNextFormulae (LtlTableau_t *tableau, Ctlsp_Formula_t *F) |
| static void | TableauLoadUntilSubFormulae (LtlTableau_t *tableau, Ctlsp_Formula_t *F) |
| LtlTableau_t * | LtlTableauGenerateTableau (Ctlsp_Formula_t *formula) |
| LtlTableau_t * | LtlTableauCreate (void) |
| void | LtlTableauFree (LtlTableau_t *tableau) |
| void | LtlTableauPrint (FILE *fp, LtlTableau_t *tableau) |
| Ctlsp_Formula_t * | LtlTableauGetUniqueXFormula (LtlTableau_t *tableau, Ctlsp_Formula_t *F) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ltlTableau.c,v 1.15 2008/04/22 21:22:33 fabio Exp $" |
Function Documentation
| static void HashNextFormulae | ( | LtlTableau_t * | tableau, |
| Ctlsp_Formula_t * | F | ||
| ) | [static] |
Function********************************************************************
Synopsis [Hash the formula 'X F' and its negation in the unique tableau.]
Description [Construct the 'X F' from the given 'F', and hash it.]
SideEffects []
Definition at line 416 of file ltlTableau.c.
{
Ctlsp_Formula_t *XF, *NXF, *tmpF;
Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F);
Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
switch( F_type ) {
case Ctlsp_X_c:
HashNextFormulae(tableau, F_left);
break;
case Ctlsp_OR_c:
case Ctlsp_AND_c:
HashNextFormulae(tableau, F_left);
HashNextFormulae(tableau, F_right);
break;
case Ctlsp_U_c:
case Ctlsp_R_c:
HashNextFormulae(tableau, F_left);
HashNextFormulae(tableau, F_right);
XF = LtlTableauGetUniqueXFormula(tableau, F);
tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, XF, NIL(Ctlsp_Formula_t));
NXF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
FREE(tmpF);
Ctlsp_LtlFormulaHashIntoUniqueTable(NXF,tableau->formulaUniqueTable);
break;
default:
break;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| LtlTableau_t* LtlTableauCreate | ( | void | ) |
Function********************************************************************
Synopsis [Allocate the data structure of tableau.]
Description []
SideEffects []
Definition at line 178 of file ltlTableau.c.
{
LtlTableau_t *tableau = ALLOC(LtlTableau_t, 1);
memset(tableau, 0, sizeof(LtlTableau_t));
tableau->F = tableau->notF = NIL(Ctlsp_Formula_t);
tableau->abIndex = 0;
tableau->abTable = 0;
tableau->abTableNegate = array_alloc(int, 0);
tableau->labelTable = 0;
tableau->labelTableNegate = array_alloc(int, 0);
/* create empty hash tables */
tableau->formulaUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
tableau->untilUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
return tableau;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void LtlTableauFree | ( | LtlTableau_t * | tableau | ) |
Function********************************************************************
Synopsis [Free the tableau data structure.]
SideEffects []
SeeAlso [LtlTableauGenerateTableau]
Definition at line 208 of file ltlTableau.c.
{
int i;
char *tmpstr;
/* free all the LTL formulae */
for (i=0; i<tableau->abIndex; i++) {
if (Ctlsp_FormulaReadType(tableau->abTable[i].F) == Ctlsp_ID_c) {
tmpstr = Ctlsp_FormulaReadVariableName(tableau->abTable[i].F);
FREE(tmpstr);
tmpstr = Ctlsp_FormulaReadValueName(tableau->abTable[i].F);
FREE(tmpstr);
}
FREE(tableau->abTable[i].F);
}
FREE(tableau->abTable);
FREE(tableau->labelTable);
array_free(tableau->abTableNegate);
array_free(tableau->labelTableNegate);
st_free_table(tableau->formulaUniqueTable);
st_free_table(tableau->untilUniqueTable);
FREE(tableau);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| LtlTableau_t* LtlTableauGenerateTableau | ( | Ctlsp_Formula_t * | formula | ) |
AutomaticEnd Function********************************************************************
Synopsis [Generate the 'Tableau' sturcture for the LTL->AUT problem. It first computes the NNF of the input formula, then create the alpha/beta entry table for both the input formula and its negation according the tableau rules, and finally compute the list of 'Until formulae'.]
SideEffects []
SeeAlso [LtlTableauGenerateRules]
Definition at line 71 of file ltlTableau.c.
{
Ctlsp_Formula_t *F, *notF, *tmpF;
LtlTableau_t *tableau;
int save_n;
int i, j;
/* compute the NNF of (formula) and (its negation) */
F = Ctlsp_LtlFormulaNegationNormalForm(formula);
tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula, NIL(Ctlsp_Formula_t));
notF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
FREE(tmpF);
/* Create the 'tableau' for this LTL->AUT problem */
tableau = LtlTableauCreate();
/* Hash F & notF into the unique table */
F = Ctlsp_LtlFormulaHashIntoUniqueTable(F,tableau->formulaUniqueTable);
notF = Ctlsp_LtlFormulaHashIntoUniqueTable(notF,tableau->formulaUniqueTable);
tableau->F = F;
tableau->notF = notF;
/* tricky part:: for each U-formula/R-formula 'F', also hash 'XF' */
TableauClearMarks(tableau);
HashNextFormulae(tableau, F);
/* Build the Alpha/Beta entry table */
tableau->abIndex = st_count(tableau->formulaUniqueTable);
tableau->abTable = ALLOC(LtlTableauEntry_t, tableau->abIndex);
tableau->labelTable = ALLOC(Ctlsp_Formula_t *, tableau->abIndex);
save_n = tableau->abIndex;
tableau->abIndex = 0;
TableauClearMarks(tableau);
TableauRules(tableau,F); /* build the Alpha-Beta table */
TableauRules(tableau, notF);
tableau->abIndex = save_n;
/* compute the negation field (.notF) for each Alpha-Beta entry */
for (i=0; i<tableau->abIndex; i++) {
if (!tableau->abTable[i].notF) {
Ctlsp_Formula_t *thisF = Ctlsp_FormulaCreate(Ctlsp_NOT_c,
tableau->abTable[i].F,
NIL(Ctlsp_Formula_t));
Ctlsp_Formula_t *nnfF = Ctlsp_LtlFormulaNegationNormalForm(thisF);
FREE(thisF);
tableau->abTable[i].notF =
Ctlsp_LtlFormulaHashIntoUniqueTable(nnfF, tableau->formulaUniqueTable);
for (j=0; j<tableau->abIndex; j++) {
if (tableau->abTable[j].F == tableau->abTable[i].notF) {
tableau->abTable[i].notF_idx = j;
tableau->abTable[j].notF_idx = i;
tableau->abTable[j].notF = tableau->abTable[i].F;
break;
}
}
assert(j < tableau->abIndex);
}
array_insert(int, tableau->abTableNegate, i, tableau->abTable[i].notF_idx);
}
/* put all constant formulae (labels) into tableau->labelTable
* includes: ID/NOT(ID) */
j = 0;
for (i=0; i<tableau->abIndex; i++) {
Ctlsp_Formula_t *holdF = tableau->abTable[i].F;
if (Ctlsp_LtlFormulaIsPropositional(holdF) &&
Ctlsp_FormulaReadType(holdF) != Ctlsp_TRUE_c &&
Ctlsp_FormulaReadType(holdF) != Ctlsp_FALSE_c) {
tableau->labelTable[j] = tableau->abTable[i].F;
Ctlsp_FormulaSetLabelIndex(tableau->abTable[i].F, j);
j++;
}
}
tableau->labelIndex = j;
/* Create the Negate Method for abTable and labelTable */
for (i=0; i<tableau->abIndex; i++) {
array_insert(int, tableau->abTableNegate, i,
Ctlsp_FormulaReadABIndex(tableau->abTable[i].notF));
}
for (i=0; i<tableau->labelIndex; i++) {
int idx = Ctlsp_FormulaReadABIndex(tableau->labelTable[i]);
array_insert(int, tableau->labelTableNegate, i,
Ctlsp_FormulaReadLabelIndex(tableau->abTable[idx].notF));
}
/* put all the 'until sub-formulae' into tableau->untilUniqueTable */
TableauClearMarks(tableau);
TableauLoadUntilSubFormulae(tableau, F);
return tableau;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Ctlsp_Formula_t* LtlTableauGetUniqueXFormula | ( | LtlTableau_t * | tableau, |
| Ctlsp_Formula_t * | F | ||
| ) |
Function********************************************************************
Synopsis [Return the unique formula 'X F' in the tableu by giving 'F'.]
Description [If there does not exist, create and hash it into the unique table.]
SideEffects []
Definition at line 284 of file ltlTableau.c.
{
Ctlsp_Formula_t *tmpF, *XF;
tmpF = Ctlsp_FormulaCreate(Ctlsp_X_c, F, NIL(Ctlsp_Formula_t));
XF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
FREE(tmpF);
XF = Ctlsp_LtlFormulaHashIntoUniqueTable(XF,tableau->formulaUniqueTable);
return XF;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void LtlTableauPrint | ( | FILE * | fp, |
| LtlTableau_t * | tableau | ||
| ) |
Function********************************************************************
Synopsis [Print the content of the tableau.]
SideEffects []
SeeAlso [LtlTableauGenerateTableau]
Definition at line 247 of file ltlTableau.c.
{
int i;
(void) fprintf(fp, "Tableau Rules for {");
Ctlsp_FormulaPrint(fp,tableau->F);
(void) fprintf(fp, "} : # of sub-formulae = %d\n", tableau->abIndex);
for (i=0; i<tableau->abIndex; i++) {
fprintf(fp, "%d [", i);
Ctlsp_FormulaPrint(fp, tableau->abTable[i].F);
fprintf(fp, "]\n\t");
fprintf(fp, "(%3d * %3d * X%3d) + (%3d * %3d * X%3d) -- notF= %3d\n",
tableau->abTable[i].A[0].B[0],
tableau->abTable[i].A[0].B[1],
tableau->abTable[i].A[0].n,
tableau->abTable[i].A[1].B[0],
tableau->abTable[i].A[1].B[1],
tableau->abTable[i].A[1].n,
tableau->abTable[i].notF_idx);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TableauClearMarks | ( | LtlTableau_t * | tableau | ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Clear the marks of all the formula in the tableau.]
Description []
SideEffects []
Definition at line 314 of file ltlTableau.c.
{
st_table *tbl = tableau->formulaUniqueTable;
st_generator *stgen;
Ctlsp_Formula_t *F;
st_foreach_item(tbl, stgen, &F, NIL(char *)) {
Ctlsp_FormulaResetMarked(F);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TableauLoadUntilSubFormulae | ( | LtlTableau_t * | tableau, |
| Ctlsp_Formula_t * | F | ||
| ) | [static] |
Function********************************************************************
Synopsis [Put all the Until sub-formulae in a list.]
Description []
SideEffects []
Definition at line 459 of file ltlTableau.c.
{
char *list;
st_table *uniqueTable = tableau->untilUniqueTable;
Ctlsp_FormulaType F_type;
if (!F)
return;
if (Ctlsp_FormulaReadMarked(F))
return;
Ctlsp_FormulaSetMarked(F);
F_type = Ctlsp_FormulaReadType(F);
if (F_type == Ctlsp_U_c) {
if(!st_is_member(uniqueTable, F)) {
list = (char *) lsCreate();
st_insert(uniqueTable, F, list);
}
Ctlsp_FormulaSetRhs(Ctlsp_FormulaReadRightChild(F));
}
if (F_type != Ctlsp_ID_c) {
TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadLeftChild(F));
TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadRightChild(F));
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int TableauRules | ( | LtlTableau_t * | tableau, |
| Ctlsp_Formula_t * | F | ||
| ) | [static] |
Function********************************************************************
Synopsis [Fill out the Alpha-Beta entry table recursively.]
Description [1) assign each formula F an index and an entry; 2) build for each formula F a expansion ( {A0B0 ^ A0B1} + {A1B0 ^ A1B1} )]
SideEffects []
Definition at line 338 of file ltlTableau.c.
{
int index;
int A0B0=-1, A0B1=-1, A0n=-1;
int A1B0=-1, A1B1=-1, A1n=-1;
Ctlsp_Formula_t *XF;
Ctlsp_Formula_t *F_left, *F_right;
Ctlsp_FormulaType F_type;
assert( F );
if (Ctlsp_FormulaReadMarked(F))
return Ctlsp_FormulaReadABIndex(F);
Ctlsp_FormulaSetMarked(F);
index = tableau->abIndex++;
Ctlsp_FormulaSetABIndex(F, index);
F_type = Ctlsp_FormulaReadType(F);
F_left = Ctlsp_FormulaReadLeftChild(F);
F_right = Ctlsp_FormulaReadRightChild(F);
switch(F_type) {
case Ctlsp_X_c:
TableauRules(tableau, F_left);
A0n = index;
break;
case Ctlsp_OR_c:
A0B0 = TableauRules(tableau, F_left);
A1B0 = TableauRules(tableau, F_right);
break;
case Ctlsp_AND_c:
A0B0 = TableauRules(tableau, F_left);
A0B1 = TableauRules(tableau, F_right);
break;
case Ctlsp_U_c:
A0B0 = TableauRules(tableau, F_left);
A1B0 = TableauRules(tableau, F_right);
XF = LtlTableauGetUniqueXFormula(tableau, F);
A0n = TableauRules(tableau, XF);
break;
case Ctlsp_R_c:
A0B0 = TableauRules(tableau, F_right);
A1B0 = TableauRules(tableau, F_right);
A1B1 = TableauRules(tableau, F_left);
XF = LtlTableauGetUniqueXFormula(tableau, F);
A0n = TableauRules(tableau, XF);
break;
default:
break;
}
tableau->abTable[index].F = F;
tableau->abTable[index].A[0].B[0] = A0B0;
tableau->abTable[index].A[0].B[1] = A0B1;
tableau->abTable[index].A[1].B[0] = A1B0;
tableau->abTable[index].A[1].B[1] = A1B1;
tableau->abTable[index].A[0].n = A0n;
tableau->abTable[index].A[1].n = A1n;
tableau->abTable[index].notF_idx = -1;
tableau->abTable[index].notF = NIL(Ctlsp_Formula_t);
return index;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ltlTableau.c,v 1.15 2008/04/22 21:22:33 fabio Exp $" [static] |
CFile***********************************************************************
FileName [ltlTableau.c]
PackageName [ltl]
Synopsis [Expand the LTL Formula by applying the Tableau Rules.]
Author [Chao Wang<chao.wang@colorado.EDU>]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 19 of file ltlTableau.c.
