#include "absInt.h"
Include dependency graph for absTranslate.c:
Go to the source code of this file.
Functions | |
| static AbsVertexInfo_t * | TranslateCtlSubFormula (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | ComputeFairPredicate (AbsVertexCatalog_t *catalog, AbsVertexInfo_t *atomicPredicate, array_t *fairArray, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlID (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity) |
| static AbsVertexInfo_t * | TranslateCtlEU (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlEG (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlEGFair (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlEX (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlNOT (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlTHEN (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlAND (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | TranslateCtlOR (AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds) |
| static AbsVertexInfo_t * | CreateConjunctionChain (AbsVertexCatalog_t *catalog, array_t *conjunctions, int polarity) |
| array_t * | AbsCtlFormulaArrayTranslate (Abs_VerificationInfo_t *verInfo, array_t *formulaArray, array_t *fairArray) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: absTranslate.c,v 1.14 2002/09/04 14:58:18 fabio Exp $" |
Function Documentation
| array_t* AbsCtlFormulaArrayTranslate | ( | Abs_VerificationInfo_t * | verInfo, |
| array_t * | formulaArray, | ||
| array_t * | fairArray | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Translate an array of CTL formulas to an array of labeled operational graphs. The graphs may share vertices among them.]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 69 of file absTranslate.c.
{
AbsVertexCatalog_t *catalog;
Ctlp_Formula_t *formulaPtr;
AbsVertexInfo_t *fairPositive;
AbsVertexInfo_t *fairNegative;
array_t *result;
boolean initialPolarity;
int uniqueIds;
int i;
if (formulaArray == NIL(array_t)) {
return NIL(array_t);
}
/* Initialize certain variables */
catalog = AbsVerificationInfoReadCatalog(verInfo);
uniqueIds = 0;
if (fairArray != NIL(array_t)) {
fairPositive = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t),
fairArray, TRUE, &uniqueIds);
fairNegative = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t),
fairArray, FALSE, &uniqueIds);
}
else {
fairPositive = NIL(AbsVertexInfo_t);
fairNegative = NIL(AbsVertexInfo_t);
}
if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
initialPolarity = TRUE;
}
else {
initialPolarity = FALSE;
}
/* Create the result */
result = array_alloc(AbsVertexInfo_t *, array_n(formulaArray));
arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formulaPtr) {
AbsVertexInfo_t *resultPtr;
/* Translate the formula */
resultPtr = TranslateCtlSubFormula(AbsVerificationInfoReadCatalog(verInfo),
formulaPtr, /* Formula */
fairArray, /* Fairness
constraints */
fairPositive, /* Predicate fair
with positive
polarity */
fairNegative, /* Predicate fair
with negative
polarity */
initialPolarity, /* Initial polarity */
&uniqueIds); /* Unique id counter */
/* Negate the formula if needed */
if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
AbsVertexInfo_t *newResult;
/* If the formula's top vertex is a negation, eliminate the redundancy */
if (AbsVertexReadType(resultPtr) == not_c) {
newResult = AbsVertexReadLeftKid(resultPtr);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
resultPtr = newResult;
}
else {
/* Create the not vertex */
newResult = AbsVertexCatalogFindOrAdd(catalog, not_c, FALSE,
resultPtr,
NIL(AbsVertexInfo_t), 0,
NIL(char),
NIL(char));
if (AbsVertexReadType(newResult) == false_c) {
AbsVertexSetPolarity(newResult, FALSE);
AbsVertexSetDepth(newResult, AbsVertexReadDepth(resultPtr) + 1);
AbsVertexSetType(newResult, not_c);
AbsVertexSetLeftKid(newResult, resultPtr);
AbsVertexSetParent(resultPtr, newResult);
}
else {
AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
}
resultPtr = newResult;
}
} /* If the formula needs to be negated */
/* Set the constant bit */
AbsFormulaSetConstantBit(resultPtr);
array_insert(AbsVertexInfo_t *, result, i, resultPtr);
}
/* Clean up */
if (fairPositive != NIL(AbsVertexInfo_t)) {
AbsVertexFree(catalog, fairPositive, NIL(AbsVertexInfo_t));
}
if (fairNegative != NIL(AbsVertexInfo_t)) {
AbsVertexFree(catalog, fairNegative, NIL(AbsVertexInfo_t));
}
#ifndef NDEBUG
{
AbsVertexInfo_t *operationGraph;
st_table *rootTable = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
st_insert(rootTable, (char *) operationGraph, NIL(char));
}
arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
assert(AbsFormulaSanityCheck(operationGraph, rootTable));
}
st_free_table(rootTable);
}
#endif
return result;
} /* End of AbsCtlFormulaArrayTranslate */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * ComputeFairPredicate | ( | AbsVertexCatalog_t * | catalog, |
| AbsVertexInfo_t * | atomicPredicate, | ||
| array_t * | fairArray, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate "fair"]
Description [Given a set of formulas f_1,...,f_n compute the predicate fair which is computed as follows: fair(p) = nu(x).(p * Product(i=1,n)(EX[E[p U (x f_i)]])). The final graph will have in its top vertex the polarity given as a parameter to the routine.]
SideEffects []
SeeAlso [AbsCtlFormulaArrayTranslate]
Definition at line 310 of file absTranslate.c.
{
Ctlp_Formula_t *ctlPtr;
AbsVertexInfo_t *mainVarVertex;
AbsVertexInfo_t *mainVarNotVertex;
AbsVertexInfo_t *vertexPtr;
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
AbsVertexInfo_t *aux3;
array_t *conjunctions;
array_t *constraintArray;
int mainVarId;
int i;
/* Obtain the representation of the fairness predicates */
constraintArray = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlPtr) {
array_insert(AbsVertexInfo_t *, constraintArray, i,
TranslateCtlSubFormula(catalog, ctlPtr, NIL(array_t),
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t), polarity,
uniqueIds));
}
/* Create the vertex representing the variable of the greatest fixed point */
mainVarId = (*uniqueIds)++;
aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity,
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t),
mainVarId, NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, 1);
AbsVertexSetType(aux1, variable_c);
AbsVertexSetVarId(aux1, mainVarId);
}
mainVarVertex = aux1;
mainVarNotVertex = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
NIL(AbsVertexInfo_t), 0,
NIL(char), NIL(char));
if (AbsVertexReadType(mainVarNotVertex) == false_c) {
AbsVertexSetPolarity(mainVarNotVertex, polarity);
AbsVertexSetDepth(mainVarNotVertex, 2);
AbsVertexSetType(mainVarNotVertex, not_c);
AbsVertexSetLeftKid(mainVarNotVertex, aux1);
AbsVertexSetParent(mainVarVertex, mainVarNotVertex);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the predicates EX[E[f U z * f_i]] */
conjunctions = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
arrayForEachItem(AbsVertexInfo_t *, constraintArray, i, vertexPtr) {
AbsVertexInfo_t *varVertex;
int variableId;
/* Create the conjunction between z and f_i */
AbsVertexReadRefs(mainVarNotVertex)++;
aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, vertexPtr,
mainVarNotVertex, 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
if (AbsVertexReadDepth(vertexPtr) > 2) {
AbsVertexSetDepth(aux1, AbsVertexReadDepth(vertexPtr) + 1);
}
else {
AbsVertexSetDepth(aux1, 3);
}
AbsVertexSetType(aux1, and_c);
AbsVertexSetLeftKid(aux1, vertexPtr);
AbsVertexSetRightKid(aux1, mainVarNotVertex);
AbsVertexSetParent(vertexPtr, aux1);
AbsVertexSetParent(mainVarNotVertex, aux1);
}
else {
/* Cache hit */
AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, mainVarNotVertex, NIL(AbsVertexInfo_t));
}
/* Create the vertex negating the previous conjunction */
aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, not_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the variable of the fixed point in the EU sub-formula*/
variableId = (*uniqueIds)++;
aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t), variableId,
NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, 1);
AbsVertexSetType(aux1, variable_c);
AbsVertexSetVarId(aux1, variableId);
}
varVertex = aux1;
/* Create the vertex storing the preimage sub-formula */
aux3 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
aux1, NIL(AbsVertexInfo_t),
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux3) == false_c) {
AbsVertexSetPolarity(aux3, polarity);
AbsVertexSetDepth(aux3, 2);
AbsVertexSetType(aux3, preImage_c);
AbsVertexSetLeftKid(aux3, aux1);
AbsVertexSetParent(aux1, aux3);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
if (atomicPredicate != NIL(AbsVertexInfo_t)) {
AbsVertexReadRefs(atomicPredicate)++;
/* Create the vertex representing the and */
aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
atomicPredicate, aux3, 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
if (AbsVertexReadDepth(atomicPredicate) > 2) {
AbsVertexSetDepth(aux1, AbsVertexReadDepth(atomicPredicate) + 1);
}
else {
AbsVertexSetDepth(aux1, 3);
}
AbsVertexSetType(aux1, and_c);
AbsVertexSetLeftKid(aux1, atomicPredicate);
AbsVertexSetRightKid(aux1, aux3);
AbsVertexSetParent(atomicPredicate, aux1);
AbsVertexSetParent(aux3, aux1);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
}
}
else {
aux1 = aux3;
}
/* Create the not vertex on top of the conjunction */
aux3 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux3) == false_c) {
AbsVertexSetPolarity(aux3, !polarity);
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux3, not_c);
AbsVertexSetLeftKid(aux3, aux1);
AbsVertexSetParent(aux1, aux3);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Vertex taking the conjunction */
aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux2, aux3,
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
if (AbsVertexReadDepth(aux2) > AbsVertexReadDepth(aux3)) {
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
}
else {
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
}
AbsVertexSetType(aux1, and_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetRightKid(aux1, aux3);
AbsVertexSetParent(aux3, aux1);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* negation of the conjunction */
aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, not_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the lfp vertex for the EU operator */
aux1 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(aux1, fixedPoint_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetFpVar(aux1, varVertex);
AbsVertexSetUseExtraCareSet(aux1, TRUE);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* Create the final EX vertex on top of the EU */
aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
aux1, NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, preImage_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
array_insert(AbsVertexInfo_t *, conjunctions, i, aux2);
} /* End of the loop iterating over the fairness constraints */
AbsVertexReadRefs(mainVarNotVertex)--;
/* Create the chain of ands for the conjunctions */
aux1 = CreateConjunctionChain(catalog, conjunctions, polarity);
/* Create the and with the atomic predicate if required */
if (atomicPredicate != NIL(AbsVertexInfo_t)) {
aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, atomicPredicate,
aux1, 0, NIL(char), NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(atomicPredicate)) {
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
}
else {
AbsVertexSetDepth(aux2, AbsVertexReadDepth(atomicPredicate) + 1);
}
AbsVertexSetType(aux2, and_c);
AbsVertexSetLeftKid(aux2, atomicPredicate);
AbsVertexSetRightKid(aux2, aux1);
AbsVertexSetParent(atomicPredicate, aux2);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
}
}
else {
aux2 = aux1;
}
/* Create the not vertex on top of the conjunction */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* Create the top most fixed point vertex */
aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
NIL(AbsVertexInfo_t), mainVarId,
NIL(char), NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, fixedPoint_c);
AbsVertexSetVarId(aux2, mainVarId);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetFpVar(aux2, mainVarVertex);
AbsVertexSetUseExtraCareSet(aux2, FALSE);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexSetUseExtraCareSet(aux2, FALSE);
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the top most vertex */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* Clean up */
array_free(constraintArray);
arrayForEachItem(AbsVertexInfo_t *, conjunctions, i, vertexPtr) {
AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
}
array_free(conjunctions);
return aux1;
} /* End of ComputeFairPredicate */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * CreateConjunctionChain | ( | AbsVertexCatalog_t * | catalog, |
| array_t * | conjunctions, | ||
| int | polarity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Given an array containing vertices, creates the conjunction of all of them.]
SideEffects []
SeeAlso [ComputeFairPredicate]
Definition at line 1596 of file absTranslate.c.
{
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
AbsVertexInfo_t *aux3;
int i;
assert(conjunctions != NIL(array_t));
aux1 = array_fetch(AbsVertexInfo_t *, conjunctions, 0);
AbsVertexReadRefs(aux1)++;
if (array_n(conjunctions) == 1) {
return aux1;
}
for (i=1; i<array_n(conjunctions); i++) {
aux2 = array_fetch(AbsVertexInfo_t *, conjunctions, i);
AbsVertexReadRefs(aux2)++;
aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, aux1, aux2, 0,
NIL(char), NIL(char));
if (AbsVertexReadType(aux3) == false_c) {
AbsVertexSetPolarity(aux3, polarity);
if (AbsVertexReadDepth(aux1) < AbsVertexReadDepth(aux2)) {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
}
else {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
}
AbsVertexSetType(aux3, and_c);
AbsVertexSetLeftKid(aux3, aux1);
AbsVertexSetRightKid(aux3, aux2);
AbsVertexSetParent(aux1, aux3);
AbsVertexSetParent(aux2, aux3);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
aux1 = aux3;
}
return aux1;
} /* End of CreateConjunctionChain */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlAND | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate of the form p AND q]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1408 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *leftResult, *rightResult;
int leftDepth;
int rightDepth;
leftResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
rightResult= TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadRightChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* Read the depths */
leftDepth = AbsVertexReadDepth(leftResult);
rightDepth = AbsVertexReadDepth(rightResult);
result = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult,
rightResult, 0, NIL(char), NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
if (leftDepth > rightDepth) {
AbsVertexSetDepth(result, leftDepth + 1);
}
else {
AbsVertexSetDepth(result, rightDepth + 1);
}
AbsVertexSetType(result, and_c);
AbsVertexSetLeftKid(result, leftResult);
AbsVertexSetRightKid(result, rightResult);
AbsVertexSetParent(leftResult, result);
AbsVertexSetParent(rightResult, result);
}
else {
AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlAND */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlEG | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of a formula of the form EG(p)]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 953 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *varVertex;
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
AbsVertexInfo_t *childResult;
int variableId;
/* Allocate a unique id for the fixed point */
variableId = (*uniqueIds)++;
/* Create the vertex storing the fixed point variable */
aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity,
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t),
variableId, NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, 1);
AbsVertexSetType(aux1, variable_c);
AbsVertexSetVarId(aux1, variableId);
}
varVertex = aux1;
/* Create the vertex to negate the variable of the fixed point */
aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
AbsVertexSetDepth(aux2, 2);
AbsVertexSetType(aux2, not_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the vertex storing the preimage sub-formula */
aux1 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
aux1, NIL(AbsVertexInfo_t),
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, 3);
AbsVertexSetType(aux1, preImage_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
/* Create the vertex representing the sub-formula of EG */
childResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
NIL(array_t), NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t), polarity,
uniqueIds);
/* Create the vertex representing the and */
aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, childResult,
aux1, 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
if (AbsVertexReadDepth(childResult) > 2) {
AbsVertexSetDepth(aux2, AbsVertexReadDepth(childResult) + 1);
}
else {
AbsVertexSetDepth(aux2, 4);
}
AbsVertexSetType(aux2, and_c);
AbsVertexSetLeftKid(aux2, childResult);
AbsVertexSetRightKid(aux2, aux1);
AbsVertexSetParent(childResult, aux2);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
}
}
else {
aux2 = aux1;
}
/* Create the not vertex on top of the conjunction */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, aux2);
AbsVertexSetParent(aux2, aux1);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* Create the fixedpoint_c vertex */
aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
NIL(AbsVertexInfo_t), variableId,
NIL(char), NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, fixedPoint_c);
AbsVertexSetVarId(aux2, variableId);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetFpVar(aux2, varVertex);
AbsVertexSetUseExtraCareSet(aux2, FALSE);
AbsVertexSetParent(aux1, aux2);
}
else {
AbsVertexSetUseExtraCareSet(aux2, FALSE);
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Create the top most not vertex */
result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(result, not_c);
AbsVertexSetLeftKid(result, aux2);
AbsVertexSetParent(aux2, result);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlEG */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlEGFair | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of a predicate of the form EGfair(f)]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1110 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *childResult;
if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) == Ctlp_TRUE_c) {
if (polarity) {
result = fairPositive;
AbsVertexReadRefs(fairPositive)++;
}
else {
result = fairNegative;
AbsVertexReadRefs(fairNegative)++;
}
}
else {
childResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
result = ComputeFairPredicate(catalog, childResult, fairArray, polarity,
uniqueIds);
}
return result;
} /* End of TranslateCtlEGFair */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlEU | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of a formula of the form E(pUq)]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 703 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *leftResult;
AbsVertexInfo_t *rightResult;
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
AbsVertexInfo_t *aux3;
AbsVertexInfo_t *varVertex;
int variableId;
/* Allocate a unique id for the fixed point */
variableId = (*uniqueIds)++;
/* Create the vertex storing the fixed point variable */
aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t), variableId,
NIL(char), NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, 1);
AbsVertexSetType(aux1, variable_c);
AbsVertexSetVarId(aux1, variableId);
}
varVertex = aux1;
/* Create the vertex storing the preimage sub-formula */
aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
aux1, NIL(AbsVertexInfo_t),
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, polarity);
AbsVertexSetDepth(aux2, 2);
AbsVertexSetType(aux2, preImage_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
/* Compute the value of the sub-formula */
leftResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* Create the vertex representing the and */
aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, aux2,
0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
if (AbsVertexReadDepth(leftResult) > 2) {
AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
}
else {
AbsVertexSetDepth(aux1, 3);
}
AbsVertexSetType(aux1, and_c);
AbsVertexSetLeftKid(aux1, leftResult);
AbsVertexSetRightKid(aux1, aux2);
AbsVertexSetParent(leftResult, aux1);
AbsVertexSetParent(aux2, aux1);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
}
} /* if type is TRUE */
else {
aux1 = aux2;
}
/* Create the not vertex on top of the conjunction */
aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(aux2, not_c);
AbsVertexSetLeftKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
}
else {
/* Cache hit */
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Evaluate the right operand of the EU */
rightResult= TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadRightChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* check if there are fairness constraints */
if (fairPositive != NIL(AbsVertexInfo_t)) {
AbsVertexInfo_t *fairness;
AbsVertexInfo_t *conjunction;
/* The negative polarity version of the fairness must be present as well */
assert(fairNegative != NIL(AbsVertexInfo_t));
/* Select the apropriate representation of the fairness constraint */
if (polarity) {
fairness = fairPositive;
}
else {
fairness = fairNegative;
}
AbsVertexReadRefs(fairness)++;
conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
rightResult, fairness, 0, NIL(char),
NIL(char));
if (AbsVertexReadType(conjunction) == false_c) {
int leftDepth;
int rightDepth;
leftDepth = AbsVertexReadDepth(rightResult);
rightDepth = AbsVertexReadDepth(fairness);
AbsVertexSetPolarity(conjunction, polarity);
if (leftDepth > rightDepth) {
AbsVertexSetDepth(conjunction, leftDepth + 1);
}
else {
AbsVertexSetDepth(conjunction, rightDepth + 1);
}
AbsVertexSetType(conjunction, and_c);
AbsVertexSetLeftKid(conjunction, rightResult);
AbsVertexSetRightKid(conjunction, fairness);
AbsVertexSetParent(rightResult, conjunction);
AbsVertexSetParent(fairness, conjunction);
}
else {
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
}
rightResult = conjunction;
}
/* If the sub-formula's top vertex is a negation, eliminate the redundancy */
if (AbsVertexReadType(rightResult) == not_c) {
AbsVertexInfo_t *newResult;
newResult = AbsVertexReadLeftKid(rightResult);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
aux1 = newResult;
}
else {
/* Vertex negating second operand */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, rightResult);
AbsVertexSetParent(rightResult, aux1);
}
else {
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
}
}
/* Vertex taking the conjunction */
aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux3) == false_c) {
AbsVertexSetPolarity(aux3, !polarity);
if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
}
else {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
}
AbsVertexSetType(aux3, and_c);
AbsVertexSetLeftKid(aux3, aux1);
AbsVertexSetRightKid(aux3, aux2);
AbsVertexSetParent(aux1, aux3);
AbsVertexSetParent(aux2, aux3);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* negation of the conjunction */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, aux3);
AbsVertexSetParent(aux3, aux1);
}
else {
AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
}
/* Top vertex fixed point operator */
result = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux1,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(aux1) + 1);
AbsVertexSetType(result, fixedPoint_c);
AbsVertexSetLeftKid(result, aux1);
AbsVertexSetFpVar(result, varVertex);
AbsVertexSetUseExtraCareSet(result, TRUE);
AbsVertexSetParent(aux1, result);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlEU */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlEX | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate EX(p)]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1156 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *childResult;
/* Translate the sub-formula regardless */
childResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* check if there are fairness constraints */
if (fairPositive != NIL(AbsVertexInfo_t)) {
AbsVertexInfo_t *fairness;
AbsVertexInfo_t *conjunction;
/* The negative polarity version of the fairness must be present as well */
assert(fairNegative != NIL(AbsVertexInfo_t));
/* Select the apropriate representation of the fairness constraint */
if (polarity) {
fairness = fairPositive;
}
else {
fairness = fairNegative;
}
AbsVertexReadRefs(fairness)++;
conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
childResult, fairness, 0, NIL(char),
NIL(char));
if (AbsVertexReadType(conjunction) == false_c) {
int leftDepth;
int rightDepth;
leftDepth = AbsVertexReadDepth(childResult);
rightDepth = AbsVertexReadDepth(fairness);
AbsVertexSetPolarity(conjunction, polarity);
if (leftDepth > rightDepth) {
AbsVertexSetDepth(conjunction, leftDepth + 1);
}
else {
AbsVertexSetDepth(conjunction, rightDepth + 1);
}
AbsVertexSetType(conjunction, and_c);
AbsVertexSetLeftKid(conjunction, childResult);
AbsVertexSetRightKid(conjunction, fairness);
AbsVertexSetParent(childResult, conjunction);
AbsVertexSetParent(fairness, conjunction);
}
else {
AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
}
childResult = conjunction;
}
/* Create the preImage vertex */
result = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
childResult, NIL(AbsVertexInfo_t), 0,
NIL(char), NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
AbsVertexSetType(result, preImage_c);
AbsVertexSetLeftKid(result, childResult);
AbsVertexSetParent(childResult, result);
}
else {
AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlEX */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlID | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| int | polarity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational grarph representation of an atomic predicate]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 664 of file absTranslate.c.
{
AbsVertexInfo_t *result;
result = AbsVertexCatalogFindOrAdd(catalog,
identifier_c,
polarity,
NIL(AbsVertexInfo_t),
NIL(AbsVertexInfo_t),
0,
Ctlp_FormulaReadVariableName(formula),
Ctlp_FormulaReadValueName(formula));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, 1);
AbsVertexSetType(result, identifier_c);
AbsVertexSetName(result,
util_strsav(Ctlp_FormulaReadVariableName(formula)));
AbsVertexSetValue(result,
util_strsav(Ctlp_FormulaReadValueName(formula)));
}
return result;
} /* End of TranslateCtlID */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlNOT | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate NOT(p)]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1251 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *childResult;
childResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
!polarity, uniqueIds);
/* If the sub-formula's top vertex is a negation, eliminate the redundancy */
if (AbsVertexReadType(childResult) == not_c) {
AbsVertexInfo_t *newResult;
newResult = AbsVertexReadLeftKid(childResult);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
return newResult;
}
/* Create the not vertex */
result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, childResult,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
AbsVertexSetType(result, not_c);
AbsVertexSetLeftKid(result, childResult);
AbsVertexSetParent(childResult, result);
}
else {
AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlNOT */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlOR | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate of the for p OR q]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1470 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *leftResult, *rightResult;
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
AbsVertexInfo_t *aux3;
leftResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
rightResult= TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadRightChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* If the sub-formula's top vertex is a negation, eliminate the redundancy */
if (AbsVertexReadType(leftResult) == not_c) {
AbsVertexInfo_t *newResult;
newResult = AbsVertexReadLeftKid(leftResult);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
aux1 = newResult;
}
else {
/* Vertex negating first operand */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, leftResult,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, leftResult);
AbsVertexSetParent(leftResult, aux1);
}
else {
AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
}
}
if (AbsVertexReadType(rightResult) == not_c) {
AbsVertexInfo_t *newResult;
newResult = AbsVertexReadLeftKid(rightResult);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
aux2 = newResult;
}
else {
/* Vertex negating second operand */
aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
AbsVertexSetDepth(aux2, AbsVertexReadDepth(rightResult) + 1);
AbsVertexSetType(aux2, not_c);
AbsVertexSetLeftKid(aux2, rightResult);
AbsVertexSetParent(rightResult, aux2);
}
else {
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
}
}
/* Vertex taking the conjunction */
aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
0, NIL(char), NIL(char));
if (AbsVertexReadType(aux3) == false_c) {
AbsVertexSetPolarity(aux3, !polarity);
if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
}
else {
AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
}
AbsVertexSetType(aux3, and_c);
AbsVertexSetLeftKid(aux3, aux1);
AbsVertexSetRightKid(aux3, aux2);
AbsVertexSetParent(aux1, aux3);
AbsVertexSetParent(aux2, aux3);
}
else {
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
/* Top vertex negation of the conjunction */
result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(aux3) + 1);
AbsVertexSetType(result, not_c);
AbsVertexSetLeftKid(result, aux3);
AbsVertexSetParent(aux3, result);
}
else {
AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlOR */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlSubFormula | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Recursive formula to translate a formula to its operational graph]
Description [This function is just a case to call the specific translation routines for the different types of sub-formulas]
SideEffects []
SeeAlso [TranslateCtlId, TranslateCtlEG, TranslateCtlEGFair, TranslateCtlEU, TranslateCtlEX, TranslateCtlNOT, TranslateCtlTHEN, TranslateCtlAND, TranslateCtlOR]
Definition at line 215 of file absTranslate.c.
{
AbsVertexInfo_t *result;
result = NIL(AbsVertexInfo_t);
switch (Ctlp_FormulaReadType(formula)) {
case Ctlp_TRUE_c:
case Ctlp_FALSE_c: {
(void) fprintf(vis_stderr, "** abs error: Error in TranslateCtlSubFormula. ");
(void) fprintf(vis_stderr, "TRUE/FALSE constant found.\n");
result = NIL(AbsVertexInfo_t);
break;
}
case Ctlp_ID_c: {
result = TranslateCtlID(catalog, formula, polarity);
break;
}
case Ctlp_EG_c: {
if (fairArray == NIL(array_t)) {
result = TranslateCtlEG(catalog, formula, polarity, uniqueIds);
}
else {
result = TranslateCtlEGFair(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
}
break;
}
case Ctlp_EU_c: {
result = TranslateCtlEU(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
case Ctlp_EX_c: {
result = TranslateCtlEX(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
case Ctlp_NOT_c: {
result = TranslateCtlNOT(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
case Ctlp_THEN_c: {
result = TranslateCtlTHEN(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
case Ctlp_EQ_c:
case Ctlp_XOR_c: {
/* Non-monotonic operators should have been replaced before
* reaching this point.
*/
fail("Encountered unexpected type of CTL formula\n");
break;
}
case Ctlp_AND_c: {
result = TranslateCtlAND(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
case Ctlp_OR_c: {
result = TranslateCtlOR(catalog, formula, fairArray, fairPositive,
fairNegative, polarity, uniqueIds);
break;
}
default: fail("Encountered unknown type of CTL formula\n");
}
return result;
} /* End of TranslateCtlSubFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| static AbsVertexInfo_t * TranslateCtlTHEN | ( | AbsVertexCatalog_t * | catalog, |
| Ctlp_Formula_t * | formula, | ||
| array_t * | fairArray, | ||
| AbsVertexInfo_t * | fairPositive, | ||
| AbsVertexInfo_t * | fairNegative, | ||
| int | polarity, | ||
| int * | uniqueIds | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the operational graph representation of the predicate of the form p -> q]
SideEffects []
SeeAlso [TranslateCtlSubFormula]
Definition at line 1308 of file absTranslate.c.
{
AbsVertexInfo_t *result;
AbsVertexInfo_t *leftResult, *rightResult;
AbsVertexInfo_t *aux1;
AbsVertexInfo_t *aux2;
leftResult = TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadLeftChild(formula),
fairArray, fairPositive, fairNegative,
!polarity, uniqueIds);
rightResult= TranslateCtlSubFormula(catalog,
Ctlp_FormulaReadRightChild(formula),
fairArray, fairPositive, fairNegative,
polarity, uniqueIds);
/* If the sub-formula's top vertex is a negation, eliminate the redundancy */
if (AbsVertexReadType(rightResult) == not_c) {
AbsVertexInfo_t *newResult;
newResult = AbsVertexReadLeftKid(rightResult);
AbsVertexReadRefs(newResult)++;
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
aux1 = newResult;
}
else {
/* Vertex negating first operand */
aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(aux1) == false_c) {
AbsVertexSetPolarity(aux1, !polarity);
AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
AbsVertexSetType(aux1, not_c);
AbsVertexSetLeftKid(aux1, rightResult);
AbsVertexSetParent(rightResult, aux1);
}
else {
AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
}
}
/* Result node holding the and of both operands */
aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, leftResult,
aux1, 0, NIL(char), NIL(char));
if (AbsVertexReadType(aux2) == false_c) {
AbsVertexSetPolarity(aux2, !polarity);
if (AbsVertexReadDepth(leftResult) > AbsVertexReadDepth(aux1)) {
AbsVertexSetDepth(aux2, AbsVertexReadDepth(leftResult) + 1);
}
else {
AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
}
AbsVertexSetType(aux2, and_c);
AbsVertexSetLeftKid(aux2, leftResult);
AbsVertexSetRightKid(aux2, aux1);
AbsVertexSetParent(aux1, aux2);
AbsVertexSetParent(leftResult, aux2);
}
else {
AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
}
/* Top vertex negation of the conjunction */
result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
NIL(AbsVertexInfo_t), 0, NIL(char),
NIL(char));
if (AbsVertexReadType(result) == false_c) {
AbsVertexSetPolarity(result, polarity);
AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
AbsVertexSetType(result, not_c);
AbsVertexSetLeftKid(result, aux2);
AbsVertexSetParent(aux2, result);
}
else {
AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
}
return result;
} /* End of TranslateCtlTHEN */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: absTranslate.c,v 1.14 2002/09/04 14:58:18 fabio Exp $" [static] |
CFile***********************************************************************
FileName [absTranslate.c]
PackageName [abs]
Synopsis [Functions to translate CTL formulas to mu-calculus graphs.]
Author [Abelardo Pardo <abel@vlsi.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 20 of file absTranslate.c.
