Changeset 30 for vis_dev/vis-2.3


Ignore:
Timestamp:
Dec 8, 2011, 4:38:48 PM (13 years ago)
Author:
cecile
Message:

We can now change the transition relation

Location:
vis_dev/vis-2.3/src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/src/debug/debug.c

    r27 r30  
    55  PackageName [debug]
    66
    7   Synopsis    [Test package initialization, ending, and the command test.]
     7  Synopsis    [Debug package initialization, ending, and the command debug]
    88
    99  Author      [Originated from SIS.]
     
    3131
    3232#include "debugInt.h"
    33 
     33#include "imgInt.h"
     34#include "partInt.h"
    3435static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
    3536
     
    6162
    6263static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
    63 static int Commandtransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
     64static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6465
    6566
     
    8889   */
    8990  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
    90   Cmd_CommandAdd("transition",  Commandtransition,      0);
     91  Cmd_CommandAdd("_transition",  CommandTransition,      0);
    9192
    9293}
     
    271272}
    272273
    273 
    274 
    275 /**Function********************************************************************
    276 
    277   Synopsis [Returns a BDD array from an Mvf array]
    278 
    279   SideEffects [None]
    280 
    281   SeeAlso     []
    282 
    283 ******************************************************************************/
    284 static array_t *
    285 markGetBddArray(array_t *mvfArray,  mdd_manager* mddManager)
     274/******************************************/
     275/* function that build a bdd for the      */
     276/* simple example :                       */
     277/*     (state = 0) -> !(state = 1)        */
     278/******************************************/
     279mdd_t * buildDummyBdd(mdd_manager   *mddManager)
    286280{
    287     int           i,phase;
    288     array_t *bddArray;
    289     Mvf_Function_t *mvf;
    290 
    291     FILE*  oFile;
    292   oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
    293 
    294     bddArray = array_alloc(bdd_node *,0);
    295  printf("mvf array : %d \n" , array_n(mvfArray));
    296 
    297     arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
    298         mdd_t     *mddTemp;
    299         bdd_node    *ddNode;
    300 
    301         mddTemp = array_fetch(mdd_t *, mvf, 1);
    302         ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
    303         bdd_ref(ddNode);
    304     mdd_FunctionPrintMain(mddManager, mddTemp, "TRANS", oFile);
    305     printf("\n");
    306         ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
    307     printf("%d --->",i);
    308     bdd_print(mddTemp);
    309     printf("\n");
    310         array_insert_last(bdd_node *, bddArray, ddNode);
    311     }
    312     fclose(oFile);
    313     return bddArray;
    314 }
    315 
    316 /**Function********************************************************************
    317 
    318   Synopsis [Returns a BDD array given an integer array of variable indices.]
    319 
    320   SideEffects [None]
    321 
    322   SeeAlso     []
    323 
    324 ******************************************************************************/
    325 static bdd_node **
    326 BddNodeArrayFromIdArray(
    327   bdd_manager   *ddManager,
    328   array_t       *idArray)
    329 {
    330     bdd_node **xvars;
    331     int i,id;
    332     int nvars = array_n(idArray);
    333 
    334     xvars = ALLOC(bdd_node *, nvars);
    335     if (xvars == NULL)
    336         return NULL;
    337 
    338     for(i = 0; i < nvars; i++) {
    339         id = array_fetch(int,idArray,i);
    340         xvars[i] = bdd_bdd_ith_var(ddManager,id);
    341         bdd_ref(xvars[i]);
    342     }
    343     return xvars;
    344 }
    345 /**Function********************************************************************
    346 
    347   Synopsis [Compute the relation between an array of function and a
    348   corresponding array of variables. A BDD is returned which represents
    349   AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
    350 
    351   SideEffects []
    352 
    353   SeeAlso     []
    354 
    355 ******************************************************************************/
    356 static bdd_node *
    357 computeTransitionRelationWithIds(
    358   bdd_manager   *ddManager,
    359   array_t       *nextBdds,
    360   bdd_node      **yVars,
    361   int           nVars)
    362 {
    363     bdd_node    *ddtemp1, *ddtemp2;
    364     bdd_node    *oldTR, *fn;
    365     int                  i;
    366 
    367 
    368     oldTR = bdd_read_one(ddManager);
    369 
    370     for(i = 0; i < nVars; i++) {
    371         ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
    372 
    373     bdd_print(ddtemp2);
    374         fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
    375         bdd_ref(fn);
    376         ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
    377         bdd_ref(ddtemp1);
    378         bdd_recursive_deref(ddManager,fn);
    379         bdd_recursive_deref(ddManager,oldTR);
    380         oldTR = ddtemp1;
    381     }
    382     return oldTR;
    383 }
    384 /*
    385 static mdd_t *
    386 computeTransitionRelationWithIds_mdd(
    387   mdd_manager   *ddManager,
    388   array_t       *nextBdds,
    389   mdd_t **yVars,
    390   int           nVars)
    391 {
    392     mdd_t       *ddtemp1, *ddtemp2;
    393     mdd_t       *oldTR, *fn;
    394     int                  i;
    395 
    396 
    397     oldTR = mdd_one(ddManager);
    398 
    399     for(i = 0; i < nVars; i++) {
    400         ddtemp2  = array_fetch(mdd_t *, nextBdds, i);
    401 
    402         fn = mdd_xnor(ddtemp2,yVars[i],1,1);
    403         ddtemp1 = mdd_and(oldTR,fn,1,1);
    404         mdd_free(oldTR);
    405         oldTR = ddtemp1;
    406     }
    407 
    408         mdd_ref(ddtemp1);
    409         mdd_free(fn);
    410     return oldTR;
    411 }
    412 */
    413 
    414 static int
    415 Commandtransition (Hrc_Manager_t ** hmgr,
    416                    int  argc, char ** argv){
    417   Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    418   Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
    419   mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
    420   printf("** TRANSITION RELATION **\n");
    421   Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
    422   printf("model : %s\n", Hrc_NodeReadModelName(n));
    423 
    424    graph_t *partition;
    425    bdd_node *tranRelation;
    426    bdd_node **xVars,**yVars, **piVars;
    427 
    428    
    429    array_t *tranFunArray, *leaveIds;
    430    array_t *nextBdds, *nextMvfs;
    431    int nVars, nPi;
    432 
    433    
    434     /*
    435      * tranFunArray is a list of next state funs.
    436      */
    437 
    438     tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
    439     char *name;
    440     int i;
    441     arrayForEachItem(char*, tranFunArray, i, name){
    442       Ntk_Node_t * latch = Ntk_NetworkFindNodeByName(network, name);
    443       printf("%s : mddid : %d\n",name , Ntk_NodeReadMddId(latch) );
    444       //int c =   Ntk_NodeReadMddId(latch);
    445     }
    446 
    447  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
    448   int                  arrSize = array_n( psVarsArray );
    449 
    450   for ( i = 0 ; i < arrSize ; ++i ) {
    451     int      mddId = array_fetch( int, psVarsArray, i );
    452     mvar_type mVar = array_fetch(mvar_type,
    453                                  mdd_ret_mvar_list(mddManager),mddId);
    454     printf("%s : mddid %d\n", mVar.name, mddId);
    455   }
    456 
    457  array_t *nsVarsArray  =  Fsm_FsmReadNextStateVars(fsm);
    458 arrSize = array_n( nsVarsArray );
    459 
    460   for ( i = 0 ; i < arrSize ; ++i ) {
    461     int      mddId = array_fetch( int, nsVarsArray, i );
    462     mvar_type mVar = array_fetch(mvar_type,
    463                                  mdd_ret_mvar_list(mddManager),mddId);
    464     printf("%s : mddid %d\n", mVar.name, mddId);
    465   }
    466 
    467 
    468     leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
    469                           Fsm_FsmReadPresentStateVars(fsm));
    470     /*
    471      * Get the BDDs for transition functions.Duplicate functions are returned.
    472      */
    473     partition = Fsm_FsmReadPartition(fsm);
    474     nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
    475                                             NIL(mdd_t));
    476 
    477     array_free(leaveIds);
    478     array_free(tranFunArray);
    479 
    480  Mvf_Function_t *mvf = array_fetch(Mvf_Function_t *,nextMvfs,1);
    481  mdd_t * recupdd = array_fetch(mdd_t *, mvf, 0);
    482  printf("plop\n");
    483  bdd_print(recupdd);
    484 /** Build cex **/
    485 
    486 /** state0 **/
     281/** state0 = 0 **/
    487282 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
    488  printf("****************\n");
    489  bdd_print (s0);
    490283 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
    491  printf("****************\n");
    492  bdd_print (s1);
    493  mdd_t * and =  mdd_one(mddManager);
    494  and = mdd_and(s0,s1,1,1);
    495  mdd_t* reach = mdd_one(mddManager);
    496  reach = Fsm_FsmReadReachableStates(fsm);
    497  mdd_t * state0 =  mdd_and(and,reach,1,1);
    498 /** next state1 **/
     284 mdd_t * state0 =  mdd_one(mddManager);
     285 state0 = mdd_and(s0,s1,1,1);
     286/** state1 = 1 **/
    499287 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
    500288 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
    501  mdd_t * state1 = mdd_and(ns0,ns1,1,1);
    502 /** new rel **/
    503  mdd_t * rel =  mdd_or(state0,state1,0,0);
    504 
    505 
    506 
    507 
    508 // Get image_info
    509 
    510   Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
    511 
    512    Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
    513 
    514 array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
    515  arrayForEachItem(mdd_t *, transRelation, i, recupdd){
    516  printf("****************\n");
    517 
    518     bdd_print(recupdd);
    519 }
    520   mdd_t* new_rel = mdd_and(recupdd,rel,1,1);
    521 FILE * oFile = fopen("relation.bdd","w");
    522  mdd_FunctionPrintMain(mddManager, recupdd, "TRANS", oFile);
    523  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
    524  mdd_FunctionPrintMain(mddManager, rel, "REL", oFile);
    525  mdd_FunctionPrintMain(mddManager, new_rel, "new_rel", oFile);
    526 
    527 fclose(oFile);
    528 array_insert(mdd_t*,transRelation,0,new_rel);
    529 Img_ReplacePartitionedTransitionRelation(imageInfo, transRelation,0);
    530  printf("****************\n");
    531 
    532 Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
    533 
    534  arrayForEachItem(mdd_t *, transRelation, i, recupdd){
    535  printf("****************\n");
    536  FsmResetReachabilityFields(fsm, 0);
    537 
    538     bdd_print(recupdd);
    539 }
     289 mdd_t * state1 =  mdd_one(mddManager);
     290 state1 = mdd_and(ns0,ns1,1,1);
     291/** state = 0) -> !(state = 1) **/
     292 mdd_t * rel =  mdd_one(mddManager);
     293 rel =  mdd_or(state0,state1,0,0);
     294 
     295 return rel;
     296}
     297
     298
     299/**Function********************************************************************
     300
     301  Synopsis    [Implements the transtion command.]
     302
     303  CommandName [_transition]
     304
     305  CommandSynopsis [compute new transition relation]
     306
     307  CommandArguments [\[-h\] \[-v\]]
     308 
     309  CommandDescription [This command create a new transition relation that is a
     310  and of the Bdd of the old one and an other bdd.
     311  <p>
     312
     313  Command options:<p> 
     314
     315  <dl>
     316  <dt> -h
     317  <dd> Print the command usage.
     318  </dl>
     319
     320  <dt> -v
     321  <dd> Verbose mode.
     322  </dl>
     323  ]
     324
     325  SideEffects [Change the fsm]
     326
     327******************************************************************************/
     328
     329static int
     330CommandTransition (Hrc_Manager_t ** hmgr,
     331                   int  argc, char ** argv){
     332int            c;
     333int            verbose = 0;              /* default value */
    540334
    541335/*
    542 FILE * dotFile = fopen("relation.dot","w");
    543 
    544 mdd_dump_dot(reach,NIL(char),dotFile);
    545 fclose(dotFile);
    546 */
    547 //    nextBdds = markGetBddArray(nextMvfs,mddManager);
    548 
    549     Mvf_FunctionArrayFree(nextMvfs);
    550 /*
    551  // Get the DdNodes for all the variables.
    552 
    553     piVars = BddNodeArrayFromIdArray(mddManager,
    554                                          Fsm_FsmReadInputVars(fsm));
    555     xVars = BddNodeArrayFromIdArray(mddManager,
    556                                         Fsm_FsmReadPresentStateVars(fsm));
    557     yVars = BddNodeArrayFromIdArray(mddManager,
    558                                         Fsm_FsmReadNextStateVars(fsm));
    559 
    560     nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
    561     nPi = array_n(Fsm_FsmReadInputVars(fsm));
    562 
    563     // Compute the transition relation
    564     tranRelation = computeTransitionRelationWithIds(mddManager, nextBdds,
    565                                                     yVars, nVars);
     336 * Parse command line options.
    566337 */
    567 /*
    568  FILE*  oFile;
    569   oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
    570 mdd_FunctionPrintMain(mddManager, tranRelation, "TRANS", oFile);
    571  fclose(oFile);
    572  */
    573   return 0;
    574 }
    575 
    576 
     338util_getopt_reset();
     339while ((c = util_getopt(argc, argv, "vh")) != EOF) {
     340  switch(c) {
     341    case 'v':
     342      verbose = 1;
     343      break;
     344    case 'h':
     345      goto usage;
     346    default:
     347      goto usage;
     348  }
     349}
     350
     351if (verbose) {
     352  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
     353}
     354
     355Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
     356Ntk_Network_t  *network      = NIL(Ntk_Network_t);
     357mdd_manager    *mddManager;
     358mdd_t          *rel          = NIL(mdd_t);
     359graph_t        *partition;
     360int            i;
     361/******************/
     362network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     363if(network == NIL(Ntk_Network_t))
     364        return 1;
     365fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
     366if(fsm ==  NIL(Fsm_Fsm_t))
     367        return 1;
     368mddManager   = Fsm_FsmReadMddManager(fsm);
     369
     370
     371
     372/**********   Build cex  ***********/
     373/* Here add the function           */
     374/* that build the Bdd to and       */
     375/* with the transtion relation     */
     376/***********************************/
     377rel = buildDummyBdd(mddManager);
     378if(rel == NIL(mdd_t))
     379{
     380        fprintf(vis_stdout,"Problem when building the new relation bdd");
     381        return 1;
     382}
     383
     384/** Get image_info **/
     385Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
     386partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
     387/**** The complete transtion relation ****/
     388// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
     389/*****************************************/
     390/*** For each latch rebuild the transition function ***/
     391/*** mvf table is composed of mdd for each possible ***/
     392/*** value of the latch                             ***/
     393ImgFunctionData_t * functionData = &(imageInfo->functionData);
     394array_t *roots = functionData->roots;
     395array_t *rangeVarMddIdArray = functionData->rangeVars;
     396char * nodeName;
     397arrayForEachItem(char *, roots, i, nodeName) {
     398        /* The new relation */
     399        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
     400    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
     401    int mddId = array_fetch(int, rangeVarMddIdArray, i);
     402        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
     403        mdd_t * n_relation = mdd_and(relation,rel,1,1);
     404    /* Build for each possible value */
     405        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
     406        int v ;
     407        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
     408        for(v = 0; v<nbValue;v++)
     409        {
     410                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
     411                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
     412                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
     413                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
     414
     415        }
     416        /* Replace the function for the latch */
     417        Part_VertexSetFunction(vertex, newMvf);
     418//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
     419        Mvf_FunctionFree(mvf);
     420}
     421
     422/** Change the fsm **/
     423fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
     424mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
     425Fsm_FsmComputeReachableStates(fsm,0,verbose,
     426                                      0,0, 0,
     427                                      0, 0, Fsm_Rch_Default_c,
     428                                      0,1, NIL(array_t),
     429                                      (verbose > 0),  NIL(array_t));
     430if(verbose)
     431        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
     432/** Change Image Info **/
     433Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
     434                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
     435                                          (void *) partition);
     436
     437
     438return 0;               /* normal exit */
     439
     440usage:
     441(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
     442(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
     443(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
     444return 1;               /* error exit */
     445
     446}
     447
     448
  • vis_dev/vis-2.3/src/debug/debugUtilities.c

    r27 r30  
    6060  return;
    6161}
    62 
  • vis_dev/vis-2.3/src/rob/Robust.c

    r21 r30  
    636636  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
    637637 
    638   // construction du vecteur des registres non protégés
     638  // construction du vecteur des registres non prot?g?s
    639639  array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protect);
    640640  array_t *bdd_vars = getbddvars(mddManager, nonProtectedIdArray);
    641   // sauvegarde des états initiaux et accessibles courants
     641  // sauvegarde des ?tats initiaux et accessibles courants
    642642  mdd_t *tmpInit = fsm->reachabilityInfo.initialStates;
    643643  mdd_t *tmpReach = mdd_dup(fsm->reachabilityInfo.reachableStates);
    644   // initialisation du résultat à inj_us(S)
     644  // initialisation du r?sultat ? inj_us(S)
    645645  mdd_t *res = inj_us(mddManager, bdd_vars, S);
    646646
     
    789789// McGSH_Unassigned_c         // Mc_GSHScheduleType GSHschedule)
    790790                             McGSH_old_c);
    791   
     791 
    792792  CtlpFormulaFree(ctlFormula); 
    793793  free(ctlNormalFormulaArray);
Note: See TracChangeset for help on using the changeset viewer.