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

Last change on this file since 93 was 45, checked in by cecile, 13 years ago

fichier biblio avec lien sur le compte verif
File size: 30.4 KB
RevLine 
[27]1/**CFile***********************************************************************
2
3  FileName    [debug.c]
4
5  PackageName [debug]
6
[30]7  Synopsis    [Debug package initialization, ending, and the command debug]
[27]8
[35]9  Author      [Cecile B.]
[27]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"
[30]33#include "imgInt.h"
34#include "partInt.h"
[27]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
[35]63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
[27]64static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
[30]65static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
[35]66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
[41]67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
[45]68static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
[27]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   */
[35]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);
[45]98  Cmd_CommandAdd("_cexbdd",      CommandBuildCexBdd, 0);
[41]99  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
[27]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
[35]132
[36]133static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
[35]134{
135  Ntk_Network_t * ntk;
[44]136  int c,verbose = 0;
137  array_t * excludes = NIL(array_t);
[36]138  Dbg_Abnormal_t * abnormal;
[35]139  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
[44]140  char * subs;
[35]141  if (ntk == NIL(Ntk_Network_t)) {
142        (void) fprintf(vis_stdout, "** abn error: No network\n");
143        return 1;
144  }
[44]145  while ((c = util_getopt(argc, argv, "vhs:")) != EOF) {
[36]146        switch(c) {
[44]147        case 'h':
148          goto usage;
[36]149                case 'v':
150                        verbose = 1;
151                        break;
[44]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;
[35]159                }
[36]160 }
161  abnormal = Dbg_DebugAbnormalAlloc(ntk);
162  abnormal->verbose = verbose;
[44]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;
[35]174}
[44]175
[27]176/**Function********************************************************************
177
[35]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 */
[41]211BmcOption_t      * options = BmcOptionAlloc();
212Ntk_Network_t    * network;
213bAig_Manager_t   * manager;
214array_t          * formulaArray;
215array_t          * LTLformulaArray;
[42]216array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
[35]217
218/*
219 * Parse command line options.
220 */
[41]221if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
222     return 1;
223}
[35]224
[41]225
[35]226
227if (verbose) {
228  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
229}
[41]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;
[35]238}
[41]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");
[35]242  BmcOptionFree(options);
243  return 1;
244}
245
[40]246Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
[41]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)));
[38]253
254
[41]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);
[38]265  Ctlsp_FormulaArrayFree(formulaArray);
[41]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);
[38]276
277
[35]278 /*
279    Compute the cone of influence
[38]280        here : a list of state variables (latches)
[41]281    TODO refine to COI of the property
[35]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    */
[41]288        if(verbose)
[35]289        {       
290                (void) fprintf(vis_stdout, "------      COI       ----\n");
291                printLatch(CoiTable);
292                (void) fprintf(vis_stdout, "--------------------------\n");
293    }
[41]294    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
[38]295
[41]296
[38]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
[41]301    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
302    fprintf(vis_stdout, "\n");
[38]303    int k = options->maxK;
304    int l;
305    // return the clause number
[44]306    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);    printf("LTL %d  \n",noLoopIndex);
[38]307   
[41]308
[42]309        array_t *objClause = NIL(array_t);
[40]310        objClause = array_alloc(int, 0);   
311        array_insert_last(int, objClause, noLoopIndex);
312        BmcCnfInsertClause(cnfClauses, objClause);
313    array_free(objClause);
[38]314
[41]315        //Add Abnormal
316    st_table * nodeToMvfAigTable =  NIL(st_table);
317    nodeToMvfAigTable =
[42]318    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
319    assert(nodeToMvfAigTable != NIL(st_table));
[38]320
[44]321    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
[38]322
[42]323    //loop abnormal
[41]324    int aIndex;
325    Ntk_Node_t * abnNode;
[42]326    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
327      char * nodeName =  Ntk_NodeReadName(abnNode);
[44]328    //set abnormal for each step
329      array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex);
330      int cnfIndex;
331      int step;
[41]332      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
[44]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
[41]351      //SAT procedure
[42]352      //assig assig input from cex
353      //TODO build cex correctly
[44]354      int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel);
[42]355      // Build set of FaultCandidates
356      if (res == SAT_SAT)
357      {
358        char * realNodeName = util_strsav(nodeName);
[44]359        realNodeName[strlen(nodeName)-3] = '\0';
360        printf("Real = %s\n", realNodeName);
[42]361        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
362        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
363      }
[38]364
[44]365      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
366        int abnIndex = array_fetch(int,cnfVal,step);       
367        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
368      }
[42]369   }
370
[35]371         if(verbose)
372                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
[42]373                latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
374 
[44]375   
[42]376        (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
377    array_n(faultNodes));
378        (void) fprintf(vis_stdout,"gates : \n");
[44]379
380
[42]381    printNodeArray(faultNodes);
382
383   
[41]384Ctlsp_FormulaArrayFree(LTLformulaArray);   
[35]385BmcCnfClausesFree(cnfClauses);
386BmcOptionFree(options);
[42]387array_free(faultNodes);
[35]388return 0;
[41]389}
[44]390
[41]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 geerate 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   {
[44]463     outName  = util_strsav(argv[util_optind]);
464     /* create SAT Solver input file */
[41]465     options->cnfFileName= outName;
[44]466     options->satInFile = options->cnfFileName;
467     cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
[41]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");
[35]520  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
[41]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");
[35]526
[41]527  BmcOptionFree(options);
528  return 1;
[35]529}
[41]530
[35]531/**Function********************************************************************
532
[27]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
[30]681/******************************************/
682/* function that build a bdd for the      */
683/* simple example :                       */
684/*     (state = 0) -> !(state = 1)        */
685/******************************************/
686mdd_t * buildDummyBdd(mdd_manager   *mddManager)
[27]687{
[30]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}
[45]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
[27]723
[45]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);
[27]738
[45]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
[27]753/**Function********************************************************************
754
[30]755  Synopsis    [Implements the transtion command.]
[27]756
[30]757  CommandName [_transition]
[27]758
[30]759  CommandSynopsis [compute new transition relation]
[27]760
[30]761  CommandArguments [\[-h\] \[-v\]]
762 
763  CommandDescription [This command create a new transition relation that is a
[45]764  and of the Bdd of the old one and another bdd.
[30]765  <p>
[27]766
[30]767  Command options:<p> 
[27]768
[30]769  <dl>
770  <dt> -h
771  <dd> Print the command usage.
772  </dl>
[27]773
[30]774  <dt> -v
775  <dd> Verbose mode.
776  </dl>
777  ]
[27]778
[30]779  SideEffects [Change the fsm]
[27]780
781******************************************************************************/
782
783static int 
[30]784CommandTransition (Hrc_Manager_t ** hmgr,
[27]785                   int  argc, char ** argv){
[30]786int            c;
787int            verbose = 0;              /* default value */
[27]788
[30]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;
[27]802  }
[30]803}
[27]804
[30]805if (verbose) {
806  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
807}
[27]808
[30]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);
[27]823
824
825
[30]826/**********   Build cex  ***********/
827/* Here add the function           */
828/* that build the Bdd to and       */
829/* with the transtion relation     */
830/***********************************/
[45]831rel = buildDummy3(mddManager,network);
[30]832if(rel == NIL(mdd_t))
833{
[45]834        fprintf(vis_stdout,"Problem when building the new relation bdd\n");
[30]835        return 1;
[27]836}
[37]837if (verbose)
838  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
[27]839
[37]840
[30]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        /* The new relation */ 
856        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
857    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
858    int mddId = array_fetch(int, rangeVarMddIdArray, i);
859        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
[45]860    mdd_FunctionPrintMain (mddManager ,relation,"MVF",vis_stdout);
861
[30]862        mdd_t * n_relation = mdd_and(relation,rel,1,1);
863    /* Build for each possible value */
864        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
865        int v ;
866        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
867        for(v = 0; v<nbValue;v++)
868        {
869                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
870                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
871                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
872                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
[27]873
[45]874
[30]875        }
876        /* Replace the function for the latch */
877        Part_VertexSetFunction(vertex, newMvf);
878//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
[27]879}
880
[37]881/** Change the fsm and the network with a new partition and the new fsm **/
882Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
883                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
884                                          (void *) partition);
885fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
[30]886mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
[37]887mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
[30]888                                      0,0, 0,
889                                      0, 0, Fsm_Rch_Default_c,
890                                      0,1, NIL(array_t),
891                                      (verbose > 0),  NIL(array_t));
[37]892fsm->reachabilityInfo.initialStates = init;
893fsm->reachabilityInfo.reachableStates = reach;
[30]894if(verbose)
895        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
[27]896
[37]897Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
898                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
899                         (void *) fsm);
[27]900
[30]901return 0;               /* normal exit */
[27]902
[30]903usage:
904(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
905(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
906(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
907return 1;               /* error exit */
[27]908
909}
910
[45]911static int 
912CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
913                   int  argc, char ** argv){
914int            c;
915int            verbose = 0;              /* default value */
[27]916
[45]917/*
918 * Parse command line options.
919 */
920util_getopt_reset();
921while ((c = util_getopt(argc, argv, "vh")) != EOF) {
922  switch(c) {
923    case 'v':
924      verbose = 1;
925      break;
926    case 'h':
927      goto usage;
928    default:
929      goto usage;
930  }
931}
932
933if (verbose) {
934  (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
935}
936
937Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
938Ntk_Network_t  *network      = NIL(Ntk_Network_t);
939mdd_manager    *mddManager; 
940mdd_t          *rel          = NIL(mdd_t);
941int            i;
942/******************/
943network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
944if(network == NIL(Ntk_Network_t))
945        return 1;
946fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
947if(fsm ==  NIL(Fsm_Fsm_t))
948        return 1;
949mddManager   = Fsm_FsmReadMddManager(fsm);
950
951
952
953/**********   Build cex  ***********/
954/* Here add the function           */
955/* that build the Bdd to and       */
956/* with the transtion relation     */
957/***********************************/
958//rel = buildDummyBdd(mddManager);
959array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
960array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
961
962/** state0 = s0 **/
963 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
964 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
965 mdd_t * state0 =  mdd_one(mddManager);
966 state0 = mdd_and(s0,s1,1,1);
967/** Next state1 = s2 + !s2  **/
968
969 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
970 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
971 mdd_t * state1 =  mdd_one(mddManager);
972 state1 = mdd_and(ns0,ns1,1,1);
973 state1 = mdd_or(state1,state1,1,0);
974
975/** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
976 rel =  mdd_one(mddManager);
977 rel =  mdd_or(state0,state1,0,0);
978/**********/
979/** state0 = s2 **/
980 mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
981 mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
982 mdd_t * state02 =  mdd_one(mddManager);
983 state02 = mdd_and(s02,s12,1,1);
984/** Next state1 = s3  **/
985
986 mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
987 mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
988 mdd_t * state12 =  mdd_one(mddManager);
989 state12 = mdd_and(ns02,ns12,1,1);
990
991/** state = s0) -> !(Nextstate = s3) **/
992 mdd_t * new_rel =  mdd_one(mddManager);
993 new_rel =  mdd_or(state02,state12,0,0);
994 rel = mdd_and(new_rel,rel,1,1);
995 mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
996
997return 0;               /* normal exit */
998
999usage:
1000(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1001(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
1002(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
1003return 1;               /* error exit */
1004
1005}
1006
1007
Note: See TracBrowser for help on using the repository browser.