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

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

first attempt debug with ltl formula
File size: 23.9 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    We need the bdd when building the transition relation of the automaton
300  */
301  if(options->inductiveStep !=0){
302    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
303 
304    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
305    if (designFsm == NIL(Fsm_Fsm_t)) {
306         (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
307      return 1;
308    }
309  }
310
311/*
312 * Read the formula
313 */
314 /* Read LTL Formulae */
315  if (!ltlFileName) 
316      goto usage;
317
318  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
319  if (options->ltlFile == NIL(FILE)) {
320    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
321    FREE(ltlFileName);
322    BmcOptionFree(options);
323  }
324  FREE(ltlFileName);
325
326 formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
327  if (formulaArray == NIL(array_t)) {
328    (void) fprintf(vis_stderr,
329                   "** bmc error: error in parsing CTL* Fromula from file\n");
330    BmcOptionFree(options);
331    return 1;
332  }
333  if (array_n(formulaArray) == 0) {
334    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
335    BmcOptionFree(options);
336    Ctlsp_FormulaArrayFree(formulaArray);
337    return 1;
338  }
339  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
340  Ctlsp_FormulaArrayFree(formulaArray);
341  if (LTLformulaArray ==  NIL(array_t)){
342    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
343    BmcOptionFree(options);
344    return 1;
345  }
346    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
347
348
349
350 /*
351    Compute the cone of influence
352        here : a list of state variables (latches)
353  */
354        st_table        *CoiTable =  generateAllLatches(network);
355  /*
356      Generate clauses for each time frame.  This is the old way of generating
357      clauses in BMC.
358    */
359    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
360        BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
361    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
362        /*
363    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
364    */
365        nodeToMvfAigTable =
366        (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
367        assert(nodeToMvfAigTable != NIL(st_table));
368
369        if(verbose)
370        {       
371                (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
372                printLatch(nodeToMvfAigTable);
373                (void) fprintf(vis_stdout, "------      COI       ----\n");
374                printLatch(CoiTable);
375                (void) fprintf(vis_stdout, "--------------------------\n");
376    }
377    /*
378      Create a clause database
379     */
380    cnfClauses = BmcCnfClausesAlloc();
381    /*
382      Generate clauses for an initialized path of length k
383     */
384    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
385     fprintf(vis_stdout, "\n");
386    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
387                                 cnfClauses, nodeToMvfAigTable, CoiTable);
388
389    //Generate ltl CNF
390    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
391    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
392    // cf. BmcLtlVerifyGeneralLtl
393    int k = options->maxK;
394    int l;
395    // return the clause number
396    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
397   
398    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
399    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
400    int rightValue,loop,andIndex;
401    array_t           *orClause = NIL(array_t);
402    array_t           *loopClause, *tmpclause;
403
404    if (leftValue != 1) {
405      orClause = array_alloc(int, 0);   
406      if (leftValue == -1){
407            array_insert_last(int, orClause, noLoopIndex);
408      }
409      loopClause = array_alloc(int, k+1);
410      for(l=0; l<=k; l++){
411            int loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
412            rightValue = checkIndex(loopIndex, cnfClauses);
413          if (rightValue == 0){
414            break;
415          }
416      if (rightValue !=0){
417            loop = cnfClauses->cnfGlobalIndex++;
418            BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
419                                                nodeToMvfAigTable, CoiTable, loop);
420          array_insert(int, loopClause, l, loop);
421          if(rightValue == -1){
422           
423            andIndex   = cnfClauses->cnfGlobalIndex++;
424            tmpclause  = array_alloc(int, 2);
425            array_insert(int, tmpclause, 0, loop);
426            array_insert(int, tmpclause, 1, -andIndex);
427            BmcCnfInsertClause(cnfClauses, tmpclause);
428
429            array_insert(int, tmpclause, 0, loopIndex);
430            array_insert(int, tmpclause, 1, -andIndex);
431            BmcCnfInsertClause(cnfClauses, tmpclause);
432        array_free(tmpclause);
433            array_insert_last(int, orClause, andIndex);
434      }
435      else {
436            array_insert_last(int, orClause, loop);
437          }
438      }} // for l loop
439      }
440       BmcCnfInsertClause(cnfClauses, orClause);
441        array_free(orClause);
442
443
444
445
446
447
448
449         if(verbose)
450                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
451                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
452       
453 Ctlsp_FormulaArrayFree(LTLformulaArray);   
454        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
455fclose(cnfFile);
456BmcCnfClausesFree(cnfClauses);
457BmcOptionFree(options);
458return 0;
459  usage:
460  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
461  minimum length] [-o cnf_file] [-p ltl_file]\n");
462  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
463  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
464  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
465  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
466  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n"); 
467  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n"); 
468  return 1;             /* error exit */
469
470}
471/**Function********************************************************************
472
473  Synopsis    [Implements the _Debug_test command.]
474
475  CommandName [_Debug_test]
476
477  CommandSynopsis [template for implementing commands]
478
479  CommandArguments [\[-h\] \[-v\]]
480 
481  CommandDescription [This command does nothing useful.  It merely serves as a
482  template for the implementation of new commands.<p>
483
484  Command options:<p> 
485
486  <dl>
487  <dt> -h
488  <dd> Print the command usage.
489  </dl>
490
491  <dt> -v
492  <dd> Verbose mode.
493  </dl>
494  ]
495
496  SideEffects []
497
498******************************************************************************/
499static int
500CommandDebug(
501  Hrc_Manager_t ** hmgr,
502  int  argc,
503  char ** argv)
504{
505  int            c;
506  int            verbose = 0;              /* default value */
507
508  /*
509   * Parse command line options.
510   */
511  util_getopt_reset();
512  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
513    switch(c) {
514      case 'v':
515        verbose = 1;
516        break;
517      case 'h':
518        goto usage;
519      default:
520        goto usage;
521    }
522  }
523
524  if (verbose) {
525    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
526  }
527
528  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
529  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
530  printf("** DEBUG MODE **\n");
531  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
532  printf("model : %s\n", Hrc_NodeReadModelName(n));
533
534  mdd_t * safe   = getSafe(fsm);
535  mdd_t * forbid = getForbidden(fsm);
536  mdd_t * reach  = getReach(fsm);
537 
538  if(safe == NIL(mdd_t))
539  {
540        printf("call command set_safe before\n");
541        return 1;
542  }
543  if(forbid == NIL(mdd_t))
544  {
545        printf("call command set_forbidden before\n");
546        return 1;
547  }
548
549  FILE*  oFile;
550  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
551 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
552//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
553
554  mdd_t * EFState = mdd_and(reach,safe,1,1);
555//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
556
557  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
558  array_t *careStatesArray = array_alloc(mdd_t *, 0);
559  array_insert(mdd_t *, careStatesArray, 0,mddOne);
560
561  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
562                   EFState,
563           fsm->fairnessInfo.states,
564           careStatesArray,
565                   0,
566           McDcLevelNone_c);
567
568  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
569  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
570
571  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
572                   EXEFState,
573           fsm->fairnessInfo.states,
574           careStatesArray,
575                   0,
576           McDcLevelNone_c);
577  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
578  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
579  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
580  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
581  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
582                   andState,
583           fsm->fairnessInfo.states,
584           careStatesArray,
585                   0,
586           McDcLevelNone_c);
587  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
588  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
589  andState =  mdd_xor(EXEFState2,andState);
590  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
591  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
592                   andState,
593           fsm->fairnessInfo.states,
594           careStatesArray,
595                   0,
596           McDcLevelNone_c);
597  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
598  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
599  andState =  mdd_xor(EXEFState2,andState);
600  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
601
602
603
604  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
605  //mdd_GetState_Values(mddManager , EFState, stdout);
606  fclose(oFile);
607
608
609
610
611
612  return 0;             /* normal exit */
613
614  usage:
615  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
616  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
617  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
618  return 1;             /* error exit */
619}
620
621/******************************************/
622/* function that build a bdd for the      */
623/* simple example :                       */
624/*     (state = 0) -> !(state = 1)        */
625/******************************************/
626mdd_t * buildDummyBdd(mdd_manager   *mddManager)
627{
628/** state0 = 0 **/
629 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
630 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
631 mdd_t * state0 =  mdd_one(mddManager);
632 state0 = mdd_and(s0,s1,1,1);
633/** state1 = 1 **/
634 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
635 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
636 mdd_t * state1 =  mdd_one(mddManager);
637 state1 = mdd_and(ns0,ns1,1,1);
638/** state = 0) -> !(state = 1) **/
639 mdd_t * rel =  mdd_one(mddManager);
640 rel =  mdd_or(state0,state1,0,0);
641 
642 return rel;
643}
644
645
646/**Function********************************************************************
647
648  Synopsis    [Implements the transtion command.]
649
650  CommandName [_transition]
651
652  CommandSynopsis [compute new transition relation]
653
654  CommandArguments [\[-h\] \[-v\]]
655 
656  CommandDescription [This command create a new transition relation that is a
657  and of the Bdd of the old one and an other bdd.
658  <p>
659
660  Command options:<p> 
661
662  <dl>
663  <dt> -h
664  <dd> Print the command usage.
665  </dl>
666
667  <dt> -v
668  <dd> Verbose mode.
669  </dl>
670  ]
671
672  SideEffects [Change the fsm]
673
674******************************************************************************/
675
676static int 
677CommandTransition (Hrc_Manager_t ** hmgr,
678                   int  argc, char ** argv){
679int            c;
680int            verbose = 0;              /* default value */
681
682/*
683 * Parse command line options.
684 */
685util_getopt_reset();
686while ((c = util_getopt(argc, argv, "vh")) != EOF) {
687  switch(c) {
688    case 'v':
689      verbose = 1;
690      break;
691    case 'h':
692      goto usage;
693    default:
694      goto usage;
695  }
696}
697
698if (verbose) {
699  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
700}
701
702Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
703Ntk_Network_t  *network      = NIL(Ntk_Network_t);
704mdd_manager    *mddManager; 
705mdd_t          *rel          = NIL(mdd_t);
706graph_t        *partition;
707int            i;
708/******************/
709network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
710if(network == NIL(Ntk_Network_t))
711        return 1;
712fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
713if(fsm ==  NIL(Fsm_Fsm_t))
714        return 1;
715mddManager   = Fsm_FsmReadMddManager(fsm);
716
717
718
719/**********   Build cex  ***********/
720/* Here add the function           */
721/* that build the Bdd to and       */
722/* with the transtion relation     */
723/***********************************/
724rel = buildDummyBdd(mddManager);
725if(rel == NIL(mdd_t))
726{
727        fprintf(vis_stdout,"Problem when building the new relation bdd");
728        return 1;
729}
730if (verbose)
731  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
732
733
734/** Get image_info **/
735Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
736partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
737/**** The complete transtion relation ****/
738// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
739/*****************************************/
740/*** For each latch rebuild the transition function ***/
741/*** mvf table is composed of mdd for each possible ***/
742/*** value of the latch                             ***/
743ImgFunctionData_t * functionData = &(imageInfo->functionData);
744array_t *roots = functionData->roots;
745array_t *rangeVarMddIdArray = functionData->rangeVars;
746char * nodeName;
747arrayForEachItem(char *, roots, i, nodeName) {
748        /* The new relation */ 
749        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
750    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
751    int mddId = array_fetch(int, rangeVarMddIdArray, i);
752        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
753        mdd_t * n_relation = mdd_and(relation,rel,1,1);
754    /* Build for each possible value */
755        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
756        int v ;
757        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
758        for(v = 0; v<nbValue;v++)
759        {
760                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
761                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
762                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
763                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
764
765        }
766        /* Replace the function for the latch */
767        Part_VertexSetFunction(vertex, newMvf);
768//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
769}
770
771/** Change the fsm and the network with a new partition and the new fsm **/
772Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
773                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
774                                          (void *) partition);
775fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
776mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
777mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
778                                      0,0, 0,
779                                      0, 0, Fsm_Rch_Default_c,
780                                      0,1, NIL(array_t),
781                                      (verbose > 0),  NIL(array_t));
782fsm->reachabilityInfo.initialStates = init;
783fsm->reachabilityInfo.reachableStates = reach;
784if(verbose)
785        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
786
787Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
788                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
789                         (void *) fsm);
790
791return 0;               /* normal exit */
792
793usage:
794(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
795(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
796(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
797return 1;               /* error exit */
798
799}
800
801
Note: See TracBrowser for help on using the repository browser.