Mercurial > hg > Applications > JavaLite

changeset 53:bea547f744d7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Mon, 07 Jan 2008 01:15:00 +0900
parents 97a6c618bcc7
children 9a03268c1443
files Changes src/lite/BDDSolver.java src/lite/ChopSolver.java src/lite/EmptySolver.java src/lite/ITLSatisfier.java src/sbdd/SBDDTest.java
diffstat 6 files changed, 43 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Sun Jan 06 23:08:08 2008 +0900
+++ b/Changes	Mon Jan 07 01:15:00 2008 +0900
@@ -1,3 +1,19 @@
+Sun Jan  6 23:09:31 JST 2008
+
+まぁ、一応、展開できるところまでできたか...
+
+empty の扱いがまだおかしい。local なものがちゃんと restore されてる?
+
+CPS なプログラムの debug の方法が良くわからない。
+
+BDD を外部(JavaBDD)にするかどうかよりも、先に、このあたりを片付けないと
+だめか。BDD を外部に出すのは、それほど難しくなさそう。
+
+state queue を持たずに、それも BDD で行う、Charcteristic function を
+使う方法もあるのだが、BDDがでかくなるんだよな〜
+
+CbC のプログラムを吐くのも難しくはないはず。
+
 Sat Jan  5 14:26:35 JST 2008
 
 BDDSolver が自分がTrue/False かどうか判断できないって、どうよ...
--- a/src/lite/BDDSolver.java	Sun Jan 06 23:08:08 2008 +0900
+++ b/src/lite/BDDSolver.java	Mon Jan 07 01:15:00 2008 +0900
@@ -68,7 +68,7 @@
 
 
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		if (id!=BDDID.Variable) {
+		if (id!=BDDID.Variable&&id!=BDDID.BDD) {
 			return var.sat(sat,next);
 		}
 		return var.sat(sat, new Continuation(sat,next,this));
--- a/src/lite/ChopSolver.java	Sun Jan 06 23:08:08 2008 +0900
+++ b/src/lite/ChopSolver.java	Mon Jan 07 01:15:00 2008 +0900
@@ -8,8 +8,8 @@
 
 	protected ITLSolver former;
 	private ITLSolver later;
-	private VariableSolver innerEmpty;
-	private ITLSolver outerEmpty;
+	//private VariableSolver innerEmpty;
+	//private ITLSolver outerEmpty;
 	ITLSolver later1;
 
 	/*
@@ -60,9 +60,10 @@
 			return former.sat(sat, new Continuation(sat,next, new ChopSolver2()));
 		} else {
 			// Make inner empty variable
-			innerEmpty = new VariableSolver("empty",true);
-			outerEmpty = sat.newEmpty(innerEmpty);  // restore it later
-			innerEmpty.setValue(true);
+			//innerEmpty = new VariableSolver("empty",true);
+			//outerEmpty = sat.newEmpty(innerEmpty);  // restore it later
+			//innerEmpty.setValue(true);
+			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()));
 		}
@@ -80,12 +81,14 @@
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			if (value==null) {
 				// former is falied on empty, try more
-			    innerEmpty.setValue(false);
-				return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
+			    // innerEmpty.setValue(false);
+			    sat.empty.setValue(false);
+		    	return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
 			} 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.
-				sat.restoreEmpty(outerEmpty);
+				// sat.restoreEmpty(outerEmpty);
+			    sat.empty.setValue(false);
 				return later.sat(sat, new Continuation(sat,next, new ChopSolver5()));
 			}
 		}
@@ -94,14 +97,13 @@
 	class ChopSolver4 implements Next {
 		// try former on more (single choice case)
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			// sat.restoreEmpty(outerEmpty);
 			if (value==null) {
 				// all failed
-				sat.restoreEmpty(outerEmpty);
 				return next.sat(value);
 			} else {
 				// former is true with @value, return @(value&later)
 				// optimize required to avoid creating same node
-				sat.restoreEmpty(outerEmpty);
 				return next.sat(sat.lf.chopNode(value,later));
 			}
 		}
@@ -109,8 +111,8 @@
 
 	class ChopSolver5 implements Next {
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			outerEmpty = sat.newEmpty(innerEmpty);  // restore it later
-			innerEmpty.setValue(false);
+			// outerEmpty = sat.newEmpty(innerEmpty);  // restore it later
+			// innerEmpty.setValue(false);
 			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()));
@@ -124,7 +126,7 @@
 	
 	class ChopSolver6 implements Next {
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			sat.restoreEmpty(outerEmpty); // all done
+			// sat.restoreEmpty(outerEmpty); // all done
 			if (value==null) {  // former is fail on more inerval
 				return next.sat(later1);
 			} else {
--- a/src/lite/EmptySolver.java	Sun Jan 06 23:08:08 2008 +0900
+++ b/src/lite/EmptySolver.java	Mon Jan 07 01:15:00 2008 +0900
@@ -12,13 +12,7 @@
 
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		value = true; // the first choice
-		try {
-			return next.sat(sat.true_);
-		} catch (Backtrack e) {
-			value = false; // the second choice
-			return next.sat(null);
-		}
+		return sat.empty.sat(sat, next);
 	}
 
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
--- a/src/lite/ITLSatisfier.java	Sun Jan 06 23:08:08 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Mon Jan 07 01:15:00 2008 +0900
@@ -1,6 +1,5 @@
 package lite;
 
-import java.util.LinkedList;
 
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
@@ -15,13 +14,11 @@
 	public ITLSolver true_;
 	public SBDDFactoryInterface lf;
 
-	public LinkedList<ITLSolver> satList;
 	public Backtrack backtrack;
 	public ITLSolver empty;
 
 	
 	public ITLSatisfier() {
-		satList = new LinkedList<ITLSolver>();
 		backtrack = new Backtrack();
 		true_  = ITLNodeFactory.trueSolver;
 	}
@@ -68,7 +65,7 @@
 		return this;
 	}
 
-
+/*
 	public ITLSolver newEmpty(ITLSolver e) {
 		ITLSolver old = this.empty;
 		addChoicePoint(e);
@@ -80,7 +77,7 @@
 		deleteChoicePoint(empty);
 		empty = outerEmpty;
 	}
-	
+	*/
 
 
 }
--- a/src/sbdd/SBDDTest.java	Sun Jan 06 23:08:08 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Mon Jan 07 01:15:00 2008 +0900
@@ -56,10 +56,14 @@
 	}
 	
 	public void verifyTest() {
+		showVerify("~(@(q))");
 		showVerify("p&q");
-		showVerify("true&q");
+		// showVerify("true&q");
+		showVerify("<>(q)");
+		showVerify("proj(length(3),<>(p))");
 		showVerify("~(true& ~q)");
-		showVerify("proj(length(3),<>(p))");
+		showVerify("@(@(@(empty)))");
+		showVerify("fin(p)=([](<>(p)))");
 	}
 
 	public void showAllNext(String s) {
@@ -67,7 +71,7 @@
 		BDDSolver b = n.toSBDD(sf);
 		System.out.println(b);
 		sat.develop(b, new Print());
-		System.out.println(sf.hash);
+		// System.out.println(sf.hash);
 		System.out.println();
 	}
 	
@@ -83,7 +87,7 @@
 		ITLSolver n = p.parse(s);
 		BDDSolver b = n.toSBDD(sf);
 		verify(b);
-		System.out.println(sf.hash);
+		// System.out.println(sf.hash);
 		System.out.println();
 	}