#include "absInt.h"
Include dependency graph for absRefine.c:
Go to the source code of this file.
Functions | |
| static mdd_t * | RefineVariable (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static mdd_t * | RefineIdentifier (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static mdd_t * | RefineNot (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static mdd_t * | RefineAnd (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static mdd_t * | RefineFixedPoint (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static mdd_t * | RefineFixedPointIterate (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet, int iterateNumber) |
| static mdd_t * | RefinePreImage (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
| static boolean | RestoreContainment (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static int | PruneIterateVector (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) |
| static mdd_t * | SuccessTest (mdd_t *sat, mdd_t *goalSet, boolean polarity) |
| mdd_t * | AbsSubFormulaRefine (Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: absRefine.c,v 1.24 2002/09/19 05:25:01 fabio Exp $" |
Function Documentation
| mdd_t* AbsSubFormulaRefine | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Refine a given sub-formula]
Description [This function just checks for some trivial cases and then calls the appropriate refinement function depending on the type of the formula]
SideEffects []
SeeAlso [RefineAnd, RefineFixedPoint, RefineNot, RefinePreImage, RefineIdentifier, RefineVariable]
Definition at line 74 of file absRefine.c.
{
AbsStats_t *stats;
mdd_manager *mddManager;
mdd_t *oldTmpCareSet = NIL(mdd_t);
mdd_t *realGoalSet;
mdd_t *result;
long verbosity;
verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
stats = AbsVerificationInfoReadStats(absInfo);
mddManager = AbsVerificationInfoReadMddManager(absInfo);
if (verbosity & ABS_VB_REFINE) {
(void) fprintf(vis_stdout, "ABS: Beginning Refinement of Vertex(%3d)\n",
AbsVertexReadId(vertexPtr));
}
/* If the goal set is empty, do not refine */
if (mdd_is_tautology(goalSet, 0)) {
if (verbosity & ABS_VB_GOALSZ) {
(void) fprintf(vis_stdout,
"ABS: Empty Goal in Refinement of Vertex(%3d)\n",
AbsVertexReadId(vertexPtr));
}
/* Set the refine flag */
AbsVertexSetTrueRefine(vertexPtr, TRUE);
return mdd_dup(goalSet);
}
realGoalSet = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet,
AbsVertexReadPolarity(vertexPtr));
/* If the vertex is refined already do not try to refine it */
if (mdd_is_tautology(realGoalSet, 0) ||
!AbsVertexReadGlobalApprox(vertexPtr)) {
if (verbosity & ABS_VB_GOALSZ) {
(void) fprintf(vis_stdout,
"ABS: Quick (%d,%d) Refinement of Vertex(%3d)\n",
mdd_is_tautology(realGoalSet, 0)? 1: 0,
AbsVertexReadGlobalApprox(vertexPtr)? 0: 1,
AbsVertexReadId(vertexPtr));
}
AbsVertexSetTrueRefine(vertexPtr, TRUE);
return realGoalSet;
}
if (verbosity & ABS_VB_GOALSZ) {
(void) fprintf(vis_stdout, "ABS: Received Goal Set-> ");
(void) fprintf(vis_stdout, "%d Nodes\n",
mdd_size(realGoalSet));
if (verbosity & ABS_VB_GLCUBE) {
AbsBddPrintMinterms(realGoalSet);
}
}
mdd_free(realGoalSet);
/* If the current vertex has more than one parent, the temporary care set
* must be reset (because it depends on the path that led to this vertex) */
if (lsLength(vertexPtr->parent) > 1) {
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
}
switch (AbsVertexReadType(vertexPtr)) {
case fixedPoint_c:
result = RefineFixedPoint(absInfo, vertexPtr, goalSet);
AbsStatsReadRefineFixedPoint(stats)++;
break;
case and_c:
result = RefineAnd(absInfo, vertexPtr, goalSet);
AbsStatsReadRefineAnd(stats)++;
break;
case not_c:
result = RefineNot(absInfo, vertexPtr, goalSet);
AbsStatsReadRefineNot(stats)++;
break;
case preImage_c:
result = RefinePreImage(absInfo, vertexPtr, goalSet);
AbsStatsReadRefinePreImage(stats)++;
break;
case identifier_c:
result = RefineIdentifier(absInfo, vertexPtr, goalSet);
AbsStatsReadRefineIdentifier(stats)++;
break;
case variable_c:
result = RefineVariable(absInfo, vertexPtr, goalSet);
AbsStatsReadRefineVariable(stats)++;
break;
default: fail("Encountered unknown type of vertex\n");
}
if (verbosity & ABS_VB_REFINE) {
(void) fprintf(vis_stdout,
"ABS: Done Refining Vertex(%3d).\n",
AbsVertexReadId(vertexPtr));
}
if (verbosity & ABS_VB_GOALSZ) {
(void) fprintf(vis_stdout, "ABS: Returned Goal Set-> ");
(void) fprintf(vis_stdout, "%d Nodes\n",
mdd_size(result));
if (verbosity & ABS_VB_GLCUBE) {
AbsBddPrintMinterms(result);
}
}
if (verbosity & ABS_VB_REFVTX) {
AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
}
if (lsLength(vertexPtr->parent) > 1) {
/* Restore the old temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
}
return result;
} /* End of AbsSubFormulaRefine */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int PruneIterateVector | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Detect early convergence in the iterations of a fix-point]
Description [After the refinement process has modified the iterations of the fix-point and the containment relation has been restored, it could happen that two iterations in the middle of the chain are identical. This is an early termination condition and the sequence of iterations needs to be pruned]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 917 of file absRefine.c.
{
array_t *newRings;
array_t *newRingApprox;
array_t *newSubApprox;
mdd_t *current;
mdd_t *previous;
mdd_t *careSet;
int numIterates;
int index;
/* Read the care Set */
careSet = AbsVerificationInfoReadCareSet(absInfo);
/* Read the number of iterates initially in the vertex */
numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
assert(numIterates > 0);
/* If there are only two iterates, no pruning is needed */
if (numIterates < 2) {
return numIterates;
}
/* Allocate the new arrays to store the new iterates */
newRings = array_alloc(mdd_t *, 0);
newRingApprox = array_alloc(boolean, 0);
newSubApprox = array_alloc(boolean, 0);
/* Initial values for the loop */
index = 1;
previous = AbsVertexFetchRing(vertexPtr, index - 1);
current = AbsVertexFetchRing(vertexPtr, index);
array_insert_last(mdd_t *, newRings, mdd_dup(previous));
array_insert_last(boolean, newRingApprox,
AbsVertexFetchRingApprox(vertexPtr, index - 1));
array_insert_last(boolean, newSubApprox,
AbsVertexFetchSubApprox(vertexPtr, index - 1));
/* Traverse the set of iterates */
while (index < numIterates &&
!AbsMddLEqualModCareSet(current, previous, careSet)) {
array_insert_last(mdd_t *, newRings, mdd_dup(current));
array_insert_last(boolean, newRingApprox,
AbsVertexFetchRingApprox(vertexPtr, index));
array_insert_last(boolean, newSubApprox,
AbsVertexFetchSubApprox(vertexPtr, index));
index++;
previous = current;
current = AbsVertexFetchRing(vertexPtr, index);
}
/* Insert the last two elements of the array */
array_insert_last(mdd_t *, newRings, mdd_dup(current));
array_insert_last(boolean, newRingApprox,
AbsVertexFetchRingApprox(vertexPtr, index));
array_insert_last(boolean, newSubApprox,
AbsVertexFetchSubApprox(vertexPtr, index));
/* Free the arrays stored in the vertex and store the new ones */
arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), index, current) {
mdd_free(current);
}
array_free(AbsVertexReadRings(vertexPtr));
array_free(AbsVertexReadRingApprox(vertexPtr));
array_free(AbsVertexReadSubApprox(vertexPtr));
/* Store the new results */
AbsVertexSetRings(vertexPtr, newRings);
AbsVertexSetRingApprox(vertexPtr, newRingApprox);
AbsVertexSetSubApprox(vertexPtr, newSubApprox);
assert(array_n(newRings) == array_n(newRingApprox));
assert(array_n(newRings) == array_n(newSubApprox));
return array_n(newRings) - 1;
} /* End of PruneIterateVector */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefineAnd | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to refine a conjunction formula]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 328 of file absRefine.c.
{
AbsVertexInfo_t *firstFormula;
AbsVertexInfo_t *secondFormula;
mdd_t *kidFirstResult;
mdd_t *conjunction;
mdd_t *result;
mdd_t *oldTmpCareSet;
/* Delete the old sat */
mdd_free(AbsVertexReadSat(vertexPtr));
/* Obtain the Sub-formulas */
firstFormula = AbsVertexReadLeftKid(vertexPtr);
secondFormula = AbsVertexReadRightKid(vertexPtr);
kidFirstResult = AbsSubFormulaRefine(absInfo, firstFormula, goalSet);
/* Store the temporary careset and set the new one */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo,
mdd_and(oldTmpCareSet,
AbsVertexReadSat(firstFormula),
1,1));
if (AbsVertexReadPolarity(vertexPtr)) {
/*
* Positive polarity: The goal set is given to one sub-formula first for
* refinement, and the left-overs are given to the second sub-formula.
*/
result = AbsSubFormulaRefine(absInfo, secondFormula, kidFirstResult);
mdd_free(kidFirstResult);
}
else { /* Vertex with negative polarity */
mdd_t *kidSecondResult;
mdd_t *reducedGoalSet;
reducedGoalSet = mdd_and(goalSet, AbsVertexReadSat(firstFormula), 1, 1);
kidSecondResult = AbsSubFormulaRefine(absInfo, secondFormula,
reducedGoalSet);
result = mdd_or(kidFirstResult, kidSecondResult, 1, 1);
mdd_free(reducedGoalSet);
mdd_free(kidFirstResult);
mdd_free(kidSecondResult);
}
/* Restore the temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
/* Re-evaluate the vertex just in case there has been some refinement */
conjunction = mdd_and(AbsVertexReadSat(firstFormula),
AbsVertexReadSat(secondFormula), 1, 1);
/* Store the new Sat value */
AbsVertexSetSat(vertexPtr, conjunction);
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(firstFormula) ||
AbsVertexReadGlobalApprox(secondFormula));
/* Set the refinement flags */
AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(firstFormula) &&
AbsVertexReadTrueRefine(secondFormula));
assert(mdd_lequal(result, goalSet, 1, 1));
return result;
} /* End of RefineAnd */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefineFixedPoint | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to refine the fix-point sub-formulas]
Description [The function calls several additional procedures to perform the refinement]
SideEffects []
SeeAlso [AbsSubFormulaRefine, AbsFixedPointIterate, RefineFixedPointIterate, PruneIterateVector, RestoreContainment]
Definition at line 418 of file absRefine.c.
{
boolean newIterates;
mdd_t *currentGoalSet;
mdd_t *result;
mdd_t *oldTmpCareSet;
mdd_t *newTmpCareSet;
mdd_t *oneMdd;
int numIterates;
/* Variable initialization */
numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
newIterates = TRUE;
/* Delete the previous result */
if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
mdd_free(AbsVertexReadSat(vertexPtr));
}
/* Set the new care set */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
newTmpCareSet = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);
oneMdd = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
currentGoalSet = mdd_dup(oneMdd);
/* While the fixed point has not been approximated exactly */
while (newIterates && AbsVertexReadGlobalApprox(vertexPtr)
&& !mdd_is_tautology(currentGoalSet, 0)) {
mdd_t *newGoalSet;
boolean pruneIterates;
newGoalSet = RefineFixedPointIterate(absInfo, vertexPtr, currentGoalSet,
numIterates);
/* Release unnecessary functions */
mdd_free(newGoalSet);
mdd_free(currentGoalSet);
/* Restore the inclusion property in the fixed point iterates */
pruneIterates = RestoreContainment(absInfo, vertexPtr);
/* Remove redundant iterates */
if (pruneIterates) {
numIterates = PruneIterateVector(absInfo, vertexPtr);
}
/* Sanity check of the refinement process */
assert(AbsIteratesSanityCheck(absInfo, vertexPtr));
/* Check if further iteration is required */
newIterates = AbsFixedPointIterate(absInfo, vertexPtr, numIterates);
numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
currentGoalSet = SuccessTest(AbsVertexFetchRing(vertexPtr, numIterates),
oneMdd, AbsVertexReadPolarity(vertexPtr));
} /* End of while loop */
mdd_free(oneMdd);
/* Restore the old temporary careset */
mdd_free(newTmpCareSet);
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
AbsVertexSetSat(vertexPtr,
mdd_dup(AbsVertexFetchRing(vertexPtr, numIterates)));
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexFetchSubApprox(vertexPtr, numIterates));
result = mdd_and(currentGoalSet, goalSet, 1, 1);
mdd_free(currentGoalSet);
return result;
} /* End of RefineFixedPoint */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefineFixedPointIterate | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet, | ||
| int | iterateNumber | ||
| ) | [static] |
Function********************************************************************
Synopsis [Apply the refinement procedure to one of the iterations of the fix-point]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 508 of file absRefine.c.
{
AbsVertexInfo_t *varFormula;
AbsVertexInfo_t *subFormula;
boolean trueRefine;
mdd_t *careSet;
mdd_t *variableValue;
mdd_t *result;
mdd_t *previousGoal;
mdd_t *refinedGoal;
mdd_t *newIterate;
mdd_t *oldIterate;
mdd_t *subFormulaSat;
int saveExact;
assert(iterateNumber != 0);
/* Variable initialization */
varFormula = AbsVertexReadFpVar(vertexPtr);
subFormula = AbsVertexReadLeftKid(vertexPtr);
careSet = AbsVerificationInfoReadCareSet(absInfo);
oldIterate = AbsVertexFetchRing(vertexPtr, iterateNumber);
/* Propagate the goalSet for refinement */
variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
AbsVertexSetSat(varFormula, variableValue);
AbsVertexSetGlobalApprox(varFormula,
AbsVertexFetchSubApprox(vertexPtr,
iterateNumber - 1));
/* Schedule the formula for Re-evaluation */
AbsFormulaScheduleEvaluation(varFormula, vertexPtr);
/* Evaluate the sub-formula again */
AbsSubFormulaVerify(absInfo, subFormula);
/* Set the goal to empty to detect if the refinement reaches it */
if (AbsVertexReadGoalSet(varFormula) != NIL(mdd_t)) {
mdd_free(AbsVertexReadGoalSet(varFormula));
AbsVertexSetGoalSet(varFormula, NIL(mdd_t));
}
/* Refine the sub-formula for this iterate */
result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);
/* Read the trueRefine from the subFormula */
trueRefine = AbsVertexReadTrueRefine(subFormula);
/* If The refinement does not need a recursive step, return. The return may
* be for three different reasons:
* a) The local refinement that was just done, succeeded completely.
* b) The goalset in varFormula is NIL, which means, the refinement
process failed somewhere earlier in the process, and therefore, the
false result was computed without the refinement of the variable.
c) trueRefine is TRUE. Which means, that even though the approximate
flag in the vertex is TRUE, meaning that there has been an
approximation, the refinement is still solid
*/
if (mdd_is_tautology(result, 0) || trueRefine ||
AbsVertexReadGoalSet(varFormula) == NIL(mdd_t)) {
subFormulaSat = AbsVertexReadSat(subFormula);
if (AbsVertexReadPolarity(vertexPtr)) {
if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
newIterate = mdd_dup(subFormulaSat);
}
else {
newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
}
}
else {
if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
newIterate = mdd_dup(subFormulaSat);
}
else {
newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
}
}
mdd_free(oldIterate);
array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
newIterate);
/* Set the new approx flag */
array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
AbsVertexReadGlobalApprox(subFormula));
AbsVertexSetTrueRefine(vertexPtr, trueRefine);
return result;
}
/* Recursive call to refine the previous iterate */
previousGoal = mdd_dup(AbsVertexReadGoalSet(varFormula));
refinedGoal = RefineFixedPointIterate(absInfo, vertexPtr, previousGoal,
iterateNumber - 1);
trueRefine = AbsVertexReadTrueRefine(vertexPtr);
/*
* Due to the refinement of the previous iterate, convergence might have
* been reached
*/
if (iterateNumber > 1) {
mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateNumber - 2);
if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
mdd_free(previousGoal);
mdd_free(refinedGoal);
mdd_free(oldIterate);
mdd_free(result);
array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
mdd_dup(AbsVertexFetchRing(vertexPtr, iterateNumber - 1)));
AbsVertexSetTrueRefine(vertexPtr, trueRefine);
/* Set the new approx flag */
array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
AbsVertexReadGlobalApprox(subFormula));
return SuccessTest(AbsVertexFetchRing(vertexPtr, iterateNumber),
goalSet, AbsVertexReadPolarity(vertexPtr));
}
}
mdd_free(previousGoal);
mdd_free(refinedGoal);
/* Evaluate the sub-formula exactly */
variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
AbsVertexSetSat(varFormula, variableValue);
mdd_free(result);
AbsVertexSetGlobalApprox(varFormula,
AbsVertexFetchSubApprox(vertexPtr,
iterateNumber - 1));
/* Schedule the formula for Re-evaluation */
AbsFormulaScheduleEvaluation(varFormula, vertexPtr);
/* Evaluate the sub-formula this time exactly */
saveExact = AbsOptionsReadExact(AbsVerificationInfoReadOptions(absInfo));
AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), TRUE);
AbsSubFormulaVerify(absInfo, subFormula);
AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), saveExact);
/* Enforce monotonicity of the approximants */
subFormulaSat = AbsVertexReadSat(subFormula);
if (AbsVertexReadPolarity(vertexPtr)) {
if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
newIterate = mdd_dup(subFormulaSat);
}
else {
newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
}
}
else {
if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
newIterate = mdd_dup(subFormulaSat);
}
else {
newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
}
}
/* Set the new approx flag */
array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
AbsVertexReadGlobalApprox(subFormula));
/* Recompute the goal set and the iterate */
result = SuccessTest(newIterate, goalSet,
AbsVertexReadPolarity(vertexPtr));
/* Some basic sanity check */
assert(AbsVertexReadPolarity(vertexPtr)?
AbsMddLEqualModCareSet(newIterate, oldIterate, careSet):
AbsMddLEqualModCareSet(oldIterate, newIterate, careSet));
/* Store the new iterate */
mdd_free(oldIterate);
array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
newIterate);
/* Set the new approx flag */
array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
AbsVertexReadGlobalApprox(subFormula));
AbsVertexSetTrueRefine(vertexPtr, trueRefine);
return result;
} /* End of RefineFixedPointIterate */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefineIdentifier | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to refine an atomic formula]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 254 of file absRefine.c.
{
/* Set the refinement flags */
AbsVertexSetTrueRefine(vertexPtr, TRUE);
/*
* If the polarity of this vertex is negative, we need to add states to
* the satisfying set. Since we already have the exact set, the states not
* in it are the returned goal. If the polarity is positive, we need to
* remove states. The states of the incoming goal that are in the
* satisfying set are the returned goal.
*/
if (AbsVertexReadPolarity(vertexPtr)) {
return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 1);
} else {
return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 0);
}
} /* End of RefineIdentifier */
Here is the caller graph for this function:
| static mdd_t * RefineNot | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Formula to refine a negation formula]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 286 of file absRefine.c.
{
AbsVertexInfo_t *subFormula;
mdd_t *result;
/* The not vertex has a trivial propagation equation */
subFormula = AbsVertexReadLeftKid(vertexPtr);
/* Go ahead and re-evaluate */
mdd_free(AbsVertexReadSat(vertexPtr));
/* Refine recursively */
result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);
/* Set the set sat */
AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));
/* Set the approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));
/* Set the trueRefine flag */
AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(subFormula));
assert(mdd_lequal(result, goalSet, 1, 1));
return result;
} /* End of RefineNot */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefinePreImage | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to refine the pre-image sub-formula]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 718 of file absRefine.c.
{
AbsStats_t *stats;
AbsVertexInfo_t *subFormula;
Img_ImageInfo_t *imageInfo;
Fsm_Fsm_t *system;
mdd_t *careSet;
mdd_t *result;
mdd_t *subResult;
mdd_t *newGoalSet;
mdd_t *oldTmpCareSet;
mdd_t *preImage;
/* Variable initialization */
system = AbsVerificationInfoReadFsm(absInfo);
subFormula = AbsVertexReadLeftKid(vertexPtr);
subResult = AbsVertexReadSat(subFormula);
stats = AbsVerificationInfoReadStats(absInfo);
imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 1);
careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);
/* Propagate the goal set */
newGoalSet = AbsImageReadOrCompute(absInfo, imageInfo, goalSet, subResult);
/* Store the new care set */
oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
AbsVerificationInfoSetTmpCareSet(absInfo,
mdd_one(AbsVerificationInfoReadMddManager(absInfo)));
/* Refine recursively */
result = AbsSubFormulaRefine(absInfo, subFormula, newGoalSet);
/* Restore the old temporary careset */
mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
if (!mdd_equal(result, newGoalSet) ||
!AbsVertexReadGlobalApprox(subFormula)) {
mdd_free(AbsVertexReadSat(vertexPtr));
if (AbsVertexReadSolutions(vertexPtr) == NIL(st_table)) {
/* Initialize the cache */
AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
}
preImage = NIL(mdd_t);
if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
AbsVertexReadSat(subFormula), careSet, FALSE,
&preImage, 0)) {
/* Set the sat */
AbsVertexSetSat(vertexPtr, mdd_dup(preImage));
}
else {
long cpuTime;
subResult = AbsVertexReadSat(subFormula);
cpuTime = util_cpu_time();
AbsVertexSetSat(vertexPtr,
Img_ImageInfoComputeBwdWithDomainVars(imageInfo,
subResult,
subResult,
careSet));
AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;
AbsStatsReadExactPreImage(stats)++;
/* Insert the result in the cache */
AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
AbsVertexReadSat(subFormula),
AbsVertexReadSat(vertexPtr), careSet,
FALSE, FALSE);
}
/* Set the new approximation flags */
AbsVertexSetLocalApprox(vertexPtr, FALSE);
AbsVertexSetGlobalApprox(vertexPtr,
AbsVertexReadGlobalApprox(subFormula));
} /* If !mdd_equal || !GlobalApprox(subFormula) */
mdd_free(careSet);
mdd_free(newGoalSet);
mdd_free(result);
result = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet,
AbsVertexReadPolarity(vertexPtr));
AbsVertexSetTrueRefine(vertexPtr,
AbsVertexReadTrueRefine(subFormula));
return result;
} /* End of RefinePreImage */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * RefineVariable | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr, | ||
| mdd_t * | goalSet | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Function to refine the sat set of a variable vertex.]
Description [The variable vertex reads the value of sat from the environment, therefore no approximation is done here. The function just reads if the goalSet is included in the current sat. This function returns trueVerification_c if the vertex has been successfully refined, falseVerification_c if the vertex has been refined until the exact computation has been performed but the refinement failed, and inconclusiveVerification_c if the vertex has been refined to the extent of the computational limits and still failed.]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 226 of file absRefine.c.
{
/* Set the current goalSet. If the pointer is non-empty, that means that the
variable belongs to a different pointer from the one being considered,
therefore, only the first goal set is of interest to us.*/
if (AbsVertexReadGoalSet(vertexPtr) == NIL(mdd_t)) {
AbsVertexSetGoalSet(vertexPtr, mdd_dup(goalSet));
}
/* Set the validity of the refinement */
AbsVertexSetTrueRefine(vertexPtr, !AbsVertexReadGlobalApprox(vertexPtr));
return mdd_dup(goalSet);
} /* End of RefineVariable */
Here is the caller graph for this function:
| static boolean RestoreContainment | ( | Abs_VerificationInfo_t * | absInfo, |
| AbsVertexInfo_t * | vertexPtr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to restore the containment relation between the iterations of a fix-point]
Description [After the refinement procedure has gone through the iterations of the fix-point, it is possible that the containment relation is no longer satisfied. This function looks at the polarity of the formula inside the fix-point and restores the containment relation to the iterations. This process can be seen as the propagation of certain refinements in the middle of the chain of iterations to the rest of the chain]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 833 of file absRefine.c.
{
mdd_t *iterateMdd;
mdd_t *iterateMddPrevious;
mdd_t *product;
boolean convergence;
int numIterates;
int index;
convergence = FALSE;
numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
if (AbsVertexReadPolarity(vertexPtr)) {
iterateMddPrevious = AbsVertexFetchRing(vertexPtr, numIterates);
for(index = numIterates - 1; index >= 0; index--) {
iterateMdd = iterateMddPrevious;
iterateMddPrevious = AbsVertexFetchRing(vertexPtr, index);
if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
AbsVerificationInfoReadCareSet(absInfo))) {
product = mdd_and(iterateMddPrevious, iterateMdd, 1, 1);
/* Add here don't care minimization */
mdd_free(iterateMddPrevious);
array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
iterateMddPrevious = product;
}
if (index != numIterates - 1 &&
AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
AbsVerificationInfoReadCareSet(absInfo))) {
convergence = TRUE;
}
}
}
else {
iterateMdd = AbsVertexFetchRing(vertexPtr, 0);
for(index = 1; index <= numIterates; index++) {
iterateMddPrevious = iterateMdd;
iterateMdd = AbsVertexFetchRing(vertexPtr, index);
if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
AbsVerificationInfoReadCareSet(absInfo))) {
product = mdd_or(iterateMddPrevious, iterateMdd, 1, 1);
/* Add here don't care minimization */
mdd_free(iterateMdd);
array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
iterateMdd = product;
}
if (index != numIterates &&
AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
AbsVerificationInfoReadCareSet(absInfo))) {
convergence = TRUE;
}
}
}
return convergence;
} /* End of RestoreContainment */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * SuccessTest | ( | mdd_t * | sat, |
| mdd_t * | goalSet, | ||
| boolean | polarity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Test if the function SAT is contained/excluded from the goal set depending on the polarity]
SideEffects []
SeeAlso [AbsSubFormulaRefine]
Definition at line 1007 of file absRefine.c.
{
mdd_t *result;
if (polarity) {
result = mdd_and(goalSet, sat, 1, 1);
}
else {
result = mdd_and(goalSet, sat, 1, 0);
}
return result;
} /* End of SuccessTest */
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: absRefine.c,v 1.24 2002/09/19 05:25:01 fabio Exp $" [static] |
CFile***********************************************************************
FileName [absRefine.c]
PackageName [abs]
Synopsis [Abstraction Refinement procedures for the mu-calculus model checker.]
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 absRefine.c.
