--- a/src/lite/ITLCommander.java	Thu Jan 17 11:09:19 2008 +0900
+++ b/src/lite/ITLCommander.java	Thu Jan 17 13:55:08 2008 +0900
@@ -55,11 +55,11 @@
 			return (Node)n;
 		} else if (name == "ex"|| name=="do") {
 			checkSat();
-			if (args.size()<1) {
+			Node n = args.get(0);
+			if (args.size()<1||n==null) {
 				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
 				return lf.trueNode();
 			}
-			Node n = args.get(0);
 			int index = -1;
 			if (n.getClass()==NumberSolver.class) {
 				index = Integer.parseInt(n.toString()); 

--- a/src/sbdd/BDDDiagnosis.java	Thu Jan 17 11:09:19 2008 +0900
+++ b/src/sbdd/BDDDiagnosis.java	Thu Jan 17 13:55:08 2008 +0900
@@ -24,6 +24,8 @@
 	public boolean falsifiable;
 	public boolean satisfiable;
 	public TreeSet<SBDDEntry> reachable;
+	public TreeSet<SBDDEntry> trueSet;
+	public TreeSet<SBDDEntry> falseSet;
 	private SBDDEntry last;
 
 	public BDDDiagnosis(BDDSatisfier sat) {
@@ -60,6 +62,7 @@
 	 * memory. 
 	 */
 	private void show(LinkedList<SBDDEntry> trace) {
+		if (trace.isEmpty()) return; 
 		SBDDEntry last = trace.getLast();
 		int i = 0;
 		for(SBDDEntry e: trace) {
@@ -76,22 +79,37 @@
 	private LinkedList<SBDDEntry> findTrueEntry(SBDDEntry e, int length) {
 		SBDDEntry dest = true_;
 		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		makeReachableEntry(e);
+		if (specialCase()) return trace;
+		dest = trueSet.first();
 		return findMore(e,dest,length,trace);
 	}
-	
+
 	private LinkedList<SBDDEntry> findFalseEntry(SBDDEntry e, int length) {
 		SBDDEntry dest = false_;
 		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		makeReachableEntry(e);
+		if (specialCase()) return trace;
+		dest = falseSet.first();
 		return findMore(e,dest,length,trace);
 	}
 
+	private boolean specialCase() {
+		if (falseSet.isEmpty()) {
+			System.out.println("valid."); return true;
+		}
+		if (trueSet.isEmpty()) {
+			System.out.println("unsatisfiable."); return true;
+		}
+		return false;
+	}
+	
 	/*
 	 * find trace from an start entry to a destination. Reachable set have to
 	 * be generated from the start entry.
 	 */
 	public LinkedList<SBDDEntry> findEntry(SBDDEntry e, SBDDEntry dest, int length, LinkedList<SBDDEntry> trace) {
 		SBDDEntry small = dest;
-		makeReachableEntry(e);
 		if (reachable.contains(dest)) {
 			while(firstPrevious(small)!=e) {
 				trace.addFirst(small);
@@ -107,7 +125,6 @@
 	 */
 	public LinkedList<SBDDEntry> findMore(SBDDEntry e, SBDDEntry dest, int length, LinkedList<SBDDEntry> trace) {
 		SBDDEntry small = dest;
-		makeReachableEntry(e);
 		if (reachable.contains(dest)) {
 			try {
 				findTrace(trace,e,small,length);
@@ -119,37 +136,45 @@
 		// not found
 		return trace;
 	}
-	
+
+	class sbddComparator implements Comparator<SBDDEntry>  {
+		public int compare(SBDDEntry arg0, SBDDEntry arg1) {
+			return arg1.id-arg0.id;
+		}
+	}
 
 	public void makeReachableEntry(SBDDEntry e) {
 		if (last==e) return; else last = e;
-		reachable = new TreeSet<SBDDEntry>(
-				new Comparator<SBDDEntry>() {
-					public int compare(SBDDEntry arg0, SBDDEntry arg1) {
-						return arg1.id-arg0.id;
-					}
-				});
+		reachable = new TreeSet<SBDDEntry>(new sbddComparator());
+		trueSet   = new TreeSet<SBDDEntry>(new sbddComparator());
+		falseSet  = new TreeSet<SBDDEntry>(new sbddComparator());
 		if (e==null) return;
-		LinkedList<Iterable<SBDDEntry>> stack = new LinkedList<Iterable<SBDDEntry>>();
+		//LinkedList<Iterable<SBDDEntry>> stack = new LinkedList<Iterable<SBDDEntry>>();
 		Iterable<SBDDEntry> current = e.nexts(); 
-		stack.add(current);
+		//stack.add(current);
 		falsifiable = false;
 		satisfiable = false;
-		while(!stack.isEmpty()) {
-			for(SBDDEntry s: current) {
-				if (reachable.add(s)) {
-					// this is a new one
-					stack.add(current);
-					current = s.nexts();
-					falsifiable|=s.falsifiable;
-					satisfiable|=s.satisfiable;
-				}
+		if(e.falsifiable) falseSet.add(e); 
+		if(e.satisfiable) trueSet.add(e);
+		addReachable(current);
+	}
+
+
+	/*
+	 * Put new set of next states in reachable state set. SBDDEntry.nexts does not
+	 * contains true/false.
+	 */
+	private void addReachable(Iterable<SBDDEntry> current) {
+		for(SBDDEntry s: current) {
+			if (reachable.add(s)) {
+				// this is a new one
+				falsifiable|=s.falsifiable; if(s.falsifiable) falseSet.add(s); 
+				satisfiable|=s.satisfiable; if(s.satisfiable) trueSet.add(s);
+				addReachable(s.nexts());
 			}
-			// this branch is completed. search another.
-			current = stack.getLast();
 		}
 	}
-	
+
 	public SBDDEntry firstPrevious(SBDDEntry e) {
 		// we assume reachable is sorted in generated order
 		// it returns always younger entry
@@ -166,12 +191,12 @@
 	}
 
 	private void findTrace(LinkedList<SBDDEntry> trace, SBDDEntry start,SBDDEntry e, int length) throws Result {
-		if (length<0) return;
+		// if (length<0) return;
 		trace.addFirst(e);
 		for(SBDDEntry p: reachable) {
 			if (p.nexts.contains(e)) {
 				if (p==start)
-					if (length==0) throw new Result();
+					if (length<=0) throw new Result();
 				findTrace(trace,start,p,length-1);
 			}
 		}