# HG changeset patch
# User kono
# Date 1200029462 -32400
# Node ID 96b1c8c2f9b9630ce5f03ef82a1357aadfe036a3
# Parent  48db54d3129bb6831e628c356293fdc7afe8c342
*** empty log message ***

diff -r 48db54d3129b -r 96b1c8c2f9b9 Changes
--- a/Changes	Fri Jan 11 02:10:06 2008 +0900
+++ b/Changes	Fri Jan 11 14:31:02 2008 +0900
@@ -1,3 +1,22 @@
+Fri Jan 11 14:23:21 JST 2008
+
+(empty & Hoge)が、なんかはびこって、項の大きさを大きくしているらしい。
+つうか、これがあると収束しないです。
+
+projection(C,I) のtermination は、I 項のverification が収束すること
+に依存しているので、I項に Projection が入っていると、projection の
+ネストの帰納法で証明する必要がある。
+
+ということは、I の方がちゃんと正規形になって有限の項の組合
+せであることを示す必要がある。I の方を前もって展開してしま
+うという手もあるけど。つまり、安易な最適化を入れて収束して
+も、それがtermination の証明にならないということ。
+
+SDDEntry.expanded は、展開されたのはなくて生成されてqueueに
+入れた時点でtrueにして良い。こうすれば、queue の中には unique
+な項しか入らないことになる。
+
+
 Thu Jan 10 13:28:26 JST 2008
 
 hasChoicePoint は、variable 毎にフラグで持っても良い。
diff -r 48db54d3129b -r 96b1c8c2f9b9 src/lite/ITLNodeParser.java
--- a/src/lite/ITLNodeParser.java	Fri Jan 11 02:10:06 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Fri Jan 11 14:31:02 2008 +0900
@@ -69,7 +69,8 @@
 // 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
+			//define("+(A) ","A& *(empty;A)");   // strong closure
+			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)))");
diff -r 48db54d3129b -r 96b1c8c2f9b9 src/sbdd/BDDSatisfier.java
--- a/src/sbdd/BDDSatisfier.java	Fri Jan 11 02:10:06 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Fri Jan 11 14:31:02 2008 +0900
@@ -83,7 +83,7 @@
 						// skip
 					System.out.print(".");
 				} else 	{
-					queue.add(e);
+					queue.add(e); e.expanded = true;
 					System.out.print(e.id+" ");
 				} 
 			} else {
@@ -104,7 +104,7 @@
 				if (e.expanded) {
 						// skip
 				} else 	{
-					queue.add(e);
+					queue.add(e); e.expanded = true;
 					s = "!"+s;
 				} 
 			}
@@ -122,10 +122,8 @@
 			System.out.println("   already checked.");
 			return;
 		}
-		queue.add(b);
+		queue.add(b); b.expanded = true;
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
-			if (e.expanded) continue;
-			e.expanded = true;
 			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
 			develop(e.key, allNext);
 			if (!verbose) System.out.println();
diff -r 48db54d3129b -r 96b1c8c2f9b9 src/sbdd/SBDDFactory.java
--- a/src/sbdd/SBDDFactory.java	Fri Jan 11 02:10:06 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Fri Jan 11 14:31:02 2008 +0900
@@ -75,7 +75,7 @@
 	}
 
 	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
-		ITLSolver v =  itlf.projectionNode(solver.toSBDD(this),solver2.toSBDD(this));
+		ITLSolver v =  itlf.projectionNode(solver,solver2);
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Projection);
 		return hash.put(b);
 	}
diff -r 48db54d3129b -r 96b1c8c2f9b9 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Fri Jan 11 02:10:06 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Fri Jan 11 14:31:02 2008 +0900
@@ -48,7 +48,7 @@
 	public void verifyTest() {
 		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");
 
-		if (true) {
+		if (false) {
 		sat.showVerify("skip");
 		sat.showVerify(" '<>'p");
 		sat.showVerify("<>(p) = <>(p)");
@@ -69,7 +69,7 @@
 		}
 		sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
-		//sat.p.parse("include('data/example').");
+		sat.p.parse("include('data/example').");
 		// System.out.println(p.parseCommand.sat.state);
 	}