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

Last change on this file since 103 was 101, checked in by syed, 13 years ago

final
File size: 34.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);
68static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
69
70
71/**AutomaticEnd***************************************************************/
72
73
74/*---------------------------------------------------------------------------*/
75/* Definition of exported functions                                          */
76/*---------------------------------------------------------------------------*/
77
78/**Function********************************************************************
79
80  Synopsis    [Initializes the test package.]
81
82  SideEffects []
83
84  SeeAlso     [Debug_End]
85
86******************************************************************************/
87void
88Debug_Init(void)
89{
90  /*
91   * Add a command to the global command table.  By using the leading
92   * underscore, the command will be listed under "help -a" but not "help".
93   */
94  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
95  Cmd_CommandAdd("_transition",  CommandTransition, 1);
96  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
97  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
98  Cmd_CommandAdd("_cexbdd",      CommandBuildCexBdd, 0);
99  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
100
101}
102
103
104/**Function********************************************************************
105
106  Synopsis    [Ends the test package.]
107
108  SideEffects []
109
110  SeeAlso     [Debug_Init]
111
112******************************************************************************/
113void
114Debug_End(void)
115{
116  /*
117   * For example, free any global memory (if any) which the test package is
118   * responsible for.
119   */
120}
121
122
123/*---------------------------------------------------------------------------*/
124/* Definition of internal functions                                          */
125/*---------------------------------------------------------------------------*/
126
127
128/*---------------------------------------------------------------------------*/
129/* Definition of static functions                                            */
130/*---------------------------------------------------------------------------*/
131
132
133static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
134{
135  Ntk_Network_t * ntk;
136  int c,verbose = 0;
137  array_t * excludes = NIL(array_t);
138  Dbg_Abnormal_t * abnormal;
139  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
140  char * subs;
141  if (ntk == NIL(Ntk_Network_t)) {
142        (void) fprintf(vis_stdout, "** abn error: No network\n");
143        return 1;
144  }
145  while ((c = util_getopt(argc, argv, "vhs:")) != EOF) {
146        switch(c) {
147        case 'h':
148          goto usage;
149                case 'v':
150                        verbose = 1;
151                        break;
152        case 's':
153            subs =  util_strsav(util_optarg);
154            excludes = array_alloc(char*,0);
155            array_insert_last(char*,excludes,subs);
156            break;
157        default :
158          goto usage;
159                }
160 }
161  abnormal = Dbg_DebugAbnormalAlloc(ntk);
162  abnormal->verbose = verbose;
163    printf("SUBS %s \n",subs);
164  Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes);
165  printf("\t # Abnormal predicate created  %d\n", array_n(abnormal->abnormal));
166    return 0;
167  usage : 
168   (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n");
169  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
170  (void) fprintf(vis_stderr, "   -v  \t verbosity\n");
171  (void) fprintf(vis_stderr, "   -s <subsystemName> \texclude the abnormal predicate\
172  for this subssytem\n");
173  return 1;
174}
175
176/**Function********************************************************************
177
178  Synopsis    [Implements the _sat_debug command.]
179
180  CommandName [_sat_debug]
181
182  CommandSynopsis [locate faulty candidates]
183
184  CommandArguments [\[-h\] \[-v\]]
185 
186  CommandDescription [This command compute the fault candidates of a given
187  properties.<p>
188
189  Command options:<p> 
190
191  <dl>
192  <dt> -h
193  <dd> Print the command usage.
194  </dl>
195
196  <dt> -v
197  <dd> Verbose mode.
198  </dl>
199  ]
200
201  SideEffects []
202
203******************************************************************************/
204static int 
205CommandSatDebug(
206Hrc_Manager_t ** hmgr, 
207int argc, 
208char ** argv){
209int            c,i;
210int            verbose = 0;              /* default value */
211BmcOption_t      * options = BmcOptionAlloc();
212Ntk_Network_t    * network;
213bAig_Manager_t   * manager;
214array_t          * formulaArray;
215array_t          * LTLformulaArray;
216array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
217
218/*
219 * Parse command line options.
220 */
221if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
222     return 1;
223}
224
225
226
227if (verbose) {
228  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
229}
230/*
231 *  Read the network
232 */
233network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
234if (network == NIL(Ntk_Network_t)) {
235  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
236  BmcOptionFree(options);
237  return 1;
238}
239manager = Ntk_NetworkReadMAigManager(network);
240if (manager == NIL(mAig_Manager_t)) {
241  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
242  BmcOptionFree(options);
243  return 1;
244}
245
246Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
247if(abn == NIL(Dbg_Abnormal_t)){
248  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
249  return 1;
250}
251if(verbose)
252  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
253
254
255formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
256if (formulaArray == NIL(array_t)) {
257  (void) fprintf(vis_stderr,
258           "** bmc error: error in parsing CTL* Fromula from file\n");
259  BmcOptionFree(options);
260  return 1;
261}
262if (array_n(formulaArray) == 0) {
263  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
264  BmcOptionFree(options);
265  Ctlsp_FormulaArrayFree(formulaArray);
266  return 1;
267}
268LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
269Ctlsp_FormulaArrayFree(formulaArray);
270if (LTLformulaArray ==  NIL(array_t)){
271  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
272  BmcOptionFree(options);
273  return 1;
274}
275Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
276
277
278 /*
279    Compute the cone of influence
280        here : a list of state variables (latches)
281    TODO refine to COI of the property
282  */
283        st_table        *CoiTable =  generateAllLatches(network);
284  /*
285      Generate clauses for each time frame.  This is the old way of generating
286      clauses in BMC.
287    */
288        if(verbose)
289        {       
290                (void) fprintf(vis_stdout, "------      COI       ----\n");
291                printLatch(CoiTable);
292                (void) fprintf(vis_stdout, "--------------------------\n");
293    }
294    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
295
296
297    //Generate ltl CNF
298    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
299    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
300    // cf. BmcLtlVerifyGeneralLtl
301    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
302    fprintf(vis_stdout, "\n");
303    int k = options->maxK;
304    int l;
305    // return the clause number
306    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);    printf("LTL %d  \n",noLoopIndex);
307   
308
309        array_t *objClause = NIL(array_t);
310        objClause = array_alloc(int, 0);   
311        array_insert_last(int, objClause, noLoopIndex);
312        BmcCnfInsertClause(cnfClauses, objClause);
313    array_free(objClause);
314
315        //Add Abnormal
316    st_table * nodeToMvfAigTable =  NIL(st_table);
317    nodeToMvfAigTable =
318    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
319    assert(nodeToMvfAigTable != NIL(st_table));
320
321    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
322
323    //loop abnormal
324    int aIndex;
325    Ntk_Node_t * abnNode;
326    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
327      char * nodeName =  Ntk_NodeReadName(abnNode);
328    //set abnormal for each step
329      array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex);
330      int cnfIndex;
331      int step;
332      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
333      array_t * cnfVal = array_alloc(int,0);
334      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
335        int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses);
336        array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
337        array_insert_last(int,cnfVal,abnIndex);
338        FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
339        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
340        fclose(cnfFile);
341        printf("AINDEX %d\n",aIndex);
342        if(aIndex == 0)
343        {
344        FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0);
345        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
346        fclose(cnfFile);
347         
348        }
349      }//end for each step
350
351      //SAT procedure
352      //assig assig input from cex
353      //TODO build cex correctly
354      int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel);
355      // Build set of FaultCandidates
356      if (res == SAT_SAT)
357      {
358        char * realNodeName = util_strsav(nodeName);
359        realNodeName[strlen(nodeName)-3] = '\0';
360        printf("Real = %s\n", realNodeName);
361        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
362        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
363      }
364
365      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
366        int abnIndex = array_fetch(int,cnfVal,step);       
367        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
368      }
369   }
370
371         if(verbose)
372                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
373                latches \n",cnfClauses->noOfClauses,st_count(CoiTable));
374 
375   
376        (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
377    array_n(faultNodes));
378        (void) fprintf(vis_stdout,"gates : \n");
379
380
381    printNodeArray(faultNodes);
382
383   
384Ctlsp_FormulaArrayFree(LTLformulaArray);   
385BmcCnfClausesFree(cnfClauses);
386BmcOptionFree(options);
387array_free(faultNodes);
388return 0;
389}
390
391/**Function********************************************************************
392
393  Synopsis    [Implements the generate_network_cnf.]
394
395  CommandName [generate_network_cnf]
396
397  CommandSynopsis [generate a CNF view of the network]
398
399  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
400 
401  CommandDescription [This command generate a CNF of the network in DMACS form.
402  The network may be unroll within k steps.
403  <p>
404
405  Command options:<p> 
406
407  <dl>
408  <dt> -h
409  <dd> Print the command usage.
410  </dl>
411
412  <dt> -v
413  <dd> Verbose mode.
414  </dl>
415
416  <dt> -k
417  <dd> number of steps (default 1).
418  </dl>
419  ]
420
421  SideEffects []
422
423******************************************************************************/
424
425static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
426{
427  BmcOption_t  *options = BmcOptionAlloc();
428  int c;
429  unsigned int i;
430  Ntk_Network_t * network;
431  bAig_Manager_t   * manager;
432  char *  outName = NIL(char);
433   FILE *cnfFile;
434  if (!options){
435    return 1;
436  }
437  options->dbgOut = 0;
438  /*
439   * Parse command line options.
440   */
441  util_getopt_reset();
442  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
443    switch(c) {
444    case 'h':
445      goto usage;
446    case 'k':
447      options->maxK = atoi(util_optarg);
448      break;
449    case 'v':
450      for (i = 0; i < strlen(util_optarg); i++) {
451        if (!isdigit((int)util_optarg[i])) {
452          goto usage;
453        }
454      }
455      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
456      break;
457    default:
458      goto usage;
459    }
460  }
461   if (argc - util_optind != 0)
462   {
463     outName  = util_strsav(argv[util_optind]);
464     /* create SAT Solver input file */
465     options->cnfFileName= outName;
466     options->satInFile = options->cnfFileName;
467     cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
468  }
469 
470 
471/*
472 *  Read the network
473 */
474network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
475if (network == NIL(Ntk_Network_t)) {
476  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
477  BmcOptionFree(options);
478  return 1;
479}
480manager = Ntk_NetworkReadMAigManager(network);
481if (manager == NIL(mAig_Manager_t)) {
482  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
483  BmcOptionFree(options);
484  return 1;
485}
486
487 /*
488    Compute the cone of influence
489        here : a list of state variables (latches)
490  */
491st_table        *CoiTable =  generateAllLatches(network);
492
493if(options->verbosityLevel)
494{       
495        (void) fprintf(vis_stdout, "------      COI       ----\n");
496        printLatch(CoiTable);
497        (void) fprintf(vis_stdout, "--------------------------\n");
498}
499BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
500  if(outName != NIL(char))
501  {
502    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
503    fclose(cnfFile);
504  }
505  else
506     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
507
508if(options->verbosityLevel)
509{       
510        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
511    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
512    st_count(CoiTable));
513} 
514   
515BmcOptionFree(options);
516 return 0;
517 usage:
518  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
519  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
520  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
521  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
522  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
523  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
524  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
525  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
526
527  BmcOptionFree(options);
528  return 1;
529}
530
531/**Function********************************************************************
532
533  Synopsis    [Implements the _Debug_test command.]
534
535  CommandName [_Debug_test]
536
537  CommandSynopsis [template for implementing commands]
538
539  CommandArguments [\[-h\] \[-v\]]
540 
541  CommandDescription [This command does nothing useful.  It merely serves as a
542  template for the implementation of new commands.<p>
543
544  Command options:<p> 
545
546  <dl>
547  <dt> -h
548  <dd> Print the command usage.
549  </dl>
550
551  <dt> -v
552  <dd> Verbose mode.
553  </dl>
554  ]
555
556  SideEffects []
557
558******************************************************************************/
559static int
560CommandDebug(
561  Hrc_Manager_t ** hmgr,
562  int  argc,
563  char ** argv)
564{
565  int            c;
566  int            verbose = 0;              /* default value */
567
568  /*
569   * Parse command line options.
570   */
571  util_getopt_reset();
572  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
573    switch(c) {
574      case 'v':
575        verbose = 1;
576        break;
577      case 'h':
578        goto usage;
579      default:
580        goto usage;
581    }
582  }
583
584  if (verbose) {
585    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
586  }
587
588  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
589  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
590  printf("** DEBUG MODE **\n");
591  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
592  printf("model : %s\n", Hrc_NodeReadModelName(n));
593
594  mdd_t * safe   = getSafe(fsm);
595  mdd_t * forbid = getForbidden(fsm);
596  mdd_t * reach  = getReach(fsm);
597 
598  if(safe == NIL(mdd_t))
599  {
600        printf("call command set_safe before\n");
601        return 1;
602  }
603  if(forbid == NIL(mdd_t))
604  {
605        printf("call command set_forbidden before\n");
606        return 1;
607  }
608
609  FILE*  oFile;
610  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
611 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
612//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
613
614  mdd_t * EFState = mdd_and(reach,safe,1,1);
615//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
616
617  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
618  array_t *careStatesArray = array_alloc(mdd_t *, 0);
619  array_insert(mdd_t *, careStatesArray, 0,mddOne);
620
621  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
622                   EFState,
623           fsm->fairnessInfo.states,
624           careStatesArray,
625                   0,
626           McDcLevelNone_c);
627
628  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
629  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
630
631  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
632                   EXEFState,
633           fsm->fairnessInfo.states,
634           careStatesArray,
635                   0,
636           McDcLevelNone_c);
637  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
638  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
639  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
640  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
641  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
642                   andState,
643           fsm->fairnessInfo.states,
644           careStatesArray,
645                   0,
646           McDcLevelNone_c);
647  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
648  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
649  andState =  mdd_xor(EXEFState2,andState);
650  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
651  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
652                   andState,
653           fsm->fairnessInfo.states,
654           careStatesArray,
655                   0,
656           McDcLevelNone_c);
657  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
658  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
659  andState =  mdd_xor(EXEFState2,andState);
660  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
661
662
663
664  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
665  //mdd_GetState_Values(mddManager , EFState, stdout);
666  fclose(oFile);
667
668
669
670
671
672  return 0;             /* normal exit */
673
674  usage:
675  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
676  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
677  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
678  return 1;             /* error exit */
679}
680
681/******************************************/
682/* function that build a bdd for the      */
683/* simple example :                       */
684/*     (state = 0) -> !(state = 1)        */
685/******************************************/
686mdd_t * buildDummyBdd(mdd_manager   *mddManager)
687{
688/** state0 = 0 **/
689 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
690 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
691 mdd_t * state0 =  mdd_one(mddManager);
692 state0 = mdd_and(s0,s1,1,1);
693/** state1 = 1 **/
694 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
695 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
696 mdd_t * state1 =  mdd_one(mddManager);
697 state1 = mdd_and(ns0,ns1,1,1);
698/** state = 0) -> !(state = 1) **/
699 mdd_t * rel =  mdd_one(mddManager);
700 rel =  mdd_or(state0,state1,0,0);
701 
702 return rel;
703}
704mdd_t * buildDummy2(mdd_manager * mddManager)
705{
706 mdd_t * rel = NIL(mdd_t);
707 mdd_t * state0 = mdd_one(mddManager);
708 mdd_t * state2 = mdd_one(mddManager);
709 mdd_t * state3 = mdd_one(mddManager);
710  // state0 = s0
711 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
712 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
713 state0 = mdd_and(s0,s1,1,1);
714  // state2 = s2
715 s0 =  mdd_eq_c(mddManager,0, 0);
716 s1 =  mdd_eq_c(mddManager,2, 1);
717 state2 = mdd_and(s0,s1,1,1);
718  // state3 = s3
719 s0 =  mdd_eq_c(mddManager,0, 1);
720 s1 =  mdd_eq_c(mddManager,2, 1);
721 state3 = mdd_and(s0,s1,1,1);
722// Build transition relation
723
724 array_t * mvarVal = array_alloc(int,0);
725 array_insert_last(int, mvarVal,2);
726 array_t * val = array_alloc(int,0);
727 array_t * mvarName = array_alloc(char*,0);
728 array_insert_last(char*, mvarName,"S1");
729 int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
730 array_insert(char*, mvarName,0,"I");
731 int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
732 array_insert_last(int, val,1);
733 mdd_t * e1 = mdd_literal(mddManager, e1Id,val);
734 mdd_t * e0 = mdd_literal(mddManager, e0Id,val);
735 mdd_t * tmp2 = mdd_and(e1,e0,0,0);
736mdd_t *  ne2_1 = mdd_or(e1,tmp2,1,1);
737mdd_t *  ne2_0 = mdd_and(e1,e0,0,1);
738
739array_insert(char*, mvarName,0,"Next_SI");
740int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
741Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2);
742Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1);
743Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0);
744mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id);
745
746//bdd_print(relation);
747mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout);
748 //bdd_ite
749 return rel;
750
751}
752
753/**Function********************************************************************
754
755  Synopsis    [Implements the transtion command.]
756
757  CommandName [_transition]
758
759  CommandSynopsis [compute new transition relation]
760
761  CommandArguments [\[-h\] \[-v\]]
762 
763  CommandDescription [This command create a new transition relation that is a
764  and of the Bdd of the old one and another bdd.
765  <p>
766
767  Command options:<p> 
768
769  <dl>
770  <dt> -h
771  <dd> Print the command usage.
772  </dl>
773
774  <dt> -v
775  <dd> Verbose mode.
776  </dl>
777  ]
778
779  SideEffects [Change the fsm]
780
781******************************************************************************/
782
783static int 
784CommandTransition (Hrc_Manager_t ** hmgr,
785                   int  argc, char ** argv){
786int            c;
787int            verbose = 0;              /* default value */
788
789/*
790 * Parse command line options.
791 */
792util_getopt_reset();
793while ((c = util_getopt(argc, argv, "vh")) != EOF) {
794  switch(c) {
795    case 'v':
796      verbose = 1;
797      break;
798    case 'h':
799      goto usage;
800    default:
801      goto usage;
802  }
803}
804
805if (verbose) {
806  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
807}
808
809Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
810Ntk_Network_t  *network      = NIL(Ntk_Network_t);
811mdd_manager    *mddManager; 
812mdd_t          *rel          = NIL(mdd_t);
813graph_t        *partition;
814int            i;
815/******************/
816network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
817if(network == NIL(Ntk_Network_t))
818        return 1;
819fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
820if(fsm ==  NIL(Fsm_Fsm_t))
821        return 1;
822mddManager   = Fsm_FsmReadMddManager(fsm);
823
824
825
826/**********   Build cex  ***********/
827/* Here add the function           */
828/* that build the Bdd to and       */
829/* with the transtion relation     */
830/***********************************/
831rel = buildDummyBdd(mddManager);
832if(rel == NIL(mdd_t))
833{
834        fprintf(vis_stdout,"Problem when building the new relation bdd\n");
835        return 1;
836}
837if (verbose)
838  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
839
840
841/** Get image_info **/
842Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
843partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
844/**** The complete transtion relation ****/
845// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
846/*****************************************/
847/*** For each latch rebuild the transition function ***/
848/*** mvf table is composed of mdd for each possible ***/
849/*** value of the latch                             ***/
850ImgFunctionData_t * functionData = &(imageInfo->functionData);
851array_t *roots = functionData->roots;
852array_t *rangeVarMddIdArray = functionData->rangeVars;
853char * nodeName;
854arrayForEachItem(char *, roots, i, nodeName) {
855 
856        /* The new relation */ 
857        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
858    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
859    int mddId = array_fetch(int, rangeVarMddIdArray, i);
860        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
861    if(verbose){
862      int x;
863      mdd_t * comp;
864
865      Mvf_FunctionForEachComponent( mvf, x, comp){
866        printf("%s,%d mdd %d ",nodeName,x,mddId);
867        mdd_FunctionPrintMain (mddManager ,comp,"MVF",vis_stdout);
868      }
869    }
870
871        mdd_t * n_relation = mdd_and(relation,rel,1,1);
872    /* Build for each possible value */
873        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
874        int v ;
875        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
876        for(v = 0; v<nbValue;v++)
877        {
878                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
879                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
880                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
881                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
882
883
884        }
885        /* Replace the function for the latch */
886        Part_VertexSetFunction(vertex, newMvf);
887//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
888}
889
890/** Change the fsm and the network with a new partition and the new fsm **/
891Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
892                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
893                                          (void *) partition);
894fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
895mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
896mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
897                                      0,0, 0,
898                                      0, 0, Fsm_Rch_Default_c,
899                                      0,1, NIL(array_t),
900                                      (verbose > 0),  NIL(array_t));
901fsm->reachabilityInfo.initialStates = init;
902fsm->reachabilityInfo.reachableStates = reach;
903if(verbose)
904        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
905
906Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
907                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
908                         (void *) fsm);
909
910return 0;               /* normal exit */
911
912usage:
913(void) fprintf(vis_stderr, "usage: _transition [-h] [-v]\n");
914(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
915(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
916return 1;               /* error exit */
917
918}
919
920static int 
921CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
922                   int  argc, char ** argv){
923int            c;
924int            verbose = 0;              /* default value */
925
926/*
927 * Parse command line options.
928 */
929util_getopt_reset();
930while ((c = util_getopt(argc, argv, "vh")) != EOF) {
931  switch(c) {
932    case 'v':
933      verbose = 1;
934      break;
935    case 'h':
936      goto usage;
937    default:
938      goto usage;
939  }
940}
941
942if (verbose) {
943  (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
944}
945
946Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
947Ntk_Network_t  *network      = NIL(Ntk_Network_t);
948mdd_manager    *mddManager; 
949Hrc_Manager_t  *hmgrCex       = NIL(Hrc_Manager_t);
950Fsm_Fsm_t      *fsmCex        = NIL(Fsm_Fsm_t);
951Ntk_Network_t  *networkCex    = NIL(Ntk_Network_t);
952mdd_t          *rel           = NIL(mdd_t);
953int            i;
954/******************/
955network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
956if(network == NIL(Ntk_Network_t))
957        return 1;
958fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
959if(fsm ==  NIL(Fsm_Fsm_t))
960        return 1;
961mddManager   = Fsm_FsmReadMddManager(fsm);
962
963mdd_t * initOrig  = Fsm_FsmComputeInitialStates(fsm);
964mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout);
965
966/**********   Build cex  ***********/
967/* Here add the function           */
968/* that build the Bdd to and       */
969/* with the transtion relation     */
970/***********************************/
971//rel = buildDummyBdd(mddManager);
972 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
973 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
974Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
975 mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
976 mdd_t * s1 =  mdd_eq_c(mddManager,22, 0);
977 mdd_t * state0 =  mdd_one(mddManager);
978 mdd_t * state1 =  mdd_one(mddManager);
979 state0 = mdd_and(s0,s1,1,1);
980 mdd_t * state12 = mdd_and(s0,s1,0,1);
981 state1 = mdd_not(state0);
982  array_insert(mdd_t *, newMvf, 1, state0);
983  array_insert(mdd_t *, newMvf, 0, state1);
984 mdd_t * ns1 =  mdd_eq_c(mddManager,17, 1);
985Mvf_Function_t * newNS  = Mvf_FunctionAlloc( mddManager,2);
986Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1));
987Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0));
988
989mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout);
990vertex_t * vert;
991vert = Part_PartitionFindVertexByName(part,"cex.s2");
992Part_VertexSetFunction(vert, newNS);
993
994vert = Part_PartitionFindVertexByName(part,"cex.s3");
995 mdd_t * ns1S3 =  mdd_eq_c(mddManager,14, 1);
996Mvf_Function_t * newS3  = Mvf_FunctionAlloc( mddManager,2);
997Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1));
998Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0));
999Part_VertexSetFunction(vert, newS3);
1000
1001// Initial state
1002mdd_t * ns1Init =  mdd_eq_c(mddManager,3, 1);
1003
1004Mvf_Function_t * newNSInit  = Mvf_FunctionAlloc(mddManager,2);
1005Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1));
1006Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0));
1007mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout);
1008Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"),
1009newNSInit);
1010
1011
1012
1013
1014 /** Change the fsm and the network with a new partition and the new fsm **/
1015Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
1016                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1017                                          (void *) part);
1018fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part);
1019
1020
1021mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
1022//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
1023mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
1024                                      0,0, 0,
1025                                      0, 0, Fsm_Rch_Default_c,
1026                                      0,1, NIL(array_t),
1027                                      (verbose > 0),  NIL(array_t));
1028fsm->reachabilityInfo.initialStates = init;
1029fsm->reachabilityInfo.reachableStates = reach;
1030       
1031   
1032   
1033Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
1034                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1035                         (void *) fsm); 
1036
1037Img_ImageInfoUpdateVariables(fsm->imageInfo,
1038                                 fsm->partition,
1039                                 fsm->fsmData.presentStateVars,
1040                                 fsm->fsmData.inputVars,
1041                                 fsm->fsmData.presentStateCube,
1042                                 fsm->fsmData.inputCube);
1043Fsm_FsmReachabilityPrintResults(fsm,3, 0);
1044//
1045//
1046mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
1047
1048/*
1049// Read_blif_mv
1050  FILE *fpC;
1051  fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
1052  boolean isCanonicalC = 0;
1053  boolean isIncrementalC = 0;
1054  boolean isVerboseC = 0;
1055  hmgrCex =  Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
1056
1057//flatten_hier
1058  lsList         varNameList = (lsList) NULL;
1059  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
1060  networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
1061  Ntk_NetworkSetMddManager(networkCex, mddManager);
1062//static_order
1063  static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
1064  static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
1065  static Ord_OrderType  suppliedOrderType = Ord_Unassigned_c;
1066  static Ord_OrderType  generatedOrderType = Ord_InputAndLatch_c;
1067  static boolean        nsAfterSupport = FALSE;
1068  lsList                suppliedNodeList = (lsList) NULL;
1069
1070 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport,
1071                            generatedOrderType, suppliedOrderType,
1072                            suppliedNodeList, isVerboseC);
1073 //build_partition_mdd
1074 char * modelName = Hrc_NodeReadModelName(currentNode);
1075 static Part_PartitionMethod method = Part_Default_c;
1076 graph_t                     *partition;
1077 lsList                      nodeList = lsCreate();
1078 boolean inTermsOfLeaves = FALSE;
1079 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
1080                                          (lsList)0, NIL(mdd_t), method, nodeList,
1081                                          inTermsOfLeaves, isVerboseC, 0);
1082//    PartPartitionPrint(vis_stdout, partition);
1083  printf(" Cex loaded \n");
1084fsmCex          =  Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
1085array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
1086array_t * nextIdsCex =   Fsm_FsmReadNextStateVars(fsmCex);
1087printf("Next Names\n");
1088printStringArray(nextNamesCex);
1089printf("Next Ids\n");
1090printIntArray(nextIdsCex);
1091
1092mddManager =  Fsm_FsmReadMddManager(fsm);
1093mdd_manager * mddManagerCex =  Fsm_FsmReadMddManager(fsmCex);
1094
1095array_t *mvar_list, *bvar_list;
1096mvar_list = mdd_ret_mvar_list(mddManager);
1097bvar_list = mdd_ret_bvar_list(mddManager);
1098printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
1099printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
1100 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
1101// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
1102graph_t * part = Fsm_FsmReadPartition(fsm);
1103printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
1104*/
1105return 0;               /* normal exit */
1106
1107usage:
1108(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1109(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
1110(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
1111return 1;               /* error exit */
1112
1113}
1114
1115
Note: See TracBrowser for help on using the repository browser.