Index: vis_dev/vis-2.3/src/rob/Robust.c =================================================================== --- vis_dev/vis-2.3/src/rob/Robust.c (revision 19) +++ vis_dev/vis-2.3/src/rob/Robust.c (revision 19) @@ -0,0 +1,1737 @@ +/**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 protected = 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) { + protected = 1; + break; + } + } + else if (strcmp(mVar.name, w) == 0) { + protected = 1; + break; + } + } + (void) fprintf(vis_stdout, "%-20s%10d", mVar.name, mVar.values); + if (protected) { + (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* protected) { + 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,protected); + + 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* protected) { + 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,protected); + + 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* protected) { + 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,protected); + + 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* protected) { + 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,protected); + 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 *protected) { + + mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); + + // construction du vecteur des registres non protégés + array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protected); + 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 int he 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; +} + Index: vis_dev/vis-2.3/src/rob/Robust.h =================================================================== --- vis_dev/vis-2.3/src/rob/Robust.h (revision 19) +++ vis_dev/vis-2.3/src/rob/Robust.h (revision 19) @@ -0,0 +1,118 @@ +/**HFile*********************************************************************** + + FileName [Robust.h] + + PackageName [rob] + + Synopsis [Headers and strcutus for Robustness package.] + + Author [Souheib Baarir, Denis Poitrenaud,J.M Ilié ] + + Copyright [Copyright (c) 1994-1996 The Regents of the Univ. 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 PARIS VI 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.] + +******************************************************************************/ + + + +#ifndef _ROB_H +#define _ROB_H +#include "../ntk/ntkInt.h" +#include "../hrc/hrcInt.h" +#include "../fsm/fsmInt.h" +#include "../bmc/bmcInt.h" +#include "../sat/sat.h" +#include "../sat/satInt.h" + +typedef enum{ + ecmd, + eofile, + earg, + enfile, + eicmd, + eiofile, + ercmd +} type_err; + +// fonctions divers +void get_number_of_states (Fsm_Fsm_t *fsm, mdd_t* b, EpDouble* ep); +array_t* determine_non_protected_registers(Fsm_Fsm_t *fsm, FILE *f); +mdd_t* compute_error_states (Fsm_Fsm_t *fsm, mdd_t* reachable, + int verbosityLevel, int printStep, + FILE* protected); +mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, mdd_t* reachable, + FILE* protected); +void compute_fair (Fsm_Fsm_t *fsm,int verbosityLevel); +Hrc_Node_t * build_golden_faulty_compo(Hrc_Manager_t * hmgr,Hrc_Node_t * rootNode, Hrc_Model_t * newRootModel); + + +int generateProtectFile(Hrc_Node_t * goldenNode, FILE *oFile,char * +instanceName); + +// fonction d'évaluation de formules CTL +mdd_t* evaluate_EF (Fsm_Fsm_t *fsm, mdd_t *target, + mdd_t* fairS, int verbosityLevel); +mdd_t* evaluate_EG (Fsm_Fsm_t *fsm, mdd_t *invariant, + mdd_t* fairS,Fsm_Fairness_t * fairCond, + int verbosityLevel); +mdd_t* evaluate_EU (Fsm_Fsm_t *fsm, mdd_t* inv, + mdd_t *target,mdd_t* fairS, + int verbosityLevel); +mdd_t* evaluate_AU (Fsm_Fsm_t *fsm, mdd_t* inv, + mdd_t *target, mdd_t* fairS, + Fsm_Fairness_t * fairCond, + int verbosityLevel); +mdd_t* evaluate (Fsm_Fsm_t *fsm,FILE* ctlfile, + mdd_t* fairS, + Fsm_Fairness_t * fairCond, + int verbosityLevel); +mdd_t* evaluate_Formula_AF_AF (Fsm_Fsm_t *fsm, mdd_t* Req, + mdd_t* forb,mdd_t* Safe, + int verbosityLevel ); +mdd_t* evaluate_Formula_AF_EF (Fsm_Fsm_t *fsm, mdd_t* Req, + mdd_t* forb,mdd_t* Safe, + int verbosityLevel ); +mdd_t* evaluate_Formula_EF_AF (Fsm_Fsm_t *fsm, mdd_t* Req, + mdd_t* forb,mdd_t* Safe, + int verbosityLevel ); +mdd_t* evaluate_Formula_EF_EF (Fsm_Fsm_t *fsm, mdd_t* Req, + mdd_t* forb,mdd_t* Safe, + int verbosityLevel ); +void callBmcRob ( Ntk_Network_t *network, + Ctlsp_Formula_t *ltlFormula, + array_t *constraintArray, + BmcOption_t *options); + +// fonctions d'acces +mdd_t* getForbidden (Fsm_Fsm_t *fsm); +mdd_t* getRequired (Fsm_Fsm_t *fsm); +mdd_t* getSafe (Fsm_Fsm_t *fsm); +mdd_t* getInitial (Fsm_Fsm_t *fsm); +mdd_t* getReach (Fsm_Fsm_t *fsm); +mdd_t* getReachOrg (Fsm_Fsm_t *fsm ); + +// fonction d'affichage +void print_number_of_states (char* msg, Fsm_Fsm_t *fsm, mdd_t* b); +void print_variables_info (Fsm_Fsm_t *fsm); +void error_msg (FILE* f, char* t, type_err e); +void conv_error_msg (FILE* f, char* cmd, type_err e); +void mdd_FunctionPrintMain (mdd_manager *mgr ,mdd_t * top, + char * macro_name, FILE * f); + +#endif /* _ROB_H */ Index: vis_dev/vis-2.3/src/rob/SatCountAlgo.c =================================================================== --- vis_dev/vis-2.3/src/rob/SatCountAlgo.c (revision 19) +++ vis_dev/vis-2.3/src/rob/SatCountAlgo.c (revision 19) @@ -0,0 +1,1580 @@ + +/**CFile*********************************************************************** + + FileName [SatCountAlgo.c] + + PackageName [rob] + + Synopsis [Functions for Sat count Algo. ] + + Author [Souheib baarir] + + Copyright [Copyright (c) 2008-2009 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 "SatCountAlgo.h" +#include +#include +#include +#include +#include +#include + +int nVar=0, nCl=0; +const int K=5; + + + +Formula_t +createFormula(mdd_manager * mgr){ + Formula_t formul = ALLOC(Formula,1); + formul->F=lsCreate(); + formul->V=mdd_zero(mgr); + formul->R=mdd_zero(mgr); + formul->mgr=mgr; + return formul; +} + + +void free_formula(Formula_t F){ + (void)lsDestroy(F->F,mdd_free); + mdd_free(F->V); + mdd_free(F->R); + free(F); +} + + +static mdd_t* +mdd_restrict(mdd_manager* mgr, + mdd_t* l,mdd_t* d){ + + DdNode * tmp=bdd_bdd_restrict(mgr, l->node,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); +} + +mdd_t* +ComposeCubes(mdd_manager* mgr, + mdd_t* vars1, + mdd_t* vars2){ + + bdd_node* v[2]; + v[0]= vars1->node; + v[1]= vars2->node; + DdNode * b = bdd_bdd_vector_support(mgr,v,2); + cuddRef(b); + return bdd_construct_bdd_t(mgr,b); + +} + +mdd_t* +Get_support(mdd_manager* mgr,mdd_t* l){ + + DdNode * v = bdd_bdd_support(mgr, l->node); + cuddRef(v); + return bdd_construct_bdd_t(mgr, v); + +} + +int +Common_support(mdd_manager* mgr, + mdd_t* f, + mdd_t* c){ + + int v=1; + + mdd_t* fs= Get_support(mgr,f); + mdd_t* cs= Get_support(mgr,c); + mdd_t* k = bdd_smooth_with_cube(fs,cs); + + assert(k!=NULL); + + if (mdd_equal(k,fs)) + v=0; + + mdd_free(k); + mdd_free(fs); + mdd_free(cs); + return v; + +} + + +Formula_t +clone_formula(Formula_t form){ + mdd_manager* mgr = form->mgr; + lsGen gen =lsStart(form->F); + + lsGeneric data; + lsHandle itemHandle; + int* vars=NULL; + int* vs=NULL; + int j=0,i=0; + int size=((DdManager *)mgr)->size; + mdd_manager* nmgr=bdd_start(size); + Formula_t f=NULL; + + if(nmgr){ + vars=Cudd_SupportIndex((DdManager *) mgr, form->V->node); + + for (i=0;i< size;i++) + if(vars[i]){ + vars[i]=j; + j++; + } + + mdd_t* zero=mdd_zero(mgr); + mdd_t* V=mdd_one(nmgr); + f=createFormula(nmgr); + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l =(mdd_t*)data; + vs =Cudd_SupportIndex((DdManager *) mgr, l->node); + mdd_t* clause=mdd_one(nmgr); + + for(i=0;iF,clause,LS_NH); + free(vs); + } + + lsFinish(gen); + + free(vars); + mdd_free(f->V); + f->V=V; + + if(!mdd_equal(form->R,zero)){ + + vars=Cudd_SupportIndex((DdManager *) mgr, form->R->node); + + for (i=0;i< size;i++) + if(vars[i]){ + vars[i]=j; + j++; + } + + mdd_free(f->R); + mdd_t* R=mdd_one(nmgr); + vs=Cudd_SupportIndex((DdManager *) mgr, form->R->node); + for(i=0;iR=R; + } + + mdd_free(zero); + } + return f; +} + + + +Formula_t +_psi(Formula_t For,mdd_t* d){ + + mdd_manager* mgr = For->mgr; + lsGen gen =lsStart(For->F); + + lsGeneric data; + lsHandle itemHandle; + + mdd_t* nd =bdd_not(d); + mdd_t* one =mdd_one(mgr); + mdd_t* zero=mdd_zero(mgr); + mdd_t* v =mdd_zero(mgr); + + Formula_t F2=createFormula(mgr); + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l=(mdd_t*)data; + + if(Common_support(mgr,l,d)){ + mdd_t* res=mdd_restrict(mgr,l,d); + if(mdd_equal(res,zero)){ + mdd_t* newl = mdd_restrict(mgr,l,nd); + (void)lsNewEnd(F2->F,newl,LS_NH); + mdd_t* tmp = v; + v=ComposeCubes(mgr,v,newl); + mdd_free(tmp); + + if(mdd_equal(newl,one)){ + lsFinish(gen); + mdd_free(res); + mdd_free(one); + mdd_free(zero); + mdd_free(nd); + return F2; + } + + } + mdd_free(res); + } + else{ + mdd_t* ll= mdd_dup(l); + (void)lsNewEnd(F2->F,ll,LS_NH); + mdd_t* tmp=v; + v=ComposeCubes(mgr,v,l); + mdd_free(tmp); + } + } + + lsFinish(gen); + // New set of elemanated variables + mdd_t* v1=ComposeCubes(mgr,v,d); + mdd_t* newelem=bdd_smooth_with_cube(For->V,v1); + mdd_t* R; + mdd_t* V; + + R=mdd_dup(For->R); + mdd_free(F2->R); + mdd_free(F2->V); + + if (!mdd_equal(newelem,one)){ + F2->R=ComposeCubes(mgr,R,newelem); + mdd_free(R); + } + else{ + F2->R=R; + } + + // New set of variables + F2->V=v; + + mdd_free(one); + mdd_free(zero); + mdd_free(v1); + mdd_free(nd); + mdd_free(newelem); + + return F2; +} + +mdd_t* +get_var_sup (Formula_t Form){ + lsGeneric data; + lsHandle itemHandle; + mdd_manager* mgr =Form->mgr; + lsGen gen=lsStart(Form->F); + mdd_t* Current; + mdd_t* Before=mdd_zero(mgr); + + (void)lsFirstItem(Form->F,&data,&itemHandle); + Current=Get_support(mgr,(mdd_t*)data); + + assert(Current!=NULL); + + do{ + + mdd_free(Before); + Before = mdd_dup(Current); + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = mdd_dup((mdd_t*)data); + mdd_t* sup =Get_support (mgr,l); + if(Common_support(mgr,Current, l)){ + mdd_t* tmp= Current; + Current=ComposeCubes(mgr,Current,sup); + mdd_free(tmp); + } + mdd_free(l); + mdd_free(sup); + } + lsFinish(gen); + gen=lsStart(Form->F); + } + while(!mdd_equal(Before,Current)); + lsFinish(gen); + + mdd_free(Before); + return Current; +} + + +int +disjoint_formula(Formula_t Form, + Formula_t* F1, + Formula_t* F2){ + + lsGeneric data; + lsHandle itemHandle; + lsGen gen=lsStart(Form->F); + mdd_manager* mgr =Form->mgr; + mdd_t* V1; + mdd_t* V2; + + V2=get_var_sup (Form); + + if (!mdd_equal(V2,Form->V)){ + + (*F1) = createFormula(mgr); + (*F2) = createFormula(mgr); + mdd_free((*F2)->V); + mdd_free((*F1)->V); + (*F2)->V = V2; + (*F1)->V = bdd_smooth_with_cube(Form->V,V2); + + assert((*F1)->V!=NULL); + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = mdd_dup((mdd_t*)data); + if(Common_support(mgr,V2, l)){ + (void)lsNewEnd((*F2)->F,mdd_dup(data),LS_NH); + } + else{ + (void)lsNewEnd((*F1)->F,mdd_dup(data),LS_NH); + } + mdd_free(l); + } + + lsFinish(gen); + return 1; + } + lsFinish(gen); + mdd_free(V2); + return 0; +} + + + + +int +_d(Formula_t Form, mdd_t* x){ + + int cpt=0; + lsGeneric data; + lsHandle itemHandle; + lsGen gen=lsStart(Form->F); + mdd_manager* mgr =Form->mgr; + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = mdd_dup((mdd_t*)data); + + if(Common_support(mgr,l,x)) + cpt ++; + + mdd_free(l); + } + + lsFinish(gen); + return cpt; +} + + + +mdd_t* +_k_clause(Formula_t Form, int k){ + int cpt=0; + lsGeneric data; + lsHandle itemHandle; + lsGen gen=lsStart(Form->F); + mdd_manager* mgr =Form->mgr; + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = (mdd_t*)data; + if (Cudd_SupportSize((DdManager *) mgr, + l->node)==k){ + lsFinish(gen); + return mdd_dup(l); + } + } + + lsFinish(gen); + return mdd_zero(mgr); +} + + +int +greater_d(Formula_t Form,int k){ + int* vars=NULL; + mdd_manager* mgr =Form->mgr; + int nbvar=((DdManager *)mgr)->size; + int d=0,i,g,s; + mdd_t* zero=mdd_zero(mgr); + + for(i=0;i d){ + d = s; + g = i; + } + mdd_free(v); + mdd_free(c); + } + + mdd_free(zero); + return g; +} + + +mdd_t* +get_w(Formula_t Form, + mdd_t* clause, + int * vars, int k){ + int i,j,nbvar=((DdManager *)(Form->mgr))->size; + mdd_manager* mgr =Form->mgr; + + for(i=0;imgr; + int i,nbvar=((DdManager *)mgr)->size; + mdd_t* w; + mdd_t* zero=mdd_zero(mgr); + + vars=Cudd_SupportIndex((DdManager *) mgr, clause->node); + + if (!mdd_equal((w=get_w(Form, clause, vars, 1)), + zero)){ + free(vars); + mdd_free(zero); + return w; + } + + mdd_free(w); + + if (!mdd_equal((w=get_w(Form, clause, vars, 2)), + zero)){ + free(vars); + mdd_free(zero); + return w; + } + + mdd_free(w); + mdd_free(zero); + free(vars); + int ind = greater_d(Form,2); + return bdd_var_with_index(mgr,ind); +} + +mdd_t* +get_neighbour(Formula_t Form, mdd_t* x,int * deg){ + + mdd_manager* mgr = Form->mgr; + lsGen gen=lsStart(Form->F); + + lsGeneric data; + lsHandle itemHandle; + mdd_t* res = mdd_zero(mgr); + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = (mdd_t*)data; + if(Common_support(mgr,l, x)){ + mdd_t* tmp=res; + mdd_t* cmp=bdd_smooth_with_cube(l,x); + res =ComposeCubes(mgr,res,cmp); + mdd_free(tmp); + mdd_free(cmp); + } + } + + lsFinish(gen); + + (*deg)= Cudd_SupportSize((DdManager *) mgr,res->node); + return res; +} + +mdd_t* +get_max_degree_(Formula_t Form, mdd_t* clause){ + int *vars=NULL; + int i,max=0,deg; + mdd_manager* mgr =Form->mgr; + int nbvar=((DdManager *)mgr)->size; + mdd_t* res=mdd_zero(mgr); + vars=Cudd_SupportIndex((DdManager *)mgr,clause->node); + + for(i=0;i max) { + max=deg; + mdd_free(res); + res=mdd_dup(v); + } + mdd_free(v); + mdd_free(nhb); + } + } + + free(vars); + return res; +} + +mdd_t* +get_max_nhb_degre(Formula_t Form, + int * vars, + int k){ + + mdd_manager* mgr =Form->mgr; + int i,deg,nbvar=((DdManager *)mgr)->size; + mdd_t* r; + + for(i=0;imgr; + int i,deg,max=0,nbvar=((DdManager *)mgr)->size; + mdd_t* w=mdd_zero(mgr); + mdd_t* zero=mdd_zero(mgr); + + vars=Cudd_SupportIndex((DdManager *) mgr, Form->V->node); + + if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 1)), + zero)){ + free(vars); + mdd_free(zero); + return w; + } + + if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 2)), + zero)){ + free(vars); + mdd_free(zero); + return w; + } + + for(i=0;i max ){ + max=deg; + mdd_free(w); + w=mdd_dup(v); + } + mdd_free(t); + mdd_free(v); + } + } + mdd_free(zero); + free(vars); + return w; +} + +int +is_empty_formula(Formula_t Form){ + mdd_manager* mgr = Form->mgr; + lsGen gen=lsStart(Form->F); + + lsGeneric data; + lsHandle itemHandle; + mdd_t* one = mdd_one(mgr); + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = (mdd_t*)data; + if(mdd_equal(l,one)){ + lsFinish(gen); + return TRUE; + } + } + mdd_free(one); + lsFinish(gen); + return FALSE; +} + + +int +D(Formula_t Form){ + mdd_manager* mgr = Form->mgr; + Formula_t F1,F2; + mdd_t* R; + mdd_t* x; + mdd_t* w; + int card_R,d_f1,d_f2; + mdd_t* zero = mdd_zero(mgr); + unsigned long lswap; + + if (is_empty_formula(Form)) { + mdd_free(zero); + return 0; + } + + if (lsLength(Form->F)==0) { + int r =Cudd_SupportSize((DdManager *)mgr, + (Form->R)->node); + card_R =(int)pow(2,r); + mdd_free(zero); + return card_R; + } + + if(disjoint_formula(Form,&F1,&F2)){ + d_f1=0;d_f2=0; + int r =Cudd_SupportSize((DdManager *)mgr, + (Form->R)->node); + card_R =(int)pow(2,r); + + // if ((rand()%K) == 0){ + if (K <= 12){ + int fd1[2]; + int fd2[2]; + + if (pipe(fd1) != 0) { + fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); + exit(1); + } + + if (pipe(fd2) != 0) { + fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); + exit(1); + } + int pid1,pid2; + + if((pid1=fork())==0){ + char buf[30]="\0"; + d_f1=D(F1); + close(fd1[0]); + sprintf(buf,"%d",d_f1); + write(fd1[1], buf, strlen(buf)); + close(fd1[1]); + //free_formula(F1); + exit(EXIT_SUCCESS); + } + + if((pid2=fork())==0){ + char buf[30]="\0"; + d_f2=D(F2); + close(fd2[0]); + sprintf(buf,"%d",d_f2); + write(fd2[1],buf,strlen(buf)); + close(fd2[1]); + //free_formula(F2); + exit(EXIT_SUCCESS); + } + + int i,s; + if(pid1 > 0){ + free_formula(F1); + char buf[30]="\0"; + i=waitpid(pid1, &s, WUNTRACED); + close(fd1[1]); + read(fd1[0],buf,30); + d_f1=atoi(buf); + close(fd1[0]); + }else{ + d_f1=D(F1); + free_formula(F1); + } + + if(pid2 > 0){ + free_formula(F2); + char buf[30]="\0"; + i=waitpid(pid2, &s, WUNTRACED); + close(fd2[1]); + read(fd2[0],buf,30); + d_f2=atoi(buf); + close(fd2[0]); + }else{ + d_f2=D(F2); + free_formula(F2); + } + } + else{ + d_f1=D(F1);free_formula(F1); + d_f2=D(F2);free_formula(F2); + } + assert( card_R*d_f1*d_f2 >= 0); + return card_R*d_f1*d_f2; + } + + if(!mdd_equal((x=_k_clause(Form,1)),zero)){ + + F1=Form; + int k; + do{ + F2 = F1; F1 =_psi(F2,x); mdd_free(x); + k=mdd_equal((x=_k_clause(F1,1)),zero); + if( F2 != Form) + free_formula(F2); + + } while(!k && !is_empty_formula(F1)); + + d_f1 =D(F1); + free_formula(F1); + mdd_free(x); + mdd_free(zero); + return d_f1; + } + + mdd_free(x); + if(!mdd_equal((x=_k_clause(Form,2)),zero)){ + w=pick_2_clause_w(Form,x); + } + else{ + w=pick_clause_w(Form); + } + + mdd_t* nw=mdd_not(w); + // if ((rand()%K) == 0){ + if (K <= 12){ + int fd1[2]; + int fd2[2]; + + if (pipe(fd1) != 0) { + fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); + exit(1); + } + + if (pipe(fd2) != 0) { + fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); + exit(1); + } + int pid1,pid2; + if((pid1=fork())==0){ + char buf[30]="\0"; + F1=_psi(Form,w); + d_f1=D(F1); + close(fd1[0]); + sprintf(buf,"%d",d_f1); + write(fd1[1],buf,strlen(buf)); + close(fd1[1]); + exit(EXIT_SUCCESS); + } + + if((pid2=fork())==0){ + char buf[30]="\0"; + F2=_psi(Form,nw); + d_f2=D(F2); + close(fd2[0]); + sprintf(buf,"%d",d_f2); + write(fd2[1],buf,strlen(buf)); + close(fd2[1]); + exit(EXIT_SUCCESS); + } + + int i,s; + if(pid1>0){ + char buf[30]="\0"; + i=waitpid(pid1,&s,WUNTRACED); + close(fd1[1]); + read(fd1[0],buf,30); + d_f1=atoi(buf); + close(fd1[0]); + }else{ + F1=_psi(Form,w); + d_f1=D(F1); + free_formula(F1); + } + + if(pid2>0){ + char buf[30]="\0"; + i=waitpid(pid2,&s, WUNTRACED); + close(fd2[1]); + read(fd2[0],buf, 30); + d_f2=atoi(buf); + close(fd2[0]); + }else{ + F2=_psi(Form,nw); + d_f2=D(F2); + free_formula(F2); + } + } + else{ + F1=_psi(Form,w); + F2=_psi(Form,nw); + d_f1=D(F1);free_formula(F1); + d_f2=D(F2);free_formula(F2); + } + + mdd_free(x); + mdd_free(w); + mdd_free(nw); + mdd_free(zero); + assert(d_f1+d_f2 >= 0); + return (d_f1+d_f2); +} + +int exit_(Formula_t Form, mdd_t* n){ + lsGen gen=lsStart(Form->F); + + lsGeneric data; + lsHandle itemHandle; + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + if(mdd_equal(data,n)){ + lsFinish(gen); + return TRUE; + } + } + lsFinish(gen); + return FALSE; +} +/* +int var_to_add(int size){ + int k,r,nb=0; + k=size; + + do{ + k=(int)k/2; + r=size % 2; + nb +=k;k +=r; + }while(k > 3); + + return nb; +} +*/ + +mdd_t* convert_dnf_cnf(Formula_t Form, + mdd_t* v1,mdd_t* v2, + mdd_t* res){ + mdd_manager* mgr = Form->mgr; + int nbvar=((DdManager *)mgr)->size; + mdd_t* tmp; + + mdd_t* ind =bdd_var_with_index(mgr,nbvar); + tmp=mdd_and(res,ind,1,1); + mdd_t*data=mdd_and(v1,v2,1,1); + (void)lsNewEnd(Form->F,mdd_and(data,ind,1,0),LS_NH); + (void)lsNewEnd(Form->F,mdd_and(ind,v1,1,0),LS_NH); + (void)lsNewEnd(Form->F,mdd_and(ind,v2,1,0),LS_NH); + mdd_free(data); + mdd_free(res); + return tmp; +} + + +void +couvert_dnf_to_cnf3(Formula_t Form, + mdd_t* clause){ + mdd_manager* mgr = Form->mgr; + int *vars=NULL; + mdd_t* res; + mdd_t* tmp=mdd_dup(clause); + + do{ + int i,t = 1; + mdd_t* v1; + mdd_t* v2; + int nbvar=((DdManager *)mgr)->size; + vars=Cudd_SupportIndex((DdManager *)mgr, + tmp->node); + int var_size=Cudd_SupportSize((DdManager *)mgr, + tmp->node); + res=mdd_one(mgr); + for(i=0;inode) > 3); + + (void)lsNewEnd(Form->F,res,LS_NH); + +} + +/* +void printf_form(Formula_t form){ + + char *filename="./test_cnf"; + FILE *cnf_file; + lsGen gen=lsStart(form->F); + lsGeneric data; + lsHandle itemHandle; + int * vars=NULL; + mdd_manager* mgr =Form->mgr; + int i,nbvar=((DdManager *)mgr)->size; + + + if(!(cnf_file = fopen(filename, "w"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + return(0); + } + + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = (mdd_t*)data; + vars=Cudd_SupportIndex((DdManager *) mgr,l); + + + + } + + lsFinish(gen); +} + +*/ +Formula_t +ReadCNF_For_Count(Ntk_Network_t *network, + st_table *nodeToMvfAigTable, + st_table *coiTable, + char *filename) { + mdd_manager* mgr; + Formula_t Form; + mdd_t* var; + FILE *fin; + char line[16384], word[1024], *lp; + int nArg,V=0,index; + int i, id, sign; + long v; + st_table* hashTable = + st_init_table(st_ptrcmp, st_ptrhash); + mdd_t* zero; + + if(!(fin = fopen(filename, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + return(0); + } + + while(fgets(line, 16384, fin)) { + + lp = sat_RemoveSpace(line); + + if(lp[0] == '\n') continue; + if(lp[0] == '#') continue; + if(lp[0] == 'c') continue; + + if(lp[0] == 'p') { + + nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); + + if(nArg < 2) { + fprintf(vis_stdout,"ERROR : Unable to read the number of "); + fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); + fclose(fin); + return(0); + } + + mgr=bdd_start(nVar); + Form=createFormula(mgr); + var=mdd_one(mgr); + zero=mdd_zero(mgr); + continue; + } + + mdd_t* data =mdd_one(mgr); + + while(1) { + lp = sat_RemoveSpace(lp); + lp = sat_CopyWord(lp, word); + + if(strlen(word)) { + id = atoi(word); + sign = 1; + + if(id != 0) { + if(id < 0) { + id = -id; + sign = 0; + } + + id <<=3; + + if(!st_lookup_int(hashTable, (char *)id, &index)) { + st_insert(hashTable, (char*)id,(char*) V); + index=V; V++; + } + + mdd_t* value= bdd_var_with_index(mgr,index); + mdd_t* d =data; + mdd_t* v =var; + + data=mdd_and(data,value,1,sign); + var=mdd_and(var,value,1,1); + mdd_free(value); + mdd_free(v); + mdd_free(d); + } + else { + + if(mdd_equal(data,zero) || + exit_(Form, data)) { + mdd_free(data); + break; + } + + + if(Cudd_SupportSize((DdManager *)mgr,data->node) > 3) + couvert_dnf_to_cnf3(Form,data); + else + (void)lsNewEnd(Form->F,data,LS_NH); + break; + } + } + } + } + mdd_free(Form->V); + // mdd_free(Form->R); + + Form->V=var; + + st_free_table(hashTable); + mdd_free(zero); + fclose(fin); + return(Form); +} + +void print_formula(Formula_t F){ + mdd_manager* mgr = F->mgr; + lsGen gen =lsStart(F->F); + + lsGeneric data; + lsHandle itemHandle; + + printf ("F->F: \n"); + while(lsNext(gen, &data, &itemHandle) == LS_OK){ + mdd_t* l = (mdd_t*)data; + bdd_print(l); + } + lsFinish(gen); + + printf ("F->R: \n"); + bdd_print(F->R); + + printf ("F->V: \n"); + bdd_print(F->V); + + getchar(); +} + + +int +main_Count_test(Ntk_Network_t *network, + st_table *nodeToMvfAigTable, + st_table *coiTable,char *filename){ + + Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable, + coiTable,filename); + srand(time(NULL)); + mdd_manager* mgr =Form->mgr; + int k=D(Form); + free_formula(Form); + bdd_end(mgr); + + return k; +} + + +Formula_t +ReadCNF_For_Count_( char *filename) { + mdd_manager* mgr; + Formula_t Form; + mdd_t* var; + FILE *fin; + char line[16384], word[1024], *lp; + int nVar, nCl, nArg,V=0,index; + int i, id, sign; + long v; + st_table* hashTable = + st_init_table(st_ptrcmp, st_ptrhash); + mdd_t* zero; + + if(!(fin = fopen(filename, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + return(0); + } + + while(fgets(line, 16384, fin)) { + + lp = sat_RemoveSpace(line); + + if(lp[0] == '\n') continue; + if(lp[0] == '#') continue; + if(lp[0] == 'c') continue; + + if(lp[0] == 'p') { + + nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); + + if(nArg < 2) { + fprintf(vis_stdout,"ERROR : Unable to read the number of "); + fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); + fclose(fin); + return(0); + } + + mgr=bdd_start(nVar); + Form=createFormula(mgr); + var=mdd_one(mgr); + zero=mdd_zero(mgr); + continue; + } + + mdd_t* data =mdd_one(mgr); + + while(1) { + lp = sat_RemoveSpace(lp); + lp = sat_CopyWord(lp, word); + + if(strlen(word)) { + id = atoi(word); + sign = 1; + + if(id != 0) { + if(id < 0) { + id = -id; + sign = 0; + } + + if(!st_lookup_int(hashTable, (char *)id, &index)) { + st_insert(hashTable, (char*)id,(char*) V); + index=V; V++; + } + + mdd_t* value= bdd_var_with_index(mgr,index); + mdd_t* d =data; + mdd_t* v =var; + + data=mdd_and(data,value,1,sign); + var=mdd_and(var,value,1,1); + mdd_free(value); + mdd_free(v); + mdd_free(d); + } + else{ + + if(mdd_equal(data,zero) || + exit_(Form, data)) { + mdd_free(data); + break; + } + (void)lsNewEnd(Form->F,data,LS_NH); break; + } + } + } + } + mdd_free(Form->V); + + Form->V=var; + + st_free_table(hashTable); + mdd_free(zero); + fclose(fin); + return(Form); +} + + + + + +int +main_Count_test_(Ntk_Network_t *network, + st_table *nodeToMvfAigTable, + st_table *coiTable,char *filename){ + + Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable, + coiTable,filename); + srand(time(NULL)); + mdd_manager* mgr =Form->mgr; + int k=D(Form); + free_formula(Form); + bdd_end(mgr); + + return k; + return 0; + +} + + + +char * +WriteCNF__rel_sat(char *filename) { + mdd_manager* mgr; + Formula_t Form; + mdd_t* var; + FILE *fin; + char line[16384], word[1024], *lp; + int nArg,V=1,index; + int i, id, sign; + long v; + st_table* hashTable = + st_init_table(st_ptrcmp, st_ptrhash); + mdd_t* zero; + char* parseBuffer=(char*)calloc(1024,sizeof(char)); + + if(!(fin = fopen(filename, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + exit(0); + } + + strcpy(parseBuffer,filename); + strcat(parseBuffer, "sat"); + char *filenamecnf ="./tmp.vis.cl"; + FILE *cnf_file; + + if(!(cnf_file = fopen(filenamecnf, "w"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + exit(0); + } + + while(fgets(line, 16384, fin)) { + + lp = sat_RemoveSpace(line); + + if(lp[0] == '\n') continue; + if(lp[0] == '#') continue; + if(lp[0] == 'c') continue; + + if(lp[0] == 'p') { + + nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); + + if(nArg < 2) { + fprintf(vis_stdout,"ERROR : Unable to read the number of "); + fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); + fclose(fin); + exit(0); + } + + continue; + } + + + while(1) { + lp = sat_RemoveSpace(lp); + lp = sat_CopyWord(lp, word); + + if(strlen(word)) { + id = atoi(word); + sign = 1; + + if(id != 0) { + + if(id < 0) { + id = -id; + sign = 0; + } + + id <<=3; + + if(!st_lookup_int(hashTable,(char *)id,&index)) { + st_insert(hashTable, (char*)id,(char*) V); + index=V; V++; + } + + if(!sign) + fprintf(cnf_file, " %d ", -index); + else + fprintf(cnf_file, " %d ", index); + } + else { + fprintf(cnf_file, "0\n"); break; + } + } + } + } + + st_free_table(hashTable); + fclose(fin); + fclose(cnf_file); + + char* Buffer=(char*)calloc(1024,sizeof(char)); + FILE* s=fopen("./tmp.vis.cnf", "w"); + fprintf (s, "p cnf %d %d \n", V-1, nCl); + fclose(s); + + strcpy(Buffer,"cat ./tmp.vis.cnf ./tmp.vis.cl > "); + strcat(Buffer, parseBuffer); + system(Buffer); + system("rm -f ./tmp.vis.cnf ./tmp.vis.cl"); + return parseBuffer; +} + + +char* +main_Count_test_sharp(char *filename, int cnt){ + + char* cnf_file=WriteCNF__rel_sat(filename); + + FILE *fp; + static char parseBuffer[1024]; + static char resBuffer[1024]; + static char rmBuffer[1024]; + int satStatus; + char* line=calloc(2048,sizeof(char)); + int num; + array_t *result = NIL(array_t); + char *tmpStr, *tmpStr1, *tmpStr2; + long solverStart; + int satTimeOutPeriod = 0; + char *fileName = NIL(char); + + +if (cnt) strcpy(parseBuffer,"sharpSAT "); +else strcpy(parseBuffer,"sharpSAT -nocount "); + + strcpy(resBuffer,filename); + strcat(resBuffer, "res"); + strcpy(rmBuffer,"rm -f "); + strcat(rmBuffer,resBuffer); + strcat(cnf_file, " > " ); + strcat(cnf_file, resBuffer); + + system(rmBuffer); + strcat(parseBuffer, cnf_file); + + //printf("\n command : %s",parseBuffer); + + satStatus = system(parseBuffer); + + if(!(fp = fopen(resBuffer, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n"); + exit(0); + } + + fgets(line, 16384, fp); + free(cnf_file); +// WriteIDL__rel_sat(filename); + return line; + +} + +char* +main_SatCount(char *filename){ + + char* cnf_file=WriteCNF__rel_sat(filename); + + FILE *fp; + static char parseBuffer[1024]; + static char resBuffer[1024]; + static char rmBuffer[1024]; + int satStatus; + char* line=calloc(2048,sizeof(char)); + int num; + array_t *result = NIL(array_t); + char *tmpStr, *tmpStr1, *tmpStr2; + long solverStart; + int satTimeOutPeriod = 0; + char *fileName = NIL(char); + + +strcpy(parseBuffer,"SatCount "); + + + strcpy(resBuffer,filename); + strcat(resBuffer, "res"); + strcpy(rmBuffer,"rm -f "); + strcat(rmBuffer,resBuffer); + strcat(cnf_file, " 40 > " ); + strcat(cnf_file, resBuffer); + + system(rmBuffer); + strcat(parseBuffer, cnf_file); + + //printf("\n command : %s",parseBuffer); + + satStatus = system(parseBuffer); + + if(!(fp = fopen(resBuffer, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n"); + exit(0); + } + + fgets(line, 16384, fp); + free(cnf_file); +// WriteIDL__rel_sat(filename); + return line; + +} + +//char * +void +WriteIDL__rel_sat(char *filename) { + mdd_manager* mgr; + Formula_t Form; + mdd_t* var; + FILE *fin; + char line[16384], word[1024], *lp; + int nArg,V=1,index; + int i, id, sign; + long v; + st_table* hashTable = + st_init_table(st_ptrcmp, st_ptrhash); + mdd_t* zero; + char* parseBuffer=(char*)calloc(1024,sizeof(char)); + + if(!(fin = fopen(filename, "r"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + exit(0); + } + + strcpy(parseBuffer,filename); + strcat(parseBuffer, "sat"); + char *filenamecnf ="./tmp.vis.idl"; + FILE *cnf_file; + + if(!(cnf_file = fopen(filenamecnf, "w"))) { + fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); + exit(0); + } + + while(fgets(line, 16384, fin)) { + + lp = sat_RemoveSpace(line); + + if(lp[0] == '\n') continue; + if(lp[0] == '#') continue; + if(lp[0] == 'c') continue; + + if(lp[0] == 'p') { + + nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); + + if(nArg < 2) { + fprintf(vis_stdout,"ERROR : Unable to read the number of "); + fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); + fclose(fin); + exit(0); + } + + continue; + } + + int k=0; + while(1) { + lp = sat_RemoveSpace(lp); + lp = sat_CopyWord(lp, word); + + if(strlen(word)) { + id = atoi(word); + sign = 1; + + if(id != 0) { + + if(id < 0) { + id = -id; + sign = 0; + } + + id <<=3; + + if(!st_lookup_int(hashTable,(char *)id,&index)) { + st_insert(hashTable, (char*)id,(char*) V); + index=V; V++; + } + + if(!sign){ + if(!k) + fprintf(cnf_file, "-1*x%d ", index); + else + fprintf(cnf_file, " -1*x%d ", index); + } + else{ + if(!k) + fprintf(cnf_file, "+1*x%d ", index); + else + fprintf(cnf_file, " +1*x%d ", index); + + } + } + else { + fprintf(cnf_file, ">= +1;\n"); break; + } + } + k++; + } + } + + st_free_table(hashTable); + fclose(fin); + fclose(cnf_file); + + // char* Buffer=(char*)calloc(1024,sizeof(char)); + + //strcpy(Buffer,"cp ./tmp.vis.idl "); + // strcat(Buffer, parseBuffer); + // system(Buffer); + // system("rm -f ./tmp.vis.cl"); + // return parseBuffer; +} Index: vis_dev/vis-2.3/src/rob/SatCountAlgo.h =================================================================== --- vis_dev/vis-2.3/src/rob/SatCountAlgo.h (revision 19) +++ vis_dev/vis-2.3/src/rob/SatCountAlgo.h (revision 19) @@ -0,0 +1,56 @@ +/**HFile*********************************************************************** + + FileName [SatCountAlgo.h] + + PackageName [rob] + + Synopsis [Headers and strcutus for Sat count Algo. package.] + + Author [Souheib Baarir] + + Copyright [Copyright (c) 2008-2009 The Regents of the Univ. 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 PARIS VI 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.] + +******************************************************************************/ + + + +#ifndef _SATCOUNT_H +#define _SATCOUNT_H + +#include "../ntk/ntkInt.h" +#include "../hrc/hrcInt.h" +#include "../fsm/fsmInt.h" +#include "../bmc/bmcInt.h" +#include "../sat/sat.h" +#include "../sat/satInt.h" +#include +#include +#include + +typedef struct form{ + lsList F; + mdd_t* V; + mdd_t* R; + mdd_manager * mgr; +} Formula; +typedef Formula* Formula_t; + + +#endif /* _SATCOUNT_H */ Index: vis_dev/vis-2.3/src/rob/rob.make =================================================================== --- vis_dev/vis-2.3/src/rob/rob.make (revision 19) +++ vis_dev/vis-2.3/src/rob/rob.make (revision 19) @@ -0,0 +1,4 @@ +CSRC += robCmd.c Robust.c SatCountAlgo.c +HEADERS += Robust.h SatCountAlgo.h + +DEPENDENCYFILES = $(CSRC) Index: vis_dev/vis-2.3/src/rob/robCmd.c =================================================================== --- vis_dev/vis-2.3/src/rob/robCmd.c (revision 19) +++ vis_dev/vis-2.3/src/rob/robCmd.c (revision 19) @@ -0,0 +1,1617 @@ + +/**CFile*********************************************************************** + + FileName [robCmd.c] + + PackageName [rob] + + Synopsis [Commands for the Robustness package.] + + Author [Souheib Baarir, Denis Poitrenaud,J.M Ilié ] + + Copyright [Copyright (c) 1994-1996 The Regents of the Univ. 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 PARIS VI 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 "Robust.h" + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ +static jmp_buf timeOutEnv; + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + + +/*************** Robustness functions ******************************************/ + +static int CommandprintmddID (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandRobustness (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandSetSafe (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandSetRequired (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandSetForbidden (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandSetInitial (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandResetRequired (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandResetForbidden (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandResetSafe (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandResetInitial (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandPrintRequired (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandPrintSafe (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandPrintForbidden (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandConvForbToProp (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandConvReachToProp (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandConvSafeToProp (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandConvReqToProp (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandConvInitToProp (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandSetLtlFormula (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandBmcRob (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandResLtlFile (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandTestCount (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandComposeGolden (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandProtectGolden (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandProtectOutput (Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandProtectRegister(Hrc_Manager_t ** hmgr,int argc, char ** argv); +static int CommandTestRob (Hrc_Manager_t ** hmgr,int argc, char ** argv); + + +/*******************************************************************************/ + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Initializes the rob package.] + + SideEffects [] + + SeeAlso [rob_End] + +******************************************************************************/ +void +Rob_Init(void) +{ + +/*************** Robustness commands ****************************************/ + Cmd_CommandAdd("printmddID", CommandprintmddID, 0); + Cmd_CommandAdd("robustness", CommandRobustness, 0); + Cmd_CommandAdd("set_safe", CommandSetSafe, 0); + Cmd_CommandAdd("set_forbidden", CommandSetForbidden, 0); + Cmd_CommandAdd("set_required", CommandSetRequired, 0); + Cmd_CommandAdd("set_init", CommandSetInitial, 0); + Cmd_CommandAdd("reset_required", CommandResetRequired, 0); + Cmd_CommandAdd("reset_forbidden",CommandResetForbidden, 0); + Cmd_CommandAdd("reset_safe", CommandResetSafe, 0); + Cmd_CommandAdd("reset_init", CommandResetInitial, 0); + Cmd_CommandAdd("print_forbidden",CommandPrintForbidden, 0); + Cmd_CommandAdd("print_required", CommandPrintRequired, 0); + Cmd_CommandAdd("print_safe", CommandPrintSafe, 0); + Cmd_CommandAdd("conv_reach_prop", CommandConvReachToProp, 0); + Cmd_CommandAdd("conv_safe_prop", CommandConvSafeToProp, 0); + Cmd_CommandAdd("conv_forb_prop", CommandConvForbToProp, 0); + Cmd_CommandAdd("conv_req_prop", CommandConvReqToProp, 0); + Cmd_CommandAdd("conv_init_prop", CommandConvInitToProp, 0); + Cmd_CommandAdd("add_ltl_formula", CommandSetLtlFormula, 0); + Cmd_CommandAdd("bmc_rob", CommandBmcRob, 0); + Cmd_CommandAdd("reset_ltl_file", CommandResLtlFile, 0); + Cmd_CommandAdd("Test_count" , CommandTestCount, 0); + Cmd_CommandAdd("compose_golden", CommandComposeGolden, 0); + Cmd_CommandAdd("protect_golden", CommandProtectGolden, 0); + Cmd_CommandAdd("protect_outputs", CommandProtectOutput, 0); + Cmd_CommandAdd("protect_registers",CommandProtectRegister,0); + Cmd_CommandAdd("test_rob", CommandTestRob, 0); + +/*****************************************************************************/ + +} + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ +void +Rob_End(void) +{ +} + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +static int +CommandprintmddID (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); + array_t *psVarsArray = Fsm_FsmReadPresentStateVars(fsm); + int arrSize = array_n( psVarsArray ); + int i; + + 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); + printf("%s : %d\n", mVar.name, mddId); + } + return 0; +} + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +static int +CommandTestCount (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + char* fichier="./test"; + int k=main_Count_test_(fichier); + printf("res= %d \n",k); + return 0; +} + + +// Reset to empty, the file +// of ltl properties. +static int +CommandResLtlFile (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + + FILE* oFile = NIL(FILE); + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "w", NIL(char *), 0); + } + else{ + oFile = Cmd_FileOpen("properties.ltl", + "w", NIL(char *), 0); + } + + fclose(oFile); + + return 0; +} + +// Add an ltl formula to the +// the file of ltl properties. +static int +CommandSetLtlFormula (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + + + char c; + int i=1; + FILE* oFile=NIL(FILE); + + if (argc < 2) { + conv_error_msg(vis_stderr, "add_ltl_formula",earg); + return 1; + } + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "f:")) != EOF) { + switch(c) { + case 'f': + oFile = Cmd_FileOpen(util_optarg, + "a+", NIL(char *), 0); + i=3; + break; + default : + break; + } + } + + if (i!=3) { + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, + "add_ltl_formula",eofile); + return 1; + } + + fprintf(oFile," %s ;\n",argv[i]); + fclose(oFile); + + return 0; +} + +// Convert the set of initial states +// to a propositional formula +// and put it in the proprerties file. +static int +CommandConvInitToProp (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + + FILE* oFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "a+", NIL(char *), 0); + } + else{ + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, "conv_init_prop",eofile); + return 1; + } + + mdd_t* set = getInitial(fsm); + if (set == NIL(mdd_t)){ + conv_error_msg(vis_stderr, "conv_init_prop",ecmd); + return 1; + } + + mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + set, "INIT", oFile); + + fclose(oFile); + return 0; +} + +// Convert the set of safe states +// to a propotitional formula +// and put it in the proprerties file. +static int +CommandConvReachToProp (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + + FILE* oFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "a+", NIL(char *), 0); + } else{ + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, + "conv_reach_prop",eofile); + return 1; + } + + mdd_t* set = getReach(fsm); + if (set == NIL(mdd_t)){ + conv_error_msg(vis_stderr, + "conv_reach_prop",ecmd); + + return 1; + } + + mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + set, "REACH", oFile); + + fclose(oFile); + return 0; +} + +// Convert the set of safe states +// to a propotitional formula +// and put it in the proprerties file. +static int +CommandConvSafeToProp (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + + FILE* oFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "a+", NIL(char *), 0); + } else{ + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, + "conv_safe_prop",eofile); + return 1; + } + + mdd_t* set = getSafe(fsm); + if (set == NIL(mdd_t)){ + conv_error_msg(vis_stderr, + "conv_safe_prop",ecmd); + + return 1; + } + + mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + set, "SAFE", oFile); + + fclose(oFile); + return 0; +} + +// Convert the set of required states +// to a propotitional formula +// and put it in the proprerties file. +static int +CommandConvReqToProp (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + FILE* oFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "a+", NIL(char *), 0); + } else{ + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, + "conv_req_prop",eofile); + return 1; + } + + mdd_t* set = getRequired(fsm); + if (set == NIL(mdd_t)){ + conv_error_msg(vis_stderr, + "conv_req_prop",ecmd); + return 1; + } + + mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + set, "REQ", oFile); + fclose(oFile); + + return 0; +} + +// Convert the set of forbidden states +// to a propotitional formula +// and put it in the proprerties file. +static int +CommandConvForbToProp (Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + FILE* oFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (argc == 2) { + oFile = Cmd_FileOpen(argv[1], + "a+", NIL(char *), 0); + } else{ + oFile = Cmd_FileOpen("properties.ltl", + "a+", NIL(char *), 0); + } + + if (oFile == NIL(FILE)) { + conv_error_msg(vis_stderr, + "conv_forb_prop",eofile); + return 1; + } + + mdd_t* set = getForbidden(fsm); + if (set == NIL(mdd_t)){ + conv_error_msg(vis_stderr, + "conv_forb_prop",ecmd); + return 1; + } + + mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + set, "FORB", oFile); + fclose(oFile); + return 0; + +} + + +// This command computes the set of forbiden states +// w.r.t a given ctl formula. This formula is read from +// a file given as a parameter. +static int +CommandSetForbidden( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + int c; + FILE* forFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c) { + case 'h': + default: + (void)error_msg(vis_stderr,"forbiden", ecmd) ; + return 1; + } + } + + if ((argc - util_optind == 0) || + (argc - util_optind > 1) ) { + (void)error_msg(vis_stderr, "forbiden",enfile ) ; + return 1; + } + + forFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + if (forFile == NIL(FILE)) { + error_msg(vis_stderr, "forbiden",eofile); + return 1; + } + + fsm->RobSets.fForb=forFile; + + if (fsm->RobSets.Forb != NIL(mdd_t)) + mdd_free(fsm->RobSets.Forb); + + mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); + array_t *careStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, careStatesArray, 0,mddOne); + + if (Fsm_FsmReadFairnessConstraint(fsm)!= + NIL(Fsm_Fairness_t)) { + Fsm_FsmComputeFairStates(fsm, + careStatesArray, + 0, + McDcLevelNone_c, + McGSH_Unassigned_c , + McBwd_c, FALSE ); + } + else { + + fsm->fairnessInfo.states = + mdd_one(Fsm_FsmReadMddManager(fsm)); + + } + + fsm->RobSets.Forb= + evaluate(fsm,forFile, + fsm->fairnessInfo.states, + Fsm_FsmReadFairnessConstraint(fsm),0); + + array_free(careStatesArray); + mdd_free(mddOne); + + + return 0; +} + +// This command sets the forbiden set of states to +// mdd_zero.This means that all states are allowed. +static int +CommandResetForbidden( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.Forb != NIL(mdd_t)) + mdd_free(fsm->RobSets.Forb); + + fsm->RobSets.Forb= + mdd_zero(Fsm_FsmReadMddManager(fsm)); + fsm->RobSets.fForb = NIL(FILE); + return 0; +} + +static int +CommandPrintForbidden( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + char formula[1024] ; + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.fForb != NIL(FILE)){ + fseek(fsm->RobSets.fForb,0,SEEK_SET); + fread (formula,sizeof(char),1024,fsm->RobSets.fForb); + printf("Forbiden is the set of states that satisfy: %s\n",formula); + } + else{ + printf("Forbiden is the set of states that satisfy: FALSE \n"); + } + + return 0; + +} + +// This command computes the set of required states +// w.r.t a given ctl formula. This formula is read from +// a file given as a parameter. +static int +CommandSetRequired( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + int c; + FILE* reqFile=NIL(FILE); + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c) { + case 'h': + default: + (void)error_msg(vis_stderr,"required", ecmd); + return 1; + } + } + + if ((argc - util_optind == 0) || + (argc - util_optind > 1) ) { + (void)error_msg(vis_stderr, "required", enfile); + return 1; + } + + reqFile = + Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + + if (reqFile == NIL(FILE)) { + error_msg(vis_stderr, "required", eofile); + return 1; + } + + fsm->RobSets.fReq=reqFile; + + if (fsm->RobSets.Req != NIL(mdd_t)) + mdd_free(fsm->RobSets.Req); + + + mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); + array_t *careStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, careStatesArray, 0,mddOne); + + if (Fsm_FsmReadFairnessConstraint(fsm)!= + NIL(Fsm_Fairness_t)) { + Fsm_FsmComputeFairStates(fsm, + careStatesArray, + 0, + McDcLevelNone_c, + McGSH_Unassigned_c , + McBwd_c, FALSE ); + } + else { + + fsm->fairnessInfo.states = + mdd_one(Fsm_FsmReadMddManager(fsm)); + + } + + fsm->RobSets.Req= + evaluate(fsm,reqFile, + fsm->fairnessInfo.states, + Fsm_FsmReadFairnessConstraint(fsm),0); + + array_free(careStatesArray); + mdd_free(mddOne); + + + return 0; + +} + +// This command sets the required set of states to +// mdd_one.This means that no restriction is given. +static int +CommandResetRequired( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.Req != NIL(mdd_t)) + mdd_free(fsm->RobSets.Req); + + fsm->RobSets.Req= + mdd_one(Fsm_FsmReadMddManager(fsm)); + fsm->RobSets.fReq = NIL(FILE); + return 0; +} + +static int +CommandPrintRequired( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + char formula[1024] ; + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.fReq != NIL(FILE)){ + fseek(fsm->RobSets.fReq,0,SEEK_SET); + fread (formula,sizeof(char),1024,fsm->RobSets.fReq); + printf("Required is the set of states that satisfy: %s\n",formula); + } + else{ + printf("Required is the set of states that satisfy: TRUE \n"); + } + + return 0; + +} +// This command computes the set of safe states +// w.r.t a given ctl formula. This formula is read from +// a file given as a parameter. +static int +CommandSetSafe( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + FILE *safeFile=NIL(FILE); + int c; + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "h")) != EOF) { + switch(c) { + case 'h': + default: + (void) error_msg(vis_stderr, "safe", ecmd); + return 1; + } + } + + if ((argc - util_optind == 0) || + (argc - util_optind > 1) ) { + (void)error_msg(vis_stderr, "safe", enfile); + return 1; + } + + safeFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0); + + if (safeFile == NIL(FILE)) { + error_msg(vis_stderr, "safe", eofile); + return 1; + } + + + + fsm->RobSets.fSafe=safeFile; + + if (fsm->RobSets.Safe != NIL(mdd_t)) + mdd_free(fsm->RobSets.Safe); + + mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); + array_t *careStatesArray = array_alloc(mdd_t *, 0); + array_insert(mdd_t *, careStatesArray, 0,mddOne); + + if (Fsm_FsmReadFairnessConstraint(fsm)!= + NIL(Fsm_Fairness_t)) { + Fsm_FsmComputeFairStates(fsm, + careStatesArray, + 0, + McDcLevelNone_c, + McGSH_Unassigned_c , + McBwd_c, FALSE ); + } + else { + + fsm->fairnessInfo.states = + mdd_one(Fsm_FsmReadMddManager(fsm)); + + } + + fsm->RobSets.Safe= + evaluate(fsm,safeFile, + fsm->fairnessInfo.states, + Fsm_FsmReadFairnessConstraint(fsm),0); + + array_free(careStatesArray); + mdd_free(mddOne); + + return 0; +} + +// This command sets the safe set of states to +// the reachable set of states (without bit-flips). +static int +CommandResetSafe( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.Safe != NIL(mdd_t)) + mdd_free(fsm->RobSets.Safe); + + 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; + fsm->RobSets.fSafe = NIL(FILE); + + return 0; +} + +static int +CommandPrintSafe( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + char formula[1024] ; + + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->RobSets.fSafe != NIL(FILE)){ + fseek(fsm->RobSets.fSafe,0,SEEK_SET); + fread (formula,sizeof(char),1024,fsm->RobSets.fSafe); + printf("Safe is the set of states that satisfy: %s\n",formula); + } + else{ + printf("Safe is the set of states that is orginaly rechable from the design \n"); + } + + return 0; + +} + +// This command computes the disign's initial set of states, +// starting from the reachable states and +// taking into acount all bit-flips arriving on non +// protected sequecial elements. The set of protected sequencial +// elements are given as parameter in a given file. +static int +CommandSetInitial(Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + FILE *proFile=NIL(FILE); + FILE *forFile=NIL(FILE); + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + static int verbosityLevel=0; + static int printStep=0; + int formula=0; + long initialTime; + long finalTime; + int c; + int fmodel = 1; + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + util_getopt_reset(); + while ((c = util_getopt(argc, argv, "hg:s:v:f:m:")) != EOF) { + switch(c) { + case 'g' : + proFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0); + if (proFile == NIL(FILE)) { + error_msg(vis_stderr, "init", eiofile); + return 1; + } + break; + case 'f' : + forFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0); + if (forFile == NIL(FILE)) { + error_msg(vis_stderr, "init", eiofile); + return 1; + } + formula=1; + break; + case 's' : + printStep = atoi(util_optarg); break; + case 'v' : + verbosityLevel = atoi(util_optarg); break; + case 'm' : + + if (strcmp(util_optarg, "usut") == 0) {fmodel = 2;break;} + if (strcmp(util_optarg, "usmt") == 0) {fmodel = 3;break;} + if (strcmp(util_optarg, "msut") == 0) {fmodel = 4;break;} + if (strcmp(util_optarg, "msmt") == 0) {fmodel = 5;break;} + + + case 'h': + default : error_msg(vis_stderr, "init", eicmd); return 1; + } + } + + if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){ + mdd_free(fsm->reachabilityInfo.initialStates); + fsm->reachabilityInfo.initialStates=NIL(mdd_t); + } + + if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){ + mdd_free(fsm->reachabilityInfo.reachableStates); + fsm->reachabilityInfo.reachableStates=NIL(mdd_t); + } + + initialTime = util_cpu_time(); + (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); + + if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){ + mdd_free(fsm->reachabilityInfo.initialStates); + fsm->reachabilityInfo.initialStates=NIL(mdd_t); + } + + //mdd_free(fsm->reachabilityInfo.initialStates); + + if (fmodel == 1) + fsm->reachabilityInfo.initialStates= + compute_error_states(fsm,fsm->reachabilityInfo.reachableStates, + verbosityLevel,printStep, proFile); + + if (fmodel == 2) + fsm->reachabilityInfo.initialStates= + error_states_us_ut(fsm,fsm->reachabilityInfo.reachableStates,proFile); + + if (fmodel == 3) + fsm->reachabilityInfo.initialStates= + error_states_us_mt(fsm,fsm->reachabilityInfo.reachableStates, proFile); + + if (fmodel == 4) + fsm->reachabilityInfo.initialStates= + error_states_ms_ut(fsm,fsm->reachabilityInfo.reachableStates, proFile); + + if (fmodel == 5){ + (void)Fsm_FsmComputeInitialStates(fsm); + mdd_t* S0 = mdd_dup(fsm->reachabilityInfo.initialStates); + mdd_free(fsm->reachabilityInfo.initialStates); + fsm->reachabilityInfo.initialStates= + error_states_ms_mt(fsm,S0,fsm->reachabilityInfo.reachableStates, proFile); + mdd_free(S0); + } + + + mdd_free(fsm->reachabilityInfo.reachableStates); + fsm->reachabilityInfo.reachableStates=NIL(mdd_t); + + if(!formula) { + fsm->reachabilityInfo.reachableStates= + Fsm_FsmComputeReachableStates(fsm,0,0, + 0,0, 0, + 0, 0, Fsm_Rch_Default_c, + 0,0, NIL(array_t), + 0, NIL(array_t)); + } + else { + mdd_t* newinit_tmp=evaluate(fsm,forFile,NIL(mdd_t), + Fsm_FsmReadFairnessConstraint(fsm),0); + mdd_t* newinit=mdd_and(fsm->reachabilityInfo.initialStates, + newinit_tmp,1,1); + + mdd_free(newinit_tmp); + mdd_free(fsm->reachabilityInfo.initialStates); + fsm->reachabilityInfo.initialStates=newinit; + mdd_free(fsm->reachabilityInfo.reachableStates); + fsm->reachabilityInfo.reachableStates= + 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(); + + if(verbosityLevel){ + (void) fprintf(vis_stdout,"********************************\n"); + print_number_of_states("Error states = ", fsm, + fsm->reachabilityInfo.initialStates); + print_number_of_states("States reachable from error states = ", fsm, + fsm->reachabilityInfo.reachableStates); + print_number_of_states("Reachable states whithout faults = ", fsm, + fsm->RobSets.originalreachableStates); + (void) fprintf(vis_stdout, "%-50s%15g\n", + "Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + +// printf("-----------------------------------------------\n"); +// print_bdd(Fsm_FsmReadMddManager(fsm), fsm->reachabilityInfo.reachableStates); +// bdd_print(fsm->reachabilityInfo.reachableStates); +// printf("-----------------------------------------------\n"); + } + + return 0; +} + +// This command sets the design's initial set of states +// to the original one (without bit-flips). It also computes +// the reachable states according to this initial set. +static int +CommandResetInitial( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){ + mdd_free(fsm->reachabilityInfo.initialStates); + fsm->reachabilityInfo.initialStates=NIL(mdd_t); + } + + 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 0; +} + +// This command computes the design's robustness. +// This needs the evaluation of the diffirent ctl formulae : +// 1- A[!forbiden U Required & A[!forbiden U Safe]] +// 2- A[!forbiden U Required & E[!forbiden U Safe]] +// 3- E[!forbiden U Required & A[!forbiden U Safe]] +// 4- E[!forbiden U Required & E[!forbiden U Safe]]. + +static int +CommandRobustness( Hrc_Manager_t ** hmgr, + int argc, + char ** argv) { + int c; + mdd_t *reachableStates = NIL(mdd_t); + mdd_t *initialStates; + long initialTime; + long finalTime; + static int verbosityLevel; + static int printStep; + static int timeOutPeriod; + Fsm_Fsm_t *fsm = + Fsm_HrcManagerReadCurrentFsm(*hmgr); + static int reorderFlag; + static int reorderThreshold; + static int shellFlag; + static int depthValue; + static int incrementalFlag; + static int approxFlag; + static int ardc; + static int recompute; + Fsm_RchType_t rchType; + + static int req; + FILE *reqFile=NIL(FILE); + static int forb; + FILE *forFile=NIL(FILE); + static int pro; + FILE *proFile=NIL(FILE); + static int fair; + FILE *fairFile=NIL(FILE); + static int init=0; + boolean rob1 = 0; + + FILE *guideFile = NIL(FILE); /* file of hints for guided search */ + array_t *guideArray = NIL(array_t); + + Img_MethodType imgMethod; + mdd_t * error_states; + mdd_t *reach, *notReach; /* Etats accessibles du systï¿œme original */ + mdd_t *tmp1, *tmp2; + EpDouble *error = EpdAlloc(); + EpDouble *err = EpdAlloc(); + EpDouble *nbstates = EpdAlloc(); + EpDouble *rch = EpdAlloc(); + EpDouble *error0 = EpdAlloc(); + char percent[1024]; + char nbst[1024]; + mdd_t *forbiden, *required, *notforbiden,*fairS; + mdd_t *XU_notForb_And_Safe; + mdd_t *Req_And_XU_notForb_And_Safe; + mdd_t *Setformula; + mdd_t *res,*res_r,*res_0; + Fsm_Fairness_t * fairCons=NIL(Fsm_Fairness_t); + + + verbosityLevel = 0; + printStep = 0; + timeOutPeriod = 0; + shellFlag = 0; + depthValue = 0; + incrementalFlag = 0; + rchType = Fsm_Rch_Default_c; + approxFlag = 0; + ardc = 0; + recompute = 0; + + if(fsm == NIL(Fsm_Fsm_t)) + return 1; + + util_getopt_reset(); + + while ((c = util_getopt(argc, argv, "hs:r:v:")) != EOF) { + switch(c) { + case 's': + printStep = atoi(util_optarg); + break; + case 'v': + verbosityLevel = atoi(util_optarg); + break; + case 'r': + rob1= atoi(util_optarg); + break; + case 'h': + default : + error_msg(vis_stderr, "rob", ercmd); return 1; + } + } + + mdd_t* Forb = getForbidden(fsm); + mdd_t* Req = getRequired(fsm); + mdd_t* Safe = getSafe(fsm); + mdd_t* Init = getInitial(fsm) ; + mdd_t* Orig = getReachOrg(fsm); + + if ((Fsm_FsmReadFairnessConstraint(fsm))!= + NIL(Fsm_Fairness_t)) { + compute_fair(fsm,verbosityLevel); + } + else { + fsm->fairnessInfo.states = + mdd_one(Fsm_FsmReadMddManager(fsm)); + } + + get_number_of_states(fsm,fsm->reachabilityInfo.reachableStates, error); + get_number_of_states(fsm,Init, error0); + get_number_of_states(fsm,Orig, rch); + + //Compute robustness 1 + if(rob1) + { + (void) fprintf(vis_stdout,"********************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = AG[Safe]]\n"); + initialTime = util_cpu_time(); + Setformula= mdd_not(evaluate_EF(fsm, Safe, fsm->fairnessInfo.states, + verbosityLevel)); + finalTime = util_cpu_time(); + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); + mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + // EG + (void) fprintf(vis_stdout,"********************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = EG[Safe]] \n"); + + initialTime = util_cpu_time(); + + Setformula=evaluate_EG(fsm, mdd_not(Safe), fsm->fairnessInfo.states,NIL(Fsm_Fairness_t),verbosityLevel); + finalTime = util_cpu_time(); + + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + + } + else{ + (void) fprintf(vis_stdout,"********************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = A[!forbiden U Required & A[!forbiden U Safe]]\n"); + initialTime = util_cpu_time(); + Setformula= evaluate_Formula_AF_AF (fsm, Req,Forb,Safe, verbosityLevel ); + finalTime = util_cpu_time(); + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); + mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + + + (void) fprintf(vis_stdout,"********************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = E[!forbiden U Required & A[!forbiden U Safe]] \n"); + + initialTime = util_cpu_time(); + Setformula=evaluate_Formula_EF_AF (fsm, Req,Forb,Safe, verbosityLevel ); + finalTime = util_cpu_time(); + + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + } + /* + (void) fprintf(vis_stdout,"********************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = A[!forbiden U Required & E[!forbiden U Safe]] \n"); + initialTime = util_cpu_time(); + Setformula=evaluate_Formula_AF_EF (fsm, Req,Forb,Safe, verbosityLevel ); + finalTime = util_cpu_time(); + + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + + (void) fprintf(vis_stdout,"*******************************\n"); + (void) fprintf(vis_stdout, + "Dealing with F = E[!forbiden U Required & E[!forbiden U Safe]] \n"); + initialTime = util_cpu_time(); + Setformula=evaluate_Formula_EF_EF (fsm, Req,Forb,Safe, verbosityLevel ); + finalTime = util_cpu_time(); + + res_0=mdd_and(Init, Setformula, 1, 1); + res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula); + + get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0); + EpdGetString(nbstates, nbst);EpdCopy(error0, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states satisfying F = ", + nbst,percent); + + get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r); + EpdGetString(nbstates, nbst); EpdCopy(rch, err); EpdSubtract2(err, nbstates); + EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent); + (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", + " --Error states originaly reachable by the design and satisfying F = ", + nbst,percent); + + + (void) fprintf(vis_stdout, "%-50s%15g\n", + " Analysis time = ", + (double)(finalTime-initialTime)/1000.0); + */ + mdd_free(Forb); + mdd_free(Req); + mdd_free(Safe); + mdd_free(Init); + mdd_free(Orig); + + alarm(0); + return (0); + + + return 1; +} + + +// (Adpateted) Bounded model checking +// command for robustness properties. +static int +CommandBmcRob( Hrc_Manager_t ** hmgr, + int argc, + char ** argv){ + Ntk_Network_t *network; + BmcOption_t *options; + int i; + array_t *formulaArray; + array_t *LTLformulaArray; + bAig_Manager_t *manager; + array_t *constraintArray = NIL(array_t); + +/* Virer dans un premier temps par Denis, seule les techniques non-sat sont intégrées + dans cette version. +*/ + + + // Parse command line options. + if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { + return 1; + } + + // Read the network + network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + if (network == NIL(Ntk_Network_t)) { + (void) fprintf(vis_stdout, "** bmc_rob error: No network\n"); + BmcOptionFree(options); + return 1; + } + + manager = Ntk_NetworkReadMAigManager(network); + if (manager == NIL(mAig_Manager_t)) { + (void) fprintf(vis_stdout, + "** bmc_rob error: run build_partition_maigs command first\n"); + BmcOptionFree(options); + return 1; + } + + + // We need the bdd when building the transition + // relation of the automaton + if(options->inductiveStep !=0){ + Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t); + + designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + if (designFsm == NIL(Fsm_Fsm_t)) { + return 1; + } + } + + formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); + if (formulaArray == NIL(array_t)) { + (void) fprintf(vis_stderr, + "** bmc error: error in parsing CTL* Fromula from file\n"); + BmcOptionFree(options); + return 1; + } + + if (array_n(formulaArray) == 0) { + (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); + BmcOptionFree(options); + Ctlsp_FormulaArrayFree(formulaArray); + return 1; + } + LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); + Ctlsp_FormulaArrayFree(formulaArray); + if (LTLformulaArray == NIL(array_t)){ + (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); + BmcOptionFree(options); + return 1; + } + + if (options->fairFile != NIL(FILE)) { + constraintArray = BmcReadFairnessConstraints(options->fairFile); + if(constraintArray == NIL(array_t)){ + Ctlsp_FormulaArrayFree(LTLformulaArray); + BmcOptionFree(options); + return 1; + } + if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){ + Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray, + constraintArray); + Ctlsp_FormulaArrayFree(constraintArray); + constraintArray = NIL(array_t); + } + } + + // Call the BMC function. + for (i = 0; i < array_n(LTLformulaArray); i++) { + Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, + LTLformulaArray, i); + callBmcRob(network, ltlFormula, constraintArray, options); + } + + // Free used memeory + if (constraintArray != NIL(array_t)){ + Ctlsp_FormulaArrayFree(constraintArray); + } + Ctlsp_FormulaArrayFree(LTLformulaArray); + BmcOptionFree(options); + fflush(vis_stdout); + fflush(vis_stderr); + alarm(0); + + return 0; +} +static int +CommandComposeGolden(Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + printf("*** Rob3 ***\n"); + //Former root + Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr); + if(Hrc_ManagerFindModelByName(*hmgr, "rob3_model") != NIL(Hrc_Model_t)) + { + fprintf(vis_stderr, "Composition already made, read a new design\n"); + return 1; + + } + //New Root + Hrc_Model_t * newRootModel = Hrc_ModelAlloc(*hmgr, "rob3_model"); + + build_golden_faulty_compo(*hmgr,rootNode,newRootModel); + + return 0; +} +static int +CommandProtectGolden(Hrc_Manager_t ** hmgr, + int argc, char ** argv) +{ + +Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr); +if(rootNode == NIL(Hrc_Node_t)){ + printf("Please build the network first"); + return 1; +} +char * name = (char*) malloc(10); +sprintf(name,"golden"); +Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name); +if(goldenNode == NIL(Hrc_Node_t)){ + printf("Please build the network first"); + return 1; +} + +FILE * oFile = Cmd_FileOpen("protect_golden.reg","w", NIL(char *), 0); +Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); +array_t *psVarsArray = Fsm_FsmReadPresentStateVars(fsm); +mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); +int nbLatches = 0; +int k; +int arrSize = array_n( psVarsArray ); + for ( k = 0 ; k < arrSize ; k++ ) { + int mddId = array_fetch( int, psVarsArray,k); + mvar_type mVar = array_fetch(mvar_type, + mdd_ret_mvar_list(mddManager),mddId); + if(strstr(mVar.name,"faulty") == NULL){ + fprintf(oFile,"%s\n",mVar.name); + nbLatches++; + } + } + st_generator * gen; + Hrc_Latch_t * latch; + Hrc_NodeForEachLatch(rootNode, gen,name,latch){ + fprintf(oFile,"%s\n",name); + } + +/* +nbLatches += Hrc_NodeReadNumLatches(rootNode); + + int i; + Var_Variable_t * var; + Hrc_NodeForEachFormalOutput(rootNode,i,var){ + fprintf(oFile,"%s\n", Var_VariableReadName(var)); + } + nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode); +*/ + printf("file protect_golden.reg created (contains %d registers)\n",nbLatches); + fclose(oFile); + return 0; + +} + +static int +CommandProtectOutput(Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr); + if(rootNode == NIL(Hrc_Node_t)){ + printf("Please build the network first\n"); + return 1; + } + FILE * oFile = Cmd_FileOpen("protect_output.reg","w", NIL(char *), 0); + int nbLatches = 0; + int i; + Var_Variable_t * var; + Hrc_NodeForEachFormalOutput(rootNode,i,var){ + fprintf(oFile,"%s\n", Var_VariableReadName(var)); + } + nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode); + printf("file protect_output created (contains %d signals)\n",nbLatches); + fclose(oFile); + return 0; + +} +static int +CommandProtectRegister(Hrc_Manager_t ** hmgr, + int argc, char ** argv){ + Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr); + if(rootNode == NIL(Hrc_Node_t)){ + printf("Please build the network first"); + return 1; + } + + FILE * oFile = Cmd_FileOpen("register.reg","w", NIL(char *), 0); + + int nbLatches = generateProtectFile(rootNode, oFile,""); + char * name; + st_generator * gen; + Hrc_Latch_t * latch; + + nbLatches += Hrc_NodeReadNumLatches(rootNode); + + printf("file register.reg created (contains %d registers)\n",nbLatches); + fclose(oFile); + return 0; + +} +static int +CommandTestRob(Hrc_Manager_t ** hmgr, + int argc, char ** argv) +{ + + + Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); + mdd_t *initialStates = getInitial(fsm); + mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); + +FILE * oFile = Cmd_FileOpen("init.prop","w", NIL(char *), 0); + +mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + initialStates, "INIT",oFile); + + array_t * golden = array_alloc(int, 0); + array_t *psVarsArray = Fsm_FsmReadPresentStateVars(fsm); + int arrSize = array_n( psVarsArray ); + int i; + 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); + if(strstr(mVar.name,"golden") !=NULL) + { + printf("-> %s\n",mVar.name); + array_insert_last(int,golden,mddId); + } +} + +mdd_print_array (golden); +mdd_t * tmp1 = mdd_cproject(mddManager,initialStates,golden); +mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm), + tmp1, "GOLDEN",oFile); + fclose(oFile); + return 0; + +} + Index: vis_dev/vis-2.3/src/rob/tags =================================================================== --- vis_dev/vis-2.3/src/rob/tags (revision 19) +++ vis_dev/vis-2.3/src/rob/tags (revision 19) @@ -0,0 +1,129 @@ +!_TAG_FILE_FORMAT 2 /extended format; --format=1 will not append ;" to lines/ +!_TAG_FILE_SORTED 1 /0=unsorted, 1=sorted, 2=foldcase/ +!_TAG_PROGRAM_AUTHOR Darren Hiebert /dhiebert@users.sourceforge.net/ +!_TAG_PROGRAM_NAME Exuberant Ctags // +!_TAG_PROGRAM_URL http://ctags.sourceforge.net /official site/ +!_TAG_PROGRAM_VERSION 5.6 // +CommandBmcRob robCmd.c /^CommandBmcRob( Hrc_Manager_t ** hmgr,$/;" f file: +CommandComposeGolden robCmd.c /^CommandComposeGolden(Hrc_Manager_t ** hmgr,$/;" f file: +CommandConvForbToProp robCmd.c /^CommandConvForbToProp (Hrc_Manager_t ** hmgr,$/;" f file: +CommandConvInitToProp robCmd.c /^CommandConvInitToProp (Hrc_Manager_t ** hmgr,$/;" f file: +CommandConvReachToProp robCmd.c /^CommandConvReachToProp (Hrc_Manager_t ** hmgr,$/;" f file: +CommandConvReqToProp robCmd.c /^CommandConvReqToProp (Hrc_Manager_t ** hmgr,$/;" f file: +CommandConvSafeToProp robCmd.c /^CommandConvSafeToProp (Hrc_Manager_t ** hmgr,$/;" f file: +CommandPrintForbidden robCmd.c /^CommandPrintForbidden( Hrc_Manager_t ** hmgr,$/;" f file: +CommandPrintRequired robCmd.c /^CommandPrintRequired( Hrc_Manager_t ** hmgr,$/;" f file: +CommandPrintSafe robCmd.c /^CommandPrintSafe( Hrc_Manager_t ** hmgr,$/;" f file: +CommandProtectGolden robCmd.c /^CommandProtectGolden(Hrc_Manager_t ** hmgr,$/;" f file: +CommandProtectOutput robCmd.c /^CommandProtectOutput(Hrc_Manager_t ** hmgr,$/;" f file: +CommandProtectRegister robCmd.c /^CommandProtectRegister(Hrc_Manager_t ** hmgr,$/;" f file: +CommandResLtlFile robCmd.c /^CommandResLtlFile (Hrc_Manager_t ** hmgr,$/;" f file: +CommandResetForbidden robCmd.c /^CommandResetForbidden( Hrc_Manager_t ** hmgr,$/;" f file: +CommandResetInitial robCmd.c /^CommandResetInitial( Hrc_Manager_t ** hmgr,$/;" f file: +CommandResetRequired robCmd.c /^CommandResetRequired( Hrc_Manager_t ** hmgr,$/;" f file: +CommandResetSafe robCmd.c /^CommandResetSafe( Hrc_Manager_t ** hmgr,$/;" f file: +CommandRobustness robCmd.c /^CommandRobustness( Hrc_Manager_t ** hmgr,$/;" f file: +CommandSetForbidden robCmd.c /^CommandSetForbidden( Hrc_Manager_t ** hmgr,$/;" f file: +CommandSetInitial robCmd.c /^CommandSetInitial(Hrc_Manager_t ** hmgr,$/;" f file: +CommandSetLtlFormula robCmd.c /^CommandSetLtlFormula (Hrc_Manager_t ** hmgr,$/;" f file: +CommandSetRequired robCmd.c /^CommandSetRequired( Hrc_Manager_t ** hmgr,$/;" f file: +CommandSetSafe robCmd.c /^CommandSetSafe( Hrc_Manager_t ** hmgr,$/;" f file: +CommandTestCount robCmd.c /^CommandTestCount (Hrc_Manager_t ** hmgr,$/;" f file: +CommandprintmddID robCmd.c /^CommandprintmddID (Hrc_Manager_t ** hmgr,$/;" f file: +Common_support SatCountAlgo.c /^Common_support(mdd_manager* mgr,$/;" f +ComposeCubes SatCountAlgo.c /^ComposeCubes(mdd_manager* mgr,$/;" f +D SatCountAlgo.c /^D(Formula_t Form){$/;" f +F SatCountAlgo.h /^ lsList F; $/;" m struct:form +Formula SatCountAlgo.h /^} Formula;$/;" t typeref:struct:form +Formula_t SatCountAlgo.h /^typedef Formula* Formula_t;$/;" t +Get_support SatCountAlgo.c /^Get_support(mdd_manager* mgr,mdd_t* l){$/;" f +K SatCountAlgo.c /^const int K=5;$/;" v +R SatCountAlgo.h /^ mdd_t* R;$/;" m struct:form +ReadCNF_For_Count SatCountAlgo.c /^ReadCNF_For_Count(Ntk_Network_t *network,$/;" f +ReadCNF_For_Count_ SatCountAlgo.c /^ReadCNF_For_Count_( char *filename) {$/;" f +Rob_End robCmd.c /^Rob_End(void)$/;" f +Rob_Init robCmd.c /^Rob_Init(void)$/;" f +V SatCountAlgo.h /^ mdd_t* V;$/;" m struct:form +WriteCNF__rel_sat SatCountAlgo.c /^WriteCNF__rel_sat(char *filename) {$/;" f +WriteIDL__rel_sat SatCountAlgo.c /^WriteIDL__rel_sat(char *filename) {$/;" f +_ROB_H Robust.h 35;" d +_SATCOUNT_H SatCountAlgo.h 35;" d +_d SatCountAlgo.c /^_d(Formula_t Form, mdd_t* x){$/;" f +_k_clause SatCountAlgo.c /^_k_clause(Formula_t Form, int k){$/;" f +_psi SatCountAlgo.c /^_psi(Formula_t For,mdd_t* d){$/;" f +build_golden_faulty_compo Robust.c /^Hrc_Node_t * build_golden_faulty_compo($/;" f +callBmcRob Robust.c /^callBmcRob( Ntk_Network_t *network,$/;" f +clone_formula SatCountAlgo.c /^clone_formula(Formula_t form){$/;" f +compute_error_states Robust.c /^mdd_t* compute_error_states(Fsm_Fsm_t *fsm, mdd_t* reachable, $/;" f +compute_fair Robust.c /^compute_fair(Fsm_Fsm_t *fsm,int verbosityLevel){$/;" f +conv_error_msg Robust.c /^conv_error_msg(FILE* f, char* cmd, type_err e){$/;" f +convert_dnf_cnf SatCountAlgo.c /^mdd_t* convert_dnf_cnf(Formula_t Form,$/;" f +couvert_dnf_to_cnf3 SatCountAlgo.c /^couvert_dnf_to_cnf3(Formula_t Form,$/;" f +createFormula SatCountAlgo.c /^createFormula(mdd_manager * mgr){$/;" f +determine_non_protected_registers Robust.c /^determine_non_protected_registers(Fsm_Fsm_t *fsm, FILE *f) {$/;" f +disjoint_formula SatCountAlgo.c /^disjoint_formula(Formula_t Form,$/;" f +earg Robust.h /^ earg,$/;" e enum:__anon1 +ecmd Robust.h /^ ecmd,$/;" e enum:__anon1 +eicmd Robust.h /^ eicmd,$/;" e enum:__anon1 +eiofile Robust.h /^ eiofile,$/;" e enum:__anon1 +enfile Robust.h /^ enfile,$/;" e enum:__anon1 +eofile Robust.h /^ eofile,$/;" e enum:__anon1 +ercmd Robust.h /^ ercmd$/;" e enum:__anon1 +error_msg Robust.c /^error_msg(FILE* f, char* cmd, type_err e){$/;" f +error_states Robust.c /^mdd_t* error_states(Fsm_Fsm_t *fsm, $/;" f +error_states_ms_mt Robust.c /^mdd_t* error_states_ms_mt(Fsm_Fsm_t *fsm, $/;" f +error_states_ms_ut Robust.c /^mdd_t* error_states_ms_ut(Fsm_Fsm_t *fsm, $/;" f +error_states_us_mt Robust.c /^mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, $/;" f +error_states_us_ut Robust.c /^mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, $/;" f +evaluate Robust.c /^mdd_t* evaluate(Fsm_Fsm_t *fsm,FILE* ctlfile,mdd_t* fairS,$/;" f +evaluate_AU Robust.c /^mdd_t* evaluate_AU(Fsm_Fsm_t *fsm, mdd_t* inv, $/;" f +evaluate_EF Robust.c /^mdd_t* evaluate_EF(Fsm_Fsm_t *fsm, mdd_t *target,$/;" f +evaluate_EG Robust.c /^mdd_t* evaluate_EG(Fsm_Fsm_t *fsm, mdd_t *invariant,$/;" f +evaluate_EU Robust.c /^mdd_t* evaluate_EU(Fsm_Fsm_t *fsm, mdd_t* inv, $/;" f +evaluate_Formula_AF_AF Robust.c /^evaluate_Formula_AF_AF (Fsm_Fsm_t *fsm,$/;" f +evaluate_Formula_AF_EF Robust.c /^evaluate_Formula_AF_EF (Fsm_Fsm_t *fsm,$/;" f +evaluate_Formula_EF_AF Robust.c /^evaluate_Formula_EF_AF (Fsm_Fsm_t *fsm,$/;" f +evaluate_Formula_EF_EF Robust.c /^evaluate_Formula_EF_EF (Fsm_Fsm_t *fsm,$/;" f +exit_ SatCountAlgo.c /^int exit_(Formula_t Form, mdd_t* n){$/;" f +form SatCountAlgo.h /^typedef struct form{ $/;" s +free_formula SatCountAlgo.c /^void free_formula(Formula_t F){$/;" f +generateProtectFile Robust.c /^int generateProtectFile($/;" f +getForbidden Robust.c /^getForbidden(Fsm_Fsm_t *fsm){$/;" f +getInitial Robust.c /^getInitial(Fsm_Fsm_t *fsm) {$/;" f +getReach Robust.c /^getReach(Fsm_Fsm_t *fsm) {$/;" f +getReachOrg Robust.c /^getReachOrg( Fsm_Fsm_t *fsm ){$/;" f +getRequired Robust.c /^getRequired(Fsm_Fsm_t *fsm){$/;" f +getSafe Robust.c /^getSafe( Fsm_Fsm_t *fsm ){$/;" f +get_max_degree_ SatCountAlgo.c /^get_max_degree_(Formula_t Form, mdd_t* clause){$/;" f +get_max_nhb_degre SatCountAlgo.c /^get_max_nhb_degre(Formula_t Form, $/;" f +get_neighbour SatCountAlgo.c /^get_neighbour(Formula_t Form, mdd_t* x,int * deg){$/;" f +get_number_of_states Robust.c /^void get_number_of_states(Fsm_Fsm_t *fsm, mdd_t* b, EpDouble* ep) {$/;" f +get_var_sup SatCountAlgo.c /^get_var_sup (Formula_t Form){$/;" f +get_w SatCountAlgo.c /^get_w(Formula_t Form,$/;" f +getbddvars Robust.c /^getbddvars( mdd_manager *mgr,$/;" f file: +greater_d SatCountAlgo.c /^greater_d(Formula_t Form,int k){$/;" f +inj_ms Robust.c /^mdd_t* inj_ms(mdd_manager *mddManager, $/;" f +inj_register Robust.c /^static mdd_t* inj_register(mdd_manager *mddManager, mdd_t* S, mdd_t* r) {$/;" f file: +inj_us Robust.c /^mdd_t* inj_us(mdd_manager *mddManager, array_t* bdd_not_protected, mdd_t* S) {$/;" f +is_empty_formula SatCountAlgo.c /^is_empty_formula(Formula_t Form){$/;" f +main_Count_test SatCountAlgo.c /^main_Count_test(Ntk_Network_t *network,$/;" f +main_Count_test_ SatCountAlgo.c /^main_Count_test_(Ntk_Network_t *network,$/;" f +main_Count_test_sharp SatCountAlgo.c /^main_Count_test_sharp(char *filename, int cnt){$/;" f +main_SatCount SatCountAlgo.c /^main_SatCount(char *filename){$/;" f +mdd_FunctionPrint Robust.c /^mdd_FunctionPrint(mdd_manager *mgr ,$/;" f +mdd_FunctionPrintMain Robust.c /^mdd_FunctionPrintMain(mdd_manager *mgr ,$/;" f +mdd_restrict Robust.c /^mdd_restrict(mdd_manager* mgr,$/;" f file: +mdd_restrict SatCountAlgo.c /^mdd_restrict(mdd_manager* mgr,$/;" f file: +mgr SatCountAlgo.h /^ mdd_manager * mgr;$/;" m struct:form +mymddGetVarById Robust.c 34;" d file: +nCl SatCountAlgo.c /^int nVar=0, nCl=0;$/;" v +nVar SatCountAlgo.c /^int nVar=0, nCl=0;$/;" v +pick_2_clause_w SatCountAlgo.c /^pick_2_clause_w(Formula_t Form, mdd_t* clause){$/;" f +pick_clause_w SatCountAlgo.c /^pick_clause_w(Formula_t Form){$/;" f +print_formula SatCountAlgo.c /^void print_formula(Formula_t F){$/;" f +print_number_of_states Robust.c /^void print_number_of_states(char* msg, Fsm_Fsm_t *fsm, mdd_t* b) {$/;" f +print_variables_info Robust.c /^void print_variables_info(Fsm_Fsm_t *fsm) {$/;" f +sat_Add_Blocking_Clauses Robust.c /^sat_Add_Blocking_Clauses( Ntk_Network_t *network,$/;" f +sat_Add_Blocking_Clauses_2 Robust.c /^sat_Add_Blocking_Clauses_2(Ntk_Network_t *network,$/;" f +timeOutEnv robCmd.c /^static jmp_buf timeOutEnv;$/;" v file: +type_err Robust.h /^} type_err;$/;" t typeref:enum:__anon1