Changeset 30

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:

• debug/debug.c (modified) (5 diffs)
• debug/debugUtilities.c (modified) (1 diff)
• rob/Robust.c (modified) (2 diffs)

vis_dev/vis-2.3/src/debug/debug.c

@@ -5 +5 @@
   PackageName [debug]
 
-  Synopsis    [Test package initialization, ending, and the command test.]
+  Synopsis    [Debug package initialization, ending, and the command debug]
 
   Author      [Originated from SIS.]
@@ -31 +31 @@
 
 #include "debugInt.h"
-
+#include "imgInt.h"
+#include "partInt.h"
 static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
 
@@ -61 +62 @@
 
 static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
-static int Commandtransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 
 
@@ -88 +89 @@
    */
   Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
-  Cmd_CommandAdd("transition",  Commandtransition,      0);
+  Cmd_CommandAdd("_transition",  CommandTransition,      0);
 
 }
@@ -271 +272 @@
 }
 
-
-
-/**Function********************************************************************
-
-  Synopsis [Returns a BDD array from an Mvf array]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static array_t *
-markGetBddArray(array_t *mvfArray,  mdd_manager* mddManager)
+/******************************************/
+/* function that build a bdd for the      */
+/* simple example :                       */
+/*     (state = 0) -> !(state = 1)        */
+/******************************************/
+mdd_t * buildDummyBdd(mdd_manager   *mddManager)
 {
-    int           i,phase;
-    array_t *bddArray;
-    Mvf_Function_t *mvf;
-
-    FILE*  oFile;
-  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
-
-    bddArray = array_alloc(bdd_node *,0);
- printf("mvf array : %d \n" , array_n(mvfArray));
-
-    arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
-        mdd_t     *mddTemp;
-        bdd_node    *ddNode;
-
-        mddTemp = array_fetch(mdd_t *, mvf, 1);
-        ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
-        bdd_ref(ddNode);
-    mdd_FunctionPrintMain(mddManager, mddTemp, "TRANS", oFile);
-    printf("\n");
-        ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
-    printf("%d --->",i);
-    bdd_print(mddTemp);
-    printf("\n");
-        array_insert_last(bdd_node *, bddArray, ddNode);
-    }
-    fclose(oFile);
-    return bddArray;
-}
-
-/**Function********************************************************************
-
-  Synopsis [Returns a BDD array given an integer array of variable indices.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static bdd_node **
-BddNodeArrayFromIdArray(
-  bdd_manager   *ddManager,
-  array_t       *idArray)
-{
-    bdd_node **xvars;
-    int i,id;
-    int nvars = array_n(idArray);
-
-    xvars = ALLOC(bdd_node *, nvars);
-    if (xvars == NULL)
-        return NULL;
-
-    for(i = 0; i < nvars; i++) {
-        id = array_fetch(int,idArray,i);
-        xvars[i] = bdd_bdd_ith_var(ddManager,id);
-        bdd_ref(xvars[i]);
-    }
-    return xvars;
-}
-/**Function********************************************************************
-
-  Synopsis [Compute the relation between an array of function and a 
-  corresponding array of variables. A BDD is returned which represents
-  AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-static bdd_node *
-computeTransitionRelationWithIds(
-  bdd_manager   *ddManager,
-  array_t       *nextBdds,
-  bdd_node      **yVars,
-  int           nVars)
-{
-    bdd_node    *ddtemp1, *ddtemp2;
-    bdd_node    *oldTR, *fn;
-    int                  i;
-
-
-    oldTR = bdd_read_one(ddManager);
-
-    for(i = 0; i < nVars; i++) {
-        ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
-
-    bdd_print(ddtemp2);
-        fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
-        bdd_ref(fn);
-        ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
-        bdd_ref(ddtemp1);
-        bdd_recursive_deref(ddManager,fn);
-        bdd_recursive_deref(ddManager,oldTR);
-        oldTR = ddtemp1;
-    }
-    return oldTR;
-}
-/*
-static mdd_t *
-computeTransitionRelationWithIds_mdd(
-  mdd_manager   *ddManager,
-  array_t       *nextBdds,
-  mdd_t **yVars,
-  int           nVars)
-{
-    mdd_t       *ddtemp1, *ddtemp2;
-    mdd_t       *oldTR, *fn;
-    int                  i;
-
-
-    oldTR = mdd_one(ddManager);
-
-    for(i = 0; i < nVars; i++) {
-        ddtemp2  = array_fetch(mdd_t *, nextBdds, i);
-
-        fn = mdd_xnor(ddtemp2,yVars[i],1,1);
-        ddtemp1 = mdd_and(oldTR,fn,1,1);
-        mdd_free(oldTR);
-        oldTR = ddtemp1;
-    }
-
-        mdd_ref(ddtemp1);
-        mdd_free(fn);
-    return oldTR;
-}
-*/
-
-static int 
-Commandtransition (Hrc_Manager_t ** hmgr,
-                   int  argc, char ** argv){
-  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
-  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
-  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
-  printf("** TRANSITION RELATION **\n");
-  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
-  printf("model : %s\n", Hrc_NodeReadModelName(n));
-
-   graph_t *partition;
-   bdd_node *tranRelation;
-   bdd_node **xVars,**yVars, **piVars;
-
-   
-   array_t *tranFunArray, *leaveIds;
-   array_t *nextBdds, *nextMvfs;
-   int nVars, nPi;
-
-   
-    /*
-     * tranFunArray is a list of next state funs.
-     */
-
-    tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
-    char *name;
-    int i;
-    arrayForEachItem(char*, tranFunArray, i, name){
-      Ntk_Node_t * latch = Ntk_NetworkFindNodeByName(network, name);
-      printf("%s : mddid : %d\n",name , Ntk_NodeReadMddId(latch) );
-      //int c =   Ntk_NodeReadMddId(latch);
-    }
-
- array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
-  int                  arrSize = array_n( psVarsArray );
-
-  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 : mddid %d\n", mVar.name, mddId);
-  }
-
- array_t *nsVarsArray  =  Fsm_FsmReadNextStateVars(fsm);
-arrSize = array_n( nsVarsArray );
-
-  for ( i = 0 ; i < arrSize ; ++i ) {
-    int      mddId = array_fetch( int, nsVarsArray, i );
-    mvar_type mVar = array_fetch(mvar_type, 
-                                 mdd_ret_mvar_list(mddManager),mddId);
-    printf("%s : mddid %d\n", mVar.name, mddId);
-  }
-
-
-    leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
-                          Fsm_FsmReadPresentStateVars(fsm));
-    /*
-     * Get the BDDs for transition functions.Duplicate functions are returned.
-     */
-    partition = Fsm_FsmReadPartition(fsm);
-    nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
-                                            NIL(mdd_t));
-
-    array_free(leaveIds);
-    array_free(tranFunArray);
-
- Mvf_Function_t *mvf = array_fetch(Mvf_Function_t *,nextMvfs,1);
- mdd_t * recupdd = array_fetch(mdd_t *, mvf, 0);
- printf("plop\n");
- bdd_print(recupdd);
-/** Build cex **/
-
-/** state0 **/
+/** state0 = 0 **/
  mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
- printf("****************\n");
- bdd_print (s0);
  mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
- printf("****************\n");
- bdd_print (s1);
- mdd_t * and =  mdd_one(mddManager);
- and = mdd_and(s0,s1,1,1);
- mdd_t* reach = mdd_one(mddManager);
- reach = Fsm_FsmReadReachableStates(fsm);
- mdd_t * state0 =  mdd_and(and,reach,1,1);
-/** next state1 **/
+ mdd_t * state0 =  mdd_one(mddManager);
+ state0 = mdd_and(s0,s1,1,1);
+/** state1 = 1 **/
  mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
  mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
- mdd_t * state1 = mdd_and(ns0,ns1,1,1);
-/** new rel **/
- mdd_t * rel =  mdd_or(state0,state1,0,0);
-
-
-
-
-// Get image_info 
-
-  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
-
-   Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
-
-array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
- arrayForEachItem(mdd_t *, transRelation, i, recupdd){
- printf("****************\n");
-
-    bdd_print(recupdd);
-}
-  mdd_t* new_rel = mdd_and(recupdd,rel,1,1);
-FILE * oFile = fopen("relation.bdd","w");
- mdd_FunctionPrintMain(mddManager, recupdd, "TRANS", oFile);
- mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
- mdd_FunctionPrintMain(mddManager, rel, "REL", oFile);
- mdd_FunctionPrintMain(mddManager, new_rel, "new_rel", oFile);
-
-fclose(oFile);
-array_insert(mdd_t*,transRelation,0,new_rel);
-Img_ReplacePartitionedTransitionRelation(imageInfo, transRelation,0);
- printf("****************\n");
-
-Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
-
- arrayForEachItem(mdd_t *, transRelation, i, recupdd){
- printf("****************\n");
- FsmResetReachabilityFields(fsm, 0);
-
-    bdd_print(recupdd);
-}
+ mdd_t * state1 =  mdd_one(mddManager);
+ state1 = mdd_and(ns0,ns1,1,1);
+/** state = 0) -> !(state = 1) **/
+ mdd_t * rel =  mdd_one(mddManager);
+ rel =  mdd_or(state0,state1,0,0);
+ 
+ return rel;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Implements the transtion command.]
+
+  CommandName [_transition]
+
+  CommandSynopsis [compute new transition relation]
+
+  CommandArguments [\[-h\] \[-v\]]
+  
+  CommandDescription [This command create a new transition relation that is a
+  and of the Bdd of the old one and an other bdd.
+  <p>
+
+  Command options:<p>  
+
+  <dl>
+  <dt> -h
+  <dd> Print the command usage.
+  </dl>
+
+  <dt> -v
+  <dd> Verbose mode.
+  </dl>
+  ]
+
+  SideEffects [Change the fsm]
+
+******************************************************************************/
+
+static int 
+CommandTransition (Hrc_Manager_t ** hmgr,
+                   int  argc, char ** argv){
+int            c;
+int            verbose = 0;              /* default value */
 
 /*
-FILE * dotFile = fopen("relation.dot","w");
-
-mdd_dump_dot(reach,NIL(char),dotFile);
-fclose(dotFile);
-*/
-//    nextBdds = markGetBddArray(nextMvfs,mddManager);
-
-    Mvf_FunctionArrayFree(nextMvfs);
-/*
- // Get the DdNodes for all the variables.
-
-    piVars = BddNodeArrayFromIdArray(mddManager, 
-                                         Fsm_FsmReadInputVars(fsm));
-    xVars = BddNodeArrayFromIdArray(mddManager, 
-                                        Fsm_FsmReadPresentStateVars(fsm));
-    yVars = BddNodeArrayFromIdArray(mddManager,
-                                        Fsm_FsmReadNextStateVars(fsm));
-
-    nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
-    nPi = array_n(Fsm_FsmReadInputVars(fsm));
-
-    // Compute the transition relation 
-    tranRelation = computeTransitionRelationWithIds(mddManager, nextBdds,
-                                                    yVars, nVars);
+ * Parse command line options.
  */
-/*
- FILE*  oFile;
-  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
-mdd_FunctionPrintMain(mddManager, tranRelation, "TRANS", oFile);
- fclose(oFile);
- */
-  return 0;
-}
-
-
+util_getopt_reset();
+while ((c = util_getopt(argc, argv, "vh")) != EOF) {
+  switch(c) {
+    case 'v':
+      verbose = 1;
+      break;
+    case 'h':
+      goto usage;
+    default:
+      goto usage;
+  }
+}
+
+if (verbose) {
+  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
+}
+
+Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
+Ntk_Network_t  *network      = NIL(Ntk_Network_t);
+mdd_manager    *mddManager; 
+mdd_t          *rel          = NIL(mdd_t);
+graph_t        *partition;
+int            i;
+/******************/
+network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if(network == NIL(Ntk_Network_t))
+        return 1;
+fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+if(fsm ==  NIL(Fsm_Fsm_t))
+        return 1;
+mddManager   = Fsm_FsmReadMddManager(fsm);
+
+
+
+/**********   Build cex  ***********/
+/* Here add the function           */
+/* that build the Bdd to and       */
+/* with the transtion relation     */
+/***********************************/
+rel = buildDummyBdd(mddManager);
+if(rel == NIL(mdd_t))
+{
+        fprintf(vis_stdout,"Problem when building the new relation bdd");
+        return 1;
+}
+
+/** Get image_info **/
+Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
+partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
+/**** The complete transtion relation ****/
+// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
+/*****************************************/
+/*** For each latch rebuild the transition function ***/
+/*** mvf table is composed of mdd for each possible ***/
+/*** value of the latch                             ***/
+ImgFunctionData_t * functionData = &(imageInfo->functionData);
+array_t *roots = functionData->roots;
+array_t *rangeVarMddIdArray = functionData->rangeVars;
+char * nodeName;
+arrayForEachItem(char *, roots, i, nodeName) {
+        /* The new relation */ 
+        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
+    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
+    int mddId = array_fetch(int, rangeVarMddIdArray, i);
+        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
+        mdd_t * n_relation = mdd_and(relation,rel,1,1);
+    /* Build for each possible value */
+        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
+        int v ;
+        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
+        for(v = 0; v<nbValue;v++)
+        {
+                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
+                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
+                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
+                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
+
+        }
+        /* Replace the function for the latch */
+        Part_VertexSetFunction(vertex, newMvf);
+//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
+        Mvf_FunctionFree(mvf);
+}
+
+/** Change the fsm **/
+fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
+mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
+Fsm_FsmComputeReachableStates(fsm,0,verbose,
+                                      0,0, 0,
+                                      0, 0, Fsm_Rch_Default_c,
+                                      0,1, NIL(array_t),
+                                      (verbose > 0),  NIL(array_t));
+if(verbose)
+        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
+/** Change Image Info **/
+Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
+                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
+                                          (void *) partition);
+
+
+return 0;               /* normal exit */
+
+usage:
+(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
+(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
+(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
+return 1;               /* error exit */
+
+}
+
+

vis_dev/vis-2.3/src/debug/debugUtilities.c

@@ -60 +60 @@
   return;
 }
-

vis_dev/vis-2.3/src/rob/Robust.c

@@ -636 +636 @@
   mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
   
-  // construction du vecteur des registres non protégés
+  // construction du vecteur des registres non prot?g?s
   array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protect);
   array_t *bdd_vars = getbddvars(mddManager, nonProtectedIdArray); 
-  // sauvegarde des états initiaux et accessibles courants
+  // 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)
+  // initialisation du r?sultat ? inj_us(S)
   mdd_t *res = inj_us(mddManager, bdd_vars, S);
 
@@ -789 +789 @@
 // McGSH_Unassigned_c         // Mc_GSHScheduleType GSHschedule)
                              McGSH_old_c);
-  
+ 
   CtlpFormulaFree(ctlFormula);  
   free(ctlNormalFormulaArray);