- Generated on Wed Oct 12 2011 00:34:48 for VIS by
1.7.3
|
VIS
|
00001 00079 #include "fsmInt.h" 00080 #include "ntm.h" 00081 00082 static char rcsid[] UNUSED = "$Id: fsmArdc.c,v 1.86 2009/04/12 00:44:04 fabio Exp $"; 00083 00084 /*---------------------------------------------------------------------------*/ 00085 /* Constant declarations */ 00086 /*---------------------------------------------------------------------------*/ 00087 00088 #define ARDC_MAX_LINE_LEN 4096 00089 00090 /*---------------------------------------------------------------------------*/ 00091 /* Structure declarations */ 00092 /*---------------------------------------------------------------------------*/ 00093 00094 00095 /*---------------------------------------------------------------------------*/ 00096 /* Type declarations */ 00097 /*---------------------------------------------------------------------------*/ 00098 00099 00102 /*---------------------------------------------------------------------------*/ 00103 /* Static function prototypes */ 00104 /*---------------------------------------------------------------------------*/ 00105 00106 static void SortSubFsmsForApproximateTraversal(array_t **subFsmArray, array_t **fanInsIndexArray, array_t **fanOutsIndexArray, int verbosityLevel); 00107 static array_t * ArdcMbmTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, mdd_t ***subReached, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag); 00108 static array_t * ArdcRfbfTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options); 00109 static array_t * ArdcTfbfTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, mdd_t ***subReached, mdd_t ***subTo, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options); 00110 static array_t * ArdcTmbmTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag); 00111 static array_t * ArdcSimpleTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, int setFlag); 00112 static void ComputeFaninConstrainArray(array_t *faninConstrainArray, mdd_t **constraint, int current, array_t *fans, int decomposeFlag, int faninConstrainMode); 00113 static void MinimizeTransitionRelationWithFaninConstraint(Img_ImageInfo_t *imageInfo, array_t *faninConstrainArray, Img_MinimizeType constrainMethod, boolean reorderPtrFlag, boolean duplicate); 00114 static void ComputeConstrainedInitialStates(Fsm_Fsm_t *subFsm, array_t *faninConstrainArray, Img_MinimizeType constrainMethod); 00115 static void ComputeApproximateReachableStatesArray(mdd_manager *mddManager, array_t *reachedArray, mdd_t **reached, mdd_t ***subReached, int nSubFsms, int decomposeFlag); 00116 static array_t * ArdcCopyOverApproxReachableStatesFromExact(Fsm_Fsm_t *fsm); 00117 static void PrintCurrentReachedStates(mdd_manager *mddManager, Fsm_Fsm_t **subFsm, mdd_t **reached, Fsm_Ardc_TraversalType_t method, int nSubFsms, int iteration, int nvars, int ardcVerbosity, boolean supportCheckFlag); 00118 static void PrintBddWithName(Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node); 00119 static void ArdcReadGroup(Ntk_Network_t *network, FILE *groupFile, array_t *latchNameArray, array_t *groupIndexArray); 00120 static void ArdcWriteOneGroup(Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i); 00121 static void ArdcPrintOneGroup(Part_Subsystem_t *partitionSubsystem, int i, int nLatches, array_t *fanIns, array_t *fanOuts); 00122 static int GetArdcSetIntValue(char *string, int l, int u, int defaultValue); 00123 static void ArdcEpdCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm, EpDouble *epd); 00124 static mdd_t * QuantifyVariables(mdd_t *state, array_t *smoothArray, mdd_t *smoothCube); 00125 static void UpdateMbmEventSchedule(Fsm_Fsm_t **subFsm, array_t *fanOutIndices, int *traverse, int lfpFlag); 00126 static void PrintTfmStatistics(array_t *subFsmArray); 00127 00131 /*---------------------------------------------------------------------------*/ 00132 /* Definition of exported functions */ 00133 /*---------------------------------------------------------------------------*/ 00134 00153 void 00154 Fsm_ArdcMinimizeTransitionRelation(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd) 00155 { 00156 char *flagValue; 00157 int value = 0; 00158 int fwd = 0; 00159 int bwd = 0; 00160 Img_ImageInfo_t *imageInfo; 00161 int saveStatus; 00162 boolean reorderPtrFlag = FALSE; 00163 00164 switch (fwdbwd) { 00165 case Img_Forward_c: 00166 fwd = 1; 00167 break; 00168 case Img_Backward_c: 00169 bwd = 1; 00170 break; 00171 case Img_Both_c: 00172 fwd = 1; 00173 bwd= 1; 00174 break; 00175 } 00176 00177 imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd); 00178 00179 saveStatus = 0; 00180 flagValue = Cmd_FlagReadByName("ardc_verbosity"); 00181 if (flagValue != NIL(char)) { 00182 sscanf(flagValue, "%d", &value); 00183 if (value > 1) { 00184 saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 00185 Img_SetPrintMinimizeStatus(imageInfo, 1); 00186 } 00187 } 00188 00189 reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr", 00190 reorderPtrFlag); 00191 Img_MinimizeTransitionRelation( 00192 imageInfo, 00193 Fsm_FsmReadCurrentOverApproximateReachableStates(fsm), 00194 Img_DefaultMinimizeMethod_c, fwdbwd, reorderPtrFlag); 00195 00196 if (value > 1) 00197 Img_SetPrintMinimizeStatus(fsm->imageInfo, saveStatus); 00198 return; 00199 } 00200 00201 00214 mdd_t * 00215 Fsm_ArdcComputeImage(Fsm_Fsm_t *fsm, 00216 mdd_t *fromLowerBound, 00217 mdd_t *fromUpperBound, 00218 array_t *toCareSetArray) 00219 { 00220 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); 00221 mdd_t *image; 00222 00223 /* Create an imageInfo for image computations, if not already created. */ 00224 imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1); 00225 00226 /* Compute the image */ 00227 image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, 00228 fromLowerBound, fromUpperBound, toCareSetArray); 00229 00230 return(image); 00231 } 00232 00233 00246 array_t * 00247 Fsm_FsmComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, 00248 int incrementalFlag, int verbosityLevel, int printStep, int depthValue, 00249 int shellFlag, int reorderFlag, int reorderThreshold, int recompute) 00250 { 00251 array_t *apprReachableStates; 00252 Fsm_ArdcOptions_t options; 00253 00254 Fsm_ArdcGetDefaultOptions(&options); 00255 00256 if (printStep && options.verbosity < 2) 00257 printStep = 0; 00258 00259 apprReachableStates = Fsm_ArdcComputeOverApproximateReachableStates(fsm, 00260 incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag, 00261 reorderFlag, reorderThreshold, recompute, &options); 00262 00263 return(apprReachableStates); 00264 } 00265 00266 00285 array_t * 00286 Fsm_ArdcComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, 00287 int incrementalFlag, 00288 int verbosityLevel, 00289 int printStep, 00290 int depthValue, int shellFlag, 00291 int reorderFlag, 00292 int reorderThreshold, 00293 int recompute, 00294 Fsm_ArdcOptions_t *options) 00295 { 00296 array_t *reachableStatesArray = NIL(array_t); 00297 mdd_t *reachableStates = NIL(mdd_t); 00298 mdd_t *initialStates; 00299 Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm); 00300 Part_Subsystem_t *partitionSubsystem; 00301 array_t *partitionArray; 00302 int i; 00303 graph_t *partition = Part_NetworkReadPartition(network); 00304 st_table *vertexTable; 00305 Fsm_Fsm_t *subFsm; 00306 array_t *subFsmArray; 00307 array_t *fanIns, *fanOuts; 00308 array_t *fanInsIndexArray, *fanOutsIndexArray; 00309 array_t *fans; 00310 array_t *psVars; 00311 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00312 char *flagValue; 00313 Fsm_RchType_t approxFlag; 00314 int nvars; /* the number of binary variables of the fsm */ 00315 FILE *groupFile = NIL(FILE); 00316 Img_MethodType imageMethod = Img_Default_c; 00317 Img_MethodType saveImageMethod = Img_Default_c; 00318 char *imageMethodString; 00319 Fsm_Ardc_AbstPpiType_t saveAbstractPseudoInput; 00320 00321 if (recompute) 00322 FsmResetReachabilityFields(fsm, Fsm_Rch_Oa_c); 00323 00324 /* If exact is already computed, copy exact to overapproximate. */ 00325 if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) { 00326 if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) { 00327 /* If the overapproximation is already the exact set, return it, 00328 * otherwise discard it. */ 00329 if (FsmReadReachabilityOverApproxComputationStatus(fsm) == 00330 Fsm_Ardc_Exact_c) { 00331 return(Fsm_FsmReadOverApproximateReachableStates(fsm)); 00332 } else { 00333 fprintf(vis_stdout, 00334 "** ardc warning : ignoring previous computation.\n"); 00335 Fsm_FsmFreeOverApproximateReachableStates(fsm); 00336 } 00337 } 00338 if (verbosityLevel > 0 || options->verbosity > 0) { 00339 fprintf(vis_stdout, 00340 "** ardc info : exact reached states are already computed.\n"); 00341 } 00342 /* Either we had no overapproximation, or it was not the exact set, and 00343 * hence it was discarded. Copy from exact to overapproximate. */ 00344 reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm); 00345 return(reachableStatesArray); 00346 } 00347 00348 /* If already computed, just return the array. */ 00349 if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) { 00350 if (FsmReadReachabilityOverApproxComputationStatus(fsm) >= 00351 Fsm_Ardc_Converged_c) { 00352 return(Fsm_FsmReadOverApproximateReachableStates(fsm)); 00353 } else { 00354 /* Here, at this time, we just throw away current approximate 00355 * reachable states which is not converged yet, then restart. 00356 */ 00357 fprintf(vis_stdout, 00358 "** ardc warning : ignoring previous computation.\n"); 00359 Fsm_FsmFreeOverApproximateReachableStates(fsm); 00360 } 00361 } 00362 00363 /* Perform state space decomposition. */ 00364 partitionArray = Fsm_ArdcDecomposeStateSpace(network, 00365 fsm->fsmData.presentStateVars, 00366 fsm->fsmData.nextStateFunctions, 00367 options); 00368 00369 /* If there is only one group, call exact reachability analysis. */ 00370 if (array_n(partitionArray) == 1) { 00371 if (options->verbosity > 0) { 00372 fprintf(vis_stdout, 00373 "** ardc info : changing to exact reachability analysis.\n"); 00374 } 00375 arrayForEachItem(Part_Subsystem_t *, partitionArray, i, 00376 partitionSubsystem) { 00377 Part_PartitionSubsystemFree(partitionSubsystem); 00378 } 00379 array_free(partitionArray); 00380 00381 if (options->useHighDensity) 00382 approxFlag = Fsm_Rch_Hd_c; 00383 else 00384 approxFlag = Fsm_Rch_Bfs_c; 00385 reachableStates = Fsm_FsmComputeReachableStates(fsm, 00386 0, verbosityLevel, printStep, 0, 00387 0, reorderFlag, reorderThreshold, 00388 approxFlag, 0, 0, NIL(array_t), (verbosityLevel > 1), 00389 NIL(array_t)); 00390 mdd_free(reachableStates); 00391 reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm); 00392 return(reachableStatesArray); 00393 } 00394 00395 /* Read the image_method flag, and save its value in imageMethodString. */ 00396 flagValue = Cmd_FlagReadByName("image_method"); 00397 if (flagValue != NIL(char)) { 00398 if (strcmp(flagValue, "iwls95") == 0 || strcmp(flagValue, "default") == 0) 00399 imageMethod = Img_Iwls95_c; 00400 else if (strcmp(flagValue, "monolithic") == 0) 00401 imageMethod = Img_Monolithic_c; 00402 else if (strcmp(flagValue, "tfm") == 0) 00403 imageMethod = Img_Tfm_c; 00404 else if (strcmp(flagValue, "hybrid") == 0) 00405 imageMethod = Img_Hybrid_c; 00406 else if (strcmp(flagValue, "mlp") == 0) 00407 imageMethod = Img_Mlp_c; 00408 else { 00409 fprintf(vis_stderr, "** ardc error: invalid image method %s.\n", 00410 flagValue); 00411 } 00412 } 00413 imageMethodString = flagValue; 00414 /* Update the image_method flag to the method specified for approximate 00415 * reachability. */ 00416 if (options->ardcImageMethod != Img_Default_c && 00417 options->ardcImageMethod != imageMethod) { 00418 saveImageMethod = imageMethod; 00419 if (options->ardcImageMethod == Img_Monolithic_c) { 00420 Cmd_FlagUpdateValue("image_method", "monolithic"); 00421 imageMethod = Img_Monolithic_c; 00422 } else if (options->ardcImageMethod == Img_Iwls95_c) { 00423 Cmd_FlagUpdateValue("image_method", "iwls95"); 00424 imageMethod = Img_Iwls95_c; 00425 } else if (options->ardcImageMethod == Img_Tfm_c) { 00426 Cmd_FlagUpdateValue("image_method", "tfm"); 00427 imageMethod = Img_Tfm_c; 00428 } else if (options->ardcImageMethod == Img_Hybrid_c) { 00429 Cmd_FlagUpdateValue("image_method", "hybrid"); 00430 imageMethod = Img_Hybrid_c; 00431 } else if (options->ardcImageMethod == Img_Mlp_c) { 00432 Cmd_FlagUpdateValue("image_method", "mlp"); 00433 imageMethod = Img_Mlp_c; 00434 } 00435 } 00436 00437 /* Open the file where to save the result of partitioning is so requested. */ 00438 if (options->writeGroupFile) { 00439 groupFile = Cmd_FileOpen(options->writeGroupFile, "w", NIL(char *), 0); 00440 if (groupFile == NIL(FILE)) { 00441 fprintf(vis_stderr, "** ardc error : can't open file [%s] to write.\n", 00442 options->writeGroupFile); 00443 } 00444 } 00445 00446 /* Compute the set of initial states, if not already computed. */ 00447 initialStates = Fsm_FsmComputeInitialStates(fsm); 00448 00449 subFsmArray = array_alloc(Fsm_Fsm_t *, 0); 00450 fanInsIndexArray = array_alloc(array_t *, 0); 00451 fanOutsIndexArray = array_alloc(array_t *, 0); 00452 00453 /* For each partitioned submachines build an FSM. */ 00454 arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) { 00455 vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem); 00456 fanIns = Part_PartitionSubsystemReadFanIn(partitionSubsystem); 00457 fanOuts = Part_PartitionSubsystemReadFanOut(partitionSubsystem); 00458 subFsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, 00459 vertexTable, TRUE, 00460 options->createPseudoVarMode); 00461 /* Depending on the options, the initial states of each submachine 00462 * are either the states of the entire system or their projection 00463 * on the subspace of the submachine. */ 00464 if (!options->projectedInitialFlag && 00465 options->abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) { 00466 subFsm->reachabilityInfo.initialStates = mdd_dup(initialStates); 00467 } else { 00468 mdd_t *dummy; 00469 00470 dummy = Fsm_FsmComputeInitialStates(subFsm); 00471 mdd_free(dummy); 00472 } 00473 array_insert_last(Fsm_Fsm_t *, subFsmArray, subFsm); 00474 array_insert_last(array_t *, fanInsIndexArray, fanIns); 00475 array_insert_last(array_t *, fanOutsIndexArray, fanOuts); 00476 00477 if (options->verbosity > 1) { 00478 int nLatches; 00479 nLatches = mdd_get_number_of_bdd_vars(mddManager, 00480 subFsm->fsmData.presentStateVars); 00481 ArdcPrintOneGroup(partitionSubsystem, i, nLatches, fanIns, fanOuts); 00482 } 00483 if (groupFile) 00484 ArdcWriteOneGroup(partitionSubsystem, groupFile, i); 00485 00486 st_free_table(vertexTable); 00487 } /* end of arrayForEachItem(partitionArray) */ 00488 mdd_free(initialStates); 00489 00490 if (groupFile) 00491 fclose(groupFile); 00492 00493 /* Sort submachines to find the order in which to traverse them. */ 00494 SortSubFsmsForApproximateTraversal(&subFsmArray, &fanInsIndexArray, 00495 &fanOutsIndexArray, options->verbosity); 00496 00497 /* Optimize pseudo-input variables to contain only the variables of fanin 00498 * submachines. If createPseudoVarMode is 0, the set of pseudo-input 00499 * variables is just the collection of the variables of all other 00500 * submachines. 00501 * If createPseudoVarMode is 1, the set is the collection of the variables 00502 * of only its fanin submachines. If createPseudoVarMode is 2, the set is 00503 * the collection of the support variables that appear in other submachines. 00504 */ 00505 if (options->createPseudoVarMode == 0) { 00506 arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) { 00507 Fsm_Fsm_t *faninSubfsm; 00508 int j, fanin; 00509 00510 subFsm->fsmData.primaryInputVars = array_dup(subFsm->fsmData.inputVars); 00511 subFsm->fsmData.pseudoInputVars = array_alloc(int, 0); 00512 fanIns = array_fetch(array_t *, fanInsIndexArray, i); 00513 arrayForEachItem(int, fanIns, j, fanin) { 00514 if (fanin == i) 00515 continue; 00516 faninSubfsm = array_fetch(Fsm_Fsm_t *, subFsmArray, fanin); 00517 array_append(subFsm->fsmData.pseudoInputVars, 00518 faninSubfsm->fsmData.presentStateVars); 00519 } 00520 subFsm->fsmData.globalPsVars = array_dup( 00521 subFsm->fsmData.presentStateVars); 00522 array_append(subFsm->fsmData.globalPsVars, 00523 subFsm->fsmData.pseudoInputVars); 00524 array_append(subFsm->fsmData.inputVars, subFsm->fsmData.pseudoInputVars); 00525 00526 subFsm->fsmData.pseudoInputBddVars = mdd_id_array_to_bdd_array(mddManager, 00527 subFsm->fsmData.pseudoInputVars); 00528 00529 if (subFsm->fsmData.createVarCubesFlag) { 00530 subFsm->fsmData.pseudoInputCube = mdd_id_array_to_bdd_cube(mddManager, 00531 subFsm->fsmData.pseudoInputVars); 00532 subFsm->fsmData.primaryInputCube = subFsm->fsmData.inputCube; 00533 subFsm->fsmData.inputCube = mdd_id_array_to_bdd_cube(mddManager, 00534 subFsm->fsmData.inputVars); 00535 subFsm->fsmData.globalPsCube = mdd_id_array_to_bdd_cube(mddManager, 00536 subFsm->fsmData.globalPsVars); 00537 } 00538 } 00539 } 00540 00541 if (options->useHighDensity) 00542 approxFlag = Fsm_Rch_Hd_c; 00543 else 00544 approxFlag = Fsm_Rch_Bfs_c; 00545 00546 /* In case of transition function method, since quantification doesn't 00547 * make any sense, we turn it off. We turn quantification off also for the 00548 * hybrid method, because it starts with tfm. 00549 */ 00550 saveAbstractPseudoInput = options->abstractPseudoInput; 00551 if (imageMethod == Img_Tfm_c || imageMethod == Img_Hybrid_c) 00552 options->abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c; 00553 00554 nvars = mdd_get_number_of_bdd_vars(mddManager, fsm->fsmData.presentStateVars); 00555 if (options->traversalMethod == Fsm_Ardc_Traversal_Mbm_c) { 00556 reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray, 00557 fanInsIndexArray, fanOutsIndexArray, NULL, 00558 incrementalFlag, verbosityLevel, printStep, 00559 depthValue, shellFlag, reorderFlag, 00560 reorderThreshold, approxFlag, options, FALSE); 00561 } else if (options->traversalMethod == Fsm_Ardc_Traversal_Rfbf_c) { 00562 if (approxFlag == Fsm_Rch_Hd_c) { 00563 fprintf(vis_stderr, 00564 "** ardc error : High Density Traversal is not allowed in FBF.\n"); 00565 } 00566 reachableStatesArray = ArdcRfbfTraversal(fsm, nvars, subFsmArray, 00567 fanInsIndexArray, 00568 incrementalFlag, verbosityLevel, printStep, 00569 depthValue, shellFlag, reorderFlag, reorderThreshold, 00570 approxFlag, options); 00571 } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tfbf_c) { 00572 if (approxFlag == Fsm_Rch_Hd_c) { 00573 fprintf(vis_stderr, 00574 "** ardc error : High Density Traversal is not allowed in FBF.\n"); 00575 } 00576 reachableStatesArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray, 00577 fanInsIndexArray, NULL, NULL, 00578 incrementalFlag, verbosityLevel, printStep, 00579 depthValue, shellFlag, reorderFlag, reorderThreshold, 00580 approxFlag, options); 00581 } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tmbm_c) { 00582 reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray, 00583 fanInsIndexArray, fanOutsIndexArray, 00584 incrementalFlag, verbosityLevel, printStep, 00585 depthValue, shellFlag, reorderFlag, reorderThreshold, 00586 approxFlag, options, FALSE); 00587 } else if (options->traversalMethod == Fsm_Ardc_Traversal_Lmbm_c) { 00588 reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray, 00589 fanInsIndexArray, fanOutsIndexArray, NULL, 00590 incrementalFlag, verbosityLevel, printStep, 00591 depthValue, shellFlag, reorderFlag, 00592 reorderThreshold, approxFlag, options, TRUE); 00593 } else if (options->traversalMethod == Fsm_Ardc_Traversal_Tlmbm_c) { 00594 reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray, 00595 fanInsIndexArray, fanOutsIndexArray, 00596 incrementalFlag, verbosityLevel, printStep, 00597 depthValue, shellFlag, reorderFlag, reorderThreshold, 00598 approxFlag, options, TRUE); 00599 } else { 00600 reachableStatesArray = ArdcSimpleTraversal(fsm, nvars, subFsmArray, 00601 incrementalFlag, verbosityLevel, printStep, 00602 depthValue, shellFlag, reorderFlag, reorderThreshold, 00603 approxFlag, options, TRUE); 00604 } 00605 options->abstractPseudoInput = saveAbstractPseudoInput; 00606 00607 if (options->verbosity && 00608 (options->ardcImageMethod == Img_Tfm_c || 00609 options->ardcImageMethod == Img_Hybrid_c)) { 00610 PrintTfmStatistics(subFsmArray); 00611 } 00612 00613 fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0); 00614 if (options->decomposeFlag) { 00615 for (i = 0; i < array_n(subFsmArray); i++) { 00616 subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 00617 psVars = array_dup(subFsm->fsmData.presentStateVars); 00618 array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars); 00619 } 00620 } else { 00621 psVars = array_dup(fsm->fsmData.presentStateVars); 00622 array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars); 00623 } 00624 00625 arrayForEachItem(array_t *, fanInsIndexArray, i, fans) { 00626 array_free(fans); 00627 } 00628 array_free(fanInsIndexArray); 00629 arrayForEachItem(array_t *, fanOutsIndexArray, i, fans) { 00630 array_free(fans); 00631 } 00632 array_free(fanOutsIndexArray); 00633 arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) { 00634 FREE(partitionSubsystem); 00635 } 00636 array_free(partitionArray); 00637 00638 arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) { 00639 Fsm_FsmSubsystemFree(subFsm); 00640 } 00641 array_free(subFsmArray); 00642 00643 /* Restore value of image_method flag. */ 00644 if (options->ardcImageMethod != Img_Default_c && 00645 options->ardcImageMethod != saveImageMethod) { 00646 if (imageMethodString) { 00647 if (saveImageMethod == Img_Monolithic_c) 00648 Cmd_FlagUpdateValue("image_method", "monolithic"); 00649 else if (saveImageMethod == Img_Iwls95_c) 00650 Cmd_FlagUpdateValue("image_method", "iwls95"); 00651 else if (saveImageMethod == Img_Tfm_c) 00652 Cmd_FlagUpdateValue("image_method", "tfm"); 00653 else if (saveImageMethod == Img_Hybrid_c) 00654 Cmd_FlagUpdateValue("image_method", "hybrid"); 00655 else if (saveImageMethod == Img_Mlp_c) 00656 Cmd_FlagUpdateValue("image_method", "mlp"); 00657 } else 00658 Cmd_FlagDeleteByName("image_method"); 00659 } 00660 00661 fsm->reachabilityInfo.apprReachableStates = reachableStatesArray; 00662 return(reachableStatesArray); 00663 } 00664 00665 00677 array_t * 00678 Fsm_ArdcDecomposeStateSpace(Ntk_Network_t *network, array_t *presentStateVars, 00679 array_t *nextStateFunctions, Fsm_ArdcOptions_t *options) 00680 { 00681 array_t *latchNameArray; 00682 array_t *groupIndexArray; 00683 char *name; 00684 Ntk_Node_t *latch; 00685 int i, mddId; 00686 Part_SubsystemInfo_t *subsystemInfo; 00687 array_t *partitionArray; 00688 FILE *groupFile = NIL(FILE); 00689 long initialTime = 0, finalTime; 00690 int verbosity = 0; 00691 float affinityFactor = 0.5; 00692 int groupSize = 8; 00693 00694 if (options) { 00695 verbosity = options->verbosity; 00696 affinityFactor = options->affinityFactor; 00697 groupSize = options->groupSize; 00698 } else { 00699 char *flagValue; 00700 00701 flagValue = Cmd_FlagReadByName("ardc_group_size"); 00702 if (flagValue != NIL(char)) { 00703 sscanf(flagValue, "%d", &groupSize); 00704 if (groupSize <= 0) { 00705 fprintf(vis_stderr, 00706 "** ardc error: invalid value %s for ardc_group_size[>0]. **\n", 00707 flagValue); 00708 groupSize = 8; 00709 } 00710 } 00711 flagValue = Cmd_FlagReadByName("ardc_verbosity"); 00712 if (flagValue != NIL(char)) 00713 sscanf(flagValue, "%d", &verbosity); 00714 flagValue = Cmd_FlagReadByName("ardc_affinity_factor"); 00715 if (flagValue != NIL(char)) { 00716 sscanf(flagValue, "%f", &affinityFactor); 00717 if (affinityFactor < 0.0 || affinityFactor > 1.0) { 00718 fprintf(vis_stderr, 00719 "** ardc error :invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n", 00720 flagValue); 00721 affinityFactor = 0.5; 00722 } 00723 } 00724 } 00725 00726 if (verbosity > 0) 00727 initialTime = util_cpu_time(); 00728 00729 if (options && options->readGroupFile) { 00730 groupFile = Cmd_FileOpen(options->readGroupFile, "r", NIL(char *), 1); 00731 if (groupFile == NIL(FILE)) { 00732 fprintf(vis_stderr, "** ardc error : can't open file [%s] to read.\n", 00733 options->readGroupFile); 00734 } 00735 } 00736 00737 if (groupFile) { 00738 latchNameArray = array_alloc(char *, 0); 00739 groupIndexArray = array_alloc(int, 0); 00740 ArdcReadGroup(network, groupFile, latchNameArray, groupIndexArray); 00741 subsystemInfo = Part_PartitionSubsystemInfoInit(network); 00742 partitionArray = Part_PartCreateSubsystems(subsystemInfo, 00743 latchNameArray, groupIndexArray); 00744 Part_PartitionSubsystemInfoFree(subsystemInfo); 00745 arrayForEachItem(char *, latchNameArray, i, name) { 00746 FREE(name); 00747 } 00748 array_free(latchNameArray); 00749 array_free(groupIndexArray); 00750 fclose(groupFile); 00751 groupFile = NIL(FILE); 00752 } else if (groupSize > 0) { 00753 subsystemInfo = Part_PartitionSubsystemInfoInit(network); 00754 /* 00755 Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity); 00756 */ 00757 Part_PartitionSubsystemInfoSetBound(subsystemInfo, groupSize); 00758 Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor); 00759 latchNameArray = array_alloc(char *, 0); 00760 arrayForEachItem(int, presentStateVars, i, mddId) { 00761 latch = Ntk_NetworkFindNodeByMddId(network, mddId); 00762 name = Ntk_NodeReadName(latch); 00763 array_insert_last(char *, latchNameArray, name); 00764 } 00765 partitionArray = Part_PartCreateSubsystems(subsystemInfo, 00766 latchNameArray, NIL(array_t)); 00767 array_free(latchNameArray); 00768 Part_PartitionSubsystemInfoFree(subsystemInfo); 00769 } else { 00770 partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network, 00771 nextStateFunctions); 00772 } 00773 if (verbosity > 0) { 00774 finalTime = util_cpu_time(); 00775 fprintf(vis_stdout, "grouping(state space decomposition) time = %g\n", 00776 (double)(finalTime - initialTime) / 1000.0); 00777 } 00778 00779 return(partitionArray); 00780 } 00781 00782 00794 Fsm_ArdcOptions_t * 00795 Fsm_ArdcAllocOptionsStruct(void) 00796 { 00797 Fsm_ArdcOptions_t *options; 00798 00799 options = ALLOC(Fsm_ArdcOptions_t, 1); 00800 (void)memset((void *)options, 0, sizeof(Fsm_ArdcOptions_t)); 00801 00802 return(options); 00803 } 00804 00805 00892 void 00893 Fsm_ArdcGetDefaultOptions(Fsm_ArdcOptions_t *options) 00894 { 00895 int groupSize = 8; 00896 float affinityFactor = 0.5; 00897 Fsm_Ardc_TraversalType_t traversalMethod = Fsm_Ardc_Traversal_Lmbm_c; 00898 int maxIteration = 0; 00899 Fsm_Ardc_ConstrainTargetType_t constrainTarget = Fsm_Ardc_Constrain_Tr_c; 00900 Img_MinimizeType constrainMethod = Img_Restrict_c; 00901 boolean decomposeFlag = TRUE; 00902 Fsm_Ardc_AbstPpiType_t abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c; 00903 boolean projectedInitialFlag = TRUE; 00904 boolean constrainReorderFlag = TRUE; 00905 Img_MethodType ardcImageMethod = Img_Default_c; 00906 boolean useHighDensity = FALSE; 00907 int createPseudoVarMode = 0; 00908 int verbosity = 0; 00909 char *flagValue; 00910 int value; 00911 float affinity; 00912 boolean reorderPtrFlag = FALSE; 00913 int faninConstrainMode = 0; 00914 int lmbmInitialStatesMode = 1; 00915 int mbmReuseTrFlag = 0; 00916 00917 flagValue = Cmd_FlagReadByName("ardc_traversal_method"); 00918 if (flagValue != NIL(char)) { 00919 sscanf(flagValue, "%d", &value); 00920 switch (value) { 00921 case 0 : 00922 traversalMethod = Fsm_Ardc_Traversal_Mbm_c; 00923 break; 00924 case 1 : 00925 traversalMethod = Fsm_Ardc_Traversal_Rfbf_c; 00926 break; 00927 case 2 : 00928 traversalMethod = Fsm_Ardc_Traversal_Tfbf_c; 00929 break; 00930 case 3 : 00931 traversalMethod = Fsm_Ardc_Traversal_Tmbm_c; 00932 break; 00933 case 4 : 00934 traversalMethod = Fsm_Ardc_Traversal_Lmbm_c; 00935 break; 00936 case 5 : 00937 traversalMethod = Fsm_Ardc_Traversal_Tlmbm_c; 00938 break; 00939 case 6 : /* hidden option */ 00940 traversalMethod = Fsm_Ardc_Traversal_Simple_c; 00941 break; 00942 default : 00943 fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue); 00944 fprintf(vis_stderr, " for ardc_traversal_method[0-5]. **\n"); 00945 break; 00946 } 00947 } 00948 options->traversalMethod = traversalMethod; 00949 00950 flagValue = Cmd_FlagReadByName("ardc_group_size"); 00951 if (flagValue != NIL(char)) { 00952 sscanf(flagValue, "%d", &value); 00953 if (value > 0) 00954 groupSize = value; 00955 else { 00956 fprintf(vis_stderr, 00957 "** ardc error : invalid value %s for ardc_group_size[>0]. **\n", 00958 flagValue); 00959 } 00960 } 00961 options->groupSize = groupSize; 00962 00963 flagValue = Cmd_FlagReadByName("ardc_affinity_factor"); 00964 if (flagValue != NIL(char)) { 00965 sscanf(flagValue, "%f", &affinity); 00966 if (affinity >= 0.0 && affinity <= 1.0) 00967 affinityFactor = affinity; 00968 else { 00969 fprintf(vis_stderr, 00970 "** ardc error : invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n", 00971 flagValue); 00972 } 00973 } 00974 options->affinityFactor = affinityFactor; 00975 00976 flagValue = Cmd_FlagReadByName("ardc_constrain_method"); 00977 if (flagValue != NIL(char)) { 00978 sscanf(flagValue, "%d", &value); 00979 switch (value) { 00980 case 0 : 00981 constrainMethod = Img_Restrict_c; 00982 break; 00983 case 1 : 00984 constrainMethod = Img_Constrain_c; 00985 break; 00986 case 2 : 00987 if (bdd_get_package_name() != CUDD) { 00988 fprintf(vis_stderr, "** ardc error : Compact in ardc_constrain_method"); 00989 fprintf(vis_stderr, " is currently supported by only CUDD. **\n"); 00990 break; 00991 } 00992 constrainMethod = Img_Compact_c; 00993 break; 00994 case 3 : 00995 if (bdd_get_package_name() != CUDD) { 00996 fprintf(vis_stderr, "** ardc error : Squeeze in ardc_constrain_method"); 00997 fprintf(vis_stderr, " is currently supported by only CUDD. **\n"); 00998 break; 00999 } 01000 constrainMethod = Img_Squeeze_c; 01001 break; 01002 case 4 : 01003 constrainMethod = Img_And_c; 01004 break; 01005 default : 01006 fprintf(vis_stderr, 01007 "** ardc error : invalid value %s for ardc_constrain_method[0-4]. **\n", 01008 flagValue); 01009 break; 01010 } 01011 } 01012 options->constrainMethod = constrainMethod; 01013 01014 flagValue = Cmd_FlagReadByName("ardc_constran_to"); 01015 if (flagValue != NIL(char)) { 01016 sscanf(flagValue, "%d", &value); 01017 switch (value) { 01018 case 0 : 01019 constrainTarget = Fsm_Ardc_Constrain_Tr_c; 01020 break; 01021 case 1 : 01022 constrainTarget = Fsm_Ardc_Constrain_Initial_c; 01023 break; 01024 case 2 : 01025 constrainTarget = Fsm_Ardc_Constrain_Both_c; 01026 break; 01027 default : 01028 fprintf(vis_stderr, 01029 "** ardc error : invalid value %s for ardc_constrain_target[0-2]. **\n", 01030 flagValue); 01031 break; 01032 } 01033 } 01034 options->constrainTarget = constrainTarget; 01035 01036 flagValue = Cmd_FlagReadByName("ardc_max_iteration"); 01037 if (flagValue != NIL(char)) { 01038 sscanf(flagValue, "%d", &value); 01039 if (value >= 0) 01040 maxIteration = value; 01041 else { 01042 fprintf(vis_stderr, 01043 "** ardc error : invalid value %s for ardc_max_iteration[>=0]. **\n", 01044 flagValue); 01045 } 01046 } 01047 options->maxIteration = maxIteration; 01048 01049 flagValue = Cmd_FlagReadByName("ardc_abstract_pseudo_input"); 01050 if (flagValue != NIL(char)) { 01051 sscanf(flagValue, "%d", &value); 01052 switch (value) { 01053 case 0 : 01054 abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c; 01055 break; 01056 case 1 : 01057 abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c; 01058 break; 01059 case 2 : 01060 abstractPseudoInput = Fsm_Ardc_Abst_Ppi_After_Image_c; 01061 break; 01062 case 3 : 01063 abstractPseudoInput = Fsm_Ardc_Abst_Ppi_At_End_c; 01064 break; 01065 default : 01066 fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue); 01067 fprintf(vis_stderr, " for ardc_abstract_pseudo_input[0-3]. **\n"); 01068 break; 01069 } 01070 } 01071 options->abstractPseudoInput = abstractPseudoInput; 01072 01073 decomposeFlag = FsmGetArdcSetBooleanValue("ardc_decompose_flag", 01074 decomposeFlag); 01075 options->decomposeFlag = decomposeFlag; 01076 01077 projectedInitialFlag = 01078 FsmGetArdcSetBooleanValue("ardc_projected_initial_flag", 01079 projectedInitialFlag); 01080 options->projectedInitialFlag = projectedInitialFlag; 01081 01082 constrainReorderFlag = FsmGetArdcSetBooleanValue("ardc_constrain_reorder", 01083 constrainReorderFlag); 01084 options->constrainReorderFlag = constrainReorderFlag; 01085 01086 flagValue = Cmd_FlagReadByName("ardc_image_method"); 01087 if (flagValue != NIL(char)) { 01088 if (strcmp(flagValue, "monolithic") == 0) 01089 ardcImageMethod = Img_Monolithic_c; 01090 else if (strcmp(flagValue, "iwls95") == 0) 01091 ardcImageMethod = Img_Iwls95_c; 01092 else if (strcmp(flagValue, "mlp") == 0) 01093 ardcImageMethod = Img_Mlp_c; 01094 else if (strcmp(flagValue, "tfm") == 0) 01095 ardcImageMethod = Img_Tfm_c; 01096 else if (strcmp(flagValue, "hybrid") == 0) 01097 ardcImageMethod = Img_Hybrid_c; 01098 else 01099 fprintf(vis_stderr, "** ardc error : invalid value %s\n", flagValue); 01100 } 01101 options->ardcImageMethod = ardcImageMethod; 01102 01103 useHighDensity = FsmGetArdcSetBooleanValue("ardc_use_high_density", 01104 useHighDensity); 01105 options->useHighDensity = useHighDensity; 01106 01107 createPseudoVarMode = GetArdcSetIntValue("ardc_create_pseudo_var_mode", 0, 2, 01108 createPseudoVarMode); 01109 options->createPseudoVarMode = createPseudoVarMode; 01110 01111 reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr", 01112 reorderPtrFlag); 01113 options->reorderPtrFlag = reorderPtrFlag; 01114 01115 faninConstrainMode = GetArdcSetIntValue("ardc_fanin_constrain_mode", 0, 1, 01116 faninConstrainMode); 01117 options->faninConstrainMode = faninConstrainMode; 01118 01119 flagValue = Cmd_FlagReadByName("ardc_read_group"); 01120 if (flagValue) 01121 options->readGroupFile = flagValue; 01122 else 01123 options->readGroupFile = NIL(char); 01124 01125 flagValue = Cmd_FlagReadByName("ardc_write_group"); 01126 if (flagValue) 01127 options->writeGroupFile = flagValue; 01128 else 01129 options->writeGroupFile = NIL(char); 01130 01131 lmbmInitialStatesMode = GetArdcSetIntValue("ardc_lmbm_initial_mode", 0, 2, 01132 lmbmInitialStatesMode); 01133 options->lmbmInitialStatesMode = lmbmInitialStatesMode; 01134 01135 mbmReuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr", 01136 mbmReuseTrFlag); 01137 options->mbmReuseTrFlag = mbmReuseTrFlag; 01138 01139 verbosity = GetArdcSetIntValue("ardc_verbosity", 0, 3, verbosity); 01140 options->verbosity = verbosity; 01141 } 01142 01143 01155 Fsm_Ardc_TraversalType_t 01156 Fsm_ArdcOptionsReadTraversalMethod(Fsm_ArdcOptions_t *options) 01157 { 01158 return(options->traversalMethod); 01159 } 01160 01161 01173 int 01174 Fsm_ArdcOptionsReadGroupSize(Fsm_ArdcOptions_t *options) 01175 { 01176 return(options->groupSize); 01177 } 01178 01179 01191 float 01192 Fsm_ArdcOptionsReadAffinityFactor(Fsm_ArdcOptions_t *options) 01193 { 01194 return(options->affinityFactor); 01195 } 01196 01197 01209 Img_MinimizeType 01210 Fsm_ArdcOptionsReadConstrainMethod(Fsm_ArdcOptions_t *options) 01211 { 01212 return(options->constrainMethod); 01213 } 01214 01215 01227 Fsm_Ardc_ConstrainTargetType_t 01228 Fsm_ArdcOptionsReadConstrainTarget(Fsm_ArdcOptions_t *options) 01229 { 01230 return(options->constrainTarget); 01231 } 01232 01233 01245 int 01246 Fsm_ArdcOptionsReadMaxIteration(Fsm_ArdcOptions_t *options) 01247 { 01248 return(options->maxIteration); 01249 } 01250 01251 01263 Fsm_Ardc_AbstPpiType_t 01264 Fsm_ArdcOptionsReadAbstractPseudoInput(Fsm_ArdcOptions_t *options) 01265 { 01266 return(options->abstractPseudoInput); 01267 } 01268 01269 01281 boolean 01282 Fsm_ArdcOptionsReadDecomposeFlag(Fsm_ArdcOptions_t *options) 01283 { 01284 return(options->decomposeFlag); 01285 } 01286 01287 01299 boolean 01300 Fsm_ArdcOptionsReadProjectedInitialFlag(Fsm_ArdcOptions_t *options) 01301 { 01302 return(options->projectedInitialFlag); 01303 } 01304 01305 01317 boolean 01318 Fsm_ArdcOptionsReadConstrainReorderFlag(Fsm_ArdcOptions_t *options) 01319 { 01320 return(options->constrainReorderFlag); 01321 } 01322 01323 01335 Img_MethodType 01336 Fsm_ArdcOptionsReadImageMethod(Fsm_ArdcOptions_t *options) 01337 { 01338 return(options->ardcImageMethod); 01339 } 01340 01341 01353 boolean 01354 Fsm_ArdcOptionsReadUseHighDensity(Fsm_ArdcOptions_t *options) 01355 { 01356 return(options->useHighDensity); 01357 } 01358 01359 01371 int 01372 Fsm_ArdcOptionsReadVerbosity(Fsm_ArdcOptions_t *options) 01373 { 01374 return(options->verbosity); 01375 } 01376 01377 01389 void 01390 Fsm_ArdcOptionsSetTraversalMethod(Fsm_ArdcOptions_t *options, 01391 Fsm_Ardc_TraversalType_t traversalMethod) 01392 { 01393 options->traversalMethod = traversalMethod; 01394 } 01395 01396 01408 void 01409 Fsm_ArdcOptionsSetGroupSize(Fsm_ArdcOptions_t *options, int groupSize) 01410 { 01411 options->groupSize = groupSize; 01412 } 01413 01414 01426 void 01427 Fsm_ArdcOptionsSetAffinityFactor(Fsm_ArdcOptions_t *options, 01428 float affinityFactor) 01429 { 01430 options->affinityFactor = affinityFactor; 01431 } 01432 01433 01445 void 01446 Fsm_ArdcOptionsSetConstrainMethod(Fsm_ArdcOptions_t *options, 01447 Img_MinimizeType constrainMethod) 01448 { 01449 options->constrainMethod = constrainMethod; 01450 } 01451 01452 01464 void 01465 Fsm_ArdcOptionsSetConstrainTarget(Fsm_ArdcOptions_t *options, 01466 Fsm_Ardc_ConstrainTargetType_t constrainTarget) 01467 { 01468 options->constrainTarget = constrainTarget; 01469 } 01470 01471 01483 void 01484 Fsm_ArdcOptionsSetMaxIteration(Fsm_ArdcOptions_t *options, int maxIteration) 01485 { 01486 options->maxIteration = maxIteration; 01487 } 01488 01489 01501 void 01502 Fsm_ArdcOptionsSetAbstractPseudoInput(Fsm_ArdcOptions_t *options, 01503 Fsm_Ardc_AbstPpiType_t abstractPseudoInput) 01504 { 01505 options->abstractPseudoInput = abstractPseudoInput; 01506 } 01507 01508 01520 void 01521 Fsm_ArdcOptionsSetDecomposeFlag(Fsm_ArdcOptions_t *options, 01522 boolean decomposeFlag) 01523 { 01524 options->decomposeFlag = decomposeFlag; 01525 } 01526 01527 01539 void 01540 Fsm_ArdcOptionsSetProjectedInitialFlag(Fsm_ArdcOptions_t *options, 01541 boolean projectedInitialFlag) 01542 { 01543 options->projectedInitialFlag = projectedInitialFlag; 01544 } 01545 01546 01558 void 01559 Fsm_ArdcOptionsSetConstrainReorderFlag(Fsm_ArdcOptions_t *options, 01560 int constrainReorderFlag) 01561 { 01562 options->constrainReorderFlag = constrainReorderFlag; 01563 } 01564 01565 01577 void 01578 Fsm_ArdcOptionsSetImageMethod(Fsm_ArdcOptions_t *options, 01579 Img_MethodType ardcImageMethod) 01580 { 01581 options->ardcImageMethod = ardcImageMethod; 01582 } 01583 01584 01596 void 01597 Fsm_ArdcOptionsSetUseHighDensity(Fsm_ArdcOptions_t *options, 01598 boolean useHighDensity) 01599 { 01600 options->useHighDensity = useHighDensity; 01601 } 01602 01603 01615 void 01616 Fsm_ArdcOptionsSetVerbosity(Fsm_ArdcOptions_t *options, int verbosity) 01617 { 01618 options->verbosity = verbosity; 01619 } 01620 01621 01633 double 01634 Fsm_ArdcCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) 01635 { 01636 mdd_t *reached; 01637 array_t *psVars, *reachedArray; 01638 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01639 double numReached = 1.0, tmpReached; 01640 int i; 01641 01642 if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) 01643 return(0.0); 01644 01645 reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm); 01646 arrayForEachItem(mdd_t *, reachedArray, i, reached) { 01647 psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i); 01648 tmpReached = mdd_count_onset(mddManager, reached, psVars); 01649 numReached *= tmpReached; 01650 } 01651 01652 return(numReached); 01653 } 01654 01668 int 01669 Fsm_ArdcBddSizeOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) 01670 { 01671 mdd_t *reached; 01672 array_t *reachedArray; 01673 int i, size = 0; 01674 01675 if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) 01676 return(0); 01677 01678 reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm); 01679 arrayForEachItem(mdd_t *, reachedArray, i, reached) { 01680 size += mdd_size(reached); 01681 } 01682 01683 return(size); 01684 } 01685 01699 mdd_t * 01700 Fsm_ArdcGetMddOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) 01701 { 01702 mdd_t *reached, *reachedSet, *tmp; 01703 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01704 array_t *reachedArray; 01705 int i; 01706 01707 if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) 01708 return(NIL(mdd_t)); 01709 01710 reachedSet = mdd_one(mddManager); 01711 reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm); 01712 arrayForEachItem(mdd_t *, reachedArray, i, reached) { 01713 tmp = reachedSet; 01714 reachedSet = mdd_and(reachedSet, reached, 1, 1); 01715 mdd_free(tmp); 01716 } 01717 01718 return(reachedSet); 01719 } 01720 01732 void 01733 Fsm_ArdcPrintReachabilityResults(Fsm_Fsm_t *fsm, long elapseTime) 01734 { 01735 array_t *psVars = Fsm_FsmReadPresentStateVars(fsm); 01736 mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm); 01737 int nvars = mdd_get_number_of_bdd_vars(mddMgr, psVars); 01738 char apprStr[24], ardcStr[24]; 01739 01740 if (nvars <= EPD_MAX_BIN) { 01741 double mintermAppr, mintermArdc; 01742 01743 mintermAppr = Fsm_ArdcCountOnsetOfOverApproximateReachableStates(fsm); 01744 sprintf(apprStr, "%10g", mintermAppr); 01745 mintermArdc = pow((double)2.0, (double)nvars) - mintermAppr; 01746 sprintf(ardcStr, "%10g", mintermArdc); 01747 } else { 01748 EpDouble apprEpd, ardcEpd; 01749 01750 ArdcEpdCountOnsetOfOverApproximateReachableStates(fsm, &apprEpd); 01751 EpdPow2(nvars, &ardcEpd); 01752 EpdSubtract2(&ardcEpd, &apprEpd); 01753 EpdGetString(&apprEpd, apprStr); 01754 EpdGetString(&ardcEpd, ardcStr); 01755 } 01756 01757 (void)fprintf(vis_stdout,"***********************************************\n"); 01758 (void)fprintf(vis_stdout,"Over-approximate Reachability analysis results:\n"); 01759 (void)fprintf(vis_stdout, "%-30s%s\n", "reachable states = ", apprStr); 01760 (void)fprintf(vis_stdout, "%-30s%s\n", "unreachable states(ARDCs) = ", 01761 ardcStr); 01762 (void)fprintf(vis_stdout, "%-30s%10d\n", "BDD size = ", 01763 Fsm_ArdcBddSizeOfOverApproximateReachableStates(fsm)); 01764 (void)fprintf(vis_stdout, "%-30s%10g\n", "analysis time = ", 01765 (double)elapseTime / 1000.0); 01766 switch (FsmReadReachabilityOverApproxComputationStatus(fsm)) { 01767 case Fsm_Ardc_NotConverged_c : 01768 (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ", 01769 "not converged(invalid)"); 01770 break; 01771 case Fsm_Ardc_Valid_c : 01772 (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ", 01773 "not converged(valid)"); 01774 break; 01775 case Fsm_Ardc_Converged_c : 01776 (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ", 01777 "converged"); 01778 break; 01779 case Fsm_Ardc_Exact_c : 01780 (void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ", 01781 "exact"); 01782 break; 01783 default : 01784 break; 01785 } 01786 } 01787 01799 int 01800 Fsm_ArdcReadVerbosity(void) 01801 { 01802 char *flagValue; 01803 int verbosity = 0; 01804 01805 flagValue = Cmd_FlagReadByName("ardc_verbosity"); 01806 if (flagValue != NIL(char)) 01807 sscanf(flagValue, "%d", &verbosity); 01808 return(verbosity); 01809 } 01810 01811 01812 /*---------------------------------------------------------------------------*/ 01813 /* Definition of internal functions */ 01814 /*---------------------------------------------------------------------------*/ 01815 01827 int 01828 FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates) 01829 { 01830 array_t *overApproxArray; 01831 mdd_t *conjunct; 01832 int i, j; 01833 mdd_t *invariant; 01834 01835 overApproxArray = Fsm_ArdcComputeOverApproximateReachableStates(fsm, 01836 0, 0, 0, 0, 0, 0, 0, 0, NIL(Fsm_ArdcOptions_t)); 01837 01838 /* for each invariant check if the over approx holds */ 01839 arrayForEachItem(mdd_t *, invarStates, i, invariant) { 01840 arrayForEachItem(mdd_t *, overApproxArray, j, conjunct) { 01841 if (conjunct == NIL(mdd_t)) 01842 continue; 01843 if (!mdd_lequal(conjunct, invariant, 1, 1)) 01844 return 0; 01845 } 01846 } 01847 return 1; 01848 } 01849 01850 01862 void 01863 FsmArdcPrintOptions(void) 01864 { 01865 Fsm_ArdcOptions_t options; 01866 char dummy[31]; 01867 01868 Fsm_ArdcGetDefaultOptions(&options); 01869 01870 switch (options.traversalMethod) { 01871 case Fsm_Ardc_Traversal_Mbm_c : 01872 sprintf(dummy, "MBM"); 01873 break; 01874 case Fsm_Ardc_Traversal_Rfbf_c : 01875 sprintf(dummy, "RFBF"); 01876 break; 01877 case Fsm_Ardc_Traversal_Tfbf_c : 01878 sprintf(dummy, "TFBF"); 01879 break; 01880 case Fsm_Ardc_Traversal_Tmbm_c : 01881 sprintf(dummy, "TMBM"); 01882 break; 01883 case Fsm_Ardc_Traversal_Lmbm_c : 01884 sprintf(dummy, "LMBM"); 01885 break; 01886 case Fsm_Ardc_Traversal_Tlmbm_c : 01887 sprintf(dummy, "TLMBM"); 01888 break; 01889 case Fsm_Ardc_Traversal_Simple_c : 01890 sprintf(dummy, "SIMPLE"); 01891 break; 01892 default : 01893 sprintf(dummy, "invalid"); 01894 break; 01895 } 01896 fprintf(vis_stdout, "ARDC: ardc_traversal_method = %d (%s)\n", 01897 options.traversalMethod, dummy); 01898 fprintf(vis_stdout, "ARDC: ardc_group_size = %d\n", options.groupSize); 01899 fprintf(vis_stdout, "ARDC: ardc_affinity_factor = %f\n", 01900 options.affinityFactor); 01901 fprintf(vis_stdout, "ARDC: ardc_max_iteration = %d\n", options.maxIteration); 01902 switch (options.constrainTarget) { 01903 case Fsm_Ardc_Constrain_Tr_c : 01904 sprintf(dummy, "transition relation"); 01905 break; 01906 case Fsm_Ardc_Constrain_Initial_c : 01907 sprintf(dummy, "initial"); 01908 break; 01909 case Fsm_Ardc_Constrain_Both_c : 01910 sprintf(dummy, "both"); 01911 break; 01912 default : 01913 sprintf(dummy, "invalid"); 01914 break; 01915 } 01916 fprintf(vis_stdout, "ARDC: ardc_constrain_target = %d (%s)\n", 01917 options.constrainTarget, dummy); 01918 switch (options.constrainMethod) { 01919 case Img_Restrict_c : 01920 sprintf(dummy, "restrict"); 01921 break; 01922 case Img_Constrain_c : 01923 sprintf(dummy, "constrain"); 01924 break; 01925 case Img_Compact_c : 01926 sprintf(dummy, "compact"); 01927 break; 01928 case Img_Squeeze_c : 01929 sprintf(dummy, "squeeze"); 01930 break; 01931 case Img_And_c : 01932 sprintf(dummy, "and"); 01933 break; 01934 case Img_DefaultMinimizeMethod_c : 01935 sprintf(dummy, "restrict"); 01936 break; 01937 default : 01938 sprintf(dummy, "invalid"); 01939 break; 01940 } 01941 fprintf(vis_stdout, "ARDC: ardc_constrain_method = %d (%s)\n", 01942 options.constrainMethod, dummy); 01943 if (options.constrainReorderFlag) 01944 sprintf(dummy, "yes"); 01945 else 01946 sprintf(dummy, "no"); 01947 fprintf(vis_stdout, "ARDC: ardc_constrain_reorder = %s\n", dummy); 01948 if (options.decomposeFlag) 01949 sprintf(dummy, "yes"); 01950 else 01951 sprintf(dummy, "no"); 01952 fprintf(vis_stdout, "ARDC: ardc_decompose_flag = %s\n", dummy); 01953 switch (options.abstractPseudoInput) { 01954 case Fsm_Ardc_Abst_Ppi_No_c : 01955 sprintf(dummy, "no"); 01956 break; 01957 case Fsm_Ardc_Abst_Ppi_Before_Image_c : 01958 sprintf(dummy, "before image"); 01959 break; 01960 case Fsm_Ardc_Abst_Ppi_After_Image_c : 01961 sprintf(dummy, "after image"); 01962 break; 01963 case Fsm_Ardc_Abst_Ppi_At_End_c : 01964 sprintf(dummy, "at end"); 01965 break; 01966 default : 01967 sprintf(dummy, "invalid"); 01968 break; 01969 } 01970 fprintf(vis_stdout, "ARDC: ardc_abstract_pseudo_input = %d (%s)\n", 01971 options.abstractPseudoInput, dummy); 01972 if (options.projectedInitialFlag) 01973 sprintf(dummy, "yes"); 01974 else 01975 sprintf(dummy, "no"); 01976 fprintf(vis_stdout, "ARDC: ardc_projected_initial_flag = %s\n", dummy); 01977 if (options.ardcImageMethod == Img_Monolithic_c) 01978 sprintf(dummy, "monolithic"); 01979 else if (options.ardcImageMethod == Img_Tfm_c) 01980 sprintf(dummy, "tfm"); 01981 else if (options.ardcImageMethod == Img_Hybrid_c) 01982 sprintf(dummy, "hybrid"); 01983 else if (options.ardcImageMethod == Img_Mlp_c) 01984 sprintf(dummy, "mlp"); 01985 else 01986 sprintf(dummy, "iwls95"); 01987 fprintf(vis_stdout, "ARDC: ardc_image_method = %s\n", dummy); 01988 if (options.useHighDensity) 01989 sprintf(dummy, "yes"); 01990 else 01991 sprintf(dummy, "no"); 01992 fprintf(vis_stdout, "ARDC: ardc_use_high_density = %s\n", dummy); 01993 if (options.reorderPtrFlag) 01994 sprintf(dummy, "yes"); 01995 else 01996 sprintf(dummy, "no"); 01997 fprintf(vis_stdout, "ARDC: ardc_reorder_ptr = %s\n", dummy); 01998 if (options.faninConstrainMode == 0) 01999 sprintf(dummy, "only fanin"); 02000 else 02001 sprintf(dummy, "fanin + itself"); 02002 fprintf(vis_stdout, "ARDC: ardc_fanin_constrain_mode = %d (%s)\n", 02003 options.faninConstrainMode, dummy); 02004 if (options.createPseudoVarMode == 0) 02005 sprintf(dummy, "with exact support"); 02006 else if (options.createPseudoVarMode == 1) 02007 sprintf(dummy, "all the other submachines"); 02008 else 02009 sprintf(dummy, "only fanin submachines"); 02010 fprintf(vis_stdout, "ARDC: ardc_create_pseudo_var_mode = %d (%s)\n", 02011 options.createPseudoVarMode, dummy); 02012 if (options.lmbmInitialStatesMode == 0) 02013 sprintf(dummy, "given initial"); 02014 else if (options.lmbmInitialStatesMode == 1) 02015 sprintf(dummy, "reached set"); 02016 else 02017 sprintf(dummy, "frontier set"); 02018 fprintf(vis_stdout, "ARDC: ardc_lmbm_initial_mode = %d (%s)\n", 02019 options.lmbmInitialStatesMode, dummy); 02020 if (options.mbmReuseTrFlag) 02021 sprintf(dummy, "yes"); 02022 else 02023 sprintf(dummy, "no"); 02024 fprintf(vis_stdout, "ARDC: ardc_mbm_reuse_tr = %s\n", dummy); 02025 if (options.readGroupFile) 02026 fprintf(vis_stdout, "ARDC: ardc_read_group = %s\n", options.readGroupFile); 02027 else 02028 fprintf(vis_stdout, "ARDC: ardc_read_group = nil\n"); 02029 if (options.writeGroupFile) { 02030 fprintf(vis_stdout, "ARDC: ardc_write_group = %s\n", 02031 options.writeGroupFile); 02032 } else 02033 fprintf(vis_stdout, "ARDC: ardc_write_group = nil\n"); 02034 fprintf(vis_stdout, "ARDC: ardc_verbosity = %d\n", options.verbosity); 02035 fprintf(vis_stdout, 02036 "See help page on print_ardc_options for setting these options\n"); 02037 } 02038 02039 02040 02052 void 02053 FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm) 02054 { 02055 mdd_t *appr; 02056 array_t *mddIdArr; 02057 02058 if (!Fsm_FsmTestIsOverApproximateReachabilityDone(fsm)) { 02059 fprintf(vis_stdout, "** ardc warning : no approximate reachable states **\n"); 02060 return; 02061 } 02062 appr = Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm); 02063 mddIdArr = Fsm_FsmReadPresentStateVars(fsm); 02064 PrintBddWithName(fsm, mddIdArr, appr); 02065 } 02066 02078 void 02079 FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm) 02080 { 02081 mdd_t *reachableStates; 02082 array_t *mddIdArr; 02083 02084 if (!Fsm_FsmTestIsReachabilityDone(fsm)) { 02085 fprintf(vis_stdout, "** ardc warning : no reachable states **\n"); 02086 return; 02087 } 02088 reachableStates = Fsm_FsmReadReachableStates(fsm); 02089 mddIdArr = Fsm_FsmReadPresentStateVars(fsm); 02090 PrintBddWithName(fsm, mddIdArr, reachableStates); 02091 } 02092 02093 02105 void 02106 FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node) 02107 { 02108 PrintBddWithName(fsm, NIL(array_t), node); 02109 } 02110 02111 02123 void 02124 FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray) 02125 { 02126 int i, j, n; 02127 array_t *array; 02128 02129 for (i = 0; i < array_n(arrayOfArray); i++) { 02130 array = array_fetch(array_t *, arrayOfArray, i); 02131 fprintf(vis_stdout, "array[%d] =", i); 02132 for (j = 0; j < array_n(array); j++) { 02133 n = array_fetch(int, array, j); 02134 fprintf(vis_stdout, " %d", n); 02135 } 02136 fprintf(vis_stdout, "\n"); 02137 } 02138 } 02139 02151 boolean 02152 FsmGetArdcSetBooleanValue(char *string, boolean defaultValue) 02153 { 02154 char *flagValue; 02155 boolean value = defaultValue; 02156 02157 flagValue = Cmd_FlagReadByName(string); 02158 if (flagValue != NIL(char)) { 02159 if (strcmp(flagValue, "yes") == 0) 02160 value = TRUE; 02161 else if (strcmp(flagValue, "no") == 0) 02162 value = FALSE; 02163 else { 02164 fprintf(vis_stderr, 02165 "** ardc error : invalid value %s for %s[yes/no]. **\n", 02166 flagValue, string); 02167 } 02168 } 02169 02170 return(value); 02171 } 02172 02173 02174 02175 /*---------------------------------------------------------------------------*/ 02176 /* Definition of static functions */ 02177 /*---------------------------------------------------------------------------*/ 02178 02179 02191 static void 02192 SortSubFsmsForApproximateTraversal(array_t **subFsmArray, 02193 array_t **fanInsIndexArray, 02194 array_t **fanOutsIndexArray, 02195 int verbosityLevel) 02196 { 02197 int n = array_n(*subFsmArray); 02198 array_t *newSubFsmArray; 02199 array_t *newFanInsIndexArray; 02200 array_t *newFanOutsIndexArray; 02201 int i, j, smallest; 02202 Fsm_Fsm_t *subFsm; 02203 array_t *fanIns, *fanOuts; 02204 Fsm_Fsm_t *smallestSubFsm = NIL(Fsm_Fsm_t); 02205 array_t *smallestFanIns = NIL(array_t); 02206 array_t *smallestFanOuts = NIL(array_t); 02207 int *flag; 02208 int *nFanIns, *nFanOuts; 02209 int fanIn, fanOut; 02210 int *order = NIL(int); 02211 int *target; 02212 02213 newSubFsmArray = array_alloc(Fsm_Fsm_t *, 0); 02214 newFanInsIndexArray = array_alloc(array_t *, 0); 02215 newFanOutsIndexArray = array_alloc(array_t *, 0); 02216 02217 flag = ALLOC(int, n); 02218 (void)memset((void *)flag, 0, sizeof(int) * n); 02219 02220 if (verbosityLevel > 1) 02221 order = ALLOC(int, n); 02222 target = ALLOC(int, n); 02223 nFanIns = ALLOC(int, n); 02224 nFanOuts = ALLOC(int, n); 02225 for (i = 0; i < n; i++) { 02226 fanIns = array_fetch(array_t *, *fanInsIndexArray, i); 02227 nFanIns[i] = array_n(fanIns); 02228 fanOuts = array_fetch(array_t *, *fanOutsIndexArray, i); 02229 nFanOuts[i] = array_n(fanOuts); 02230 } 02231 02232 for (i = 0; i < n; i++) { 02233 /* 02234 ** finds a submachine which has the smallest number of fanins 02235 ** if tie, use number of fanouts 02236 */ 02237 smallest = -1; 02238 for (j = 0; j < n; j++) { 02239 if (flag[j]) 02240 continue; 02241 subFsm = array_fetch(Fsm_Fsm_t *, *subFsmArray, j); 02242 fanIns = array_fetch(array_t *, *fanInsIndexArray, j); 02243 fanOuts = array_fetch(array_t *, *fanOutsIndexArray, j); 02244 if (smallest == -1 || nFanIns[j] < nFanIns[smallest] || 02245 (nFanIns[j] == nFanIns[smallest] && 02246 nFanOuts[j] < nFanOuts[smallest])) { 02247 smallest = j; 02248 smallestSubFsm = subFsm; 02249 smallestFanIns = fanIns; 02250 smallestFanOuts = fanOuts; 02251 } 02252 } 02253 target[smallest] = i; 02254 if (verbosityLevel > 1) 02255 order[i] = smallest; 02256 flag[smallest] = 1; 02257 array_insert_last(Fsm_Fsm_t *, newSubFsmArray, smallestSubFsm); 02258 array_insert_last(array_t *, newFanInsIndexArray, smallestFanIns); 02259 array_insert_last(array_t *, newFanOutsIndexArray, smallestFanOuts); 02260 /* 02261 ** decrease number of fanouts by 1 from each submachine 02262 ** which is not chosen yet 02263 */ 02264 for (j = 0; j < array_n(smallestFanIns); j++) { 02265 fanIn = array_fetch(int, smallestFanIns, j); 02266 if (flag[fanIn]) 02267 continue; 02268 nFanOuts[fanIn]--; 02269 } 02270 /* 02271 ** decrease number of fanins by 1 from each submachine 02272 ** which is not chosen yet 02273 */ 02274 for (j = 0; j < array_n(smallestFanOuts); j++) { 02275 fanOut = array_fetch(int, smallestFanOuts, j); 02276 if (flag[fanOut]) 02277 continue; 02278 nFanIns[fanOut]--; 02279 } 02280 } 02281 02282 /* make new fanins & fanouts index array according to new order */ 02283 for (i = 0; i < n; i++) { 02284 fanIns = array_fetch(array_t *, newFanInsIndexArray, i); 02285 for (j = 0; j < array_n(fanIns); j++) { 02286 fanIn = array_fetch(int, fanIns, j); 02287 array_insert(int, fanIns, j, target[fanIn]); 02288 } 02289 fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i); 02290 for (j = 0; j < array_n(fanOuts); j++) { 02291 fanOut = array_fetch(int, fanOuts, j); 02292 array_insert(int, fanOuts, j, target[fanOut]); 02293 } 02294 } 02295 02296 if (verbosityLevel > 1) { 02297 int k; 02298 02299 fprintf(vis_stdout, "=== sorted sub-fsm order ===\n"); 02300 for (i = 0; i < n; i++) 02301 fprintf(vis_stdout, " %d", order[i]); 02302 fprintf(vis_stdout, "\n"); 02303 02304 for (i = 0; i < n; i++) { 02305 fprintf(vis_stdout, "SUB-FSM [%d]\n", i); 02306 fanIns = array_fetch(array_t *, newFanInsIndexArray, i); 02307 fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i); 02308 fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns)); 02309 for (j = 0; j < array_n(fanIns); j++) { 02310 k = array_fetch(int, fanIns, j); 02311 fprintf(vis_stdout, " %d", k); 02312 } 02313 fprintf(vis_stdout, "\n"); 02314 fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts)); 02315 for (j = 0; j < array_n(fanOuts); j++) { 02316 k = array_fetch(int, fanOuts, j); 02317 fprintf(vis_stdout, " %d", k); 02318 } 02319 fprintf(vis_stdout, "\n"); 02320 } 02321 } 02322 02323 FREE(flag); 02324 FREE(nFanIns); 02325 FREE(nFanOuts); 02326 if (verbosityLevel > 1) 02327 FREE(order); 02328 FREE(target); 02329 array_free(*subFsmArray); 02330 array_free(*fanInsIndexArray); 02331 array_free(*fanOutsIndexArray); 02332 *subFsmArray = newSubFsmArray; 02333 *fanInsIndexArray = newFanInsIndexArray; 02334 *fanOutsIndexArray = newFanOutsIndexArray; 02335 } 02336 02337 02400 static array_t * 02401 ArdcMbmTraversal( 02402 Fsm_Fsm_t *fsm, 02403 int nvars, 02404 array_t *subFsmArray, 02405 array_t *fanInsIndexArray, 02406 array_t *fanOutsIndexArray, 02407 mdd_t ***subReached /* sub-result for TMBM, pointer of bdd array */, 02408 /* The following arguments up to approxFlag are passed for exact 02409 * reachability. */ 02410 int incrementalFlag, 02411 int verbosityLevel, 02412 int printStep, 02413 int depthValue, 02414 int shellFlag, 02415 int reorderFlag, 02416 int reorderThreshold, 02417 Fsm_RchType_t approxFlag, 02418 Fsm_ArdcOptions_t *options, 02419 boolean lfpFlag /* If TRUE, performs LMBM */ 02420 ) 02421 { 02422 mdd_manager *mddManager; 02423 int i, n = array_n(subFsmArray); 02424 int *traverse; 02425 mdd_t **reached, **constraint; 02426 mdd_t **oldReached; 02427 mdd_t **frontier; 02428 int converged = 0; 02429 Fsm_Fsm_t **subFsm; 02430 array_t *fans; 02431 mdd_t *tmp; 02432 int iteration = 0; 02433 mdd_t **initial = NIL(mdd_t *); 02434 array_t *reachedArray = array_alloc(mdd_t *, 0); 02435 array_t *faninConstrainArray; 02436 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); 02437 int dynStatus; 02438 bdd_reorder_type_t dynMethod; 02439 boolean restoreContainmentFlag; 02440 boolean reuseTrFlag = FALSE; 02441 /* If set, just update the transition relation 02442 without copying the original transition relation */ 02443 boolean reused = FALSE; 02444 boolean duplicate; 02445 boolean tmpReorderPtrFlag; 02446 int nConstrainOps = 0; 02447 long tImgComps = 0; 02448 long tConstrainOps = 0; 02449 long tRestoreContainment = 0; 02450 long tAbstractVars = 0; 02451 long tBuildTr = 0; 02452 long initialTime = 0, finalTime; 02453 int maxIteration = options->maxIteration; 02454 int constrainTarget = options->constrainTarget; 02455 boolean decomposeFlag = options->decomposeFlag; 02456 int abstractPseudoInput = options->abstractPseudoInput; 02457 Img_MinimizeType constrainMethod = options->constrainMethod; 02458 boolean projectedInitialFlag = options->projectedInitialFlag; 02459 int ardcVerbosity = options->verbosity; 02460 boolean constrainReorderFlag = options->constrainReorderFlag; 02461 boolean reorderPtrFlag = options->reorderPtrFlag; 02462 int faninConstrainMode = options->faninConstrainMode; 02463 int lmbmInitialStatesMode = options->lmbmInitialStatesMode; 02464 02465 reuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr", reuseTrFlag); 02466 if (reuseTrFlag && lfpFlag) { 02467 /* This is to use the i-th constrained transition relation in 02468 * the (i+1)-th iteration, instead of the original transition relation. 02469 * Therefore, the i-th constraint should be a superset of the (i+1)-th. */ 02470 fprintf(vis_stderr, 02471 "** ardc error : can't reuse transition relation in LMBM. **\n"); 02472 reuseTrFlag = FALSE; 02473 } 02474 02475 Img_ResetNumberOfImageComputation(Img_Forward_c); 02476 02477 reached = ALLOC(mdd_t *, n); 02478 constraint = ALLOC(mdd_t *, n); 02479 traverse = ALLOC(int, n); /* array used for scheduling */ 02480 subFsm = ALLOC(Fsm_Fsm_t *, n); 02481 oldReached = ALLOC(mdd_t *, n); 02482 02483 mddManager = Fsm_FsmReadMddManager(fsm); 02484 for (i = 0; i < n; i++) { 02485 subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 02486 oldReached[i] = NIL(mdd_t); 02487 } 02488 02489 /* Set up. */ 02490 if (lfpFlag) { /* LMBM */ 02491 initial = ALLOC(mdd_t *, n); 02492 for (i = 0; i < n; i++) 02493 initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]); 02494 if (lmbmInitialStatesMode >= 1) /* restart from frontier states */ 02495 frontier = ALLOC(mdd_t *, n); 02496 else 02497 frontier = NIL(mdd_t *); 02498 02499 for (i = 0; i < n; i++) { 02500 reached[i] = mdd_dup(initial[i]); 02501 constraint[i] = mdd_dup(initial[i]); 02502 traverse[i] = 1; 02503 if (frontier) 02504 frontier[i] = NIL(mdd_t); 02505 } 02506 } else { /* MBM */ 02507 for (i = 0; i < n; i++) { 02508 reached[i] = mdd_one(mddManager); 02509 constraint[i] = mdd_one(mddManager); 02510 traverse[i] = 1; 02511 } 02512 02513 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 02514 constrainTarget == Fsm_Ardc_Constrain_Both_c) { 02515 initial = ALLOC(mdd_t *, n); 02516 for (i = 0; i < n; i++) 02517 initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]); 02518 } 02519 02520 frontier = NIL(mdd_t *); 02521 } 02522 02523 /* Set the flag for containment restoration according to the options. */ 02524 if (constrainMethod == Img_Constrain_c && 02525 constrainReorderFlag == FALSE && 02526 abstractPseudoInput == Fsm_Ardc_Abst_Ppi_No_c) { 02527 restoreContainmentFlag = FALSE; 02528 } else 02529 restoreContainmentFlag = TRUE; 02530 02531 /* Compute fixpoint. */ 02532 do { 02533 converged = 1; 02534 for (i = 0; i < n; i++) { 02535 if (!traverse[i]) 02536 continue; 02537 if (ardcVerbosity > 1) 02538 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 02539 if (oldReached[i]) 02540 mdd_free(oldReached[i]); 02541 oldReached[i] = reached[i]; 02542 /* Build constraint array. */ 02543 faninConstrainArray = array_alloc(mdd_t *, 0); 02544 fans = array_fetch(array_t *, fanInsIndexArray, i); 02545 ComputeFaninConstrainArray(faninConstrainArray, constraint, 02546 i, fans, decomposeFlag, faninConstrainMode); 02547 /* Build constrained transition relation. */ 02548 dynStatus = bdd_reordering_status(mddManager, &dynMethod); 02549 if (dynStatus != 0 && constrainReorderFlag == 0) 02550 bdd_dynamic_reordering_disable(mddManager); 02551 if (ardcVerbosity > 0) 02552 initialTime = util_cpu_time(); 02553 imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); /* forward */ 02554 if (ardcVerbosity > 0) { 02555 finalTime = util_cpu_time(); 02556 tBuildTr += finalTime - initialTime; 02557 } 02558 /* Minimize the transition relation of the current submachine w.r.t. 02559 * the reached set of its fanin submachines. 02560 */ 02561 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) { 02562 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 02563 if (ardcVerbosity > 2) 02564 Img_SetPrintMinimizeStatus(imageInfo, 2); 02565 else if (ardcVerbosity > 0) 02566 Img_SetPrintMinimizeStatus(imageInfo, 1); 02567 else 02568 Img_SetPrintMinimizeStatus(imageInfo, 0); 02569 if (reuseTrFlag) { 02570 if (reused) 02571 duplicate = FALSE; 02572 else 02573 duplicate = TRUE; 02574 } else 02575 duplicate = TRUE; 02576 if (reorderPtrFlag && 02577 abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) { 02578 tmpReorderPtrFlag = 1; 02579 } else 02580 tmpReorderPtrFlag = 0; 02581 if (ardcVerbosity > 0) 02582 initialTime = util_cpu_time(); 02583 MinimizeTransitionRelationWithFaninConstraint(imageInfo, 02584 faninConstrainArray, constrainMethod, tmpReorderPtrFlag, 02585 duplicate); 02586 if (ardcVerbosity > 0) { 02587 finalTime = util_cpu_time(); 02588 tConstrainOps += finalTime - initialTime; 02589 } 02590 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 02591 } 02592 if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) { 02593 ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray, 02594 constrainMethod); 02595 } 02596 nConstrainOps++; 02597 mdd_array_free(faninConstrainArray); 02598 /* Restore dynamic reordering options if they had been changed. */ 02599 if (dynStatus != 0 && constrainReorderFlag == 0) { 02600 bdd_dynamic_reordering(mddManager, dynMethod, 02601 BDD_REORDER_VERBOSITY_DEFAULT); 02602 } 02603 /* Quantify pseudo-input variables from the transition relation. */ 02604 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 02605 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 02606 if (ardcVerbosity > 2) 02607 Img_SetPrintMinimizeStatus(imageInfo, 2); 02608 else if (ardcVerbosity > 0) 02609 Img_SetPrintMinimizeStatus(imageInfo, 1); 02610 else 02611 Img_SetPrintMinimizeStatus(imageInfo, 0); 02612 if (ardcVerbosity > 0) 02613 initialTime = util_cpu_time(); 02614 Img_AbstractTransitionRelation(imageInfo, 02615 subFsm[i]->fsmData.pseudoInputBddVars, 02616 subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c); 02617 if (reorderPtrFlag) 02618 Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c); 02619 if (ardcVerbosity > 0) { 02620 finalTime = util_cpu_time(); 02621 tAbstractVars += finalTime - initialTime; 02622 } 02623 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 02624 } 02625 if (lfpFlag && lmbmInitialStatesMode > 0 && iteration > 0) { 02626 /* Update the initial states to either reached or frontier. */ 02627 FsmSetReachabilityApproxComputationStatus(subFsm[i], Fsm_Rch_Under_c); 02628 mdd_free(subFsm[i]->reachabilityInfo.initialStates); 02629 if (lmbmInitialStatesMode == 1) 02630 subFsm[i]->reachabilityInfo.initialStates = mdd_dup(reached[i]); 02631 else 02632 subFsm[i]->reachabilityInfo.initialStates = mdd_dup(frontier[i]); 02633 } else { 02634 /* Reset the reachable states for a new reachability. */ 02635 if (subFsm[i]->reachabilityInfo.reachableStates) { 02636 mdd_free(subFsm[i]->reachabilityInfo.reachableStates); 02637 subFsm[i]->reachabilityInfo.reachableStates = NIL(mdd_t); 02638 } 02639 subFsm[i]->reachabilityInfo.depth = 0; 02640 } 02641 /* Traverse this submachine. */ 02642 if (ardcVerbosity > 0) 02643 initialTime = util_cpu_time(); 02644 reached[i] = Fsm_FsmComputeReachableStates(subFsm[i], 02645 incrementalFlag, verbosityLevel, printStep, depthValue, 02646 shellFlag, reorderFlag, reorderThreshold, 02647 approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t)); 02648 if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || 02649 Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { 02650 Img_TfmFlushCache(imageInfo, FALSE); 02651 } 02652 if (ardcVerbosity > 0) { 02653 finalTime = util_cpu_time(); 02654 tImgComps += finalTime - initialTime; 02655 } 02656 /* Compute the frontier for LMBM. */ 02657 if (lfpFlag && lmbmInitialStatesMode > 0) { 02658 if (lmbmInitialStatesMode >= 1) { 02659 if (iteration == 0) 02660 frontier[i] = mdd_dup(reached[i]); 02661 else { 02662 mdd_t *fromLowerBound; 02663 02664 fromLowerBound = mdd_and(reached[i], oldReached[i], 1, 0); 02665 tmp = reached[i]; 02666 reached[i] = mdd_or(oldReached[i], tmp, 1, 1); 02667 mdd_free(tmp); 02668 mdd_free(frontier[i]); 02669 if (lmbmInitialStatesMode == 2) { 02670 frontier[i] = bdd_between(fromLowerBound, reached[i]); 02671 mdd_free(fromLowerBound); 02672 } else 02673 frontier[i] = fromLowerBound; 02674 } 02675 } 02676 if (iteration > 0) { 02677 mdd_free(subFsm[i]->reachabilityInfo.initialStates); 02678 subFsm[i]->reachabilityInfo.initialStates = mdd_dup(initial[i]); 02679 } 02680 } 02681 /* Restore the original transition relation. */ 02682 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) { 02683 if (!reuseTrFlag) 02684 Img_RestoreTransitionRelation(imageInfo, Img_Forward_c); 02685 } 02686 /* Quantify the pseudo-input variables from reached. */ 02687 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) { 02688 if (ardcVerbosity > 0) 02689 initialTime = util_cpu_time(); 02690 if (n > 1) { 02691 tmp = reached[i]; 02692 reached[i] = QuantifyVariables(reached[i], 02693 subFsm[i]->fsmData.pseudoInputBddVars, 02694 subFsm[i]->fsmData.pseudoInputCube); 02695 mdd_free(tmp); 02696 } 02697 if (ardcVerbosity > 0) { 02698 finalTime = util_cpu_time(); 02699 tAbstractVars += finalTime - initialTime; 02700 } 02701 } 02702 02703 mdd_free(constraint[i]); 02704 constraint[i] = mdd_dup(reached[i]); 02705 /* Update traversal schedule and possibly restore containment. */ 02706 traverse[i] = 0; 02707 if (!mdd_equal(oldReached[i], reached[i])) { 02708 if (ardcVerbosity > 2) { 02709 double r1, r2; 02710 02711 r1 = mdd_count_onset(mddManager, reached[i], 02712 subFsm[i]->fsmData.presentStateVars); 02713 r2 = mdd_count_onset(mddManager, oldReached[i], 02714 subFsm[i]->fsmData.presentStateVars); 02715 fprintf(vis_stdout, "oldReached = %g, reached = %g\n", r2, r1); 02716 } 02717 02718 /* Restore-containment operation. */ 02719 if (restoreContainmentFlag) { 02720 if (ardcVerbosity > 0) 02721 initialTime = util_cpu_time(); 02722 if (lfpFlag) { /* LMBM */ 02723 if (mdd_lequal(oldReached[i], reached[i], 1, 1)) { 02724 /* Containment OK. */ 02725 fans = array_fetch(array_t *, fanOutsIndexArray, i); 02726 UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag); 02727 } else { 02728 /* Restoration needed. */ 02729 if (ardcVerbosity > 1) { 02730 fprintf(vis_stdout, 02731 "** ardc info: reached is not superset of oldReached in subFsm[%d] **\n", 02732 i); 02733 } 02734 mdd_free(reached[i]); 02735 reached[i] = mdd_or(oldReached[i], 02736 subFsm[i]->reachabilityInfo.reachableStates, 1, 1); 02737 mdd_free(subFsm[i]->reachabilityInfo.reachableStates); 02738 subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]); 02739 mdd_free(constraint[i]); 02740 constraint[i] = mdd_dup(reached[i]); 02741 if (!mdd_equal(oldReached[i], reached[i])) { 02742 fans = array_fetch(array_t *, fanOutsIndexArray, i); 02743 UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag); 02744 } 02745 } 02746 } else { /* MBM */ 02747 if (!mdd_lequal(reached[i], oldReached[i], 1, 1)) { 02748 /* Restoration needed. */ 02749 if (ardcVerbosity > 1) { 02750 fprintf(vis_stdout, 02751 "** ardc info: reached is not subset of oldReached in subFsm[%d] **\n", i); 02752 } 02753 mdd_free(reached[i]); 02754 reached[i] = mdd_and(oldReached[i], 02755 subFsm[i]->reachabilityInfo.reachableStates, 1, 1); 02756 mdd_free(subFsm[i]->reachabilityInfo.reachableStates); 02757 subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]); 02758 mdd_free(constraint[i]); 02759 constraint[i] = mdd_dup(reached[i]); 02760 if (!mdd_equal(oldReached[i], reached[i])) { 02761 fans = array_fetch(array_t *, fanOutsIndexArray, i); 02762 UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag); 02763 } 02764 } else { 02765 /* Containment OK. */ 02766 fans = array_fetch(array_t *, fanOutsIndexArray, i); 02767 UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag); 02768 } 02769 } 02770 if (ardcVerbosity > 0) { 02771 finalTime = util_cpu_time(); 02772 tRestoreContainment += finalTime - initialTime; 02773 } 02774 } else { /* no containment restoration needed */ 02775 fans = array_fetch(array_t *, fanOutsIndexArray, i); 02776 UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag); 02777 } 02778 } 02779 } 02780 /* Check for convergence. */ 02781 for (i = 0; i < n; i++) { 02782 if (traverse[i]) { 02783 converged = 0; 02784 break; 02785 } 02786 } 02787 iteration++; 02788 if (ardcVerbosity > 0) { 02789 boolean supportCheckFlag = FALSE; 02790 02791 /* Print the current reached states and check the supports. */ 02792 if (projectedInitialFlag || 02793 abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 02794 supportCheckFlag = TRUE; 02795 } 02796 if (lfpFlag) { 02797 PrintCurrentReachedStates(mddManager, subFsm, reached, 02798 Fsm_Ardc_Traversal_Lmbm_c, 02799 n, iteration, nvars, ardcVerbosity, 02800 supportCheckFlag); 02801 } else { 02802 PrintCurrentReachedStates(mddManager, subFsm, reached, 02803 Fsm_Ardc_Traversal_Mbm_c, 02804 n, iteration, nvars, ardcVerbosity, 02805 supportCheckFlag); 02806 } 02807 } 02808 02809 if (iteration == maxIteration) 02810 break; 02811 } while (!converged); 02812 02813 /* Restore the original transtion relation. */ 02814 if (reuseTrFlag) { 02815 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) 02816 Img_RestoreTransitionRelation(imageInfo, Img_Forward_c); 02817 } 02818 02819 if (ardcVerbosity > 0) { 02820 if (lfpFlag) 02821 fprintf(vis_stdout, "LMBM : total iterations %d\n", iteration); 02822 else 02823 fprintf(vis_stdout, "MBM : total iterations %d\n", iteration); 02824 } 02825 02826 /* Reset the initial states to the original. */ 02827 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 02828 constrainTarget == Fsm_Ardc_Constrain_Both_c || lfpFlag) { 02829 for (i = 0; i < n; i++) { 02830 mdd_free(subFsm[i]->reachabilityInfo.initialStates); 02831 subFsm[i]->reachabilityInfo.initialStates = initial[i]; 02832 } 02833 FREE(initial); 02834 } 02835 02836 /* Quantify the pseudo-input variables from reached. */ 02837 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) { 02838 if (ardcVerbosity > 0) 02839 initialTime = util_cpu_time(); 02840 for (i = 0; i < n; i++) { 02841 tmp = reached[i]; 02842 reached[i] = QuantifyVariables(reached[i], 02843 subFsm[i]->fsmData.pseudoInputBddVars, 02844 subFsm[i]->fsmData.pseudoInputCube); 02845 mdd_free(tmp); 02846 } 02847 if (ardcVerbosity > 0) { 02848 finalTime = util_cpu_time(); 02849 tAbstractVars += finalTime - initialTime; 02850 } 02851 } 02852 02853 /* Set the status of current overapproximate reached states. */ 02854 if (converged) 02855 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c); 02856 else if (lfpFlag) 02857 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c); 02858 else 02859 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Valid_c); 02860 02861 ComputeApproximateReachableStatesArray(mddManager, reachedArray, 02862 reached, subReached, n, 02863 decomposeFlag); 02864 /* Clean up. */ 02865 if (decomposeFlag) { 02866 for (i = 0; i < n; i++) { 02867 mdd_free(oldReached[i]); 02868 mdd_free(constraint[i]); 02869 } 02870 } else { 02871 for (i = 0; i < n; i++) { 02872 mdd_free(oldReached[i]); 02873 if (subReached == NULL) 02874 mdd_free(reached[i]); 02875 mdd_free(constraint[i]); 02876 } 02877 } 02878 02879 if (subReached) 02880 *subReached = reached; 02881 else 02882 FREE(reached); 02883 FREE(traverse); 02884 FREE(constraint); 02885 FREE(subFsm); 02886 FREE(oldReached); 02887 if (lfpFlag && lmbmInitialStatesMode >= 1) {/*consistent:from >1 to >=1 C.W*/ 02888 for (i = 0; i < n; i++) { 02889 if (frontier[i]) 02890 mdd_free(frontier[i]); 02891 } 02892 FREE(frontier); 02893 } 02894 02895 /* Print final stats. */ 02896 if (ardcVerbosity > 0) { 02897 fprintf(vis_stdout, "%d image computations, %d constrain operations\n", 02898 Img_GetNumberOfImageComputation(Img_Forward_c), nConstrainOps); 02899 fprintf(vis_stdout, 02900 "image computation time = %g, constrain operation time = %g\n", 02901 (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0); 02902 fprintf(vis_stdout, "restore-containment time = %g\n", 02903 (double)tRestoreContainment / 1000.0); 02904 fprintf(vis_stdout, "abstract variables time = %g\n", 02905 (double)tAbstractVars / 1000.0); 02906 fprintf(vis_stdout, "build TR time = %g\n", 02907 (double)tBuildTr / 1000.0); 02908 } 02909 02910 return(reachedArray); 02911 } 02912 02913 02930 static array_t * 02931 ArdcRfbfTraversal(Fsm_Fsm_t *fsm, int nvars, 02932 array_t *subFsmArray, array_t *fanInsIndexArray, 02933 int incrementalFlag, int verbosityLevel, 02934 int printStep, int depthValue, int shellFlag, 02935 int reorderFlag, int reorderThreshold, 02936 Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options) 02937 { 02938 mdd_manager *mddManager; 02939 int i, n = array_n(subFsmArray); 02940 mdd_t **reached, **constraint, **newConstraint; 02941 mdd_t **newReached, *to; 02942 int converged = 0; 02943 Fsm_Fsm_t **subFsm; 02944 array_t *fans; 02945 mdd_t *tmp; 02946 mdd_t *initialStates; 02947 int iteration = 0; 02948 mdd_t **initial = NIL(mdd_t *); 02949 array_t *reachedArray = array_alloc(mdd_t *, 0); 02950 array_t *faninConstrainArray; 02951 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); 02952 int dynStatus; 02953 bdd_reorder_type_t dynMethod; 02954 boolean restoreContainmentFlag; 02955 mdd_t *toCareSet; 02956 array_t *toCareSetArray = array_alloc(mdd_t *, 0); 02957 int depth = 0; 02958 boolean tmpReorderPtrFlag; 02959 long tImgComps = 0; 02960 long tConstrainOps = 0; 02961 long initialTime = 0, finalTime; 02962 int maxIteration = options->maxIteration; 02963 int constrainTarget = options->constrainTarget; 02964 boolean decomposeFlag = options->decomposeFlag; 02965 int abstractPseudoInput = options->abstractPseudoInput; 02966 Img_MinimizeType constrainMethod = options->constrainMethod; 02967 boolean projectedInitialFlag = options->projectedInitialFlag; 02968 int ardcVerbosity = options->verbosity; 02969 boolean constrainReorderFlag = options->constrainReorderFlag; 02970 boolean reorderPtrFlag = options->reorderPtrFlag; 02971 int faninConstrainMode = options->faninConstrainMode; 02972 02973 Img_ResetNumberOfImageComputation(Img_Forward_c); 02974 02975 reached = ALLOC(mdd_t *, n); 02976 constraint = ALLOC(mdd_t *, n); 02977 newConstraint = ALLOC(mdd_t *, n); 02978 subFsm = ALLOC(Fsm_Fsm_t *, n); 02979 newReached = ALLOC(mdd_t *, n); 02980 02981 mddManager = Fsm_FsmReadMddManager(fsm); 02982 for (i = 0; i < n; i++) { 02983 subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 02984 initialStates = Fsm_FsmComputeInitialStates(subFsm[i]); 02985 reached[i] = initialStates; 02986 constraint[i] = mdd_dup(initialStates); 02987 02988 if (printStep && ((depth % printStep) == 0)) { 02989 if (ardcVerbosity > 1) 02990 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 02991 (void)fprintf(vis_stdout, 02992 "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth, 02993 mdd_count_onset(mddManager, reached[i], 02994 subFsm[i]->fsmData.presentStateVars), 02995 (long)mdd_size(reached[i])); 02996 } 02997 } 02998 02999 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 03000 constrainTarget == Fsm_Ardc_Constrain_Both_c) { 03001 initial = ALLOC(mdd_t *, n); 03002 for (i = 0; i < n; i++) 03003 initial[i] = mdd_dup(reached[i]); 03004 } 03005 03006 if (constrainMethod != Img_Constrain_c || 03007 constrainReorderFlag == TRUE || 03008 abstractPseudoInput != Fsm_Ardc_Abst_Ppi_No_c) { 03009 restoreContainmentFlag = TRUE; 03010 } else 03011 restoreContainmentFlag = FALSE; 03012 03013 converged = 0; 03014 do { 03015 depth++; 03016 for (i = 0; i < n; i++) { 03017 if (ardcVerbosity > 1) 03018 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 03019 faninConstrainArray = array_alloc(mdd_t *, 0); 03020 fans = array_fetch(array_t *, fanInsIndexArray, i); 03021 ComputeFaninConstrainArray(faninConstrainArray, constraint, 03022 i, fans, decomposeFlag, faninConstrainMode); 03023 dynStatus = bdd_reordering_status(mddManager, &dynMethod); 03024 if (dynStatus != 0 && constrainReorderFlag == 0) 03025 bdd_dynamic_reordering_disable(mddManager); 03026 imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); 03027 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) { 03028 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 03029 if (ardcVerbosity > 2) 03030 Img_SetPrintMinimizeStatus(imageInfo, 2); 03031 else if (ardcVerbosity > 0) 03032 Img_SetPrintMinimizeStatus(imageInfo, 1); 03033 else 03034 Img_SetPrintMinimizeStatus(imageInfo, 0); 03035 if (reorderPtrFlag && 03036 abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03037 tmpReorderPtrFlag = 1; 03038 } else 03039 tmpReorderPtrFlag = 0; 03040 if (ardcVerbosity > 0) 03041 initialTime = util_cpu_time(); 03042 MinimizeTransitionRelationWithFaninConstraint(imageInfo, 03043 faninConstrainArray, constrainMethod, tmpReorderPtrFlag, 03044 TRUE); 03045 if (ardcVerbosity > 0) { 03046 finalTime = util_cpu_time(); 03047 tConstrainOps += finalTime - initialTime; 03048 } 03049 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 03050 } 03051 if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) { 03052 ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray, 03053 constrainMethod); 03054 } 03055 mdd_array_free(faninConstrainArray); 03056 if (dynStatus != 0 && constrainReorderFlag == 0) { 03057 bdd_dynamic_reordering(mddManager, dynMethod, 03058 BDD_REORDER_VERBOSITY_DEFAULT); 03059 } 03060 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03061 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 03062 if (ardcVerbosity > 2) 03063 Img_SetPrintMinimizeStatus(imageInfo, 2); 03064 else if (ardcVerbosity > 0) 03065 Img_SetPrintMinimizeStatus(imageInfo, 1); 03066 else 03067 Img_SetPrintMinimizeStatus(imageInfo, 0); 03068 Img_AbstractTransitionRelation(imageInfo, 03069 subFsm[i]->fsmData.pseudoInputBddVars, 03070 subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c); 03071 if (reorderPtrFlag) 03072 Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c); 03073 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 03074 } 03075 toCareSet = mdd_not(reached[i]); 03076 array_insert(mdd_t *, toCareSetArray, 0, toCareSet); 03077 if (ardcVerbosity > 0) 03078 initialTime = util_cpu_time(); 03079 to = Fsm_ArdcComputeImage(subFsm[i], reached[i], reached[i], 03080 toCareSetArray); 03081 if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || 03082 Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { 03083 Img_TfmFlushCache(imageInfo, FALSE); 03084 } 03085 if (ardcVerbosity > 0) { 03086 finalTime = util_cpu_time(); 03087 tImgComps += finalTime - initialTime; 03088 } 03089 mdd_free(toCareSet); 03090 03091 newReached[i] = mdd_or(reached[i], to, 1, 1); 03092 mdd_free(to); 03093 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) 03094 Img_RestoreTransitionRelation(imageInfo, Img_Forward_c); 03095 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) { 03096 tmp = newReached[i]; 03097 newReached[i] = QuantifyVariables(newReached[i], 03098 subFsm[i]->fsmData.pseudoInputBddVars, 03099 subFsm[i]->fsmData.pseudoInputCube); 03100 mdd_free(tmp); 03101 } 03102 03103 /* restore-containment operation */ 03104 if (restoreContainmentFlag) { 03105 if (!mdd_lequal(reached[i], newReached[i], 1, 1)) { 03106 if (ardcVerbosity > 2) { 03107 double r1, r2; 03108 03109 fprintf(vis_stdout, 03110 "** ardc warning : newReached is not superset of reached in subFsm[%d] **\n", 03111 i); 03112 r1 = mdd_count_onset(mddManager, reached[i], 03113 subFsm[i]->fsmData.presentStateVars); 03114 r2 = mdd_count_onset(mddManager, newReached[i], 03115 subFsm[i]->fsmData.presentStateVars); 03116 fprintf(vis_stdout, "reached = %g, newReached = %g\n", r1, r2); 03117 } 03118 tmp = newReached[i]; 03119 newReached[i] = mdd_or(newReached[i], reached[i], 1, 1); 03120 mdd_free(tmp); 03121 } 03122 } 03123 03124 newConstraint[i] = mdd_dup(newReached[i]); 03125 03126 if (printStep && ((depth % printStep) == 0)) { 03127 (void)fprintf(vis_stdout, 03128 "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", 03129 depth, mdd_count_onset(mddManager, newReached[i], 03130 subFsm[i]->fsmData.presentStateVars), 03131 (long)mdd_size(newReached[i])); 03132 } 03133 } 03134 converged = 1; 03135 for (i = 0; i < n; i++) { 03136 if (mdd_equal(reached[i], newReached[i])) 03137 mdd_free(newReached[i]); 03138 else { 03139 converged = 0; 03140 mdd_free(reached[i]); 03141 reached[i] = newReached[i]; 03142 } 03143 } 03144 iteration++; 03145 if (ardcVerbosity > 0) { 03146 boolean supportCheckFlag = FALSE; 03147 03148 if (projectedInitialFlag || 03149 abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03150 supportCheckFlag = TRUE; 03151 } 03152 PrintCurrentReachedStates(mddManager, subFsm, reached, 03153 Fsm_Ardc_Traversal_Rfbf_c, 03154 n, iteration, nvars, ardcVerbosity, 03155 supportCheckFlag); 03156 } 03157 03158 /* update constraints */ 03159 for (i = 0; i < n; i++) { 03160 mdd_free(constraint[i]); 03161 constraint[i] = newConstraint[i]; 03162 newConstraint[i] = NIL(mdd_t); 03163 } 03164 03165 if (iteration == maxIteration) 03166 break; 03167 } while (!converged); 03168 if (ardcVerbosity > 0) { 03169 fprintf(vis_stdout, "RFBF : total iteration %d\n", iteration); 03170 fprintf(vis_stdout, "%d image computations, %d constrain operations\n", 03171 Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration); 03172 fprintf(vis_stdout, 03173 "image computation time = %g, constrain operation time = %g\n", 03174 (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0); 03175 } 03176 03177 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 03178 constrainTarget == Fsm_Ardc_Constrain_Both_c) { 03179 for (i = 0; i < n; i++) { 03180 mdd_free(subFsm[i]->reachabilityInfo.initialStates); 03181 subFsm[i]->reachabilityInfo.initialStates = initial[i]; 03182 } 03183 FREE(initial); 03184 } 03185 03186 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) { 03187 for (i = 0; i < n; i++) { 03188 tmp = reached[i]; 03189 reached[i] = QuantifyVariables(reached[i], 03190 subFsm[i]->fsmData.pseudoInputBddVars, 03191 subFsm[i]->fsmData.pseudoInputCube); 03192 mdd_free(tmp); 03193 } 03194 } 03195 03196 /* sets the status of current overapproximate reached states */ 03197 if (converged) 03198 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c); 03199 else 03200 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c); 03201 03202 ComputeApproximateReachableStatesArray(mddManager, reachedArray, 03203 reached, NULL, n, decomposeFlag); 03204 if (decomposeFlag) { 03205 for (i = 0; i < n; i++) { 03206 mdd_free(constraint[i]); 03207 } 03208 } else { 03209 for (i = 0; i < n; i++) { 03210 mdd_free(reached[i]); 03211 mdd_free(constraint[i]); 03212 } 03213 } 03214 03215 FREE(reached); 03216 FREE(constraint); 03217 FREE(newConstraint); 03218 FREE(subFsm); 03219 FREE(newReached); 03220 array_free(toCareSetArray); 03221 03222 return(reachedArray); 03223 } 03224 03225 03242 static array_t * 03243 ArdcTfbfTraversal(Fsm_Fsm_t *fsm, int nvars, 03244 array_t *subFsmArray, array_t *fanInsIndexArray, 03245 mdd_t ***subReached, mdd_t ***subTo, 03246 int incrementalFlag, int verbosityLevel, 03247 int printStep, int depthValue, int shellFlag, 03248 int reorderFlag, int reorderThreshold, 03249 Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options) 03250 { 03251 mdd_manager *mddManager = NIL(mdd_manager); 03252 int i, j, n = array_n(subFsmArray); 03253 mdd_t **reached, **constraint, **newConstraint; 03254 mdd_t **to, **old_to; 03255 int converged = 0; 03256 Fsm_Fsm_t **subFsm; 03257 array_t *pi_to; 03258 mdd_t *tmp; 03259 array_t *fans; 03260 mdd_t *initialStates; 03261 int iteration = 0; 03262 mdd_t **initial = NIL(mdd_t *); 03263 array_t *reachedArray = array_alloc(mdd_t *, 0); 03264 array_t *faninConstrainArray; 03265 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); 03266 int dynStatus; 03267 bdd_reorder_type_t dynMethod; 03268 mdd_t *toCareSet; 03269 array_t *toCareSetArray = array_alloc(mdd_t *, 0); 03270 int depth = 0; 03271 boolean tmpReorderPtrFlag; 03272 long tImgComps = 0; 03273 long tConstrainOps = 0; 03274 long initialTime = 0, finalTime; 03275 int maxIteration = options->maxIteration; 03276 int constrainTarget = options->constrainTarget; 03277 boolean decomposeFlag = options->decomposeFlag; 03278 int abstractPseudoInput = options->abstractPseudoInput; 03279 Img_MinimizeType constrainMethod = options->constrainMethod; 03280 boolean projectedInitialFlag = options->projectedInitialFlag; 03281 int ardcVerbosity = options->verbosity; 03282 boolean constrainReorderFlag = options->constrainReorderFlag; 03283 boolean reorderPtrFlag = options->reorderPtrFlag; 03284 int faninConstrainMode = options->faninConstrainMode; 03285 03286 Img_ResetNumberOfImageComputation(Img_Forward_c); 03287 03288 reached = ALLOC(mdd_t *, n); 03289 constraint = ALLOC(mdd_t *, n); 03290 newConstraint = ALLOC(mdd_t *, n); 03291 subFsm = ALLOC(Fsm_Fsm_t *, n); 03292 pi_to = array_alloc(mdd_t *, 0); 03293 to = ALLOC(mdd_t *, n); 03294 array_insert_last(mdd_t **, pi_to, to); 03295 03296 mddManager = Fsm_FsmReadMddManager(fsm); 03297 for (i = 0; i < n; i++) { 03298 subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 03299 initialStates = Fsm_FsmComputeInitialStates(subFsm[i]); 03300 reached[i] = initialStates; 03301 constraint[i] = mdd_dup(initialStates); 03302 to[i] = mdd_zero(mddManager); 03303 03304 if (printStep && ((depth % printStep) == 0)) { 03305 if (ardcVerbosity > 1) 03306 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 03307 (void)fprintf(vis_stdout, 03308 "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth, 03309 mdd_count_onset(mddManager, reached[i], 03310 subFsm[i]->fsmData.presentStateVars), 03311 (long)mdd_size(reached[i])); 03312 } 03313 } 03314 03315 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 03316 constrainTarget == Fsm_Ardc_Constrain_Both_c) { 03317 initial = ALLOC(mdd_t *, n); 03318 for (i = 0; i < n; i++) 03319 initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]); 03320 } 03321 03322 converged = 0; 03323 do { 03324 depth++; 03325 to = ALLOC(mdd_t *, n); 03326 for (i = 0; i < n; i++) { 03327 if (ardcVerbosity > 1) 03328 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 03329 faninConstrainArray = array_alloc(mdd_t *, 0); 03330 fans = array_fetch(array_t *, fanInsIndexArray, i); 03331 ComputeFaninConstrainArray(faninConstrainArray, constraint, 03332 i, fans, decomposeFlag, faninConstrainMode); 03333 dynStatus = bdd_reordering_status(mddManager, &dynMethod); 03334 if (dynStatus != 0 && constrainReorderFlag == 0) 03335 bdd_dynamic_reordering_disable(mddManager); 03336 imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); 03337 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) { 03338 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 03339 if (ardcVerbosity > 2) 03340 Img_SetPrintMinimizeStatus(imageInfo, 2); 03341 else if (ardcVerbosity > 0) 03342 Img_SetPrintMinimizeStatus(imageInfo, 1); 03343 else 03344 Img_SetPrintMinimizeStatus(imageInfo, 0); 03345 if (reorderPtrFlag && 03346 abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03347 tmpReorderPtrFlag = 1; 03348 } else 03349 tmpReorderPtrFlag = 0; 03350 if (ardcVerbosity > 0) 03351 initialTime = util_cpu_time(); 03352 MinimizeTransitionRelationWithFaninConstraint(imageInfo, 03353 faninConstrainArray, constrainMethod, tmpReorderPtrFlag, 03354 TRUE); 03355 if (ardcVerbosity > 0) { 03356 finalTime = util_cpu_time(); 03357 tConstrainOps += finalTime - initialTime; 03358 } 03359 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 03360 } 03361 if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) { 03362 ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray, 03363 constrainMethod); 03364 } 03365 mdd_array_free(faninConstrainArray); 03366 if (dynStatus != 0 && constrainReorderFlag == 0) { 03367 bdd_dynamic_reordering(mddManager, dynMethod, 03368 BDD_REORDER_VERBOSITY_DEFAULT); 03369 } 03370 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03371 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 03372 if (ardcVerbosity > 2) 03373 Img_SetPrintMinimizeStatus(imageInfo, 2); 03374 else if (ardcVerbosity > 0) 03375 Img_SetPrintMinimizeStatus(imageInfo, 1); 03376 else 03377 Img_SetPrintMinimizeStatus(imageInfo, 0); 03378 Img_AbstractTransitionRelation(imageInfo, 03379 subFsm[i]->fsmData.pseudoInputBddVars, 03380 subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c); 03381 if (reorderPtrFlag) 03382 Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c); 03383 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 03384 } 03385 toCareSet = mdd_not(reached[i]); 03386 array_insert(mdd_t *, toCareSetArray, 0, toCareSet); 03387 if (ardcVerbosity > 0) 03388 initialTime = util_cpu_time(); 03389 to[i] = Fsm_ArdcComputeImage(subFsm[i], constraint[i], 03390 constraint[i], toCareSetArray); 03391 if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || 03392 Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { 03393 Img_TfmFlushCache(imageInfo, FALSE); 03394 } 03395 if (ardcVerbosity > 0) { 03396 finalTime = util_cpu_time(); 03397 tImgComps += finalTime - initialTime; 03398 } 03399 mdd_free(toCareSet); 03400 if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) 03401 Img_RestoreTransitionRelation(imageInfo, Img_Forward_c); 03402 03403 tmp = reached[i]; 03404 reached[i] = mdd_or(reached[i], to[i], 1, 1); 03405 mdd_free(tmp); 03406 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) { 03407 tmp = reached[i]; 03408 reached[i] = QuantifyVariables(reached[i], 03409 subFsm[i]->fsmData.pseudoInputBddVars, 03410 subFsm[i]->fsmData.pseudoInputCube); 03411 mdd_free(tmp); 03412 } 03413 newConstraint[i] = mdd_dup(to[i]); 03414 03415 if (printStep && ((depth % printStep) == 0)) { 03416 (void)fprintf(vis_stdout, 03417 "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", 03418 depth, mdd_count_onset(mddManager, reached[i], 03419 subFsm[i]->fsmData.presentStateVars), 03420 (long)mdd_size(reached[i])); 03421 } 03422 } 03423 for (i = 0; i < array_n(pi_to); i++) { 03424 old_to = array_fetch(mdd_t **, pi_to, i); 03425 for (j = 0; j < n; j++) { 03426 if (!mdd_equal(old_to[j], to[j])) 03427 break; 03428 } 03429 if (j == n) 03430 break; 03431 } 03432 if (i == array_n(pi_to)) 03433 converged = 0; 03434 else { 03435 converged = 1; 03436 if (ardcVerbosity > 0) { 03437 fprintf(vis_stdout, 03438 "** ardc info : TFBF converged at iteration %d(=%d).\n", 03439 iteration + 1, i); 03440 } 03441 } 03442 iteration++; 03443 if (ardcVerbosity > 0) { 03444 boolean supportCheckFlag = FALSE; 03445 03446 if (projectedInitialFlag || 03447 abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03448 supportCheckFlag = TRUE; 03449 } 03450 PrintCurrentReachedStates(mddManager, subFsm, reached, 03451 Fsm_Ardc_Traversal_Tfbf_c, 03452 n, iteration, nvars, ardcVerbosity, 03453 supportCheckFlag); 03454 } 03455 03456 /* update constraints */ 03457 for (i = 0; i < n; i++) { 03458 mdd_free(constraint[i]); 03459 constraint[i] = newConstraint[i]; 03460 newConstraint[i] = NIL(mdd_t); 03461 } 03462 03463 if (converged || iteration == maxIteration) { 03464 if (subTo) 03465 *subTo = to; 03466 else { 03467 for (i = 0; i < n; i++) 03468 mdd_free(to[i]); 03469 FREE(to); 03470 } 03471 break; 03472 } 03473 array_insert_last(mdd_t **, pi_to, to); 03474 } while (!converged); 03475 if (ardcVerbosity > 0) { 03476 fprintf(vis_stdout, "TFBF : total iteration %d\n", iteration); 03477 fprintf(vis_stdout, "%d image computations, %d constrain operations\n", 03478 Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration); 03479 fprintf(vis_stdout, 03480 "image computation time = %g, constrain operation time = %g\n", 03481 (double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0); 03482 } 03483 03484 if (constrainTarget == Fsm_Ardc_Constrain_Initial_c || 03485 constrainTarget == Fsm_Ardc_Constrain_Both_c) { 03486 for (i = 0; i < n; i++) { 03487 mdd_free(subFsm[i]->reachabilityInfo.initialStates); 03488 subFsm[i]->reachabilityInfo.initialStates = initial[i]; 03489 } 03490 FREE(initial); 03491 } 03492 03493 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) { 03494 for (i = 0; i < n; i++) { 03495 tmp = reached[i]; 03496 reached[i] = QuantifyVariables(reached[i], 03497 subFsm[i]->fsmData.pseudoInputBddVars, 03498 subFsm[i]->fsmData.pseudoInputCube); 03499 mdd_free(tmp); 03500 } 03501 } 03502 03503 /* sets the status of current overapproximate reached states */ 03504 if (converged) 03505 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c); 03506 else 03507 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c); 03508 03509 ComputeApproximateReachableStatesArray(mddManager, reachedArray, 03510 reached, subReached, n, decomposeFlag); 03511 if (decomposeFlag) { 03512 for (i = 0; i < n; i++) { 03513 mdd_free(constraint[i]); 03514 } 03515 } else { 03516 for (i = 0; i < n; i++) { 03517 if (subReached == NULL) 03518 mdd_free(reached[i]); 03519 mdd_free(constraint[i]); 03520 } 03521 } 03522 03523 if (subReached) 03524 *subReached = reached; 03525 else 03526 FREE(reached); 03527 FREE(constraint); 03528 FREE(newConstraint); 03529 FREE(subFsm); 03530 for (i = 0; i < array_n(pi_to); i++) { 03531 to = array_fetch(mdd_t **, pi_to, i); 03532 for (j = 0; j < n; j++) 03533 mdd_free(to[j]); 03534 FREE(to); 03535 } 03536 array_free(pi_to); 03537 array_free(toCareSetArray); 03538 03539 return(reachedArray); 03540 } 03541 03542 03559 static array_t * 03560 ArdcTmbmTraversal( 03561 Fsm_Fsm_t *fsm, 03562 int nvars, 03563 array_t *subFsmArray, 03564 array_t *fanInsIndexArray, 03565 array_t *fanOutsIndexArray, 03566 int incrementalFlag, 03567 int verbosityLevel, 03568 int printStep, 03569 int depthValue, 03570 int shellFlag, 03571 int reorderFlag, 03572 int reorderThreshold, 03573 Fsm_RchType_t approxFlag, 03574 Fsm_ArdcOptions_t *options, 03575 boolean lfpFlag) 03576 { 03577 mdd_manager *mddManager; 03578 int i, n = array_n(subFsmArray); 03579 mdd_t **reached, **tfbf_reached; 03580 mdd_t **to, **initial; 03581 Fsm_Fsm_t *subFsm = NIL(Fsm_Fsm_t); 03582 mdd_t *tmp; 03583 array_t *reachedArray; 03584 int saveMaxIteration; 03585 03586 saveMaxIteration = options->maxIteration; 03587 if (options->maxIteration == 0) 03588 options->maxIteration = 10; /* default */ 03589 03590 /* Try TFBF for the presecribed number of steps. */ 03591 reachedArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray, fanInsIndexArray, 03592 &tfbf_reached, &to, 03593 incrementalFlag, verbosityLevel, printStep, 03594 depthValue, shellFlag, reorderFlag, 03595 reorderThreshold, approxFlag, options); 03596 03597 /* If TFBF converged in the allotted number of iterations, clean up and 03598 * return. */ 03599 if (FsmReadReachabilityOverApproxComputationStatus(fsm) >= 03600 Fsm_Ardc_Converged_c) { 03601 for (i = 0; i < n; i++) { 03602 mdd_free(tfbf_reached[i]); 03603 mdd_free(to[i]); 03604 } 03605 FREE(tfbf_reached); 03606 FREE(to); 03607 return(reachedArray); 03608 } 03609 03610 mdd_array_free(reachedArray); 03611 03612 /* Save the initial states of each submachine in "initial"; thenset it 03613 * to the "to" states returned by TFBF. */ 03614 initial = ALLOC(mdd_t *, n); 03615 for (i = 0; i < n; i++) { 03616 subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 03617 initial[i] = subFsm->reachabilityInfo.initialStates; 03618 subFsm->reachabilityInfo.initialStates = mdd_dup(to[i]); 03619 } 03620 03621 /* Apply either MBM or LMBM starting from the "to" states returned by 03622 * TFBF. */ 03623 options->maxIteration = 0; 03624 reachedArray = ArdcMbmTraversal(fsm, nvars, subFsmArray, 03625 fanInsIndexArray, fanOutsIndexArray, &reached, 03626 incrementalFlag, verbosityLevel, printStep, 03627 depthValue, shellFlag, reorderFlag, reorderThreshold, 03628 approxFlag, options, lfpFlag); 03629 options->maxIteration = saveMaxIteration; 03630 03631 mdd_array_free(reachedArray); 03632 03633 /* Combine the reachability results of TFBF and (L)MBM and restore 03634 * the initial states of the submachines. */ 03635 for (i = 0; i < n; i++) { 03636 tmp = reached[i]; 03637 reached[i] = mdd_or(tfbf_reached[i], reached[i], 1, 1); 03638 mdd_free(tmp); 03639 subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 03640 mdd_free(subFsm->reachabilityInfo.initialStates); 03641 subFsm->reachabilityInfo.initialStates = initial[i]; 03642 } 03643 03644 /* Build the array of reachable states in either monolithic or decomposed 03645 * form depending on the value of decomposeFlag. */ 03646 reachedArray = array_alloc(mdd_t *, 0); 03647 mddManager = Fsm_FsmReadMddManager(subFsm); 03648 ComputeApproximateReachableStatesArray(mddManager, reachedArray, 03649 reached, NULL, n, 03650 options->decomposeFlag); 03651 if (!options->decomposeFlag) { 03652 for (i = 0; i < n; i++) 03653 mdd_free(reached[i]); 03654 } 03655 03656 /* Clean up. */ 03657 for (i = 0; i < n; i++) { 03658 mdd_free(tfbf_reached[i]); 03659 mdd_free(to[i]); 03660 } 03661 03662 FREE(reached); 03663 FREE(tfbf_reached); 03664 FREE(to); 03665 FREE(initial); 03666 03667 return(reachedArray); 03668 } 03669 03670 03684 static array_t * 03685 ArdcSimpleTraversal(Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, 03686 int incrementalFlag, int verbosityLevel, 03687 int printStep, int depthValue, int shellFlag, 03688 int reorderFlag, int reorderThreshold, 03689 Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, 03690 int setFlag) 03691 { 03692 mdd_manager *mddManager; 03693 int i, n = array_n(subFsmArray); 03694 mdd_t **reached; 03695 Fsm_Fsm_t **subFsm; 03696 mdd_t *tmp; 03697 array_t *reachedArray = array_alloc(mdd_t *, 0); 03698 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); 03699 boolean decomposeFlag = options->decomposeFlag; 03700 int abstractPseudoInput = options->abstractPseudoInput; 03701 boolean projectedInitialFlag = options->projectedInitialFlag; 03702 int ardcVerbosity = options->verbosity; 03703 03704 reached = ALLOC(mdd_t *, n); 03705 subFsm = ALLOC(Fsm_Fsm_t *, n); 03706 03707 for (i = 0; i < n; i++) 03708 subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 03709 03710 mddManager = Fsm_FsmReadMddManager(subFsm[0]); 03711 for (i = 0; i < n; i++) { 03712 if (printStep && ardcVerbosity > 1) 03713 fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i); 03714 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03715 int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo); 03716 if (ardcVerbosity > 2) 03717 Img_SetPrintMinimizeStatus(imageInfo, 2); 03718 else if (ardcVerbosity > 0) 03719 Img_SetPrintMinimizeStatus(imageInfo, 1); 03720 else 03721 Img_SetPrintMinimizeStatus(imageInfo, 0); 03722 imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); 03723 Img_AbstractTransitionRelation(imageInfo, 03724 subFsm[i]->fsmData.pseudoInputBddVars, 03725 subFsm[i]->fsmData.pseudoInputCube, 03726 Img_Forward_c); 03727 Img_SetPrintMinimizeStatus(imageInfo, saveStatus); 03728 } 03729 reached[i] = Fsm_FsmComputeReachableStates(subFsm[i], 03730 incrementalFlag, verbosityLevel, printStep, depthValue, 03731 shellFlag, reorderFlag, reorderThreshold, 03732 approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t)); 03733 if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c || 03734 Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) { 03735 Img_TfmFlushCache(imageInfo, FALSE); 03736 } 03737 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) { 03738 if (n > 1) { 03739 tmp = reached[i]; 03740 reached[i] = QuantifyVariables(reached[i], 03741 subFsm[i]->fsmData.pseudoInputBddVars, 03742 subFsm[i]->fsmData.pseudoInputCube); 03743 mdd_free(tmp); 03744 } 03745 } 03746 } 03747 03748 if (ardcVerbosity > 0) { 03749 boolean supportCheckFlag = FALSE; 03750 03751 if (projectedInitialFlag || 03752 abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) { 03753 supportCheckFlag = TRUE; 03754 } 03755 PrintCurrentReachedStates(mddManager, subFsm, reached, 03756 Fsm_Ardc_Traversal_Simple_c, 03757 n, 0, nvars, ardcVerbosity, 03758 supportCheckFlag); 03759 } 03760 03761 if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) { 03762 for (i = 0; i < n; i++) { 03763 tmp = reached[i]; 03764 reached[i] = QuantifyVariables(reached[i], 03765 subFsm[i]->fsmData.pseudoInputBddVars, 03766 subFsm[i]->fsmData.pseudoInputCube); 03767 mdd_free(tmp); 03768 } 03769 } 03770 03771 /* sets the status of current overapproximate reached states */ 03772 if (setFlag) 03773 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c); 03774 03775 ComputeApproximateReachableStatesArray(mddManager, reachedArray, 03776 reached, NULL, n, decomposeFlag); 03777 03778 FREE(reached); 03779 FREE(subFsm); 03780 03781 return(reachedArray); 03782 } 03783 03784 03798 static void 03799 ComputeFaninConstrainArray(array_t *faninConstrainArray, mdd_t **constraint, 03800 int current, array_t *fans, 03801 int decomposeFlag, int faninConstrainMode) 03802 { 03803 mdd_t *faninConstrain, *tmp; 03804 int i, fanin; 03805 03806 if (decomposeFlag) { 03807 if (faninConstrainMode == 1) { 03808 array_insert_last(mdd_t *, faninConstrainArray, 03809 mdd_dup(constraint[current])); 03810 } 03811 arrayForEachItem(int, fans, i, fanin) { 03812 array_insert_last(mdd_t *, faninConstrainArray, 03813 mdd_dup(constraint[fanin])); 03814 } 03815 } else { 03816 if (faninConstrainMode == 1) 03817 faninConstrain = mdd_dup(constraint[current]); 03818 else 03819 faninConstrain = NIL(mdd_t); 03820 arrayForEachItem(int, fans, i, fanin) { 03821 if (faninConstrain) { 03822 tmp = faninConstrain; 03823 faninConstrain = mdd_and(faninConstrain, constraint[fanin], 1, 1); 03824 mdd_free(tmp); 03825 } else 03826 faninConstrain = mdd_dup(constraint[fanin]); 03827 } 03828 array_insert_last(mdd_t *, faninConstrainArray, faninConstrain); 03829 } 03830 } 03831 03832 03844 static void 03845 MinimizeTransitionRelationWithFaninConstraint(Img_ImageInfo_t *imageInfo, 03846 array_t *faninConstrainArray, 03847 Img_MinimizeType constrainMethod, 03848 boolean reorderPtrFlag, 03849 boolean duplicate) 03850 { 03851 if (duplicate) { 03852 Img_DupTransitionRelation(imageInfo, Img_Forward_c); 03853 Img_ResetTrMinimizedFlag(imageInfo, Img_Forward_c); 03854 } 03855 Img_MinimizeTransitionRelation(imageInfo, faninConstrainArray, 03856 constrainMethod, Img_Forward_c, 03857 reorderPtrFlag); 03858 } 03859 03860 03873 static void 03874 ComputeConstrainedInitialStates(Fsm_Fsm_t *subFsm, 03875 array_t *faninConstrainArray, 03876 Img_MinimizeType constrainMethod) 03877 { 03878 int i; 03879 mdd_t *faninConstrain, *tmp, *constrainedInitial; 03880 03881 constrainedInitial = subFsm->reachabilityInfo.initialStates; 03882 for (i = 0; i < array_n(faninConstrainArray); i++) { 03883 faninConstrain = array_fetch(mdd_t *, faninConstrainArray, i); 03884 tmp = constrainedInitial; 03885 constrainedInitial = Img_MinimizeImage(constrainedInitial, 03886 faninConstrain, constrainMethod, 03887 TRUE); 03888 mdd_free(tmp); 03889 } 03890 subFsm->reachabilityInfo.initialStates = constrainedInitial; 03891 } 03892 03893 03905 static void 03906 ComputeApproximateReachableStatesArray(mdd_manager *mddManager, 03907 array_t *reachedArray, 03908 mdd_t **reached, 03909 mdd_t ***subReached, 03910 int nSubFsms, 03911 int decomposeFlag) 03912 { 03913 int i; 03914 03915 if (decomposeFlag) { 03916 for (i = 0; i < nSubFsms; i++) { 03917 if (subReached) 03918 array_insert_last(mdd_t *, reachedArray, mdd_dup(reached[i])); 03919 else 03920 array_insert_last(mdd_t *, reachedArray, reached[i]); 03921 } 03922 } else { 03923 mdd_t *reachedSet = mdd_one(mddManager); 03924 for (i = 0; i < nSubFsms; i++) { 03925 mdd_t *tmp = reachedSet; 03926 reachedSet = mdd_and(reachedSet, reached[i], 1, 1); 03927 mdd_free(tmp); 03928 } 03929 array_insert_last(mdd_t *, reachedArray, reachedSet); 03930 } 03931 } 03932 03933 03945 static array_t * 03946 ArdcCopyOverApproxReachableStatesFromExact(Fsm_Fsm_t *fsm) 03947 { 03948 array_t *reachableStatesArray; 03949 03950 if (Fsm_FsmReadReachableStates(fsm) == NIL(mdd_t)) 03951 return(NIL(array_t)); 03952 03953 reachableStatesArray = array_alloc(mdd_t *, 0); 03954 array_insert_last(mdd_t *, reachableStatesArray, 03955 mdd_dup(Fsm_FsmReadReachableStates(fsm))); 03956 FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Exact_c); 03957 fsm->reachabilityInfo.apprReachableStates = reachableStatesArray; 03958 fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0); 03959 array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, 03960 array_dup(fsm->fsmData.presentStateVars)); 03961 return(reachableStatesArray); 03962 } 03963 03964 03976 static void 03977 PrintCurrentReachedStates(mdd_manager *mddManager, Fsm_Fsm_t **subFsm, 03978 mdd_t **reached, Fsm_Ardc_TraversalType_t method, 03979 int nSubFsms, int iteration, int nvars, 03980 int ardcVerbosity, boolean supportCheckFlag) 03981 { 03982 int i; 03983 char string[24]; 03984 double tmpReached; 03985 03986 if (nvars <= EPD_MAX_BIN) { 03987 double numReached = 1.0, tmpReached; 03988 03989 for (i = 0; i < nSubFsms; i++) { 03990 tmpReached = mdd_count_onset(mddManager, reached[i], 03991 subFsm[i]->fsmData.presentStateVars); 03992 if (ardcVerbosity > 1) { 03993 if (ardcVerbosity > 2 && supportCheckFlag) { 03994 assert(mdd_check_support(mddManager, reached[i], 03995 subFsm[i]->fsmData.presentStateVars)); 03996 } 03997 fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n", 03998 i, tmpReached); 03999 } 04000 numReached *= tmpReached; 04001 } 04002 sprintf(string, "%g", numReached); 04003 } else { 04004 EpDouble epd; 04005 04006 EpdConvert((double)1.0, &epd); 04007 04008 for (i = 0; i < nSubFsms; i++) { 04009 tmpReached = mdd_count_onset(mddManager, reached[i], 04010 subFsm[i]->fsmData.presentStateVars); 04011 if (ardcVerbosity > 1) { 04012 if (ardcVerbosity > 2 && supportCheckFlag) { 04013 assert(mdd_check_support(mddManager, reached[i], 04014 subFsm[i]->fsmData.presentStateVars)); 04015 } 04016 fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n", 04017 i, tmpReached); 04018 } 04019 EpdMultiply(&epd, tmpReached); 04020 } 04021 EpdGetString(&epd, string); 04022 } 04023 04024 switch (method) { 04025 case Fsm_Ardc_Traversal_Mbm_c : 04026 fprintf(vis_stdout, "MBM : iteration %d, # of reached = %s\n", 04027 iteration, string); 04028 break; 04029 case Fsm_Ardc_Traversal_Rfbf_c : 04030 fprintf(vis_stdout, "RFBF : iteration %d, # of reached = %s\n", 04031 iteration, string); 04032 break; 04033 case Fsm_Ardc_Traversal_Tfbf_c : 04034 fprintf(vis_stdout, "TFBF : iteration %d, # of reached = %s\n", 04035 iteration, string); 04036 break; 04037 case Fsm_Ardc_Traversal_Tmbm_c : 04038 fprintf(vis_stdout, "TMBM : iteration %d, # of reached = %s\n", 04039 iteration, string); 04040 break; 04041 case Fsm_Ardc_Traversal_Lmbm_c : 04042 fprintf(vis_stdout, "LMBM : iteration %d, # of reached = %s\n", 04043 iteration, string); 04044 break; 04045 case Fsm_Ardc_Traversal_Tlmbm_c : 04046 fprintf(vis_stdout, "TLMBM : iteration %d, # of reached = %s\n", 04047 iteration, string); 04048 break; 04049 case Fsm_Ardc_Traversal_Simple_c : 04050 fprintf(vis_stdout, "SIMPLE : # of reached = %s\n", string); 04051 break; 04052 default : 04053 break; 04054 } 04055 } 04056 04057 04069 static void 04070 PrintBddWithName(Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node) 04071 { 04072 int i, j, size; 04073 mdd_manager *mddManager; 04074 array_t *mvarArray; 04075 mvar_type mv; 04076 int bddId, mddId, varLevel; 04077 bdd_t *varBdd; 04078 04079 if (!node) 04080 return; 04081 04082 mddManager = Fsm_FsmReadMddManager(fsm); 04083 if (!mddIdArr) 04084 mddIdArr = mdd_get_support(mddManager, node); 04085 mvarArray = mdd_ret_mvar_list(mddManager); 04086 04087 size = array_n(mddIdArr); 04088 for (i = 0; i < size; i++) { 04089 mddId = array_fetch(int, mddIdArr, i); 04090 mv = array_fetch(mvar_type, mvarArray, mddId); 04091 for (j = 0; j < mv.encode_length; j++) { 04092 bddId = mdd_ret_bvar_id(&mv, j); 04093 varBdd = bdd_get_variable(mddManager, bddId); 04094 varLevel = bdd_top_var_level(mddManager, varBdd); 04095 if (mv.encode_length == 1) 04096 fprintf(vis_stdout, "%s %d\n", mv.name, varLevel); 04097 else 04098 fprintf(vis_stdout, "%s[%d] %d\n", mv.name, j, varLevel); 04099 bdd_free(varBdd); 04100 } 04101 } 04102 bdd_print_minterm(node); 04103 } 04104 04105 04117 static void 04118 ArdcReadGroup(Ntk_Network_t *network, FILE *groupFile, 04119 array_t *latchNameArray, array_t *groupIndexArray) 04120 { 04121 char line[ARDC_MAX_LINE_LEN]; 04122 char *latchName, *name, *group; 04123 int groupIndex = 0; 04124 04125 while (fgets(line, ARDC_MAX_LINE_LEN, groupFile)) { 04126 if (strlen(line) == 0) 04127 continue; 04128 if (line[0] == '#') 04129 continue; 04130 if (line[strlen(line) - 1] == '\n') 04131 line[strlen(line) - 1] = '\0'; 04132 group = strtok(line, " "); 04133 if (strncmp(group, "GROUP[", 6) == 0) 04134 sscanf(group, "GROUP[%d]:", &groupIndex); 04135 else { 04136 latchName = util_strsav(group); 04137 array_insert_last(char *, latchNameArray, latchName); 04138 array_insert_last(int, groupIndexArray, groupIndex); 04139 } 04140 while ((name = strtok(NIL(char), " \t")) != NIL(char)) { 04141 latchName = util_strsav(name); 04142 array_insert_last(char *, latchNameArray, latchName); 04143 array_insert_last(int, groupIndexArray, groupIndex); 04144 } 04145 } 04146 } 04147 04148 04160 static void 04161 ArdcWriteOneGroup(Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i) 04162 { 04163 st_generator *stGen; 04164 st_table *vertexNameTable; 04165 char *latchName; 04166 04167 fprintf(groupFile, "GROUP[%d]:", i); 04168 vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem); 04169 st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) { 04170 fprintf(groupFile, " %s", latchName); 04171 } 04172 fprintf(groupFile, "\n"); 04173 } 04174 04175 04187 static void 04188 ArdcPrintOneGroup(Part_Subsystem_t *partitionSubsystem, int i, int nLatches, 04189 array_t *fanIns, array_t *fanOuts) 04190 { 04191 int j, k; 04192 st_generator *stGen; 04193 st_table *vertexNameTable; 04194 char *latchName; 04195 04196 fprintf(vis_stdout, "SUB-FSM [%d]\n", i); 04197 fprintf(vis_stdout, "== latches(%d) :", nLatches); 04198 vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem); 04199 st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) { 04200 fprintf(vis_stdout, " %s", latchName); 04201 } 04202 fprintf(vis_stdout, "\n"); 04203 fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns)); 04204 for (j = 0; j < array_n(fanIns); j++) { 04205 k = array_fetch(int, fanIns, j); 04206 fprintf(vis_stdout, " %d", k); 04207 } 04208 fprintf(vis_stdout, "\n"); 04209 fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts)); 04210 for (j = 0; j < array_n(fanOuts); j++) { 04211 k = array_fetch(int, fanOuts, j); 04212 fprintf(vis_stdout, " %d", k); 04213 } 04214 fprintf(vis_stdout, "\n"); 04215 } 04216 04217 04229 static int 04230 GetArdcSetIntValue(char *string, int l, int u, int defaultValue) 04231 { 04232 char *flagValue; 04233 int tmp; 04234 int value = defaultValue; 04235 04236 flagValue = Cmd_FlagReadByName(string); 04237 if (flagValue != NIL(char)) { 04238 sscanf(flagValue, "%d", &tmp); 04239 if (tmp >= l && (tmp <= u || u == 0)) 04240 value = tmp; 04241 else { 04242 fprintf(vis_stderr, 04243 "** ardc error : invalid value %d for %s[%d-%d]. **\n", tmp, string, 04244 l, u); 04245 } 04246 } 04247 04248 return(value); 04249 } 04250 04251 04263 static void 04264 ArdcEpdCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm, EpDouble *epd) 04265 { 04266 mdd_t *reached; 04267 array_t *psVars, *reachedArray; 04268 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 04269 double tmpReached; 04270 int i; 04271 04272 EpdMakeZero(epd, 0); 04273 04274 if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) 04275 return; 04276 04277 EpdConvert((double)1.0, epd); 04278 reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm); 04279 arrayForEachItem(mdd_t *, reachedArray, i, reached) { 04280 psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i); 04281 tmpReached = mdd_count_onset(mddManager, reached, psVars); 04282 EpdMultiply(epd, tmpReached); 04283 } 04284 } 04285 04286 04300 static mdd_t * 04301 QuantifyVariables(mdd_t *state, array_t *smoothArray, mdd_t *smoothCube) 04302 { 04303 if (smoothCube) 04304 return(bdd_smooth_with_cube(state, smoothCube)); 04305 else 04306 return(bdd_smooth(state, smoothArray)); 04307 } 04308 04309 04321 static void 04322 UpdateMbmEventSchedule(Fsm_Fsm_t **subFsm, array_t *fanOutIndices, 04323 int *traverse, int lfpFlag) 04324 { 04325 int i, fanout; 04326 04327 arrayForEachItem(int, fanOutIndices, i, fanout) { 04328 if (lfpFlag) { 04329 if (!subFsm[fanout]->reachabilityInfo.reachableStates || 04330 !bdd_is_tautology(subFsm[fanout]->reachabilityInfo.reachableStates, 04331 1)) { 04332 traverse[fanout] = 1; 04333 } 04334 } else 04335 traverse[fanout] = 1; 04336 } 04337 } 04338 04339 04351 static void 04352 PrintTfmStatistics(array_t *subFsmArray) 04353 { 04354 int i; 04355 Img_ImageInfo_t *imageInfo; 04356 Fsm_Fsm_t *subFsm; 04357 double tInserts, tLookups, tHits, tEntries; 04358 double inserts, lookups, hits, entries; 04359 int nSlots, tSlots, maxChainLength; 04360 float avgDepth, tAvgDepth, avgDecomp, tAvgDecomp; 04361 int tRecurs, tLeaves, tTurns, tDecomps, minDecomp; 04362 int nRecurs, nLeaves, nTurns; 04363 int nDecomps, topDecomp, maxDecomp, tMaxDecomp; 04364 int maxDepth, tMaxDepth; 04365 int flag, globalCache; 04366 04367 tInserts = tLookups = tHits = tEntries = 0.0; 04368 tSlots = 0; 04369 tRecurs = tLeaves = tTurns = tDecomps = 0; 04370 tAvgDepth = tAvgDecomp = 0.0; 04371 tMaxDecomp = tMaxDepth = 0; 04372 minDecomp = 10000000; /* arbitrarily large number */ 04373 04374 globalCache = Img_TfmCheckGlobalCache(0); 04375 if (globalCache) { 04376 flag = Img_TfmGetCacheStatistics(NIL(Img_ImageInfo_t), 0, &inserts, 04377 &lookups, &hits, &entries, &nSlots, 04378 &maxChainLength); 04379 tInserts = inserts; 04380 tLookups = lookups; 04381 tHits = hits; 04382 tEntries = entries; 04383 tSlots = nSlots; 04384 } 04385 04386 for (i = 0; i < array_n(subFsmArray); i++) { 04387 subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i); 04388 imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm, 0, 1); 04389 04390 if (!globalCache) { 04391 flag = Img_TfmGetCacheStatistics(imageInfo, 0, &inserts, &lookups, &hits, 04392 &entries, &nSlots, &maxChainLength); 04393 if (flag) { 04394 tInserts += inserts; 04395 tLookups += lookups; 04396 tHits += hits; 04397 tEntries += entries; 04398 tSlots += nSlots; 04399 } 04400 } 04401 04402 flag = Img_TfmGetRecursionStatistics(imageInfo, 0, &nRecurs, &nLeaves, 04403 &nTurns, &avgDepth, &maxDepth, &nDecomps, 04404 &topDecomp, &maxDecomp, &avgDecomp); 04405 if (flag) { 04406 tAvgDepth = (tAvgDepth * (float)tLeaves + avgDepth * (float)nLeaves) / 04407 (float)(tLeaves + nLeaves); 04408 tRecurs += nRecurs; 04409 tLeaves += nLeaves; 04410 tTurns += nTurns; 04411 tAvgDecomp = (tAvgDecomp * (float)tDecomps + 04412 avgDecomp * (float)nDecomps) / (float)(tDecomps + nDecomps); 04413 tDecomps += nDecomps; 04414 if (topDecomp < minDecomp) 04415 minDecomp = topDecomp; 04416 if (maxDecomp > tMaxDecomp) 04417 tMaxDecomp = maxDecomp; 04418 if (maxDepth > tMaxDepth) 04419 tMaxDepth = maxDepth; 04420 } 04421 } 04422 04423 if (tInserts != 0.0) { 04424 if (globalCache) { 04425 fprintf(vis_stdout, 04426 "** global cache statistics of transition function **\n"); 04427 } else 04428 fprintf(vis_stdout, "** cache statistics of transition function **\n"); 04429 fprintf(vis_stdout, "# insertions = %g\n", tInserts); 04430 fprintf(vis_stdout, "# lookups = %g\n", tLookups); 04431 fprintf(vis_stdout, "# hits = %g (%.2f%%)\n", tHits, 04432 tHits / tLookups * 100.0); 04433 fprintf(vis_stdout, "# misses = %g (%.2f%%)\n", tLookups - tHits, 04434 (tLookups - tHits) / tLookups * 100.0); 04435 fprintf(vis_stdout, "# entries = %g\n", tEntries); 04436 if (tSlots > 0) { 04437 fprintf(vis_stdout, "# slots = %d\n", tSlots); 04438 fprintf(vis_stdout, "maxChainLength = %d\n", maxChainLength); 04439 } 04440 } 04441 04442 if (tRecurs != 0) { 04443 fprintf(vis_stdout, "** recursion statistics of transition function **\n"); 04444 fprintf(vis_stdout, "# recursions = %d\n", tRecurs); 04445 fprintf(vis_stdout, "# leaves = %d\n", tLeaves); 04446 fprintf(vis_stdout, "# turns = %d\n", tTurns); 04447 fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n", 04448 tAvgDepth, tMaxDepth); 04449 fprintf(vis_stdout, 04450 "# decompositions = %d (top = %d, max = %d, average = %g)\n", 04451 tDecomps, minDecomp, tMaxDecomp, tAvgDecomp); 04452 } 04453 }
1.7.3