source: vis_dev/vis-2.3/src/debug/debug.c @ 40

Last change on this file since 40 was 40, checked in by cecile, 13 years ago

abnormal structure in network
File size: 22.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [debug.c]
4
5  PackageName [debug]
6
7  Synopsis    [Debug package initialization, ending, and the command debug]
8
9  Author      [Cecile B.]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "debugInt.h"
33#include "imgInt.h"
34#include "partInt.h"
35static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
36
37/*---------------------------------------------------------------------------*/
38/* Constant declarations                                                     */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Structure declarations                                                    */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Variable declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Macro declarations                                                        */
55/*---------------------------------------------------------------------------*/
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes                                                */
61/*---------------------------------------------------------------------------*/
62
63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
65static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
67
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions                                          */
74/*---------------------------------------------------------------------------*/
75
76/**Function********************************************************************
77
78  Synopsis    [Initializes the test package.]
79
80  SideEffects []
81
82  SeeAlso     [Debug_End]
83
84******************************************************************************/
85void
86Debug_Init(void)
87{
88  /*
89   * Add a command to the global command table.  By using the leading
90   * underscore, the command will be listed under "help -a" but not "help".
91   */
92  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
93  Cmd_CommandAdd("_transition",  CommandTransition, 1);
94  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
95  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
96
97}
98
99
100/**Function********************************************************************
101
102  Synopsis    [Ends the test package.]
103
104  SideEffects []
105
106  SeeAlso     [Debug_Init]
107
108******************************************************************************/
109void
110Debug_End(void)
111{
112  /*
113   * For example, free any global memory (if any) which the test package is
114   * responsible for.
115   */
116}
117
118
119/*---------------------------------------------------------------------------*/
120/* Definition of internal functions                                          */
121/*---------------------------------------------------------------------------*/
122
123
124/*---------------------------------------------------------------------------*/
125/* Definition of static functions                                            */
126/*---------------------------------------------------------------------------*/
127
128
129static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
130{
131  Ntk_Network_t * ntk;
132  int c,verbose;
133  Dbg_Abnormal_t * abnormal;
134  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
135  if (ntk == NIL(Ntk_Network_t)) {
136        (void) fprintf(vis_stdout, "** abn error: No network\n");
137        return 1;
138  }
139  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
140        switch(c) {
141                case 'v':
142                        verbose = 1;
143                        break;
144                }
145 }
146  abnormal = Dbg_DebugAbnormalAlloc(ntk);
147  abnormal->verbose = verbose;
148  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
149}
150/**Function********************************************************************
151
152  Synopsis    [Implements the _sat_debug command.]
153
154  CommandName [_sat_debug]
155
156  CommandSynopsis [locate faulty candidates]
157
158  CommandArguments [\[-h\] \[-v\]]
159 
160  CommandDescription [This command compute the fault candidates of a given
161  properties.<p>
162
163  Command options:<p> 
164
165  <dl>
166  <dt> -h
167  <dd> Print the command usage.
168  </dl>
169
170  <dt> -v
171  <dd> Verbose mode.
172  </dl>
173  ]
174
175  SideEffects []
176
177******************************************************************************/
178static int
179checkIndex(
180  int             index,
181  BmcCnfClauses_t *cnfClauses)
182{
183  int     rtnValue = -1; /* it is not TRUE or FALSE*/
184
185  if (index == 0){ /* TRUE or FALSE*/
186    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
187      rtnValue = 0; /* FALSE */
188    } else {
189      /*
190        if (cnfClauses->noOfClauses == 0)
191        rtnValue = 1;
192        }
193      */
194      rtnValue = 1; /* TRUE */
195    }
196  }
197  return rtnValue;
198}
199
200
201static int 
202CommandSatDebug(
203Hrc_Manager_t ** hmgr, 
204int argc, 
205char ** argv){
206int            c,i;
207int            verbose = 0;              /* default value */
208BmcOption_t  *options = BmcOptionAlloc();
209Ntk_Network_t * network;
210bAig_Manager_t    *manager;
211array_t           *formulaArray;
212array_t           *LTLformulaArray;
213char *ltlFileName     = NIL(char);
214
215/*
216 * Parse command line options.
217 */
218util_getopt_reset();
219while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
220  switch(c) {
221    case 'v':
222      verbose = 1;
223          options->verbosityLevel =  verbose;
224      break;
225    case 'h':
226      goto usage;
227        case 'm':
228      for (i = 0; i < strlen(util_optarg); i++) {
229                if (!isdigit((int)util_optarg[i])) {
230                        goto usage;
231                }
232      }
233      options->minK = atoi(util_optarg);
234      break;
235    case 'k':
236      for (i = 0; i < strlen(util_optarg); i++) {
237                if (!isdigit((int)util_optarg[i])) {
238                        goto usage;
239                }
240      }
241          options->maxK = atoi(util_optarg);
242          break;
243        case 'o':
244      options->cnfFileName = util_strsav(util_optarg);
245      break;
246    case 'p':
247      ltlFileName     = util_strsav(util_optarg);
248    break;
249
250    default:
251      goto usage;
252  }
253}
254printf("MAX K %d", options->maxK);
255 if (options->minK > options->maxK){
256    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
257    goto usage;
258  }
259
260if (verbose) {
261  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
262}
263 /* create SAT Solver input file */
264 if (options->cnfFileName == NIL(char)) {
265    options->satInFile = BmcCreateTmpFile(); 
266}
267 else {
268    options->satInFile = options->cnfFileName;
269 }
270
271/* create SAT Solver output file */
272options->satOutFile = BmcCreateTmpFile();
273if (options->satOutFile == NIL(char)){
274  BmcOptionFree(options);
275 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
276  return 1;
277}
278
279options->verbosityLevel =  1;
280//options->satSolver
281//options->clauses
282
283 /*
284   * Read the network
285   */
286  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
287  if (network == NIL(Ntk_Network_t)) {
288    (void) fprintf(vis_stdout, "** bmc error: No network\n");
289    BmcOptionFree(options);
290    return 1;
291  }
292  manager = Ntk_NetworkReadMAigManager(network);
293  if (manager == NIL(mAig_Manager_t)) {
294    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
295    BmcOptionFree(options);
296    return 1;
297  }
298
299  /*
300    We need the bdd when building the transition relation of the automaton
301  */
302  if(options->inductiveStep !=0){
303    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
304 
305    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
306    if (designFsm == NIL(Fsm_Fsm_t)) {
307         (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
308      return 1;
309    }
310  }
311Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
312printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
313/*
314 * Read the formula
315 */
316 /* Read LTL Formulae */
317  if (!ltlFileName) 
318      goto usage;
319
320  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
321  if (options->ltlFile == NIL(FILE)) {
322    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
323    FREE(ltlFileName);
324    BmcOptionFree(options);
325  }
326  FREE(ltlFileName);
327
328 formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
329  if (formulaArray == NIL(array_t)) {
330    (void) fprintf(vis_stderr,
331                   "** bmc error: error in parsing CTL* Fromula from file\n");
332    BmcOptionFree(options);
333    return 1;
334  }
335  if (array_n(formulaArray) == 0) {
336    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
337    BmcOptionFree(options);
338    Ctlsp_FormulaArrayFree(formulaArray);
339    return 1;
340  }
341  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
342  Ctlsp_FormulaArrayFree(formulaArray);
343  if (LTLformulaArray ==  NIL(array_t)){
344    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
345    BmcOptionFree(options);
346    return 1;
347  }
348    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
349
350
351
352 /*
353    Compute the cone of influence
354        here : a list of state variables (latches)
355  */
356        st_table        *CoiTable =  generateAllLatches(network);
357  /*
358      Generate clauses for each time frame.  This is the old way of generating
359      clauses in BMC.
360    */
361    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
362        BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
363    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
364        /*
365    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
366    */
367        nodeToMvfAigTable =
368        (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
369        assert(nodeToMvfAigTable != NIL(st_table));
370
371        if(verbose)
372        {       
373                (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
374                printLatch(nodeToMvfAigTable);
375                (void) fprintf(vis_stdout, "------      COI       ----\n");
376                printLatch(CoiTable);
377                (void) fprintf(vis_stdout, "--------------------------\n");
378    }
379    /*
380      Create a clause database
381     */
382    cnfClauses = BmcCnfClausesAlloc();
383    /*
384      Generate clauses for an initialized path of length k
385     */
386    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
387     fprintf(vis_stdout, "\n");
388    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
389                                 cnfClauses, nodeToMvfAigTable, CoiTable);
390
391    //Generate ltl CNF
392    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
393    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
394    // cf. BmcLtlVerifyGeneralLtl
395    int k = options->maxK;
396    int l;
397    // return the clause number
398    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
399   
400    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
401    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
402        array_t           *objClause = NIL(array_t);
403        objClause = array_alloc(int, 0);   
404        array_insert_last(int, objClause, noLoopIndex);
405        BmcCnfInsertClause(cnfClauses, objClause);
406    array_free(objClause);
407
408       
409//TODO Add abnormal formula
410
411
412
413
414
415         if(verbose)
416                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
417                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
418       
419 Ctlsp_FormulaArrayFree(LTLformulaArray);   
420        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
421fclose(cnfFile);
422BmcCnfClausesFree(cnfClauses);
423BmcOptionFree(options);
424return 0;
425  usage:
426  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
427  minimum length] [-o cnf_file] [-p ltl_file]\n");
428  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
429  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
430  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
431  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
432  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n"); 
433  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n"); 
434  return 1;             /* error exit */
435
436}
437/**Function********************************************************************
438
439  Synopsis    [Implements the _Debug_test command.]
440
441  CommandName [_Debug_test]
442
443  CommandSynopsis [template for implementing commands]
444
445  CommandArguments [\[-h\] \[-v\]]
446 
447  CommandDescription [This command does nothing useful.  It merely serves as a
448  template for the implementation of new commands.<p>
449
450  Command options:<p> 
451
452  <dl>
453  <dt> -h
454  <dd> Print the command usage.
455  </dl>
456
457  <dt> -v
458  <dd> Verbose mode.
459  </dl>
460  ]
461
462  SideEffects []
463
464******************************************************************************/
465static int
466CommandDebug(
467  Hrc_Manager_t ** hmgr,
468  int  argc,
469  char ** argv)
470{
471  int            c;
472  int            verbose = 0;              /* default value */
473
474  /*
475   * Parse command line options.
476   */
477  util_getopt_reset();
478  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
479    switch(c) {
480      case 'v':
481        verbose = 1;
482        break;
483      case 'h':
484        goto usage;
485      default:
486        goto usage;
487    }
488  }
489
490  if (verbose) {
491    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
492  }
493
494  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
495  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
496  printf("** DEBUG MODE **\n");
497  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
498  printf("model : %s\n", Hrc_NodeReadModelName(n));
499
500  mdd_t * safe   = getSafe(fsm);
501  mdd_t * forbid = getForbidden(fsm);
502  mdd_t * reach  = getReach(fsm);
503 
504  if(safe == NIL(mdd_t))
505  {
506        printf("call command set_safe before\n");
507        return 1;
508  }
509  if(forbid == NIL(mdd_t))
510  {
511        printf("call command set_forbidden before\n");
512        return 1;
513  }
514
515  FILE*  oFile;
516  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
517 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
518//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
519
520  mdd_t * EFState = mdd_and(reach,safe,1,1);
521//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
522
523  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
524  array_t *careStatesArray = array_alloc(mdd_t *, 0);
525  array_insert(mdd_t *, careStatesArray, 0,mddOne);
526
527  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
528                   EFState,
529           fsm->fairnessInfo.states,
530           careStatesArray,
531                   0,
532           McDcLevelNone_c);
533
534  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
535  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
536
537  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
538                   EXEFState,
539           fsm->fairnessInfo.states,
540           careStatesArray,
541                   0,
542           McDcLevelNone_c);
543  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
544  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
545  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
546  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
547  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
548                   andState,
549           fsm->fairnessInfo.states,
550           careStatesArray,
551                   0,
552           McDcLevelNone_c);
553  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
554  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
555  andState =  mdd_xor(EXEFState2,andState);
556  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
557  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
558                   andState,
559           fsm->fairnessInfo.states,
560           careStatesArray,
561                   0,
562           McDcLevelNone_c);
563  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
564  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
565  andState =  mdd_xor(EXEFState2,andState);
566  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
567
568
569
570  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
571  //mdd_GetState_Values(mddManager , EFState, stdout);
572  fclose(oFile);
573
574
575
576
577
578  return 0;             /* normal exit */
579
580  usage:
581  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
582  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
583  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
584  return 1;             /* error exit */
585}
586
587/******************************************/
588/* function that build a bdd for the      */
589/* simple example :                       */
590/*     (state = 0) -> !(state = 1)        */
591/******************************************/
592mdd_t * buildDummyBdd(mdd_manager   *mddManager)
593{
594/** state0 = 0 **/
595 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
596 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
597 mdd_t * state0 =  mdd_one(mddManager);
598 state0 = mdd_and(s0,s1,1,1);
599/** state1 = 1 **/
600 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
601 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
602 mdd_t * state1 =  mdd_one(mddManager);
603 state1 = mdd_and(ns0,ns1,1,1);
604/** state = 0) -> !(state = 1) **/
605 mdd_t * rel =  mdd_one(mddManager);
606 rel =  mdd_or(state0,state1,0,0);
607 
608 return rel;
609}
610
611
612/**Function********************************************************************
613
614  Synopsis    [Implements the transtion command.]
615
616  CommandName [_transition]
617
618  CommandSynopsis [compute new transition relation]
619
620  CommandArguments [\[-h\] \[-v\]]
621 
622  CommandDescription [This command create a new transition relation that is a
623  and of the Bdd of the old one and an other bdd.
624  <p>
625
626  Command options:<p> 
627
628  <dl>
629  <dt> -h
630  <dd> Print the command usage.
631  </dl>
632
633  <dt> -v
634  <dd> Verbose mode.
635  </dl>
636  ]
637
638  SideEffects [Change the fsm]
639
640******************************************************************************/
641
642static int 
643CommandTransition (Hrc_Manager_t ** hmgr,
644                   int  argc, char ** argv){
645int            c;
646int            verbose = 0;              /* default value */
647
648/*
649 * Parse command line options.
650 */
651util_getopt_reset();
652while ((c = util_getopt(argc, argv, "vh")) != EOF) {
653  switch(c) {
654    case 'v':
655      verbose = 1;
656      break;
657    case 'h':
658      goto usage;
659    default:
660      goto usage;
661  }
662}
663
664if (verbose) {
665  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
666}
667
668Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
669Ntk_Network_t  *network      = NIL(Ntk_Network_t);
670mdd_manager    *mddManager; 
671mdd_t          *rel          = NIL(mdd_t);
672graph_t        *partition;
673int            i;
674/******************/
675network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
676if(network == NIL(Ntk_Network_t))
677        return 1;
678fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
679if(fsm ==  NIL(Fsm_Fsm_t))
680        return 1;
681mddManager   = Fsm_FsmReadMddManager(fsm);
682
683
684
685/**********   Build cex  ***********/
686/* Here add the function           */
687/* that build the Bdd to and       */
688/* with the transtion relation     */
689/***********************************/
690rel = buildDummyBdd(mddManager);
691if(rel == NIL(mdd_t))
692{
693        fprintf(vis_stdout,"Problem when building the new relation bdd");
694        return 1;
695}
696if (verbose)
697  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
698
699
700/** Get image_info **/
701Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
702partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
703/**** The complete transtion relation ****/
704// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
705/*****************************************/
706/*** For each latch rebuild the transition function ***/
707/*** mvf table is composed of mdd for each possible ***/
708/*** value of the latch                             ***/
709ImgFunctionData_t * functionData = &(imageInfo->functionData);
710array_t *roots = functionData->roots;
711array_t *rangeVarMddIdArray = functionData->rangeVars;
712char * nodeName;
713arrayForEachItem(char *, roots, i, nodeName) {
714        /* The new relation */ 
715        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
716    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
717    int mddId = array_fetch(int, rangeVarMddIdArray, i);
718        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
719        mdd_t * n_relation = mdd_and(relation,rel,1,1);
720    /* Build for each possible value */
721        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
722        int v ;
723        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
724        for(v = 0; v<nbValue;v++)
725        {
726                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
727                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
728                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
729                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
730
731        }
732        /* Replace the function for the latch */
733        Part_VertexSetFunction(vertex, newMvf);
734//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
735}
736
737/** Change the fsm and the network with a new partition and the new fsm **/
738Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
739                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
740                                          (void *) partition);
741fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
742mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
743mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
744                                      0,0, 0,
745                                      0, 0, Fsm_Rch_Default_c,
746                                      0,1, NIL(array_t),
747                                      (verbose > 0),  NIL(array_t));
748fsm->reachabilityInfo.initialStates = init;
749fsm->reachabilityInfo.reachableStates = reach;
750if(verbose)
751        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
752
753Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
754                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
755                         (void *) fsm);
756
757return 0;               /* normal exit */
758
759usage:
760(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
761(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
762(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
763return 1;               /* error exit */
764
765}
766
767
Note: See TracBrowser for help on using the repository browser.