Changeset 100 for vis_dev/vis-2.3

Timestamp:

Jul 18, 2012, 4:46:43 PM (12 years ago)

Author:

cecile

Message:

exemple transition with cex

Location:

vis_dev/vis-2.3

Files:

• models/transition/cex.ctl (modified) (1 diff)
• models/transition/cex.v (modified) (1 diff)
• src/debug/debug.c (modified) (7 diffs)
• src/mc/mcCmd.c (modified) (1 diff)

vis_dev/vis-2.3/models/transition/cex.ctl

@@ -1 @@
-(((cex.state[2:0] = 7  * cex.s2 = 1 ) )  * S.state[1:0] = 0)  * 
-EX( S.state[1:0] = 1 ) ; 
+#cex.state[2:0] = 7  * cex.s2 = 1 * S.state[1:0] = 0 * EX(cex.state[2:0] = 2 *
+# S.state[1:0] = 1) ;
+
+#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 * S.state[1:0] = 0));
+#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 ));
+#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 1 ));
+#cex.s2 = 1 * EX(cex.s2 = 0 * EX(cex.s3 = 1 ));
+cex.state[2:0] = 7 * cex.s2 = 1 * S.state[1:0] = 0 * (EX(cex.state[2:0] = 2
+* cex.s2 = 0 * S.state[1:0] = 1 * EX(cex.s2 = 0)));
+ cex.s2 = 1 * S.state[1:0] = 0 * (EX( cex.s2 = 1 * S.state[1:0] = 0 * EX(S.state[1:0] = 0 * cex.s3 = 0 
+* EX(S.state[1:0] =  0 * EX(S.state[1:0] = 1)))));
+
+

vis_dev/vis-2.3/models/transition/cex.v

@@ -18 +18 @@
     state[2] = $ND(0,1);
     if(state == 3)
+        begin
       s2 = 0;
+          s3 = $ND(0,1);
+          s4 = $ND(0,1);
+        end
     else
+          begin
       s2 = 1;
-  s3 = $ND(0,1);
-  s4 = $ND(0,1);
+          s3 = 0;
+      s4 = 0;
+          end
   end
 

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

@@ -371 +371 @@
          if(verbose)
                 (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
-                latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
+                latches \n",cnfClauses->noOfClauses,st_count(CoiTable));
   
     
@@ -970 +970 @@
 /***********************************/
 //rel = buildDummyBdd(mddManager);
-array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
-array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
-array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
-printf("Next Names\n");
-printStringArray(nextNames);
-printf("Next Ids\n");
-printIntArray(nextIds);
-printf("Current Ids\n");
-printIntArray(currentIds);
-Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
  graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
-
-lsGen gen;
-vertex_t *vertexPtr;
-
-
-//foreach_vertex(part, gen, vertexPtr) {
-//      if (PartVertexReadName(vertexPtr) != NIL(char)) {
-//        (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr));
-//      }
-//}
-vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
-Mvf_Function_t*  vertexFunction = PartVertexReadFunction(v_s2);
-  if (vertexFunction != NIL(Mvf_Function_t)) {
-printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
-}
-else
-  printf("no fonction");
-
+ vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
 Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
  mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
@@ -1005 +978 @@
  mdd_t * state1 =  mdd_one(mddManager);
  state0 = mdd_and(s0,s1,1,1);
+ mdd_t * state12 = mdd_and(s0,s1,0,1);
  state1 = mdd_not(state0);
   array_insert(mdd_t *, newMvf, 1, state0);
   array_insert(mdd_t *, newMvf, 0, state1);
-Mvf_Function_t * newMvf2  = Mvf_FunctionAlloc( mddManager,2);
- mdd_t * s0_2 =  mdd_eq_c(mddManager,20, 1);
- mdd_t * s1_2 =  mdd_eq_c(mddManager,22, 0);
- mdd_t * state0_2 =  mdd_one(mddManager);
- mdd_t * state1_2 =  mdd_one(mddManager);
- state0_2 = mdd_and(s0_2,s1_2,1,1);
- state1_2 = mdd_not(state0_2);
-  array_insert(mdd_t *, newMvf2, 1, state0_2);
-  array_insert(mdd_t *, newMvf2, 0, state1_2);
-FILE * file = fopen("mvf.txt","w");
-foreach_vertex(part, gen, vertexPtr) {
-fprintf(file,"*********  (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) );
- Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr);
- mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
- mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file);
- mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
- mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file);
-
- if(Part_VertexReadMddId(vertexPtr) == 17)
- {
- Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
-
-   mdd_t * new0 = Mvf_FunctionReadComponent(fun,0);
-   new0 = mdd_and(new0,state1,1,1);
-   mdd_t * new1 = Mvf_FunctionReadComponent(fun,1);
-   new1 = mdd_and(new1,state0,1,1);
-    array_insert(mdd_t *, newMvf, 1, new1);
-    array_insert(mdd_t *, newMvf, 0, new0);
-    mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
-     mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
-    Part_VertexSetFunction(vertexPtr, newMvf);
- }
- else{
-  Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf);
-  Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf);
-  //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2);
- mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0);
- mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
- mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1);
- mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
-
- Part_VertexSetFunction(vertexPtr, newFun);
- Part_VertexSetFunction(vertexPtr, newFun1);
-// Part_VertexSetFunction(vertexPtr, newFun2);
- }
-}
-fclose(file);
-
-
-
-
-  array_t       * psVars = fsm->fsmData.presentStateVars;
-   int  numLatches = array_n(psVars);
-
-
-   for (i=0; i<numLatches; i++){
-    int latchMddId = array_fetch(int, psVars, i);
-    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
-    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
-    vertex_t   *initVertex = Part_PartitionFindVertexByName(part,
-                                Ntk_NodeReadName(initNode));
-    Mvf_Function_t * fun = PartVertexReadFunction(initVertex);
-   printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode),
-   Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) );
-   
- mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
- mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout);
- mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
- mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout);
-
-
-    }
+ mdd_t * ns1 =  mdd_eq_c(mddManager,17, 1);
+Mvf_Function_t * newNS  = Mvf_FunctionAlloc( mddManager,2);
+Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1));
+Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0));
+
+mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout);
+vertex_t * vert;
+vert = Part_PartitionFindVertexByName(part,"cex.s2");
+Part_VertexSetFunction(vert, newNS);
+
+vert = Part_PartitionFindVertexByName(part,"cex.s3");
+ mdd_t * ns1S3 =  mdd_eq_c(mddManager,14, 1);
+Mvf_Function_t * newS3  = Mvf_FunctionAlloc( mddManager,2);
+Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1));
+Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0));
+Part_VertexSetFunction(vert, newS3);
+
+// Initial state
+mdd_t * ns1Init =  mdd_eq_c(mddManager,3, 1);
+
+Mvf_Function_t * newNSInit  = Mvf_FunctionAlloc(mddManager,2);
+Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1));
+Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0));
+mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout);
+Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"),
+newNSInit);
+
+
 
 
@@ -1086 +1016 @@
                                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                                           (void *) part);
-fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
+fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part);
+
+
 mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
 //mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
@@ -1094 +1026 @@
                                       0,1, NIL(array_t),
                                       (verbose > 0),  NIL(array_t));
-//mdd_t * n_reach =  Mvf_MddComposeWithFunction(reach, 17 , newMvf);
-//fsm->reachabilityInfo.initialStates = n_init;
-//fsm->reachabilityInfo.reachableStates = n_reach;
-//      
-//    
+fsm->reachabilityInfo.initialStates = init;
+fsm->reachabilityInfo.reachableStates = reach;
+        
+   
     
 Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
@@ -1104 +1035 @@
                          (void *) fsm); 
 
+Img_ImageInfoUpdateVariables(fsm->imageInfo,
+                                 fsm->partition,
+                                 fsm->fsmData.presentStateVars,
+                                 fsm->fsmData.inputVars,
+                                 fsm->fsmData.presentStateCube,
+                                 fsm->fsmData.inputCube);
 Fsm_FsmReachabilityPrintResults(fsm,3, 0);
 //
@@ -1166 +1103 @@
 printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
 */
-/** state0 = s0 **/
-// mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
-// mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
-// mdd_t * state0 =  mdd_one(mddManager);
-// state0 = mdd_and(s0,s1,1,1);
-///** Next state1 = s2 + !s2  **/
-//
-// mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
-// mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
-// mdd_t * state1 =  mdd_one(mddManager);
-// state1 = mdd_and(ns0,ns1,1,1);
-// state1 = mdd_or(state1,state1,1,0);
-//
-///** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
-// rel =  mdd_one(mddManager);
-// rel =  mdd_or(state0,state1,0,0);
-///**********/
-///** state0 = s2 **/
-// mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
-// mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
-// mdd_t * state02 =  mdd_one(mddManager);
-// state02 = mdd_and(s02,s12,1,1);
-///** Next state1 = s3  **/
-//
-// mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
-// mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
-// mdd_t * state12 =  mdd_one(mddManager);
-// state12 = mdd_and(ns02,ns12,1,1);
-//
-///** state = s0) -> !(Nextstate = s3) **/
-// mdd_t * new_rel =  mdd_one(mddManager);
-// new_rel =  mdd_or(state02,state12,0,0);
-// rel = mdd_and(new_rel,rel,1,1);
-// mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
-
 return 0;               /* normal exit */
 

vis_dev/vis-2.3/src/mc/mcCmd.c

@@ -945 +945 @@
     mddMgr = Fsm_FsmReadMddManager(modelFsm);
 
+        mdd_FunctionPrintMain(mddMgr,modelInitialStates,"INIT_MC",vis_stdout);
+        
     /* compute don't cares. */
     if (modelCareStatesArray == NIL(array_t)) {