Changeset 100 for vis_dev


Ignore:
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:
4 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/models/transition/cex.ctl

    r99 r100  
    1 (((cex.state[2:0] = 7  * cex.s2 = 1 ) )  * S.state[1:0] = 0)  *
    2 EX( S.state[1:0] = 1 ) ;
     1#cex.state[2:0] = 7  * cex.s2 = 1 * S.state[1:0] = 0 * EX(cex.state[2:0] = 2 *
     2# S.state[1:0] = 1) ;
     3
     4#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 * S.state[1:0] = 0));
     5#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 ));
     6#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 1 ));
     7#cex.s2 = 1 * EX(cex.s2 = 0 * EX(cex.s3 = 1 ));
     8cex.state[2:0] = 7 * cex.s2 = 1 * S.state[1:0] = 0 * (EX(cex.state[2:0] = 2
     9* cex.s2 = 0 * S.state[1:0] = 1 * EX(cex.s2 = 0)));
     10 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
     11* EX(S.state[1:0] =  0 * EX(S.state[1:0] = 1)))));
     12
     13
  • vis_dev/vis-2.3/models/transition/cex.v

    r99 r100  
    1818    state[2] = $ND(0,1);
    1919    if(state == 3)
     20        begin
    2021      s2 = 0;
     22          s3 = $ND(0,1);
     23          s4 = $ND(0,1);
     24        end
    2125    else
     26          begin
    2227      s2 = 1;
    23   s3 = $ND(0,1);
    24   s4 = $ND(0,1);
     28          s3 = 0;
     29      s4 = 0;
     30          end
    2531  end
    2632
  • vis_dev/vis-2.3/src/debug/debug.c

    r98 r100  
    371371         if(verbose)
    372372                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
    373                 latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
     373                latches \n",cnfClauses->noOfClauses,st_count(CoiTable));
    374374 
    375375   
     
    970970/***********************************/
    971971//rel = buildDummyBdd(mddManager);
    972 array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
    973 array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
    974 array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
    975 printf("Next Names\n");
    976 printStringArray(nextNames);
    977 printf("Next Ids\n");
    978 printIntArray(nextIds);
    979 printf("Current Ids\n");
    980 printIntArray(currentIds);
    981 Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
    982972 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
    983 
    984 lsGen gen;
    985 vertex_t *vertexPtr;
    986 
    987 
    988 //foreach_vertex(part, gen, vertexPtr) {
    989 //      if (PartVertexReadName(vertexPtr) != NIL(char)) {
    990 //        (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr));
    991 //      }
    992 //}
    993 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
    994 Mvf_Function_t*  vertexFunction = PartVertexReadFunction(v_s2);
    995   if (vertexFunction != NIL(Mvf_Function_t)) {
    996 printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
    997 }
    998 else
    999   printf("no fonction");
    1000 
     973 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
    1001974Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
    1002975 mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
     
    1005978 mdd_t * state1 =  mdd_one(mddManager);
    1006979 state0 = mdd_and(s0,s1,1,1);
     980 mdd_t * state12 = mdd_and(s0,s1,0,1);
    1007981 state1 = mdd_not(state0);
    1008982  array_insert(mdd_t *, newMvf, 1, state0);
    1009983  array_insert(mdd_t *, newMvf, 0, state1);
    1010 Mvf_Function_t * newMvf2  = Mvf_FunctionAlloc( mddManager,2);
    1011  mdd_t * s0_2 =  mdd_eq_c(mddManager,20, 1);
    1012  mdd_t * s1_2 =  mdd_eq_c(mddManager,22, 0);
    1013  mdd_t * state0_2 =  mdd_one(mddManager);
    1014  mdd_t * state1_2 =  mdd_one(mddManager);
    1015  state0_2 = mdd_and(s0_2,s1_2,1,1);
    1016  state1_2 = mdd_not(state0_2);
    1017   array_insert(mdd_t *, newMvf2, 1, state0_2);
    1018   array_insert(mdd_t *, newMvf2, 0, state1_2);
    1019 FILE * file = fopen("mvf.txt","w");
    1020 foreach_vertex(part, gen, vertexPtr) {
    1021 fprintf(file,"*********  (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) );
    1022  Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr);
    1023  mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
    1024  mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file);
    1025  mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
    1026  mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file);
    1027 
    1028  if(Part_VertexReadMddId(vertexPtr) == 17)
    1029  {
    1030  Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
    1031 
    1032    mdd_t * new0 = Mvf_FunctionReadComponent(fun,0);
    1033    new0 = mdd_and(new0,state1,1,1);
    1034    mdd_t * new1 = Mvf_FunctionReadComponent(fun,1);
    1035    new1 = mdd_and(new1,state0,1,1);
    1036     array_insert(mdd_t *, newMvf, 1, new1);
    1037     array_insert(mdd_t *, newMvf, 0, new0);
    1038     mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
    1039      mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
    1040     Part_VertexSetFunction(vertexPtr, newMvf);
    1041  }
    1042  else{
    1043   Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf);
    1044   Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf);
    1045   //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2);
    1046  mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0);
    1047  mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
    1048  mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1);
    1049  mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
    1050 
    1051  Part_VertexSetFunction(vertexPtr, newFun);
    1052  Part_VertexSetFunction(vertexPtr, newFun1);
    1053 // Part_VertexSetFunction(vertexPtr, newFun2);
    1054  }
    1055 }
    1056 fclose(file);
    1057 
    1058 
    1059 
    1060 
    1061   array_t       * psVars = fsm->fsmData.presentStateVars;
    1062    int  numLatches = array_n(psVars);
    1063 
    1064 
    1065    for (i=0; i<numLatches; i++){
    1066     int latchMddId = array_fetch(int, psVars, i);
    1067     Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
    1068     Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
    1069     vertex_t   *initVertex = Part_PartitionFindVertexByName(part,
    1070                                 Ntk_NodeReadName(initNode));
    1071     Mvf_Function_t * fun = PartVertexReadFunction(initVertex);
    1072    printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode),
    1073    Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) );
    1074    
    1075  mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
    1076  mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout);
    1077  mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
    1078  mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout);
    1079 
    1080 
    1081     }
     984 mdd_t * ns1 =  mdd_eq_c(mddManager,17, 1);
     985Mvf_Function_t * newNS  = Mvf_FunctionAlloc( mddManager,2);
     986Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1));
     987Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0));
     988
     989mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout);
     990vertex_t * vert;
     991vert = Part_PartitionFindVertexByName(part,"cex.s2");
     992Part_VertexSetFunction(vert, newNS);
     993
     994vert = Part_PartitionFindVertexByName(part,"cex.s3");
     995 mdd_t * ns1S3 =  mdd_eq_c(mddManager,14, 1);
     996Mvf_Function_t * newS3  = Mvf_FunctionAlloc( mddManager,2);
     997Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1));
     998Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0));
     999Part_VertexSetFunction(vert, newS3);
     1000
     1001// Initial state
     1002mdd_t * ns1Init =  mdd_eq_c(mddManager,3, 1);
     1003
     1004Mvf_Function_t * newNSInit  = Mvf_FunctionAlloc(mddManager,2);
     1005Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1));
     1006Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0));
     1007mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout);
     1008Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"),
     1009newNSInit);
     1010
     1011
    10821012
    10831013
     
    10861016                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
    10871017                                          (void *) part);
    1088 fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
     1018fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part);
     1019
     1020
    10891021mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
    10901022//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
     
    10941026                                      0,1, NIL(array_t),
    10951027                                      (verbose > 0),  NIL(array_t));
    1096 //mdd_t * n_reach =  Mvf_MddComposeWithFunction(reach, 17 , newMvf);
    1097 //fsm->reachabilityInfo.initialStates = n_init;
    1098 //fsm->reachabilityInfo.reachableStates = n_reach;
    1099 //     
    1100 //   
     1028fsm->reachabilityInfo.initialStates = init;
     1029fsm->reachabilityInfo.reachableStates = reach;
     1030       
     1031   
    11011032   
    11021033Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
     
    11041035                         (void *) fsm);
    11051036
     1037Img_ImageInfoUpdateVariables(fsm->imageInfo,
     1038                                 fsm->partition,
     1039                                 fsm->fsmData.presentStateVars,
     1040                                 fsm->fsmData.inputVars,
     1041                                 fsm->fsmData.presentStateCube,
     1042                                 fsm->fsmData.inputCube);
    11061043Fsm_FsmReachabilityPrintResults(fsm,3, 0);
    11071044//
     
    11661103printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
    11671104*/
    1168 /** state0 = s0 **/
    1169 // mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
    1170 // mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
    1171 // mdd_t * state0 =  mdd_one(mddManager);
    1172 // state0 = mdd_and(s0,s1,1,1);
    1173 ///** Next state1 = s2 + !s2  **/
    1174 //
    1175 // mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
    1176 // mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
    1177 // mdd_t * state1 =  mdd_one(mddManager);
    1178 // state1 = mdd_and(ns0,ns1,1,1);
    1179 // state1 = mdd_or(state1,state1,1,0);
    1180 //
    1181 ///** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
    1182 // rel =  mdd_one(mddManager);
    1183 // rel =  mdd_or(state0,state1,0,0);
    1184 ///**********/
    1185 ///** state0 = s2 **/
    1186 // mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
    1187 // mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
    1188 // mdd_t * state02 =  mdd_one(mddManager);
    1189 // state02 = mdd_and(s02,s12,1,1);
    1190 ///** Next state1 = s3  **/
    1191 //
    1192 // mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
    1193 // mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
    1194 // mdd_t * state12 =  mdd_one(mddManager);
    1195 // state12 = mdd_and(ns02,ns12,1,1);
    1196 //
    1197 ///** state = s0) -> !(Nextstate = s3) **/
    1198 // mdd_t * new_rel =  mdd_one(mddManager);
    1199 // new_rel =  mdd_or(state02,state12,0,0);
    1200 // rel = mdd_and(new_rel,rel,1,1);
    1201 // mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
    1202 
    12031105return 0;               /* normal exit */
    12041106
  • vis_dev/vis-2.3/src/mc/mcCmd.c

    r14 r100  
    945945    mddMgr = Fsm_FsmReadMddManager(modelFsm);
    946946
     947        mdd_FunctionPrintMain(mddMgr,modelInitialStates,"INIT_MC",vis_stdout);
     948       
    947949    /* compute don't cares. */
    948950    if (modelCareStatesArray == NIL(array_t)) {
Note: See TracChangeset for help on using the changeset viewer.