/**CFile*********************************************************************** FileName [mcUtil.c] PackageName [mc] Synopsis [Utilities for Fair CTL model checker and debugger] Author [Adnan Aziz, Tom Shiple, In-Ho Moon] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "mcInt.h" #include "mdd.h" #include "cmd.h" #include "fsm.h" #include "img.h" #include "sat.h" #include "baig.h" #include static char rcsid[] UNUSED = "$Id: mcUtil.c,v 1.113 2009/04/11 18:26:10 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void PrintNodes(array_t *mddIdArray, Ntk_Network_t *network); static array_t * SortMddIds(array_t *mddIdArray, Ntk_Network_t *network); static void PrintDeck(array_t *mddValues, array_t *mddIdArray, Ntk_Network_t *network); static int cmp(const void * s1, const void * s2); static boolean AtomicFormulaCheckSemantics(Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed); static void NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable); static void NodeTableAddLtlFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable); static boolean MintermCheckWellFormed(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr); static boolean SetCheckSupport(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr); static mdd_t * Mc_ComputeRangeOfPseudoInputs(Ntk_Network_t *network); static array_t *Mc_BuildBackwardRingsWithInvariants(mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Return Boolean TRUE/FALSE depending on whether states in specialStates can reach states in targetStates.] Description [Return Boolean TRUE/FALSE depending on whether states in specialStates can reach states in targetStates. If true, onionRings is set to results of fixed point computation going back from targetStates to specialStates.] SideEffects [] ******************************************************************************/ int Mc_FsmComputeStatesReachingToSet( Fsm_Fsm_t *modelFsm, mdd_t *targetStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *fromUpperBound; mdd_t *toCareSet; array_t *toCareSetArray = array_alloc(mdd_t *, 0); mdd_t *image; Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); mdd_t *reachingStates = mdd_dup( targetStates ); mdd_t *fromLowerBound = mdd_dup( targetStates ); /* Iterate until fromLowerBound is empty. */ while (mdd_is_tautology(fromLowerBound, 0) == 0){ /* fromLowerBound is the "onion shell" of states just examined. */ array_insert_last(mdd_t*, onionRings, mdd_dup(fromLowerBound)); if ( !mdd_lequal( fromLowerBound, specialStates, 1, 0 ) ) { mdd_free( fromLowerBound ); mdd_free( reachingStates ); return TRUE; } /* fromUpperBound is the set of all states reaching targets thus far. */ fromUpperBound = mdd_dup( reachingStates ); /* toCareSet is the set of all states not reached so far. */ toCareSet = mdd_not(reachingStates); array_insert(mdd_t *, toCareSetArray, 0, toCareSet); /* * Pre-Image of some set between lower and upper, where we care * about the image only on unreaching states. */ image = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); mdd_free(toCareSet); mdd_free(fromLowerBound); /* New set of reaching states is old set plus new image. */ mdd_free( reachingStates ); reachingStates = mdd_or(fromUpperBound, image, 1, 1); mdd_free(image); /* * New lower bound is the states just reached (note not on * fromUpperBound). */ fromLowerBound = mdd_and(reachingStates, fromUpperBound, 1, 0); mdd_free(fromUpperBound); } mdd_array_free( onionRings ); mdd_free( reachingStates ); mdd_free(fromLowerBound); array_free(toCareSetArray); return FALSE; } /**Function******************************************************************** Synopsis [Return Boolean TRUE/FALSE depending on whether states in specialStates are reachable from initialStates.] Description [Return Boolean TRUE/FALSE depending on whether states in specialStates are reachable from initialStates.If true, onionRings is set to results of fixed point computation going forward from initialStates to specialStates. Otherwise onionRings is freed.] SideEffects [] ******************************************************************************/ int Mc_FsmComputeStatesReachableFromSet( Fsm_Fsm_t *modelFsm, mdd_t *initialStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { boolean reachable=FALSE; mdd_t *fromUpperBound; mdd_t *toCareSet; array_t *toCareSetArray = array_alloc(mdd_t *, 0); mdd_t *image; Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); mdd_t *reachableStates = mdd_dup( initialStates ); mdd_t *fromLowerBound = mdd_dup( initialStates ); /* Iterate until fromLowerBound is empty. */ while (mdd_is_tautology(fromLowerBound, 0) == 0){ /* fromLowerBound is the "onion shell" of states just reached. */ array_insert_last(mdd_t*, onionRings, mdd_dup(fromLowerBound)); if (!mdd_lequal( fromLowerBound, specialStates, 1, 0 ) ) { mdd_free( fromLowerBound ); mdd_free( reachableStates ); return TRUE; } /* fromUpperBound is the set of all states reached thus far. */ fromUpperBound = mdd_dup( reachableStates ); /* toCareSet is the set of all states not reached so far. */ toCareSet = mdd_not(reachableStates); array_insert(mdd_t *, toCareSetArray, 0, toCareSet); /* * Image of some set between lower and upper, where we care * about the image only on unreached states. */ image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); mdd_free(toCareSet); mdd_free(fromLowerBound); /* New set of reachable states is old set plus new image. */ mdd_free( reachableStates ); reachableStates = mdd_or(fromUpperBound, image, 1, 1); mdd_free(image); /* * New lower bound is the states just reached (note not on * fromUpperBound). */ fromLowerBound = mdd_and(reachableStates, fromUpperBound, 1, 0); mdd_free(fromUpperBound); } mdd_array_free( onionRings ); mdd_free( reachableStates ); mdd_free(fromLowerBound); array_free(toCareSetArray); return reachable; } /**Function******************************************************************** Synopsis [Perform static semantic check of ctl formula on network.] Description [Perform static semantic check of ctl formula on network. Specifically, given an atomic formula of the form LHS=RHS, check that the LHS is the name of a latch/wire in the network, and that RHS is of appropriate type (enum/integer) and is lies in the range of the latch/wire values. If LHS is a wire, and inputsAllowed is false, check to see that the algebraic support of the wire consists of only latches and constants.] SideEffects [] ******************************************************************************/ boolean Mc_FormulaStaticSemanticCheckOnNetwork( Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed ) { boolean lCheck; boolean rCheck; Ctlp_Formula_t *leftChild; Ctlp_Formula_t *rightChild; if(formula == NIL(Ctlp_Formula_t)){ return TRUE; } if(Ctlp_FormulaReadType(formula) == Ctlp_ID_c){ return AtomicFormulaCheckSemantics(formula, network, inputsAllowed); } leftChild = Ctlp_FormulaReadLeftChild(formula); rightChild = Ctlp_FormulaReadRightChild(formula); lCheck = Mc_FormulaStaticSemanticCheckOnNetwork(leftChild, network, inputsAllowed); if(!lCheck) return FALSE; rCheck = Mc_FormulaStaticSemanticCheckOnNetwork(rightChild, network, inputsAllowed); if (!rCheck) return FALSE; return TRUE; } /**Function******************************************************************** Synopsis [Build Path to Core starting at aState.] Description [Build Path to Core (the first onion ring) starting at aState.

For the onion rings should be built in such a way that for every state v in ring i+1 there is a state v' in ring i such that there is an edge from v to v'. This function will also works for non-BFS rings, where we just require that for every state v in a ring i > 0, there is a state in a ring 0 <= j < i that is a successor of v.

For paths of length at least one, set PathLengthType to McGreaterZero_c. Otherwise, use McGreaterOrEqualZero_c. The function returns a sequence of states to a state in the core of onionRings, starting at aState. It is the users responsibility to free the array returned as well as its members.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildPathToCore( mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) { int i; /* index into the onionRings */ int startingPoint; mdd_t *currentState; Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); array_t *pathToCore; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *toCareSetArray; if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) { return(Mc_BuildPathToCoreFAFW( aState, onionRings, modelFsm, PathLengthType)); } pathToCore = array_alloc( mdd_t * , 0 ); toCareSetArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr)); if ( PathLengthType == McGreaterZero_c ) startingPoint = 1; else if ( PathLengthType == McGreaterOrEqualZero_c ) startingPoint = 0; else fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n"); /* RB: How do you guarantee that aState is in one of the onion rings [1,n]?*/ /*Find the lowest ring that holds aState*/ for ( i = startingPoint ; i < array_n( onionRings ); i++ ) { mdd_t *ring = array_fetch( mdd_t *, onionRings, i ); if ( McStateTestMembership( aState, ring ) ) break; } if ( i == array_n( onionRings ) ) return NIL(array_t); currentState = mdd_dup( aState ); array_insert_last( mdd_t *, pathToCore, currentState ); /* until we get to ring 0, keep finding successors for currentState */ while( i > 0 ) { mdd_t *currentStateSuccs; mdd_t *innerRing; mdd_t *currentStateSuccsInInnerRing; mdd_t *witnessSuccState; i--; currentStateSuccs = Img_ImageInfoComputeImageWithDomainVars(imageInfo, currentState, currentState, toCareSetArray); currentStateSuccsInInnerRing = mdd_zero(mddMgr); /* find the highest ring that contains a successor, starting with i */ while(mdd_is_tautology(currentStateSuccsInInnerRing, 0)){ assert(i >= 0); if(i < 0) return NIL(array_t); innerRing = array_fetch( mdd_t *, onionRings, i ); mdd_free(currentStateSuccsInInnerRing); currentStateSuccsInInnerRing = mdd_and(currentStateSuccs, innerRing, 1, 1 ); i--; } i++; witnessSuccState = Mc_ComputeACloseState(currentStateSuccsInInnerRing, currentState, modelFsm ); array_insert_last( mdd_t *, pathToCore, witnessSuccState ); currentState = witnessSuccState; mdd_free( currentStateSuccs ); mdd_free( currentStateSuccsInInnerRing ); /* next, see if we cannot move a few more rings down. We have to do this, * since a nontrivial path is not guaranteed to exist from a node in ring i * to a node in a lower ring. In fact a state in ring i may also be in * ring 0. */ { boolean contained = TRUE; while(contained && i > 0){ i--; innerRing = array_fetch( mdd_t *, onionRings, i ); contained = mdd_lequal(witnessSuccState, innerRing, 1, 1); } /* i is highest ring not containing witnessSuccState, or i = 0 */ if(!contained){ i++; } /* i is lowest ring containing witnessSuccState */ } } mdd_array_free(toCareSetArray); return pathToCore; } /**Function******************************************************************** Synopsis [Build a onion ring from initial state.] Description [Build a onion ring from initial state. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildForwardRings( mdd_t *S, Fsm_Fsm_t *fsm, array_t *onionRings) { mdd_t *nextStates; mdd_t *states, *nStates, *oneMdd; array_t *toCareSetArray, *forwardRings; int i; mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm); states = mdd_zero(mddMgr); oneMdd = mdd_one(mddMgr); for(i=0; iIn the case of BFS search, the onion rings are built forward, so that any state in ring i+1 has at least one predecessor in ring i-1. In non-BFS search that may not be true, but we will have that every state in ring i+1 has a predecessor in ring i or less. The fsm is checked to see if the search was BFS. If not, every ring from the beginning is searched to find the shortest path. This is a greedy heuristic and the shortest path is not guaranteed to be found. McBuildPathToCore takes a different approach.

It is the users responsibility to free the array returned as well as its members.] SideEffects [] SeeAlso[Mc_BuildPathToCore] ******************************************************************************/ array_t * Mc_BuildPathFromCore( mdd_t *aStates, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) { int i, j; int startingPoint; mdd_t *currentState, *aState; Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); array_t *pathToCore; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *toCareSetArray; array_t *pathFromCore; mdd_t *currentStatePreds, *currentStatePredsInInnerRing; mdd_t *innerRing = NIL(mdd_t), *witnessPredState; boolean shortestDist = (Fsm_FsmReadReachabilityOnionRingsMode(modelFsm) == Fsm_Rch_Bfs_c); if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) { pathFromCore = Mc_BuildPathFromCoreFAFW( aStates, onionRings, modelFsm, PathLengthType); return(pathFromCore); } aState = Mc_ComputeAState(aStates, modelFsm); pathToCore = array_alloc( mdd_t * , 0 ); toCareSetArray = NIL(array_t); if ( PathLengthType == McGreaterZero_c ) { startingPoint = 1; } else if ( PathLengthType == McGreaterOrEqualZero_c ) { startingPoint = 0; } else { fail("Called Mc_BuildPathFromCore with ill formed PathLengthType\n"); } /* check that the state occurs in an onion ring. */ for ( i = startingPoint ; i < array_n( onionRings ); i++ ) { mdd_t *ring = array_fetch( mdd_t *, onionRings, i ); if ( McStateTestMembership( aState, ring ) ) break; } if ( i == array_n( onionRings ) ) { mdd_free(aState); return NIL(array_t); } /* insert the state in the path to the core */ currentState = aState; array_insert_last( mdd_t *, pathToCore, currentState ); /* initialize */ toCareSetArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr)); /* loop until a path is found to the core */ while( i-- > 0 ) { if (shortestDist) { /* a predecessor is guaranteed to be in the previous ring */ mdd_array_free(toCareSetArray); toCareSetArray = array_alloc(mdd_t *, 0); innerRing = array_fetch( mdd_t *, onionRings, i ); array_insert(mdd_t *, toCareSetArray, 0, mdd_dup(innerRing)); currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars( imageInfo, currentState, currentState, toCareSetArray); } else { /* compute the predecessors */ currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars( imageInfo, currentState, currentState, toCareSetArray ); /* search for a predecessor in the earliest onion ring */ for (j = 0; j <= i; j++) { innerRing = array_fetch( mdd_t *, onionRings, j ); if (!mdd_lequal(currentStatePreds, innerRing, 1, 0)) { i = j; break; } } } /* compute the set of predecessors in the chosen ring. */ currentStatePredsInInnerRing = mdd_and(currentStatePreds, innerRing, 1, 1); mdd_free( currentStatePreds ); /* find a state in the predecessor */ witnessPredState = Mc_ComputeACloseState(currentStatePredsInInnerRing, currentState, modelFsm); mdd_free( currentStatePredsInInnerRing ); /* insert predecessor in the path */ array_insert_last( mdd_t *, pathToCore, witnessPredState ); currentState = witnessPredState; } mdd_array_free(toCareSetArray); /* flip the path to a path from the core */ { int i; pathFromCore = array_alloc( mdd_t *, 0 ); for( i=0; i < array_n( pathToCore ); i++ ) { mdd_t *tmpMdd = array_fetch(mdd_t *, pathToCore, (array_n(pathToCore) - (i+1))); array_insert_last( mdd_t *, pathFromCore, tmpMdd ); } array_free( pathToCore ); return pathFromCore; } } /**Function******************************************************************** Synopsis [Build a path from initial state to target.] Description [Build a path from initial state to target. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildPathToCoreFAFW( mdd_t *aStates, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) { int i, startingPoint; array_t *pathFromCore, *pathToCore; array_t *reachableOnionRings; mdd_t *currentStates; if ( PathLengthType == McGreaterZero_c ) { startingPoint = 1; } else if ( PathLengthType == McGreaterOrEqualZero_c ) { startingPoint = 0; } else { fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n"); } for ( i = startingPoint ; i < array_n( onionRings ); i++ ) { mdd_t *ring = array_fetch( mdd_t *, onionRings, i ); if ( McStateTestMembership( aStates, ring ) ) break; } if(i==0) { pathToCore = array_alloc( mdd_t * , 0 ); array_insert_last( mdd_t *, pathToCore, mdd_dup(aStates) ); return pathToCore; } reachableOnionRings = Mc_BuildForwardRings(aStates, modelFsm, onionRings); currentStates = array_fetch(mdd_t *, onionRings, 0); pathFromCore = Mc_BuildPathFromCoreFAFW( currentStates, reachableOnionRings, modelFsm, PathLengthType); mdd_array_free(reachableOnionRings); return(pathFromCore); } /**Function******************************************************************** Synopsis [Build a path from target to initial state with general algorithm.] Description [Build a path from target to initial state with general algorithm. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildPathFromCoreFAFWGeneral( mdd_t *T, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) { mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm); mdd_t *S, *H, *nH, *ring; int i; array_t *L; array_t *pathFromCore; array_t *npathFromCore; H = mdd_zero(mgr); for(i=0; i0) { Li = array_fetch(mdd_t *, L, i-1); nLi = bdd_smooth_with_cube(Li, extCube); Q_Li = mdd_and(Q, nLi, 1, 1); mdd_free(nLi); if(!mdd_equal(Q_Li, zeroMdd)) { i--; mdd_free(Q); Q = Q_Li; free = 1; imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1); Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo); Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer); /** Fsm_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); Fsm_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, Li); **/ } } ring_Q = NULL; for(q=0; q= array_n(R)) { imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1); Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo); /** Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); **/ continue; } Q = Mc_ComputeACloseState(ring_Q, T, modelFsm); mdd_free(ring_Q); if(free == 0) { array_insert_last(mdd_t *, path, (mdd_t *)((long)P+1)); } else if(free ==1) { array_insert_last(mdd_t *, path, P); free = 0; } Q_T = mdd_and(Q, T, 1, 1); if(!mdd_equal(Q_T, zeroMdd)) { array_insert_last(mdd_t *, path, (mdd_t *)((long)Q+1)); mdd_free(Q_T); break; } mdd_free(Q_T); P = Q; } array_free(careStatesArray); mdd_free(oneMdd); mdd_free(zeroMdd); imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1); Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo); /** Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); **/ return(path); } /**Function******************************************************************** Synopsis [Build a fate and free will layer.] Description [Build a fate and free will layer. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildFAFWLayer(Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H) { mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm); Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); mdd_t *zeroMdd, *oneMdd; mdd_t *S, *nH, *EX_S, *extCube, *S_new; array_t *L; array_t *careStatesArray; zeroMdd = mdd_zero(mgr); oneMdd = mdd_one(mgr); L = array_alloc(mdd_t *, 0); extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm); careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, oneMdd); while(!mdd_equal(H, zeroMdd)) { Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1); S = Mc_FsmEvaluateAUFormula(modelFsm, H, T, NIL(mdd_t), oneMdd, careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, 0, McVerbosityNone_c, McDcLevelNone_c, NIL(boolean)); Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0); array_insert_last(mdd_t *, L, S); S_new = bdd_smooth_with_cube(S, extCube); mdd_free(S); nH = mdd_and(H, S_new, 1, 0); if(mdd_equal(H, nH)) { mdd_free(nH); mdd_free(S_new); break; } mdd_free(H); H = nH; mdd_free(T); EX_S = Img_ImageInfoComputePreImageWithDomainVars( imageInfo, S_new, S_new, careStatesArray); mdd_free(S_new); T = mdd_and(EX_S, H, 1, 1); } array_free(careStatesArray); mdd_free(zeroMdd); mdd_free(oneMdd); mdd_free(T); mdd_free(H); return(L); } /**Function******************************************************************** Synopsis [Build a path from target to initial state.] Description [Build a path from target to initial state. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildPathFromCoreFAFW( mdd_t *Ts, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) { int startingPoint, prevFlag; int i, p, dist, forced; bdd_t *T, *S, *H, *nH, *Hp, *S1, *Swin; bdd_t *ring, *oneMdd, *zeroMdd; array_t *C, *newC, *AUrings, *segment; array_t *R, *ESrings; array_t *careStatesArray; array_t *pathFromCore; bdd_t *T_wedge_ring, *S1_wedge_ring, *Hp_wedge_S1; bdd_t *T_wedge_S, *C_T_wedge_S, *ESresult, *EX_T; bdd_t *EX_T_wedge_ring, *Hp_wedge_EX_T, *lastR; bdd_t *C_T_wedge_ring, *new_, *extCube; bdd_t *bundle, *single, *preSingle; Img_ImageInfo_t *imageInfo; mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm); if(Fsm_FsmReadFAFWFlag(modelFsm) == 2) { pathFromCore = Mc_BuildPathFromCoreFAFWGeneral( Ts, rings, modelFsm, PathLengthType); return(pathFromCore); } T = mdd_dup(Ts); imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); if ( PathLengthType == McGreaterZero_c ) { startingPoint = 1; } else if( PathLengthType == McGreaterOrEqualZero_c ) { startingPoint = 0; } else { fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n"); } oneMdd = mdd_one(mgr); zeroMdd = mdd_zero(mgr); S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint)); prevFlag = 0; /** free **/ H = mdd_zero(mgr); for(i=startingPoint; ip; i--) { ring = array_fetch(mdd_t *, rings, i); nH = mdd_and(H, ring, 1, 0); mdd_free(H); H = nH; } AUrings = array_alloc(mdd_t *, 0); Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1); Swin = Mc_FsmEvaluateAUFormula(modelFsm, H, T, NIL(mdd_t), oneMdd, careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, AUrings, McVerbosityNone_c, McDcLevelNone_c, NIL(boolean)); Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0); S1 = bdd_smooth_with_cube(Swin, extCube); mdd_array_free(AUrings); if(mdd_equal(S1, T)) { mdd_free(S1); mdd_free(Swin); continue; } for(i=p-1; i>=startingPoint; i--) { ring = array_fetch(mdd_t *, rings, i); S1_wedge_ring = mdd_and(S1, ring, 1, 1); if(mdd_equal(S1_wedge_ring, zeroMdd)) { mdd_free(S1_wedge_ring); break; } mdd_free(S1_wedge_ring); } p = i+1; Hp = array_fetch(mdd_t *, rings, p); ESrings = array_alloc(mdd_t *, 0); Hp_wedge_S1 = mdd_and(Hp, S1, 1, 1); ESresult = McEvaluateESFormulaWithGivenTRFAFW( modelFsm, S1, Hp_wedge_S1, NIL(mdd_t), oneMdd, careStatesArray, MC_NO_EARLY_TERMINATION, ESrings, McVerbosityNone_c, McDcLevelNone_c, NIL(boolean), Swin); mdd_free(ESresult); mdd_free(Hp_wedge_S1); mdd_free(S1); R = ESrings; if(array_n(R) <= 1) { mdd_array_free(R); mdd_free(Swin); continue; } } else { /* force segment */ Swin = 0; prevFlag = 0; /* free segment */ EX_T = Img_ImageInfoComputePreImageWithDomainVars( imageInfo, T, T, careStatesArray); for(i=p-1; i>=startingPoint; i--) { ring = array_fetch(mdd_t *, rings, i); EX_T_wedge_ring = mdd_and(EX_T, ring, 1, 1); if(mdd_equal(EX_T_wedge_ring, zeroMdd)) { mdd_free(EX_T_wedge_ring); break; } mdd_free(EX_T_wedge_ring); } p = i+1; Hp = array_fetch(mdd_t *, rings, p); R = array_alloc(mdd_t *, 0); Hp_wedge_EX_T = mdd_and(Hp, EX_T, 1, 1); array_insert_last(mdd_t *, R, Hp_wedge_EX_T); /**array_insert_last(mdd_t *, R, T); **/ array_insert_last(mdd_t *, R, mdd_dup(T)); mdd_free(EX_T); } lastR = array_fetch(mdd_t *, R, 0); segment = Mc_BuildShortestPathFAFW(Swin, lastR, T, R, mgr, modelFsm, prevFlag); if(Swin) { mdd_free(Swin); Swin = 0; } mdd_array_free(R); newC = array_join(C, segment); array_free(C); C = newC; T = array_fetch(mdd_t *, segment, array_n(segment)-1); if((long)T %2) T = (mdd_t *)((long)T - 1); /** T = mdd_dup(T); **/ array_free(segment); T_wedge_S = mdd_and(T, S, 1, 1); if(!mdd_equal(T_wedge_S, zeroMdd)) { mdd_free(T_wedge_S); /** mdd_free(T); **/ mdd_free(S); mdd_free(H); break; } mdd_free(T_wedge_S); startingPoint = 0; mdd_free(S); S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint)); } array_free(careStatesArray); mdd_free(oneMdd); mdd_free(zeroMdd); { int i; pathFromCore = array_alloc( mdd_t *, 0 ); if(startingPoint == 1) { T = array_fetch(mdd_t *, rings, 0); array_insert_last(mdd_t *, pathFromCore, bdd_dup(T)); } preSingle = NULL; for( i=0; i < array_n( C ); i++ ) { bundle = array_fetch(mdd_t *, C, (array_n(C) - (i+1))); forced = 0; if((long)bundle%2) { bundle = (mdd_t *)((long)bundle -1); forced++; } if(i==0) single = Mc_ComputeAState(bundle, modelFsm); else single = Mc_ComputeACloseState(bundle, preSingle, modelFsm); array_insert_last( mdd_t *, pathFromCore, (mdd_t *)((long)(single) + forced) ); preSingle = single; } McNormalizeBddPointer(C); mdd_array_free(C); return pathFromCore; } } /**Function******************************************************************** Synopsis [Build a shortest path from T to S.] Description [Make a shortest path from T to S which only passes through states in rings. There is always a path from T to S. Returns a sequence of states starting from T, leading to S. It is the users responsibility to free the returned array as well as its members. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * Mc_BuildShortestPathFAFW(mdd_t *win, mdd_t *S, mdd_t *T, array_t *rings, mdd_manager *mgr, Fsm_Fsm_t *fsm, int prevFlag) { int q, dist; mdd_t *zeroMdd, *oneMdd; mdd_t *inputCube; mdd_t *ring, *ring_wedge_T, *Cn, *Cs; mdd_t *K, *realK, *range; mdd_t *preimage_of_Cn; array_t *C, *stateVars, *inputVars; array_t *toCareSetArray; Img_ImageInfo_t *imageInfo; imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 1, 0); stateVars = Fsm_FsmReadPresentStateVars(fsm); inputVars = Fsm_FsmReadInputVars(fsm); inputCube = mdd_id_array_to_bdd_cube(mgr, inputVars); zeroMdd = mdd_zero(mgr); oneMdd = mdd_one(mgr); ring_wedge_T = NULL; for (q = 0; q < array_n(rings); q++){ ring = array_fetch(mdd_t *, rings, q); ring_wedge_T = mdd_and(T, ring, 1, 1); if(!mdd_equal(ring_wedge_T, zeroMdd)) break; mdd_free(ring_wedge_T); ring_wedge_T = 0; } if(ring_wedge_T) { mdd_free(ring_wedge_T); } else { fprintf(stdout, "We cannot find T\n"); } C = array_alloc(mdd_t *, 0); Cn = (T); toCareSetArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, toCareSetArray, 0, oneMdd); range = mdd_range_mdd(mgr, stateVars); while(q > 0) { preimage_of_Cn = Img_ImageInfoComputePreImageWithDomainVars( imageInfo, Cn, Cn, toCareSetArray); K = NULL; for (q = 0; q < array_n(rings); q++){ ring = array_fetch(mdd_t *, rings, q); K = mdd_and(preimage_of_Cn, ring, 1, 1); if(!mdd_equal(K, zeroMdd)) break; mdd_free(K); K = 0; } mdd_free(preimage_of_Cn); realK = mdd_and(K, range, 1, 1); mdd_free(K); Cs = bdd_closest_cube(realK, Cn, &dist); mdd_free(realK); Cn = bdd_smooth_with_cube(Cs, inputCube); mdd_free(Cs); if(!prevFlag) /** free segment **/ array_insert_last(mdd_t *, C, Cn); else /** fated segment **/ array_insert_last(mdd_t *, C, (mdd_t *)((long)Cn+1)); } array_free(toCareSetArray); mdd_free(zeroMdd); mdd_free(oneMdd); mdd_free(range); mdd_free(inputCube); return(C); } /**Function******************************************************************** Synopsis [Make a path from aState to bState.] Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members.] SideEffects [] ******************************************************************************/ array_t * Mc_CompletePath( mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis dirn) { if ( dirn == McFwd_c ) { return McCompletePathFwd(aState, bState, invariantStates, modelFsm, careSetArray, verbosity, dcLevel ); } else { return McCompletePathBwd(aState, bState, invariantStates, modelFsm, careSetArray, verbosity, dcLevel ); } } /**Function******************************************************************** Synopsis [Pick an arbitrary minterm from the given set.] Description [Pick an arbitrary minterm from the given set. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.] SideEffects [] ******************************************************************************/ mdd_t * Mc_ComputeAMinterm( mdd_t *aSet, array_t *Support, mdd_manager *mddMgr) { /* check that support of set is contained in Support */ assert( SetCheckSupport( aSet, Support, mddMgr )); assert(!mdd_is_tautology(aSet, 0)); if(bdd_get_package_name() == CUDD){ mdd_t *range; /* range of Support */ mdd_t *legalSet; /* aSet without the don't cares */ array_t *bddSupport; /* Support in terms of bdd vars */ mdd_t *minterm; /* a random minterm */ range = mdd_range_mdd(mddMgr, Support); legalSet = bdd_intersects(aSet, range); mdd_free(range); bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support); minterm = bdd_pick_one_minterm(legalSet, bddSupport); assert(MintermCheckWellFormed(minterm, Support, mddMgr)); assert(mdd_count_onset(mddMgr, minterm, Support) == 1); assert(mdd_lequal(minterm,legalSet,1,1)); mdd_array_free(bddSupport); mdd_free(legalSet); return minterm; }else{ int i, j; mdd_t *aSetDup; mdd_t *resultMdd; array_t *resultMddArray = array_alloc( mdd_t *, 0 ); aSetDup = mdd_dup( aSet ); for( i = 0 ; i < array_n( Support ); i++ ) { int aSupportVar = array_fetch( int, Support, i ); for( j = 0 ;;) { mdd_t *faceMdd, *tmpMdd; array_t *tmpArray = array_alloc( int, 0 ); array_insert_last( int, tmpArray, j ); /* this call will crash if have run through range of mvar */ faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray ); array_free( tmpArray ); tmpMdd = mdd_and( faceMdd, aSetDup, 1, 1 ); if ( !mdd_is_tautology( tmpMdd, 0 ) ) { array_insert_last( mdd_t *, resultMddArray, faceMdd ); mdd_free( aSetDup ); aSetDup = tmpMdd; break; } mdd_free( faceMdd ); mdd_free( tmpMdd ); j++; } } mdd_free( aSetDup ); resultMdd = mdd_one( mddMgr ); for ( i = 0 ; i < array_n( resultMddArray ); i++ ) { mdd_t *faceMdd = array_fetch( mdd_t *, resultMddArray, i ); mdd_t *tmpMdd = mdd_and( faceMdd, resultMdd, 1, 1 ); mdd_free( resultMdd ); mdd_free( faceMdd ); resultMdd = tmpMdd; } array_free( resultMddArray ); return resultMdd; }/* IF CUDD */ } /**Function******************************************************************** Synopsis [Pick a minterm from the given set close to target. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.] SideEffects [] ******************************************************************************/ mdd_t * Mc_ComputeACloseMinterm( mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr) { if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) { mdd_t *range; /* range of Support */ mdd_t *legalSet; /* aSet without the don't cares */ mdd_t *closeCube; int dist; array_t *bddSupport; /* Support in terms of bdd vars */ mdd_t *minterm; /* a random minterm */ /* Check that support of set is contained in Support. */ assert(SetCheckSupport(aSet, Support, mddMgr)); assert(!mdd_is_tautology(aSet, 0)); range = mdd_range_mdd(mddMgr, Support); legalSet = bdd_and(aSet, range, 1, 1); mdd_free(range); closeCube = mdd_closest_cube(legalSet, target, &dist); bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support); minterm = bdd_pick_one_minterm(closeCube, bddSupport); assert(MintermCheckWellFormed(minterm, Support, mddMgr)); assert(mdd_count_onset(mddMgr, minterm, Support) == 1); assert(mdd_lequal(minterm,legalSet,1,1)); mdd_array_free(bddSupport); mdd_free(legalSet); mdd_free(closeCube); return minterm; } else { return Mc_ComputeAMinterm(aSet, Support, mddMgr); }/* if CUDD */ } /* McComputeACloseMinterm */ /**Function******************************************************************** Synopsis [Return a string for a minterm.] SideEffects [] ******************************************************************************/ char * Mc_MintermToStringAiger( mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) { int i; char *tmp1String; char *tmp2String; char bodyString[McMaxStringLength_c]; char *mintermString = NIL(char); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork ); array_t *valueArray; array_t *stringArray = array_alloc( char *, 0 ); aMinterm = GET_NORMAL_PT(aMinterm); valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr); for ( i = 0 ; i < array_n( aSupport ); i++ ) { int mddId = array_fetch( int, aSupport, i ); int value = array_fetch( int, valueArray, i ); Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); char *nodeName = Ntk_NodeReadName( node ); if(!((nodeName[0] == '$') && (nodeName[1] == '_'))) { Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node ); if ( Var_VariableTestIsSymbolic( nodeVar ) ) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value ); sprintf( bodyString, "%s", symbolicValue ); } else { sprintf( bodyString, "%d", value ); } tmp1String = util_strsav( bodyString ); array_insert_last( char *, stringArray, tmp1String ); } } array_free(valueArray); array_sort( stringArray, cmp); for ( i = 0 ; i < array_n( stringArray ); i++ ) { tmp1String = array_fetch( char *, stringArray, i ); if( i == 0 ) { mintermString = util_strcat3(tmp1String, "", "" ); } else { tmp2String = util_strcat3(mintermString, "", tmp1String ); FREE(mintermString); mintermString = tmp2String; } FREE(tmp1String); } array_free( stringArray ); tmp1String = util_strcat3(mintermString, " ", ""); FREE(mintermString); mintermString = tmp1String; return mintermString; } /**Function******************************************************************** Synopsis [Return a string for a minterm.] SideEffects [] ******************************************************************************/ char * Mc_MintermToStringAigerInput( mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) { int i; char *tmp1String; char *tmp2String; char bodyString[McMaxStringLength_c]; char *mintermString = NIL(char); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork ); array_t *valueArray; array_t *stringArray = array_alloc( char *, 0 ); aMinterm = GET_NORMAL_PT(aMinterm); valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr); for ( i = 0 ; i < array_n( aSupport ); i++ ) { int mddId = array_fetch( int, aSupport, i ); int value = array_fetch( int, valueArray, i ); Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); char *nodeName = Ntk_NodeReadName( node ); if((nodeName[0] == '$') && (nodeName[1] == '_')) { Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node ); if ( Var_VariableTestIsSymbolic( nodeVar ) ) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value ); sprintf( bodyString, "%s", symbolicValue ); } else { sprintf( bodyString, "%d", value ); } tmp1String = util_strsav( bodyString ); array_insert_last( char *, stringArray, tmp1String ); } } array_free(valueArray); array_sort( stringArray, cmp); for ( i = 0 ; i < array_n( stringArray ); i++ ) { tmp1String = array_fetch( char *, stringArray, i ); if( i == 0 ) { mintermString = util_strcat3(tmp1String, "", "" ); } else { tmp2String = util_strcat3(mintermString, "", tmp1String ); FREE(mintermString); mintermString = tmp2String; } FREE(tmp1String); } array_free( stringArray ); tmp1String = util_strcat3(mintermString, " ", ""); FREE(mintermString); mintermString = tmp1String; return mintermString; } /**Function******************************************************************** Synopsis [Return a string for a minterm.] SideEffects [] ******************************************************************************/ char * Mc_MintermToString( mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) { int i; char *tmp1String; char *tmp2String; char bodyString[McMaxStringLength_c]; char *mintermString = NIL(char); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork ); array_t *valueArray; array_t *stringArray = array_alloc( char *, 0 ); aMinterm = GET_NORMAL_PT(aMinterm); valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr); for ( i = 0 ; i < array_n( aSupport ); i++ ) { int mddId = array_fetch( int, aSupport, i ); int value = array_fetch( int, valueArray, i ); Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); char *nodeName = Ntk_NodeReadName( node ); Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node ); if ( Var_VariableTestIsSymbolic( nodeVar ) ) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value ); sprintf( bodyString, "%s:%s", nodeName, symbolicValue ); } else { sprintf( bodyString, "%s:%d", nodeName, value ); } tmp1String = util_strsav( bodyString ); array_insert_last( char *, stringArray, tmp1String ); } array_free(valueArray); array_sort( stringArray, cmp); for ( i = 0 ; i < array_n( stringArray ); i++ ) { tmp1String = array_fetch( char *, stringArray, i ); if( i == 0 ) { mintermString = util_strcat3(tmp1String, "", "" ); } else { tmp2String = util_strcat3(mintermString, "\n", tmp1String ); FREE(mintermString); mintermString = tmp2String; } FREE(tmp1String); } array_free( stringArray ); tmp1String = util_strcat3(mintermString, "\n", ""); FREE(mintermString); mintermString = tmp1String; return mintermString; } /**Function******************************************************************** Synopsis [Utility function - prints states on path, inputs for transitions] SideEffects [] ******************************************************************************/ int Mc_PrintPath( array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput) { int check, forced, i; int numForced; mdd_t *inputSet=NIL(mdd_t); mdd_t *uInput = NIL(mdd_t); mdd_t *vInput = NIL(mdd_t); array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm ); array_t *inputVars = Fsm_FsmReadInputVars( modelFsm ); mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); forced = 0; check = 1; numForced = 0; for( i = -1 ; i < (array_n( aPath )-1); i++ ) { mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i ); mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) ); if((long)aState%2) { aState = (mdd_t *)((long)aState -1); forced++; } else forced = 0; if((long)bState%2) { bState = (mdd_t *)((long)bState -1); } if ( printInput == TRUE && i != -1) { inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, aState, bState ); vInput = Mc_ComputeACloseMinterm( inputSet, uInput, inputVars, mddMgr ); } if(forced) { fprintf(vis_stdout, "---- Forced %d\n", forced); numForced ++; } McPrintTransition( aState, bState, uInput, vInput, psVars, inputVars, printInput, modelFsm, (i+1) ); if ( uInput != NIL(mdd_t) ) { mdd_free(uInput); } uInput = vInput; if ( inputSet != NIL(mdd_t) ) { mdd_free(inputSet); } } if ( vInput != NIL(mdd_t) ) { mdd_free(uInput); } if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) { fprintf(vis_stdout, "# MC: the number of non-trivial forced segments %d\n", numForced); } return 1; } /**Function******************************************************************** Synopsis [Utility function - prints states on path, inputs for transitions] SideEffects [] ******************************************************************************/ int Mc_PrintPathAiger( array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput) { int check, forced, i; int numForced; mdd_t *inputSet=NIL(mdd_t); mdd_t *uInput = NIL(mdd_t); mdd_t *vInput = NIL(mdd_t); array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm ); array_t *inputVars = Fsm_FsmReadInputVars( modelFsm ); forced = 0; check = 1; numForced = 0; Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm ); FILE *psO = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0); for(i=0; i 0) { fprintf(vis_stdout, "# MC: the number of non-trivial forced segments %d\n", numForced); } return 1; } /**Function******************************************************************** Synopsis [Builds MVF for a node that is a pseudo input.] Description [Builds MVF for a node that is a pseudo input. This node has a single output and no inputs. Its table has several row entries. We build an MVF whose components correspond exactly to possible table outputs.] SideEffects [] Comment [Although pseudo inputs, constants, and internal nodes all have tables, a single procedure cannot be used to build their MVF. A pseudo input MVF is built in terms of its mddId, whereas a constant or internal is not. A constant or pseudo input doesn't have any inputs, whereas an internal does.] SeeAlso [Tbl_TableBuildMvfForNonDetConstant] ******************************************************************************/ static Mvf_Function_t * NodeBuildPseudoInputMvf( Ntk_Node_t * node, mdd_manager * mddMgr) { Mvf_Function_t *mvf; int columnIndex = Ntk_NodeReadOutputIndex(node); Tbl_Table_t *table = Ntk_NodeReadTable(node); int mddId = Ntk_NodeReadMddId(node); assert(mddId != NTK_UNASSIGNED_MDD_ID); mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex, mddId, mddMgr); return mvf; } /**Function******************************************************************** Synopsis [Return the range of pseudo inputs if they are defined by subsets of range.] Description [The result can be used to extract correct input conditions.] SideEffects [] ******************************************************************************/ static mdd_t * Mc_ComputeRangeOfPseudoInputs( Ntk_Network_t *network) { mdd_manager *mddMgr = Ntk_NetworkReadMddManager( network ); Mvf_Function_t *nodeMvf; mdd_t *tmpMdd, *zeroMdd; mdd_t *restrictMdd, *sumMdd; int restrictFlag; lsGen gen; Ntk_Node_t *node; int i; zeroMdd = mdd_zero(mddMgr); restrictMdd = mdd_one(mddMgr); restrictFlag = 0; Ntk_NetworkForEachPseudoInput(network, gen, node) { nodeMvf = NodeBuildPseudoInputMvf(node, mddMgr); for(i=0; inum; i++) { tmpMdd = array_fetch(mdd_t *, nodeMvf, i); if(mdd_equal(tmpMdd, zeroMdd)) { restrictFlag = 1; break; } } if(restrictFlag) { sumMdd = mdd_zero(mddMgr); for(i=0; inum; i++) { tmpMdd = array_fetch(mdd_t *, nodeMvf, i); if(!mdd_equal(tmpMdd, zeroMdd)) { tmpMdd = mdd_or( sumMdd, tmpMdd, 1, 1 ); mdd_free(sumMdd); sumMdd = tmpMdd; } } tmpMdd = mdd_and( sumMdd, restrictMdd, 1, 1 ); mdd_free(sumMdd); mdd_free(restrictMdd); restrictMdd = tmpMdd; } Mvf_FunctionFree(nodeMvf); } mdd_free(zeroMdd); return(restrictMdd); } /**Function******************************************************************** Synopsis [Return all inputs which cause a transition from aState to bState.] Description [Return all inputs which cause a transition from aState to bState. It is assumed that aState,bState are truly minterms over the PS variables.] SideEffects [] ******************************************************************************/ mdd_t * Mc_FsmComputeDrivingInputMinterms( Fsm_Fsm_t *fsm, mdd_t *aState, mdd_t *bState ) { int i; int psMddId; int inputMddId; mdd_gen *mddGen; Ntk_Node_t *latch, *node, *dataNode; array_t *aMinterm, *bMinterm; mdd_t *resultMdd; array_t *resultMvfs; array_t *inputArray = Fsm_FsmReadInputVars( fsm ); array_t *psArray = Fsm_FsmReadPresentStateVars( fsm ); Ntk_Network_t *network = Fsm_FsmReadNetwork( fsm ); st_table *leaves = st_init_table(st_ptrcmp, st_ptrhash); array_t *roots = array_alloc( Ntk_Node_t *, 0 ); array_t *latches = array_alloc( Ntk_Node_t *, 0 ); array_t *support = array_alloc( int, 0 ); mdd_t *rangeOfPseudoInputs, *tmpMdd; arrayForEachItem(int , psArray, i, psMddId ) { latch = Ntk_NetworkFindNodeByMddId( network, psMddId ); dataNode = Ntk_LatchReadDataInput( latch ); array_insert_last( int, support, psMddId ); array_insert_last( Ntk_Node_t *, roots, dataNode ); array_insert_last( Ntk_Node_t *, latches, latch ); } /* Convert the minterm to an array of assignments to support vars. */ foreach_mdd_minterm(aState, mddGen, aMinterm, support) { mdd_gen_free(mddGen); break; /* NOT REACHED */ } foreach_mdd_minterm(bState, mddGen, bMinterm, support) { mdd_gen_free(mddGen); break; /* NOT REACHED */ } array_free( support ); arrayForEachItem(int , inputArray, i, inputMddId ) { node = Ntk_NetworkFindNodeByMddId( network, inputMddId ); st_insert(leaves, (char *) node, (char *) NTM_UNUSED ); } for ( i = 0 ; i < array_n( roots ); i++ ) { int value = array_fetch( int, aMinterm, i ); latch = array_fetch( Ntk_Node_t *, latches, i ); st_insert( leaves, (char *) latch, (char *) (long) value ); } resultMvfs = Ntm_NetworkBuildMvfs( network, roots, leaves, NIL(mdd_t) ); array_free( roots ); array_free( latches ); st_free_table( leaves ); rangeOfPseudoInputs = Mc_ComputeRangeOfPseudoInputs(network); resultMdd = rangeOfPseudoInputs; for ( i = 0 ; i < array_n( resultMvfs ) ; i++ ) { Mvf_Function_t *mvf = array_fetch( Mvf_Function_t *, resultMvfs, i ); int value = array_fetch( int, bMinterm, i ); mdd_t *activeMdd = Mvf_FunctionReadComponent( mvf, value ); tmpMdd = mdd_and( activeMdd, resultMdd, 1, 1 ); if(mdd_is_tautology(tmpMdd, 0)) { fprintf(stdout, "current error\n"); } mdd_free( resultMdd ); resultMdd = tmpMdd; Mvf_FunctionFree( mvf ); } array_free( resultMvfs); array_free( aMinterm ); array_free( bMinterm ); return resultMdd; } /**Function******************************************************************** Synopsis [Select an arbitrary state from the given set] SideEffects [] ******************************************************************************/ mdd_t * Mc_ComputeAState( mdd_t *states, Fsm_Fsm_t *modelFsm) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr ); return result; } /**Function******************************************************************** Synopsis [Select a state from the given set close to target.] SideEffects [] ******************************************************************************/ mdd_t * Mc_ComputeACloseState( mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); mdd_t *result = Mc_ComputeACloseMinterm( states, target, PSVars, mddMgr ); return result; } /**Function******************************************************************** Synopsis [Print a minterm.] SideEffects [] ******************************************************************************/ void Mc_MintermPrint( mdd_t *aMinterm, array_t *support, Ntk_Network_t *aNetwork) { char *tmpString = Mc_MintermToString( aMinterm, support, aNetwork ); fprintf( vis_stdout, "%s", tmpString ); FREE(tmpString); } /**Function******************************************************************** Synopsis [Add nodes for wires referred to in formula to nodesTable.] SideEffects [] ******************************************************************************/ void Mc_NodeTableAddCtlFormulaNodes( Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable ) { NodeTableAddCtlFormulaNodes( network, formula, nodesTable ); } /**Function******************************************************************** Synopsis [Add nodes for wires referred to in formula to nodesTable.] Description [Add nodes for wires referred to in formula to nodesTable.] SideEffects [] ******************************************************************************/ void Mc_NodeTableAddLtlFormulaNodes( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable ) { NodeTableAddLtlFormulaNodes(network, formula, nodesTable); } /**Function******************************************************************** Synopsis [Form an FSM reduced with respect to the specified formula] Description [Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.] SideEffects [] ******************************************************************************/ Fsm_Fsm_t * Mc_ConstructReducedFsm( Ntk_Network_t *network, array_t *ctlFormulaArray) { return(McConstructReducedFsm(network, ctlFormulaArray)); } /**Function******************************************************************** Synopsis [Converts a string to a schedule type.] Description [Converts a string to a schedule type. If string does not refer to one of the allowed schedule types, then returns McGSH_Unassigned_c.] SideEffects [] ******************************************************************************/ Mc_GSHScheduleType Mc_StringConvertToScheduleType( char *string) { return McStringConvertToScheduleType(string); } /**Function******************************************************************** Synopsis [Converts a string to a lockstep mode.] Description [Converts a string to a lockstep mode. If string does not refer to one of the allowed lockstep modes, it returns MC_LOCKSTEP_UNASSIGNED. The allowed values are: MC_LOCKSTEP_OFF, MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive integer n (lockstep enumerates up to n fair SCCs).] SideEffects [] ******************************************************************************/ int Mc_StringConvertToLockstepMode( char *string) { return McStringConvertToLockstepMode(string); } /**Function******************************************************************** Synopsis [Allocate an earlytermination struct and initialize with arguments] SideEffects [] ******************************************************************************/ Mc_EarlyTermination_t * Mc_EarlyTerminationAlloc( Mc_EarlyTerminationType mode, mdd_t *states) { Mc_EarlyTermination_t *result = ALLOC(Mc_EarlyTermination_t, 1); result->mode = mode; if (states != NIL(mdd_t)) { result->states = mdd_dup(states); } else { result->states = NIL(mdd_t); } return result; } /**Function******************************************************************** Synopsis [Free an earlytermination struct (you are allowed to pass MC_NO_EARLY_TERMINATION, or NULL, and it will have no effect. ] SideEffects [] ******************************************************************************/ void Mc_EarlyTerminationFree(Mc_EarlyTermination_t *earlyTermination) { if(earlyTermination == NIL(Mc_EarlyTermination_t) || earlyTermination == MC_NO_EARLY_TERMINATION) return; if(earlyTermination->states != NIL(mdd_t)) mdd_free(earlyTermination->states); free(earlyTermination); return; } /**Function******************************************************************** Synopsis [Return TRUE iff the early termination condition specifies that the computation can be entirely skipped.] SideEffects [none] ******************************************************************************/ boolean Mc_EarlyTerminationIsSkip(Mc_EarlyTermination_t *earlyTermination) { if (earlyTermination == NIL(Mc_EarlyTermination_t) || earlyTermination == MC_NO_EARLY_TERMINATION) return FALSE; return (earlyTermination->mode == McCare_c && earlyTermination->states == NIL(mdd_t)); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Make a path from aState to bState using fwd reachability.] Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from aState and does forward reachability till it hits bState or a fixed point.] SideEffects [] ******************************************************************************/ array_t * McCompletePathFwd( mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *tmp1Mdd; array_t *result; mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); mdd_t *zeroMdd = mdd_zero( mddMgr ); array_t *onionRings = array_alloc( mdd_t *, 0 ); Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); mdd_t *c0, *c1; assert( mdd_lequal( aState, invariantStates, 1, 1 ) ); assert( mdd_lequal( bState, invariantStates, 1, 1 ) ); if ( mdd_equal( aState, bState ) ) { /* * Alter the starting point to force routine to produce cycle if exists * Question: would it be quicker to do simultaneous backward/forward * analysis? */ c0 = mdd_dup( aState ); array_insert_last( mdd_t *, onionRings, c0 ); tmp1Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState, aState, careSetArray); c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 ); mdd_free(tmp1Mdd); array_insert_last( mdd_t *, onionRings, c1 ); } else { c0 = zeroMdd; c1 = mdd_dup( aState ); array_insert_last( mdd_t *, onionRings, c1 ); } while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) { mdd_t *tmp2Mdd; if ( McStateTestMembership( bState, c1 ) ) { break; } /* * performance gain from using dc's in this fp computation. * use only when dclevel >= max */ if ( dcLevel >= McDcLevelRchFrontier_c ) { mdd_t *annulusMdd = mdd_and( c0, c1, 0, 1 ); mdd_t *discMdd = mdd_dup( c1 ); mdd_t *dcMdd = bdd_between( annulusMdd, discMdd ); tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, annulusMdd, discMdd, careSetArray); if ( verbosity > McVerbosityNone_c ) { fprintf(vis_stdout, "--Fwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n", mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd)); } mdd_free( annulusMdd ); mdd_free( discMdd ); mdd_free( dcMdd ); } else { tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, c1, c1, careSetArray); } tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1); mdd_free(tmp2Mdd); c0 = c1; c1 = mdd_or( c1, tmp1Mdd, 1, 1 ); mdd_free( tmp1Mdd ); array_insert_last( mdd_t *, onionRings, c1 ); } if ( McStateTestMembership( bState, c1 ) ) { result = Mc_BuildPathFromCore(bState, onionRings, modelFsm, McGreaterZero_c ); } else { result = NIL(array_t); } mdd_free( zeroMdd ); mdd_array_free( onionRings); return result; } /**Function******************************************************************** Synopsis [Make a path from aState to bState using bwd reachability.] Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from bState and does backward reachability till it hits aState or a fixed point.] SideEffects [] ******************************************************************************/ array_t * McCompletePathBwd( mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *tmp1Mdd; array_t *result; mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); mdd_t *zeroMdd = mdd_zero( mddMgr ); array_t *onionRings = array_alloc( mdd_t *, 0 ); Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); mdd_t *c0, *c1; assert( mdd_lequal( aState, invariantStates, 1, 1 ) ); assert( mdd_lequal( bState, invariantStates, 1, 1 ) ); if ( mdd_equal( aState, bState ) ) { /* * Alter the starting point to force routine to produce cycle if exists * Question: would it be quicker to do simultaneous backward/forward * analysis? */ c0 = mdd_dup( bState ); array_insert_last( mdd_t *, onionRings, c0 ); tmp1Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, bState, bState, careSetArray); c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 ); mdd_free(tmp1Mdd); array_insert_last( mdd_t *, onionRings, c1 ); } else { c0 = zeroMdd; c1 = mdd_dup( bState ); array_insert_last( mdd_t *, onionRings, c1 ); } while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) { mdd_t *tmp2Mdd; if ( McStateTestMembership( aState, c1 ) ) { break; } /* * performance gain from using dc's in this fp computation. * use only when dclevel >= max */ if ( dcLevel >= McDcLevelRchFrontier_c ) { mdd_t *annulusMdd = mdd_and( c0, c1, 0, 1 ); mdd_t *discMdd = mdd_dup( c1 ); mdd_t *dcMdd = bdd_between( annulusMdd, discMdd ); tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, annulusMdd, discMdd, careSetArray); if ( verbosity > McVerbosityNone_c ) { fprintf(vis_stdout, "--Bwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n", mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd)); } mdd_free( annulusMdd ); mdd_free( discMdd ); mdd_free( dcMdd ); } else { tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, c1, c1, careSetArray); } tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1); mdd_free(tmp2Mdd); c0 = c1; c1 = mdd_or( c1, tmp1Mdd, 1, 1 ); mdd_free( tmp1Mdd ); array_insert_last( mdd_t *, onionRings, c1 ); } if ( McStateTestMembership( aState, c1 ) ) { result = Mc_BuildPathToCore(aState, onionRings, modelFsm, McGreaterZero_c); } else { result = NIL(array_t); } mdd_free( zeroMdd ); mdd_array_free( onionRings); return result; } /**Function******************************************************************** Synopsis [Write resettability condition as a CTL formula] CommandName [_init_state_formula] CommandSynopsis [write resettability condition as a CTL formula] CommandArguments [ \[-h\] \[<init_file>\] ] CommandDescription [Write resettability condition as a CTL formula. Writes to init_file is specified, else stdout.] SideEffects [] ******************************************************************************/ int McCommandInitState( Hrc_Manager_t **hmgr, int argc, char **argv) { mdd_t *modelInitialStates; mdd_t *anInitialState; Fsm_Fsm_t *modelFsm; char *formulaTxt; array_t *stateVars; FILE *ctlFile; if ( argc == 1 ) { ctlFile = vis_stdout; } else { if ( !strcmp( "-h", argv[1] ) || ( argc > 2 ) ) { fprintf( vis_stdout, "Usage: _init_state_formula [-h] init_file\n\tinit_file - file to write init state formula to (default is stdout)\n"); return 1; } ctlFile = Cmd_FileOpen( argv[1], "w", NIL(char *), 0 ); } modelFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); if (modelFsm == NIL(Fsm_Fsm_t)) { if ( argc != 1 ) { fclose( ctlFile ); } return 1; } stateVars = Fsm_FsmReadPresentStateVars( modelFsm ); modelInitialStates = Fsm_FsmComputeInitialStates( modelFsm ); if ( modelInitialStates == NIL(mdd_t) ) { (void) fprintf( vis_stdout, "** mc error: - cant build init states (mutual latch dependancy?)\n%s\n", error_string() ); if ( argc != 1 ) { fclose( ctlFile ); } return 1; } anInitialState = Mc_ComputeAState( modelInitialStates, modelFsm ); mdd_free(modelInitialStates); formulaTxt = McStatePrintAsFormula( anInitialState, stateVars, modelFsm ); mdd_free(anInitialState); fprintf( ctlFile, "AG EF %s;\n", formulaTxt ); FREE(formulaTxt); if ( argc != 1 ) { fclose(ctlFile); } return 0; } /**Function******************************************************************** Synopsis [Return a CTL formula for a minterm.] SideEffects [] ******************************************************************************/ char * McStatePrintAsFormula( mdd_t *aMinterm, array_t *aSupport, Fsm_Fsm_t *modelFsm) { int i; char *tmp1String; char *tmp2String; char *tmp3String; char bodyString[McMaxStringLength_c]; char *mintermString = NIL(char); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm ); array_t *valueArray = McConvertMintermToValueArray( aMinterm, aSupport, mddMgr ); array_t *stringArray = array_alloc( char *, 0 ); for ( i = 0 ; i < array_n( aSupport ); i++ ) { int mddId = array_fetch( int, aSupport, i ); int value = array_fetch( int, valueArray, i ); Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); char *nodeName = Ntk_NodeReadName( node ); Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node ); if ( Var_VariableTestIsSymbolic( nodeVar ) ) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value ); sprintf( bodyString, "%s=%s", nodeName, symbolicValue ); } else { sprintf( bodyString, "%s=%d", nodeName, value ); } tmp1String = util_strsav( bodyString ); array_insert_last( char *, stringArray, tmp1String ); } array_free(valueArray); array_sort( stringArray, cmp); for ( i = 0 ; i < array_n( stringArray ); i++ ) { tmp1String = array_fetch( char *, stringArray, i ); if( i == 0 ) { mintermString = util_strcat3("(", tmp1String, ")" ); } else { tmp2String = util_strcat3( mintermString, " * (", tmp1String ); FREE(mintermString); tmp3String = util_strcat3( tmp2String, ")", "" ); FREE(tmp2String); mintermString = tmp3String; } FREE(tmp1String); } array_free( stringArray ); tmp1String = util_strcat3( "( ", mintermString, " )" ); FREE(mintermString); mintermString = tmp1String; return mintermString; } /**Function******************************************************************** Synopsis [Search the given array of "Onion Rings" for the Onion Rings with the clore closest to specified state.] Description [Search the given array of "Onion Rings" for the Onion Rings with the core closest to specified state. By "Onion Rings" we refer to an array of sets of states (so arrayOfOnionRings is an array of arrays of states). The first member of a set of onion rings is referred to as the "core". The "Onion Rings" array has the property that the first set is all states that can reach the core (this may be mod a care set like the reached states). The succesive sets are those which can reach the core in successively fewer iterations. We find the i with the smallest index j for which arrayOfOnionRings[i][j] contains aState.] SideEffects [] ******************************************************************************/ int McComputeOnionRingsWithClosestCore( mdd_t *aState, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm) { int index; int distance = 0; while( TRUE ) { for( index = 0 ; index < array_n( arrayOfOnionRings ) ; index++ ) { array_t *iOnionRings = array_fetch( array_t *, arrayOfOnionRings, index ); /* will crash if run out of rings -> if not in there */ mdd_t *stateSet = array_fetch( mdd_t *, iOnionRings, distance ); if ( McStateTestMembership( aState, stateSet ) ) return index; } distance++; } assert(0); } /**Function******************************************************************** Synopsis [Remove array indexed by index from array of arrays.] Description [Remove array indexed by index from array of arrays. Does NOT free the input arrayOfOnionRings.] SideEffects [] ******************************************************************************/ array_t * McRemoveIndexedOnionRings( int index, array_t *arrayOfOnionRings) { int i; array_t *dupArrayOfOnionRings = array_alloc( array_t *, 0 ); array_t *OnionRings; for ( i = 0 ; i < array_n( arrayOfOnionRings ) ; i++ ) { if ( i == index ) { continue; } OnionRings = array_fetch( array_t *, arrayOfOnionRings, i ); array_insert_last( array_t *, dupArrayOfOnionRings, OnionRings ); } return dupArrayOfOnionRings; } /**Function******************************************************************** Synopsis [Convert a minterm to an array of integers] SideEffects [] ******************************************************************************/ array_t * McConvertMintermToValueArray( mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr) { array_t *resultValueArray; /* this will be performed only in v0s-g executables */ assert( MintermCheckWellFormed( aMinterm, aSupport, mddMgr )); resultValueArray = array_alloc( int, 0 ); { int i; for( i = 0 ; i < array_n( aSupport ); i++ ) { int aSupportVar = array_fetch( int, aSupport, i ); int j; for( j = 0 ; TRUE ; j++) { mdd_t *faceMdd, *tmpMdd; array_t *tmpArray = array_alloc( int, 0 ); array_insert_last( int, tmpArray, j ); faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray ); array_free( tmpArray ); tmpMdd = mdd_and( faceMdd, aMinterm, 1, 1 ); mdd_free( faceMdd ); if ( !mdd_is_tautology( tmpMdd, 0 ) ) { mdd_free( tmpMdd ); array_insert_last( int, resultValueArray, j ); break; } mdd_free( tmpMdd ); } } } return resultValueArray; } /**Function******************************************************************** Synopsis [Print a transition to vis_stdout.] Description [Print a transition to vis_stdout. The transition is supposed to be from aState to bState on input vInput. If uInput is not NIL, instead of printing vInput, we only print the places where it differs from uInput. If there is no difference anywhere, we print "-Unchanged-". Similarly, we print only the incremental difference from aState to bState; if there is none, we print "-Unchanged-". If aState is NIL we simply print bState and return.] SideEffects [] ******************************************************************************/ void McPrintTransitionAiger( mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber) { Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm ); char *aString = aState ? Mc_MintermToStringAiger( aState, stateSupport, modelNetwork ) : NIL(char); char *bString = Mc_MintermToStringAiger( bState, stateSupport, modelNetwork ); char *inpString = aState ? Mc_MintermToStringAigerInput( aState, stateSupport, modelNetwork ) : NIL(char); st_table *node2MvfAigTable; node2MvfAigTable = (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY); if ( aState == NIL(mdd_t) ) { FREE(bString); return; } fprintf(vis_stdout, "%s", aString); fprintf(vis_stdout, "%s", inpString); /* first test that there are inputs */ /* if ( array_n( inputSupport ) > 0 ) { if ( uInput == NIL(mdd_t) ) { char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork ); FREE(vString); } else { boolean unchanged=TRUE; char *uString = Mc_MintermToStringAiger( uInput, inputSupport, modelNetwork ); char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork ); FREE(uString); FREE(vString); } } */ if(seqNumber == 1) { fprintf(vis_stdout, "1 "); } else { fprintf(vis_stdout, "0 "); } fprintf(vis_stdout, "%s", bString); FREE( aString ); FREE( bString ); fprintf (vis_stdout, "\n"); return; } /**Function******************************************************************** Synopsis [Print a transition to vis_stdout.] Description [Print a transition to vis_stdout. The transition is supposed to be from aState to bState on input vInput. If uInput is not NIL, instead of printing vInput, we only print the places where it differs from uInput. If there is no difference anywhere, we print "-Unchanged-". Similarly, we print only the incremental difference from aState to bState; if there is none, we print "-Unchanged-". If aState is NIL we simply print bState and return.] SideEffects [] ******************************************************************************/ void McPrintTransition( mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber) { Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm ); char *aString = aState ? Mc_MintermToString( aState, stateSupport, modelNetwork ) : NIL(char); char *bString = Mc_MintermToString( bState, stateSupport, modelNetwork ); char *tmp1String = aString; char *tmp2String = bString; char *ptr1; char *ptr2; st_table *node2MvfAigTable; node2MvfAigTable = (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY); if ( aState == NIL(mdd_t) ) { fprintf( vis_stdout, "--State %d:\n%s\n", seqNumber, bString ); FREE(bString); return; } fprintf(vis_stdout, "--Goes to state %d:\n", seqNumber ); { boolean unchanged=TRUE; while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) { ptr2 = strchr( tmp2String, '\n' ); *ptr1 = 0; *ptr2 = 0; if ( (strcmp( tmp1String, tmp2String ) ) ) { fprintf( vis_stdout, "%s\n", tmp2String ); unchanged = FALSE; } tmp1String = & (ptr1[1]); tmp2String = & (ptr2[1]); } if (unchanged == TRUE) { fprintf( vis_stdout, "\n"); } } if ( printInputs == TRUE ) { /* first test that there are inputs */ if ( array_n( inputSupport ) > 0 ) { fprintf(vis_stdout, "--On input:\n"); if ( uInput == NIL(mdd_t) ) { char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork ); fprintf(vis_stdout, "%s", vString ); FREE(vString); } else { boolean unchanged=TRUE; char *uString = Mc_MintermToString( uInput, inputSupport, modelNetwork ); char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork ); tmp1String = uString; tmp2String = vString; while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) { ptr2 = strchr( tmp2String, '\n' ); *ptr1 = 0; *ptr2 = 0; if ( (strcmp( tmp1String, tmp2String ) ) ) { fprintf( vis_stdout, "%s\n", tmp2String ); unchanged = FALSE; } tmp1String = & (ptr1[1]); tmp2String = & (ptr2[1]); } if (unchanged == TRUE) { fprintf( vis_stdout, "\n"); } FREE(uString); FREE(vString); } } } FREE( aString ); FREE( bString ); fprintf (vis_stdout, "\n"); } /**Function******************************************************************** Synopsis [Print message saying given state passes formula.] SideEffects [] ******************************************************************************/ void McStatePassesFormula( mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) { McStatePassesOrFailsFormula( aState, formula, 1, debugLevel, modelFsm ); } /**Function******************************************************************** Synopsis [Print message saying given state fails formula.] SideEffects [] ******************************************************************************/ void McStateFailsFormula( mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) { McStatePassesOrFailsFormula( aState, formula, 0, debugLevel, modelFsm ); } /**Function******************************************************************** Synopsis [Utility function - prints state passes or fails formula] SideEffects [] ******************************************************************************/ void McStatePassesOrFailsFormula( mdd_t *aState, Ctlp_Formula_t *formula, int pass, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); char *formulaText = Ctlp_FormulaConvertToString( formula ); Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm ); /* Nodes created in converting formulae like AU may not have text * attached to them. */ if (formulaText == NIL(char)) return; fprintf( vis_stdout, "--State\n"); Mc_MintermPrint( aState, PSVars, modelNetwork ); if ( pass ) fprintf( vis_stdout, "passes "); else fprintf( vis_stdout, "fails "); if( debugLevel > McDbgLevelMin_c) fprintf(vis_stdout, "%s.\n\n", formulaText); else fprintf(vis_stdout, "\n\n"); FREE(formulaText); } /**Function******************************************************************** Synopsis [Utility function - convert McPath_t to normal form.] Description [Utility function - convert McPath_t to normal form. A normal McPath_t is one where the stem leads to a state, which then returns it self in the cycle.] SideEffects [] ******************************************************************************/ McPath_t * McPathNormalize( McPath_t *aPath) { int i, j; int forced; array_t *stemArray = McPathReadStemArray( aPath ); array_t *cycleArray = McPathReadCycleArray( aPath ); McPath_t *result = McPathAlloc(); array_t *newStem = array_alloc( mdd_t *, 0 ); array_t *newCycle = array_alloc( mdd_t *, 0 ); mdd_t *lastState = GET_NORMAL_PT(array_fetch_last(mdd_t *, cycleArray)); McPathSetStemArray( result, newStem ); McPathSetCycleArray( result, newCycle ); for( i = 0 ; i < array_n( stemArray ) ; i++ ) { mdd_t *tmpState = array_fetch( mdd_t *, stemArray, i ); forced = 0; if((long)tmpState % 2) { forced = 1; tmpState = (mdd_t *)((long)tmpState - 1); } array_insert_last(mdd_t *, newStem, (mdd_t *)((long)(mdd_dup(tmpState)) + forced) ); if ( mdd_equal( lastState, tmpState ) ) { break; } } for( j = i; j < array_n( stemArray ); j++ ) { mdd_t *tmpState = array_fetch( mdd_t *, stemArray, j ); forced = 0; if((long)tmpState % 2) { forced = 1; tmpState = (mdd_t *)((long)tmpState - 1); } array_insert_last(mdd_t *, newCycle, (mdd_t *)((long)(mdd_dup(tmpState)) + forced) ); } /* first state of cycle array == last state of stem array => start from j=1 */ for( j = 1; j < array_n( cycleArray ); j++ ) { mdd_t *tmpState = array_fetch( mdd_t *, cycleArray, j ); forced = 0; if((long)tmpState % 2) { forced = 1; tmpState = (mdd_t *)((long)tmpState - 1); } array_insert_last(mdd_t *, newCycle, (mdd_t *)((long)(mdd_dup(tmpState)) + forced) ); } return result; } /**Function******************************************************************** Synopsis [Utility function - merges two paths.] Description [Utility function - merges two paths. Note that the merge is done by adding the elements of the second array starting from the second element onwards. This is because we often have to merge paths where the end point of the first is the starting point of the second.] SideEffects [] ******************************************************************************/ array_t * McCreateMergedPath( array_t *aPath, array_t *bPath) { int i, pos, forced; mdd_t *tmpState, *endOfAPath; array_t *aPathDup = McMddArrayDuplicateFAFW( aPath ); array_t *bPathDup = McMddArrayDuplicateFAFW( bPath ); for( i = 1 ; i < array_n( bPathDup ) ; i++ ) { tmpState = array_fetch( mdd_t *, bPathDup, i ); array_insert_last( mdd_t *, aPathDup, tmpState ); } pos = array_n(aPathDup) - array_n(bPathDup); endOfAPath = array_fetch(mdd_t *, aPathDup, pos); tmpState = array_fetch( mdd_t *, bPathDup, 0 ); forced = 0; if((long)tmpState % 2) { forced = 1; tmpState = (mdd_t *)((long)tmpState - 1); } if(forced && mdd_equal(tmpState, endOfAPath)) { array_insert(mdd_t *, aPathDup, pos, (mdd_t *)((long)endOfAPath + forced) ); } mdd_free( tmpState ); array_free( bPathDup ); return aPathDup; } /**Function******************************************************************** Synopsis [Utility function - duplicate bdd array.] Description [To represent the forced segment, the mdd_t is complemented. Therefore one cannot use mdd_array_duplicate. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ array_t * McMddArrayDuplicateFAFW(array_t *mddArray) { int i, forced; mdd_t *newTempMdd; int length = array_n(mddArray); array_t *result = array_alloc(mdd_t *, length); for (i = 0; i < length; i++) { mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i); forced = 0; if((long)tempMdd % 2) { forced = 1; tempMdd = (mdd_t *)((long)tempMdd - 1); } newTempMdd = mdd_dup(tempMdd); array_insert(mdd_t *, result, i, (mdd_t *)((long)newTempMdd + forced)); } return (result); } /**Function******************************************************************** Synopsis [Utility function - compute the intersection of the elements.] Description [Utility function - compute the intersection of the elements.] SideEffects [] ******************************************************************************/ mdd_t * McMddArrayAnd(array_t *mddArray) { mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t); int i; result = NIL(mdd_t); arrayForEachItem(mdd_t *, mddArray, i, mdd1) { if (result == NIL(mdd_t)) result = mdd_dup(mdd1); else { mdd2 = result; result = mdd_and(result, mdd1, 1, 1); mdd_free(mdd2); } } return (result); } /**Function******************************************************************** Synopsis [Utility function - compute the union of the elements.] Description [Utility function - compute the union of the elements.] SideEffects [] ******************************************************************************/ mdd_t * McMddArrayOr(array_t *mddArray) { mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t); int i; result = NIL(mdd_t); arrayForEachItem(mdd_t *, mddArray, i, mdd1) { if (result == NIL(mdd_t)) result = mdd_dup(mdd1); else { mdd2 = result; result = mdd_or(result, mdd1, 1, 1); mdd_free(mdd2); } } return (result); } /**Function******************************************************************** Synopsis [Utility function - joins two paths.] Description [Utility function - joins two paths. Note that the joins is done by adding the elements of the second array starting from the first element onwards.] SeeAlso [McCreateMergedPath] SideEffects [] ******************************************************************************/ array_t * McCreateJoinedPath( array_t *aPath, array_t *bPath) { int i; mdd_t *tmpState; array_t *aPathDup = McMddArrayDuplicateFAFW( aPath ); array_t *bPathDup = McMddArrayDuplicateFAFW( bPath ); for( i = 0 ; i < array_n( bPathDup ) ; i++ ) { tmpState = array_fetch( mdd_t *, bPathDup, i ); array_insert_last( mdd_t *, aPathDup, tmpState ); } array_free( bPathDup ); return aPathDup; } /**Function******************************************************************** Synopsis [ Check to see if aState lies in set of states satisfying aFormula ] SideEffects [] ******************************************************************************/ boolean McStateSatisfiesFormula( Ctlp_Formula_t *aFormula, mdd_t *aState ) { mdd_t *passStates = Ctlp_FormulaObtainLatestApprox( aFormula ); if ( mdd_lequal( aState, passStates, 1, 1 ) ) { mdd_free( passStates ); return TRUE; } else { mdd_free( passStates ); return FALSE; } } /**Function******************************************************************** Synopsis [ Tests aState is a member of setOfStates ] SideEffects [] ******************************************************************************/ boolean McStateTestMembership( mdd_t *aState, mdd_t *setOfStates ) { return mdd_lequal( aState, setOfStates, 1, 1 ); } /**Function******************************************************************** Synopsis [Obtain a successor of aState which is in targetStates] SideEffects [] ******************************************************************************/ mdd_t * McGetSuccessorInTarget( mdd_t *aState, mdd_t *targetStates, Fsm_Fsm_t *modelFsm ) { mdd_t *tmpMdd, *succsInTarget, *result; array_t *careSetArray = array_alloc(mdd_t *, 0); Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); array_insert_last(mdd_t *, careSetArray, targetStates); tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState, aState, careSetArray); array_free(careSetArray); succsInTarget = mdd_and(tmpMdd, targetStates, 1, 1); #if 1 result = Mc_ComputeAState(succsInTarget, modelFsm); #else result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm); #endif mdd_free( tmpMdd ); mdd_free( succsInTarget ); return result; } /**Function******************************************************************** Synopsis [Obtain a successor of aState which is in targetStates] SideEffects [] ******************************************************************************/ mdd_t * McGetSuccessorInTargetAmongFairStates( mdd_t *aState, mdd_t *targetStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm ) { mdd_t *tmpMdd, *succsInTarget, *result; mdd_t *fairStates, *newFairStates, *onionRing; mdd_t *targetStatesInFairStates; array_t *onionRings; int i, j; array_t *careSetArray = array_alloc(mdd_t *, 0); Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); fairStates = 0; for(i=0; istemArray; } /**Function******************************************************************** Synopsis [Obtain cycle of fair path] SideEffects [] ******************************************************************************/ array_t * McPathReadCycleArray( McPath_t *aPath ) { return aPath->cycleArray; } /**Function******************************************************************** Synopsis [Set stem of fair path] SideEffects [] ******************************************************************************/ void McPathSetStemArray( McPath_t *aPath, array_t *stemArray) { aPath->stemArray = stemArray; } /**Function******************************************************************** Synopsis [Set cycle of fair path] SideEffects [] ******************************************************************************/ void McPathSetCycleArray( McPath_t *aPath, array_t *cycleArray ) { aPath->cycleArray = cycleArray; } /**Function******************************************************************** Synopsis [Allocate a Path Struct] SideEffects [] ******************************************************************************/ McPath_t * McPathAlloc(void) { McPath_t *tmpPath = ( McPath_t * ) malloc( sizeof( McPath_t ) ); tmpPath->stemArray = NIL(array_t); tmpPath->cycleArray = NIL(array_t); return tmpPath; } /**Function******************************************************************** Synopsis [Free a Path Struct] SideEffects [] ******************************************************************************/ void McNormalizeBddPointer(array_t *bddArray) { int i; bdd_t *p; for(i=0; istemArray ) { McNormalizeBddPointer(aPath->stemArray); mdd_array_free( aPath->stemArray ); } if ( aPath->cycleArray ) { McNormalizeBddPointer(aPath->cycleArray); mdd_array_free( aPath->cycleArray ); } FREE( aPath ); } /**Function******************************************************************** Synopsis [Allocate an McOptions_t struct.] SideEffects [] ******************************************************************************/ McOptions_t * McOptionsAlloc(void) { McOptions_t *result = ALLOC(McOptions_t, 1); memset(result, 0, sizeof(McOptions_t)); result->useMore = FALSE; result->reduceFsm = FALSE; result->printInputs = FALSE; result->useFormulaTree = FALSE; result->simFormat = FALSE; result->ctlFile = NIL(FILE); result->guideFile = NIL(FILE); result->debugFile = NIL(FILE); result->fwdBwd = McFwd_c; result->dcLevel = McDcLevelNone_c; result->dbgLevel = McDbgLevelMin_c; result->schedule = McGSH_EL_c; result->lockstep = MC_LOCKSTEP_OFF; result->verbosityLevel = McVerbosityNone_c; result->timeOutPeriod = 0; result->ardcOptions = NIL(Fsm_ArdcOptions_t); result->invarApproxFlag = Fsm_Rch_Default_c; result->invarOnionRingsFlag = FALSE; result->traversalDirection = McBwd_c; result->doCoverageHoskote = FALSE; result->doCoverageImproved = FALSE; result->incre = TRUE; return result; } /**Function******************************************************************** Synopsis [Free an McOptions_t struct.] SideEffects [] ******************************************************************************/ void McOptionsFree( McOptions_t *options) { if (options->debugFile != NIL(FILE)){ fclose(options->debugFile); } if (options->ardcOptions != NIL(Fsm_ArdcOptions_t)){ FREE(options->ardcOptions); } FREE(options); } /**Function******************************************************************** Synopsis [Return Dbg level set at options.] SideEffects [] ******************************************************************************/ McDbgLevel McOptionsReadDbgLevel( McOptions_t *options ) { return options->dbgLevel; } /**Function******************************************************************** Synopsis [Return filepointer for guide file (NULL if guided search is disabled)] SideEffects [] ******************************************************************************/ FILE * McOptionsReadGuideFile( McOptions_t *options ) { return options->guideFile; } /**Function******************************************************************** Synopsis [Return filepointer for system variables file for FAFW ] SideEffects [] ******************************************************************************/ FILE * McOptionsReadSystemFile( McOptions_t *options ) { return options->systemFile; } /**Function******************************************************************** Synopsis [Return time out period set at options.] SideEffects [] ******************************************************************************/ int McOptionsReadTimeOutPeriod( McOptions_t *options ) { return options->timeOutPeriod; } /**Function******************************************************************** Synopsis [Return Verbosity level of options.] SideEffects [] ******************************************************************************/ Mc_VerbosityLevel McOptionsReadVerbosityLevel( McOptions_t *options ) { return options->verbosityLevel; } /**Function******************************************************************** Synopsis [Return the language emptiness checking method of options.] SideEffects [] ******************************************************************************/ Mc_LeMethod_t McOptionsReadLeMethod( McOptions_t *options ) { return options->leMethod; } /**Function******************************************************************** Synopsis [Return Dbg level of options.] SideEffects [] ******************************************************************************/ Mc_DcLevel McOptionsReadDcLevel( McOptions_t *options ) { return options->dcLevel; } /**Function******************************************************************** Synopsis [Return ctl file set at options.] SideEffects [] ******************************************************************************/ FILE * McOptionsReadCtlFile( McOptions_t *options ) { return options->ctlFile; } /**Function******************************************************************** Synopsis [Return debug file set at options.] SideEffects [] ******************************************************************************/ FILE * McOptionsReadDebugFile( McOptions_t *options ) { return options->debugFile; } /**Function******************************************************************** Synopsis [Read sim flag at options.] SideEffects [] ******************************************************************************/ int McOptionsReadSimValue( McOptions_t *options) { return options->simFormat; } /**Function******************************************************************** Synopsis [Read use more as pipe at options.] SideEffects [] ******************************************************************************/ int McOptionsReadUseMore( McOptions_t *options) { return options->useMore; } /**Function******************************************************************** Synopsis [Returns the value of Vacuity Detection option.] SideEffects [] ******************************************************************************/ boolean McOptionsReadVacuityDetect( McOptions_t *options) { return options->vd ; } /**Function******************************************************************** Synopsis [Returns the value of the option for the Beer method.] SideEffects [] ******************************************************************************/ int McOptionsReadBeerMethod( McOptions_t *options) { return options->beer ; } /**Function******************************************************************** Synopsis [Read use CTL formula specific reduction.] SideEffects [] ******************************************************************************/ int McOptionsReadReduceFsm( McOptions_t *options) { return options->reduceFsm; } /**Function******************************************************************** Synopsis [Read print inputs in debug trace.] SideEffects [] ******************************************************************************/ int McOptionsReadPrintInputs( McOptions_t *options) { return options->printInputs; } /**Function******************************************************************** Synopsis [Read use of CTL formula tree.] SideEffects [] ******************************************************************************/ boolean McOptionsReadUseFormulaTree( McOptions_t *options) { return options->useFormulaTree; } /**Function******************************************************************** Synopsis [Read schedule for GSH.] SideEffects [] ******************************************************************************/ Mc_GSHScheduleType McOptionsReadSchedule( McOptions_t *options) { return options->schedule; } /**Function******************************************************************** Synopsis [Read lockstep option.] SideEffects [] ******************************************************************************/ int McOptionsReadLockstep( McOptions_t *options) { return options->lockstep; } /**Function******************************************************************** Synopsis [Read reachability analysis type for check_invariant] SideEffects [] ******************************************************************************/ Fsm_RchType_t McOptionsReadInvarApproxFlag( McOptions_t *options) { return (options->invarApproxFlag); } /**Function******************************************************************** Synopsis [Read onion rings flag for check_invariant] SideEffects [] ******************************************************************************/ boolean McOptionsReadInvarOnionRingsFlag( McOptions_t *options) { return (options->invarOnionRingsFlag); } /**Function******************************************************************** Synopsis [Read whether to use forward or backward analysis] SideEffects [] ******************************************************************************/ Mc_FwdBwdAnalysis McOptionsReadFwdBwd( McOptions_t *options) { return options->fwdBwd; } /**Function******************************************************************** Synopsis [Read whether to use forward or backward traversal.] SideEffects [] ******************************************************************************/ Mc_FwdBwdAnalysis McOptionsReadTraversalDirection( McOptions_t *options) { return options->traversalDirection; } /**Function******************************************************************** Synopsis [Read ARDC options.] SideEffects [] ******************************************************************************/ Fsm_ArdcOptions_t * McOptionsReadArdcOptions( McOptions_t *options) { return options->ardcOptions; } /**Function******************************************************************** Synopsis [Read whether to do coverage computation using Hoskote et.al's algorithm] SideEffects [] ******************************************************************************/ int McOptionsReadCoverageHoskote( McOptions_t *options) { return options->doCoverageHoskote; } /**Function******************************************************************** Synopsis [Read whether to do coverage computation using the improved algorithm] SideEffects [] ******************************************************************************/ int McOptionsReadCoverageImproved( McOptions_t *options) { return options->doCoverageImproved; } /**Function******************************************************************** Synopsis [Set use forward or backward analysis] SideEffects [] ******************************************************************************/ void McOptionsSetFwdBwd( McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd ) { options->fwdBwd = fwdBwd; } /**Function******************************************************************** Synopsis [Set guided search file (set to NULL if no guided search)] SideEffects [] ******************************************************************************/ void McOptionsSetGuideFile( McOptions_t *options, FILE *guideFile ) { options->guideFile = guideFile; } /**Function******************************************************************** Synopsis [Set varibles for system file for FAFW] SideEffects [] ******************************************************************************/ void McOptionsSetVariablesForSystem( McOptions_t *options, FILE *systemFile ) { options->systemFile = systemFile; } /**Function******************************************************************** Synopsis [Set use forward or backward traversal] SideEffects [] ******************************************************************************/ void McOptionsSetTraversalDirection( McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd ) { options->traversalDirection = fwdBwd; } /**Function******************************************************************** Synopsis [Set use more pipe flag at options.] SideEffects [] ******************************************************************************/ void McOptionsSetUseMore( McOptions_t *options, boolean useMore ) { options->useMore = useMore; } /**Function******************************************************************** Synopsis [Set reduce fsm flag] SideEffects [] ******************************************************************************/ void McOptionsSetReduceFsm( McOptions_t *options, boolean reduceFsm ) { options->reduceFsm = reduceFsm; } /**Function******************************************************************** Synopsis [Set Vacuity Detect flag] SideEffects [] ******************************************************************************/ void McOptionsSetVacuityDetect( McOptions_t *options, boolean vd ) { options->vd = vd; } /**Function******************************************************************** Synopsis [Set Beer Method for vacuity detection flag] SideEffects [] ******************************************************************************/ void McOptionsSetBeerMethod( McOptions_t *options, boolean beer ) { options->beer = beer; } /**Function******************************************************************** Synopsis [Set flag for fate and free will algorithm] SideEffects [] ******************************************************************************/ void McOptionsSetFAFWFlag( McOptions_t *options, boolean FAFWFlag ) { options->FAFWFlag = FAFWFlag; } /**Function******************************************************************** Synopsis [Set print inputs flag] SideEffects [] ******************************************************************************/ void McOptionsSetPrintInputs( McOptions_t *options, boolean printInputs ) { options->printInputs = printInputs; } /**Function******************************************************************** Synopsis [Set use formula tree flag] SideEffects [] ******************************************************************************/ void McOptionsSetUseFormulaTree( McOptions_t *options, boolean useFormulaTree ) { options->useFormulaTree = useFormulaTree; } /**Function******************************************************************** Synopsis [Set GSH schedule] SideEffects [] ******************************************************************************/ void McOptionsSetSchedule( McOptions_t *options, Mc_GSHScheduleType schedule ) { options->schedule = schedule; } /**Function******************************************************************** Synopsis [Set lockstep option] SideEffects [] ******************************************************************************/ void McOptionsSetLockstep( McOptions_t *options, int lockstep ) { options->lockstep = lockstep; } /**Function******************************************************************** Synopsis [Set sim flag at options.] SideEffects [] ******************************************************************************/ void McOptionsSetSimValue( McOptions_t *options, boolean simValue ) { options->simFormat = simValue; } /**Function******************************************************************** Synopsis [Set Dbg level at options.] SideEffects [] ******************************************************************************/ void McOptionsSetDbgLevel( McOptions_t *options, McDbgLevel dbgLevel ) { options->dbgLevel = dbgLevel; } /**Function******************************************************************** Synopsis [Set Verbosity at options.] SideEffects [] ******************************************************************************/ void McOptionsSetVerbosityLevel( McOptions_t *options, Mc_VerbosityLevel verbosityLevel ) { options->verbosityLevel = verbosityLevel; } /**Function******************************************************************** Synopsis [Set language emptiness checking method at options.] SideEffects [] ******************************************************************************/ void McOptionsSetLeMethod( McOptions_t *options, Mc_LeMethod_t leMethod) { options->leMethod = leMethod; } /**Function******************************************************************** Synopsis [Set Dc level at options.] SideEffects [] ******************************************************************************/ void McOptionsSetDcLevel( McOptions_t *options, Mc_DcLevel dcLevel) { options->dcLevel = dcLevel; } /**Function******************************************************************** Synopsis [Set ARDC options.] SideEffects [] ******************************************************************************/ void McOptionsSetArdcOptions( McOptions_t *options, Fsm_ArdcOptions_t *ardcOptions) { options->ardcOptions = ardcOptions; } /**Function******************************************************************** Synopsis [Set a flag to store onion rings during invariant checking.] SideEffects [] ******************************************************************************/ void McOptionsSetInvarOnionRingsFlag( McOptions_t *options, int shellFlag) { if (shellFlag) options->invarOnionRingsFlag = TRUE; else options->invarOnionRingsFlag = FALSE; } /**Function******************************************************************** Synopsis [Set CTL File at options.] SideEffects [] ******************************************************************************/ void McOptionsSetCtlFile( McOptions_t *options, FILE *file) { options->ctlFile = file; } /**Function******************************************************************** Synopsis [Set Debug File at options.] SideEffects [] ******************************************************************************/ void McOptionsSetDebugFile( McOptions_t *options, FILE *file) { options->debugFile = file; } /**Function******************************************************************** Synopsis [Set ime out periopd at options.] SideEffects [] ******************************************************************************/ void McOptionsSetTimeOutPeriod( McOptions_t *options, int timeOutPeriod) { options->timeOutPeriod = timeOutPeriod; } /**Function******************************************************************** Synopsis [Set reachability analysis type] SideEffects [] ******************************************************************************/ void McOptionsSetInvarApproxFlag( McOptions_t *options, Fsm_RchType_t approxFlag) { options->invarApproxFlag = approxFlag; } /**Function******************************************************************** Synopsis [Set do Coverage-Hoskote flag] SideEffects [] ******************************************************************************/ void McOptionsSetCoverageHoskote( McOptions_t *options, boolean doCoverageHoskote ) { options->doCoverageHoskote = doCoverageHoskote; } /**Function******************************************************************** Synopsis [Set do Coverage-Improved flag] SideEffects [] ******************************************************************************/ void McOptionsSetCoverageImproved( McOptions_t *options, boolean doCoverageImproved ) { options->doCoverageImproved = doCoverageImproved; } /**Function******************************************************************** Synopsis [Query user to continue.] SideEffects [] ******************************************************************************/ boolean McQueryContinue(char *query) { char result[2]; fprintf(vis_stdout, "%s", query); if (fgets(result, 2, stdin) == NULL) return FALSE; if(!strcmp(result,"1")) return TRUE; else if(!strcmp(result,"0")) return FALSE; else { fprintf(vis_stdout, "-- Must enter 0/1\n"); return McQueryContinue(query); } } /**Function******************************************************************** Synopsis [Print Support of Function] SideEffects [] ******************************************************************************/ void McPrintSupport( mdd_t *aMdd, mdd_manager *mddMgr, Ntk_Network_t *aNetwork ) { int i; char *tmp1String, *tmp2String; char *mintermString = NIL(char); char bodyString[McMaxStringLength_c]; array_t *aSupport = mdd_get_support( mddMgr, aMdd ); array_t *stringArray = array_alloc( char *, 0 ); for ( i = 0 ; i < array_n( aSupport ); i++ ) { int mddId = array_fetch( int, aSupport, i ); Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId ); char *nodeName = Ntk_NodeReadName( node ); sprintf( bodyString, "%s", nodeName ); tmp1String = util_strsav( bodyString ); array_insert_last( char *, stringArray, tmp1String ); } array_sort( stringArray, cmp); for ( i = 0 ; i < array_n( stringArray ); i++ ) { tmp1String = array_fetch( char *, stringArray, i ); if( i == 0 ) { mintermString = util_strcat3(tmp1String, "", "" ); } else { tmp2String = util_strcat3(mintermString, "\n", tmp1String ); FREE(mintermString); mintermString = tmp2String; } FREE(tmp1String); } fprintf(vis_stdout, "%s\n", mintermString ); } /**Function******************************************************************** Synopsis [Print path as sim trace] SideEffects [] ******************************************************************************/ int McPrintSimPath( FILE *outputFile, array_t *aPath, Fsm_Fsm_t *modelFsm) { int i; array_t *inputVars = Fsm_FsmReadInputVars( modelFsm ); array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm ); Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm ); mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); array_t *inputSortedVars = SortMddIds( inputVars, network ); array_t *psSortedVars = SortMddIds( psVars, network ); fprintf(outputFile, "# UC Berkeley, VIS Release 1.3\n"); fprintf(outputFile, "# Network: %s\n", Ntk_NetworkReadName( network ) ); fprintf(outputFile, "# Simulation vectors have been generated to show language non-empty\n\n"); fprintf( outputFile, ".inputs " ); PrintNodes( inputSortedVars, network ); fprintf( outputFile, "\n" ); fprintf( outputFile, ".latches " ); PrintNodes( psSortedVars, network ); fprintf( outputFile, "\n" ); fprintf( outputFile, ".outputs\n" ); for( i = -1 ; i < (array_n( aPath ) - 1); i++ ) { if ( i == -1 ) { mdd_t *initState = array_fetch( mdd_t *, aPath, (i+1) ); array_t *initValues = McConvertMintermToValueArray( initState, psSortedVars, mddMgr ); fprintf( outputFile, ".initial "); PrintDeck( initValues, psSortedVars, network ); array_free( initValues ); fprintf( outputFile, "\n" ); fprintf( outputFile, ".start_vectors\n"); } else { array_t *psValues; array_t *nsValues; array_t *inputValues; mdd_t *psState = array_fetch( mdd_t *, aPath, i ); mdd_t *nsState = array_fetch( mdd_t *, aPath, (i+1) ); mdd_t *inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, psState, nsState ); mdd_t *input = Mc_ComputeAMinterm( inputSet, inputVars, mddMgr ); inputValues = McConvertMintermToValueArray( input, inputSortedVars, mddMgr ); PrintDeck( inputValues, inputSortedVars, network ); array_free( inputValues ); fprintf( outputFile, " ;"); psValues = McConvertMintermToValueArray( psState, psSortedVars, mddMgr ); PrintDeck( psValues, psSortedVars, network ); array_free( psValues ); fprintf( outputFile, " ;"); nsValues = McConvertMintermToValueArray( nsState, psSortedVars, mddMgr ); PrintDeck( nsValues, psSortedVars, network ); array_free( nsValues ); fprintf( outputFile, " ;\n"); mdd_free( inputSet ); mdd_free( input ); } } array_free( psSortedVars ); array_free( inputSortedVars ); return 1; } /**Function******************************************************************** Synopsis [Form an FSM reduced with respect to the specified formula] Description [Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.] SideEffects [] ******************************************************************************/ Fsm_Fsm_t * McConstructReducedFsm( Ntk_Network_t *network, array_t *ctlFormulaArray ) { int i; Ntk_Node_t *node; array_t *nodeArray; st_table *formulaNodes; Ctlp_Formula_t *fairnessCondition; Ctlp_Formula_t *ctlFormula; array_t *formulaCombNodes; Fsm_Fsm_t *netFsm = Fsm_NetworkReadFsm( network ); Fsm_Fsm_t *reducedFsm; Fsm_Fairness_t *netFairness = Fsm_FsmReadFairnessConstraint( netFsm ); array_t *reducedFsmFairness = array_alloc( Ctlp_Formula_t *, 0 ); if (netFairness) { if ( !Fsm_FairnessTestIsBuchi( netFairness ) ) { (void) fprintf(vis_stderr, "** mc error: non Buchi fairness constraints not supported\n"); (void) fprintf(vis_stderr, "** mc error: ignoring fairness constraints\n"); } else { int j; int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( netFairness, 0 ); for( j = 0 ; j < numBuchi; j++ ) { Ctlp_Formula_t *tmpFormula = Fsm_FairnessReadFinallyInfFormula( netFairness, 0, j ); Ctlp_Formula_t *reducedFsmCondition = Ctlp_FormulaDup( tmpFormula ); array_insert_last( Ctlp_Formula_t *, reducedFsmFairness, reducedFsmCondition ); } } } formulaNodes = st_init_table( st_ptrcmp, st_ptrhash ); arrayForEachItem( Ctlp_Formula_t *, ctlFormulaArray, i, ctlFormula ) { NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes ); } arrayForEachItem( Ctlp_Formula_t *, reducedFsmFairness, i, fairnessCondition ) { NodeTableAddCtlFormulaNodes( network, fairnessCondition, formulaNodes ); } { st_generator *stGen; nodeArray = array_alloc( Ntk_Node_t *, 0 ); st_foreach_item( formulaNodes, stGen, &node, NIL(char *) ) { array_insert_last( Ntk_Node_t *, nodeArray, node ); } } st_free_table( formulaNodes ); formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network, nodeArray, FALSE ); array_free( nodeArray ); if(array_n(formulaCombNodes) == 0) { /* Free the fairness constraint array (if any) */ for (i=0; i For negation, ALL becomes SOME and vice versa, while CARE is passed unchanged.

For conjunction, disjunction, and implication: if the current node has a termination condition of type ALL or SOME, this is refined and propagated. Otherwise, the returned early termination condition is of type CARE. The care states are the conjunction of earlyTermination->states and either careStates (for conjunction and implication) or the complement of careStates (for disjunction).

In some cases, one can immediately determine that the goal cannot be reached, or has already been reached. In these cases, the termination condition has mode=CARE and states=mdd_zero.

The other types of formulae produce no early termination condition for their children. That is, they declare that all states are care states.] SideEffects [] ******************************************************************************/ Mc_EarlyTermination_t * McObtainUpdatedEarlyTerminationCondition( Mc_EarlyTermination_t *earlyTermination, mdd_t *careStates, Ctlp_FormulaType formulaType) { Mc_EarlyTermination_t *result; switch (formulaType) { case Ctlp_NOT_c: if (earlyTermination == MC_NO_EARLY_TERMINATION) return MC_NO_EARLY_TERMINATION; result = Mc_EarlyTerminationAlloc(earlyTermination->mode, earlyTermination->states); switch (result->mode) { case McAll_c: result->mode = McSome_c; break; case McSome_c: result->mode = McAll_c; break; case McCare_c: break; default: assert(0); } break; case Ctlp_AND_c: if (careStates == NIL(mdd_t)) { if (earlyTermination == MC_NO_EARLY_TERMINATION) { result = MC_NO_EARLY_TERMINATION; } else if (earlyTermination->mode == McAll_c) { result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states); } else { /* Here mode is CARE or SOME: inherit care states from parent. */ result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states); } } else { /* There are care states from sibling. */ if (earlyTermination == MC_NO_EARLY_TERMINATION) { /* No early termination from parent: just use sibling's care states. */ result = Mc_EarlyTerminationAlloc(McCare_c, careStates); } else if (earlyTermination->mode == McAll_c) { /* If some goal states are not in care set, we know we cannot achieve * the goal; otherwise, we just propagate the parent's condition. */ if (mdd_lequal(earlyTermination->states, careStates, 1, 1)) { result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states); } else { result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */ } } else if (earlyTermination->mode == McSome_c) { /* If no goal states are in the care set, we have failed; otherwise * we refine the goal set to those states also in the care set. */ if (mdd_lequal(earlyTermination->states, careStates, 1, 0)) { result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */ } else { mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1); result = Mc_EarlyTerminationAlloc(McSome_c, andMdd); mdd_free(andMdd); } } else { /* if (earlyTermination->mode == McCare_c) */ /* Intersect care states from parent and sibling. */ mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1); result = Mc_EarlyTerminationAlloc(McCare_c, andMdd); mdd_free(andMdd); } } break; case Ctlp_THEN_c: case Ctlp_OR_c: if (careStates == NIL(mdd_t)) { if (earlyTermination == MC_NO_EARLY_TERMINATION) { result = MC_NO_EARLY_TERMINATION; } else if (earlyTermination->mode == McSome_c) { if (formulaType == Ctlp_OR_c) { result = Mc_EarlyTerminationAlloc(McSome_c, earlyTermination->states); } else { result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states); } } else { /* Here mode is CARE or ALL: inherit care states from parent. */ result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states); } } else { /* There are care states from sibling. * Since f->g is !f+g, we treat the THEN and OR cases together by * complementing the care set in the latter case. */ mdd_t *mask = (formulaType == Ctlp_OR_c) ? bdd_not(careStates) : bdd_dup(careStates); if (earlyTermination == MC_NO_EARLY_TERMINATION) { /* No early termination from parent: just use sibling's care states. */ result = Mc_EarlyTerminationAlloc(McCare_c, mask); } else if (earlyTermination->mode == McAll_c) { /* Remove the goal states already attained from the goal set. */ mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1); result = Mc_EarlyTerminationAlloc(McAll_c, andMdd); mdd_free(andMdd); } else if (earlyTermination->mode == McSome_c) { /* If some goal states were already attained, declare success; * otherwise just propagate the parent's condition. */ if (mdd_lequal(earlyTermination->states, mask, 1, 1)) { result = Mc_EarlyTerminationAlloc(McSome_c, earlyTermination->states); } else { result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* success */ } } else { /* if (earlyTermination->mode == McCare_c) */ /* Intersect care states from parent and sibling. */ mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1); result = Mc_EarlyTerminationAlloc(McCare_c, andMdd); mdd_free(andMdd); } mdd_free(mask); } break; default: result = MC_NO_EARLY_TERMINATION; } return result; } /* McObtainUpdatedEarlyTerminationCondition */ /**Function******************************************************************** Synopsis [Check if an underapproximation of the evaluation guarantees that the early termination conditions hold.] Description [Check if an underapproximation of the evaluation guarantees that the early termination conditions hold , modulo a care set modeled by an implicitly conjoined array of bdds. If we are looking for ALL of ETstates, or we are are given a set of CARE states, then we are done if ETstates \subseteq underapprox, because that implies ETstates \subseteq exactset. If we are looking for SOME of ETstates, we are done if underapprox and ETstates overlap, because that means that the exact set and ETstates also overlap. If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the function is false.] SideEffects [] ******************************************************************************/ boolean McCheckEarlyTerminationForUnderapprox( Mc_EarlyTermination_t *earlyTermination, mdd_t *underApprox, array_t *careStatesArray) { if(earlyTermination == MC_NO_EARLY_TERMINATION) return FALSE; /* for an underapproximation and McAll_c (McSome_c), you just check whether all states (some states) are already reached */ return(((earlyTermination->mode != McSome_c) && (mdd_lequal_mod_care_set_array(earlyTermination->states, underApprox, 1, 1, careStatesArray))) || ( (earlyTermination->mode == McSome_c) && (!mdd_lequal_mod_care_set_array(underApprox, earlyTermination->states, 1, 0, careStatesArray)))); } /**Function******************************************************************** Synopsis [Check if an overapproximation of the evaluation guarantees that the early termination conditions hold.] Description [Check if an overapproximation of the evaluation guarantees that the early termination conditions hold, modulo a care set modeled by an implicitly conjoined array of bdds. If we are looking for ALL of ETstates, then we are done if we have overapprox is not a superset of ETstates, because the exact set will not hold all of ETstates. If we are looking for SOME of ETstates, or we are given a set of CARE states, we are done if overapprox is disjoint from ETstates, because that means that the exact set is also disjoint from ETstates. If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the function is false.] SideEffects [] ******************************************************************************/ boolean McCheckEarlyTerminationForOverapprox( Mc_EarlyTermination_t *earlyTermination, mdd_t *overApprox, array_t *careStatesArray) { if(earlyTermination == MC_NO_EARLY_TERMINATION) return FALSE; /* For an overapproximation and McAll_c (McSome_c), you check whether some state (all states) are already missing */ return(((earlyTermination->mode == McAll_c) && (!mdd_lequal_mod_care_set_array(earlyTermination->states, overApprox, 1, 1, careStatesArray))) || ((earlyTermination->mode != McAll_c) && (mdd_lequal_mod_care_set_array(earlyTermination->states, overApprox, 1, 0, careStatesArray)))); } /**Function******************************************************************** Synopsis [Return an array of formulae representing the hints] Description [Read the guide file and store the hint formulae in an array. Adds the 1 hint to the end of the array. Returns NIL if something goes wrong: parse error in the file or temporal operators in the hints] SideEffects [] ******************************************************************************/ array_t * Mc_ReadHints( FILE *guideFP ) { Ctlp_FormulaArray_t *invarArray; /* formulae representing hints */ int i; /* to iterate over formulae */ Ctlp_Formula_t *formula; /* idem */ if (guideFP == NIL(FILE)){ fprintf(vis_stderr, "** mc error: can't read hint file.\n"); return NIL(array_t); } invarArray = Ctlp_FileParseFormulaArray( guideFP ); if (invarArray == NIL(array_t)){ fprintf(vis_stderr, "** mc error: parse error in hints file.\n"); return NIL(array_t); } if (array_n(invarArray) == 0){ fprintf(vis_stdout, "** mc error: File contained no hints.\n"); Ctlp_FormulaArrayFree(invarArray); return NIL(array_t); } array_insert_last(Ctlp_Formula_t *, invarArray, Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void))); /* some checks */ arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){ if(!Ctlp_FormulaTestIsQuantifierFree(formula)){ (void) fprintf(vis_stdout, "** mc error: Hints contain temporal operators\n"); Ctlp_FormulaArrayFree(invarArray); return NIL(array_t); } /* quantifier free */ }/* checks */ return invarArray; }/* Mc_ReadHints */ /**Function******************************************************************** Synopsis [Return an array of variables controlled by system ] Description [Read the system variables file and store the variables controlled by system in an array. Returns NIL if something goes wrong: parse error in the file or variables that are not contained in model.] SideEffects [] ******************************************************************************/ st_table * Mc_ReadSystemVariablesFAFW( Fsm_Fsm_t *fsm, FILE *systemFP ) { st_table *variablesTable; array_t *bddIdArray; char line[1024], nodeName[1024], *next; int mddId, bddId; int i, j, len, index; int errorFlag; Ntk_Node_t *node; Ntk_Network_t *network; mdd_manager *mgr; errorFlag = 0; if (systemFP == NIL(FILE)){ fprintf(vis_stderr, "** mc error: can't read system file.\n"); return NIL(st_table); } network = Fsm_FsmReadNetwork(fsm); mgr = Fsm_FsmReadMddManager(fsm); variablesTable = st_init_table(st_numcmp, st_numhash); while(fgets(line, 1024, systemFP)) { len = strlen(line); for(i=0; inum_entries == 0) { st_free_table(variablesTable); variablesTable = 0; } if(errorFlag) { if(variablesTable) st_free_table(variablesTable); variablesTable = 0; return((st_table *)-1); } return variablesTable; }/* Mc_ReadSystemVariablesFAFW */ /**Function******************************************************************** Synopsis [] Description [] SideEffects [] ******************************************************************************/ st_table * Mc_SetAllInputToSystem(Fsm_Fsm_t *fsm) { mdd_manager *mgr; array_t *inputVars, *bddIdArray; int i, j; int mddId, bddId; st_table *idTable; idTable = st_init_table(st_numcmp, st_numhash); mgr = Fsm_FsmReadMddManager(fsm); /* inputVars = Fsm_FsmReadPrimaryInputVars(fsm); */ inputVars = Fsm_FsmReadInputVars(fsm); if(inputVars) { for(i=0; i 0) { fprintf(vis_stdout, "GS warning ** Quantifying out variables not relevant to the reduced FSM in hint %d. \n", i+1); arrayForEachItem(int, leftOverVars, j, mddId) { fprintf(vis_stdout, "%s\n", (mdd_get_var_by_id(mddMgr, mddId)).name); } temp = mdd_smooth(mddMgr, invarFormulaStates, leftOverVars); mdd_free(invarFormulaStates); invarFormulaStates = temp; } array_free(leftOverVars); st_free_table(supportTable); array_free(supportArray); } array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates); }/* for each formula */ array_free(psInputVars); mdd_free(one); return invarStatesArray; }/* Mc_EvaluateHints */ /**Function******************************************************************** Synopsis [Return an array of hints] Description [Read the guide file and compute the BDDs of the hints and store in an array. Adds the 1 hint to the end of the array. Closes the guideFP. Returns NIL if something goes wrong.] SideEffects [] ******************************************************************************/ array_t * Mc_ComputeGuideArray( Fsm_Fsm_t *fsm, FILE *guideFP ) { Ctlp_FormulaArray_t *hintFormulae; array_t * hintSets; hintFormulae = Mc_ReadHints(guideFP); fclose(guideFP); if( hintFormulae == NIL(Ctlp_FormulaArray_t)) return NIL(array_t); hintSets = Mc_EvaluateHints(fsm, hintFormulae); Ctlp_FormulaArrayFree(hintFormulae); return hintSets; }/* Mc_ComputeGuideArray */ /**Function******************************************************************** Synopsis [Read and parse the hints_type set flag] Description [Read and parse the hints_type set flag. If it is not set return the default: local. Return Mc_None_c if there is an error.] SideEffects [] ******************************************************************************/ Mc_GuidedSearch_t Mc_ReadGuidedSearchType(void) { char *string = Cmd_FlagReadByName("guided_search_hint_type"); if(string == NIL(char)) /* default */ return Mc_Local_c; if(!strcmp(string, "global")) return Mc_Global_c; if(!strcmp(string, "local")) return Mc_Local_c; else return Mc_None_c; } /**Function******************************************************************** Synopsis [Debug function to check if there exists a proper input value] Description [Check the existence of path by extracting input condition.] SideEffects [] ******************************************************************************/ void Mc_CheckPathToCore(Fsm_Fsm_t *fsm, array_t *pathToCore) { array_t *inputVars; int i; mdd_t *fromState, *toState, *inputSet; mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm)); inputVars = Fsm_FsmReadInputVars( fsm ); for(i=-1; i0; i--) { fromState = (i==array_n(pathFromCore)) ? 0 : array_fetch(mdd_t *, pathFromCore, i); toState = array_fetch(mdd_t *, pathFromCore, i-1); if((long)fromState % 2) fromState = (mdd_t *)((long)fromState - 1); if((long)toState % 2) toState = (mdd_t *)((long)toState - 1); inputSet = ( i == array_n(pathFromCore)) ? 0 : Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState ); if(inputSet) Mc_ComputeAMinterm( inputSet, inputVars, mgr ); else if(i != array_n(pathFromCore)) fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1); } } /**Function******************************************************************** Synopsis [Print states in terms of state variables] Description [Print states in terms of state variables] SideEffects [] ******************************************************************************/ void Mc_PrintStates( Fsm_Fsm_t *modelFsm, mdd_t *states) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm ); mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); mdd_t *zeroMdd, *new_states; char *tmpString; double size; /* * sometimes, this function will be constrained by number of minterm * in the given set of states. * num_minterm = mdd_num_of_mintern(states); * if(num_minterm > MAX_MINTERM) { * fprintf( stdout, "Too many minterms in given states\n" ); * return; * } */ if((long)states % 2) { states = (mdd_t *)((long)states - 1); } zeroMdd = mdd_zero( mddMgr ); states = mdd_dup(states); if(mdd_equal(states, zeroMdd)) { fprintf(stdout, "ZERO mdd\n"); mdd_free(zeroMdd); return; } size = mdd_count_onset(mddMgr, states, PSVars); if(size > 40.0) { fprintf(stdout, "Too many minterms in given states %.0f\n", size); return; } fprintf( stdout, " " ); while(1) { mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr ); new_states = mdd_and( states, result, 1, 0 ); mdd_free( states ); states = new_states; tmpString = Mc_MintermToString( result, PSVars, aNetwork ); fprintf( stdout, "%s ", tmpString ); FREE(tmpString); mdd_free( result ); if(mdd_equal(states, zeroMdd)) { mdd_free(zeroMdd); mdd_free(states); break; } } fprintf(stdout, "\n"); } /**Function******************************************************************** Synopsis [Print the number of states] Description [Print the number of states.] SideEffects [] ******************************************************************************/ void Mc_PrintNumStates( Fsm_Fsm_t *modelFsm, mdd_t *states) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm ); mdd_t *zeroMdd; double size; /* * sometimes, this function will be constrained by number of minterm * in the given set of states. * num_minterm = mdd_num_of_mintern(states); * if(num_minterm > MAX_MINTERM) { * fprintf( stdout, "Too many minterms in given states\n" ); * return; * } */ if((long)states % 2) { states = (mdd_t *)((long)states - 1); } zeroMdd = mdd_zero( mddMgr ); states = mdd_dup(states); if(mdd_equal(states, zeroMdd)) { fprintf(stdout, "ZERO mdd\n"); mdd_free(zeroMdd); mdd_free(states); return; } size = mdd_count_onset(mddMgr, states, PSVars); fprintf(stdout, "num states : %.0f\n", size); mdd_free(zeroMdd); mdd_free(states); } /**Function******************************************************************** Synopsis [Print the states of each ring] Description [Print the states of each ring] SideEffects [] ******************************************************************************/ void Mc_PrintRings( Fsm_Fsm_t *modelFsm, array_t *onionRings) { int j; mdd_t *innerRing; if(array_n(onionRings) > 0) { for(j=0; j 0) { for(j=0; j