Mercurial > hg > Applications > JavaLite
changeset 70:416e4d272e79 main-loop
*** empty log message ***
author | kono |
---|---|
date | Mon, 14 Jan 2008 16:48:48 +0900 |
parents | 5fd456b0a073 |
children | 01356168f25f |
files | src/data/example src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDEntry.java src/sbdd/SBDDHash.java src/sbdd/SBDDTest.java |
diffstat | 7 files changed, 149 insertions(+), 41 deletions(-) [+] |
line wrap: on
line diff
--- a/src/data/example Mon Jan 14 03:01:45 2008 +0900 +++ b/src/data/example Mon Jan 14 16:48:48 2008 +0900 @@ -41,7 +41,7 @@ % dining philosopher % note: unspecified resource increase states % ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * -ex0(19,(more, +ex(19,(more, % three philosophers *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) , *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) , @@ -63,7 +63,7 @@ '[]'( ~ ( dr, el)), '[]'( ~ ( er, al)) )). % :-fail. % too big to verify (sigh...) % -ex0(21,(more, +ex(21,(more, share([ar,bl]),share([br,cl]),share([cr,dl]), share([dr,el]),share([er,al]), *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) , @@ -73,7 +73,7 @@ *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) , true)). % :-fail. % too big to verify (sigh...) -ex0(22,(more, +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) ) , @@ -161,52 +161,52 @@ def("demo(X,Y)","ex(X,Y)"). % def("demo(X,Y)","true"). % length 5 interval -demo(1, length(5)). +demo(1001, length(5)). % p is trun at the top of a interval -demo(2, (length(5),p)). +demo(1002, (length(5),p)). % @ meas next time. -demo(3, (length(5),@p,@ @q,@ @ @r)). +demo(1003, (length(5),@p,@ @q,@ @ @r)). % &(chop) devides an interval into to parts -demo(4, ((length(2),p)) & (length(3),q)). +demo(1004, ((length(2),p)) & (length(3),q)). % there are several ways of division. -demo(5, (length(5),(p&q))). +demo(1005, (length(5),(p&q))). % sometime usinng chop -demo(6, (length(5),(true & p))). +demo(1006, (length(5),(true & p))). % always: dual of sometime -demo(7, (length(5),not(true & not(p)))). +demo(1007, (length(5),not(true & not(p)))). % counter intutive theorem -demo(8, '<>' '[]'(p) = '[]'('<>'(p))). +demo(1008, '<>' '[]'(p) = '[]'('<>'(p))). % shared resource / exclusive condition -demo(9, (length(5), +demo(1009, (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, +demo(1010, (more, proj((@ '<>'(q),length(2)),true))). % time sharing taks by Projection -demo(11, (more,length(7), +demo(1011, (more,length(7), proj(true,('[]'(p),length(4))))). % combination of periodical task -demo(12, (more, +demo(1012, (more, proj(length(2),'[]'(ac)), proj(length(3),'[]'(bc)), proj(length(5),'[]'(cc)))). % periodical task with shared resources -demo(13, (more, +demo(1013, (more, proj((length(3),@ '<>'(ac)),true), proj((length(5),@ '<>'(bc)),true), proj((length(5),@ '<>'(cc)),true), @@ -214,7 +214,7 @@ true)). % combination of periodical taks and aperiodical task with shared resource -demo(14, ( +demo(1014, ( ((proj(true,(length(5),'[]'(dc))),length(15) )&true), proj((length(3),@ '<>'(ac)),true), proj((length(5),@ '<>'(bc)),true), @@ -226,7 +226,7 @@ true)). % combination of periodical taks and aperiodical task with shared resource % schedulable case -demo(15, ( +demo(1015, ( ((proj(true,(length(4),'[]'(dc))),length(15) )&true), proj((length(3),@ '<>'(ac)),true), proj((length(5),@ '<>'(bc)),true), @@ -239,14 +239,14 @@ % model restriction by share predicate ( a little smaller.... :-) -demo(16, ( +demo(1016, ( 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, ( +demo(1017, ( ((proj(true,(length(5),'[]'(c))),length(15))&true), (proj((length(3),@ '<>'(a)),true)&less(3)), (proj((length(5),@ '<>'(b)),true)&less(5)),
--- a/src/lite/ITLCommander.java Mon Jan 14 03:01:45 2008 +0900 +++ b/src/lite/ITLCommander.java Mon Jan 14 16:48:48 2008 +0900 @@ -1,6 +1,8 @@ package lite; +import java.util.HashMap; import java.util.LinkedList; + import sbdd.BDDSatisfier; import logicNode.parser.Command; @@ -10,10 +12,12 @@ private ITLNodeFactoryInterface<Node> lf; private ITLNodeParser<Node> parser; public BDDSatisfier sat; + private HashMap<Integer,Node> examples; public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) { this.lf = lf; this.parser = parser; + this.examples = new HashMap<Integer,Node>(); } public Node exec(Node predicate, Node value, LinkedList<Node> args) { @@ -36,20 +40,44 @@ n = lf.orNode(lf.emptyNode(),lf.nextNode(n)); } return (Node)n; - } else if (name == "ex") { - if (sat==null) sat = new BDDSatisfier(); - // System.out.println(args.get(0)+":"+args.get(1)); - System.out.println(args.get(0)); - sat.verify(args.get(1)); - return lf.trueNode(); + } else if (name == "ex"|| name=="do") { + checkSat(); + if (args.size()<1) { + parser.error("ex(1) or ex(<>p) or ex(10,[]p)"); + return lf.trueNode(); + } + Node n = args.get(0); + int index = -1; + if (n.getClass()==NumberSolver.class) { + index = Integer.parseInt(n.toString()); + } + if (args.size()==1) { + // System.out.println(args.get(0)+":"+args.get(1)); + if (index>=0) { + n = examples.get(index); + if (n==null) { + parser.error("Unknown registered example"); + return lf.trueNode(); + } + } + System.out.println(n); + sat.verify(n); + return lf.trueNode(); + } else if (args.size()==2 && index>=0){ + examples.put(index, args.get(1)); + return lf.trueNode(); + } } else if (name == "def") { parser.define(args.get(0).toString(),args.get(1).toString()); return lf.trueNode(); } else if (name == "verbose") { - if (Integer.parseInt(args.get(0).toString())==0) { - sat.verbose = false; - } else { - sat.verbose = true; + Node n= null; + checkSat(); + try { + int i = Integer.parseInt((n=args.get(0)).toString()); + sat.verbose = (i==0)? false:true; + } catch (NumberFormatException e) { + sat.verbose = (n==lf.trueNode())?true:false; } return lf.trueNode(); } else if (name == "include") { @@ -61,4 +89,8 @@ return value; } + private void checkSat() { + if (sat==null) sat = new BDDSatisfier(); + } + }
--- a/src/lite/ITLNodeParser.java Mon Jan 14 03:01:45 2008 +0900 +++ b/src/lite/ITLNodeParser.java Mon Jan 14 16:48:48 2008 +0900 @@ -85,6 +85,7 @@ define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))"); define("ex(N,Exp)","true",50,parseCommand); + define("do(N)","true",50,parseCommand); define("def(Head,Body,Order)","true",50,parseCommand); define("include(path)","true",50,parseCommand); @@ -139,6 +140,7 @@ // parseCommand requires reserved word for string comparison dict.reserve("less"); dict.reserve("ex"); + dict.reserve("do"); dict.reserve("include"); dict.reserve("def"); dict.reserve("verbose"); @@ -250,4 +252,5 @@ return emptyNode; } + }
--- a/src/sbdd/BDDSatisfier.java Mon Jan 14 03:01:45 2008 +0900 +++ b/src/sbdd/BDDSatisfier.java Mon Jan 14 16:48:48 2008 +0900 @@ -12,8 +12,9 @@ import lite.ITLSatisfier; import lite.ITLSolver; import lite.Next; +import logicNode.parser.ExecutorInterface; -public class BDDSatisfier extends ITLSatisfier { +public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface<ITLSolver> { public ITLNodeParser<ITLSolver> p; @@ -21,6 +22,13 @@ public LinkedList<SBDDEntry> queue; public SBDDSet state; + public SBDDEntry currentState; + + + private boolean satisfiable; + private boolean falsfiable; + public SBDDEntry last; + /** * @@ -31,6 +39,7 @@ public void init() { lf = new ITLNodeFactory(); p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf); + // p.setExecutor(this); sf = new SBDDFactory(); // empty = ITLNodeFactory.emptySolver; // empty = SBDDFactory.emptySolver; @@ -98,14 +107,21 @@ 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) { + if (value==true_) { + satisfiable = true; s="true"; + } else { + SBDDEntry e = state.getEntry(value); + currentState.addNext(e); + s = value.toString(); s = Integer.toString(e.id)+":"+s; + if (e.expanded) { // skip - } else { - queue.add(e); e.expanded = true; - s = "!"+s; - } + } else { + queue.add(e); e.expanded = true; + s = "!"+s; + } + } + } else { + falsfiable = true; } System.out.println(s); throw sat.backtrack; @@ -113,9 +129,12 @@ } public void verify(ITLSolver n) { + falsfiable = false; + satisfiable = false; queue = new LinkedList<SBDDEntry>(); Next allNext = verbose? new AllNextVerbose() : new AllNext(); SBDDEntry b = state.getEntry(n); + last = b; if (b.expanded) { // already checked System.out.println(" already checked."); @@ -124,10 +143,18 @@ queue.add(b); b.expanded = true; for(SBDDEntry e;(e = queue.poll())!=null; ) { System.out.println(e.id+":"+(verbose?e.key+"->":"")); + currentState = e; develop(e.key, allNext); if (!verbose) System.out.println(); } + if (!verbose) { + if (!falsfiable) { + System.out.println("valid"); + } + if (!satisfiable) { + System.out.println("unsatisfiable"); + } + } } - }
--- a/src/sbdd/SBDDEntry.java Mon Jan 14 03:01:45 2008 +0900 +++ b/src/sbdd/SBDDEntry.java Mon Jan 14 16:48:48 2008 +0900 @@ -7,6 +7,7 @@ import java.util.Map.Entry; + public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> { public ITLSolver key; @@ -16,6 +17,7 @@ public SBDDEntry(ITLSolver now) { this.key = now; + nexts = new LinkedList<SBDDEntry>(); } public boolean equals(Object e0) { @@ -42,5 +44,9 @@ return this; } + public boolean addNext(SBDDEntry e) { + if (nexts.contains(e)) return false; + return nexts.add(e); + } }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sbdd/SBDDHash.java Mon Jan 14 16:48:48 2008 +0900 @@ -0,0 +1,32 @@ +package sbdd; + +import java.util.AbstractMap; +import java.util.Set; + +import lite.ITLSolver; + +public class SBDDHash extends AbstractMap<ITLSolver,SBDDEntry> { + + SBDDSet set; + SBDDHash() { + set = new SBDDSet(); + } + + + + @Override public boolean containsKey(Object o) { + set.hash = o.hashCode(); + return super.containsKey(o); + } + + @Override public SBDDEntry get(Object o) { + set.hash = o.hashCode(); + return super.get(o); + } + + @Override + public Set<Entry<ITLSolver, SBDDEntry>> entrySet() { + return set; + } + +}
--- a/src/sbdd/SBDDTest.java Mon Jan 14 03:01:45 2008 +0900 +++ b/src/sbdd/SBDDTest.java Mon Jan 14 16:48:48 2008 +0900 @@ -18,9 +18,12 @@ //test.bddTest(); //test.satTest(); - test.verifyTest(); + //test.verifyTest(); + test.mainLoop(); } + + SBDDTest() { sat = new BDDSatisfier(); p = sat.p; @@ -88,8 +91,13 @@ // sat.showVerify("+(a & b)"); //System.out.println(sat.state); sat.p.parse("include('data/example')."); - System.out.println(p.parseCommand.sat.state); + //System.out.println(p.parseCommand.sat.state); } + public void mainLoop() { + BDDSatisfier sat = new BDDSatisfier(); + sat.p.parseFile("data/example"); + sat.p.parse(System.in); + } }