Index: /vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.c	(revision 27)
+++ /vis_dev/vis-2.3/src/debug/debug.c	(revision 27)
@@ -0,0 +1,576 @@
+/**CFile***********************************************************************
+
+  FileName    [debug.c]
+
+  PackageName [debug]
+
+  Synopsis    [Test package initialization, ending, and the command test.]
+
+  Author      [Originated from SIS.]
+
+  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
+  All rights reserved.
+
+  Permission is hereby granted, without written agreement and without license
+  or royalty fees, to use, copy, modify, and distribute this software and its
+  documentation for any purpose, provided that the above copyright notice and
+  the following two paragraphs appear in all copies of this software.
+
+  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
+  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
+  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
+  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
+  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
+  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
+
+******************************************************************************/
+
+#include "debugInt.h"
+
+static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
+static int Commandtransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Initializes the test package.]
+
+  SideEffects []
+
+  SeeAlso     [Debug_End]
+
+******************************************************************************/
+void
+Debug_Init(void)
+{
+  /*
+   * Add a command to the global command table.  By using the leading
+   * underscore, the command will be listed under "help -a" but not "help".
+   */
+  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
+  Cmd_CommandAdd("transition",  Commandtransition,      0);
+
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Ends the test package.]
+
+  SideEffects []
+
+  SeeAlso     [Debug_Init]
+
+******************************************************************************/
+void
+Debug_End(void)
+{
+  /*
+   * For example, free any global memory (if any) which the test package is
+   * responsible for.
+   */
+}
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Implements the _Debug_test command.]
+
+  CommandName [_Debug_test]
+
+  CommandSynopsis [template for implementing commands]
+
+  CommandArguments [\[-h\] \[-v\]]
+  
+  CommandDescription [This command does nothing useful.  It merely serves as a
+  template for the implementation of new commands.<p>
+
+  Command options:<p>  
+
+  <dl>
+  <dt> -h
+  <dd> Print the command usage.
+  </dl>
+
+  <dt> -v
+  <dd> Verbose mode.
+  </dl>
+  ]
+
+  SideEffects []
+
+******************************************************************************/
+static int
+CommandDebug(
+  Hrc_Manager_t ** hmgr,
+  int  argc,
+  char ** argv)
+{
+  int            c;
+  int            verbose = 0;              /* default value */
+
+  /*
+   * Parse command line options.
+   */
+  util_getopt_reset();
+  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
+    switch(c) {
+      case 'v':
+        verbose = 1;
+        break;
+      case 'h':
+        goto usage;
+      default:
+        goto usage;
+    }
+  }
+
+  if (verbose) {
+    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
+  }
+
+  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
+  printf("** DEBUG MODE **\n");
+  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
+  printf("model : %s\n", Hrc_NodeReadModelName(n));
+
+  mdd_t * safe   = getSafe(fsm);
+  mdd_t * forbid = getForbidden(fsm);
+  mdd_t * reach  = getReach(fsm);
+  
+  if(safe == NIL(mdd_t))
+  {
+	printf("call command set_safe before\n");
+	return 1;
+  }
+  if(forbid == NIL(mdd_t))
+  {
+	printf("call command set_forbidden before\n");
+	return 1;
+  }
+
+  FILE*  oFile;
+  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
+ // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
+//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
+
+  mdd_t * EFState = mdd_and(reach,safe,1,1);
+//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
+
+  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
+  array_t *careStatesArray = array_alloc(mdd_t *, 0);
+  array_insert(mdd_t *, careStatesArray, 0,mddOne);
+
+  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
+		   EFState,
+           fsm->fairnessInfo.states,
+           careStatesArray,
+		   0,
+           McDcLevelNone_c);
+
+  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
+  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
+
+  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
+		   EXEFState,
+           fsm->fairnessInfo.states,
+           careStatesArray,
+		   0,
+           McDcLevelNone_c);
+  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
+  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
+  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
+  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
+  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
+		   andState,
+           fsm->fairnessInfo.states,
+           careStatesArray,
+		   0,
+           McDcLevelNone_c);
+  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
+  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
+  andState =  mdd_xor(EXEFState2,andState);
+  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
+  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
+		   andState,
+           fsm->fairnessInfo.states,
+           careStatesArray,
+		   0,
+           McDcLevelNone_c);
+  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
+  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
+  andState =  mdd_xor(EXEFState2,andState);
+  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
+
+
+
+  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
+  //mdd_GetState_Values(mddManager , EFState, stdout);
+  fclose(oFile);
+
+
+
+
+
+  return 0;		/* normal exit */
+
+  usage:
+  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
+  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
+  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
+  return 1;		/* error exit */
+}
+
+
+
+/**Function********************************************************************
+
+  Synopsis [Returns a BDD array from an Mvf array]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+static array_t *
+markGetBddArray(array_t *mvfArray,  mdd_manager* mddManager)
+{
+    int 	  i,phase;
+    array_t *bddArray;
+    Mvf_Function_t *mvf;
+
+    FILE*  oFile;
+  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
+
+    bddArray = array_alloc(bdd_node *,0);
+ printf("mvf array : %d \n" , array_n(mvfArray));
+
+    arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
+	mdd_t     *mddTemp;
+	bdd_node    *ddNode;
+
+	mddTemp = array_fetch(mdd_t *, mvf, 1);
+	ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
+	bdd_ref(ddNode);
+    mdd_FunctionPrintMain(mddManager, mddTemp, "TRANS", oFile);
+    printf("\n");
+  	ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
+    printf("%d --->",i);
+    bdd_print(mddTemp);
+    printf("\n");
+	array_insert_last(bdd_node *, bddArray, ddNode);
+    }
+    fclose(oFile);
+    return bddArray;
+}
+
+/**Function********************************************************************
+
+  Synopsis [Returns a BDD array given an integer array of variable indices.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+static bdd_node **
+BddNodeArrayFromIdArray(
+  bdd_manager	*ddManager,
+  array_t	*idArray)
+{
+    bdd_node **xvars;
+    int i,id;
+    int nvars = array_n(idArray);
+
+    xvars = ALLOC(bdd_node *, nvars);
+    if (xvars == NULL)
+	return NULL;
+
+    for(i = 0; i < nvars; i++) {
+	id = array_fetch(int,idArray,i);
+	xvars[i] = bdd_bdd_ith_var(ddManager,id);
+	bdd_ref(xvars[i]);
+    }
+    return xvars;
+}
+/**Function********************************************************************
+
+  Synopsis [Compute the relation between an array of function and a 
+  corresponding array of variables. A BDD is returned which represents
+  AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+static bdd_node *
+computeTransitionRelationWithIds(
+  bdd_manager	*ddManager,
+  array_t	*nextBdds,
+  bdd_node	**yVars,
+  int		nVars)
+{
+    bdd_node	*ddtemp1, *ddtemp2;
+    bdd_node	*oldTR, *fn;
+    int 		 i;
+
+
+    oldTR = bdd_read_one(ddManager);
+
+    for(i = 0; i < nVars; i++) {
+	ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
+
+    bdd_print(ddtemp2);
+	fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
+	bdd_ref(fn);
+	ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
+	bdd_ref(ddtemp1);
+	bdd_recursive_deref(ddManager,fn);
+	bdd_recursive_deref(ddManager,oldTR);
+	oldTR = ddtemp1;
+    }
+    return oldTR;
+}
+/*
+static mdd_t *
+computeTransitionRelationWithIds_mdd(
+  mdd_manager	*ddManager,
+  array_t	*nextBdds,
+  mdd_t	**yVars,
+  int		nVars)
+{
+    mdd_t	*ddtemp1, *ddtemp2;
+    mdd_t	*oldTR, *fn;
+    int 		 i;
+
+
+    oldTR = mdd_one(ddManager);
+
+    for(i = 0; i < nVars; i++) {
+	ddtemp2  = array_fetch(mdd_t *, nextBdds, i);
+
+	fn = mdd_xnor(ddtemp2,yVars[i],1,1);
+	ddtemp1 = mdd_and(oldTR,fn,1,1);
+	mdd_free(oldTR);
+	oldTR = ddtemp1;
+    }
+
+	mdd_ref(ddtemp1);
+	mdd_free(fn);
+    return oldTR;
+}
+*/
+
+static int 
+Commandtransition (Hrc_Manager_t ** hmgr,
+		   int  argc, char ** argv){
+  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
+  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
+  printf("** TRANSITION RELATION **\n");
+  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
+  printf("model : %s\n", Hrc_NodeReadModelName(n));
+
+   graph_t *partition;
+   bdd_node *tranRelation;
+   bdd_node **xVars,**yVars, **piVars;
+
+   
+   array_t *tranFunArray, *leaveIds;
+   array_t *nextBdds, *nextMvfs;
+   int nVars, nPi;
+
+   
+    /*
+     * tranFunArray is a list of next state funs.
+     */
+
+    tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
+    char *name;
+    int i;
+    arrayForEachItem(char*, tranFunArray, i, name){
+      Ntk_Node_t * latch = Ntk_NetworkFindNodeByName(network, name);
+      printf("%s : mddid : %d\n",name , Ntk_NodeReadMddId(latch) );
+      //int c =   Ntk_NodeReadMddId(latch);
+    }
+
+ array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
+  int                  arrSize = array_n( psVarsArray );
+
+  for ( i = 0 ; i < arrSize ; ++i ) {
+    int      mddId = array_fetch( int, psVarsArray, i );
+    mvar_type mVar = array_fetch(mvar_type, 
+				 mdd_ret_mvar_list(mddManager),mddId);
+    printf("%s : mddid %d\n", mVar.name, mddId);
+  }
+
+ array_t *nsVarsArray  =  Fsm_FsmReadNextStateVars(fsm);
+arrSize = array_n( nsVarsArray );
+
+  for ( i = 0 ; i < arrSize ; ++i ) {
+    int      mddId = array_fetch( int, nsVarsArray, i );
+    mvar_type mVar = array_fetch(mvar_type, 
+				 mdd_ret_mvar_list(mddManager),mddId);
+    printf("%s : mddid %d\n", mVar.name, mddId);
+  }
+
+
+    leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
+			  Fsm_FsmReadPresentStateVars(fsm));
+    /*
+     * Get the BDDs for transition functions.Duplicate functions are returned.
+     */
+    partition = Fsm_FsmReadPartition(fsm);
+    nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
+					    NIL(mdd_t));
+
+    array_free(leaveIds);
+    array_free(tranFunArray);
+
+ Mvf_Function_t *mvf = array_fetch(Mvf_Function_t *,nextMvfs,1);
+ mdd_t * recupdd = array_fetch(mdd_t *, mvf, 0);
+ printf("plop\n");
+ bdd_print(recupdd);
+/** Build cex **/
+
+/** state0 **/
+ mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
+ printf("****************\n");
+ bdd_print (s0);
+ mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
+ printf("****************\n");
+ bdd_print (s1);
+ mdd_t * and =  mdd_one(mddManager);
+ and = mdd_and(s0,s1,1,1);
+ mdd_t* reach = mdd_one(mddManager);
+ reach = Fsm_FsmReadReachableStates(fsm);
+ mdd_t * state0 =  mdd_and(and,reach,1,1);
+/** next state1 **/
+ mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
+ mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
+ mdd_t * state1 = mdd_and(ns0,ns1,1,1);
+/** new rel **/
+ mdd_t * rel =  mdd_or(state0,state1,0,0);
+
+
+
+
+// Get image_info 
+
+  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
+
+   Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
+
+array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
+ arrayForEachItem(mdd_t *, transRelation, i, recupdd){
+ printf("****************\n");
+
+    bdd_print(recupdd);
+}
+  mdd_t* new_rel = mdd_and(recupdd,rel,1,1);
+FILE * oFile = fopen("relation.bdd","w");
+ mdd_FunctionPrintMain(mddManager, recupdd, "TRANS", oFile);
+ mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
+ mdd_FunctionPrintMain(mddManager, rel, "REL", oFile);
+ mdd_FunctionPrintMain(mddManager, new_rel, "new_rel", oFile);
+
+fclose(oFile);
+array_insert(mdd_t*,transRelation,0,new_rel);
+Img_ReplacePartitionedTransitionRelation(imageInfo, transRelation,0);
+ printf("****************\n");
+
+Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
+
+ arrayForEachItem(mdd_t *, transRelation, i, recupdd){
+ printf("****************\n");
+ FsmResetReachabilityFields(fsm, 0);
+
+    bdd_print(recupdd);
+}
+
+/*
+FILE * dotFile = fopen("relation.dot","w");
+
+mdd_dump_dot(reach,NIL(char),dotFile);
+fclose(dotFile);
+*/
+//    nextBdds = markGetBddArray(nextMvfs,mddManager);
+
+    Mvf_FunctionArrayFree(nextMvfs);
+/*
+ // Get the DdNodes for all the variables.
+
+    piVars = BddNodeArrayFromIdArray(mddManager, 
+					 Fsm_FsmReadInputVars(fsm));
+    xVars = BddNodeArrayFromIdArray(mddManager, 
+					Fsm_FsmReadPresentStateVars(fsm));
+    yVars = BddNodeArrayFromIdArray(mddManager,
+					Fsm_FsmReadNextStateVars(fsm));
+
+    nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
+    nPi = array_n(Fsm_FsmReadInputVars(fsm));
+
+    // Compute the transition relation 
+    tranRelation = computeTransitionRelationWithIds(mddManager, nextBdds,
+						    yVars, nVars);
+ */
+/*
+ FILE*  oFile;
+  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
+mdd_FunctionPrintMain(mddManager, tranRelation, "TRANS", oFile);
+ fclose(oFile);
+ */
+  return 0;
+}
+
+
Index: /vis_dev/vis-2.3/src/debug/debug.h
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.h	(revision 27)
+++ /vis_dev/vis-2.3/src/debug/debug.h	(revision 27)
@@ -0,0 +1,92 @@
+/**CHeaderFile*****************************************************************
+
+  FileName    [debug.h]
+
+  PackageName [debug]
+
+  Synopsis    [Test package illustrating VIS conventions.]
+
+  Description [This is a test package illustrating how to create a package in
+  VIS. It shows how to create commands, and illustrates naming conventions.]
+
+  Author      [Originated from SIS.]
+
+  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
+  All rights reserved.
+
+  Permission is hereby granted, without written agreement and without license
+  or royalty fees, to use, copy, modify, and distribute this software and its
+  documentation for any purpose, provided that the above copyright notice and
+  the following two paragraphs appear in all copies of this software.
+
+  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
+  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
+  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
+  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
+  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
+  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
+
+  Revision    [$Id: debug.h,v 1.2 2011/04/12 00:12:06 braun Exp $]
+
+******************************************************************************/
+
+#ifndef _DBG
+#define _DBG
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+#include "vm.h"
+#include "../ntk/ntkInt.h"
+#include "../hrc/hrcInt.h"
+#include "../fsm/fsmInt.h"
+#include "../bmc/bmcInt.h"
+#include "../sat/sat.h"
+#include "../sat/satInt.h"
+#include "../rob/Robust.h"
+#include "mdd.h"
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Function prototypes                                                       */
+/*---------------------------------------------------------------------------*/
+
+
+void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
+EXTERN void Debug_Init(void);
+EXTERN void Debug_End(void);
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* _DBG */
Index: /vis_dev/vis-2.3/src/debug/debug.make
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.make	(revision 27)
+++ /vis_dev/vis-2.3/src/debug/debug.make	(revision 27)
@@ -0,0 +1,4 @@
+CSRC += debug.c
+HEADERS += debug.h debugInt.h
+
+DEPENDENCYFILES = $(CSRC)
Index: /vis_dev/vis-2.3/src/debug/debugInt.h
===================================================================
--- /vis_dev/vis-2.3/src/debug/debugInt.h	(revision 27)
+++ /vis_dev/vis-2.3/src/debug/debugInt.h	(revision 27)
@@ -0,0 +1,81 @@
+/**CHeaderFile*****************************************************************
+
+  FileName    [debugInt.h]
+
+  PackageName [Debug]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Originated from SIS.]
+
+  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
+  All rights reserved.
+
+  Permission is hereby granted, without written agreement and without license
+  or royalty fees, to use, copy, modify, and distribute this software and its
+  documentation for any purpose, provided that the above copyright notice and
+  the following two paragraphs appear in all copies of this software.
+
+  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
+  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
+  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
+  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
+  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
+  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
+
+  Revision    [$Id: debugInt.h,v 1.2 2011/04/12 22:28:37 Braunstein Exp $]
+
+******************************************************************************/
+
+#ifndef _TSTINT
+#define _TSTINT
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+#include "debug.h"
+#include "cmd.h"
+#include <string.h>
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Function prototypes                                                       */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* _DBGINT */
+
+
Index: /vis_dev/vis-2.3/src/debug/debugUtilities.c
===================================================================
--- /vis_dev/vis-2.3/src/debug/debugUtilities.c	(revision 27)
+++ /vis_dev/vis-2.3/src/debug/debugUtilities.c	(revision 27)
@@ -0,0 +1,62 @@
+#include "Debug.h"
+
+void mdd_GetState_Values(
+mdd_manager *mgr ,
+mdd_t *  top, 
+FILE  * f) 
+{
+  mdd_t * T;
+  mdd_t * E;
+  int    id;
+  array_t * val = array_alloc(int, 4); 
+  static int level;
+  char c = ' ' ;
+
+  level++;
+
+  id = bdd_top_var_id(top);
+
+  mvar_type mv =  
+array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id));
+ // fprintf(f,"(");
+
+  // Pour le Then
+  T=bdd_then(top);
+ 
+ //variable belongs to what we are looking for
+// if(strstr(mv.name,var_name) !=NULL)
+  if(bdd_is_tautology(T,1)){
+    //array_insert(type, array, position, object)
+    fprintf(f,"%s = 1 ",mv.name);
+    //c = '+';
+  } else
+    if(!bdd_is_tautology(T,0)){
+      fprintf(f,"%s = 1 * ",mv.name);
+      //mdd_FunctionPrint(mgr, T,f);
+     // c = '+';
+    }
+
+  mdd_free(T);
+  
+  //pour le Else
+  E=bdd_else(top);
+  if(bdd_is_tautology(E,0)){
+    goto fin;
+  }
+  
+  if(bdd_is_tautology(E,1)){
+    fprintf(f,"%c %s = 0",c, mv.name);
+    goto fin;
+  }
+  
+  fprintf(f,"%c %s = 0 * ",c, mv.name);
+  /*
+  mdd_FunctionPrint(mgr, E,f);
+  mdd_free(E);
+*/
+ fin:
+  fprintf(f,")");
+  level--;
+  return;
+}
+
Index: /vis_dev/vis-2.3/src/vm/vmInit.c
===================================================================
--- /vis_dev/vis-2.3/src/vm/vmInit.c	(revision 26)
+++ /vis_dev/vis-2.3/src/vm/vmInit.c	(revision 27)
@@ -72,4 +72,5 @@
   Cmd_Init();
   Tst_Init();
+  Debug_Init();
   Tbl_Init();
   Io_Init();
@@ -143,4 +144,5 @@
   Res_End();
   Tst_End();
+  Debug_End();
   Cmd_End();
   Abs_End();
Index: /vis_dev/vis-2.3/src/vm/vmInt.h
===================================================================
--- /vis_dev/vis-2.3/src/vm/vmInt.h	(revision 26)
+++ /vis_dev/vis-2.3/src/vm/vmInt.h	(revision 27)
@@ -67,4 +67,5 @@
 #include "grab.h"
 #include "puresat.h"
+#include "debug.h"
 
 #if STDC_HEADERS