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

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

add part of cex
File size: 38.4 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 %d \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("%d mdd %d ",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);
972array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
973array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
974array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
975printf("Next Names\n");
976printStringArray(nextNames);
977printf("Next Ids\n");
978printIntArray(nextIds);
979printf("Current Ids\n");
980printIntArray(currentIds);
981Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
982 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
983
984lsGen gen;
985vertex_t *vertexPtr;
986
987
988//foreach_vertex(part, gen, vertexPtr) {
989//      if (PartVertexReadName(vertexPtr) != NIL(char)) {
990//        (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr));
991//      }
992//}
993vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
994Mvf_Function_t*  vertexFunction = PartVertexReadFunction(v_s2);
995  if (vertexFunction != NIL(Mvf_Function_t)) {
996printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
997}
998else
999  printf("no fonction");
1000
1001Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
1002 mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
1003 mdd_t * s1 =  mdd_eq_c(mddManager,22, 0);
1004 mdd_t * state0 =  mdd_one(mddManager);
1005 mdd_t * state1 =  mdd_one(mddManager);
1006 state0 = mdd_and(s0,s1,1,1);
1007 state1 = mdd_not(state0);
1008  array_insert(mdd_t *, newMvf, 1, state0);
1009  array_insert(mdd_t *, newMvf, 0, state1);
1010Mvf_Function_t * newMvf2  = Mvf_FunctionAlloc( mddManager,2);
1011 mdd_t * s0_2 =  mdd_eq_c(mddManager,20, 1);
1012 mdd_t * s1_2 =  mdd_eq_c(mddManager,22, 0);
1013 mdd_t * state0_2 =  mdd_one(mddManager);
1014 mdd_t * state1_2 =  mdd_one(mddManager);
1015 state0_2 = mdd_and(s0_2,s1_2,1,1);
1016 state1_2 = mdd_not(state0_2);
1017  array_insert(mdd_t *, newMvf2, 1, state0_2);
1018  array_insert(mdd_t *, newMvf2, 0, state1_2);
1019FILE * file = fopen("mvf.txt","w");
1020foreach_vertex(part, gen, vertexPtr) {
1021fprintf(file,"*********  (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) );
1022 Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr);
1023 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
1024 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file);
1025 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
1026 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file);
1027
1028 if(Part_VertexReadMddId(vertexPtr) == 17)
1029 {
1030 Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
1031
1032   mdd_t * new0 = Mvf_FunctionReadComponent(fun,0);
1033   new0 = mdd_and(new0,state1,1,1);
1034   mdd_t * new1 = Mvf_FunctionReadComponent(fun,1);
1035   new1 = mdd_and(new1,state0,1,1);
1036    array_insert(mdd_t *, newMvf, 1, new1);
1037    array_insert(mdd_t *, newMvf, 0, new0);
1038    mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
1039     mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
1040    Part_VertexSetFunction(vertexPtr, newMvf);
1041 }
1042 else{
1043  Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf);
1044  Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf);
1045  //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2);
1046 mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0);
1047 mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
1048 mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1);
1049 mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
1050
1051 Part_VertexSetFunction(vertexPtr, newFun);
1052 Part_VertexSetFunction(vertexPtr, newFun1);
1053// Part_VertexSetFunction(vertexPtr, newFun2);
1054 }
1055}
1056fclose(file);
1057
1058
1059
1060
1061  array_t       * psVars = fsm->fsmData.presentStateVars;
1062   int  numLatches = array_n(psVars);
1063
1064
1065   for (i=0; i<numLatches; i++){
1066    int latchMddId = array_fetch(int, psVars, i);
1067    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
1068    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
1069    vertex_t   *initVertex = Part_PartitionFindVertexByName(part,
1070                                Ntk_NodeReadName(initNode));
1071    Mvf_Function_t * fun = PartVertexReadFunction(initVertex);
1072   printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode),
1073   Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) );
1074   
1075 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
1076 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout);
1077 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
1078 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout);
1079
1080
1081    }
1082
1083
1084 /** Change the fsm and the network with a new partition and the new fsm **/
1085Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
1086                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1087                                          (void *) part);
1088fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
1089mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
1090//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
1091mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
1092                                      0,0, 0,
1093                                      0, 0, Fsm_Rch_Default_c,
1094                                      0,1, NIL(array_t),
1095                                      (verbose > 0),  NIL(array_t));
1096//mdd_t * n_reach =  Mvf_MddComposeWithFunction(reach, 17 , newMvf);
1097//fsm->reachabilityInfo.initialStates = n_init;
1098//fsm->reachabilityInfo.reachableStates = n_reach;
1099//     
1100//   
1101   
1102Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
1103                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1104                         (void *) fsm); 
1105
1106Fsm_FsmReachabilityPrintResults(fsm,3, 0);
1107//
1108//
1109mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
1110
1111/*
1112// Read_blif_mv
1113  FILE *fpC;
1114  fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
1115  boolean isCanonicalC = 0;
1116  boolean isIncrementalC = 0;
1117  boolean isVerboseC = 0;
1118  hmgrCex =  Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
1119
1120//flatten_hier
1121  lsList         varNameList = (lsList) NULL;
1122  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
1123  networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
1124  Ntk_NetworkSetMddManager(networkCex, mddManager);
1125//static_order
1126  static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
1127  static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
1128  static Ord_OrderType  suppliedOrderType = Ord_Unassigned_c;
1129  static Ord_OrderType  generatedOrderType = Ord_InputAndLatch_c;
1130  static boolean        nsAfterSupport = FALSE;
1131  lsList                suppliedNodeList = (lsList) NULL;
1132
1133 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport,
1134                            generatedOrderType, suppliedOrderType,
1135                            suppliedNodeList, isVerboseC);
1136 //build_partition_mdd
1137 char * modelName = Hrc_NodeReadModelName(currentNode);
1138 static Part_PartitionMethod method = Part_Default_c;
1139 graph_t                     *partition;
1140 lsList                      nodeList = lsCreate();
1141 boolean inTermsOfLeaves = FALSE;
1142 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
1143                                          (lsList)0, NIL(mdd_t), method, nodeList,
1144                                          inTermsOfLeaves, isVerboseC, 0);
1145//    PartPartitionPrint(vis_stdout, partition);
1146  printf(" Cex loaded \n");
1147fsmCex          =  Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
1148array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
1149array_t * nextIdsCex =   Fsm_FsmReadNextStateVars(fsmCex);
1150printf("Next Names\n");
1151printStringArray(nextNamesCex);
1152printf("Next Ids\n");
1153printIntArray(nextIdsCex);
1154
1155mddManager =  Fsm_FsmReadMddManager(fsm);
1156mdd_manager * mddManagerCex =  Fsm_FsmReadMddManager(fsmCex);
1157
1158array_t *mvar_list, *bvar_list;
1159mvar_list = mdd_ret_mvar_list(mddManager);
1160bvar_list = mdd_ret_bvar_list(mddManager);
1161printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
1162printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
1163 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
1164// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
1165graph_t * part = Fsm_FsmReadPartition(fsm);
1166printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
1167*/
1168/** state0 = s0 **/
1169// mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
1170// mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
1171// mdd_t * state0 =  mdd_one(mddManager);
1172// state0 = mdd_and(s0,s1,1,1);
1173///** Next state1 = s2 + !s2  **/
1174//
1175// mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
1176// mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
1177// mdd_t * state1 =  mdd_one(mddManager);
1178// state1 = mdd_and(ns0,ns1,1,1);
1179// state1 = mdd_or(state1,state1,1,0);
1180//
1181///** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
1182// rel =  mdd_one(mddManager);
1183// rel =  mdd_or(state0,state1,0,0);
1184///**********/
1185///** state0 = s2 **/
1186// mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
1187// mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
1188// mdd_t * state02 =  mdd_one(mddManager);
1189// state02 = mdd_and(s02,s12,1,1);
1190///** Next state1 = s3  **/
1191//
1192// mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
1193// mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
1194// mdd_t * state12 =  mdd_one(mddManager);
1195// state12 = mdd_and(ns02,ns12,1,1);
1196//
1197///** state = s0) -> !(Nextstate = s3) **/
1198// mdd_t * new_rel =  mdd_one(mddManager);
1199// new_rel =  mdd_or(state02,state12,0,0);
1200// rel = mdd_and(new_rel,rel,1,1);
1201// mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
1202
1203return 0;               /* normal exit */
1204
1205usage:
1206(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1207(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
1208(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
1209return 1;               /* error exit */
1210
1211}
1212
1213
Note: See TracBrowser for help on using the repository browser.