Mercurial > hg > Applications > JavaLite

changeset 65:48db54d3129b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Fri, 11 Jan 2008 02:10:06 +0900
parents 80db395eeb30
children 96b1c8c2f9b9
files Changes src/data/example src/lite/ChopSolver.java src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/lite/ITLSatisfier.java src/lite/ITLSolver.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDEntry.java src/sbdd/SBDDFactory.java src/sbdd/SBDDSet.java src/sbdd/SBDDTest.java
diffstat 12 files changed, 114 insertions(+), 59 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Thu Jan 10 18:16:00 2008 +0900
+++ b/Changes	Fri Jan 11 02:10:06 2008 +0900
@@ -4,6 +4,14 @@
 その方が linear search しなくて良いので少し速い。
 けど、exists との相性は悪い。(かな?)
 
+exists は、true/false にセットしたところで、try/catchしないと
+だめらしい。(chop はいいのか? 悪いとしたら、それをテストする
+例は?)
+
+weak next をbaseにした方が
+     @p =  next(p),~empty
+で、~empty が他と共有されるので調子が良い。
+
 Wed Jan  9 20:42:17 JST 2008
 
 あぁ、そうか。
--- a/src/data/example	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/data/example	Fri Jan 11 02:10:06 2008 +0900
@@ -41,37 +41,37 @@
 % dining philosopher
 %   note: unspecified resource increase states
 %   ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * 
-%ex(19,(more,
-%% three philosophers 
-%        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
-%        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
-%        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
-%% shared resources
-%	'[]'( ~ ( ar, bl)),
-%	'[]'( ~ ( br, cl)),
-%	'[]'( ~ ( cr, al))
-%)).
-%ex(20,(more,
+ex(19,(more,
+% three philosophers 
+        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
+        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
+        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
+% shared resources
+	'[]'( ~ ( ar, bl)),
+	'[]'( ~ ( br, cl)),
+	'[]'( ~ ( cr, al))
+)).
+ex(20,(more,
 %% five philosophers 
-%        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
-%        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
-%        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
-%        *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
-%        *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
+        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
+        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
+        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
+        *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
+        *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
 %% shared resources
-%	'[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
-%	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
-%)). % :-fail.  % too big to verify (sigh...)
+	'[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
+	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
+)). % :-fail.  % too big to verify (sigh...)
 %
-%ex(21,(more,
-%	share([ar,bl]),share([br,cl]),share([cr,dl]),
-%	share([dr,el]),share([er,al]),
-%        *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
-%        *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
-%        *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
-%        *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
-%        *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
-%true)).  % :-fail.  % too big to verify (sigh...)
+ex0(21,(more,
+	share(ar,bl),share(br,c),share(cr,dl),
+	share(dr,el),share(er,a),
+        *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
+        *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
+        *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
+        *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
+        *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
+true)).  % :-fail.  % too big to verify (sigh...)
 
 ex(22,(more,
 %% three philosophers  with no iteration
@@ -158,6 +158,7 @@
 
 
 % demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
+%def("demo(X,Y)","ex(X,Y)").
 def("demo(X,Y)","true").
 % length 5 interval
 demo(1, length(5)).
@@ -239,7 +240,7 @@
 
 % model restriction by share predicate ( a little smaller.... :-)
 demo(16, (
-	share([ac,bc,cc,dc]),
+	share(ac,bc,cc,dc),
 	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
--- a/src/lite/ChopSolver.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/lite/ChopSolver.java	Fri Jan 11 02:10:06 2008 +0900
@@ -75,15 +75,19 @@
 
 	class ChopSolver3 implements Next {
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			if (value==null) {
-				// former is falied on empty, try more
-			    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.empty.setValue(false);
-				return later.sat(sat, new Continuation(sat,next, new ChopSolver5()));
+			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()));
+				} 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()));
+				}
+			} catch (Backtrack e) {
+				sat.empty.setValue(true);
+				throw e;
 			}
 		}
 	}
@@ -91,6 +95,7 @@
 	class ChopSolver4 implements Next {
 		// try former on more (single choice case)
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			try {
 			if (value==null) {
 				// all failed
 				return next.sat(value);
@@ -99,6 +104,10 @@
 				// optimize required to avoid creating same node
 				return next.sat(sat.lf.chopNode(value,later));
 			}
+			} catch (Backtrack e) {
+				sat.empty.setValue(false);
+				throw e;
+			}
 		}
 	}
 
@@ -117,6 +126,7 @@
 	
 	class ChopSolver6 implements Next {
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			try {
 			if (value==null) {  // former is fail on more inerval
 				return next.sat(later1);
 			} else {
@@ -127,6 +137,10 @@
 				if (v==sat.false_) v = null;
 				return next.sat(v);
 			}
+			} catch (Backtrack e) {
+				sat.empty.setValue(false);
+				throw e;
+			}
 		}
 	}
 
--- a/src/lite/ITLCommander.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/lite/ITLCommander.java	Fri Jan 11 02:10:06 2008 +0900
@@ -40,6 +40,13 @@
 		} else if (predicate.toString() == "def") {
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
+		} else if (predicate.toString() == "verbose") {
+			if (Integer.parseInt(args.get(0).toString())==0) {
+				sat.verbose = false;
+			} else {
+				sat.verbose = true;
+			}
+			return lf.trueNode();
 		} else if (predicate.toString() == "include") {
 			String file = args.getFirst().toString();
 			parser.parseFile(file);
--- a/src/lite/ITLNodeParser.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Fri Jan 11 02:10:06 2008 +0900
@@ -54,7 +54,7 @@
 	                        for(int i =0;i<length;i++) {
 	                                n = logicNodeFactory.nextNode(n);
 	                        }
-	                        return (Node)n;
+	                        return n;
 						}
 			});
 			define("less(I)","false",50,parseCommand);               // less than N length
@@ -68,8 +68,8 @@
             define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))");
 // def(P<=Q,Q=>P)");
 // loop stuff and quantifiers
-			define("*(A) ","proj(true,(A;empty))");  // weak closure
-			define("+(A) ","proj(true,(A))");        // strong closure
+			define("*(A) ","proj(A,true),fin(A)");  // weak closure
+			define("+(A) ","A& *(empty;A)");   // 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)))");
@@ -79,11 +79,16 @@
 			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)))) ))");
+
+			// share([a,b,c]) is too difficult
 			
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("def(Head,Body,Order)","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)
 
 	}
@@ -111,6 +116,7 @@
 		dict.reserve("ex",TokenID.Exec);
 		dict.reserve("include",TokenID.Include);
 		dict.reserve("def",TokenID.Define);
+		dict.reserve("verbose",TokenID.Less);
 	}
 
 	@Override
--- a/src/lite/ITLSatisfier.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Fri Jan 11 02:10:06 2008 +0900
@@ -17,6 +17,7 @@
 
 	public Backtrack backtrack;
 	public ITLSolver empty;
+	public boolean verbose = true;
 
 	
 	public ITLSatisfier() {
--- a/src/lite/ITLSolver.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/lite/ITLSolver.java	Fri Jan 11 02:10:06 2008 +0900
@@ -58,7 +58,7 @@
 	}
 	
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
-		return null;
+		return (BDDSolver) sf.falseNode();
 	}
 
 	
--- a/src/sbdd/BDDSatisfier.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Fri Jan 11 02:10:06 2008 +0900
@@ -74,27 +74,48 @@
 		System.out.println();
 	}
 	
-	
 	class AllNext implements Next {
+
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			System.out.print(" "+sat.choicePoint()+" -> "+value);
 			if (value!=null) {
 				SBDDEntry e = state.getEntry(value);
 				if (e.expanded) {
 						// skip
+					System.out.print(".");
 				} else 	{
 					queue.add(e);
-					System.out.print("!");
+					System.out.print(e.id+" ");
+				} 
+			} else {
+				System.out.print("f");
+			}
+			throw sat.backtrack;
+		}
+	}
+	
+	class AllNextVerbose implements Next {
+
+		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			String s = "null";
+			System.out.print(" "+sat.choicePoint()+" -> ");
+			if (value!=null) {
+				SBDDEntry e = state.getEntry(value);
+				s = value.toString(); s = Integer.toString(e.id)+":"+s;
+				if (e.expanded) {
+						// skip
+				} else 	{
+					queue.add(e);
+					s = "!"+s;
 				} 
 			}
-			System.out.println();
+			System.out.println(s);
 			throw sat.backtrack;
 		}
 	}
 
 	public void verify(ITLSolver n) {
 		queue = new LinkedList<SBDDEntry>();
-		AllNext allNext = new AllNext();
+		Next allNext = verbose? new AllNextVerbose() : new AllNext();
 		SBDDEntry b = state.getEntry(n);
 		if (b.expanded) {
 			// already checked
@@ -105,12 +126,9 @@
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
 			if (e.expanded) continue;
 			e.expanded = true;
-			System.out.println(e.key+"->");
+			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
 			develop(e.key, allNext);
-			if (this.size()>0) {
-				System.err.println("cb remains "+this);
-				this.clear();
-			}
+			if (!verbose) System.out.println();
 		}
 	}
 		
--- a/src/sbdd/SBDDEntry.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/sbdd/SBDDEntry.java	Fri Jan 11 02:10:06 2008 +0900
@@ -2,15 +2,17 @@
 
 
 import lite.ITLSolver;
+
+import java.util.LinkedList;
 import java.util.Map.Entry;
 
 
 public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> {
 
-	public static int count = 0;
-	
 	public ITLSolver key;
 	boolean expanded = false;
+	int id;
+	LinkedList<SBDDEntry>nexts;
 	
 	public SBDDEntry(ITLSolver now) {
 		this.key = now;
--- a/src/sbdd/SBDDFactory.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Fri Jan 11 02:10:06 2008 +0900
@@ -75,7 +75,7 @@
 	}
 
 	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
-		ITLSolver v =  itlf.projectionNode(solver,solver2);
+		ITLSolver v =  itlf.projectionNode(solver.toSBDD(this),solver2.toSBDD(this));
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Projection);
 		return hash.put(b);
 	}
--- a/src/sbdd/SBDDSet.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Fri Jan 11 02:10:06 2008 +0900
@@ -88,7 +88,7 @@
 		}
 		sbddArray[hash%hashSize] = (SBDDEntry) e;
 		lastEntry = null;
-		size++;
+		e.getValue().id = size++;
 		return true;
 	}
 
--- a/src/sbdd/SBDDTest.java	Thu Jan 10 18:16:00 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Fri Jan 11 02:10:06 2008 +0900
@@ -67,9 +67,7 @@
 		sat.showVerify("even(p)");
 		sat.showVerify("Q, keep( @Q = ~Q)");
 		}
-		sat.showVerify("even(p)");
-		sat.showVerify("evenp(p)");
-		//sat.showVerify("even(p)<->evenp(p)");
+		sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
 		//sat.p.parse("include('data/example').");
 		// System.out.println(p.parseCommand.sat.state);