Index: /vis_dev/dev/Makefile
===================================================================
--- /vis_dev/dev/Makefile	(revision 15)
+++ /vis_dev/dev/Makefile	(revision 15)
@@ -0,0 +1,12 @@
+LIBGLUDIR=../glu-2.3/
+LIBVISDIR=../vis-2.3/
+INCVISDIR=${LIBVISDIR}/include/
+INCGLUDIR=${LIBGLUDIR}/include/
+
+a.out : main.c utilities.o 
+	gcc main.c -lm -L$(LIBGLUDIR) -lglu -L$(LIBVISDIR) -lvis2  -I$(INCVISDIR) -I$(INCGLUDIR)
+
+utilities.o : utilities.c
+	gcc -c utilities.c -lm -L$(LIBGLUDIR) -lglu -L$(LIBVISDIR) -lvis2  -I$(INCVISDIR) -I$(INCGLUDIR)
+clean:
+	rm *.o a.out
Index: /vis_dev/dev/main.c
===================================================================
--- /vis_dev/dev/main.c	(revision 15)
+++ /vis_dev/dev/main.c	(revision 15)
@@ -0,0 +1,9 @@
+#include "stdio.h"
+#include "hrc.h"
+#include "ntk.h"
+
+int main()
+{
+Hrc_Manager_t * hmge;
+  return 0;
+}
Index: /vis_dev/dev/utilities.c
===================================================================
--- /vis_dev/dev/utilities.c	(revision 15)
+++ /vis_dev/dev/utilities.c	(revision 15)
@@ -0,0 +1,454 @@
+#include "utilities.h"
+/*---------------------------------------------------------------------------*/
+/* Read_blif_mv                                                              */
+/*---------------------------------------------------------------------------*/
+Hrc_Manager_t * rlmv(FILE * file)
+{
+		return  Io_BlifMvRead( file, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
+
+}
+/*---------------------------------------------------------------------------*/
+/* flatten_hierarchy                                                         */
+/*---------------------------------------------------------------------------*/
+Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr)
+{
+	assert(hmgr != NULL);
+	int            sweep       = 1;
+	int            verbose     = 0;
+	lsList         varNameList = (lsList) NULL;
+	Ntk_Network_t *ntk;
+	// flatten
+	Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgr);
+	ntk = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
+
+	Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
+                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
+                      (Hrc_ApplInfoChangeFn) NULL,  // not currently used by hrc 
+                      (void *) ntk);
+	Ntk_NetworkSweep(ntk, verbose);
+	return ntk;
+
+}
+/*---------------------------------------------------------------------------*/
+/* Build_partition_maigs                                                     */
+/*---------------------------------------------------------------------------*/
+
+st_table * build_partition_maigs(Ntk_Network_t * ntk)
+{
+	Ntk_Node_t    *node, *latch;
+    lsGen          gen;
+	int i;
+	array_t       *result;
+	array_t		  *inputs;
+	array_t       *roots;
+	st_table      *leaves;
+	st_table      *nodeToMvfAigTable;  /* mapes each node with its mvfAig */
+	MvfAig_Function_t  *mvfAig;
+	mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(ntk);
+	if (manager == NIL(mAig_Manager_t)) {
+		manager = mAig_initAig();
+		Ntk_NetworkSetMAigManager(ntk, manager);
+	}
+	  roots = array_alloc(Ntk_Node_t *, 0);
+  Ntk_NetworkForEachCombOutput(ntk, gen, node) {
+    array_insert_last(Ntk_Node_t *, roots, node);
+  }
+  Ntk_NetworkForEachNode(ntk, gen, node) {
+    if(Ntk_NodeTestIsShadow(node))	continue;
+    if(Ntk_NodeTestIsCombInput(node))	continue;
+    if(Ntk_NodeTestIsCombOutput(node))continue;
+
+    if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) {
+	/**
+      fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node));
+      **/
+      array_insert_last(Ntk_Node_t *, roots, node);
+    }
+  }
+
+  leaves = st_init_table(st_ptrcmp, st_ptrhash);
+
+  inputs = array_alloc(Ntk_Node_t *, 16);
+  Ntk_NetworkForEachCombInput(ntk, gen, node) {
+    array_insert_last(Ntk_Node_t *, inputs, node);
+  }
+  array_sort(inputs, nodenameCompare);
+  for(i=0; i<array_n(inputs); i++) {
+    node = array_fetch(Ntk_Node_t *, inputs, i);
+    st_insert(leaves,  node, (char *) ntmaig_UNUSED);
+    Ntk_NodeSetMAigId(node, 
+                       mAig_CreateVar(manager,
+		                      Ntk_NodeReadName(node),
+                                      Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
+  }
+  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);
+
+  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, 
+						  MVFAIG_NETWORK_APPL_KEY);
+  Ntk_NetworkForEachLatch(ntk, gen, latch) {
+		node  = Ntk_LatchReadDataInput(latch);
+		st_lookup(nodeToMvfAigTable, node,  &mvfAig);
+		Ntk_NodeSetMAigId(node, mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
+		node  = Ntk_LatchReadInitialInput(latch);
+		st_lookup(nodeToMvfAigTable, node,  &mvfAig);
+		Ntk_NodeSetMAigId(node,   mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
+	}
+
+	roots->num = 0;
+	Ntk_NetworkForEachLatch(ntk, gen, latch) {
+		if(!st_lookup(nodeToMvfAigTable, latch,  &mvfAig))
+			array_insert_last(Ntk_Node_t *, roots, latch);
+		}
+  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);
+  array_free(roots);
+  array_free(inputs);
+  st_free_table(leaves);
+  MvfAig_FunctionArrayFree(result);
+  return nodeToMvfAigTable;
+}
+/*---------------------------------------------------------------------------*/
+/* Create unroll circuit k steps                                             */
+/*---------------------------------------------------------------------------*/
+void printLatch(st_table* CoiTable)
+{
+// COI contents
+   printf("*** COI ***\n");
+   st_generator    *stGen;
+   Ntk_Node_t * latch;
+   st_foreach_item(CoiTable, stGen, &latch, NULL) {
+	printf("%s\n",Ntk_NodeReadName(latch)); 
+  }
+}
+
+st_table * generateAllLatches(Ntk_Network_t * ntk)
+{
+    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
+	lsGen           gen ;
+	Ntk_Node_t		*node;
+
+	Ntk_NetworkForEachNode(ntk,gen, node){
+		if (Ntk_NodeTestIsLatch(node)){
+			st_insert(CoiTable, (char *) node, (char *) 0);
+		}
+	}
+	return CoiTable;
+
+}
+void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses)
+{
+    st_table        *CoiTable =  generateAllLatches(ntk);
+	lsGen           gen ;
+	Ntk_Node_t		*node;
+
+
+	
+	Ntk_NetworkForEachNode(ntk,gen, node){
+		if (Ntk_NodeTestIsLatch(node)){
+			st_insert(CoiTable, (char *) node, (char *) 0);
+		}
+	}
+
+	 options->verbosityLevel = BmcVerbosityMax_c;
+	 options->satSolver = CirCUs;
+	 options->timeOutPeriod = 0;
+	 options->printInputs = TRUE;
+	 options->minK = bound;
+	 options->maxK = bound;
+	 options->step = bound;
+	 options->dbgLevel = 1;
+
+     //nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph 
+     st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, MVFAIG_NETWORK_APPL_KEY);
+     assert(nodeToMvfAigTable != NIL(st_table));
+
+     // Create clauses database 
+	 int initState = BMC_INITIAL_STATES;
+	 BmcCnfGenerateClausesForPath(ntk, 0, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);
+
+}
+
+void printSATAssig( array_t* result)
+{
+	int k;
+	printf("RESULT : \n");
+	for(k=0; k< array_n(result); k++){
+		printf("%d\n",array_fetch(int, result, k));
+	}
+}
+void printNodeToMvFaigTable(st_table* nodeToMvfAigTable)
+{
+	// nodeToMvFaigTable contents
+	st_generator    *stGen;
+	Ntk_Node_t * latch;
+	printf("*** NODETOMV ***\n");
+	st_foreach_item(nodeToMvfAigTable, stGen, &latch, NULL) {
+		printf("%s , %d\n",Ntk_NodeReadName(latch),Ntk_NodeReadMAigId(latch)); 
+   	}
+	printf("***************\n");
+}
+void printCNFIndex(BmcCnfClauses_t* cnfClauses)
+{
+	// Cnf index Table content
+	st_generator    *stGen;
+	nameType_t      *nodeName;
+	int index,i,k;
+	printf("*** cnfIndextable ***\n");
+	st_foreach_item(cnfClauses->cnfIndexTable, stGen,&nodeName,&index){
+		printf("(%s,%d)\n",nodeName, index);
+	}
+}
+void printCNFClauses(BmcCnfClauses_t* cnfClauses)
+{
+	int i,k;
+	printf("*** clause table ***\n");
+	for (i = 0; i < cnfClauses->nextIndex; i++) {
+		k = array_fetch(int, cnfClauses->clauseArray, i);
+		printf("%d%c", k, (k == 0) ? '\n' : ' ');
+    }
+}
+void
+printClauseLits(satManager_t *cm,long concl,FILE * file)
+{
+  long i, node, var_idx,*lit;
+
+  for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
+    node = SATgetNode(*lit);
+    var_idx = SATnodeID(node);
+    if(SATisInverted(node))
+      fprintf(file,"%ld ", -var_idx);
+    else
+      fprintf(file,"%ld ",var_idx);
+  }
+  fprintf(file,"0\n");
+}
+
+int getClsIndex(long concl,int numVarInCnf)
+{
+	int clsIndex;
+	clsIndex = concl -  numVarInCnf * satNodeSize;
+    clsIndex = (clsIndex/satNodeSize)-1;
+	return clsIndex;
+
+}
+
+void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore)
+{
+	int i,v,clsIndex;
+     for(i=0; i<clauseIndexInCore->num; i++) {
+	 	v = clauseIndexInCore->space[i];
+	 	clsIndex = getClsIndex(v,cm->initNumVariables);
+		printf("\nclause idx = %d\n",clsIndex);
+		printClauseLits(cm,v,vis_stdout);
+	 }		
+}
+void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename)
+{
+	FILE * file = fopen(filename,"w");
+	fprintf(file,"p cnf %d %d\n",clauseIndexInCore->num,cm->initNumVariables);
+	int i,v,clsIndex;
+     for(i=0; i<clauseIndexInCore->num; i++) {
+	 	v = clauseIndexInCore->space[i];
+	 	clsIndex = getClsIndex(v,cm->initNumVariables);
+		//printf("\nclause idx = %d\n",clsIndex);
+		printClauseLits(cm,v,file);
+	 }		
+	 fclose(file);
+}
+
+array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,	satArray_t *clauseIndexInCore)
+{
+
+  satOption_t  *satOption;
+  array_t      *result = NIL(array_t);
+  int          maxSize;
+
+  satOption = sat_InitOption();
+  satOption->verbose = options->verbosityLevel;
+  //satOption->unsatCoreFileName = "Ucore.txt";
+  satOption->clauseDeletionHeuristic = 0;
+  satOption->coreGeneration = unsatcore;
+  satOption->minimizeConflictClause = 1;
+
+  cm->comment = ALLOC(char, 2);
+  cm->comment[0] = ' ';
+  cm->comment[1] = '\0';
+  cm->stdOut = stdout;
+  cm->stdErr = stderr;
+
+  cm->option = satOption;
+  cm->each = sat_InitStatistics();
+
+  cm->unitLits = sat_ArrayAlloc(16);
+  cm->pureLits = sat_ArrayAlloc(16);
+
+  maxSize = 10000 << (bAigNodeSize-4);
+  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
+  cm->maxNodesArraySize = maxSize;
+  cm->nodesArraySize = bAigNodeSize;
+
+  sat_AllocLiteralsDB(cm);
+	
+  sat_ReadCNF(cm, options->satInFile);
+  sat_Main(cm);
+   if(cm->status == SAT_UNSAT) {
+    if (options->verbosityLevel != BmcVerbosityNone_c){
+      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
+	  }
+	  if(unsatcore)
+	  {
+		clauseIndexInCore =  cm->clauseIndexInCore;
+	  }
+    fflush(cm->stdOut);
+
+	}else if(cm->status == SAT_SAT) {
+    if (options->verbosityLevel != BmcVerbosityNone_c){
+      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
+    }
+    fflush(cm->stdOut);
+    result = array_alloc(int, 0);
+    {
+      int i, size, value;
+      
+      size = cm->initNumVariables * bAigNodeSize;
+      for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
+		value = SATvalue(i);
+		if(value == 1) {
+			array_insert_last(int, result, SATnodeID(i));
+		}
+		else if(value == 0) {
+			array_insert_last(int, result, -(SATnodeID(i)));
+		}
+      }
+    }
+  }
+  return result;
+
+}
+int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName)
+{	
+	int index;
+	st_lookup(cnfClauses->cnfIndexTable,nodeName,&index);
+	return index;
+
+}
+
+mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val,
+mdd_manager * mddManager)
+{
+	array_t * mvar_val= array_alloc(int,0);
+	array_t * mvar_name= array_alloc(char*,0);
+	array_t * mvar_strides= NIL(array_t);
+
+    if(array_n(stateName) == 1)
+	{
+		array_insert_last(int, mvar_val,max);
+		array_insert_last(char*, mvar_name,array_fetch(char*, stateName,0));
+	}
+	else
+	{
+		int i;
+		for( i = 0;i<max;i++)  array_insert_last(int, mvar_val,1);
+		mvar_name = array_dup(stateName);
+
+		printf(" Num of var , %d %d \n",array_n(stateName),array_n(mvar_val));
+		
+	}
+	
+	mdd_create_variables(mddManager, mvar_val,mvar_name, mvar_strides);
+
+	array_t *mvar_list = mdd_ret_mvar_list(mddManager);
+	array_t *bvar_list = mdd_ret_bvar_list(mddManager);
+
+	bvar_type bv = array_fetch(bvar_type, bvar_list, 0);
+
+	mvar_type mv;
+	bdd_node* f,*f2, * left, *right;
+	int i,v, value,mask;
+
+	f =  bdd_read_one(mddManager);
+	bdd_ref(f);
+	mv = array_fetch(mvar_type, mvar_list, 0);
+	printf("mvar name: %s;%d\n", mv.name,array_n(bvar_list)); 
+//	for(v=0;v<array_n(val); v++)
+//	{	
+		value = array_fetch(int,val,0);
+		mask = 1;
+		for(i= array_n(bvar_list)-1;i>=0; i--)
+		{
+		  printf("---->value %d , %d, %d \n",value,(value & mask),i);
+			left =  bdd_bdd_ith_var(mddManager,i);
+			if((value&mask) > 0)
+				right =  bdd_bdd_and(mddManager,left,f);
+			else
+				right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f);
+			bdd_ref(right);
+			bdd_recursive_deref(mddManager,f);
+			f = right;
+			mask = mask *2;
+		}
+
+	for(v=1;v<array_n(val); v++)
+	{	
+		value = array_fetch(int,val,v);
+		mask = 1;
+		printf("----val_value : %d\n",value);
+		f2 =  bdd_read_one(mddManager);
+		bdd_ref(f2);
+
+		for(i= array_n(bvar_list)-1;i>=0; i--)
+		{
+		  printf("---->value %d , %d, %d \n",value,(value & mask),i);
+			left =  bdd_bdd_ith_var(mddManager,i);
+			if((value&mask) > 0)
+				right =  bdd_bdd_and(mddManager,left,f2);
+			else
+				right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f2);
+			bdd_ref(right);
+			bdd_recursive_deref(mddManager,f2);
+			f2 = right;
+			mask = mask *2;
+		}
+		right =  bdd_bdd_or(mddManager,f2,f);
+		bdd_ref(right);
+		bdd_recursive_deref(mddManager,f2);
+		bdd_recursive_deref(mddManager,f);
+		f = right;
+	}
+		
+	mdd_t * mdd = bdd_construct_bdd_t(mddManager, f);
+	mdd_print_support(mdd); 
+	//FILE * file = fopen("bdd.dot","w");
+	//bdd_dump_dot(mddManager, 1, &f, NULL, NULL,file);
+
+	//fclose(file);
+	array_free(mvar_val);
+	array_free(mvar_name);
+
+	return mdd;
+	
+}
+
+
+void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses)
+{
+		
+	mdd_manager * mddManager = mdd_init_empty();
+	mdd_t * mdd =  buildBdd4StateVal(stateName, max,val,mddManager);
+	int index;
+	index = BmcGenerateCnfFormulaForBdd(mdd,steps, cnfClauses);
+	printf("number of clause : %d index %d \n", cnfClauses-> noOfClauses,index);
+
+	array_t * newClause;
+	newClause = array_alloc(int,1);
+	array_insert(int,newClause,0,index);
+	BmcCnfInsertClause(cnfClauses, newClause);
+
+
+
+
+	array_free(newClause);
+	mdd_quit(mddManager);
+
+	
+}
+
Index: /vis_dev/dev/utilities.h
===================================================================
--- /vis_dev/dev/utilities.h	(revision 15)
+++ /vis_dev/dev/utilities.h	(revision 15)
@@ -0,0 +1,75 @@
+#ifndef UTILITIES_H_
+#define UTILITIES_H_
+#include "ntk.h"
+#include "ord.h"
+#include "part.h"
+#include "maig.h"
+#include "ntmaig.h"
+#include "fsm.h"
+#include "ctlp.h"
+#include "ctlsp.h"
+#include "mcInt.h"
+#include "grabInt.h"
+#include "bmc.h"
+#include "bmcInt.h"
+#include "satInt.h"
+#include <stdio.h>
+#include <stdlib.h>
+
+
+static int
+nodenameCompare(
+  const void * node1,
+  const void * node2)
+{
+Ntk_Node_t *v1, *v2;
+char *name1, *name2;
+
+  v1 = *(Ntk_Node_t **)(node1);
+  v2 = *(Ntk_Node_t **)(node2);
+  name1 = Ntk_NodeReadName(v1);
+  name2 = Ntk_NodeReadName(v2);
+  
+  return (strcmp(name1, name2));
+} 
+
+// Read blifmv file 
+Hrc_Manager_t * rlmv(FILE * file);
+//flatten_hier
+// @ return the network
+Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr);
+// Build_partition_maigs  
+// @ return table node_ntk to aigTable
+st_table * build_partition_maigs(Ntk_Network_t * ntk);
+void printNodeToMvFaigTable(st_table* nodeToMvfAigTable);
+// print name of table containing Ntk_Node_t
+void printLatch(st_table* CoiTable);
+// generate all node of a network
+// @return a table with all node of a given network
+st_table * generateAllLatches(Ntk_Network_t * ntk);
+// Create unroll circuit k steps  
+// Build SAT instance
+//   Create clauses database 
+//	 BmcOption_t *options =  BmcOptionAlloc();
+//   BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
+//	 cnfClauses = BmcCnfClausesAlloc();
+void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses);
+void printSATAssig( array_t* result);
+void printCNFIndex(BmcCnfClauses_t* cnfClauses);
+void printCNFClauses(BmcCnfClauses_t* cnfClauses);
+void printClauseLits(satManager_t *cm,long concl,FILE * file);
+int getClsIndex(long concl,int numVarInCnf);
+void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore);
+void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename);
+// Check Sat
+// @return array_t empty if unsat
+// else print cex with : 
+// 	BmcPrintCounterExample(ntk1,nodeToMvfAigTable,cnfClauses,result,steps,CoiTable,options,	NIL(array_t));
+
+array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,	satArray_t *clauseIndexInCore);
+int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName);
+// Add val to state register
+mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val, mdd_manager * mddManager);
+void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses);
+
+#endif
Index: /vis_dev/glu-2.3/src/array/array.c
===================================================================
--- /vis_dev/glu-2.3/src/array/array.c	(revision 14)
+++ /vis_dev/glu-2.3/src/array/array.c	(revision 15)
@@ -65,4 +65,30 @@
     }
     (void) memcpy(newa->space, old->space, old->num * old->obj_size);
+    return newa;
+}
+
+array_t *
+array_partial_dup(array_t *old, int i)
+{
+    array_t *newa;
+
+    newa = ALLOC(array_t, 1);
+    if (newa == NIL(array_t)) {
+	return NIL(array_t);
+    }
+    newa->num = old->num - 1;
+    newa->n_size = old->num - 1;
+    newa->obj_size = old->obj_size;
+    newa->index = -newa->obj_size;
+    newa->space = ALLOC(char, newa->n_size * newa->obj_size);
+    if (newa->space == NIL(char)) {
+	FREE(newa);
+	return NIL(array_t);
+    }
+    if (i > 0)
+      (void) memcpy(newa->space, old->space, i * old->obj_size);
+    if (i < old->num - 1)
+      (void) memcpy(newa->space + ((i) * old->obj_size), 
+		    old->space + ((i+1) * old->obj_size), (old->num - (i + 1)) * old->obj_size);
     return newa;
 }
Index: /vis_dev/glu-2.3/src/array/array.h
===================================================================
--- /vis_dev/glu-2.3/src/array/array.h	(revision 14)
+++ /vis_dev/glu-2.3/src/array/array.h	(revision 15)
@@ -34,4 +34,5 @@
 EXTERN int array_resize ARGS((array_t *, int));
 EXTERN char *array_do_data ARGS((array_t *));
+EXTERN array_t * array_partial_dup(array_t *old, int i);
 
 extern int unsigned array_global_index;
Index: /vis_dev/vis-2.3/Makefile.in
===================================================================
--- /vis_dev/vis-2.3/Makefile.in	(revision 14)
+++ /vis_dev/vis-2.3/Makefile.in	(revision 15)
@@ -94,5 +94,5 @@
 #----------------------------------------------------------------------
 
-ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm grab hrc imc img io ltl \
+ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm rob grab hrc imc img io ltl \
 	maig mark mc mvf mvfaig ntk ntm ntmaig ord part puresat rst res restr \
 	rt sat sim spfd synth tbl truesim tst var vm
Index: /vis_dev/vis-2.3/src/bmc/bmcCmd.c
===================================================================
--- /vis_dev/vis-2.3/src/bmc/bmcCmd.c	(revision 14)
+++ /vis_dev/vis-2.3/src/bmc/bmcCmd.c	(revision 15)
@@ -46,5 +46,5 @@
 /*---------------------------------------------------------------------------*/
 
-static BmcOption_t * ParseBmcOptions(int argc, char **argv);
+/*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv);
 static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
 static void TimeOutHandle(void);
@@ -104,5 +104,5 @@
 
 ******************************************************************************/
-static BmcOption_t *
+/*static*/ BmcOption_t *
 ParseBmcOptions(
   int argc,
Index: /vis_dev/vis-2.3/src/fsm/fsmInt.h
===================================================================
--- /vis_dev/vis-2.3/src/fsm/fsmInt.h	(revision 14)
+++ /vis_dev/vis-2.3/src/fsm/fsmInt.h	(revision 15)
@@ -180,4 +180,13 @@
     boolean createVarCubesFlag;
   } fsmData;
+
+    // For robustness computation
+  struct {
+    mdd_t * originalreachableStates;
+    mdd_t * Safe; FILE* fSafe;
+    mdd_t * Forb; FILE* fForb;
+    mdd_t * Req;  FILE* fReq;
+  } RobSets;
+
 };
 
Index: /vis_dev/vis-2.3/src/fsm/fsmReach.c
===================================================================
--- /vis_dev/vis-2.3/src/fsm/fsmReach.c	(revision 14)
+++ /vis_dev/vis-2.3/src/fsm/fsmReach.c	(revision 15)
@@ -65,5 +65,5 @@
 
 static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
-static int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
+/*static*/ int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
 static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
 static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo);
@@ -1162,5 +1162,5 @@
 
 ******************************************************************************/
-static int
+/*static*/ int
 ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager,
 			       array_t *mddIdArray)
Index: /vis_dev/vis-2.3/src/vm/vmInit.c
===================================================================
--- /vis_dev/vis-2.3/src/vm/vmInit.c	(revision 14)
+++ /vis_dev/vis-2.3/src/vm/vmInit.c	(revision 15)
@@ -105,4 +105,5 @@
   Bmc_Init();
   PureSat_Init();
+  Rob_Init();
 }
 
@@ -154,5 +155,5 @@
   ntmaig_End();
   Bmc_End();
-
+  Rob_End();
   if (vis_stdout != stdout) {  
     (void) fclose(vis_stdout);