/**CFile*********************************************************************** FileName [amcBlock.c] PackageName [amc] Synopsis [Implementation of the block-tearing abstraction.] Author [Woohyuk Lee] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "amcInt.h" #include "mcInt.h" static char rcsid[] UNUSED = "$Id: amcBlock.c,v 1.35 2005/04/25 20:24:53 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Block tearing specific information.] Description [] ******************************************************************************/ struct BlockInfoStruct { Amc_SubsystemInfo_t *optimalSystem; /* temporary storage for Block method */ int bestSystem; /* temporary storage for Block method */ }; struct BlockSubsystemInfoStruct { int scheduledForRefinement; }; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct BlockInfoStruct BlockInfo_t; typedef struct BlockSubsystemInfoStruct BlockSubsystemInfo_t; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static BlockInfo_t * AmcObtainOptimalSystemUpperBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity); static BlockInfo_t * AmcObtainOptimalSystemLowerBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity); static void AmcInitializeDependency(array_t *subSystemArray, int isMBM); static void AmcInitializeSchedule(Amc_Info_t *amcInfo); static int AmcIsEverySubsystemRescheduled(Amc_Info_t *amcInfo); static void AmcPrintScheduleInformation(Amc_Info_t *amcInfo); #if 0 static void AmcRescheduleForRefinement(st_table *fanOutSystemTable); static mdd_t * AmcRefineWithSatisfyStatesOfFanInSystem(Amc_SubsystemInfo_t *subSystem, mdd_t *careStates); #endif static array_t * AmcInitializeQuantifyVars(Amc_SubsystemInfo_t *subSystem); #if 0 static void AmcFreeBlockInfo(BlockInfo_t *BlockInfo); #endif static int AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystemInfo_t *system); static void AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystemInfo_t *system, int data); #if 0 static Amc_SubsystemInfo_t * AmcBlockReadOptimalSubsystem(BlockInfo_t *system); #endif static void AmcBlockSetOptimalSystem(BlockInfo_t *system, Amc_SubsystemInfo_t *data); #if 0 static int AmcBlockReadBestSystem(BlockInfo_t *system); #endif static void AmcBlockSetBestSystem(BlockInfo_t *system, int data); #if 0 static Amc_SubsystemInfo_t * AmcClearInputVarsFromFSM(Amc_SubsystemInfo_t *subSystem); #endif /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [A block-tearing procedure.] Description [From an array of subsystems, the routine picks a subsystem that produces best result. When proving true positive, a subsystem that produces smallest cardinality of the error state is chosen as the best subsystem. Error states are defined as; (Initial States) - (Subset of states satisfying given formula). An over-approximation of the transition relation produces a subset of states satisfying the original ACTL formula. Whenever the subset of states satisfying given formula contains the initial states, we conclude that the system models the specification. The routine treats initial states as a monotonically decreasing(cardinality wise) set. This is because when we identify the set of subsets of states satisfying given ACTL formula cover the initial states, we can conclude that the initial states are entirely contained in the exact set of states satisfying given ACTL formula. Hence, once we identify an error states, the routine updates the error states as new initial states. When proving true negative of given ACTL formula, the best subsystem is that produces smallest cardinality of the superset of states satisfying ACTL formula in consideration. An under-approximation of the transition relation of the original system produces a superset of states satisfying the ACTL formulas. Whenever we find an initial state(s) that are not contained in the superset of states satisfying given ACTL formula, we conclude that the system does not model the specification. An initial state(s) that is not contained in the superset of states satisfying an ACTL formula is used to produce a debug trace. When "machine by machine" switch is ON, refinement of either subsets or the supersets of states satisfying given formula is performed. This process is done until the refinements cannot be made. (Note; "machine by machine" refinement is not yet supported. 2/12/97) ] SideEffects [] ******************************************************************************/ int AmcBlockTearingProc( Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, int verbosity) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem; BlockInfo_t BlockInfo; /* * Update fan-in subsystems and fan-out subsystems when machine by machine * method is ON. * Update initial states in BlockInfo. * Reschedule every subsystem to be evaluated. */ if( amcInfo->optimalSystem == NIL(Amc_SubsystemInfo_t) ) { AmcInitializeDependency(subSystemArray, amcInfo->isMBM); } AmcInitializeSchedule(amcInfo); /* BlockInfo is a temporary storage. optimal system is not freed */ BlockInfo.optimalSystem = NIL(Amc_SubsystemInfo_t); /* * Outer loop until there's no scheduled subsystem. */ while(AmcIsEverySubsystemRescheduled(amcInfo)) { if(verbosity == Amc_VerbosityNone_c) AmcPrintScheduleInformation(amcInfo); if( !amcInfo->lowerBound ) { AmcObtainOptimalSystemUpperBound(amcInfo, formula, &BlockInfo, verbosity); /* AmcObtainOptimalSystemUpperBoundWithDI(amcInfo, formula, &BlockInfo, verbosity); */ } else { AmcObtainOptimalSystemLowerBound(amcInfo, formula, &BlockInfo, verbosity); /* AmcObtainOptimalSystemLowerBoundWithMBM(amcInfo, formula, &BlockInfo, verbosity); */ } if(amcInfo->isVerified) { int best = BlockInfo.bestSystem; subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, best); subSystem->takenIntoOptimal = 1; return 1; } if(!amcInfo->isMBM) break; } /* End of while() */ if(verbosity == Amc_VerbosityNone_c) AmcPrintScheduleInformation(amcInfo); /* Update the subsystem that had been included in optimal system */ { int best = BlockInfo.bestSystem; subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, best); subSystem->takenIntoOptimal = 1; } /* Update amcInfo's optimal system */ if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) { #ifdef AMC_DEBUG { Amc_SubsystemInfo_t *previousOpt = amcInfo->optimalSystem; Amc_SubsystemInfo_t *currentOpt = BlockInfo.optimalSystem; if(!amcInfo->lowerBound) { if(mdd_lequal(previousOpt->satisfyStates, currentOpt->satisfyStates, 1, 1)) { fprintf(vis_stdout, "\n###AMC : We are ok."); } else { fprintf(vis_stdout, "\n** amc error: Somethings wrong."); } } else { if( mdd_lequal(currentOpt->satisfyStates, previousOpt->satisfyStates, 1, 1)) { fprintf(vis_stdout, "\n###AMC : We are ok."); } else { fprintf(vis_stdout, "\n** amc error: Somethings wrong."); } } } #endif Amc_AmcSubsystemFree(amcInfo->optimalSystem); } AmcSetOptimalSystem(amcInfo, BlockInfo.optimalSystem); return 1; } /**Function******************************************************************** Synopsis [Frees block-tearing specific data structure.] SideEffects [] ******************************************************************************/ void AmcFreeBlock( Amc_Info_t *amcInfo) { Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; int i ; /* what if amc doesn't free partition */ arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, subSystem) { BlockSubsystem = (BlockSubsystemInfo_t *)AmcSubsystemReadMethodSpecificData(subSystem); if(BlockSubsystem != NIL(BlockSubsystemInfo_t)) FREE(BlockSubsystem); Amc_AmcSubsystemFree(subSystem); } array_free(amcInfo->subSystemArray); if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(amcInfo->optimalSystem); amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t); } if( amcInfo->initialStates != NIL(mdd_t)) { mdd_free(amcInfo->initialStates); amcInfo->initialStates = NIL(mdd_t); } FREE(amcInfo); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Obtain best subsystem that has not taken into the optimal system.] Description [The routine is used to prove true positive of given ACTL formula. An over-approximation of transition relation is used. Over-approximation of the transition relation is obtained by simply replacing the subsystems not in consideration into tautology. We are adding more behavior into the system by preserving only the subset of subsystems(subFSMs). We call this procedure a block-tearing abstraction. We do not abstract initial states in any sense. The best subsystem is chosen from those subsystems that has not yet been taken into the optimal system. A subsystem that produces best result is determined by the smallest error states. An error states are defined as; Error States = (Initial States) - (Subset of states satisfying given ACTL formula) For each subsystem, a subset of states satisfying given ACTL formula is computed by using an over-approximation of the transition relation obtained from the subsystem. The routine picks a subsystem whose corresponding error states are cardinality wise minimal. The optimal system is the collection of subsystems that were chosen as the best subsystem in each iteration. A function call to this routine is regarded as a single iteration when "machine by machine" refinement is turned OFF. These subsystems are synchronously combined to form a optimal system. Once the best subsystem is chosen(from the set of subsystems that has not been combined into the optimal system), an initial states are updated with an error states. An error states are defined as; (Initial States) - (Subset of states satisfying given ACTL formula) A more aggressive update of initial states may also be performed. If we denote a subset of states satisfying given ACTL formula as Sat^L(\phi). New Initial States = (Old Initial States) - \Sigma_{i}(Sat^L_i(\phi) The routine currently does not attempt above aggressive approach. The routine update initial state as; New Initial States = (Old Initial States) - Sat^L_{Best i}(\phi). ] SideEffects [] ******************************************************************************/ static BlockInfo_t * AmcObtainOptimalSystemUpperBound( Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem, *bestCombinedSystem; mdd_t *initialStates; mdd_t *smallestStates, *currentErrorStates, *careStates; int i, best = 0; graph_t *partition = Part_NetworkReadPartition(amcInfo->network); mdd_manager *mddManager = Part_PartitionReadMddManager(partition); mdd_t *mddOne = mdd_one(mddManager); array_t *quantifyVars; Mc_DcLevel dcLevel; char *flagValue; /* * Initial states must be set before coming into this routine. */ initialStates = amcInfo->initialStates; if( initialStates == NIL(mdd_t) ) { (void)fprintf(vis_stderr, "** amc error: \n"); return(NIL(BlockInfo_t)); } /* Read in the usage of don't care level */ flagValue = Cmd_FlagReadByName("amc_DC_level"); if(flagValue != NIL(char)){ dcLevel = (Mc_DcLevel) atoi(flagValue); if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c; } else{ /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */ dcLevel = McDcLevelNone_c; } /* * Update the set of states satisfying the formula for each sub-systems. * The process of "combining sub-systems" is equivalent of taking a * "synchronous product" of multiple sub-subsystems. */ smallestStates = NIL(mdd_t); bestCombinedSystem = NIL(Amc_SubsystemInfo_t); arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { mdd_t *reachableStates, *fairStates, *satisfyStates; Fsm_Fsm_t *combinedFsm; Fsm_Fairness_t *fairCond; Amc_SubsystemInfo_t *combinedSystem; /* Proceed if the subsystem had not yet been taken into the optimal system. */ if(!subSystem->takenIntoOptimal) { /* * Combine subsystems. If optimal subsystem is NIL, duplicate the * subsystem. */ combinedSystem = Amc_CombineSubsystems(amcInfo->network, amcInfo->optimalSystem, subSystem); combinedFsm = AmcSubsystemReadFsm(combinedSystem); quantifyVars = AmcInitializeQuantifyVars(combinedSystem); /* * Currently forced not to compute reachable states. This is to reduce * computational overhead of computing it when dealing with complex * examples. */ reachableStates = mdd_one(mddManager); fairStates = mdd_one(mddManager); fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm); /* Obtain new care set from fan-in systems */ careStates = mdd_dup(reachableStates); Ctlp_FlushStates(formula); satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem, subSystemArray, formula, fairStates, fairCond, careStates, amcInfo->lowerBound, quantifyVars, /*NIL(array_t),*/ (Mc_VerbosityLevel) verbosity, dcLevel)); { int x; array_t *quantifyStateVars; arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) { array_free(quantifyStateVars); } array_free(quantifyVars); } /* Free */ mdd_free(careStates); mdd_free(reachableStates); mdd_free(fairStates); /* * Update the set of states satisfying the formula for each subsystems * when newly computed states are tighter than the one already stored. * Notice, "satisfySates" holds the set of states satisfying the formula * computed with the combined_system(optimal_system || current_subsystem). * */ if( subSystem->satisfyStates != NIL(mdd_t) ) { if( !(mdd_equal(subSystem->satisfyStates, satisfyStates )) && (mdd_lequal(subSystem->satisfyStates, satisfyStates, 1, 1)) ) { /* We got a tighter approximation. */ mdd_free(subSystem->satisfyStates); AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates)); } } else { /* We are in the first level of the lattice */ AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates)); } /* Update the set of states satisfying the formula for the combined_system. */ if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) ) mdd_free( AmcSubsystemReadSatisfy(combinedSystem) ); AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates)); if( verbosity == Amc_VerbosityVomit_c) { mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm); array_t *psVars = Fsm_FsmReadPresentStateVars(combinedSystem->fsm); fprintf(vis_stdout, "\n#AMC STATUS: The states satisfying the formula : %10g", mdd_count_onset( mddMgr, combinedSystem->satisfyStates, psVars ) ); fflush(vis_stdout); } /* * Check whether the formula evaluates to TRUE. */ { mdd_t *notSatisfyStates = mdd_not(satisfyStates); currentErrorStates = mdd_and(initialStates, notSatisfyStates, 1, 1); mdd_free(notSatisfyStates); mdd_free(satisfyStates); } if ( mdd_is_tautology(currentErrorStates, 0) ) { /* The formula is verified TRUE!! */ AmcBlockSetBestSystem(BlockInfo, i); amcInfo->isVerified = 1; amcInfo->amcAnswer = Amc_Verified_True_c; fprintf(vis_stdout, "\n# AMC: formula passed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula)); if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates); if(smallestStates != NIL(mdd_t)) mdd_free(smallestStates); if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) ) Amc_AmcSubsystemFree(bestCombinedSystem); mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); Ctlp_FlushStates(formula); return BlockInfo; } /* end of if */ else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){ /* The formula is verified FALSE!! */ array_t *careStatesArray; AmcBlockSetBestSystem(BlockInfo, i); amcInfo->isVerified = 1; amcInfo->amcAnswer = Amc_Verified_False_c; fprintf(vis_stdout, "\n# AMC: formula failed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula)); if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates); if(smallestStates != NIL(mdd_t)) mdd_free(smallestStates); if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) ) Amc_AmcSubsystemFree(bestCombinedSystem); { /* Temporarily stay here until the damn thing becomes visible. */ McOptions_t *mcOptions = ALLOC(McOptions_t, 1); mcOptions->useMore = FALSE; mcOptions->fwdBwd = McFwd_c; mcOptions->reduceFsm = FALSE; mcOptions->printInputs = FALSE; mcOptions->simFormat = FALSE; mcOptions->verbosityLevel = McVerbosityNone_c; mcOptions->dbgLevel = McDbgLevelMin_c; mcOptions->dcLevel = McDcLevelNone_c; mcOptions->ctlFile = NIL(FILE); mcOptions->debugFile = NIL(FILE); careStatesArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, careStatesArray, 0, mddOne); fprintf(vis_stdout, "\n"); McFsmDebugFormula((McOptions_t *)mcOptions, formula, combinedSystem->fsm, careStatesArray); array_free(careStatesArray); FREE(mcOptions); } mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); Ctlp_FlushStates(formula); return BlockInfo; } /* * Get the locally optimal subsystem by choosing a subsystem that produces * smallest error states. */ if( smallestStates == NIL(mdd_t) || mdd_count_onset(mddManager, currentErrorStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <= mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) { if( smallestStates != NIL(mdd_t) ) mdd_free(smallestStates); smallestStates = currentErrorStates; if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(bestCombinedSystem); bestCombinedSystem = NIL(Amc_SubsystemInfo_t); } bestCombinedSystem = combinedSystem; best = i; } else { /* Free combined system, current error states */ Amc_AmcSubsystemFree(combinedSystem); combinedSystem = NIL(Amc_SubsystemInfo_t); mdd_free(currentErrorStates); } } /* end of if(!takenIntoOptimal) */ } /* end of arrayForEachItem(subSystemArray) */ /* * Flush the formula that was kept in last iteration. * Update Block Info. */ Ctlp_FlushStates(formula); /* Update the inital states */ { mdd_t *initialStates; if((initialStates = AmcReadInitialStates(amcInfo)) != NIL(mdd_t)) mdd_free(initialStates); AmcSetInitialStates(amcInfo, smallestStates); } if( verbosity == Amc_VerbositySpit_c ) { mdd_manager *mddMgr = Fsm_FsmReadMddManager(bestCombinedSystem->fsm); array_t *psVars = Fsm_FsmReadPresentStateVars(bestCombinedSystem->fsm); fprintf(vis_stdout, "\n#AMC : The BDD size of the states satisfying the formula : %d", mdd_size(bestCombinedSystem->satisfyStates) ); fprintf(vis_stdout, "\n#AMC : The cardinality of the states satisfying the formula : %10g ", mdd_count_onset( mddMgr, bestCombinedSystem->satisfyStates, psVars ) ); fprintf(vis_stdout, "\n#AMC : The BDD size of the states new initial states : %d", mdd_size(smallestStates) ); fprintf(vis_stdout, "\n#AMC : The cardinality of the new initial states : %10g ", mdd_count_onset( mddMgr, smallestStates, psVars ) ); } /* * Update the optimal system BlockInfo->optimalSystem. BlockInfo is a temporary * storage that survive through single level of the lattice. */ if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(BlockInfo->optimalSystem); AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t)); } AmcSetOptimalSystem(BlockInfo, bestCombinedSystem); /* Set the best system. */ AmcBlockSetBestSystem(BlockInfo, best); mdd_free(mddOne); return BlockInfo; } /**Function******************************************************************** Synopsis [Obtain best subsystem that has not taken into the optimal system.] Description [The routine is to choose a subsystem that produces a best result when proving true negative of the formula. An under-approximation of the transition is used to obtain a superset of states satisfying given formula. The best subsystem is a subsystem that produces a smallest cardinality of a superset of states satisfying given ACTL formula.] SideEffects [] ******************************************************************************/ static BlockInfo_t * AmcObtainOptimalSystemLowerBound( Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem, *bestCombinedSystem; mdd_t *initialStates; mdd_t *smallestStates, *currentErrorStates, *careStates; int i, best = 0; graph_t *partition = Part_NetworkReadPartition(amcInfo->network); mdd_manager *mddManager = Part_PartitionReadMddManager(partition); mdd_t *mddOne = mdd_one(mddManager); array_t *quantifyVars; Mc_DcLevel dcLevel; char *flagValue; /* * Initial states must be set before coming into this routine. */ initialStates = amcInfo->initialStates; if( initialStates == NIL(mdd_t) ) { (void)fprintf(vis_stderr, "** amc error: \n"); return(NIL(BlockInfo_t)); } /* Read in the usage of don't care level. Do not want to pass parameters. */ flagValue = Cmd_FlagReadByName("amc_DC_level"); if(flagValue != NIL(char)){ dcLevel = (Mc_DcLevel) atoi(flagValue); if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c; } else{ /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */ dcLevel = McDcLevelNone_c; } /* * Update the set of states satisfying the formula for each subsystem. * The process of "combining sub-systems" is equivalent of taking a * "synchronous product" of multiple subsystems. */ smallestStates = NIL(mdd_t); bestCombinedSystem = NIL(Amc_SubsystemInfo_t); arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { mdd_t *reachableStates, *fairStates, *satisfyStates; Fsm_Fsm_t *combinedFsm; Fsm_Fairness_t *fairCond; Amc_SubsystemInfo_t *combinedSystem; /* Proceed if the subsystem has not yet been taken into the optimal system. */ if(!subSystem->takenIntoOptimal) { /* * Combine subsystems. If optimal subsystem is NIL, duplicate the * subsystem. */ combinedSystem = Amc_CombineSubsystems(amcInfo->network, amcInfo->optimalSystem, subSystem); /* Remove input variables from the FSM */ /* combinedSystem = AmcClearInputVarsFromFSM(combinedSystem);*/ combinedFsm = AmcSubsystemReadFsm(combinedSystem); /* * Use takenIntoOptimal field for the purpose of excluding current block * when universally quantifying variables from transition relation. * Obtain lower bound of transition relation by universal quantification. */ quantifyVars = AmcInitializeQuantifyVars(combinedSystem); combinedSystem->takenIntoOptimal = i; /* * Currently forced not to compute reachable states. This is to reduce * computational burden of computing it when dealing with complex * examples. */ reachableStates = mdd_one(mddManager); fairStates = mdd_one(mddManager); fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm); careStates = mdd_dup(reachableStates); Ctlp_FlushStates(formula); satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem, subSystemArray, formula, fairStates, fairCond, careStates, amcInfo->lowerBound, quantifyVars, (Mc_VerbosityLevel) verbosity, dcLevel)); { int x; array_t *quantifyStateVars; arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) { array_free(quantifyStateVars); } array_free(quantifyVars); } mdd_free(careStates); mdd_free(reachableStates); mdd_free(fairStates); /* */ if( subSystem->satisfyStates != NIL(mdd_t) ) { if( !(mdd_equal(satisfyStates, subSystem->satisfyStates )) && (mdd_lequal(satisfyStates, subSystem->satisfyStates, 1, 1)) ) { /* We got a tighter approximation. */ mdd_free(subSystem->satisfyStates); AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates)); } } /* end of if( subSystem->satisfyStates != NIL(mdd_t) ) */ else { /* Update subsystem when we are in level 1 of the lattice */ AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates)); } if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) ) mdd_free( AmcSubsystemReadSatisfy(combinedSystem) ); AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates)); /* Test if the formula is verified */ { mdd_t *notSatisfyStates = mdd_not(satisfyStates); currentErrorStates = mdd_and(initialStates, notSatisfyStates, 1, 1); mdd_free(notSatisfyStates); mdd_free(satisfyStates); } if( verbosity == Amc_VerbosityVomit_c) { mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm); array_t *psVars = Fsm_FsmReadPresentStateVars(combinedSystem->fsm); fprintf(vis_stdout, "\n#AMC STATUS: The states satisfying the formula : %10g", mdd_count_onset(mddMgr, combinedSystem->satisfyStates, psVars ) ); fflush(vis_stdout); } if ( !mdd_is_tautology(currentErrorStates, 0) ) { array_t *careStatesArray; /* Verified the formula FALSE!! */ AmcBlockSetBestSystem(BlockInfo, i); amcInfo->isVerified = 1; amcInfo->amcAnswer = Amc_Verified_False_c; fprintf(vis_stdout, "\n# AMC: formula failed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula)); if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates); if(smallestStates != NIL(mdd_t)) mdd_free(smallestStates); if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) ) Amc_AmcSubsystemFree(bestCombinedSystem); { /* Temporarily stay here until the damn thing becomes visible. */ McOptions_t *mcOptions = ALLOC(McOptions_t, 1); mcOptions->useMore = FALSE; mcOptions->fwdBwd = McFwd_c; mcOptions->reduceFsm = FALSE; mcOptions->printInputs = FALSE; mcOptions->simFormat = FALSE; mcOptions->verbosityLevel = McVerbosityNone_c; mcOptions->dbgLevel = McDbgLevelMinVerbose_c; mcOptions->dcLevel = McDcLevelNone_c; mcOptions->ctlFile = NIL(FILE); mcOptions->debugFile = NIL(FILE); careStatesArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, careStatesArray, 0, mddOne); fprintf(vis_stdout, "\n"); McFsmDebugFormula((McOptions_t *)mcOptions, formula, combinedSystem->fsm, careStatesArray); array_free(careStatesArray); FREE(mcOptions); } mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); Ctlp_FlushStates(formula); return BlockInfo; }else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){ /* The formula is verified true!! */ AmcBlockSetBestSystem(BlockInfo, i); amcInfo->isVerified = 1; amcInfo->amcAnswer = Amc_Verified_True_c; fprintf(vis_stdout, "\n# AMC: formula passed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula)); if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates); if(smallestStates != NIL(mdd_t)) mdd_free(smallestStates); if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) ) Amc_AmcSubsystemFree(bestCombinedSystem); mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); Ctlp_FlushStates(formula); return BlockInfo; } mdd_free(currentErrorStates); /* * Choose a subsystem that produces smallest satisfying states. */ if( smallestStates == NIL(mdd_t) || mdd_count_onset(mddManager, subSystem->satisfyStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <= mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) { /* * Found locally optimal subsystem. * Free smallest-error-state, best combined system so far. * Update smallest-error-states and best combined system. */ if( smallestStates != NIL(mdd_t) ) mdd_free(smallestStates); smallestStates = mdd_dup(subSystem->satisfyStates); if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(bestCombinedSystem); bestCombinedSystem = NIL(Amc_SubsystemInfo_t); } bestCombinedSystem = combinedSystem; best = i; } else { /* Free combined system, current error states */ Amc_AmcSubsystemFree(combinedSystem); combinedSystem = NIL(Amc_SubsystemInfo_t); } } /* end of if(!takenIntoOptimal) */ } /* end of arrayForEachItem(subSystemArray) */ mdd_free(smallestStates); /* * Flush formula that was kept in last iteration. Update Block Info. */ Ctlp_FlushStates(formula); /* * Update optimal system BlockInfo->optimalSystem. BlockInfo is a temporary * storage that survive through single level of the lattice. */ if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(BlockInfo->optimalSystem); AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t)); } AmcSetOptimalSystem(BlockInfo, bestCombinedSystem); /* Set best system. */ AmcBlockSetBestSystem(BlockInfo, best); mdd_free(mddOne); return BlockInfo; } /**Function******************************************************************** Synopsis [Initialize dependencies between subsystems.] SideEffects [] ******************************************************************************/ static void AmcInitializeDependency( array_t *subSystemArray, int isMBM) { Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; int i; if(!isMBM) { int i; arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { AmcSubsystemSetMethodSpecificData(subSystem, NIL(BlockSubsystemInfo_t)); } return; } arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { BlockSubsystem = ALLOC(BlockSubsystemInfo_t, 1); AmcSubsystemSetMethodSpecificData(subSystem, BlockSubsystem); } } /**Function******************************************************************** Synopsis [Initialize scheduling information.] SideEffects [] ******************************************************************************/ static void AmcInitializeSchedule( Amc_Info_t *amcInfo) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; int i; /* If MBM flag is not set just return */ if(!amcInfo->isMBM) return; arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem); if(!subSystem->takenIntoOptimal) AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1); } } /**Function******************************************************************** Synopsis [Test whether there is any subsystems to be reevaluated.] SideEffects [] ******************************************************************************/ static int AmcIsEverySubsystemRescheduled( Amc_Info_t *amcInfo) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; int i; /* If MBM flag is not set just return */ if( !amcInfo->isMBM ) return 1; arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem); if( AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) ) return 1; } return 0; } /**Function******************************************************************** Synopsis [Print schedule information.] SideEffects [] ******************************************************************************/ static void AmcPrintScheduleInformation( Amc_Info_t *amcInfo) { array_t *subSystemArray = amcInfo->subSystemArray; Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; int i; /* If MBM flag is not set just return */ if(!amcInfo->isMBM) return; fprintf(vis_stdout, "\nSchedule information : "); arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) { BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem); fprintf(vis_stdout, " %d ", AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) ); } } #if 0 /**Function******************************************************************** Synopsis [Update scheduling information for reevaluation.] SideEffects [] ******************************************************************************/ static void AmcRescheduleForRefinement( st_table *fanOutSystemTable) { Amc_SubsystemInfo_t *subSystem; BlockSubsystemInfo_t *BlockSubsystem; st_generator *stGen; st_foreach_item(fanOutSystemTable, stGen, &subSystem, NIL(char *)) { /* reschedule only ones that are not taken */ if(!subSystem->takenIntoOptimal) { BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem); AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1); } } } /**Function******************************************************************** Synopsis [Refine result with transitive fanin subsystems.] SideEffects [] ******************************************************************************/ static mdd_t * AmcRefineWithSatisfyStatesOfFanInSystem( Amc_SubsystemInfo_t *subSystem, mdd_t *careStates) { st_table *fanInTable = AmcSubsystemReadFanInTable(subSystem); Amc_SubsystemInfo_t *fanInSystem; st_generator *stGen; mdd_t *oldCareStates = careStates; st_foreach_item(fanInTable, stGen, &fanInSystem, NIL(char *)) { if(fanInSystem->satisfyStates != NIL(mdd_t)) { mdd_t *fanInSatisfyStates = mdd_dup(fanInSystem->satisfyStates); careStates = mdd_and(fanInSatisfyStates, oldCareStates, 1, 1); mdd_free(oldCareStates); mdd_free(fanInSatisfyStates); oldCareStates = careStates; } } return(careStates); } /* end of "machine by machine" refinement of the careset */ #endif /**Function******************************************************************** Synopsis [Initialize mdd variables to be quantified. Used in under-approximation of the transition relation.] SideEffects [] ******************************************************************************/ static array_t * AmcInitializeQuantifyVars( Amc_SubsystemInfo_t *subSystem) { array_t *quantifyVars = array_alloc(array_t *, 0); array_t *quantifyPresentVars = array_alloc(int, 0); array_t *quantifyNextVars = array_alloc(int, 0); array_t *quantifyInputVars = array_alloc(int, 0); Ntk_Network_t *network = Fsm_FsmReadNetwork(AmcSubsystemReadFsm(subSystem)); Ntk_Node_t *latch; st_table *vertexTable = AmcSubsystemReadVertexTable(subSystem); lsGen gen; Ntk_NetworkForEachLatch(network, gen, latch) { char *latchName = Ntk_NodeReadName(latch); #ifdef AMC_DEBUG fprintf(vis_stdout, "\nlatch name: %s", latchName); fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(latch)); fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); fflush(vis_stdout); #endif if(!st_lookup(vertexTable, latchName, (char **)0)) { /* Next state variables. */ array_insert_last(int, quantifyNextVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); /* Present state variables. */ array_insert_last(int, quantifyPresentVars, Ntk_NodeReadMddId(latch)); } /* end of if(st_lookup(vertexTable)) */ } /* end of Ntk_NetworkForEachLatch */ { st_table *inputVarTable = st_init_table(st_numcmp, st_numhash); Ntk_Node_t *primaryInput; /* Build the hash table of input vars of this subsystem. */ /* arrayForEachItem(int, inputVarArray, i, inputVar) { st_insert(inputVarTable, (char *)(long)inputVar, (char *)0); } */ Ntk_NetworkForEachInput(network, gen, primaryInput) { int mddId = Ntk_NodeReadMddId(primaryInput); #ifdef AMC_DEBUG char *inputName = Ntk_NodeReadName(primaryInput); int testMddId = Ntk_NodeReadMddId(primaryInput); fprintf(vis_stdout, "\nprimary input name : %s", inputName); fprintf(vis_stdout, "\nprimary input mdd id : %d", testMddId); fflush(vis_stdout); #endif /* if(!st_lookup(inputVarTable, (char *)(long)mddId, (char **)0)) { */ array_insert_last(int, quantifyInputVars, mddId); /* } */ } st_free_table(inputVarTable); } array_insert_last(array_t *, quantifyVars, quantifyPresentVars); array_insert_last(array_t *, quantifyVars, quantifyNextVars); array_insert_last(array_t *, quantifyVars, quantifyInputVars); return quantifyVars; } #if 0 /**Function******************************************************************** Synopsis [Frees block-tearing specific data structure.] SideEffects [] ******************************************************************************/ static void AmcFreeBlockInfo( BlockInfo_t *BlockInfo) { if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) { Amc_AmcSubsystemFree(BlockInfo->optimalSystem); } } #endif /**Function******************************************************************** Synopsis [Read scheduling information.] SideEffects [] ******************************************************************************/ static int AmcBlockSubsystemReadScheduledForRefinement( BlockSubsystemInfo_t *system) { return system->scheduledForRefinement; } /**Function******************************************************************** Synopsis [Set scheduling information.] SideEffects [] ******************************************************************************/ static void AmcBlockSubsystemSetScheduledForRefinement( BlockSubsystemInfo_t *system, int data) { system->scheduledForRefinement = data; } #if 0 /**Function******************************************************************** Synopsis [Read optimal system.] SideEffects [] ******************************************************************************/ static Amc_SubsystemInfo_t * AmcBlockReadOptimalSubsystem( BlockInfo_t *system) { return system->optimalSystem; } #endif /**Function******************************************************************** Synopsis [Set optimal system.] SideEffects [] ******************************************************************************/ static void AmcBlockSetOptimalSystem( BlockInfo_t *system, Amc_SubsystemInfo_t *data) { system->optimalSystem = data; } #if 0 /**Function******************************************************************** Synopsis [Read best system.] SideEffects [] ******************************************************************************/ static int AmcBlockReadBestSystem( BlockInfo_t *system) { return system->bestSystem; } #endif /**Function******************************************************************** Synopsis [Set best system.] SideEffects [] ******************************************************************************/ static void AmcBlockSetBestSystem( BlockInfo_t *system, int data) { system->bestSystem = data; } #if 0 /**Function******************************************************************** Synopsis [Clear input variables from the FSM of the subsystem.] Description [Preimage computation existentially abstract both range variables and input variables. This function is used to prevent existential abstraction of input variables when computing the preimage.] SideEffects [] ******************************************************************************/ static Amc_SubsystemInfo_t * AmcClearInputVarsFromFSM( Amc_SubsystemInfo_t *subSystem) { Fsm_Fsm_t *fsm = subSystem->fsm; array_t *inputVarArray = Fsm_FsmReadInputVars(fsm); array_t *newInputVarArray = array_alloc(int, 0); array_free(inputVarArray); (void) Fsm_FsmSetInputVars(fsm, newInputVarArray); return(subSystem); } #endif