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

Last change on this file since 41 was 41, checked in by cecile, 12 years ago

new command generate cnf from network
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);
67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
68
69
70/**AutomaticEnd***************************************************************/
71
72
73/*---------------------------------------------------------------------------*/
74/* Definition of exported functions                                          */
75/*---------------------------------------------------------------------------*/
76
77/**Function********************************************************************
78
79  Synopsis    [Initializes the test package.]
80
81  SideEffects []
82
83  SeeAlso     [Debug_End]
84
85******************************************************************************/
86void
87Debug_Init(void)
88{
89  /*
90   * Add a command to the global command table.  By using the leading
91   * underscore, the command will be listed under "help -a" but not "help".
92   */
93  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
94  Cmd_CommandAdd("_transition",  CommandTransition, 1);
95  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
96  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
97  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
98
99}
100
101
102/**Function********************************************************************
103
104  Synopsis    [Ends the test package.]
105
106  SideEffects []
107
108  SeeAlso     [Debug_Init]
109
110******************************************************************************/
111void
112Debug_End(void)
113{
114  /*
115   * For example, free any global memory (if any) which the test package is
116   * responsible for.
117   */
118}
119
120
121/*---------------------------------------------------------------------------*/
122/* Definition of internal functions                                          */
123/*---------------------------------------------------------------------------*/
124
125
126/*---------------------------------------------------------------------------*/
127/* Definition of static functions                                            */
128/*---------------------------------------------------------------------------*/
129
130
131static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
132{
133  Ntk_Network_t * ntk;
134  int c,verbose;
135  Dbg_Abnormal_t * abnormal;
136  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
137  if (ntk == NIL(Ntk_Network_t)) {
138        (void) fprintf(vis_stdout, "** abn error: No network\n");
139        return 1;
140  }
141  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
142        switch(c) {
143                case 'v':
144                        verbose = 1;
145                        break;
146                }
147 }
148  abnormal = Dbg_DebugAbnormalAlloc(ntk);
149  abnormal->verbose = verbose;
150  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
151}
152/**Function********************************************************************
153
154  Synopsis    [Implements the _sat_debug command.]
155
156  CommandName [_sat_debug]
157
158  CommandSynopsis [locate faulty candidates]
159
160  CommandArguments [\[-h\] \[-v\]]
161 
162  CommandDescription [This command compute the fault candidates of a given
163  properties.<p>
164
165  Command options:<p> 
166
167  <dl>
168  <dt> -h
169  <dd> Print the command usage.
170  </dl>
171
172  <dt> -v
173  <dd> Verbose mode.
174  </dl>
175  ]
176
177  SideEffects []
178
179******************************************************************************/
180static int 
181CommandSatDebug(
182Hrc_Manager_t ** hmgr, 
183int argc, 
184char ** argv){
185int            c,i;
186int            verbose = 0;              /* default value */
187BmcOption_t      * options = BmcOptionAlloc();
188Ntk_Network_t    * network;
189bAig_Manager_t   * manager;
190array_t          * formulaArray;
191array_t          * LTLformulaArray;
192char             * ltlFileName     = NIL(char);
193
194
195/*
196 * Parse command line options.
197 */
198if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
199     return 1;
200}
201
202
203printf("MAX K %d", options->maxK);
204
205if (verbose) {
206  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
207}
208/*
209 *  Read the network
210 */
211network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
212if (network == NIL(Ntk_Network_t)) {
213  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
214  BmcOptionFree(options);
215  return 1;
216}
217manager = Ntk_NetworkReadMAigManager(network);
218if (manager == NIL(mAig_Manager_t)) {
219  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
220  BmcOptionFree(options);
221  return 1;
222}
223
224Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
225if(abn == NIL(Dbg_Abnormal_t)){
226  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
227  return 1;
228}
229if(verbose)
230  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
231
232
233formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
234if (formulaArray == NIL(array_t)) {
235  (void) fprintf(vis_stderr,
236           "** bmc error: error in parsing CTL* Fromula from file\n");
237  BmcOptionFree(options);
238  return 1;
239}
240if (array_n(formulaArray) == 0) {
241  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
242  BmcOptionFree(options);
243  Ctlsp_FormulaArrayFree(formulaArray);
244  return 1;
245}
246LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
247Ctlsp_FormulaArrayFree(formulaArray);
248if (LTLformulaArray ==  NIL(array_t)){
249  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
250  BmcOptionFree(options);
251  return 1;
252}
253Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
254
255
256
257 /*
258    Compute the cone of influence
259        here : a list of state variables (latches)
260    TODO refine to COI of the property
261  */
262        st_table        *CoiTable =  generateAllLatches(network);
263  /*
264      Generate clauses for each time frame.  This is the old way of generating
265      clauses in BMC.
266    */
267        if(verbose)
268        {       
269                (void) fprintf(vis_stdout, "------      COI       ----\n");
270                printLatch(CoiTable);
271                (void) fprintf(vis_stdout, "--------------------------\n");
272    }
273    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
274
275
276    //Generate ltl CNF
277    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
278    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
279    // cf. BmcLtlVerifyGeneralLtl
280    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
281    fprintf(vis_stdout, "\n");
282    int k = options->maxK;
283    int l;
284    // return the clause number
285    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
286   
287
288        array_t           *objClause = NIL(array_t);
289        objClause = array_alloc(int, 0);   
290        array_insert_last(int, objClause, noLoopIndex);
291        BmcCnfInsertClause(cnfClauses, objClause);
292    array_free(objClause);
293
294        //Add Abnormal
295    st_table * nodeToMvfAigTable =  NIL(st_table);
296    nodeToMvfAigTable =
297(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
298assert(nodeToMvfAigTable != NIL(st_table));
299
300    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
301
302      //loop abnormal
303    int aIndex;
304    Ntk_Node_t * abnNode;
305     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
306     if(aIndex<=0){
307     //set abnormal
308      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
309      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
310      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
311      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
312
313      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
314      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
315      fclose(cnfFile);
316
317      //SAT procedure
318      int res = Dbg_SatCheck("assig",options->cnfFileName);
319
320        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
321        }
322     }
323
324         if(verbose)
325                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
326                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
327       
328Ctlsp_FormulaArrayFree(LTLformulaArray);   
329BmcCnfClausesFree(cnfClauses);
330BmcOptionFree(options);
331return 0;
332 
333}
334/**Function********************************************************************
335
336  Synopsis    [Implements the generate_network_cnf.]
337
338  CommandName [generate_network_cnf]
339
340  CommandSynopsis [generate a CNF view of the network]
341
342  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
343 
344  CommandDescription [This command geerate a CNF of the network in DMACS form.
345  The network may be unroll within k steps.
346  <p>
347
348  Command options:<p> 
349
350  <dl>
351  <dt> -h
352  <dd> Print the command usage.
353  </dl>
354
355  <dt> -v
356  <dd> Verbose mode.
357  </dl>
358
359  <dt> -k
360  <dd> number of steps (default 1).
361  </dl>
362  ]
363
364  SideEffects []
365
366******************************************************************************/
367
368static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
369{
370  BmcOption_t  *options = BmcOptionAlloc();
371  int c;
372  unsigned int i;
373  Ntk_Network_t * network;
374  bAig_Manager_t   * manager;
375  char *  outName = NIL(char);
376   FILE *cnfFile;
377  if (!options){
378    return 1;
379  }
380  options->dbgOut = 0;
381  /*
382   * Parse command line options.
383   */
384  util_getopt_reset();
385  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
386    switch(c) {
387    case 'h':
388      goto usage;
389    case 'k':
390      options->maxK = atoi(util_optarg);
391      break;
392    case 'v':
393      for (i = 0; i < strlen(util_optarg); i++) {
394        if (!isdigit((int)util_optarg[i])) {
395          goto usage;
396        }
397      }
398      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
399      break;
400    default:
401      goto usage;
402    }
403  }
404   if (argc - util_optind != 0)
405   {
406      outName  = util_strsav(argv[util_optind]);
407      /* create SAT Solver input file */
408     options->cnfFileName= outName;
409    options->satInFile = options->cnfFileName;
410    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
411  }
412 
413 
414/*
415 *  Read the network
416 */
417network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
418if (network == NIL(Ntk_Network_t)) {
419  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
420  BmcOptionFree(options);
421  return 1;
422}
423manager = Ntk_NetworkReadMAigManager(network);
424if (manager == NIL(mAig_Manager_t)) {
425  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
426  BmcOptionFree(options);
427  return 1;
428}
429
430 /*
431    Compute the cone of influence
432        here : a list of state variables (latches)
433  */
434st_table        *CoiTable =  generateAllLatches(network);
435
436if(options->verbosityLevel)
437{       
438        (void) fprintf(vis_stdout, "------      COI       ----\n");
439        printLatch(CoiTable);
440        (void) fprintf(vis_stdout, "--------------------------\n");
441}
442BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
443  if(outName != NIL(char))
444  {
445    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
446    fclose(cnfFile);
447  }
448  else
449     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
450
451if(options->verbosityLevel)
452{       
453        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
454    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
455    st_count(CoiTable));
456} 
457   
458BmcOptionFree(options);
459 return 0;
460 usage:
461  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
462  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
463  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
464  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
465  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
466  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
467  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
468  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
469
470  BmcOptionFree(options);
471  return 1;
472}
473
474/**Function********************************************************************
475
476  Synopsis    [Implements the _Debug_test command.]
477
478  CommandName [_Debug_test]
479
480  CommandSynopsis [template for implementing commands]
481
482  CommandArguments [\[-h\] \[-v\]]
483 
484  CommandDescription [This command does nothing useful.  It merely serves as a
485  template for the implementation of new commands.<p>
486
487  Command options:<p> 
488
489  <dl>
490  <dt> -h
491  <dd> Print the command usage.
492  </dl>
493
494  <dt> -v
495  <dd> Verbose mode.
496  </dl>
497  ]
498
499  SideEffects []
500
501******************************************************************************/
502static int
503CommandDebug(
504  Hrc_Manager_t ** hmgr,
505  int  argc,
506  char ** argv)
507{
508  int            c;
509  int            verbose = 0;              /* default value */
510
511  /*
512   * Parse command line options.
513   */
514  util_getopt_reset();
515  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
516    switch(c) {
517      case 'v':
518        verbose = 1;
519        break;
520      case 'h':
521        goto usage;
522      default:
523        goto usage;
524    }
525  }
526
527  if (verbose) {
528    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
529  }
530
531  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
532  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
533  printf("** DEBUG MODE **\n");
534  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
535  printf("model : %s\n", Hrc_NodeReadModelName(n));
536
537  mdd_t * safe   = getSafe(fsm);
538  mdd_t * forbid = getForbidden(fsm);
539  mdd_t * reach  = getReach(fsm);
540 
541  if(safe == NIL(mdd_t))
542  {
543        printf("call command set_safe before\n");
544        return 1;
545  }
546  if(forbid == NIL(mdd_t))
547  {
548        printf("call command set_forbidden before\n");
549        return 1;
550  }
551
552  FILE*  oFile;
553  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
554 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
555//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
556
557  mdd_t * EFState = mdd_and(reach,safe,1,1);
558//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
559
560  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
561  array_t *careStatesArray = array_alloc(mdd_t *, 0);
562  array_insert(mdd_t *, careStatesArray, 0,mddOne);
563
564  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
565                   EFState,
566           fsm->fairnessInfo.states,
567           careStatesArray,
568                   0,
569           McDcLevelNone_c);
570
571  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
572  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
573
574  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
575                   EXEFState,
576           fsm->fairnessInfo.states,
577           careStatesArray,
578                   0,
579           McDcLevelNone_c);
580  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
581  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
582  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
583  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
584  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
585                   andState,
586           fsm->fairnessInfo.states,
587           careStatesArray,
588                   0,
589           McDcLevelNone_c);
590  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
591  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
592  andState =  mdd_xor(EXEFState2,andState);
593  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
594  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
595                   andState,
596           fsm->fairnessInfo.states,
597           careStatesArray,
598                   0,
599           McDcLevelNone_c);
600  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
601  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
602  andState =  mdd_xor(EXEFState2,andState);
603  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
604
605
606
607  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
608  //mdd_GetState_Values(mddManager , EFState, stdout);
609  fclose(oFile);
610
611
612
613
614
615  return 0;             /* normal exit */
616
617  usage:
618  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
619  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
620  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
621  return 1;             /* error exit */
622}
623
624/******************************************/
625/* function that build a bdd for the      */
626/* simple example :                       */
627/*     (state = 0) -> !(state = 1)        */
628/******************************************/
629mdd_t * buildDummyBdd(mdd_manager   *mddManager)
630{
631/** state0 = 0 **/
632 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
633 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
634 mdd_t * state0 =  mdd_one(mddManager);
635 state0 = mdd_and(s0,s1,1,1);
636/** state1 = 1 **/
637 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
638 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
639 mdd_t * state1 =  mdd_one(mddManager);
640 state1 = mdd_and(ns0,ns1,1,1);
641/** state = 0) -> !(state = 1) **/
642 mdd_t * rel =  mdd_one(mddManager);
643 rel =  mdd_or(state0,state1,0,0);
644 
645 return rel;
646}
647
648
649/**Function********************************************************************
650
651  Synopsis    [Implements the transtion command.]
652
653  CommandName [_transition]
654
655  CommandSynopsis [compute new transition relation]
656
657  CommandArguments [\[-h\] \[-v\]]
658 
659  CommandDescription [This command create a new transition relation that is a
660  and of the Bdd of the old one and an other bdd.
661  <p>
662
663  Command options:<p> 
664
665  <dl>
666  <dt> -h
667  <dd> Print the command usage.
668  </dl>
669
670  <dt> -v
671  <dd> Verbose mode.
672  </dl>
673  ]
674
675  SideEffects [Change the fsm]
676
677******************************************************************************/
678
679static int 
680CommandTransition (Hrc_Manager_t ** hmgr,
681                   int  argc, char ** argv){
682int            c;
683int            verbose = 0;              /* default value */
684
685/*
686 * Parse command line options.
687 */
688util_getopt_reset();
689while ((c = util_getopt(argc, argv, "vh")) != EOF) {
690  switch(c) {
691    case 'v':
692      verbose = 1;
693      break;
694    case 'h':
695      goto usage;
696    default:
697      goto usage;
698  }
699}
700
701if (verbose) {
702  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
703}
704
705Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
706Ntk_Network_t  *network      = NIL(Ntk_Network_t);
707mdd_manager    *mddManager; 
708mdd_t          *rel          = NIL(mdd_t);
709graph_t        *partition;
710int            i;
711/******************/
712network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
713if(network == NIL(Ntk_Network_t))
714        return 1;
715fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
716if(fsm ==  NIL(Fsm_Fsm_t))
717        return 1;
718mddManager   = Fsm_FsmReadMddManager(fsm);
719
720
721
722/**********   Build cex  ***********/
723/* Here add the function           */
724/* that build the Bdd to and       */
725/* with the transtion relation     */
726/***********************************/
727rel = buildDummyBdd(mddManager);
728if(rel == NIL(mdd_t))
729{
730        fprintf(vis_stdout,"Problem when building the new relation bdd");
731        return 1;
732}
733if (verbose)
734  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
735
736
737/** Get image_info **/
738Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
739partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
740/**** The complete transtion relation ****/
741// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
742/*****************************************/
743/*** For each latch rebuild the transition function ***/
744/*** mvf table is composed of mdd for each possible ***/
745/*** value of the latch                             ***/
746ImgFunctionData_t * functionData = &(imageInfo->functionData);
747array_t *roots = functionData->roots;
748array_t *rangeVarMddIdArray = functionData->rangeVars;
749char * nodeName;
750arrayForEachItem(char *, roots, i, nodeName) {
751        /* The new relation */ 
752        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
753    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
754    int mddId = array_fetch(int, rangeVarMddIdArray, i);
755        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
756        mdd_t * n_relation = mdd_and(relation,rel,1,1);
757    /* Build for each possible value */
758        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
759        int v ;
760        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
761        for(v = 0; v<nbValue;v++)
762        {
763                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
764                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
765                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
766                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
767
768        }
769        /* Replace the function for the latch */
770        Part_VertexSetFunction(vertex, newMvf);
771//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
772}
773
774/** Change the fsm and the network with a new partition and the new fsm **/
775Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
776                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
777                                          (void *) partition);
778fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
779mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
780mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
781                                      0,0, 0,
782                                      0, 0, Fsm_Rch_Default_c,
783                                      0,1, NIL(array_t),
784                                      (verbose > 0),  NIL(array_t));
785fsm->reachabilityInfo.initialStates = init;
786fsm->reachabilityInfo.reachableStates = reach;
787if(verbose)
788        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
789
790Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
791                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
792                         (void *) fsm);
793
794return 0;               /* normal exit */
795
796usage:
797(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
798(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
799(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
800return 1;               /* error exit */
801
802}
803
804
Note: See TracBrowser for help on using the repository browser.