--- a/src/lite/ITLCommander.java	Fri Jan 18 17:31:49 2008 +0900
+++ b/src/lite/ITLCommander.java	Fri Jan 18 20:52:45 2008 +0900
@@ -7,6 +7,7 @@
 
 import sbdd.BDDDiagnosis;
 import sbdd.BDDSatisfier;
+import sbdd.SBDDEntry;
 
 public class ITLCommander<Node extends ITLSolver> implements Command<Node> {
 
@@ -53,25 +54,22 @@
 		
 		if (name=="less") {
 			Node n = lf.falseNode();
-			int length = Integer.parseInt(args.get(0).toString());
+			int length = atoi(args);
 			for(int i =0;i<length;i++) {
 				n = lf.nextNode(n);
 			}
 			return (Node)n;
 		} else if (name == "ex"|| name=="do") {
 			checkSat();
-			Node n = args.get(0);
-			if (args.size()<1||n==null) {
+			if (args.size()<1) {
 				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
 				return lf.trueNode();
 			}
-			int index = -1;
-			if (n.getClass()==NumberSolver.class) {
-				index = Integer.parseInt(n.toString()); 
-			}
+			int index = atoi(args);
 			if (args.size()==1) {
-				// System.out.println(args.get(0)+":"+args.get(1));
+				Node n = args.get(0);
 				if (index>=0) {
+					// do(10) case
 					n = examples.get(index);
 					if (n==null) {
 						parser.error("Unknown registered example");
@@ -95,31 +93,31 @@
 			parser.define(args.get(0).toString(),args.get(1).toString());
 		} else if (name == "verbose") {
 			// verbose(true) / verbose(off)
-			Node n= null;
 			checkSat();
-			try {
-				int i = Integer.parseInt((n=args.get(0)).toString());
-				sat.verbose =  (i==0)? false:true;
-			} catch (NumberFormatException e) {
-				sat.verbose = (n==lf.trueNode())?true:false;
-			}
+			Node n;
+			if (args.size()==0 || (n=args.get(0))==null) n = lf.trueNode();
+			sat.verbose = (n==lf.trueNode())?true:false;
 		} else if (name == "include") {
 			String file = args.getFirst().toString();
 			parser.parseFile(file);
 		} else if (name == "exe") {
 			int length = 0;
-			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
+			if (args.size()>1) length = atoi(args);
 			checkSat();
 			diag.execute(sat.last, length );
 		} else if (name == "diag") {
 			int length = 0;
-			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
+			if (args.size()>1) length = atoi(args);
 			checkSat();
 			diag.counterExample(sat.last, length);
 		} else if (name == "clear") {
 			sat = new BDDSatisfier();
 		} else if (name == "states") {
-			System.out.println(sat.sf.hash);
+			// System.out.println(sat.sf.hash); too large
+			for(SBDDEntry e: sat.sf.hash.sbddArray) {
+				if (e==null) continue;
+				System.out.println(e);
+			}
 		} else if (name == "show") {
 			checkSat();
 			diag.showState(sat.last);
@@ -128,6 +126,18 @@
 		return lf.trueNode();
 	}
 
+	private int atoi(LinkedList<Node> args) {
+		// should have more strcit check..
+		int i=0;
+		if (args.size()==0) return i;
+		Node n = args.get(0);
+		if (n==null) return 0;
+		if (n.getClass()==NumberSolver.class) {
+			i = Integer.parseInt(n.toString()); 
+		}
+		return i;
+	}
+
 	private void checkSat() {
 		if (sat==null) {
 			sat = new BDDSatisfier();