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

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

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