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

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

Fault candidates OK
File size: 24.5 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);
193array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
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);
298    assert(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      char * nodeName =  Ntk_NodeReadName(abnNode);
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      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
313      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
314      fclose(cnfFile);
315     
316      //SAT procedure
317      //assig assig input from cex
318      //TODO build cex correctly
319      int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel);
320      // Build set of FaultCandidates
321      if (res == SAT_SAT)
322      {
323        char * realNodeName = util_strsav(nodeName);
324        realNodeName[strlen(nodeName)-4] = '\0';
325        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
326        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
327      }
328
329
330      array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
331   }
332
333         if(verbose)
334                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
335                latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
336 
337        (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
338    array_n(faultNodes));
339        (void) fprintf(vis_stdout,"gates : \n");
340    printNodeArray(faultNodes);
341
342   
343Ctlsp_FormulaArrayFree(LTLformulaArray);   
344BmcCnfClausesFree(cnfClauses);
345BmcOptionFree(options);
346array_free(faultNodes);
347return 0;
348 
349}
350/**Function********************************************************************
351
352  Synopsis    [Implements the generate_network_cnf.]
353
354  CommandName [generate_network_cnf]
355
356  CommandSynopsis [generate a CNF view of the network]
357
358  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
359 
360  CommandDescription [This command geerate a CNF of the network in DMACS form.
361  The network may be unroll within k steps.
362  <p>
363
364  Command options:<p> 
365
366  <dl>
367  <dt> -h
368  <dd> Print the command usage.
369  </dl>
370
371  <dt> -v
372  <dd> Verbose mode.
373  </dl>
374
375  <dt> -k
376  <dd> number of steps (default 1).
377  </dl>
378  ]
379
380  SideEffects []
381
382******************************************************************************/
383
384static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
385{
386  BmcOption_t  *options = BmcOptionAlloc();
387  int c;
388  unsigned int i;
389  Ntk_Network_t * network;
390  bAig_Manager_t   * manager;
391  char *  outName = NIL(char);
392   FILE *cnfFile;
393  if (!options){
394    return 1;
395  }
396  options->dbgOut = 0;
397  /*
398   * Parse command line options.
399   */
400  util_getopt_reset();
401  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
402    switch(c) {
403    case 'h':
404      goto usage;
405    case 'k':
406      options->maxK = atoi(util_optarg);
407      break;
408    case 'v':
409      for (i = 0; i < strlen(util_optarg); i++) {
410        if (!isdigit((int)util_optarg[i])) {
411          goto usage;
412        }
413      }
414      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
415      break;
416    default:
417      goto usage;
418    }
419  }
420   if (argc - util_optind != 0)
421   {
422      outName  = util_strsav(argv[util_optind]);
423      /* create SAT Solver input file */
424     options->cnfFileName= outName;
425    options->satInFile = options->cnfFileName;
426    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
427  }
428 
429 
430/*
431 *  Read the network
432 */
433network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
434if (network == NIL(Ntk_Network_t)) {
435  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
436  BmcOptionFree(options);
437  return 1;
438}
439manager = Ntk_NetworkReadMAigManager(network);
440if (manager == NIL(mAig_Manager_t)) {
441  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
442  BmcOptionFree(options);
443  return 1;
444}
445
446 /*
447    Compute the cone of influence
448        here : a list of state variables (latches)
449  */
450st_table        *CoiTable =  generateAllLatches(network);
451
452if(options->verbosityLevel)
453{       
454        (void) fprintf(vis_stdout, "------      COI       ----\n");
455        printLatch(CoiTable);
456        (void) fprintf(vis_stdout, "--------------------------\n");
457}
458BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
459  if(outName != NIL(char))
460  {
461    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
462    fclose(cnfFile);
463  }
464  else
465     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
466
467if(options->verbosityLevel)
468{       
469        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
470    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
471    st_count(CoiTable));
472} 
473   
474BmcOptionFree(options);
475 return 0;
476 usage:
477  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
478  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
479  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
480  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
481  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
482  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
483  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
484  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
485
486  BmcOptionFree(options);
487  return 1;
488}
489
490/**Function********************************************************************
491
492  Synopsis    [Implements the _Debug_test command.]
493
494  CommandName [_Debug_test]
495
496  CommandSynopsis [template for implementing commands]
497
498  CommandArguments [\[-h\] \[-v\]]
499 
500  CommandDescription [This command does nothing useful.  It merely serves as a
501  template for the implementation of new commands.<p>
502
503  Command options:<p> 
504
505  <dl>
506  <dt> -h
507  <dd> Print the command usage.
508  </dl>
509
510  <dt> -v
511  <dd> Verbose mode.
512  </dl>
513  ]
514
515  SideEffects []
516
517******************************************************************************/
518static int
519CommandDebug(
520  Hrc_Manager_t ** hmgr,
521  int  argc,
522  char ** argv)
523{
524  int            c;
525  int            verbose = 0;              /* default value */
526
527  /*
528   * Parse command line options.
529   */
530  util_getopt_reset();
531  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
532    switch(c) {
533      case 'v':
534        verbose = 1;
535        break;
536      case 'h':
537        goto usage;
538      default:
539        goto usage;
540    }
541  }
542
543  if (verbose) {
544    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
545  }
546
547  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
548  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
549  printf("** DEBUG MODE **\n");
550  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
551  printf("model : %s\n", Hrc_NodeReadModelName(n));
552
553  mdd_t * safe   = getSafe(fsm);
554  mdd_t * forbid = getForbidden(fsm);
555  mdd_t * reach  = getReach(fsm);
556 
557  if(safe == NIL(mdd_t))
558  {
559        printf("call command set_safe before\n");
560        return 1;
561  }
562  if(forbid == NIL(mdd_t))
563  {
564        printf("call command set_forbidden before\n");
565        return 1;
566  }
567
568  FILE*  oFile;
569  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
570 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
571//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
572
573  mdd_t * EFState = mdd_and(reach,safe,1,1);
574//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
575
576  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
577  array_t *careStatesArray = array_alloc(mdd_t *, 0);
578  array_insert(mdd_t *, careStatesArray, 0,mddOne);
579
580  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
581                   EFState,
582           fsm->fairnessInfo.states,
583           careStatesArray,
584                   0,
585           McDcLevelNone_c);
586
587  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
588  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
589
590  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
591                   EXEFState,
592           fsm->fairnessInfo.states,
593           careStatesArray,
594                   0,
595           McDcLevelNone_c);
596  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
597  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
598  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
599  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
600  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
601                   andState,
602           fsm->fairnessInfo.states,
603           careStatesArray,
604                   0,
605           McDcLevelNone_c);
606  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
607  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
608  andState =  mdd_xor(EXEFState2,andState);
609  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
610  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
611                   andState,
612           fsm->fairnessInfo.states,
613           careStatesArray,
614                   0,
615           McDcLevelNone_c);
616  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
617  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
618  andState =  mdd_xor(EXEFState2,andState);
619  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
620
621
622
623  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
624  //mdd_GetState_Values(mddManager , EFState, stdout);
625  fclose(oFile);
626
627
628
629
630
631  return 0;             /* normal exit */
632
633  usage:
634  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
635  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
636  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
637  return 1;             /* error exit */
638}
639
640/******************************************/
641/* function that build a bdd for the      */
642/* simple example :                       */
643/*     (state = 0) -> !(state = 1)        */
644/******************************************/
645mdd_t * buildDummyBdd(mdd_manager   *mddManager)
646{
647/** state0 = 0 **/
648 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
649 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
650 mdd_t * state0 =  mdd_one(mddManager);
651 state0 = mdd_and(s0,s1,1,1);
652/** state1 = 1 **/
653 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
654 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
655 mdd_t * state1 =  mdd_one(mddManager);
656 state1 = mdd_and(ns0,ns1,1,1);
657/** state = 0) -> !(state = 1) **/
658 mdd_t * rel =  mdd_one(mddManager);
659 rel =  mdd_or(state0,state1,0,0);
660 
661 return rel;
662}
663
664
665/**Function********************************************************************
666
667  Synopsis    [Implements the transtion command.]
668
669  CommandName [_transition]
670
671  CommandSynopsis [compute new transition relation]
672
673  CommandArguments [\[-h\] \[-v\]]
674 
675  CommandDescription [This command create a new transition relation that is a
676  and of the Bdd of the old one and an other bdd.
677  <p>
678
679  Command options:<p> 
680
681  <dl>
682  <dt> -h
683  <dd> Print the command usage.
684  </dl>
685
686  <dt> -v
687  <dd> Verbose mode.
688  </dl>
689  ]
690
691  SideEffects [Change the fsm]
692
693******************************************************************************/
694
695static int 
696CommandTransition (Hrc_Manager_t ** hmgr,
697                   int  argc, char ** argv){
698int            c;
699int            verbose = 0;              /* default value */
700
701/*
702 * Parse command line options.
703 */
704util_getopt_reset();
705while ((c = util_getopt(argc, argv, "vh")) != EOF) {
706  switch(c) {
707    case 'v':
708      verbose = 1;
709      break;
710    case 'h':
711      goto usage;
712    default:
713      goto usage;
714  }
715}
716
717if (verbose) {
718  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
719}
720
721Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
722Ntk_Network_t  *network      = NIL(Ntk_Network_t);
723mdd_manager    *mddManager; 
724mdd_t          *rel          = NIL(mdd_t);
725graph_t        *partition;
726int            i;
727/******************/
728network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
729if(network == NIL(Ntk_Network_t))
730        return 1;
731fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
732if(fsm ==  NIL(Fsm_Fsm_t))
733        return 1;
734mddManager   = Fsm_FsmReadMddManager(fsm);
735
736
737
738/**********   Build cex  ***********/
739/* Here add the function           */
740/* that build the Bdd to and       */
741/* with the transtion relation     */
742/***********************************/
743rel = buildDummyBdd(mddManager);
744if(rel == NIL(mdd_t))
745{
746        fprintf(vis_stdout,"Problem when building the new relation bdd");
747        return 1;
748}
749if (verbose)
750  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
751
752
753/** Get image_info **/
754Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
755partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
756/**** The complete transtion relation ****/
757// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
758/*****************************************/
759/*** For each latch rebuild the transition function ***/
760/*** mvf table is composed of mdd for each possible ***/
761/*** value of the latch                             ***/
762ImgFunctionData_t * functionData = &(imageInfo->functionData);
763array_t *roots = functionData->roots;
764array_t *rangeVarMddIdArray = functionData->rangeVars;
765char * nodeName;
766arrayForEachItem(char *, roots, i, nodeName) {
767        /* The new relation */ 
768        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
769    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
770    int mddId = array_fetch(int, rangeVarMddIdArray, i);
771        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
772        mdd_t * n_relation = mdd_and(relation,rel,1,1);
773    /* Build for each possible value */
774        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
775        int v ;
776        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
777        for(v = 0; v<nbValue;v++)
778        {
779                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
780                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
781                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
782                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
783
784        }
785        /* Replace the function for the latch */
786        Part_VertexSetFunction(vertex, newMvf);
787//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
788}
789
790/** Change the fsm and the network with a new partition and the new fsm **/
791Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
792                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
793                                          (void *) partition);
794fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
795mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
796mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
797                                      0,0, 0,
798                                      0, 0, Fsm_Rch_Default_c,
799                                      0,1, NIL(array_t),
800                                      (verbose > 0),  NIL(array_t));
801fsm->reachabilityInfo.initialStates = init;
802fsm->reachabilityInfo.reachableStates = reach;
803if(verbose)
804        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
805
806Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
807                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
808                         (void *) fsm);
809
810return 0;               /* normal exit */
811
812usage:
813(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
814(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
815(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
816return 1;               /* error exit */
817
818}
819
820
Note: See TracBrowser for help on using the repository browser.