Mercurial > hg > Applications > JavaLite

changeset 107:30e74062f06c continuation-removal

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Sun, 20 Jan 2008 18:22:55 +0900
parents f664474ae23b
children b508608e3cce
files Changes src/lite/AndSolver.java src/lite/BDDSolver.java src/lite/Backtrack.java src/lite/ChoicePointList.java src/lite/ChopSolver.java src/lite/Continuation.java src/lite/EmptySolver.java src/lite/ExistsSolver.java src/lite/FalseSolver.java src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/lite/ITLNodeScanner.java src/lite/ITLNodeScannerTest.java src/lite/ITLSatisfier.java src/lite/ITLSolver.java src/lite/ITLSolverTest.java src/lite/MacroSolver.java src/lite/Next.java src/lite/NextSolver.java src/lite/NotSolver.java src/lite/NumberSolver.java src/lite/OrSolver.java src/lite/PredicateSolver.java src/lite/ProjectionSolver.java src/lite/TrueSolver.java src/lite/VariableSolver.java src/parser/ITLCommander.java src/parser/ITLNodeParser.java src/parser/ITLNodeScanner.java src/parser/ITLNodeScannerTest.java src/parser/LogicNodeParser.java src/parser/MacroNodeParser.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDTest.java
diffstat 35 files changed, 1038 insertions(+), 833 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Sun Jan 20 01:53:55 2008 +0900
+++ b/Changes	Sun Jan 20 18:22:55 2008 +0900
@@ -1,3 +1,56 @@
+Sun Jan 20 10:44:41 JST 2008
+
+うーん、たぶん、class Continuation を取り除くことは可能なんだろうな。
+
+	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 { } ....
+
+とかの代わりに、
+
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return sat.empty.sat(sat, new Chop1(next));
+       }
+
+       class Chop1 implements Next {
+            Next next;
+            Chop1(Next next) {
+                  this.next = next;
+            }
+            public ITLSolver next(ITLSolver value) {
+                   if(value==null) 
+		       return next.next(myValue);   // return case
+                   return  var.sat(sat, new Chop2(next)); // call case
+           }
+       }
+
+ぐらい? next を自分で持っていれば、いらない? Recursive call が
+なければ。いや、あるか。この方が new Continuation がなくなる分、
+速いよね。割と簡単に直せる?!
+
+Chop1 とかが増えるのを嫌って汎用のContinuationを入れたんだけど、
+どうせたくさんあるから、関係ないってことなのか。
+
+done in 30032msec
+-> show.
+All Edges: 324099
+Number of BDD: 12273
+Number of Subterm: 70
+Reachable state: 1366
+-> 
+
+done in 26869msec
+-> show.
+All Edges: 324099
+Number of BDD: 12273
+Number of Subterm: 70
+Reachable state: 1366
+
+あぁ、やっぱり少し速くはなるのか。
+
 Sun Jan 20 01:30:04 JST 2008
 
 とりあえず Release 。Release の時に Changes を入れないように
--- a/src/lite/AndSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/AndSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,7 +1,6 @@
 package lite;
 
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 
 public class AndSolver extends ITLSolver {
@@ -19,35 +18,21 @@
 	}
 
 
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		return left.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(null);
-		} else if (value==sat.true_) {
-			return right.sat(sat, next);
-		} else {
-			return right.sat(sat, new Continuation(sat,next,
-					new AndSolver2(value)));
-		}
-	}
 
 	class AndSolver2 implements Next {
 		ITLSolver residue;
-		public AndSolver2(ITLSolver value) {
+		Next next;
+		public AndSolver2(Next next,ITLSolver value) {
 			residue = value;
+			this.next = next;
 		}
-
-		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {
-				return next.sat(null);
+				return next.next(sat,null);
 			} else if (value==sat.true_) {
-				return next.sat(residue);
+				return next.next(sat,residue);
 			} else {
-				return next.sat(sat.lf.andNode(residue,value));
+				return next.next(sat,sat.lf.andNode(residue,value));
 			}
 		}
 	}
@@ -56,5 +41,25 @@
 		return left.toSBDD(sf).and(sf, right.toSBDD(sf)).toSBDD(sf);
 	}
 
+	class AndSolver1 implements Next {
+		Next next;
+		public AndSolver1(Next next) {
+			this.next = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) {
+				return next.next(sat,null);
+			} else if (value==sat.true_) {
+				return right.sat(sat, next);
+			} else {
+				return right.sat(sat, new AndSolver2(next,value));
+			}
+		}
+	}
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return left.sat(sat,new AndSolver1(next));
+	}
+
 	
 }
--- a/src/lite/BDDSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/BDDSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import sbdd.BDDID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class BDDSolver extends ITLSolver {
 	
@@ -63,61 +62,42 @@
 	}
 
 
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		if (id!=BDDID.Variable&&id!=BDDID.BDD) {
-			return var.sat(sat,next);
-		}
-		return var.sat(sat, new Continuation(sat,next,this));
-	}
-
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value==null) {
-			return low.sat(sat, next);
-		} else if (value==sat.true_) {
-			return high.sat(sat, next);
-		} else {
-			return high.sat(sat, new Continuation(sat,next,
-					new BDDSolver2(value)));
-		}
-	}
-
 	class BDDSolver2 implements Next {
-		ITLSolver cond;
-		public BDDSolver2(ITLSolver value) {
-			cond = value;
+		ITLSolver cond; Next next;
+		public BDDSolver2(Next next,ITLSolver value) {
+			cond = value;this.next = next;
 		}
 
-		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-			return low.sat(sat, new Continuation(sat,next,
-					new BDDSolver3(cond,value)));
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			return low.sat(sat, new BDDSolver3(next,cond,value));
 		}
 	}
 
 	class BDDSolver3 implements Next {
-		ITLSolver cond, high;
-		public BDDSolver3(ITLSolver cond, ITLSolver value) {
+		ITLSolver cond, high; Next next;
+		public BDDSolver3(Next next,ITLSolver cond, ITLSolver value) {
 			this.cond = cond;
 			high = value;
+			this.next = next;
 		}
 
-		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver low) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver low) throws Backtrack {
 			if (low==sat.true_ && high==sat.true_) 
-				return next.sat(low);
+				return next.next(sat,low);
 			if (low==null && high==null) 
-				return next.sat(null);
+				return next.next(sat,null);
 			if (low == high) {
-				return next.sat(low);
+				return next.next(sat,low);
 			} else {
 				// lf.bddNode(cond,high,low) won't work
 				if (low==null)  low = sat.lf.falseNode();
 				if (high==null) high = sat.lf.falseNode();
 				// if (cond==null) cond = sat.lf.falseNode();
-				ITLSolver value = sat.lf.orNode(
+				ITLSolver value1 = sat.lf.orNode(
 						sat.lf.andNode(cond, high),
 						sat.lf.andNode(sat.lf.notNode(cond), low));
-				if (value==sat.false_) value = null;
-				return next.sat(value);
+				if (value1==sat.false_) value1 = null;
+				return next.next(sat,value1);
 			}
 		}
 	}
@@ -216,4 +196,29 @@
 	public ITLSolver var() {
 		return var;
 	}
+
+	class BDDSolver1 implements Next {
+		Next next;
+		public BDDSolver1(Next next) {
+			this.next = next;
+		}
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) {
+				return low.sat(sat, next);
+			} else if (value==sat.true_) {
+				return high.sat(sat, next);
+			} else {
+				return high.sat(sat, new BDDSolver2(next,value));
+			}
+		}
+	}
+	
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		if (id!=BDDID.Variable&&id!=BDDID.BDD) {
+			return var.sat(sat,next);
+		}
+		return var.sat(sat, new BDDSolver1(next));
+	}
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/Backtrack.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,10 @@
+package lite;
+
+public class Backtrack extends Exception {
+
+	/**
+	 * 
+	 */
+	private static final long serialVersionUID = 1L;
+
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ChoicePointList.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,57 @@
+package lite;
+
+import java.util.LinkedList;
+
+public class ChoicePointList<CP extends ITLSolver> extends LinkedList<CP> {
+
+	/**
+	 * 
+	 */
+	private static final long serialVersionUID = 1L;
+
+	public void addChoicePoint(CP cp) {
+		add(cp);
+	}
+
+	public void deleteChoicePoint(CP cp) {
+		remove(cp);
+	}
+
+	public boolean hasChoicePoint(CP cp) {
+		return contains(cp);
+	}
+	
+	public String toString() {
+		CP n;
+		String s = "[";
+		if (!this.isEmpty()) { 
+			if ((n=this.getFirst())!=null) {
+				s += cpToString(n);
+			}
+			if (!this.isEmpty()) {
+				for(int i=1;i<size();i++) {
+					n = get(i);
+					s += ","+cpToString(n);
+				}
+			}
+		}
+		return s+"]";
+	}
+
+	public String cpToString(CP cp) { 
+		if (!cp.value()) {
+			return "~"+cp  ;
+		} else {
+			return cp.toString();
+		}
+	}
+	
+	public String cpToStringHash(CP cp) { 
+		if (!cp.value()) {
+			return "~"+cp  +"("+cp.hashCode()+")";
+		} else {
+			return cp.toString()+"("+cp.hashCode()+")";
+		}
+	}
+
+}
\ No newline at end of file
--- a/src/lite/ChopSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ChopSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class ChopSolver extends ITLSolver {
 
@@ -45,42 +44,60 @@
 	public String toString() {
 		return "("+former+" & "+later+")";
 	}
-
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+	
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
 		// make choice point on empty, first try empty case
-		return sat.empty.sat(sat, new Continuation(sat,next,this));
+		return sat.empty.sat(sat, new ChopSolver1(next));
 	}
 
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value!=null) { // Outer empty case
-			return former.sat(sat, new Continuation(sat,next, new ChopSolver2()));
-		} else {
-			sat.empty.setValue(true);
-			// Try inner empty case ( former is going to check on empty interval )
-			return former.sat(sat, new Continuation(sat,next, new ChopSolver3()));
+
+	class ChopSolver1 implements Next {
+		Next next;
+		ChopSolver1(Next next) {
+			this.next = next;
+		}
+		// check later part on Outer empty case (same as AndSolver )
+		public ITLSolver next(ITLSatisfier sat,ITLSolver value) throws Backtrack {
+			if (value!=null) { // Outer empty case
+				return former.sat(sat, new ChopSolver2(next));
+			} else {
+				sat.empty.setValue(true);
+				// Try inner empty case ( former is going to check on empty interval )
+				return former.sat(sat, new ChopSolver3(next));
+			}
 		}
 	}
 
 	class ChopSolver2 implements Next {
+
+		Next next;
+		ChopSolver2(Next next) {
+			this.next = next;
+		}
 		// check later part on Outer empty case (same as AndSolver )
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			if (value==null) return next.sat(value);
+
+		public ITLSolver next(ITLSatisfier sat,ITLSolver value) throws Backtrack {
+			if (value==null) return next.next(sat,value);
 			else return later.sat(sat, next);
 		}
 	}
 
 	class ChopSolver3 implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+
+		Next next;
+		ChopSolver3(Next next) {
+			this.next = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			try {
 				sat.empty.setValue(false);
 				if (value==null) {
 					// former is falied on empty, try more
-					return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
+					return former.sat(sat,  new ChopSolver4(next));
 				} else {
 					// former is true on empty try later part on outer interval
 					// outerEmpty is false now (we have already tried true case), so if later contains empty, it will fail.
-					return later.sat(sat, new Continuation(sat,next, new ChopSolver5()));
+					return later.sat(sat, new ChopSolver5(next));
 				}
 			} catch (Backtrack e) {
 				sat.empty.setValue(true);
@@ -91,54 +108,66 @@
 	
 	class ChopSolver4 implements Next {
 		// try former on more (single choice case)
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+
+		Next next;
+		ChopSolver4(Next next) {
+			this.next = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			try {
-			if (value==null) {
-				// all failed
-				return next.sat(value);
-			} else {
-				// former is true with @value, return @(value&later)
-				// optimize required to avoid creating same node
-				return next.sat(sat.lf.chopNode(value,later));
-			}
-			} catch (Backtrack e) {
-				sat.empty.setValue(false);
-				throw e;
-			}
+				if (value==null) {
+					// all failed
+					return next.next(sat,value);
+				} else {
+					// former is true with @value, return @(value&later)
+					// optimize required to avoid creating same node
+					return next.next(sat,sat.lf.chopNode(value,later));
+				}
+				} catch (Backtrack e) {
+					sat.empty.setValue(false);
+					throw e;
+				}
 		}
 	}
 
 	class ChopSolver5 implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+
+		Next next;
+		ChopSolver5(Next next) {
+			this.next = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {  // former is true on empty but later is failed on more
 				// try again only on more case
-				return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
+				return former.sat(sat,  new ChopSolver4(next));
 			} else {
 				// try innerMore case with this next term
-				return former.sat(sat,  new Continuation(sat,next, new ChopSolver6(value)));
+				return former.sat(sat,  new ChopSolver6(next,value));
 			}
 		}
 	}
 	
 	class ChopSolver6 implements Next {
 		ITLSolver later1;
-		ChopSolver6(ITLSolver value) { later1 = value; }
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		Next next;
+		ChopSolver6(Next next,ITLSolver value) { later1 = value;this.next = next; }
+		
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			try {
-			if (value==null) {  // former is fail on more inerval
-				return next.sat(later1);
-			} else {
-				// we don't have to execute later case now, do it on next clock
-				ITLSolver former1 = sat.lf.chopNode(value,later);
-				// return disjunction with other choice
-				ITLSolver v = sat.lf.orNode(later1,former1);
-				if (v==sat.false_) v = null;
-				return next.sat(v);
-			}
-			} catch (Backtrack e) {
-				sat.empty.setValue(false);
-				throw e;
-			}
+				if (value==null) {  // former is fail on more inerval
+					return next.next(sat,later1);
+				} else {
+					// we don't have to execute later case now, do it on next clock
+					ITLSolver former1 = sat.lf.chopNode(value,later);
+					// return disjunction with other choice
+					ITLSolver v = sat.lf.orNode(later1,former1);
+					if (v==sat.false_) v = null;
+					return next.next(sat,v);
+				}
+				} catch (Backtrack e) {
+					sat.empty.setValue(false);
+					throw e;
+				}
 		}
 	}
 
--- a/src/lite/Continuation.java	Sun Jan 20 01:53:55 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-package lite;
-
-import verifier.Backtrack;
-
-public class Continuation {
-
-	public ITLSatisfier sat;
-	public Continuation next;
-	public Next solver;
-
-	/*
-	 * Depth first search stack
-	 * we use CPS style programming for try/throw backtrack
-	 * but it is better to use stack base implementation?
-	 */
-	public Continuation(ITLSatisfier sat, Continuation next, Next solver) {
-		// keep next and our boss's state (solver)
-		this.sat = sat; this.next = next; this.solver = solver;
-	}
-
-
-	public ITLSolver sat(ITLSolver value) throws Backtrack {
-		// We've gotten the value, pass it to our boss with next execution point
-		return solver.next(sat,next,value);
-	}
-
-
-}
--- a/src/lite/EmptySolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/EmptySolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class EmptySolver extends ITLSolver {
 
@@ -16,19 +15,19 @@
 		return name;
 	}
 
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+	
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
 		// return sat.empty.sat(sat, next);
 		if (sat.cp.hasChoicePoint(this))
-			return next.sat(value?sat.true_:null);
+			return next.next(sat,value?sat.true_:null);
 		value = true;
 		try {
 			sat.cp.addChoicePoint(this);
-			return next.sat(sat.true_);
+			return next.next(sat,sat.true_);
 		} catch (Backtrack e) {
 			value = false;
 			try {
-				return next.sat(null);
+				return next.next(sat,null);
 			} catch (Backtrack e1) {
 				sat.cp.deleteChoicePoint(this);
 				throw sat.backtrack;
@@ -62,4 +61,5 @@
 		}
 		return false;
 	}
+
 }
--- a/src/lite/ExistsSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ExistsSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -3,7 +3,6 @@
 import parser.TokenID;
 
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class ExistsSolver extends ITLSolver {
 
@@ -22,19 +21,6 @@
 		return "exists("+var+",("+node+"))";
 	}
 
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		old = var.value;
-		makeLocal(sat,true);
-		try {
-			return node.sat(sat, new Continuation(sat,next,this));
-		} catch (Backtrack e) {
-			restoreLocal(sat);
-			var.setValue(old);
-			throw sat.backtrack;
-		}
-	}
-
 
 	private void restoreLocal(ITLSatisfier sat) {
 		sat.cp.deleteChoicePoint(var);
@@ -46,43 +32,14 @@
 		var.setValue(newv);
 	}
 
-	private ITLSolver restoreLocal(ITLSatisfier sat,boolean now,ITLSolver value,Continuation next) throws Backtrack {
-		restoreLocal(sat);
-		try {
-			return next.sat(value);
-		} catch (Backtrack e) {
-			makeLocal(sat,now);
-			throw sat.backtrack;
+	class ExistsSolver2 implements Next {
+		private Next next;
+
+		public ExistsSolver2(Next next) {
+			this.next = next;
 		}
-	}
-	
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value==null) {
-			var.setValue(false);
-			try {
-				return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
-			} catch (Backtrack e) {
-				var.setValue(true);
-				throw e;
-			}
-		} else if (value==sat.true_) {
-			return restoreLocal(sat,true,value,next);
-		} else {
-			var.setValue(false);
-			residue = value;
-			try {
-				return node.sat(sat, new Continuation(sat,next,
-					new ExistsSolver2()));
-			} catch (Backtrack e) {
-				var.setValue(true);
-				throw e;
-			}
-		}
-	}
 
-	class ExistsSolver2 implements Next {
-		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {
 				value = sat.lf.existsNode(var,residue);
 			} else if (value==sat.true_) {
@@ -98,9 +55,25 @@
 			return restoreLocal(sat,false,value,next);
 		}
 	}
-	
+
+	private ITLSolver restoreLocal(ITLSatisfier sat, boolean now, ITLSolver value, Next next) throws Backtrack {
+		restoreLocal(sat);
+		try {
+			return next.next(sat,value);
+		} catch (Backtrack e) {
+			makeLocal(sat,now);
+			throw sat.backtrack;
+		}
+	}
+
+
 	class ExistsSolver3 implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		Next next;
+		public ExistsSolver3(Next next) {
+			this.next = next;
+		}
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {
 			} else if (value==sat.true_) {
 			} else {
@@ -136,4 +109,48 @@
 		}
 		return false;
 	}
+
+
+	class ExistsSolver1 implements Next {
+		Next next;
+		ExistsSolver1(Next next) {
+			this.next = next;
+		}
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) {
+				var.setValue(false);
+				try {
+					return node.sat(sat, new ExistsSolver3(next));
+				} catch (Backtrack e) {
+					var.setValue(true);
+					throw e;
+				}
+			} else if (value==sat.true_) {
+				return restoreLocal(sat,true,value,next);
+			} else {
+				var.setValue(false);
+				residue = value;
+				try {
+					return node.sat(sat,new ExistsSolver2(next));
+				} catch (Backtrack e) {
+					var.setValue(true);
+					throw e;
+				}
+			}
+		}
+	}
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		old = var.value;
+		makeLocal(sat,true);
+		try {
+			return node.sat(sat, new ExistsSolver1(next));
+		} catch (Backtrack e) {
+			restoreLocal(sat);
+			var.setValue(old);
+			throw sat.backtrack;
+		}
+	}
 }
--- a/src/lite/FalseSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/FalseSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class FalseSolver extends ITLSolver {
 
@@ -10,10 +9,6 @@
 		order = TokenID.False.hash;
 	}
 	
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		return next.sat(null);
-	}
 	
 
 	public String toString() {
@@ -34,4 +29,10 @@
 	public boolean equals(Object o) {
 		return o==this;
 	}
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return next.next(sat, null);
+	}
 }
--- a/src/lite/ITLCommander.java	Sun Jan 20 01:53:55 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-package lite;
-
-import java.util.LinkedList;
-import java.util.TreeMap;
-
-import parser.Command;
-
-import sbdd.BDDDiagnosis;
-import sbdd.BDDSatisfier;
-import sbdd.SBDDEntry;
-
-public class ITLCommander<Node extends ITLSolver> implements Command<Node> {
-
-
-	private ITLNodeFactoryInterface<Node> lf;
-	private ITLNodeParser parser;
-	public BDDSatisfier sat;
-	private TreeMap<Integer,Node> examples;
-	private BDDDiagnosis diag;
-
-	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser parser) {
-		this.lf = lf;
-		this.parser = parser;
-		this.examples = new TreeMap<Integer,Node>();
-		
-		parser.addHelp(
-			"do(p).                     verify formula p or a numberd example, try do(10).\n"+
-			"ex(N,p).                   register numbered examle p\n"+
-			"ls.                        list predefined example\n"+
-			"verbose(TF).               set verbose mode (true/false)\n"+
-			"include(File).             read from File\n"+
-			"def('head(p)','body(p)').  define macro\n"+
-			"exe.                       execute last verifed formula\n"+
-			"diag.                      counter example of last verifed formula\n"+
-			"clear.                     clear state database\n"+
-			"show.                      show state statistics\n"+
-			"readme.                    show README\n"+
-			"help.                      show this\n"+
-			""
-				);
-	}
-
-	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
-		
-		// All names used here have to be reserved. Otherwise, parser generated name becomes 
-		// different string at run time, as a result, name=="less" will fail even if name contains "less". 
-		// If we reseve it, paredicateNode.varaibleNode.name contains pregenerated String which is 
-		// equivalent to used here. Of course name.equal("less") works fine, but it is time consuming. 
-		// Although it is practically allowed but I cannot accept.
-		
-		// We can also define Command as internal interface class in ITLNodeParser. In this case
-		// reserve operation is not required, like "length" macro.
-
-		String name = predicate.toString();
-		
-		if (name=="less") {
-			Node n = lf.falseNode();
-			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();
-			if (args.size()<1) {
-				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
-				return lf.trueNode();
-			}
-			int index = atoi(args);
-			if (args.size()==1) {
-				Node n = args.get(0);
-				if (index>=0) {
-					// do(10) case
-					n = examples.get(index);
-					if (n==null) {
-						parser.error("Unknown registered example");
-						return lf.trueNode();
-					}
-				}
-				System.out.println(n);
-				sat.verify(n);
-			} else if (args.size()==2 && index>=0){
-				examples.put(index, args.get(1));
-			}
-		} else if (name == "ls") {
-			// this is not human readable...
-			//for(int i:examples.keySet()) {
-			// System.out.println(i+":"+examples.get(i));
-			//}
-			parser.showResourceFile("data/example");
-		} else if (name == "readme") {
-			parser.showResourceFile("data/README");
-		} else if (name == "help") {
-			parser.help();
-		} else if (name == "def") {
-			parser.define(args.get(0).toString(),args.get(1).toString());
-		} else if (name == "verbose") {
-			// verbose(true) / verbose(off)
-			checkSat();
-			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 = atoi(args);
-			checkSat();
-			diag.execute(sat.last, length );
-		} else if (name == "diag") {
-			int length = 0;
-			if (args.size()>1) length = atoi(args);
-			checkSat();
-			diag.counterExample(sat.last, length);
-		} else if (name == "clear") {
-			sat = null;
-			checkSat();
-		} else if (name == "states") {
-			// 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);
-		} else
-			parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
-		return lf.trueNode();
-	}
-
-	private int atoi(LinkedList<Node> args) {
-		// should have more strcit check..
-		int i=-1;
-		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();
-			diag = new BDDDiagnosis(sat);
-		}
-	}
-
-}
--- a/src/lite/ITLNodeParser.java	Sun Jan 20 01:53:55 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,264 +0,0 @@
-package lite;
-
-import java.util.LinkedList;
-
-import parser.Command;
-import parser.Dictionary;
-import parser.LogicNodeScope;
-import parser.MacroNodeParser;
-import parser.Token;
-import parser.TokenID;
-
-
-public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> {
-
-	public ITLNodeFactoryInterface<Node> logicNodeFactory;
-	public ITLNodeScanner<Node> scanner;
-	public ITLCommander<Node> parseCommand;
-	public Node emptyNode;
-	private Node periodNode;
-	public String help = "";
-	
-	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
-
-		super(lf);
-		logicNodeFactory = lf;
-		initialize();
-
-		Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty);
-		emptyNode = emptyToken.value = logicNodeFactory.emptyNode();
-		
-		parseCommand = new ITLCommander<Node>(lf,this);
-		
-			define("not(P)","~P");                               // not
-			define("P->Q","(not(P);Q))",101);                         // imply
-			define("P<->Q","((not(P);Q),(P; not(Q)))");            // equiv
-			define("P=Q","((not(P);Q),(P; not(Q)))");              // equiv 
-			// P&&Q have to be left associative ( xfy i.e. a&&b&&c = a&&(b&&c)
-			// odd order means xfy associativity. & is right associative (yfx) in this
-			// parser, but & has associative, so it is alright. (&& is not assosicative)
-			define("P && Q","((not(empty),P) & Q))",901);             // strong chop
-			define("'<>'(Q)","(true & Q))");                        // sometime
-			define("'#'(Q)"," not(true & not(Q)))");                // always
-			define("'[]'(Q)"," not(true & not(Q)))");               // always
-			define("'[a]'(Q)"," not(true & not(Q) & true))");       // always with arbitary fin
-			define("'<a>'(Q)"," (true & Q & true))");       // sometime with arbitary fin
-			define("fin(Q)","(true & (empty,Q)))");                 // final state in the interval
-			define("keep(Q)"," not(true & not((empty ; Q))))");     // except final state
-			define("halt(Q)"," '[]'(empty=Q))");    
-			define("more"," not(empty))");                          // non empty interval
-// discrete stuff
-			define("skip"," @(empty))");                            // 1 length interval
-			define("infinite"," (true & false))");                  // 
-			define("finite"," ~((true & false)))");                 // 
-			// define("length(I)", "true",50,command);            // length operator
-			define("length(I)", "empty",50,                          // length operator
-					new Command<Node>() {
-						public Node exec(Node predicate, Node value, LinkedList<Node> args) {
-	                        Node n = value;
-	                        int length = Integer.parseInt(args.get(0).toString());
-	                        for(int i =0;i<length;i++) {
-	                            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("@(P)","(~empty, next(P)))");
-// temporal assignments
-			define("gets(A,B)","keep(@A<->B))");
-			define("stable(A)","keep(@A<->A))");
-			// define("state(A)","(share(A),'[]'(L))):- def_state(A,L)");
-// def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R))))");
-//   easier one
-            define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))");
-// def(P<=Q,Q=>P)");
-// loop stuff and quantifiers
-			define("*(A) ","proj(A,true),fin(A)");  // weak closure
-			// define("+(A) ","A& *(empty;A)");   // strong closure (difficult one)
-			define("+(A) ","A & proj(A,true)");   // strong closure
-			define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
-			define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
-			define("all(P,Q)","not(exists(P,not(Q)))");
-			define("local(P)"," (P = (P&true))");
-// test predicates
-//			define("trace(X,List),L) :- !,make_trace(List,X,L)");
-			define("even(P)","exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P)))))");
-			define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))"); 
-			define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");
-
-			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);
-			
-			define("ex0(N,Exp)","skipped");
-			define("verbose(I)", "true",50,parseCommand);                    
-			
-			define("^(r)","r"); // interval variable (we cannot handle now)
-			
-			periodNode = logicNodeFactory.variableNode(".", true);
-			define("help","true",50,parseCommand);
-			define("show","true",50,parseCommand);
-			define("states","true",50,parseCommand);
-			define("ls","true",50,parseCommand);
-			define("readme","true",50,parseCommand);
-			define("clear","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>() {
-				@SuppressWarnings("unchecked")
-				public Node exec(Node predicate, Node value, LinkedList<Node> args) {
-					Node allElse = logicNodeFactory.trueNode();
-					Node allFalse = allElse;
-					Node falseNode = value= logicNodeFactory.falseNode();
-					LinkedList<? extends ITLSolver> list = args.get(0).arguments();
-					if (list==null) {
-						error("sahre: missing [] argument");
-						return value;
-					}
-					if (list.isEmpty()) return value;
-					for(ITLSolver n:  list) {
-						Node n1 = (Node)n;
-						value = logicNodeFactory.bddNode(n1, allElse, value);
-						allElse = logicNodeFactory.bddNode(n1,falseNode,allElse); 
-						allFalse = logicNodeFactory.andNode(
-								logicNodeFactory.notNode(n1), allFalse);
-					}
-					//return value;
-					return logicNodeFactory.orNode(value,allFalse);
-				}
-			});
-
-	}
-
-	public ITLNodeParser() {
-		super();
-	}
-	
-
-	@Override
-	public void initialize() {
-		dict = new Dictionary<Node>();
-		scope = new LogicNodeScope<Node>(null,dict);
-		initReservedWord();
-		scanner = new ITLNodeScanner<Node>(dict);
-		super.scanner = scanner;
-
-		dict.reserve("&",TokenID.Chop);
-		dict.reserve("next",TokenID.Next);
-		dict.reserve("proj",TokenID.Projection);
-		
-		// parseCommand requires compile tme reserved word for string comparison
-		dict.reserve("less");
-		dict.reserve("ex");
-		dict.reserve("do");
-		dict.reserve("include");
-		dict.reserve("def");
-		dict.reserve("verbose");
-		dict.reserve("help");
-		dict.reserve("diag");
-		dict.reserve("exe");
-		dict.reserve("show");
-		dict.reserve("ls");
-		dict.reserve("readme");
-		dict.reserve("states");
-		dict.reserve("clear");
-	}
-
-	@Override
-	public Node expr2() {
-		Node n = exprI2();
-		while(nextToken.type==TokenID.And) {
-			nextToken();
-			n = logicNodeFactory.andNode(n, exprI2()) ;
-		}
-		return n;
-	}
-
-	@Override
-	public Node expr3() {
-		if (nextToken.type == TokenID.Next) {
-			nextToken();
-			return logicNodeFactory.nextNode(expr3());
-		}
-		Node n = super.expr3();
-		while(nextToken.type==TokenID.Question) {
-			nextToken();
-			Node cond = n;
-			Node high = expr3();
-			if (nextToken.type!=TokenID.Colon) {
-				error(": expected");
-				return logicNodeFactory.trueNode();
-			}
-			nextToken();
-			Node low = expr3();
-			n = logicNodeFactory.orNode(
-					logicNodeFactory.andNode(cond, high),
-					logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low));
-		}
-		return n;
-	}
-
-	
-	@Override
-	public Node term() {
-		if (nextToken.type==TokenID.BParen) {
-			Node predicate = periodNode;
-			nextToken();
-			LinkedList<Node> arg = arguments();
-			return logicNodeFactory.predicateNode(predicate, arg);
-		}
-		return super.term();
-	}
-	
-	public Node exprI2() {
-		Node n = exprM1();
-		while(nextToken.type == TokenID.Chop) {
-			nextToken();
-			n = logicNodeFactory.chopNode(n, exprM1());
-		}
-		return n;
-	}
-
-
-	@Override
-	protected LinkedList<Node> arguments() {
-		Node n;
-		LinkedList<Node> arg = new LinkedList<Node>();
-		while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) {
-			if (nextToken.type==TokenID.NULL) break;
-			n = exprI2();
-			arg.add(n);
-			if (nextToken.type == TokenID.And)
-				nextToken();
-		}
-		if (nextToken.type==TokenID.CloseParen||
-				nextToken.type==TokenID.CloseBParen) nextToken();
-		else {
-			scanner.error(") expected");
-		}
-		return arg;
-	}
-	
-	public Node emptyNode() {
-		return emptyNode;
-	}
-
-	public void addHelp(String string) {
-		help += string;
-	}
-	
-	public void help() {
-		System.out.println(help);
-	}
-
-
-
-}
--- a/src/lite/ITLNodeScanner.java	Sun Jan 20 01:53:55 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-package lite;
-
-
-import parser.Dictionary;
-import parser.LogicNodeScanner;
-import verifier.LogicSolver;
-
-public class ITLNodeScanner<Node extends LogicSolver> extends LogicNodeScanner<Node> {
-
-
-	public ITLNodeScanner(Dictionary<Node> dict) {
-		super(dict);
-	}
-	
-
-}
--- a/src/lite/ITLNodeScannerTest.java	Sun Jan 20 01:53:55 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-package lite;
-
-import java.io.FileNotFoundException;
-import java.io.FileReader;
-
-import parser.*;
-
-
-public class ITLNodeScannerTest extends LogicNodeScannerTest {
-
-	public static ITLNodeScanner<ITLSolver> scan;
-
-	public static void initScanner() {
-		Dictionary<ITLSolver> dict = new Dictionary<ITLSolver>();
-		scan = new ITLNodeScanner<ITLSolver>(dict);
-	}
-
-
-	public static void scan(String exp) {
-		for(Token<ITLSolver> t : scan.scanToken(exp)) {
-			System.out.print(t+" ");
-		}
-		System.out.println();
-	}
-	
-	public static void scan(FileReader file) {
-		for(Token<ITLSolver> t : scan.scanToken(file)) {
-			System.out.print(t+" ");
-			System.out.println();
-		}
-	}
-	
-
-	public static void main(String arg[]) {
-		initScanner();
-		if (arg.length==0) {
-			arg = new String[1];
-			arg[0] = "test";
-		}
-		for(String file: arg) {
-			try {
-				scan(new FileReader(file));
-			} catch (FileNotFoundException e) {
-				scan(file);
-			}
-		}
-	}
-}
--- a/src/lite/ITLSatisfier.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Sun Jan 20 18:22:55 2008 +0900
@@ -3,8 +3,6 @@
 
 import sbdd.SBDDFactory;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
-import verifier.ChoicePointList;
 
 public class ITLSatisfier implements Next {
 
@@ -38,7 +36,7 @@
 
 	public ITLSolver satisfiable(ITLSolver n) {
 		try {
-			return n.sat(this, new Continuation(this,null,this));
+			return n.sat(this, this);
 		} catch (Backtrack e) {
 			// no more choice
 			return null; // unsatisfiable
@@ -46,22 +44,18 @@
 	}
 	
 	public void develop(ITLSolver n, Next next) {
+//		try {
+//			n.sat(this,new Continuation(this,null,next));
+//		} catch (Backtrack e) {
+//			return; // all end
+//		}
 		try {
-			n.sat(this,new Continuation(this,null,next));
+			n.sat(this,next);
 		} catch (Backtrack e) {
 			return; // all end
 		}
 	}
 
-	public ITLSolver next(ITLSatisfier sat, 
-			Continuation next, ITLSolver value) throws Backtrack {
-		if (value==null) {
-			// try other choice on 
-			throw backtrack;
-		}
-		return value;  // satisfiable
-	}
-
 	public ITLSolver true_() {
 		return true_;
 	}
@@ -71,6 +65,14 @@
 		return cp;
 	}
 
+	public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+		if (value==null) {
+			// try other choice on 
+			throw backtrack;
+		}
+		return value;  // satisfiable
+	}
+
 
 
 }
--- a/src/lite/ITLSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ITLSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,31 +2,24 @@
 
 import java.util.LinkedList;
 
+
 import sbdd.BDDInterface;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
-import verifier.LogicSolver;
 
-public class ITLSolver extends LogicSolver 
-	implements Next,BDDInterface {
+public abstract class ITLSolver
+	implements BDDInterface {
 	
 	public int hash=-1;     // hash value cache
 	public int order=-1;    // BDD variable order for this subterm
-	
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		return null;
-	}
+	public boolean value;
+
+	public abstract ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack ;
+
 
 	@Override
 	public String toString() {
 		return null;
 	}
-
-	public ITLSolver next(ITLSatisfier sat, lite.Continuation next, ITLSolver value) throws Backtrack {
-		return null;
-	}
-
-
 	public void setValue(boolean solver) {
 		
 	}
@@ -63,5 +56,12 @@
 		return value;
 	}
 
+	public int order() {
+		return order;
+	}
+
+	public boolean isxfy() {
+		return order%2==1;
+	}
 	
 }
--- a/src/lite/ITLSolverTest.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ITLSolverTest.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,6 +1,8 @@
 package lite;
 
-import verifier.Backtrack;
+import parser.ITLNodeParser;
+import parser.ITLNodeScanner;
+
 
 public class ITLSolverTest {
 
@@ -76,7 +78,8 @@
 	}
 	
 	class Print implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			System.out.println(" "+sat.choicePoint()+" -> "+value);
 			throw sat.backtrack;
 		}
--- a/src/lite/MacroSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/MacroSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -6,7 +6,6 @@
 import parser.MacroNodeParserInterface;
 
 
-import verifier.Backtrack;
 
 public class MacroSolver extends ITLSolver {
 
@@ -27,11 +26,6 @@
 	}
 
 
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		// TODO Auto-generated method stub
-		return null;
-	}
 
 	@Override
 	public String toString() {
@@ -68,4 +62,9 @@
 		return order;
 	}
 
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return null;
+	}
+
 }
--- a/src/lite/Next.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/Next.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,9 +1,9 @@
 package lite;
 
-import verifier.Backtrack;
+
 
 public interface Next {
 
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack;
+	public ITLSolver next(ITLSatisfier sat,ITLSolver value) throws Backtrack;
 
 }
--- a/src/lite/NextSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/NextSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class NextSolver extends ITLSolver {
 
@@ -15,19 +14,6 @@
 		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(sat.true_); 
-	}
-
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
 		return sf.nextNode(node.toSBDD(sf)).toSBDD(sf);
 	}
@@ -49,4 +35,20 @@
 		}
 		return false;
 	}
+
+	class NextSolver1 implements Next {
+		Next next;
+		NextSolver1(Next next) { this.next = next; }
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) {
+				return next.next(sat,node); // not empty case
+			} else
+				return next.next(sat,sat.true_); 
+		}
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return sat.empty.sat(sat, new NextSolver1(next));
+	}
 }
--- a/src/lite/NotSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/NotSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,7 +1,6 @@
 package lite;
 
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 
 
@@ -18,22 +17,25 @@
 	public String toString() {
 		return "(not "+node+")";
 	}
-
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-
-		return node.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(sat.true_);
-		else if (value==sat.true_) return next.sat(null);
-		return next.sat(sat.lf.notNode(value));
-	}
-
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
 		return node.toSBDD(sf).not(sf).toSBDD(sf);
 	}
 
+
+	class NotSolver1 implements Next {
+		Next next;
+		NotSolver1(Next next) { this.next = next; }
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) return next.next(sat,sat.true_);
+			else if (value==sat.true_) return next.next(sat,null);
+			return next.next(sat,sat.lf.notNode(value));
+		}
+	}
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return node.sat(sat, new NotSolver1(next));
+	}
+
 }
--- a/src/lite/NumberSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/NumberSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,6 +1,8 @@
 package lite;
 
 
+
+
 public class NumberSolver extends ITLSolver {
 
 	int num;
@@ -13,4 +15,9 @@
 		return Integer.toString(num);
 	}
 
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return null;
+	}
+
 }
--- a/src/lite/OrSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/OrSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,12 +1,12 @@
 package lite;
 
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class OrSolver extends ITLSolver {
 
 	ITLSolver left;
 	ITLSolver right;
+
 	public OrSolver(ITLSolver left, ITLSolver right) {
 		this.left = left;
 		this.right = right;
@@ -17,38 +17,20 @@
 	}
 
 
-
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-
-		return left.sat(sat, new Continuation(sat,next,this));
-	}
-
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value==null) {
-			return right.sat(sat, next);
-		} else if (value==sat.true_) {
-			return next.sat(value);
-		} else {
-			return right.sat(sat, new Continuation(sat,next,
-					new OrSolver2(value)));
-		}
-	}
-
 	class OrSolver2 implements Next {
+		Next next;
 		ITLSolver residue;
-		public OrSolver2(ITLSolver value) {
-			residue = value;
+		public OrSolver2(Next next,ITLSolver value) {
+			residue = value; this.next = next;
 		}
 
-		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {
-				return next.sat(residue);
+				return next.next(sat,residue);
 			} else if (value==sat.true_) {
-				return next.sat(value);
+				return next.next(sat,value);
 			} else {
-				return next.sat(sat.lf.orNode(residue,value));
+				return next.next(sat,sat.lf.orNode(residue,value));
 			}
 		}
 	}
@@ -56,4 +38,28 @@
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
 		return left.toSBDD(sf).or(sf, right.toSBDD(sf)).toSBDD(sf);
 	}
+
+
+	class OrSolver1 implements Next {
+		Next next;
+
+		public OrSolver1(Next next) {
+			this.next = next;
+		}
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value==null) {
+				return right.sat(sat, next);
+			} else if (value==sat.true_) {
+				return next.next(sat,value);
+			} else {
+				return right.sat(sat, new OrSolver2(next,value));
+			}
+		}
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return left.sat(sat, new OrSolver1(next));
+	}
 }
--- a/src/lite/PredicateSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/PredicateSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,6 +2,9 @@
 
 import java.util.LinkedList;
 
+
+
+
 public class PredicateSolver extends ITLSolver {
 
 	private LinkedList<ITLSolver> arg;
@@ -27,5 +30,11 @@
 		return predicate;
 	}
 
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
 
 }
--- a/src/lite/ProjectionSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/ProjectionSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class ProjectionSolver extends ITLSolver {
 
@@ -46,43 +45,40 @@
 	public String toString() {
 		return "proj("+clock+","+interval+")";
 	}
+	class ProjectionSolver2 implements Next {
 
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		// try empty case
-		return sat.empty.sat(sat, new Continuation(sat,next,this));
-	}
+		private Next next;
 
-	@Override
-	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-		if (value!=null) { // empty case, only check interval
-			return interval.sat(sat, next);
-		} else {
-			// execute 1 clock on clock and interval. Try clock first.
-			return clock.sat(sat, new Continuation(sat,next, new ProjectionSolver2()));
+		public ProjectionSolver2(Next next) {
+			this.next = next;
 		}
-	}
 
-	class ProjectionSolver2 implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {
 				// clock is falied, return null
-				return next.sat(value);
+				return next.next(sat,value);
 			} else {
 				// try interval keeping @clock
 				clock1 = value;
-				return interval.sat(sat, new Continuation(sat,next, new ProjectionSolver3()));
+				return interval.sat(sat, new ProjectionSolver3(next));
 			}
 		}
 	}
 	
 	class ProjectionSolver3 implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		private Next next;
+
+		public ProjectionSolver3(Next next) {
+			this.next = next;
+		}
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value==null) {  // interval is failed, return null
-				return next.sat(value);
+				return next.next(sat,value);
 			} else {
 				// return    @clock & proj(clock,@interval)
 				ITLSolver projection1 =sat.lf.projectionNode(clock,value);
-				return next.sat(sat.lf.chopNode(clock1,projection1));
+				return next.next(sat,sat.lf.chopNode(clock1,projection1));
 			}
 		}
 	}
@@ -108,4 +104,28 @@
 		}
 		return false;
 	}
+
+
+	class ProjectionSolver1 implements Next {
+		private Next next;
+
+		public ProjectionSolver1(Next next) {
+			this.next = next;
+		}
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
+			if (value!=null) { // empty case, only check interval
+				return interval.sat(sat, next);
+			} else {
+				// execute 1 clock on clock and interval. Try clock first.
+				return clock.sat(sat, new ProjectionSolver2(next));
+			}
+		}
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		// try empty case
+		return sat.empty.sat(sat, new ProjectionSolver1(next));
+	}
 }
--- a/src/lite/TrueSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/TrueSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,7 +2,6 @@
 
 import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class TrueSolver extends ITLSolver {
 
@@ -10,10 +9,6 @@
 		order = TokenID.True.hash;
 	}
 
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		return next.sat(sat.true_);
-	}
 	
 	public String toString() {
 		return "true";
@@ -35,4 +30,10 @@
 	public boolean equals(Object o) {
 		return o==this;
 	}
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		return next.next(sat,sat.true_);
+	}
 }
--- a/src/lite/VariableSolver.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/lite/VariableSolver.java	Sun Jan 20 18:22:55 2008 +0900
@@ -1,7 +1,6 @@
 package lite;
 
 import sbdd.SBDDFactoryInterface;
-import verifier.Backtrack;
 
 public class VariableSolver extends ITLSolver {
 		
@@ -21,30 +20,6 @@
 		return name;
 	}
 	
-	@Override
-	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		if (sat.cp.hasChoicePoint(this)) {
-			// choice point is already made, use it
-			return next.sat(value?sat.true_:null);
-		}
-		sat.cp.addChoicePoint(this);
-		value = true; // the first choice
-		try {
-			return next.sat(sat.true_);
-		} catch (Backtrack e) {
-			value = false; // the second choice
-			try {
-				return next.sat(null);
-			} catch (Backtrack e1) {
-				// no more choices, remove this choice and 
-				// request backtrack to the previous choice or
-				// top level terminator
-				sat.cp.deleteChoicePoint(this);
-				throw e1;
-			}
-		}
-	}
-	
 
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
 		return sf.bddNode(this, sf.trueNode(), sf.falseNode()).toSBDD(sf);
@@ -68,5 +43,30 @@
 		}
 		return false;
 	}
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
+		if (sat.cp.hasChoicePoint(this)) {
+			// choice point is already made, use it
+			return next.next(sat,value?sat.true_:null);
+		}
+		sat.cp.addChoicePoint(this);
+		value = true; // the first choice
+		try {
+			return next.next(sat,sat.true_);
+		} catch (Backtrack e) {
+			value = false; // the second choice
+			try {
+				return next.next(sat,null);
+			} catch (Backtrack e1) {
+				// no more choices, remove this choice and 
+				// request backtrack to the previous choice or
+				// top level terminator
+				sat.cp.deleteChoicePoint(this);
+				throw e1;
+			}
+		}
+	}
 	
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/ITLCommander.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,155 @@
+package parser;
+
+import java.util.LinkedList;
+import java.util.TreeMap;
+
+import lite.ITLNodeFactoryInterface;
+import lite.ITLSolver;
+import lite.NumberSolver;
+
+
+import sbdd.BDDDiagnosis;
+import sbdd.BDDSatisfier;
+import sbdd.SBDDEntry;
+
+public class ITLCommander<Node extends ITLSolver> implements Command<Node> {
+
+
+	private ITLNodeFactoryInterface<Node> lf;
+	private ITLNodeParser parser;
+	public BDDSatisfier sat;
+	private TreeMap<Integer,Node> examples;
+	private BDDDiagnosis diag;
+
+	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser parser) {
+		this.lf = lf;
+		this.parser = parser;
+		this.examples = new TreeMap<Integer,Node>();
+		
+		parser.addHelp(
+			"do(p).                     verify formula p or a numberd example, try do(10).\n"+
+			"ex(N,p).                   register numbered examle p\n"+
+			"ls.                        list predefined example\n"+
+			"verbose(TF).               set verbose mode (true/false)\n"+
+			"include(File).             read from File\n"+
+			"def('head(p)','body(p)').  define macro\n"+
+			"exe.                       execute last verifed formula\n"+
+			"diag.                      counter example of last verifed formula\n"+
+			"clear.                     clear state database\n"+
+			"show.                      show state statistics\n"+
+			"readme.                    show README\n"+
+			"help.                      show this\n"+
+			""
+				);
+	}
+
+	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
+		
+		// All names used here have to be reserved. Otherwise, parser generated name becomes 
+		// different string at run time, as a result, name=="less" will fail even if name contains "less". 
+		// If we reseve it, paredicateNode.varaibleNode.name contains pregenerated String which is 
+		// equivalent to used here. Of course name.equal("less") works fine, but it is time consuming. 
+		// Although it is practically allowed but I cannot accept.
+		
+		// We can also define Command as internal interface class in ITLNodeParser. In this case
+		// reserve operation is not required, like "length" macro.
+
+		String name = predicate.toString();
+		
+		if (name=="less") {
+			Node n = lf.falseNode();
+			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();
+			if (args.size()<1) {
+				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
+				return lf.trueNode();
+			}
+			int index = atoi(args);
+			if (args.size()==1) {
+				Node n = args.get(0);
+				if (index>=0) {
+					// do(10) case
+					n = examples.get(index);
+					if (n==null) {
+						parser.error("Unknown registered example");
+						return lf.trueNode();
+					}
+				}
+				System.out.println(n);
+				sat.verify(n);
+			} else if (args.size()==2 && index>=0){
+				examples.put(index, args.get(1));
+			}
+		} else if (name == "ls") {
+			// this is not human readable...
+			//for(int i:examples.keySet()) {
+			// System.out.println(i+":"+examples.get(i));
+			//}
+			parser.showResourceFile("data/example");
+		} else if (name == "readme") {
+			parser.showResourceFile("data/README");
+		} else if (name == "help") {
+			parser.help();
+		} else if (name == "def") {
+			parser.define(args.get(0).toString(),args.get(1).toString());
+		} else if (name == "verbose") {
+			// verbose(true) / verbose(off)
+			checkSat();
+			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 = atoi(args);
+			checkSat();
+			diag.execute(sat.last, length );
+		} else if (name == "diag") {
+			int length = 0;
+			if (args.size()>1) length = atoi(args);
+			checkSat();
+			diag.counterExample(sat.last, length);
+		} else if (name == "clear") {
+			sat = null;
+			checkSat();
+		} else if (name == "states") {
+			// 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);
+		} else
+			parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
+		return lf.trueNode();
+	}
+
+	private int atoi(LinkedList<Node> args) {
+		// should have more strcit check..
+		int i=-1;
+		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();
+			diag = new BDDDiagnosis(sat);
+		}
+	}
+
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/ITLNodeParser.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,261 @@
+package parser;
+
+import java.util.LinkedList;
+
+import lite.ITLNodeFactoryInterface;
+import lite.ITLSolver;
+
+
+
+public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> {
+
+	public ITLNodeFactoryInterface<Node> logicNodeFactory;
+	public ITLNodeScanner<Node> scanner;
+	public ITLCommander<Node> parseCommand;
+	public Node emptyNode;
+	private Node periodNode;
+	public String help = "";
+	
+	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
+
+		super(lf);
+		logicNodeFactory = lf;
+		initialize();
+
+		Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty);
+		emptyNode = emptyToken.value = logicNodeFactory.emptyNode();
+		
+		parseCommand = new ITLCommander<Node>(lf,this);
+		
+			define("not(P)","~P");                               // not
+			define("P->Q","(not(P);Q))",101);                         // imply
+			define("P<->Q","((not(P);Q),(P; not(Q)))");            // equiv
+			define("P=Q","((not(P);Q),(P; not(Q)))");              // equiv 
+			// P&&Q have to be left associative ( xfy i.e. a&&b&&c = a&&(b&&c)
+			// odd order means xfy associativity. & is right associative (yfx) in this
+			// parser, but & has associative, so it is alright. (&& is not assosicative)
+			define("P && Q","((not(empty),P) & Q))",901);             // strong chop
+			define("'<>'(Q)","(true & Q))");                        // sometime
+			define("'#'(Q)"," not(true & not(Q)))");                // always
+			define("'[]'(Q)"," not(true & not(Q)))");               // always
+			define("'[a]'(Q)"," not(true & not(Q) & true))");       // always with arbitary fin
+			define("'<a>'(Q)"," (true & Q & true))");       // sometime with arbitary fin
+			define("fin(Q)","(true & (empty,Q)))");                 // final state in the interval
+			define("keep(Q)"," not(true & not((empty ; Q))))");     // except final state
+			define("halt(Q)"," '[]'(empty=Q))");    
+			define("more"," not(empty))");                          // non empty interval
+// discrete stuff
+			define("skip"," @(empty))");                            // 1 length interval
+			define("infinite"," (true & false))");                  // 
+			define("finite"," ~((true & false)))");                 // 
+			// define("length(I)", "true",50,command);            // length operator
+			define("length(I)", "empty",50,                          // length operator
+					new Command<Node>() {
+						public Node exec(Node predicate, Node value, LinkedList<Node> args) {
+	                        Node n = value;
+	                        int length = Integer.parseInt(args.get(0).toString());
+	                        for(int i =0;i<length;i++) {
+	                            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("@(P)","(~empty, next(P)))");
+// temporal assignments
+			define("gets(A,B)","keep(@A<->B))");
+			define("stable(A)","keep(@A<->A))");
+			// define("state(A)","(share(A),'[]'(L))):- def_state(A,L)");
+// def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R))))");
+//   easier one
+            define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))");
+// def(P<=Q,Q=>P)");
+// loop stuff and quantifiers
+			define("*(A) ","proj(A,true),fin(A)");  // weak closure
+			// define("+(A) ","A& *(empty;A)");   // strong closure (difficult one)
+			define("+(A) ","A & proj(A,true)");   // strong closure
+			define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
+			define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
+			define("all(P,Q)","not(exists(P,not(Q)))");
+			define("local(P)"," (P = (P&true))");
+// test predicates
+//			define("trace(X,List),L) :- !,make_trace(List,X,L)");
+			define("even(P)","exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P)))))");
+			define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))"); 
+			define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");
+
+			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);
+			
+			define("ex0(N,Exp)","skipped");
+			define("verbose(I)", "true",50,parseCommand);                    
+			
+			define("^(r)","r"); // interval variable (we cannot handle now)
+			
+			periodNode = logicNodeFactory.variableNode(".", true);
+			define("help","true",50,parseCommand);
+			define("show","true",50,parseCommand);
+			define("states","true",50,parseCommand);
+			define("ls","true",50,parseCommand);
+			define("readme","true",50,parseCommand);
+			define("clear","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>() {
+				@SuppressWarnings("unchecked")
+				public Node exec(Node predicate, Node value, LinkedList<Node> args) {
+					Node allElse = logicNodeFactory.trueNode();
+					Node allFalse = allElse;
+					Node falseNode = value= logicNodeFactory.falseNode();
+					LinkedList<? extends ITLSolver> list = args.get(0).arguments();
+					if (list==null) {
+						error("sahre: missing [] argument");
+						return value;
+					}
+					if (list.isEmpty()) return value;
+					for(ITLSolver n:  list) {
+						Node n1 = (Node)n;
+						value = logicNodeFactory.bddNode(n1, allElse, value);
+						allElse = logicNodeFactory.bddNode(n1,falseNode,allElse); 
+						allFalse = logicNodeFactory.andNode(
+								logicNodeFactory.notNode(n1), allFalse);
+					}
+					//return value;
+					return logicNodeFactory.orNode(value,allFalse);
+				}
+			});
+
+	}
+
+	public ITLNodeParser() {
+		super();
+	}
+	
+
+	@Override
+	public void initialize() {
+		dict = new Dictionary<Node>();
+		scope = new LogicNodeScope<Node>(null,dict);
+		initReservedWord();
+		scanner = new ITLNodeScanner<Node>(dict);
+		super.scanner = scanner;
+
+		dict.reserve("&",TokenID.Chop);
+		dict.reserve("next",TokenID.Next);
+		dict.reserve("proj",TokenID.Projection);
+		
+		// parseCommand requires compile tme reserved word for string comparison
+		dict.reserve("less");
+		dict.reserve("ex");
+		dict.reserve("do");
+		dict.reserve("include");
+		dict.reserve("def");
+		dict.reserve("verbose");
+		dict.reserve("help");
+		dict.reserve("diag");
+		dict.reserve("exe");
+		dict.reserve("show");
+		dict.reserve("ls");
+		dict.reserve("readme");
+		dict.reserve("states");
+		dict.reserve("clear");
+	}
+
+	@Override
+	public Node expr2() {
+		Node n = exprI2();
+		while(nextToken.type==TokenID.And) {
+			nextToken();
+			n = logicNodeFactory.andNode(n, exprI2()) ;
+		}
+		return n;
+	}
+
+	@Override
+	public Node expr3() {
+		if (nextToken.type == TokenID.Next) {
+			nextToken();
+			return logicNodeFactory.nextNode(expr3());
+		}
+		Node n = super.expr3();
+		while(nextToken.type==TokenID.Question) {
+			nextToken();
+			Node cond = n;
+			Node high = expr3();
+			if (nextToken.type!=TokenID.Colon) {
+				error(": expected");
+				return logicNodeFactory.trueNode();
+			}
+			nextToken();
+			Node low = expr3();
+			n = logicNodeFactory.orNode(
+					logicNodeFactory.andNode(cond, high),
+					logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low));
+		}
+		return n;
+	}
+
+	
+	@Override
+	public Node term() {
+		if (nextToken.type==TokenID.BParen) {
+			Node predicate = periodNode;
+			nextToken();
+			LinkedList<Node> arg = arguments();
+			return logicNodeFactory.predicateNode(predicate, arg);
+		}
+		return super.term();
+	}
+	
+	public Node exprI2() {
+		Node n = exprM1();
+		while(nextToken.type == TokenID.Chop) {
+			nextToken();
+			n = logicNodeFactory.chopNode(n, exprM1());
+		}
+		return n;
+	}
+
+
+	@Override
+	protected LinkedList<Node> arguments() {
+		Node n;
+		LinkedList<Node> arg = new LinkedList<Node>();
+		while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) {
+			if (nextToken.type==TokenID.NULL) break;
+			n = exprI2();
+			arg.add(n);
+			if (nextToken.type == TokenID.And)
+				nextToken();
+		}
+		if (nextToken.type==TokenID.CloseParen||
+				nextToken.type==TokenID.CloseBParen) nextToken();
+		else {
+			scanner.error(") expected");
+		}
+		return arg;
+	}
+	
+	public Node emptyNode() {
+		return emptyNode;
+	}
+
+	public void addHelp(String string) {
+		help += string;
+	}
+	
+	public void help() {
+		System.out.println(help);
+	}
+
+
+
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/ITLNodeScanner.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,14 @@
+package parser;
+
+
+import lite.ITLSolver;
+
+public class ITLNodeScanner<Node extends ITLSolver> extends LogicNodeScanner<Node> {
+
+
+	public ITLNodeScanner(Dictionary<Node> dict) {
+		super(dict);
+	}
+	
+
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/ITLNodeScannerTest.java	Sun Jan 20 18:22:55 2008 +0900
@@ -0,0 +1,47 @@
+package parser;
+
+import java.io.FileNotFoundException;
+import java.io.FileReader;
+
+import lite.ITLSolver;
+
+public class ITLNodeScannerTest extends LogicNodeScannerTest {
+
+	public static ITLNodeScanner<ITLSolver> scan;
+
+	public static void initScanner() {
+		Dictionary<ITLSolver> dict = new Dictionary<ITLSolver>();
+		scan = new ITLNodeScanner<ITLSolver>(dict);
+	}
+
+
+	public static void scan(String exp) {
+		for(Token<ITLSolver> t : scan.scanToken(exp)) {
+			System.out.print(t+" ");
+		}
+		System.out.println();
+	}
+	
+	public static void scan(FileReader file) {
+		for(Token<ITLSolver> t : scan.scanToken(file)) {
+			System.out.print(t+" ");
+			System.out.println();
+		}
+	}
+	
+
+	public static void main(String arg[]) {
+		initScanner();
+		if (arg.length==0) {
+			arg = new String[1];
+			arg[0] = "test";
+		}
+		for(String file: arg) {
+			try {
+				scan(new FileReader(file));
+			} catch (FileNotFoundException e) {
+				scan(file);
+			}
+		}
+	}
+}
--- a/src/parser/LogicNodeParser.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/parser/LogicNodeParser.java	Sun Jan 20 18:22:55 2008 +0900
@@ -7,9 +7,10 @@
 import java.net.URL;
 import java.util.LinkedList;
 
-import verifier.LogicSolver;
+import lite.ITLSolver;
 
-public class LogicNodeParser<Node extends LogicSolver> {
+
+public class LogicNodeParser<Node extends ITLSolver> {
 
 	/*
 	 * Simple Logic Node Parser
--- a/src/parser/MacroNodeParser.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/parser/MacroNodeParser.java	Sun Jan 20 18:22:55 2008 +0900
@@ -2,10 +2,10 @@
 
 import java.util.LinkedList;
 
-import verifier.LogicSolver;
+import lite.ITLSolver;
 
 
-public class MacroNodeParser<Node extends LogicSolver>
+public class MacroNodeParser<Node extends ITLSolver>
      extends LogicNodeParser<Node> 
 	 implements MacroNodeParserInterface<Node> {
 
@@ -202,7 +202,7 @@
 		Node n = logicNodeFactory.macroNode(m, body, order, command, this);
 
 		Token<Node> t;
-		LogicSolver p = m.predicate();
+		ITLSolver p = m.predicate();
 		if (p!=null && (t = dict.get(p.toString()))!=null) {
 			t.setMacro(n);
 		} else {
--- a/src/sbdd/BDDSatisfier.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Sun Jan 20 18:22:55 2008 +0900
@@ -4,15 +4,14 @@
 import java.util.LinkedList;
 
 import parser.ExecutorInterface;
+import parser.ITLNodeParser;
 
-import verifier.Backtrack;
-import verifier.ChoicePointList;
 
 
 import lite.BDDSolver;
-import lite.Continuation;
+import lite.Backtrack;
+import lite.ChoicePointList;
 import lite.ITLNodeFactory;
-import lite.ITLNodeParser;
 import lite.ITLSatisfier;
 import lite.ITLSolver;
 import lite.Next;
@@ -74,7 +73,8 @@
 	}
 	
 	class Print implements Next {
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			System.out.println("  "+sat.choicePoint()+" -> "+value);
 			throw sat.backtrack;
 		}
@@ -91,7 +91,7 @@
 
 	class AllNext implements Next {
 
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			edge++;
 			if (value!=null) {
 				if (value==true_) satisfiable = true;
@@ -113,7 +113,7 @@
 
 	class AllNextVerbose implements Next {
 
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			String s = "null";
 			System.out.print(" "+sat.choicePoint()+" -> ");
 			edge++;
@@ -161,7 +161,12 @@
 			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
 			currentState = e; falsifiable=false; satisfiable = false;
 			cp.clear();                           // all choice point is searched and removed
-			develop(e.key, allNext);
+			//develop(e.key, allNext);
+			try {
+				e.key.sat(this, allNext);
+			} catch (Backtrack e1) {
+				// all end
+			}
 			// this flag is work on current state
 			// to check validity/unsatisfiability, full check is required.
 			e.falsifiable = falsifiable; e.satisfiable = satisfiable;
@@ -188,7 +193,8 @@
 		public FindOne(SBDDEntry next) {
 			this.dest = next;
 		}
-		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+		
+		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
 			if (value!=null && state.getEntry(value)==dest) {
 				cp = sat.cp; return null;
 			}
--- a/src/sbdd/SBDDTest.java	Sun Jan 20 01:53:55 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Sun Jan 20 18:22:55 2008 +0900
@@ -5,8 +5,9 @@
 import java.io.InputStream;
 import java.net.URL;
 
+import parser.ITLNodeParser;
+
 import lite.BDDSolver;
-import lite.ITLNodeParser;
 import lite.ITLSolver;
 
 public class SBDDTest {