Mercurial > hg > Applications > JavaLite

changeset 56:57259d2b9484

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 22:02:16 +0900
parents 99abe1d8fe69
children e416e9def04d
files Changes src/data/example src/lite/ChopSolver.java src/lite/ITLSatisfier.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDEntry.java src/sbdd/SBDDFactory.java src/sbdd/SBDDSet.java src/sbdd/SBDDTest.java
diffstat 9 files changed, 319 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Mon Jan 07 15:08:49 2008 +0900
+++ b/Changes	Mon Jan 07 22:02:16 2008 +0900
@@ -1,3 +1,27 @@
+Mon Jan  7 15:11:55 JST 2008
+
+verifier まで動きました。
+
+empty はparserでvariable に変換していたのを忘れてました。
+
+何故か同じ形で二度展開されるものがある。
+
+あとは、例題を全部動かせば良いだけか。Interval variable
+もやるか?
+
+この方法だと、variable をtryする順序が固定なので、order的には、
+2^v * (sbdd term の組合せ) となる。これは、遅いよね。
+印刷すると遅いけど、印刷されたものをすべてたどっているわけではないん
+だが...
+
+variable の順序を見つけるのにだけ、SATを使えばいいんじゃないか?
+といっても、sbdd term の組合せだけ用意しないとだめか。
+
+     develop
+       find sat variable order by SAT
+
+という感じか?
+
 Sun Jan  6 23:09:31 JST 2008
 
 まぁ、一応、展開できるところまでできたか...
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/data/example	Mon Jan 07 22:02:16 2008 +0900
@@ -0,0 +1,257 @@
+
+ex(0,(p)).
+ex(1,((p&q))).
+ex(2,( (fin(p)&true) <-> '<>'p)).
+ex(3,( fin(p) <-> '[]'( '<>' p) )).
+ex(4,(~(true&q))).
+ex(5,(~(true& ~q))).
+ex(6,(((true& p),(true& q)))).
+ex(7,('[]'((p -> '<>' q)))).
+ex(8,( '<>' '[]'(p))).
+ex(9,( '[]'( '<>'(p)))).
+ex(10,((p && p && p && p && p && ~p && p)-> '[]'('<>'(p)))).
+% weak closure (or finite closure)
+ex(11,+ (a,@ (b,@ (c,@empty)))).
+% quantifier
+ex(12,exists(R,(R,keep(@R = ~R),'[]'((R->p))))).
+% temporal assignment
+ex(13,exists(R,(R = p,keep(@R = R),fin(R = p)))).
+%
+ex(14,
+	exists(Q,(Q, 
+	  '[]'((Q -> 
+	          (((((a,skip) & (b,skip)), @ keep(~Q)) & Q)
+	          ;empty))
+	  )))
+   <->  *(((a,skip) & (b,skip) ; empty))
+).
+ex(15,
+        while(q,((a,skip) & (b,skip)))
+   <->  exists(C,(C, 
+          '[]'(
+             (C -> 
+                  (((q -> ((a,skip) & (b,skip)), @ keep(~C)) & C),
+                    (~q -> empty))
+             ))))
+).
+ex(16,even(p)<->evenp(p)).
+% wrong example, but hard to solve
+% ex(17,(p=>(q=>r)) <-> ((p=>q)=>r)).
+% ex(18,exists(Q,(p=>Q & Q=>r)) <-> (p=>r)).
+% 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,
+% 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) ) ,
+% shared resources
+	'[]'( ~ ( 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...)
+
+ex(22,(more,
+% three philosophers  with no iteration
+        ( ('[]'((~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))
+)).
+% These are not schema. Just check
+% Linear Time Axioms, valid in ITL
+ex(100,('[]'((a->b)) -> ('[]'(a) -> '[]'(b)))).  		%   K
+ex(101,('[]'(((a , '[]'(a))->b));'[]'(((b , '[]'(b))->a)))).    %   4
+ex(102,('[]'(a)-> '<>'(a))).                           	%   D
+ex(103,('[]'(a)-> '[]'('[]'(a)))).                      	%   L
+ex(104,(('[]'(a)) -> a)).                              	%   T
+ex(105,('[]'('[]'((((a-> '[]'(a)))->a))) -> ((('<>'('[]'(a)))-> '[]'(a))))). %   Diodorean discreteness
+% Linear Time Axioms, not valid in ITL
+ex(106,('[]'(('[]'(a)->a))-> ((('<>'('[]'(a)))-> '[]'(a))))).   	%   Z discreteness
+ex(107,('[]'(('[]'(a)->a))-> ('[]'(a)))).                	%   W weak density
+% Other Axioms, not valid in ITL
+ex(108,(a-> '[]'('<>'(a)))).                          	%   B
+ex(109,(('<>'a)-> '[]'('<>'(a)))).                    	%   5
+
+ex(110,(more-> (more&more))).                   	%   our dense time
+
+ex(demo(X),Y) :- demo(X,Y).
+% Regular variable examples ( doesnot work now....)
+
+ex(200,^r).
+ex(201,true & ^r).   		% will terminate?
+ex(202,((^r & ^r),not(^r))).	% is non-local?
+ex(203,(^r,length(4))).		% distinguish different state?
+ex(204,('[a]'(^r))).		% non-deterministic?
+ex(205,('[a]'(^r = length(2)))). 		% imitate length?
+ex(206,('[a]'(^r = length(4)),(^r& ^r))).
+ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
+ex(208,('[]'(^r = (
+         a,@ ^r;
+         not(a),c,@ @ ^r;
+         not(a),not(c),b,empty)),^r)).        % RE
+ex(209,('[a]'(^r = (
+         a,@((^r & @((b,empty)))) ;
+         not(a),b,empty)),
+      ^r)).                                   % CFG
+
+% Linear Time Axioms, valid in ITL
+ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))).            	%   K
+ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))).   	%   4
+ex(212,('[]'(^a)-> '<>'(^a))).                             		%   D
+ex(213,('[]'(^a)-> '[]'('[]'(^a)))).                         		%   L
+ex(214,(('[]'(^a))-> ^a)).                                	%   T
+%   Diodorean discreteness
+ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))). 
+% Linear Time Axioms, not valid in ITL
+%   Z discreteness
+ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))).
+%   W weak density
+ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))).
+% Other Axioms, not v^alid in ITL
+ex(218,(^a-> '[]'('<>'(^a)))).                              %   B
+ex(219,(('<>' ^a)-> '[]'('<>'(^a)))).                         %   5
+
+% State Diagram Support
+
+ex(300,(((length(2), @ '<>'(q)) proj true),
+      st(ns0)
+      )) :- ensure_loaded(kiss_ex).
+
+% Infinite Interval
+
+ex(400,infinite).
+ex(401,*infinite).
+ex(402,*skip).
+ex(403,*length(5)).
+ex(404,~('<>'(empty))).
+ex(405,('<>'(empty))).   % unsatisfiable 
+ex(406,(infinite-> @infinite)).
+ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
+ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))).  % satisfiable
+ex(409,finite).   % unsatisfiable
+
+
+demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
+
+% length 5 interval
+demo(1, length(5)).
+
+% p is trun at the top of a interval
+demo(2, (length(5),p)).
+
+% @ meas next time.
+demo(3, (length(5),@p,@ @q,@ @ @r)).
+
+% &(chop) devides an interval into to parts
+demo(4, ((length(2),p)) & (length(3),q)).
+
+%  there are several ways of division.
+demo(5, (length(5),(p&q))).
+
+% sometime usinng chop
+demo(6, (length(5),(true & p))).
+
+% always: dual of sometime
+demo(7, (length(5),not(true & not(p)))).
+
+% counter intutive theorem
+demo(8, '<>' '[]'(p) = '[]'('<>'(p))).
+
+% shared resource / exclusive condition
+demo(9, (length(5),
+        '[]'(((    ac ,not(bc),not(cc),not(dc));
+            (not(ac),    bc ,not(cc),not(dc));
+            (not(ac),not(bc),    cc ,not(dc));
+            (not(ac),not(bc),not(cc),    dc ))))).
+
+% periodical task by Projection
+demo(10, (more,
+	proj((@ '<>'(q),length(2)),true))).
+
+% time sharing taks by Projection
+demo(11, (more,length(7),
+	proj(true,('[]'(p),length(4))))).
+
+% combination of periodical task
+demo(12, (more,
+	proj(length(2),'[]'(ac)),
+	proj(length(3),'[]'(bc)),
+	proj(length(5),'[]'(cc)))).
+
+% periodical task with shared resources
+demo(13, (more,
+	proj((length(3),@ '<>'(ac)),true),
+	proj((length(5),@ '<>'(bc)),true),
+	proj((length(5),@ '<>'(cc)),true),
+	'[]'((not((ac,bc)),not((bc,cc)),not((cc,ac)))),
+	true)).
+
+% combination of periodical taks and aperiodical task with shared resource
+demo(14, (
+	((proj(true,(length(5),'[]'(dc))),length(15) )&true),
+	proj((length(3),@ '<>'(ac)),true),
+	proj((length(5),@ '<>'(bc)),true),
+	proj((length(5),@ '<>'(cc)),true),
+	'[]'(((    ac ,not(bc),not(cc),not(dc));
+	    (not(ac),    bc ,not(cc),not(dc));
+	    (not(ac),not(bc),    cc ,not(dc));
+	    (not(ac),not(bc),not(cc),    dc ))),
+	true)).
+% combination of periodical taks and aperiodical task with shared resource
+%  schedulable case
+demo(15, (
+	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
+	proj((length(3),@ '<>'(ac)),true),
+	proj((length(5),@ '<>'(bc)),true),
+	proj((length(5),@ '<>'(cc)),true),
+	'[]'(((    ac ,not(bc),not(cc),not(dc));
+	    (not(ac),    bc ,not(cc),not(dc));
+	    (not(ac),not(bc),    cc ,not(dc));
+	    (not(ac),not(bc),not(cc),    dc ))),
+	true)).
+
+
+% model restriction by share predicate ( a little smaller.... :-)
+demo(16, (
+	share([ac,bc,cc,dc]),
+	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
+	proj((length(3),@ '<>'(ac)),true),
+	proj((length(5),@ '<>'(bc)),true),
+	proj((length(5),@ '<>'(cc)),true),
+	true)).
+demo(17, (
+((proj(true,(length(5),'[]'(c))),length(15))&true),
+(proj((length(3),@ '<>'(a)),true)&less(3)),
+(proj((length(5),@ '<>'(b)),true)&less(5)),
+'[]'(not((a,b))),
+'[]'(not((b,c))),
+'[]'(not((c,a)))
+)).
+
+end.
--- a/src/lite/ChopSolver.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/lite/ChopSolver.java	Mon Jan 07 22:02:16 2008 +0900
@@ -59,10 +59,6 @@
 		if (value!=null) { // Outer empty case
 			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);
 			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()));
@@ -81,13 +77,11 @@
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			if (value==null) {
 				// former is falied on empty, try more
-			    // 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.empty.setValue(false);
 				return later.sat(sat, new Continuation(sat,next, new ChopSolver5()));
 			}
@@ -97,7 +91,6 @@
 	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
 				return next.sat(value);
@@ -111,8 +104,6 @@
 
 	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);
 			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()));
@@ -126,7 +117,6 @@
 	
 	class ChopSolver6 implements Next {
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			// sat.restoreEmpty(outerEmpty); // all done
 			if (value==null) {  // former is fail on more inerval
 				return next.sat(later1);
 			} else {
--- a/src/lite/ITLSatisfier.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Mon Jan 07 22:02:16 2008 +0900
@@ -65,19 +65,6 @@
 		return this;
 	}
 
-/*
-	public ITLSolver newEmpty(ITLSolver e) {
-		ITLSolver old = this.empty;
-		addChoicePoint(e);
-		empty = e;
-		return old;
-	}
-
-	public void restoreEmpty(ITLSolver outerEmpty) {
-		deleteChoicePoint(empty);
-		empty = outerEmpty;
-	}
-	*/
 
 
 }
--- a/src/sbdd/BDDSatisfier.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Mon Jan 07 22:02:16 2008 +0900
@@ -63,6 +63,7 @@
 	public void showVerify(String s) {
 		ITLSolver n = p.parse(s);
 		BDDSolver b = n.toSBDD(sf);
+		System.out.println(s);
 		verify(b);
 		// System.out.println(sf.hash);
 		System.out.println();
@@ -94,7 +95,8 @@
 		state = sf.set();
 		queue = new LinkedList<SBDDEntry>();
 		AllNext allNext = new AllNext();
-		queue.add(new SBDDEntry(n));
+		SBDDEntry b = state.getEntry(n);
+		queue.add(b);
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
 			if (e.expanded) continue;
 			e.expanded = true;
--- a/src/sbdd/SBDDEntry.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/sbdd/SBDDEntry.java	Mon Jan 07 22:02:16 2008 +0900
@@ -2,9 +2,10 @@
 
 
 import lite.ITLSolver;
+import java.util.Map.Entry;
 
 
-public class SBDDEntry {
+public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> {
 
 	public static int count = 0;
 	
@@ -24,6 +25,20 @@
 	public int hashCode() {
 		return key.hashCode();
 	}
+
+	public ITLSolver getKey() {
+		return key;
+	}
+
+	public SBDDEntry getValue() {
+		return this;
+	}
+
+	public SBDDEntry setValue(SBDDEntry e) {
+		key = e.key;
+		expanded = e.expanded;
+		return this;
+	}
 	
 
 }
--- a/src/sbdd/SBDDFactory.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Mon Jan 07 22:02:16 2008 +0900
@@ -4,7 +4,6 @@
 
 import lite.BDDSolver;
 import lite.ITLNodeFactory;
-import lite.ITLNodeParser;
 import lite.ITLSolver;
 import logicNode.parser.TokenID;
 
@@ -41,6 +40,10 @@
 	
 
 	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) {
+		// too slow?
+		//solver = hash.put(solver);
+		//solver2 = hash.put(solver2);
+		//if (solver==solver2) return solver;
 		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
 		return hash.put(v); 
 	}
--- a/src/sbdd/SBDDSet.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Mon Jan 07 22:02:16 2008 +0900
@@ -3,19 +3,19 @@
 import java.util.AbstractSet;
 import java.util.Collection;
 import java.util.Iterator;
-import java.util.Set;
+import java.util.Map.Entry;
 
 import lite.BDDSolver;
 import lite.ITLSolver;
 
-public class SBDDSet extends  AbstractSet<SBDDEntry>
-		implements Set<SBDDEntry> {
+public class SBDDSet extends  AbstractSet<Entry<ITLSolver, SBDDEntry>> {
 	public SBDDEntry[] sbddArray ;
 	public int hash;
 	private int hash0;
 	private int hashSize = 1024;
 	public Object lastEntry;
 	SBDDFactory sf;
+	int size = 0;
 
 	SBDDSet() {
 		sbddArray = new SBDDEntry [hashSize];
@@ -37,15 +37,16 @@
 	}
 	
 	@Override
-	public Iterator<SBDDEntry> iterator() {
-		return new Iterator<SBDDEntry>() {
+	public Iterator<Entry<ITLSolver, SBDDEntry>> iterator() {
+		hash0 = hash-1+hashSize;
+		return new Iterator<Entry<ITLSolver, SBDDEntry>>() {
 
 			public boolean hasNext() {
-				return (hash!=hash0 && sbddArray[hash % hashSize]!=null) ;
+				return (sbddArray[hash%hashSize]!=null && hash!=hash0) ;
 			}
 
 			public SBDDEntry next() {
-				return sbddArray[hash++ % hashSize];
+				return sbddArray[hash++%hashSize];
 			}
 
 			public void remove() {
@@ -54,8 +55,6 @@
 		};
 	}
 
-
-
 	@Override
 	public  boolean contains(Object e) {
 		return get(e)!=null;
@@ -78,17 +77,18 @@
 	
 	@Override
 	public int size() {
-		return hashSize;
+		return size;
 	}
 
 	@Override
-	public boolean add(SBDDEntry e) {
+	public boolean add(Entry<ITLSolver, SBDDEntry> e) {
 		// check hash is already set by contains
 		if (lastEntry!=e) {
 			if (get(e)!=null||hash==hash0) return false;
 		}
 		sbddArray[hash%hashSize] = (SBDDEntry) e;
 		lastEntry = null;
+		size++;
 		return true;
 	}
 
@@ -114,7 +114,7 @@
 		for(int i = 0;i<sbddArray.length;i++) {
 			if (sbddArray[i]!=null) {
 				SBDDEntry e  = sbddArray[i];
-				s += "\t"+i+"\thash="+e.key.hashCode()+":"+e.key+"\n";
+				s += i+"\t"/*+"\thash="+(e.key.hashCode()%hashSize)*/+":"+e.key+"\n";
 			}
 		}
 		return s+"]";
--- a/src/sbdd/SBDDTest.java	Mon Jan 07 15:08:49 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Mon Jan 07 22:02:16 2008 +0900
@@ -50,14 +50,12 @@
 		sat.showVerify("<>(p) = <>(p)");
 		sat.showVerify("~(@(q))");
 		sat.showVerify("p&q");
-		// showVerify("true&q");
+		// sat.showVerify("true&q");
 		sat.showVerify("<>(q)");
-		// showVerify("proj(length(3),<>(p))");
+		sat.showVerify("proj(length(3),<>(p))");
 		sat.showVerify("~(true& ~q)");
-		// showVerify("@(@(@(empty)))");
+		// sat.showVerify("@(@(@(empty)))");
 		sat.showVerify("fin(p)=([](<>(p)))");
-		//sat.sf.init();
-		//sat.state.put(sat.empty);
 		}
 		sat.showVerify("fin(p)");
 		System.out.println(sat.state);