# HG changeset patch # User kono # Date 1199710936 -32400 # Node ID 57259d2b948416c82c7054652cc6fd6783375634 # Parent 99abe1d8fe6934cebe554b4a1efe7072ffbfdcae *** empty log message *** diff -r 99abe1d8fe69 -r 57259d2b9484 Changes --- 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 まぁ、一応、展開できるところまでできたか... diff -r 99abe1d8fe69 -r 57259d2b9484 src/data/example --- /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. diff -r 99abe1d8fe69 -r 57259d2b9484 src/lite/ChopSolver.java --- 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 { diff -r 99abe1d8fe69 -r 57259d2b9484 src/lite/ITLSatisfier.java --- 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; - } - */ } diff -r 99abe1d8fe69 -r 57259d2b9484 src/sbdd/BDDSatisfier.java --- 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(); 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; diff -r 99abe1d8fe69 -r 57259d2b9484 src/sbdd/SBDDEntry.java --- 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 { 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; + } } diff -r 99abe1d8fe69 -r 57259d2b9484 src/sbdd/SBDDFactory.java --- 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); } diff -r 99abe1d8fe69 -r 57259d2b9484 src/sbdd/SBDDSet.java --- 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 - implements Set { +public class SBDDSet extends AbstractSet> { 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 iterator() { - return new Iterator() { + public Iterator> iterator() { + hash0 = hash-1+hashSize; + return new Iterator>() { 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 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(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);