--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/AndSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,39 @@
+package lite;
+
+import verifier.Backtrack;
+
+
+public class AndSolver extends ITLSolver {
+
+	ITLSolver left;
+	ITLSolver right;
+	
+	public AndSolver(ITLSolver _left,ITLSolver _right) {
+		left = _left;
+		right = _right;
+	}
+	public boolean value() {
+		return left.value() && right.value();
+	}
+	
+	public String toString() {
+		return "("+left+" and "+right+")";
+	}
+
+
+	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 {
+			return next.sat(null);
+		}
+	}
+
+	
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/Continuation.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,21 @@
+package lite;
+
+import verifier.Backtrack;
+
+public class Continuation {
+
+	public ITLSatisfier sat;
+	public Continuation next;
+	public ITLSolver solver;
+	
+		public Continuation(ITLSatisfier sat, Continuation next, ITLSolver 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);
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ExistsSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,43 @@
+package lite;
+
+import verifier.Backtrack;
+
+public class ExistsSolver extends ITLSolver {
+
+	ITLSolver node;
+	ITLSolver var;
+
+	public ExistsSolver(ITLSolver var, ITLSolver node) {
+		this.node = node;
+		this.var = var;
+	}
+	
+	public boolean value() {
+		boolean v;
+		var.setValue(this);
+		v = node.value();
+		if (v) return v;
+		var.setValue(null);
+		return node.value();
+	}
+	
+	public String toString() {
+		return "exists("+var+","+node+")";
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		var.setValue(this);
+		return node.sat(sat, new Continuation(sat,next,this));
+	}
+
+	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		if (value == null) {
+			var.setValue(null);
+			return node.sat(sat, next);
+		} else {
+			return next.sat(sat.true_());
+		}
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/FalseSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,18 @@
+package lite;
+
+import verifier.Backtrack;
+
+public class FalseSolver extends ITLSolver {
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		return next.sat(null);
+	}
+	
+	public boolean value() { return false; }
+
+	public String toString() {
+		return "false";
+	}
+
+}

--- a/src/lite/ITLSatisfier.java	Wed Dec 26 12:29:31 2007 +0900
+++ b/src/lite/ITLSatisfier.java	Wed Dec 26 16:09:16 2007 +0900
@@ -9,6 +9,8 @@
 
 public class ITLSatisfier implements ChoicePointList<ITLSolver>, Next {
 
+	static public final ITLSolver true_ = new TrueSolver();
+	
 	public ITLSatisfier(ITLSolver true_) {
 		// TODO Auto-generated constructor stub
 	}
@@ -37,4 +39,8 @@
 		// TODO Auto-generated method stub
 		return null;
 	}
+
+	public ITLSolver true_() {
+		return true_;
+	}
 }

--- a/src/lite/ITLSolver.java	Wed Dec 26 12:29:31 2007 +0900
+++ b/src/lite/ITLSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -1,14 +1,13 @@
 package lite;
 
+import java.util.LinkedList;
+
 import verifier.Backtrack;
-import verifier.Continuation;
-import verifier.LogicSolver;
-import verifier.Satisfier;
+
+public class ITLSolver implements Next {
 
-public class ITLSolver extends LogicSolver {
 
-	@Override
-	public ITLSolver sat(Satisfier sat, Continuation next) throws Backtrack {
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		// TODO Auto-generated method stub
 		return null;
 	}
@@ -19,10 +18,30 @@
 		return null;
 	}
 
-	@Override
+	public ITLSolver next(ITLSatisfier sat, lite.Continuation next, ITLSolver value) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
 	public boolean value() {
-		// TODO Auto-generated method stub
 		return false;
 	}
 
+	public void setValue(ITLSolver solver) {
+		
+	}
+
+	public boolean isMacro() {
+		return false;
+	}
+	
+
+	public LinkedList<ITLSolver> arguments() {
+		return null;
+	}
+
+	public ITLSolver eval(LinkedList<ITLSolver> args) {
+		return this;
+	}
+
 }

--- a/src/lite/ITLSolverTest.java	Wed Dec 26 12:29:31 2007 +0900
+++ b/src/lite/ITLSolverTest.java	Wed Dec 26 16:09:16 2007 +0900
@@ -11,6 +11,16 @@
 		true_= lf.trueNode();
 		
 		p = new ITLNodeParser<ITLSolver>(lf);
+		
+		System.out.println(p.parse("p & q"));
+		System.out.println(p.parse("p & @q"));
+		System.out.println(p.parse("<>(p)"));
+		System.out.println(p.parse("[](p)"));
+		System.out.println(p.parse("empty & q"));
+		System.out.println(p.parse("fin(p)=[](<>(p))"));
+		System.out.println(p.parse("length(3)"));
+		System.out.println(p.parse("[](more)"));
+
 		sat("false");
 		sat("true");
 	}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/MacroSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,59 @@
+package lite;
+
+import java.util.LinkedList;
+
+import verifier.Backtrack;
+
+public class MacroSolver extends ITLSolver {
+
+
+	private ITLSolver predicate;
+	private String body;
+	private ITLNodeParser<ITLSolver> parser;
+
+
+	public MacroSolver(ITLSolver macro, String body, ITLNodeParser<ITLSolver> parser) {
+		this.predicate = macro;
+		this.body = body;
+		this.parser = parser;
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public String toString() {
+		return predicate.toString();
+	}
+
+	@Override
+	public boolean value() {
+		// TODO Auto-generated method stub
+		return false;
+	}
+	
+
+	@Override
+	public boolean isMacro() {
+		return true;
+	}
+	
+	@Override
+	public LinkedList<ITLSolver> arguments() {
+		return predicate.arguments();
+	}
+
+	/* 
+	 * Macro Expansion
+	 *      locally define parameters by given arguments
+	 */
+	@Override
+	public ITLSolver eval(LinkedList<ITLSolver> args) {
+		return parser.eval(args, predicate, body,predicate.arguments()); 
+	}
+	
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/Next.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,9 @@
+package lite;
+
+import verifier.Backtrack;
+
+public interface Next {
+
+	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack;
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/NotSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,35 @@
+package lite;
+
+import verifier.Backtrack;
+
+
+
+
+public class NotSolver extends ITLSolver {
+
+	ITLSolver node;
+
+	public NotSolver(ITLSolver node) {
+		this.node = node;
+	}
+
+	public boolean value() {
+		return ! node.value() ;
+	}
+
+	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 {
+		return next.sat(value==null?ITLSatisfier.true_:null);
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/OrSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,40 @@
+package lite;
+
+import verifier.Backtrack;
+
+
+
+public class OrSolver extends ITLSolver {
+
+	ITLSolver left;
+	ITLSolver right;
+	public OrSolver(ITLSolver left, ITLSolver right) {
+		this.left = left;
+		this.right = right;
+	}
+	public boolean value() {
+		return left.value() || right.value();
+	}
+	
+	public String toString() {
+		return "("+left+" or "+right+")";
+	}
+
+
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+
+		return left.sat(sat, new Continuation(sat,next,this));
+	}
+
+	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		if (value!=null) {
+			return right.sat(sat, next);
+		} else {
+			return next.sat(ITLSatisfier.true_);
+		}
+	}
+
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/PredicateSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,43 @@
+package lite;
+
+import java.util.LinkedList;
+
+import verifier.Backtrack;
+
+
+
+public class PredicateSolver extends ITLSolver {
+
+	private LinkedList<ITLSolver> arg;
+	private ITLSolver predicate;
+
+	public PredicateSolver(ITLSolver predicate, LinkedList<ITLSolver> arg) {
+		this.predicate = predicate;
+		this.arg = arg;
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public String toString() {
+		return predicate.toString();
+	}
+
+	@Override
+	public boolean value() {
+		// TODO Auto-generated method stub
+		return false;
+	}
+
+	@Override
+	public LinkedList<ITLSolver> arguments() {
+		return arg;
+	}
+	
+
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/TrueSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,22 @@
+package lite;
+
+import verifier.Backtrack;
+
+public class TrueSolver extends ITLSolver {
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		return next.sat(ITLSatisfier.true_);
+	}
+
+	
+	public String toString() {
+		return "true";
+	}
+
+
+	@Override
+	public boolean value() {
+		return true;
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/VariableSolver.java	Wed Dec 26 16:09:16 2007 +0900
@@ -0,0 +1,54 @@
+package lite;
+
+import verifier.Backtrack;
+
+public class VariableSolver extends ITLSolver {
+		
+	public String name;
+	public boolean value;
+	
+	public VariableSolver(String _name0, boolean _value0) {
+		name = _name0;
+		value = _value0;
+	}
+	
+	public String name() {
+		return name;
+	}
+	public boolean value() {
+		return value;
+	}
+		
+	public String toString() {
+		// return name+"."+this.hashCode();
+		return name;
+	}
+	
+	public void setValue(ITLSolver b) {
+		value = b!=null;
+	}
+
+	@Override
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		if (sat.hasChoicePoint(this)) {
+			// choice point is already made, use it
+			return next.sat(value?ITLSatisfier.true_:null);
+		}
+		sat.addChoicePoint(this);
+		value = true; // the first choice
+		try {
+			return next.sat(ITLSatisfier.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.deleteChoicePoint(this);
+				throw e1;
+			}
+		}
+	}
+}