/**CFile*********************************************************************** FileName [absEvaluate.c] PackageName [abs] Synopsis [Evaluation procedures for the abstraction based mu-calculus model checker.] Author [Abelardo Pardo ] 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.] ******************************************************************************/ #include "absInt.h" static char rcsid[] UNUSED = "$Id: absEvaluate.c,v 1.19 2002/09/19 05:25:00 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void EvaluateVariable(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static void EvaluateIdentifier(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static void EvaluateNot(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static void EvaluateAnd(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static void EvaluateFixedPoint(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static void EvaluatePreImage(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); static mdd_t * OverApproximatePreImageWithSubFSM(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet); static mdd_t * OverApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet); static mdd_t * UnderApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Procedure to evaluate a sub-formula] Description [This procedure is simply a switch to call the apropriate evaluation procedures depending on the type of formula] SideEffects [EvaluateFixedPoint, EvaluateAnd, EvaluateNot, EvaluatePreImage, EvaluateIdentifier, EvaluateVariable] ******************************************************************************/ void AbsSubFormulaVerify( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { AbsStats_t *stats; mdd_manager *mddManager; mdd_t *oldTmpCareSet = NIL(mdd_t); long verbosity; stats = AbsVerificationInfoReadStats(absInfo); mddManager = AbsVerificationInfoReadMddManager(absInfo); /* 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: EvaluateFixedPoint(absInfo, vertexPtr); AbsStatsReadEvalFixedPoint(stats)++; break; case and_c: EvaluateAnd(absInfo, vertexPtr); AbsStatsReadEvalAnd(stats)++; break; case not_c: EvaluateNot(absInfo, vertexPtr); AbsStatsReadEvalNot(stats)++; break; case preImage_c: EvaluatePreImage(absInfo, vertexPtr); AbsStatsReadEvalPreImage(stats)++; break; case identifier_c: EvaluateIdentifier(absInfo, vertexPtr); AbsStatsReadEvalIdentifier(stats)++; break; case variable_c: EvaluateVariable(absInfo, vertexPtr); AbsStatsReadEvalVariable(stats)++; break; default: fail("Encountered unknown type of vertex\n"); } verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo)); /* Print the size of the care set */ if (verbosity & ABS_VB_CARESZ) { (void) fprintf(vis_stdout, "ABS: Size of Care Set: "); (void) fprintf(vis_stdout, "%d Nodes.\n", mdd_size(AbsVerificationInfoReadCareSet(absInfo))); } /* Print the care set */ if (verbosity & ABS_VB_CARE) { (void) fprintf(vis_stdout, "ABS: Care Set for Evaluation:\n"); AbsBddPrintMinterms(AbsVerificationInfoReadCareSet(absInfo)); } /* Print the contents of the vertex */ if (verbosity & ABS_VB_VTXCNT) { AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity); } if (lsLength(vertexPtr->parent) > 1) { /* Restore the old temporary careset */ mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo)); AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet); } } /* End of AbsSubFormulaVerify */ /**Function******************************************************************** Synopsis [Traverse the operational graph and mark formulas for evaluation] Description [This procedure receives two pointers and marks every formula in between for later evaluation. The marking process is simply setting the field served to 0] SideEffects [] SeeAlso [AbsFixedPointIterate] ******************************************************************************/ void AbsFormulaScheduleEvaluation( AbsVertexInfo_t *current, AbsVertexInfo_t *limit) { /* We reached the final case */ if (current == limit) { return; } else { AbsVertexInfo_t *parentPtr; lsList parentList; lsGen gen; /* Set the re-evaluation flag for the current vertex */ AbsVertexSetServed(current, 0); /* Recur over the parents */ parentList = AbsVertexReadParent(current); lsForEachItem(parentList, gen, parentPtr) { if (parentPtr != NIL(AbsVertexInfo_t)) { AbsFormulaScheduleEvaluation(parentPtr, limit); } } } return; } /* End of AbsFormulaScheduleEvaluation */ /**Function******************************************************************** Synopsis [Function to minimize the size of the BDD representing one iteration of the fix-point] Description [This function is simply to encapsulate the call to the minimize procedure and have a simple place where to explore the different choices when it comes to select upper and lower bounds for a function. In the case of fix-point evaluation, there are several bounds that can be used to look for a compact representation, this is the function in which that experimenting should be included] SideEffects [] SeeAlso [AbsFixedPointIterate] ******************************************************************************/ mdd_t * AbsComputeOptimalIterate( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *lowerIterate, mdd_t *upperIterate) { mdd_t *tmp; mdd_t *result; if (AbsOptionsReadMinimizeIterate(AbsVerificationInfoReadOptions(absInfo)) && AbsVertexReadUseExtraCareSet(vertexPtr)) { /* * For this computation we have three ingredients and a handfull of * choices. The ingredients are the sets newIterate, iterate and * careSet. The goal is to compute an interval delimited by two boolean * functions and then call the function bdd_between to try to obtain * the best bdd in size inside that interval. To compute the extremes * of the interval there are several choices. For example, the care set * can be used in the lower bound of the interval or in both * bounds. The bigger the interval the more choice the function * bdd_between has to minimize, however, this does not turn into a * better result. * * Current Choice: [newIterate * iterate', newIterate] */ tmp = mdd_and(lowerIterate, upperIterate, 0, 1); result = bdd_between(tmp, upperIterate); /* This line for debugging purposes, should be removed (void) fprintf(vis_stdout, "newIterate : %d, Diff : %d, result %d\n", mdd_size(upperIterate), mdd_size(tmp), mdd_size(result)); */ mdd_free(tmp); } else { result = mdd_dup(upperIterate); } return result; } /* End of AbsComputeOptimalIterate */ /**Function******************************************************************** Synopsis [Function to compute the iteration in a fix-point computation] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ boolean AbsFixedPointIterate( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, int iterateIndex) { AbsVertexInfo_t *subFormula; boolean keepIterating; boolean globalApprox; int stepCount; long verbosity; mdd_t *iterate; mdd_t *newIterate; mdd_t *careSet; /* Do not allow to iterate from the middle of a fixed point computation */ assert(iterateIndex == array_n(AbsVertexReadRings(vertexPtr)) - 1); careSet = AbsVerificationInfoReadCareSet(absInfo); /* Check if the set of iterates has already converged */ if (array_n(AbsVertexReadRings(vertexPtr)) > 1) { mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateIndex); mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateIndex - 1); if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) { return FALSE; } iterate = AbsVertexFetchRing(vertexPtr, iterateIndex - 1); } else { iterate = AbsVertexFetchRing(vertexPtr, iterateIndex); } newIterate = AbsVertexFetchRing(vertexPtr, iterateIndex); /* Variable initialization */ keepIterating = TRUE; stepCount = iterateIndex; verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo)); subFormula = AbsVertexReadLeftKid(vertexPtr); globalApprox = AbsVertexFetchSubApprox(vertexPtr, iterateIndex); /* Main loop for the fixed point computation */ while (keepIterating) { mdd_t *best; /* * Given newIterate, iterate and CareSet, if the use of extra care set is * enabled, choose the best candidate as the value of the iterate. */ best = AbsComputeOptimalIterate(absInfo, vertexPtr, iterate, newIterate); /* Print the iterates */ if ((verbosity & ABS_VB_PITER) || (verbosity & ABS_VB_ITSIZ)) { (void) fprintf(vis_stdout, "ABS: New Iterate: "); if (verbosity & ABS_VB_ITSIZ) { (void) fprintf(vis_stdout, "%d -> %d\n", mdd_size(newIterate), mdd_size(best)); } else { (void) fprintf(vis_stdout, "\n"); } if (verbosity & ABS_VB_PITER) { AbsBddPrintMinterms(newIterate); } } /* Store the value of the variable */ AbsVertexSetSat(AbsVertexReadFpVar(vertexPtr), best); /* Mark the proper sub-formulas for re-evaluation */ AbsFormulaScheduleEvaluation(AbsVertexReadFpVar(vertexPtr), vertexPtr); /* Evaluate the sub-formula */ AbsSubFormulaVerify(absInfo, subFormula); mdd_free(best); iterate = newIterate; /* * Compute the new iterate. Due to the fact that don't cares are being * used, it might be possible that the new iterate does not contain the * previous one, in that case the or is taken */ newIterate = mdd_or(iterate, AbsVertexReadSat(subFormula), 1, 1); assert(AbsMddLEqualModCareSet(iterate, newIterate, careSet)); /* Set the rings and the approximation flags */ AbsVertexInsertRing(vertexPtr, newIterate); AbsVertexInsertRingApprox(vertexPtr, FALSE); globalApprox = globalApprox || AbsVertexReadGlobalApprox(subFormula); AbsVertexInsertSubApprox(vertexPtr, globalApprox); keepIterating = !AbsMddEqualModCareSet(newIterate, iterate, careSet); stepCount++; } /* End of main while loop */ return TRUE; } /* End of AbsFixedPointIterate */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Function to evaluate a sub-formula representing the variable of a fix-point computation] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluateVariable( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluateVariable */ /**Function******************************************************************** Synopsis [Evaluate a vertex storing an Id] Description [This vertex represents a subformula with an atomic proposition. No approximation is done on its evaluation. The assumption is that this operation does not cause blow up in the memory requirements. This situation might change though] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluateIdentifier( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { if (AbsVertexReadServed(vertexPtr) == 0) { Ntk_Node_t *node; Var_Variable_t *nodeVar; graph_t *partition; vertex_t *partitionVertex; Mvf_Function_t *nodeFunction; mdd_t *result; char *nodeNameString; char *nodeValueString; int nodeValue; /* Clean up of previous result */ if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) { mdd_free(AbsVertexReadSat(vertexPtr)); AbsVertexSetSat(vertexPtr, NIL(mdd_t)); } /* Read the partition */ partition = AbsVerificationInfoReadPartition(absInfo); assert(partition != NIL(graph_t)); /* Obtain the name and the value being used */ nodeNameString = AbsVertexReadName(vertexPtr); nodeValueString = AbsVertexReadValue(vertexPtr); /* Obtain the the node in the network and the variable attached to it */ node = Ntk_NetworkFindNodeByName(AbsVerificationInfoReadNetwork(absInfo), nodeNameString); nodeVar = Ntk_NodeReadVariable(node); /* Obtain the real value of the multi-valued vairable */ if (Var_VariableTestIsSymbolic(nodeVar)) { nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString); } else { nodeValue = atoi(nodeValueString); } /* Read the partition, find the vertex in the partition and its function */ partitionVertex = Part_PartitionFindVertexByName(partition, nodeNameString); /* If the vertex is not represented in the partition must be built */ if (partitionVertex == NIL(vertex_t)) { Ntk_Node_t *tmpNode; lsGen tmpGen; array_t *mvfArray; array_t *tmpRoots; st_table *tmpLeaves; /* Initialize the variables */ tmpRoots = array_alloc(Ntk_Node_t *, 0); tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash); /* Insert the parameters in the array and table */ array_insert_last(Ntk_Node_t *, tmpRoots, node); Ntk_NetworkForEachCombInput(AbsVerificationInfoReadNetwork(absInfo), tmpGen, tmpNode) { st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED); } /* Effectively build the mdd for the given vertex */ mvfArray = Ntm_NetworkBuildMvfs(AbsVerificationInfoReadNetwork(absInfo), tmpRoots, tmpLeaves, NIL(mdd_t)); nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0); array_free(tmpRoots); st_free_table(tmpLeaves); array_free(mvfArray); /* Store the result in the vertex */ result = Mvf_FunctionReadComponent(nodeFunction, nodeValue); AbsVertexSetSat(vertexPtr, mdd_dup(result)); Mvf_FunctionFree(nodeFunction); } else { /* Store the result in the vertex */ nodeFunction = Part_VertexReadFunction(partitionVertex); result = Mvf_FunctionReadComponent(nodeFunction, nodeValue); AbsVertexSetSat(vertexPtr, mdd_dup(result)); } /* Set the approximation flags */ AbsVertexSetLocalApprox(vertexPtr, FALSE); AbsVertexSetGlobalApprox(vertexPtr, FALSE); } /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluateIdentifier */ /**Function******************************************************************** Synopsis [Evaluate a negation vertex] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluateNot( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { if (AbsVertexReadServed(vertexPtr) == 0) { AbsVertexInfo_t *subFormula; /* Clean up of previous result */ if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) { mdd_free(AbsVertexReadSat(vertexPtr)); AbsVertexSetSat(vertexPtr, NIL(mdd_t)); } /* Recursively evaluate the sub-formula */ subFormula = AbsVertexReadLeftKid(vertexPtr); AbsSubFormulaVerify(absInfo, subFormula); /* Negate the result of the sub-formula */ AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula))); /* Set the approximation flags */ AbsVertexSetLocalApprox(vertexPtr, FALSE); AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula)); } /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluateNot */ /**Function******************************************************************** Synopsis [Evaluate a conjunction vertex] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluateAnd( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { if (AbsVertexReadServed(vertexPtr) == 0) { AbsVertexInfo_t *firstFormula; AbsVertexInfo_t *secondFormula; mdd_t *oldTmpCareSet; /* Clean up of previous result */ if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) { mdd_free(AbsVertexReadSat(vertexPtr)); AbsVertexSetSat(vertexPtr, NIL(mdd_t)); } /* Obtain the subformulas to evaluate */ firstFormula = AbsVertexReadLeftKid(vertexPtr); secondFormula = AbsVertexReadRightKid(vertexPtr); /* Recursively evaluate the first sub-formula */ AbsSubFormulaVerify(absInfo, firstFormula); /* Store the temporary careset and set the new one */ oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo); AbsVerificationInfoSetTmpCareSet(absInfo, mdd_and(oldTmpCareSet, AbsVertexReadSat(firstFormula), 1,1)); /* Recursively evaluate the second sub-formula */ AbsSubFormulaVerify(absInfo, secondFormula); /* Restore the temporary careset */ mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo)); AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet); /* Compute result, so far no approximation is required */ AbsVertexSetSat(vertexPtr, mdd_and(AbsVertexReadSat(firstFormula), AbsVertexReadSat(secondFormula), 1, 1)); /* Set the approximation flags */ AbsVertexSetLocalApprox(vertexPtr, FALSE); AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(firstFormula) || AbsVertexReadGlobalApprox(secondFormula)); } /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluateAnd */ /**Function******************************************************************** Synopsis [Evaluate a fix-point vertex] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluateFixedPoint( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { if (AbsVertexReadServed(vertexPtr) == 0) { mdd_manager *mddManager; mdd_t *oldTmpCareSet; mdd_t *newTmpCareSet; if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) { mdd_t *ringUnit; int i; arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), i, ringUnit) { mdd_free(ringUnit); } array_free(AbsVertexReadRings(vertexPtr)); array_free(AbsVertexReadRingApprox(vertexPtr)); array_free(AbsVertexReadSubApprox(vertexPtr)); mdd_free(AbsVertexReadSat(vertexPtr)); } /* Re-allocation of the temporary structures */ AbsVertexSetRings(vertexPtr, array_alloc(mdd_t *, 0)); AbsVertexSetRingApprox(vertexPtr, array_alloc(boolean, 0)); AbsVertexSetSubApprox(vertexPtr, array_alloc(boolean, 0)); /* Initial values of the fixed point */ mddManager = AbsVerificationInfoReadMddManager(absInfo); AbsVertexInsertRing(vertexPtr, mdd_zero(mddManager)); AbsVertexInsertRingApprox(vertexPtr, FALSE); AbsVertexInsertSubApprox(vertexPtr, FALSE); /* Reset the temporary careset to the mdd one */ oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo); newTmpCareSet = mdd_one(mddManager); AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet); /* Effectively iterate the body */ AbsFixedPointIterate(absInfo, vertexPtr, 0); /* Restore the old temporary careset */ mdd_free(newTmpCareSet); AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet); /* Set the last result as the set sat*/ AbsVertexSetSat(vertexPtr, mdd_dup(AbsVertexFetchRing(vertexPtr, array_n(AbsVertexReadRings(vertexPtr)) - 1))); /* Set the approximation flags */ AbsVertexSetLocalApprox(vertexPtr, FALSE); AbsVertexSetGlobalApprox(vertexPtr, AbsVertexFetchSubApprox(vertexPtr, array_n(AbsVertexReadSubApprox(vertexPtr)) - 1)); } /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluateFixedPoint */ /**Function******************************************************************** Synopsis [Evaluate a pre-image vertex] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static void EvaluatePreImage( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr) { AbsOptions_t *options; AbsStats_t *stats; long verbosity; /* Variable initialization */ options = AbsVerificationInfoReadOptions(absInfo); verbosity = AbsOptionsReadVerbosity(options); stats = AbsVerificationInfoReadStats(absInfo); if (AbsVertexReadServed(vertexPtr) == 0) { AbsVertexInfo_t *subFormula; mdd_manager *mddManager; mdd_t *result; mdd_t *careSet; mdd_t *oldTmpCareSet; mdd_t *minimizedSet; /* Variable initialization */ mddManager = AbsVerificationInfoReadMddManager(absInfo); subFormula = AbsVertexReadLeftKid(vertexPtr); /* * Compute the care set as the conjunction of the given one and the * temporary one */ careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo), AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1); /* Clean up */ if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) { mdd_free(AbsVertexReadSat(vertexPtr)); AbsVertexSetSat(vertexPtr, NIL(mdd_t)); } /* Reset the temporary careset to the mdd one */ oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo); AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager)); /* Evaluate the sub-formula */ AbsSubFormulaVerify(absInfo, subFormula); /* Restore the old temporary careset */ mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo)); AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet); /* Check for trivial cases */ if (mdd_is_tautology(AbsVertexReadSat(subFormula), 0) || mdd_is_tautology(AbsVertexReadSat(subFormula), 1)) { AbsVertexSetSat(vertexPtr, mdd_dup(AbsVertexReadSat(subFormula))); AbsVertexSetLocalApprox(vertexPtr, FALSE); AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula)); mdd_free(careSet); return; } /* if (AbsOptionsReadMinimizeIterate(options)){ */ if (FALSE){ minimizedSet = bdd_minimize(AbsVertexReadSat(subFormula), AbsVerificationInfoReadCareSet(absInfo)); } else { minimizedSet = mdd_dup(AbsVertexReadSat(subFormula)); } /* Look up in the cache if the result has been previously computed */ if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) { mdd_t *unit; boolean localFlag; boolean exactness; exactness = AbsOptionsReadExact(options); if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr), minimizedSet, careSet, !exactness, &unit, &localFlag)) { /* Set the sat */ AbsVertexSetSat(vertexPtr, mdd_dup(unit)); /* Set the approximation flags */ AbsVertexSetLocalApprox(vertexPtr, localFlag & !exactness); AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula) || AbsVertexReadLocalApprox(vertexPtr)); /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; mdd_free(careSet); mdd_free(minimizedSet); return; } } else { /* Initialize the cache */ AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash)); } /* Effectively compute preImage */ if (!AbsOptionsReadExact(options)) { if (AbsVertexReadPolarity(vertexPtr)) { if (AbsOptionsReadPartApprox(options)) { result = OverApproximatePreImageWithSubFSM(absInfo, minimizedSet, minimizedSet, careSet); } else { result = OverApproximatePreImageWithBddSubsetting(absInfo, minimizedSet, minimizedSet, careSet); } AbsVertexSetLocalApprox(vertexPtr, TRUE); } else { result = UnderApproximatePreImageWithBddSubsetting(absInfo, minimizedSet, minimizedSet, careSet); AbsVertexSetLocalApprox(vertexPtr, TRUE); } AbsStatsReadApproxPreImage(AbsVerificationInfoReadStats(absInfo))++; } else { Fsm_Fsm_t *system; Img_ImageInfo_t *imageInfo; long cpuTime; system = AbsVerificationInfoReadFsm(absInfo); imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0); cpuTime = util_cpu_time(); result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, minimizedSet, minimizedSet,careSet); AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime; AbsStatsReadExactPreImage(stats)++; AbsVertexSetLocalApprox(vertexPtr, FALSE); } AbsVertexSetSat(vertexPtr, result); /* Set the value in the cache */ AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr), minimizedSet, AbsVertexReadSat(vertexPtr), careSet, AbsVertexReadLocalApprox(vertexPtr), FALSE); AbsStatsReadPreImageCacheEntries(stats)++; mdd_free(minimizedSet); /* Set the approximation flags */ AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula) || AbsVertexReadLocalApprox(vertexPtr)); /* Print the number of states in the on set of Sat */ if (verbosity & ABS_VB_TSAT) { Fsm_Fsm_t *globalSystem; array_t *domainVars; mdd_t *intersection; intersection = mdd_and(AbsVertexReadSat(vertexPtr), careSet, 1, 1); globalSystem = AbsVerificationInfoReadFsm(absInfo); domainVars = Fsm_FsmReadPresentStateVars(globalSystem); (void) fprintf(vis_stdout, "ABS: %.0f States satisfy the EX formula.\n", mdd_count_onset(AbsVerificationInfoReadMddManager(absInfo), intersection, domainVars)); mdd_free(intersection); } mdd_free(careSet); } /* Increase the number of times the result has been used */ AbsVertexReadServed(vertexPtr)++; return; } /* End of EvaluatePreImage */ /**Function******************************************************************** Synopsis [Compute an over-approximation of the Preimage] SideEffects [This overapproximation is computed by just ignoring some FSM components] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static mdd_t * OverApproximatePreImageWithSubFSM( Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) { Fsm_Fsm_t *system; Img_ImageInfo_t *imageInfo; mdd_t *result; long cpuTime; /* Initialize some variables */ system = AbsVerificationInfoReadApproxFsm(absInfo); if (system == NIL(Fsm_Fsm_t)) { system = AbsVerificationInfoReadFsm(absInfo); } /* Obtain the image info */ imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0); cpuTime = util_cpu_time(); result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, lowerBound, upperBound, careSet); AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= util_cpu_time() - cpuTime; return result; } /* End of OverApproximatePreImageWithSubFSM */ /**Function******************************************************************** Synopsis [A second procedure to compute an over-approximation of the Preimage] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static mdd_t * OverApproximatePreImageWithBddSubsetting( Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) { Fsm_Fsm_t *system; Img_ImageInfo_t *imageInfo; mdd_t *superSet; mdd_t *result; long cpuTime; /* Initialize some variables */ system = AbsVerificationInfoReadFsm(absInfo); /* Compute the subset of the restriction set */ superSet = bdd_approx_remap_ua(lowerBound,BDD_OVER_APPROX, AbsVerificationInfoReadNumStateVars(absInfo), 0,1); /* Obtain the image info */ imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0); cpuTime = util_cpu_time(); result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, superSet, superSet, careSet); AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= util_cpu_time() - cpuTime; mdd_free(superSet); return result; } /* End of OverApproximatePreImageWithBddSubsetting */ /**Function******************************************************************** Synopsis [Compute an under-approximation of the preimage] SideEffects [] SeeAlso [AbsSubFormulaVerify] ******************************************************************************/ static mdd_t * UnderApproximatePreImageWithBddSubsetting( Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet) { Fsm_Fsm_t *system; Img_ImageInfo_t *imageInfo; mdd_t *subSet; mdd_t *result; long cpuTime; /* Initialize some variables */ system = AbsVerificationInfoReadFsm(absInfo); /* Compute the subset of the restriction set */ subSet = bdd_approx_remap_ua(lowerBound, BDD_UNDER_APPROX, AbsVerificationInfoReadNumStateVars(absInfo), 0,1); /* Obtain the image info */ imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0); cpuTime = util_cpu_time(); result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, subSet, subSet, careSet); AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= util_cpu_time() - cpuTime; mdd_free(subSet); return result; } /* End of UnderApproximatePreImageWithBddSubsetting */