--- a/src/lite/EmptySolver.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/EmptySolver.java	Wed Jan 16 14:34:11 2008 +0900
@@ -14,18 +14,18 @@
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		// return sat.empty.sat(sat, next);
-		if (sat.hasChoicePoint(this))
+		if (sat.cp.hasChoicePoint(this))
 			return next.sat(value?sat.true_:null);
 		value = true;
 		try {
-			sat.addChoicePoint(this);
+			sat.cp.addChoicePoint(this);
 			return next.sat(sat.true_);
 		} catch (Backtrack e) {
 			value = false;
 			try {
 				return next.sat(null);
 			} catch (Backtrack e1) {
-				sat.deleteChoicePoint(this);
+				sat.cp.deleteChoicePoint(this);
 				throw sat.backtrack;
 			}
 		}

--- a/src/lite/ExistsSolver.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/ExistsSolver.java	Wed Jan 16 14:34:11 2008 +0900
@@ -37,12 +37,12 @@
 
 
 	private void restoreLocal(ITLSatisfier sat) {
-		sat.deleteChoicePoint(var);
+		sat.cp.deleteChoicePoint(var);
 		var.setValue(old);
 	}
 
 	private void makeLocal(ITLSatisfier sat,boolean newv) {
-		sat.addChoicePoint(var);
+		sat.cp.addChoicePoint(var);
 		var.setValue(newv);
 	}
 

--- a/src/lite/ITLCommander.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/ITLCommander.java	Wed Jan 16 14:34:11 2008 +0900
@@ -3,6 +3,7 @@
 import java.util.HashMap;
 import java.util.LinkedList;
 
+import sbdd.BDDDiagnosis;
 import sbdd.BDDSatisfier;
 import logicNode.parser.Command;
 
@@ -13,11 +14,22 @@
 	private ITLNodeParser<Node> parser;
 	public BDDSatisfier sat;
 	private HashMap<Integer,Node> examples;
+	private BDDDiagnosis diag;
 
 	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
 		this.lf = lf;
 		this.parser = parser;
 		this.examples = new HashMap<Integer,Node>();
+		
+		parser.addHelp(
+			"do(p).                     verify formula p\n"+
+			"ex(N,p).                   register numbered examle p\n"+
+			"verbose(TF).               set verbose mode (true/false)\n"+
+			"include(File).             read from File\n"+
+			"def('head(p)','body(p)').  define macro\n"+
+			"help.                      show this\n"+
+			""
+				);
 	}
 
 	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
@@ -37,7 +49,7 @@
 			Node n = lf.falseNode();
 			int length = Integer.parseInt(args.get(0).toString());
 			for(int i =0;i<length;i++) {
-				n = lf.orNode(lf.emptyNode(),lf.nextNode(n));
+				n = lf.nextNode(n);
 			}
 			return (Node)n;
 		} else if (name == "ex"|| name=="do") {
@@ -67,6 +79,9 @@
 				examples.put(index, args.get(1));
 				return lf.trueNode();
 			}
+		} else if (name == "help") {
+			parser.help();
+			return lf.trueNode();
 		} else if (name == "def") {
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
@@ -85,13 +100,24 @@
 			String file = args.getFirst().toString();
 			parser.parseFile(file);
 			return lf.trueNode();
+		} else if (name == "exe") {
+			int length = 0;
+			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
+			diag.execute(sat.last, length );
+		} else if (name == "diag") {
+			int length = 0;
+			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
+			diag.counterExample(sat.last, length);
 		}
 		System.out.println("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
 		return value;
 	}
 
 	private void checkSat() {
-		if (sat==null) sat = new BDDSatisfier();
+		if (sat==null) {
+			sat = new BDDSatisfier();
+			diag = new BDDDiagnosis(sat);
+		}
 	}
 
 }

--- a/src/lite/ITLNodeParser.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Wed Jan 16 14:34:11 2008 +0900
@@ -18,6 +18,7 @@
 	public ITLCommander<Node> parseCommand;
 	public Node emptyNode;
 	private Node periodNode;
+	public String help = "";
 	
 	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
 
@@ -55,13 +56,17 @@
 	                        Node n = value;
 	                        int length = Integer.parseInt(args.get(0).toString());
 	                        for(int i =0;i<length;i++) {
-	                                n = logicNodeFactory.nextNode(n);
+	                            n = logicNodeFactory.nextNode(n);
+	                            n=logicNodeFactory.andNode(
+	                            		logicNodeFactory.notNode(
+	                            			logicNodeFactory.emptyNode())
+	                                		,n);
 	                        }
 	                        return n;
 						}
 			});
 			define("less(I)","false",50,parseCommand);               // less than N length
-			define("next(P)","(empty; @(P)))");
+			define("@(P)","(~empty, next(P)))");
 // temporal assignments
 			define("gets(A,B)","keep(@A<->B))");
 			define("stable(A)","keep(@A<->A))");
@@ -86,6 +91,8 @@
 
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("do(N)","true",50,parseCommand);
+			define("diag(N)","true",50,parseCommand);
+			define("exe(N)","true",50,parseCommand);
 			define("def(Head,Body)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
 			
@@ -95,6 +102,7 @@
 			define("^(r)","r"); // interval variable (we cannot handle now)
 			
 			periodNode = logicNodeFactory.variableNode(".", true);
+			define("help","true",50,parseCommand);
 			// only one of the is true (should allow all false case?)
 			define("share(L)","[](share0(L))");
 			define("share0(L)","true",50, new Command<Node>() {
@@ -134,7 +142,7 @@
 		super.scanner = scanner;
 
 		dict.reserve("&",TokenID.Chop);
-		dict.reserve("@",TokenID.Next);
+		dict.reserve("next",TokenID.Next);
 		dict.reserve("proj",TokenID.Projection);
 		
 		// parseCommand requires reserved word for string comparison
@@ -144,6 +152,9 @@
 		dict.reserve("include");
 		dict.reserve("def");
 		dict.reserve("verbose");
+		dict.reserve("help");
+		dict.reserve("diag");
+		dict.reserve("exe");
 	}
 
 	@Override
@@ -225,5 +236,13 @@
 		return emptyNode;
 	}
 
+	public void addHelp(String string) {
+		help += string;
+	}
+	
+	public void help() {
+		System.out.println(help);
+	}
+
 
 }

--- a/src/lite/ITLSatisfier.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Wed Jan 16 14:34:11 2008 +0900
@@ -5,12 +5,12 @@
 import verifier.Backtrack;
 import verifier.ChoicePointList;
 
-public class ITLSatisfier extends ChoicePointList<ITLSolver> implements Next {
+public class ITLSatisfier implements Next {
 
 	/**
 	 * 
 	 */
-	private static final long serialVersionUID = 1L;
+	public ChoicePointList<ITLSolver> cp;
 	public ITLSolver true_;
 	public ITLSolver false_;
 	public SBDDFactoryInterface lf;
@@ -24,6 +24,7 @@
 		backtrack = new Backtrack();
 		true_   = ITLNodeFactory.trueSolver;
 		false_  = ITLNodeFactory.falseSolver;
+		cp = new ChoicePointList<ITLSolver>();
 	}
 	
 	public ITLSatisfier(ITLSolver p) {
@@ -65,7 +66,7 @@
 
 	
 	public ChoicePointList<ITLSolver> choicePoint() {
-		return this;
+		return cp;
 	}
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/MainLoop.java	Wed Jan 16 14:34:11 2008 +0900
@@ -0,0 +1,14 @@
+package lite;
+
+import sbdd.BDDSatisfier;
+
+public class MainLoop {
+
+	public static void main(String arg[]) {
+		BDDSatisfier sat = new BDDSatisfier();
+		// read predefined examples
+		sat.p.parseFile("data/example");
+		sat.p.help();
+		sat.p.parse(System.in);
+	}
+}

--- a/src/lite/NextSolver.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/NextSolver.java	Wed Jan 16 14:34:11 2008 +0900
@@ -12,21 +12,12 @@
 	}
 		
 	public String toString() {
-		return "@("+node+")";
+		return "next("+node+")";
 	}
 
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		return sat.empty.sat(sat, new Continuation(sat,next,this));
-	}
-
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value==null) {
-			return next.sat(node); // not empty case
-		} else {
-			return next.sat(null); // this is strong next, false on empty
-		}
+		return next.sat(node); // not empty case
 	}
 
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {

--- a/src/lite/VariableSolver.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/lite/VariableSolver.java	Wed Jan 16 14:34:11 2008 +0900
@@ -23,11 +23,11 @@
 	
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		if (sat.hasChoicePoint(this)) {
+		if (sat.cp.hasChoicePoint(this)) {
 			// choice point is already made, use it
 			return next.sat(value?sat.true_:null);
 		}
-		sat.addChoicePoint(this);
+		sat.cp.addChoicePoint(this);
 		value = true; // the first choice
 		try {
 			return next.sat(sat.true_);
@@ -39,7 +39,7 @@
 				// no more choices, remove this choice and 
 				// request backtrack to the previous choice or
 				// top level terminator
-				sat.deleteChoicePoint(this);
+				sat.cp.deleteChoicePoint(this);
 				throw e1;
 			}
 		}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/BDDDiagnosis.java	Wed Jan 16 14:34:11 2008 +0900
@@ -0,0 +1,180 @@
+package sbdd;
+
+import java.util.Comparator;
+import java.util.LinkedList;
+import java.util.TreeSet;
+
+import lite.ITLSolver;
+import verifier.ChoicePointList;
+
+public class BDDDiagnosis {
+
+	/*
+	 * Search over generated SBDDEntry for satisfiability.
+	 * find example or counter example.
+	 * 
+	 * For each tested SBDDEntry, Reachable set of SBDDEntry is necessary.
+	 * It is stored in TreeSet in generated order.
+	 */
+	
+	private BDDSatisfier sat;
+	private SBDDEntry true_;
+	private SBDDEntry false_;
+	
+	public boolean falsifiable;
+	public boolean satisfiable;
+	public TreeSet<SBDDEntry> reachable;
+	private SBDDEntry last;
+
+	public BDDDiagnosis(BDDSatisfier sat) {
+		this.sat = sat;
+		this.true_ = sat.getEntry(sat.true_);
+		this.false_ = sat.getEntry(sat.false_);
+	}
+
+	public void execute(SBDDEntry e,int length) {
+		LinkedList<SBDDEntry> trace = findTrueEntry(e,length);
+		show(trace);
+	}
+	
+	public void counterExample(SBDDEntry e,int length) {
+		LinkedList<SBDDEntry> trace = findFalseEntry(e,length);
+		show(trace);
+	}
+	
+	public void execute(int length) {
+		LinkedList<SBDDEntry> trace = findTrueEntry(last,length);
+		show(trace);
+	}
+	
+	public void counterExample(int length) {
+		LinkedList<SBDDEntry> trace = findFalseEntry(last,length);
+		show(trace);
+	}
+
+	/*
+	 * Show found trace. SBDDEntry does not contains choice point set
+	 * i.e. transition condition represented by true/false combination of
+	 * variables. Choice point have to be generated on the fly. Condition
+	 * Edge is 2^(number of variable), so it is not good to have all in
+	 * memory. 
+	 */
+	private void show(LinkedList<SBDDEntry> trace) {
+		SBDDEntry last = trace.getLast();
+		int i = 0;
+		for(SBDDEntry e: trace) {
+			System.out.print(i+":"+e.id+":\t");
+			if (e!=last) {
+				ChoicePointList<ITLSolver>cp = 
+					sat.findNext(e,trace.get(i++));
+				System.out.print(cp);
+			}
+			System.out.println();
+		}
+	}
+
+	private LinkedList<SBDDEntry> findTrueEntry(SBDDEntry e, int length) {
+		SBDDEntry dest = true_;
+		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		return findMore(e,dest,length,trace);
+	}
+	
+	private LinkedList<SBDDEntry> findFalseEntry(SBDDEntry e, int length) {
+		SBDDEntry dest = false_;
+		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
+		return findMore(e,dest,length,trace);
+	}
+
+	/*
+	 * 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);
+			}
+			trace.addFirst(e);
+		}
+		return trace;
+	}
+
+	/*
+	 * find lengthy trace from an start entry to a destination. Reachable 
+	 * set have to be generated from the start entry.
+	 */
+	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);
+			} catch (Result e1) {
+				// found
+				return trace;
+			}
+		}
+		// not found
+		return trace;
+	}
+	
+
+	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;
+					}
+				});
+		if (e==null) return;
+		LinkedList<Iterable<SBDDEntry>> stack = new LinkedList<Iterable<SBDDEntry>>();
+		Iterable<SBDDEntry> current = e.nexts(); 
+		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;
+				}
+			}
+			// 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
+		for(SBDDEntry p: reachable) {
+			if (p.nexts.contains(e)) {
+				return e;
+			}
+		}
+		return null;
+	}
+	
+	class Result extends Exception {
+		private static final long serialVersionUID = 1L;
+	}
+
+	private void findTrace(LinkedList<SBDDEntry> trace, SBDDEntry start,SBDDEntry e, int length) throws Result {
+		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();
+				findTrace(trace,start,p,length-1);
+			}
+		}
+		trace.removeFirst(); // have to be e
+	}
+}

--- a/src/sbdd/BDDSatisfier.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Wed Jan 16 14:34:11 2008 +0900
@@ -2,8 +2,10 @@
 
 import java.util.LinkedList;
 
+import verifier.Backtrack;
+import verifier.ChoicePointList;
 
-import verifier.Backtrack;
+
 import lite.BDDSolver;
 import lite.Continuation;
 import lite.ITLNodeFactory;
@@ -12,6 +14,7 @@
 import lite.ITLSatisfier;
 import lite.ITLSolver;
 import lite.Next;
+import lite.VariableSolver;
 import logicNode.parser.ExecutorInterface;
 
 public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface<ITLSolver> {
@@ -23,12 +26,8 @@
 	public  LinkedList<SBDDEntry> queue;
 	public  SBDDSet state;
 	public SBDDEntry currentState;
-	
-
-	private boolean satisfiable;
-	private boolean falsfiable;
 	public SBDDEntry last;
-
+	boolean falsifiable,satisfiable;
 
 	/**
 	 * 
@@ -82,24 +81,49 @@
 		// System.out.println(sf.hash);
 		System.out.println();
 	}
-	
+
 	class AllNext implements Next {
 
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			if (value!=null) {
+				if (value==true_) satisfiable = true;
 				SBDDEntry e = state.getEntry(value);
+				currentState.addNext(e);
 				if (e.expanded) {
 					System.out.print((e.key==sat.true_)?"t":".");
 				} else 	{
 					queue.add(e); e.expanded = true;
 					System.out.print(e.id+" ");
-				} 
+				}
 			} else {
-				System.out.print("f");
+				System.out.print("f"); falsifiable = true;
 			}
 			throw sat.backtrack;
 		}
 	}
+
+	public ChoicePointList<ITLSolver> copy(ChoicePointList<ITLSolver> cplist) {
+		ChoicePointList<ITLSolver> newcp = new ChoicePointList<ITLSolver>();
+		for(ITLSolver cp : cplist) {
+			newcp.add(new VariableSolver(cp.toString(),cp.value));
+		}
+		return newcp;
+	}
+	
+	class FindNext extends LinkedList<ChoicePointList<ITLSolver>> implements Next  {
+		private static final long serialVersionUID = 1L;
+		public SBDDEntry dest;
+		FindNext(SBDDEntry dest) { this.dest = dest; }
+		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			if (value!=null&&value!=true_) {
+				SBDDEntry e = state.getEntry(value);
+				if (e.expanded) {
+					add(copy(sat.cp));
+				} 
+			} 
+			throw sat.backtrack;
+		}
+	}
 	
 	class AllNextVerbose implements Next {
 
@@ -108,7 +132,7 @@
 			System.out.print(" "+sat.choicePoint()+" -> ");
 			if (value!=null) {
 				if (value==true_) {
-					satisfiable = true; s="true";
+					s="true";satisfiable = true;
 				} else {
 					SBDDEntry e = state.getEntry(value);
 					currentState.addNext(e);
@@ -118,10 +142,10 @@
 					} else 	{
 						queue.add(e); e.expanded = true;
 						s = "!"+s;
-					} 
+					}
 				}
 			} else {
-				falsfiable = true;
+				falsifiable = true;
 			}
 			System.out.println(s);
 			throw sat.backtrack;
@@ -129,8 +153,6 @@
 	}
 
 	public void verify(ITLSolver n) {
-		falsfiable = false;
-		satisfiable = false;
 		queue = new LinkedList<SBDDEntry>();
 		Next allNext = verbose? new AllNextVerbose() : new AllNext();
 		SBDDEntry b = state.getEntry(n);
@@ -143,18 +165,23 @@
 		queue.add(b); b.expanded = true;
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
 			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
-			currentState = e;
+			currentState = e; falsifiable=false; satisfiable = false;
 			develop(e.key, allNext);
+			// this flag is work on current state
+			// to check validity/unsatisfiability, full check is required.
+			e.falsifiable = falsifiable; e.satisfiable = satisfiable;
 			if (!verbose) System.out.println();
 		}
-		if (verbose) {
-			if (!falsfiable) {
-				System.out.println("valid");
-			}
-			if (!satisfiable) {
-				System.out.println("unsatisfiable");
-			}
-		}
+	}
+
+	public SBDDEntry getEntry(ITLSolver key) {
+		return sf.hash.getEntry(key);
+	}
+
+
+	public ChoicePointList<ITLSolver> findNext(SBDDEntry e, SBDDEntry entry) {
+		// TODO Auto-generated method stub
+		return null;
 	}
 	
 }

--- a/src/sbdd/SBDDEntry.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/sbdd/SBDDEntry.java	Wed Jan 16 14:34:11 2008 +0900
@@ -2,18 +2,19 @@
 
 
 import lite.ITLSolver;
-
+import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.Map.Entry;
 
 
-
 public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> {
 
 	public ITLSolver key;
 	boolean expanded = false;
 	int id;
 	LinkedList<SBDDEntry>nexts;
+	public boolean falsifiable;
+	public boolean satisfiable;
 	
 	public SBDDEntry(ITLSolver now) {
 		this.key = now;
@@ -49,4 +50,22 @@
 		return nexts.add(e);
 	}
 
+	// Iterate over possible next
+	public Iterable<SBDDEntry> nexts() {
+		return new Iterable<SBDDEntry>() {
+			int i = 0;
+			public Iterator<SBDDEntry> iterator() {
+				return new Iterator<SBDDEntry>() {
+					public boolean hasNext() {
+						return nexts.size()>i;
+					}
+					public SBDDEntry next() {
+						return nexts.get(i++);
+					}
+					public void remove() {
+					}
+				};
+			}
+		};
+	}
 }

--- a/src/sbdd/SBDDTest.java	Wed Jan 16 14:34:04 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Wed Jan 16 14:34:11 2008 +0900
@@ -18,8 +18,8 @@
 		
 		//test.bddTest();
 		//test.satTest();
-		//test.verifyTest();
-		test.mainLoop();
+		test.verifyTest();
+		//test.mainLoop();
 	}
 	
 	
@@ -63,7 +63,7 @@
 	public void verifyTest() {
 		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");
 
-		if (false) {
+		if (true) {
 		sat.showVerify("skip");
 		sat.showVerify(" '<>'p");
 		sat.showVerify("<>(p) = <>(p)");
@@ -92,6 +92,7 @@
 		//System.out.println(sat.state);
 		sat.p.parse("include('data/example').");
 		//System.out.println(p.parseCommand.sat.state);
+		sat.p.parse("do(10)");
 	}
 
 	public void mainLoop() {