/**CFile*********************************************************************** FileName [Robust.c] PackageName [rob] Synopsis [Functions for Robustness computation.] Author [Souheib baarir, Denis poitrenaud, J.M. Ilié] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Paris VI. 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 PARIS VI 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 #include "Robust.h" #define mymddGetVarById( mgr, id ) \ array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id)) void conv_error_msg(FILE* f, char* cmd, type_err e){ switch(e){ case eofile :fprintf(f,cmd); fprintf(f," error :"); fprintf(f," the output file cannot be read \n"); break; case ecmd :fprintf(f,cmd); fprintf(f," error :"); fprintf(f," the mdd is not set \n"); break; case earg :fprintf(f,cmd);fprintf(f," error : too many arguments\n"); fprintf(f,"usage: %s \" ltl_formula \" \n",cmd); break; } } void error_msg(FILE* f, char* cmd, type_err e){ switch(e){ case ecmd : fprintf(f,"usage: set_"), fprintf(f, cmd); fprintf(f," [-h] file\n"); fprintf(f," -h : print the command usage\n"); fprintf(f," file: file file containing the ctl formula\n"); break; case eofile :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error :"); fprintf(f,cmd); fprintf(f," ctl definition file cannot be read. Check permissions and path\n "); break; case earg :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error : too many arguments\n"); break; case enfile :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error :"); fprintf(f,cmd); fprintf(f," ctl definition file not provided\n");break; case eicmd : fprintf(f,"usage : set_init [-h] [-s #] [-v #] [[-m fmodel] [-g file] | -f file] \n"); fprintf(f," -h : print the command usage\n"); fprintf(f," -s # : print reachability information every printStep steps (0 for no information).\n"); fprintf(f," -v # : verbosity level\n"); fprintf(f," -m fmodel : precises the fault model, where fmodel can be one of the following : \n"); fprintf(f," usut : a single fault on a single time unit \n"); fprintf(f," usmt : a single fault on multiple time units \n"); fprintf(f," msut : multiple falts on a sigle time unit \n"); fprintf(f," msmt : multiple falts on a multiple time units \n"); fprintf(f," -g file : compute the set of initial errors states with respect to a sequential elements protection, given in file\n"); fprintf(f," -f file : compute the set of initial errors states with respect to a ctl formula given in file\n"); break; case eiofile : fprintf(f,"set_init error : Protected/Formula definition file cannot be read. Check permissions and path\n "); break; case ercmd : fprintf(f,"usage : robustness [-h] [-s #] [-v #] [-r #]\n"); fprintf(f," -h : print the command usage\n"); fprintf(f," -s # : print reachability information every printStep steps (0 for no information).\n"); fprintf(f," -v # : verbosity level\n"); fprintf(f," -r # : robustness type 1 = rob1 default rob4\n"); break; } } void get_number_of_states(Fsm_Fsm_t *fsm, mdd_t* b, EpDouble* ep) { array_t *psVarsArray; int nvars; mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); psVarsArray = Fsm_FsmReadPresentStateVars(fsm); nvars = ComputeNumberOfBinaryStateVariables(mddManager, psVarsArray); if (nvars <= EPD_MAX_BIN) { EpdConvert(mdd_count_onset(mddManager, b, psVarsArray),ep); } else { mdd_epd_count_onset(mddManager, b, psVarsArray, ep); } } void print_number_of_states(char* msg, Fsm_Fsm_t *fsm, mdd_t* b) { EpDouble *ep = EpdAlloc(); get_number_of_states(fsm, b, ep); char buff[1024]; EpdGetString(ep, buff); EpdFree(ep); (void) fprintf(vis_stdout, "%-50s%15s\n", msg, buff); } array_t * determine_non_protected_registers(Fsm_Fsm_t *fsm, FILE *f) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *wordArray = array_alloc(char*, 0); array_t *nonProtectedIdArray = array_alloc(int, 0); array_t *psVarsArray = Fsm_FsmReadPresentStateVars(fsm); int arrSize = array_n( psVarsArray ); int i, j; char word[1024]; if (!f) { (void) fprintf(vis_stdout, "no register is protected \n"); // return nonProtectedIdArray; } else{ fscanf(f, "%1023s", word); while (!feof(f)) { char *buff = (char*)malloc(strlen(word) + 1); strcpy(buff, word); array_insert_last(char*, wordArray, buff); fscanf(f, "%1023s", word); } fclose(f); } // construction du vecteur des registres non protégés for ( i = 0 ; i < arrSize ; i++ ) { int mddId = array_fetch( int, psVarsArray, i ); mvar_type mVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager),mddId); int protect = 0, j; for ( j = 0 ; j < array_n( wordArray ) ; j++ ) { char* w = array_fetch( char*, wordArray, j ); int l = strlen(w); //printf("%s \n",w); if (l > 0 && w[l-1] == '*') { if (strncmp(mVar.name, w, l-1) == 0) { protect = 1; break; } } else if (strcmp(mVar.name, w) == 0) { protect = 1; break; } } (void) fprintf(vis_stdout, "%-20s%10d", mVar.name, mVar.values); if (protect) { (void) fprintf(vis_stdout, " protected\n"); } else { array_insert_last(int, nonProtectedIdArray, mddId); (void) fprintf(vis_stdout, " not protected\n"); if (mVar.values > 2) (void) fprintf(vis_stdout, "WARNING : the variable %s seems to be a control state (of %d values) and not a register\n", mVar.name, mVar.values); } } for ( i = 0 ; i < array_n( wordArray ) ; i++ ) free(array_fetch( char*, wordArray, i )); array_free(wordArray); return nonProtectedIdArray; } mdd_t* compute_error_states(Fsm_Fsm_t *fsm, mdd_t* reachable, int verbosityLevel, int printStep, FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray; mdd_t *prec, *tmp1, *tmp2, *res, *reach, *old; int numit = 0, arrSize; // construction du vecteur des registres non protégés nonProtectedIdArray = determine_non_protected_registers(fsm,protect); if (array_n(nonProtectedIdArray) == array_n( Fsm_FsmReadPresentStateVars(fsm) )) { // All the registers are unprotected return mdd_one(mddManager); } // calcul des états d'erreur old = fsm->reachabilityInfo.initialStates; reach = mdd_dup(reachable); prec = mdd_zero(mddManager); while (1) { numit++; if(verbosityLevel > 1){ (void) fprintf(vis_stdout, "iteration number: %15d\n", numit); print_number_of_states("known error states = ", fsm, prec); } tmp1 = mdd_smooth(mddManager, reach, nonProtectedIdArray); mdd_free(reach); res = mdd_or(tmp1, prec, 1, 1); mdd_free(tmp1); if (mdd_lequal(res, prec, 1, 1)) { if(verbosityLevel > 1) (void) fprintf(vis_stdout, "number of iterations: %15d\n", numit); mdd_free(prec); array_free(nonProtectedIdArray); fsm->reachabilityInfo.initialStates = old; return res; } mdd_free(prec);prec = res; fsm->reachabilityInfo.initialStates = mdd_dup(res); reach = Fsm_FsmComputeReachableStates( fsm, 0, verbosityLevel, printStep, 0, 0, 0, 0, Fsm_Rch_Default_c, 0, 1, NIL(array_t), 0, NIL(array_t)); mdd_free(fsm->reachabilityInfo.initialStates); } (void) fprintf(vis_stdout, "Oups, erreur grave\n"); assert(0); return res; } mdd_t* error_states(Fsm_Fsm_t *fsm, mdd_t* reachable, array_t *nonProtectedIdArray) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); mdd_t *prec, *tmp1, *tmp2, *res, *reach, *old; int numit = 0, arrSize; if (array_n(nonProtectedIdArray) == array_n( Fsm_FsmReadPresentStateVars(fsm) )) { // All the registers are unprotected return mdd_one(mddManager); } // calcul des états d'erreur old = fsm->reachabilityInfo.initialStates; reach = mdd_dup(reachable); prec = mdd_zero(mddManager); while (1) { tmp1 = mdd_smooth(mddManager, reach, nonProtectedIdArray); mdd_free(reach); res = mdd_or(tmp1, prec, 1, 1); mdd_free(tmp1); if (mdd_lequal(res, prec, 1, 1)) { mdd_free(prec); fsm->reachabilityInfo.initialStates = old; return res; } mdd_free(prec);prec = res; fsm->reachabilityInfo.initialStates = mdd_dup(res); reach = Fsm_FsmComputeReachableStates( fsm, 0, 0, 0, 0, 0, 0, 0, Fsm_Rch_Default_c, 0, 1, NIL(array_t), 0, NIL(array_t)); mdd_free(fsm->reachabilityInfo.initialStates); } return res; } static array_t * getbddvars( mdd_manager *mgr, array_t *mvars) { array_t *bdd_vars = array_alloc(bdd_t *, 0); int i, j, mv_no; mvar_type mv; mdd_t *top; bdd_t *temp; array_t *mvar_list = mdd_ret_mvar_list(mgr); if ( mvars == NIL(array_t) || array_n(mvars) == 0) { printf("\nWARNING: Empty Array of MDD Variables\n"); return bdd_vars; } for (i=0; inode,d->node); if (tmp== DD_ONE((DdManager *)mgr) ) { return mdd_one(mgr); } if (tmp==Cudd_Not(DD_ONE((DdManager *)mgr))) { return mdd_zero(mgr); } cuddRef(tmp); return bdd_construct_bdd_t(mgr,tmp); } // injection effective d'une erreur dans le registre r à partir des états de S // return $S_{\left|r} \wedge \neg r \vee S_{\left|\neg r} \wedge r$ static mdd_t* inj_register(mdd_manager *mddManager, mdd_t* S, mdd_t* r) { mdd_t *tmp1, *tmp2, *res; tmp1 = mdd_restrict(mddManager, S, r); tmp2 = mdd_and(tmp1, r, 1, 0); mdd_free(tmp1); res = tmp2; tmp2 = bdd_not(r); tmp1 = mdd_restrict(mddManager, S, tmp2); mdd_free(tmp2); tmp2 = mdd_and(tmp1, r, 1, 1); mdd_free(tmp1); tmp1 = mdd_or(res, tmp2, 1, 1); mdd_free(res); mdd_free(tmp2); return tmp1; } // injection effective d'une erreur unique dans un des registres non protégés mdd_t* inj_us(mdd_manager *mddManager, array_t* bdd_not_protected, mdd_t* S) { int arrSize, i; mdd_t *tmp1, *tmp2, *v, *res; res = mdd_zero(mddManager); arrSize = array_n(bdd_not_protected); for ( i = 0 ; i < arrSize ; i++ ) { v = array_fetch(bdd_t *, bdd_not_protected, i); tmp1 = inj_register(mddManager, S, v); tmp2 = mdd_or(res, tmp1, 1, 1); mdd_free(res); mdd_free(tmp1); res = tmp2; } return res; } // injection effective d'erreurs multiples // dans au moins un des registres non protégés mdd_t* inj_ms(mdd_manager *mddManager, array_t* bdd_not_protected, mdd_t* S) { int arrSize, i; mdd_t *tmp1, *tmp2, *v, *res; array_t* bdd_vars; res = mdd_zero(mddManager); arrSize = array_n(bdd_not_protected); for ( i = 0 ; i < arrSize ; i++ ) { v = array_fetch(bdd_t *, bdd_not_protected, i); tmp1 = inj_register(mddManager, S, v); bdd_vars = array_partial_dup(bdd_not_protected, i) ; tmp2 = bdd_smooth(tmp1, bdd_vars); mdd_free(tmp1); tmp1 = mdd_or(res, tmp2, 1, 1); mdd_free(res); mdd_free(tmp2); array_free(bdd_vars); res = tmp1; } return res; } /* mdd_t* error_states_us(Fsm_Fsm_t *fsm, */ /* mdd_t* reachable, */ /* FILE* protected) { */ /* mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); */ /* array_t *nonProtectedIdArray,*bdd_vars, */ /* *bdd_one_v= array_alloc(bdd_t *, 0); */ /* mdd_t *prec, *tmp1, *tmp2, *res, *reach, *old; */ /* int numit = 0, arrSize=0; */ /* construction du vecteur des registres non protégés */ /* nonProtectedIdArray = */ /* determine_non_protected_registers(fsm,protected); */ /* if (array_n(nonProtectedIdArray) == */ /* array_n( Fsm_FsmReadPresentStateVars(fsm) )) { */ /* All the registers are unprotected */ /* return mdd_one(mddManager); */ /* } */ /* bdd_vars = getbddvars(mddManager, nonProtectedIdArray); */ /* arrSize = array_n(bdd_vars); */ /* calcul des états d'erreur */ /* old = fsm->reachabilityInfo.initialStates; */ /* reach = mdd_dup(reachable); */ /* prec = mdd_zero(mddManager); */ /* do { */ /* tmp1= */ /* for (i=0; ireachabilityInfo.initialStates = mdd_dup(res); */ /* reach = Fsm_FsmComputeReachableStates( */ /* fsm, 0, 0, 0, 0, 0, */ /* 0, 0, Fsm_Rch_Default_c, */ /* 0, 1, NIL(array_t), */ /* 0, NIL(array_t)); */ /* mdd_free(fsm->reachabilityInfo.initialStates); */ /* }while() */ /* return res; */ /* } */ // modèle de faute unicité spaciale et unicité temporelle //(S doit désigner l'ensemble des états accessibles) mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, mdd_t* S, FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; mdd_t *res; // construction du vecteur des registres non protégés nonProtectedIdArray = determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); res = inj_us(mddManager, bdd_vars, S); array_free(bdd_vars); array_free(nonProtectedIdArray); return res; } // modèle de faute multiplicité spaciale et unicité temporelle // (S doit désigner l'ensemble des états accessibles) mdd_t* error_states_ms_ut(Fsm_Fsm_t *fsm, mdd_t* S, FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; mdd_t *res; // construction du vecteur des registres non protégés nonProtectedIdArray = determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); res = inj_ms(mddManager, bdd_vars, S); array_free(bdd_vars); array_free(nonProtectedIdArray); return res; } // modèle de faute multiplicité spaciale et multiplicité temporelle // (S doit désigner l'ensemble des états accessibles) mdd_t* error_states_ms_mt(Fsm_Fsm_t *fsm, mdd_t* S0, mdd_t* S, FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; mdd_t *res,*delta_reachB; // construction du vecteur des registres non protégés mdd_t *tmp = fsm->reachabilityInfo.initialStates; mdd_t *tmpReach = fsm->reachabilityInfo.reachableStates; nonProtectedIdArray = determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); fsm->reachabilityInfo.initialStates = error_states(fsm, S,nonProtectedIdArray); delta_reachB = Fsm_FsmComputeReachableStates( fsm, 0, 0, 0, 0, 0, 0, 0, Fsm_Rch_Default_c, 0, 1, NIL(array_t), 0, NIL(array_t)); mdd_free(fsm->reachabilityInfo.initialStates); mdd_t* restmp = mdd_or(S0, delta_reachB, 1, 1); fsm->reachabilityInfo.initialStates=tmp; fsm->reachabilityInfo.reachableStates = tmpReach; res = inj_ms(mddManager, bdd_vars, restmp); mdd_free(delta_reachB); mdd_free(restmp); array_free(bdd_vars); array_free(nonProtectedIdArray); return res; } // modèle de faute unicité spaciale et multiplicité temporelle // (S doit désigner l'ensemble des états accessibles) /* mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, */ /* mdd_t* S, */ /* FILE* protected) { */ /* mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); */ /* array_t *nonProtectedIdArray, *bdd_vars; */ /* mdd_t *res,*delta_reachB,*tmp, */ /* *prec=mdd_one(Fsm_FsmReadMddManager(fsm));; */ /* // construction du vecteur des registres non protégés */ /* nonProtectedIdArray = */ /* determine_non_protected_registers(fsm,protected); */ /* bdd_vars = getbddvars(mddManager, nonProtectedIdArray); */ /* tmp = fsm->reachabilityInfo.initialStates; */ /* res = inj_us(mddManager, bdd_vars, S); */ /* do{ */ /* mdd_t *e,*p,*next; */ /* mdd_free(prec); */ /* prec = mdd_dup(res); */ /* e = mdd_dup(res); */ /* // compute delta(e) */ /* mdd_t * fromLowerBound = mdd_dup(e); */ /* mdd_t * fromUpperBound = mdd_dup(e); */ /* mdd_t * toCareSet = mdd_one(Fsm_FsmReadMddManager(fsm)); */ /* // Compute set of next states */ /* // Computes the forward image of a set, under the function vector */ /* // in imageInfo */ /* e = Img_ImageInfoComputeFwdWithDomainVars( fsm->imageInfo , */ /* fromLowerBound, */ /* fromUpperBound, */ /* toCareSet); */ /* // compute delta*(delta(e)) */ /* fsm->reachabilityInfo.initialStates = mdd_dup(e); */ /* mdd_free(fsm->reachabilityInfo.reachableStates); */ /* fsm->reachabilityInfo.reachableStates=NIL(mdd_t); */ /* e = mdd_dup(Fsm_FsmComputeReachableStates(fsm, 0, 0, 0, 0, 0, */ /* 0, 0, Fsm_Rch_Default_c, */ /* 0, 0, NIL(array_t), */ /* 0, NIL(array_t))); */ /* // res = res \vee inj_us(\delta*(delta(e))) */ /* // fault injection only for the set of next states */ /* mdd_t *tmp1, */ /* *e_inj= inj_us(mddManager, bdd_vars, e); */ /* tmp1=mdd_or(res,e_inj , 1, 1); */ /* mdd_free(e_inj); */ /* mdd_free(res); */ /* res=tmp1; */ /* }while(!mdd_equal(res, prec)); */ /* fsm->reachabilityInfo.initialStates=tmp; */ /* array_free(bdd_vars); */ /* array_free(nonProtectedIdArray); */ /* return res; */ /* } */ mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, mdd_t *S, FILE *protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); // construction du vecteur des registres non prot?g?s array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protect); array_t *bdd_vars = getbddvars(mddManager, nonProtectedIdArray); // sauvegarde des ?tats initiaux et accessibles courants mdd_t *tmpInit = fsm->reachabilityInfo.initialStates; mdd_t *tmpReach = mdd_dup(fsm->reachabilityInfo.reachableStates); // initialisation du r?sultat ? inj_us(S) mdd_t *res = inj_us(mddManager, bdd_vars, S); mdd_t *prec = mdd_one(mddManager); mdd_t *toCareSet = mdd_one(mddManager); do { mdd_free(prec); prec = mdd_dup(res); // compute e = delta(res) mdd_t *e = Img_ImageInfoComputeFwdWithDomainVars( fsm->imageInfo , res, res, toCareSet); // compute e = delta*(e) fsm->reachabilityInfo.initialStates = mdd_dup(e); mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.reachableStates=NIL(mdd_t); mdd_free(e); e = mdd_dup(Fsm_FsmComputeReachableStates(fsm, 0, 0, 0, 0, 0, 0, 0, Fsm_Rch_Default_c, 0, 0, NIL(array_t), 0, NIL(array_t))); // compute res = res | inj_us(e) mdd_t *e_inj = inj_us(mddManager, bdd_vars, e); mdd_free(e); e = mdd_or(res, e_inj , 1, 1); mdd_free(res); mdd_free(e_inj); res = e; } while(!mdd_equal(res, prec)); mdd_free(prec); mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.reachableStates=tmpReach; fsm->reachabilityInfo.initialStates=tmpInit; array_free(bdd_vars); array_free(nonProtectedIdArray); return res; } void print_variables_info(Fsm_Fsm_t *fsm) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *psVarsArray; int i, arrSize, mddId; mvar_type mVar; psVarsArray = Fsm_FsmReadPresentStateVars(fsm); arrSize = array_n( psVarsArray ); for ( i = 0 ; i < arrSize ; i++ ) { mddId = array_fetch( int, psVarsArray, i ); mVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager),mddId); (void) fprintf(vis_stdout, "%-20s%10d\n", mVar.name, mVar.values); } } mdd_t* evaluate_EF(Fsm_Fsm_t *fsm, mdd_t *target, mdd_t* fairS, int verbosityLevel) { mdd_t *res; mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); res = Mc_FsmEvaluateEUFormula( fsm, // Fsm_Fsm_t *fsm, mddOne, // mdd_t *invariant, target, // mdd_t *target, NIL(mdd_t), // mdd_t *underapprox, fairS, // mdd_t *fairStates, careStatesArray, // array_t *careStatesArray, MC_NO_EARLY_TERMINATION, // Mc_EarlyTermination_t *earlyTermination, NIL(array_t), // Fsm_HintsArray_t *hintsArray, Mc_None_c, // Mc_GuidedSearch_t hintType, NIL(array_t), // array_t *onionRings, verbosityLevel, // Mc_VerbosityLevel verbosity, McDcLevelNone_c, // Mc_DcLevel dcLevel, NIL(boolean) ); // boolean *fixpoint) array_free(careStatesArray); mdd_free(mddOne); return res; } mdd_t* evaluate_EG(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t* fairS,Fsm_Fairness_t * fairCond, int verbosityLevel) { mdd_t *res; mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); res = Mc_FsmEvaluateEGFormula( fsm, // Fsm_Fsm_t *fsm, invariant, // mdd_t *invariant,notforbiden NIL(mdd_t), // mdd_t *overapprox, fairS, // mdd_t *fairStates, fairCond, // Fsm_Fairness_t *modelFairness, careStatesArray, // array_t *careStatesArray, MC_NO_EARLY_TERMINATION, // Mc_EarlyTermination_t *earlyTermination, NIL(array_t), // Fsm_HintsArray_t *hintsArray, Mc_None_c, // Mc_GuidedSearch_t hintType, NIL(array_t*), // array_t **pOnionRingsArrayForDbg, verbosityLevel, // Mc_VerbosityLevel verbosity, McDcLevelNone_c, // Mc_DcLevel dcLevel, NIL(boolean), // boolean *fixpoint, McGSH_old_c // McGSH_Unassigned_c // Mc_GSHScheduleType GSHschedule) ); array_free(careStatesArray); mdd_free(mddOne); return res; } mdd_t* evaluate(Fsm_Fsm_t *fsm,FILE* ctlfile,mdd_t* fairS, Fsm_Fairness_t * fairCond, int verbosityLevel) { int i; mdd_t *res; mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); array_t * formula=Ctlp_FileParseFormulaArray(ctlfile); array_t * ctlNormalFormulaArray= Ctlp_FormulaArrayConvertToExistentialFormTree(formula); Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *, ctlNormalFormulaArray, 0); res= Mc_FsmEvaluateFormula(fsm, ctlFormula, fairS, fairCond, careStatesArray, MC_NO_EARLY_TERMINATION , NIL(array_t), Mc_None_c, verbosityLevel, McDcLevelNone_c, 0, // McGSH_Unassigned_c // Mc_GSHScheduleType GSHschedule) McGSH_old_c); CtlpFormulaFree(ctlFormula); free(ctlNormalFormulaArray); free(formula); // Ctlp_FormulaArrayFree(ctlNormalFormulaArray); // Ctlp_FormulaArrayFree(formula); array_free(careStatesArray); mdd_free(mddOne); return res; } mdd_t* evaluate_EU(Fsm_Fsm_t *fsm, mdd_t* inv, mdd_t *target,mdd_t* fairS, int verbosityLevel) { mdd_t *res; mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); res = Mc_FsmEvaluateEUFormula( fsm, // Fsm_Fsm_t *fsm, inv, // mdd_t *invariant, target, // mdd_t *target, NIL(mdd_t), // mdd_t *underapprox, fairS, // mdd_t *fairStates, careStatesArray, // array_t *careStatesArray, MC_NO_EARLY_TERMINATION, // Mc_EarlyTermination_t *earlyTermination, NIL(array_t), // Fsm_HintsArray_t *hintsArray, Mc_None_c, // Mc_GuidedSearch_t hintType, NIL(array_t), // array_t *onionRings, verbosityLevel, // Mc_VerbosityLevel verbosity, McDcLevelNone_c, // Mc_DcLevel dcLevel, NIL(boolean) // boolean *fixpoint) ); array_free(careStatesArray); mdd_free(mddOne); return res; } mdd_t* evaluate_AU(Fsm_Fsm_t *fsm, mdd_t* inv, mdd_t *target, mdd_t* fairS, Fsm_Fairness_t * fairCond, int verbosityLevel) { /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */ mdd_t* not_f = mdd_not(inv); mdd_t* not_g = mdd_not(target); mdd_t* not_g_and_not_f = mdd_and(not_f, not_g, 1, 1); mdd_t* eg_not_g = evaluate_EG(fsm, not_g, fairS, fairCond, verbosityLevel); mdd_t* e_not_g_U_not_g_and_not_f = evaluate_EU(fsm, not_g, not_g_and_not_f, fairS, verbosityLevel); mdd_t* or = mdd_or(e_not_g_U_not_g_and_not_f, eg_not_g, 1, 1); mdd_t* res = mdd_not(or); mdd_free(not_f); mdd_free(not_g); mdd_free(not_g_and_not_f); mdd_free(eg_not_g); mdd_free(e_not_g_U_not_g_and_not_f); mdd_free(or); return res; } void compute_fair(Fsm_Fsm_t *fsm,int verbosityLevel){ long initialTime; long finalTime; EpDouble *error = EpdAlloc(); mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, careStatesArray, 0, mddOne); mdd_t *res,*fairS; mdd_t* tmpfair = Fsm_FsmComputeFairStates(fsm, careStatesArray, verbosityLevel, McDcLevelNone_c, McGSH_Unassigned_c , McBwd_c, FALSE ); res=mdd_and(fsm->reachabilityInfo.initialStates, tmpfair, 1, 1); if(verbosityLevel){ (void) fprintf(vis_stdout,"********************************\n"); print_number_of_states("Fair error states = ", fsm, res); } mdd_free(tmpfair); if (!mdd_lequal(fsm->reachabilityInfo.initialStates, res, 1, 1)) { (void) fprintf(vis_stdout, "WARNING : some error states are not fair\n"); (void) fprintf(vis_stdout, "WARNING : only fair error states will be taken into account\n"); // attention, il faut prendre en compte le cas ou aucun 'error state' n'est fa ir mdd_free(fsm->reachabilityInfo.initialStates); fsm->reachabilityInfo.initialStates = res; // mise à jour des états accessibles mdd_free(fsm->reachabilityInfo.reachableStates); (void)Fsm_FsmComputeReachableStates(fsm,0,0, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,0, NIL(array_t), 0, NIL(array_t)); finalTime = util_cpu_time(); (void) fprintf(vis_stdout,"********************************\n"); print_number_of_states("States reachable from fair error states = ", fsm, fsm->reachabilityInfo.reachableStates); } else mdd_free(res); array_free(careStatesArray); mdd_free(mddOne); } mdd_t* getForbidden(Fsm_Fsm_t *fsm){ assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->RobSets.Forb == NIL(mdd_t)) fsm->RobSets.Forb= mdd_zero(Fsm_FsmReadMddManager(fsm)); return mdd_dup(fsm->RobSets.Forb); } mdd_t* getRequired(Fsm_Fsm_t *fsm){ assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->RobSets.Req == NIL(mdd_t)) fsm->RobSets.Req= mdd_one(Fsm_FsmReadMddManager(fsm)); return mdd_dup(fsm->RobSets.Req); } mdd_t* getSafe( Fsm_Fsm_t *fsm ){ assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->RobSets.Safe == NIL(mdd_t)){ mdd_t* inits=fsm->reachabilityInfo.initialStates; mdd_t* reachs=fsm->reachabilityInfo.reachableStates; fsm->reachabilityInfo.initialStates=NIL(mdd_t); fsm->reachabilityInfo.reachableStates=NIL(mdd_t); (void)Fsm_FsmComputeInitialStates(fsm); (void)Fsm_FsmComputeReachableStates(fsm,0,0, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,0, NIL(array_t), 0, NIL(array_t)); fsm->RobSets.Safe= mdd_dup(fsm->reachabilityInfo.reachableStates); mdd_free(fsm->reachabilityInfo.initialStates); mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.initialStates=inits; fsm->reachabilityInfo.reachableStates=reachs; } return mdd_dup(fsm->RobSets.Safe); } mdd_t* getInitial(Fsm_Fsm_t *fsm) { assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)) return mdd_dup(fsm->reachabilityInfo.initialStates); if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){ mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.reachableStates=NIL(mdd_t); } (void)Fsm_FsmComputeInitialStates(fsm); (void)Fsm_FsmComputeReachableStates(fsm,0,0, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,0, NIL(array_t), 0, NIL(array_t)); return mdd_dup(fsm->reachabilityInfo.initialStates); } mdd_t* getReachOrg( Fsm_Fsm_t *fsm ){ assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->RobSets.originalreachableStates == NIL(mdd_t)){ mdd_t* inits=fsm->reachabilityInfo.initialStates; mdd_t* reachs=fsm->reachabilityInfo.reachableStates; fsm->reachabilityInfo.initialStates=NIL(mdd_t); fsm->reachabilityInfo.reachableStates=NIL(mdd_t); (void)Fsm_FsmComputeInitialStates(fsm); (void)Fsm_FsmComputeReachableStates(fsm,0,0, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,0, NIL(array_t), 0, NIL(array_t)); fsm->RobSets.originalreachableStates= mdd_dup(fsm->reachabilityInfo.reachableStates); mdd_free(fsm->reachabilityInfo.initialStates); mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.initialStates=inits; fsm->reachabilityInfo.reachableStates=reachs; } return mdd_dup(fsm->RobSets.originalreachableStates); } mdd_t* getReach(Fsm_Fsm_t *fsm) { assert(fsm != NIL(Fsm_Fsm_t)); if (fsm->reachabilityInfo.reachableStates != NIL(mdd_t)) return mdd_dup(fsm->reachabilityInfo.reachableStates); if (fsm->reachabilityInfo.initialStates == NIL(mdd_t)) { (void)Fsm_FsmComputeInitialStates(fsm); } (void)Fsm_FsmComputeReachableStates(fsm,0,0, 0,0, 0, 0, 0, Fsm_Rch_Default_c, 0,0, NIL(array_t), 0, NIL(array_t)); return mdd_dup(fsm->reachabilityInfo.reachableStates); } mdd_t* evaluate_Formula_AF_AF (Fsm_Fsm_t *fsm, mdd_t* Req,mdd_t* forb,mdd_t* Safe, int verbosityLevel ){ mdd_t *notforbiden=mdd_not(forb);; mdd_t *XU_notForb_And_Safe; mdd_t *Req_And_XU_notForb_And_Safe; mdd_t *Setformula; XU_notForb_And_Safe = evaluate_AU(fsm, notforbiden,Safe, fsm->fairnessInfo.states, fsm->fairnessInfo.constraint, verbosityLevel); Req_And_XU_notForb_And_Safe = mdd_and(Req, XU_notForb_And_Safe, 1, 1); mdd_free(XU_notForb_And_Safe); Setformula=evaluate_AU(fsm, notforbiden, Req_And_XU_notForb_And_Safe, fsm->fairnessInfo.states, fsm->fairnessInfo.constraint, verbosityLevel); mdd_free(Req_And_XU_notForb_And_Safe); mdd_free(notforbiden); return Setformula; } mdd_t* evaluate_Formula_EF_AF (Fsm_Fsm_t *fsm, mdd_t* Req,mdd_t* forb, mdd_t* Safe, int verbosityLevel ){ mdd_t *notforbiden=mdd_not(forb);; mdd_t *XU_notForb_And_Safe; mdd_t *Req_And_XU_notForb_And_Safe; mdd_t *Setformula; XU_notForb_And_Safe = evaluate_AU(fsm, notforbiden, Safe, fsm->fairnessInfo.states, fsm->fairnessInfo.constraint, verbosityLevel); Req_And_XU_notForb_And_Safe = mdd_and(Req,XU_notForb_And_Safe,1,1); mdd_free( XU_notForb_And_Safe); Setformula=evaluate_EU(fsm, notforbiden, Req_And_XU_notForb_And_Safe, fsm->fairnessInfo.states, verbosityLevel); mdd_free(Req_And_XU_notForb_And_Safe); mdd_free(notforbiden); return Setformula; } mdd_t* evaluate_Formula_AF_EF (Fsm_Fsm_t *fsm, mdd_t* Req,mdd_t* forb,mdd_t* Safe, int verbosityLevel ){ mdd_t *notforbiden=mdd_not(forb);; mdd_t *XU_notForb_And_Safe; mdd_t *Req_And_XU_notForb_And_Safe; mdd_t *Setformula; XU_notForb_And_Safe = evaluate_EU(fsm, notforbiden, Safe, fsm->fairnessInfo.states, verbosityLevel); Req_And_XU_notForb_And_Safe = mdd_and(Req,XU_notForb_And_Safe,1,1); mdd_free( XU_notForb_And_Safe); Setformula=evaluate_AU(fsm, notforbiden, Req_And_XU_notForb_And_Safe, fsm->fairnessInfo.states, fsm->fairnessInfo.constraint, verbosityLevel); mdd_free(Req_And_XU_notForb_And_Safe); mdd_free(notforbiden); return Setformula; } mdd_t* evaluate_Formula_EF_EF (Fsm_Fsm_t *fsm, mdd_t* Req,mdd_t* forb,mdd_t* Safe, int verbosityLevel ){ mdd_t *notforbiden=mdd_not(forb);; mdd_t *XU_notForb_And_Safe; mdd_t *Req_And_XU_notForb_And_Safe; mdd_t *Setformula; XU_notForb_And_Safe = evaluate_EU(fsm, notforbiden,Safe, fsm->fairnessInfo.states, verbosityLevel); Req_And_XU_notForb_And_Safe =mdd_and(Req,XU_notForb_And_Safe,1,1); mdd_free( XU_notForb_And_Safe); Setformula=evaluate_EU(fsm, notforbiden, Req_And_XU_notForb_And_Safe, fsm->fairnessInfo.states, verbosityLevel); mdd_free(Req_And_XU_notForb_And_Safe); mdd_free(notforbiden); return Setformula; } void mdd_FunctionPrint(mdd_manager *mgr , mdd_t * top, FILE * f) { mdd_t * T; mdd_t * E; int id; char c=' '; static int level; level++; id = bdd_top_var_id(top); mvar_type mv = mymddGetVarById(mgr,id); fprintf(f,"("); // Pour le Then T=bdd_then(top); if(bdd_is_tautology(T,1)){ fprintf(f,"%s = 1 ",mv.name); c = '+'; } else if(!bdd_is_tautology(T,0)){ fprintf(f,"%s = 1 * ",mv.name); mdd_FunctionPrint(mgr, T,f); c = '+'; } mdd_free(T); //pour le Else E=bdd_else(top); if(bdd_is_tautology(E,0)){ goto fin; } if(bdd_is_tautology(E,1)){ fprintf(f,"%c %s = 0",c, mv.name); goto fin; } fprintf(f,"%c %s = 0 * ",c, mv.name); mdd_FunctionPrint(mgr, E,f); mdd_free(E); fin: fprintf(f,")"); level--; return; } void mdd_FunctionPrintMain(mdd_manager *mgr , mdd_t * top, char * macro_name, FILE * f){ if(bdd_is_tautology(top,0)){ fprintf(f,"\\define %s (FALSE)\n", macro_name); return; } if(bdd_is_tautology(top,1)){ fprintf(f,"\\define %s (TRUE)\n", macro_name); return; } fprintf(f,"\\define %s ", macro_name); mdd_FunctionPrint(mgr,top,f); fprintf(f,"\n"); return; } void callBmcRob( Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options) { Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula); st_table *CoiTable = //NIL(st_table); st_init_table(st_ptrcmp, st_ptrhash); assert(ltlFormula != NIL(Ctlsp_Formula_t)); assert(network != NIL(Ntk_Network_t)); // Print out the given LTL formula if (options->verbosityLevel >= BmcVerbosityMax_c){ fprintf(vis_stdout, "Formula: "); Ctlsp_FormulaPrint(vis_stdout, ltlFormula); fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "Negated formula: "); Ctlsp_FormulaPrint(vis_stdout, negLtlFormula); fprintf(vis_stdout, "\n"); } // Compute the cone of influence of the LTL formula // BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable); // CoiTable= (st_table *) Ntk_NetworkReadApplInfo(network, // MVFAIG_NETWORK_APPL_KEY); Ntk_Node_t *node; lsGen gen; Ntk_NetworkForEachLatch(network, gen, node){ st_insert(CoiTable, (char *) node, (char *) 0); } if(options->clauses == 2){ BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options); } else { if(options->encoding == 0) BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options, 0); else if(options->encoding == 1) BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options, 1); else if(options->encoding == 2) BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula, CoiTable, constraintArray, options); } st_free_table(CoiTable); Ctlsp_FormulaFree(negLtlFormula); } /* void callBmcRob( Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options) { Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula); st_table *CoiTable = st_init_table(st_ptrcmp, st_ptrhash); assert(ltlFormula != NIL(Ctlsp_Formula_t)); assert(network != NIL(Ntk_Network_t)); // Print out the given LTL formula if (options->verbosityLevel >= BmcVerbosityMax_c){ fprintf(vis_stdout, "Formula: "); Ctlsp_FormulaPrint(vis_stdout, ltlFormula); fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "Negated formula: "); Ctlsp_FormulaPrint(vis_stdout, negLtlFormula); fprintf(vis_stdout, "\n"); } // CoiTable= (st_table *) Ntk_NetworkReadApplInfo(network, // MVFAIG_NETWORK_APPL_KEY); BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable); BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options); st_free_table(CoiTable); Ctlsp_FormulaFree(negLtlFormula); } */ /* bAigEdge_t sat_Add_Blocking_Clauses(mAig_Manager_t *manager , char* filename){ FILE *fin; char line[102400], word[1024]; char *lp; int v,v1; int i, size, index, value,lvalue,k=0; bAigEdge_t *tv,j,result=mAig_One; FILE *blfile; bAigTimeFrame_t *timeframe= manager->timeframeWOI; int bound = timeframe->currentTimeframe; if(!(fin = fopen(filename, "r"))) { fprintf(vis_stdout, "ERROR : Can't open file %s\n", filename); exit(0); } for (k=0 ; kli2index, (char *)j, &index)) continue ; j = timeframe->latchInputs[k][index]; if(j == bAig_One) { result = mAig_And(manager, result, bAig_GetCanonical(manager, j)); } else if (j != bAig_Zero) { tv = sat_GetCanonical(manager, j); lvalue = bAig_GetValueOfNode(manager, tv); if(lvalue == 1) result = mAig_And(manager, result, bAig_GetCanonical(manager, j)); } } else { break; } } } rewind(fin); } fclose(fin); return result; } */ bAigEdge_t sat_Add_Blocking_Clauses( Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable ){ mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t *timeframe= manager->timeframeWOI; int bound = timeframe->currentTimeframe; Ntk_Node_t *node; int tmp,k,i,j,index; array_t * latchArr = array_alloc(Ntk_Node_t *, 0); MvfAig_Function_t *mvfAig; bAigEdge_t *tv,v,result=mAig_One; lsGen gen; int lvalue; Ntk_NetworkForEachLatch(network, gen, node){ if (st_lookup_int(coiTable, (char *) node, &tmp)){ array_insert_last(Ntk_Node_t *, latchArr, node); } } for (k=0 ; kli2index, (char *)v, &index)) continue; v = timeframe->latchInputs[k][index]; if(v == bAig_One) { result = mAig_And(manager, result, bAig_GetCanonical(manager, v)); break; } if(v != bAig_Zero) { tv = bAig_GetCanonical(manager, v); lvalue = bAig_GetValueOfNode(manager, tv); if(lvalue == 1){ result = mAig_And(manager, result, bAig_GetCanonical(manager, v)); break; } } } } } array_free(latchArr); return result; } /* mdd_t * find_removed_latchs( Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, st_table *hashTable, mdd_manager *mgr, int *V ){ mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t *timeframe= manager->timeframeWOI; int bound = timeframe->currentTimeframe; Ntk_Node_t *node; int tmp,k,i,j,index,lvalue; array_t * latchArr = array_alloc(Ntk_Node_t *, 0); MvfAig_Function_t *mvfAig; bAigEdge_t *tv,v,result=mAig_One; lsGen gen; mdd_t* one = mdd_one(mgr); mdd_t* zero = mdd_zero(mgr); mdd_t* R=mdd_one(mgr); int found,t; Ntk_NetworkForEachLatch(network, gen, node){ if (st_lookup_int(coiTable, (char *) node, &tmp)){ array_insert_last(Ntk_Node_t *, latchArr, node); } } for (k=0 ; kli2index, (char *)v, &index)) continue; t = timeframe->latchInputs[k][index]; if(!st_lookup_int(hashTable,(char *)t, &index)) continue; else found=1; } if (!found){ st_insert(hashTable, (char*)t,(char*) (*V)+1);(*V)++; mdd_t* value=bdd_construct_bdd_t(mgr,Cudd_IndicesToCube(mgr,V,1)); mdd_t* tmp=R; R=mdd_and(R,value,1,1); mdd_free(value); mdd_free(tmp); } } array_free(latchArr); if(mdd_equal(R,one)){ mdd_free(R); R=mdd_zero(mgr); } mdd_free(one); mdd_free(zero); return R; } */ void sat_Add_Blocking_Clauses_2(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, FILE* cnffile ){ mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); bAigTimeFrame_t *timeframe= manager->timeframeWOI; int bound = timeframe->currentTimeframe; Ntk_Node_t *node; int tmp,k,i,j,index; array_t * latchArr = array_alloc(Ntk_Node_t *, 0); MvfAig_Function_t *mvfAig; bAigEdge_t *tv,v,result=mAig_One; lsGen gen; int lvalue; Ntk_NetworkForEachLatch(network, gen, node){ if (st_lookup_int(coiTable, (char *) node, &tmp)){ array_insert_last(Ntk_Node_t *, latchArr, node); } } for (k=0 ; kli2index, (char *)v, &index)) continue; v = timeframe->latchInputs[k][index]; if(v == bAig_One) { result = mAig_And(manager, result, bAig_GetCanonical(manager, v)); break; } if(v != bAig_Zero) { tv = bAig_GetCanonical(manager, v); lvalue = bAig_GetValueOfNode(manager, tv); if(lvalue == 1){ result = mAig_And(manager, result, bAig_GetCanonical(manager, v)); break; } } } } } array_free(latchArr); } /**Function******************************************************************** * Synopsis [Build a new model based on the current Hierarchy] Description [Build a new hierarchy named ROB3. Composition of two instances (golden and faulty) of the current hierarchy. The inputs are the same as before. The outputs are doubled. Return the new created node. ] SideEffects [] ******************************************************************************/ Hrc_Node_t * build_golden_faulty_compo( Hrc_Manager_t * hmgr, Hrc_Node_t* rootNode, Hrc_Model_t* newRootModel ) { int i; Var_Variable_t *var; char * name, *newName; array_t *actualOutputArray, *actualOutputArrayG; array_t *actualInputArray, *actualInputArrayG; Hrc_Model_t * rootModel = Hrc_ManagerFindModelByName(hmgr,Hrc_NodeReadModelName(rootNode)); printf("Root %s\n", Hrc_NodeReadModelName(rootNode)); Hrc_Node_t * newRootNode = Hrc_ModelReadMasterNode(newRootModel); actualOutputArray = array_alloc(Var_Variable_t*,Hrc_NodeReadNumFormalOutputs(rootNode)); actualOutputArrayG = array_alloc(Var_Variable_t*,0); // New Outputs Faulty and Golden Hrc_NodeForEachFormalOutput(rootNode,i,var){ name = Var_VariableReadName(var); newName = ALLOC(char, strlen(name) +4); sprintf(newName, "%sG", name); Var_Variable_t * vG = Var_VariableDup(var, newRootNode); Var_VariableChangeName(vG,newName); Var_Variable_t * v = Var_VariableDup(var, newRootNode); Hrc_NodeAddVariable(newRootNode,v); array_insert_last(Var_Variable_t *, actualOutputArray, v); Hrc_NodeAddVariable(newRootNode,vG); array_insert_last(Var_Variable_t *, actualOutputArrayG, vG); Var_VariableResetPO(v); Var_VariableResetPO(vG); Hrc_NodeAddFormalOutput(newRootNode,v); Hrc_NodeAddFormalOutput(newRootNode,vG); } //New Inputs Hrc_NodeForEachFormalInput(rootNode,i,var){ Var_Variable_t * v = Var_VariableDup(var, newRootNode); Hrc_NodeAddVariable(newRootNode,v); Var_VariableResetPI(v); Hrc_NodeAddFormalInput(newRootNode,v); } // Create 2 instances "golden" and "faulty" of the previous hierarchy actualInputArray = array_dup(Hrc_NodeReadFormalInputs(newRootNode)); actualInputArrayG= array_dup(Hrc_NodeReadFormalInputs(newRootNode)); Hrc_ModelAddSubckt(newRootModel,rootModel, "golden",actualInputArrayG, actualOutputArrayG); Hrc_ModelAddSubckt(newRootModel,rootModel, "faulty",actualInputArray, actualOutputArray); // Create the new Hierarchy newRootNode = Hrc_ModelCreateHierarchy(hmgr, newRootModel, "ROB3"); //replace the hierarchy with the new one Hrc_TreeReplace(rootNode,newRootNode); return newRootNode; } /**Function******************************************************************** * Synopsis [Generate name of protected register] Description [Generate file containing names of latches in the golden model that have to be protected. ] SideEffects [] ******************************************************************************/ int generateProtectFile( Hrc_Node_t * goldenNode, FILE *oFile, char * instanceName) { st_generator * gen; char* name, *childName,*newName; Hrc_Latch_t * latch; Hrc_Node_t * child; int a; Hrc_NodeForEachLatch(goldenNode, gen,name,latch){ if( instanceName =="") fprintf(oFile,"%s\n",name); else fprintf(oFile,"%s.%s\n",instanceName,name); } a = Hrc_NodeReadNumLatches(goldenNode); if(Hrc_NodeReadNumChildren(goldenNode) != 0){ Hrc_NodeForEachChild(goldenNode,gen,childName,child){ newName = malloc(strlen(instanceName)+strlen(childName)+1); if( instanceName =="") sprintf(newName,"%s",childName); else sprintf(newName,"%s.%s",instanceName,childName); a += generateProtectFile(child,oFile,newName); } } return a; }