# HG changeset patch # User kono # Date 1200639637 -32400 # Node ID 6b3535ea6958b0e3a6a13325971de29fdc650748 # Parent 40d37728c803cf5aa16c7835e9e63de2cbee8ed7 *** empty log message *** diff -r 40d37728c803 -r 6b3535ea6958 Changes --- a/Changes Fri Jan 18 00:32:39 2008 +0900 +++ b/Changes Fri Jan 18 16:00:37 2008 +0900 @@ -1,5 +1,47 @@ +Fri Jan 18 14:19:49 JST 2008 + +SBDDSet をクリアするには、new SBDDFactory() すれば良いらしい。 +subterms は、既に、ITLSolver (SBDDSet のkey)にセットされていて、 +それをclear するのは難しいが、そのまま放置すれば重なることはない +ので、害はない。 + +new SBDDFactory() して、old SBDDSet の key order を修正して、 +新しくBDDを構築してやれば、key のreorder が可能。key order +を修正しても hash は変わらないので、hash table 中の位置は変 +わらない。と言うことは、variable reorder では、SBDDSet を新 +しく作る必要はないということか... + +ということは、BDDの大きさはHashTable の大きさとは関係ない +ということか! すべてのBDDがHashに登録されるんじゃないの? +reorder で使われなくなるBDDがあるってことなのか。ということは、 +やっぱり、SBDDSet は変更されるということなのね。いや、 +subterm は不変であって、pure BDD term は変わるということか。 +確かに、 +Number of BDD: 223 +Number of Subterm: 81 +なので、Subterm の方が少ない。 + +done in 36751msec +-> show. +All Edges: 283053 +Number of BDD: 1802 +Number of Subterm: 176 +Reachable state: 1366 + +あ、なんか遅くなった。 + Thu Jan 17 23:50:12 JST 2008 +do(20). +done in 18762msec +exe. +0:483: [~empty,al,~ar,~bl,~br,cl,~cr,~dl,~dr,~el,~er] +1:495: [~empty,~bl,~br,ar,al,cl,cr,~dl,~dr,el,~er] +2:515: [~empty,~bl,~br,ar,~al,cr,~cl,~dl,~dr,el,er] +3:565: [~empty,bl,~br,~ar,~al,~cl,~cr,dl,~dr,er,~el] +4:666: [~empty,~al,~ar,~cl,~cr,br,bl,dr,~el,dl,er] +5:1112: [empty,~al,ar,~cl,cr,~bl,br,~dl,dr,~el] + diag, exe も、なんとなく動いているし、MainLoop に、jar のresource からの読み込みも出来たし。ほとんど、終った気がする。いろいろ謎な 部分は残っているけど。 diff -r 40d37728c803 -r 6b3535ea6958 src/lite/ITLCommander.java --- a/src/lite/ITLCommander.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/lite/ITLCommander.java Fri Jan 18 16:00:37 2008 +0900 @@ -1,7 +1,7 @@ package lite; -import java.util.HashMap; import java.util.LinkedList; +import java.util.TreeMap; import parser.Command; @@ -14,20 +14,25 @@ private ITLNodeFactoryInterface lf; private ITLNodeParser parser; public BDDSatisfier sat; - private HashMap examples; + private TreeMap examples; private BDDDiagnosis diag; public ITLCommander(ITLNodeFactoryInterface lf, ITLNodeParser parser) { this.lf = lf; this.parser = parser; - this.examples = new HashMap(); + this.examples = new TreeMap(); parser.addHelp( - "do(p). verify formula p\n"+ + "do(p). verify formula p or a numberd example, try do(10).\n"+ "ex(N,p). register numbered examle p\n"+ + "ls. list predefined example\n"+ "verbose(TF). set verbose mode (true/false)\n"+ "include(File). read from File\n"+ "def('head(p)','body(p)'). define macro\n"+ + "exe. execute last verifed formula\n"+ + "diag. counter example of last verifed formula\n"+ + "clear. clear state database\n"+ + "show. show state statistics\n"+ "help. show this\n"+ "" ); @@ -75,17 +80,19 @@ } 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 == "ls") { + // this is human unreadable... + //for(int i:examples.keySet()) { + // System.out.println(i+":"+examples.get(i)); + //} + parser.showResourceFile("data/example"); } else if (name == "help") { parser.help(); - return lf.trueNode(); } else if (name == "def") { parser.define(args.get(0).toString(),args.get(1).toString()); - return lf.trueNode(); } else if (name == "verbose") { // verbose(true) / verbose(off) Node n= null; @@ -96,24 +103,29 @@ } catch (NumberFormatException e) { sat.verbose = (n==lf.trueNode())?true:false; } - return lf.trueNode(); } else if (name == "include") { String file = args.getFirst().toString(); parser.parseFile(file); - return lf.trueNode(); } else if (name == "exe") { int length = 0; if (args.size()>1) length = Integer.parseInt(args.get(0).toString()); + checkSat(); diag.execute(sat.last, length ); - return lf.trueNode(); } else if (name == "diag") { int length = 0; if (args.size()>1) length = Integer.parseInt(args.get(0).toString()); + checkSat(); diag.counterExample(sat.last, length); - return lf.trueNode(); - } - parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args); - return value; + } else if (name == "clear") { + sat = new BDDSatisfier(); + } else if (name == "states") { + System.out.println(sat.sf.hash); + } else if (name == "show") { + checkSat(); + diag.showState(sat.last); + } else + parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args); + return lf.trueNode(); } private void checkSat() { diff -r 40d37728c803 -r 6b3535ea6958 src/lite/ITLNodeParser.java --- a/src/lite/ITLNodeParser.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/lite/ITLNodeParser.java Fri Jan 18 16:00:37 2008 +0900 @@ -107,6 +107,10 @@ periodNode = logicNodeFactory.variableNode(".", true); define("help","true",50,parseCommand); + define("show","true",50,parseCommand); + define("states","true",50,parseCommand); + define("ls","true",50,parseCommand); + define("clear","true",50,parseCommand); // only one of the is true (should allow all false case?) define("share(L)","[](share0(L))"); define("share0(L)","true",50, new Command() { @@ -149,7 +153,7 @@ dict.reserve("next",TokenID.Next); dict.reserve("proj",TokenID.Projection); - // parseCommand requires reserved word for string comparison + // parseCommand requires compile tme reserved word for string comparison dict.reserve("less"); dict.reserve("ex"); dict.reserve("do"); @@ -159,6 +163,10 @@ dict.reserve("help"); dict.reserve("diag"); dict.reserve("exe"); + dict.reserve("show"); + dict.reserve("ls"); + dict.reserve("states"); + dict.reserve("clear"); } @Override @@ -249,4 +257,5 @@ } + } diff -r 40d37728c803 -r 6b3535ea6958 src/lite/MainLoop.java --- a/src/lite/MainLoop.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/lite/MainLoop.java Fri Jan 18 16:00:37 2008 +0900 @@ -11,6 +11,6 @@ if (!sat.p.getResource("/data/example")) sat.p.parseFile("data/example"); sat.p.help(); - sat.p.parse(System.in); + sat.p.parse(System.in,"-> "); } } diff -r 40d37728c803 -r 6b3535ea6958 src/sbdd/BDDDiagnosis.java --- a/src/sbdd/BDDDiagnosis.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/sbdd/BDDDiagnosis.java Fri Jan 18 16:00:37 2008 +0900 @@ -19,8 +19,6 @@ private SBDDEntry empty_; private SBDDEntry false_; - public boolean falsifiable; - public boolean satisfiable; public TreeSet reachable; public TreeSet trueSet; public TreeSet falseSet; @@ -54,11 +52,7 @@ } /* - * Show found trace. SBDDEntry does not contains choice point set - * i.e. transition condition represented by true/false combination of - * variables. Choice point have to be generated on the fly. Condition - * Edge is 2^(number of variable), so it is not good to have all in - * memory. + * Show found trace. */ private void show(LinkedList trace) { if (trace.isEmpty()) return; @@ -67,10 +61,20 @@ for(SBDDEntry e: trace) { if (e!=last) { System.out.print(i+":"+e.id+":\t"); + // show choice point generated on the fly System.out.println( sat.findNext(e,trace.get(++i))); } } } + + public void showState(SBDDEntry entry) { + System.out.println("All Edges: "+sat.edge); + System.out.println("Number of BDD: "+sat.sf.hash.size()); + System.out.println("Number of Subterm: "+(SBDDSet.subterms-SBDDSet.INITIAL_SUBTERMS)); + makeReachableEntry(entry); + System.out.println("Reachable state: "+reachable.size()); + specialCase(); + } private LinkedList findTrueEntry(SBDDEntry e, int length) { SBDDEntry dest = true_; @@ -150,8 +154,6 @@ //LinkedList> stack = new LinkedList>(); Iterable current = e.nexts(); //stack.add(current); - falsifiable = false; - satisfiable = false; if(e.falsifiable) falseSet.add(e); if(e.satisfiable) trueSet.add(e); reachable.add(e); @@ -169,8 +171,8 @@ if (s==empty_) trueSet.add(s); if (reachable.add(s)) { // this is a new one - falsifiable|=s.falsifiable; if(s.falsifiable) falseSet.add(s); - satisfiable|=s.satisfiable; if(s.satisfiable) trueSet.add(s); + if(s.falsifiable) falseSet.add(s); + if(s.satisfiable) trueSet.add(s); addReachable(s.nexts()); } } diff -r 40d37728c803 -r 6b3535ea6958 src/sbdd/BDDSatisfier.java --- a/src/sbdd/BDDSatisfier.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/sbdd/BDDSatisfier.java Fri Jan 18 16:00:37 2008 +0900 @@ -1,5 +1,6 @@ package sbdd; +import java.util.Date; import java.util.LinkedList; import parser.ExecutorInterface; @@ -11,12 +12,10 @@ import lite.BDDSolver; import lite.Continuation; import lite.ITLNodeFactory; -import lite.ITLNodeFactoryInterface; import lite.ITLNodeParser; import lite.ITLSatisfier; import lite.ITLSolver; import lite.Next; -import lite.VariableSolver; public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface { @@ -29,6 +28,7 @@ public SBDDEntry currentState; public SBDDEntry last; boolean falsifiable,satisfiable; + int edge; /** * Tableau expansion verifier for ITL with Subterm BDD. @@ -46,16 +46,16 @@ public void init() { - lf = new ITLNodeFactory(); - p = new ITLNodeParser((ITLNodeFactoryInterface) lf); + p = new ITLNodeParser(new ITLNodeFactory()); sf = new SBDDFactory(); - // empty = lf.emptyNode(); - // empty = lf.emptyNode(); + edge = 0; } public BDDSatisfier() { init(); - lf = new SBDDFactory(); + lf = sf; // this is strage. + // the parser uses ITLNodeFactory for syntax tree, but in Satisfier, + // SBDDFactory have be used. true_ = SBDDFactory.trueSolver; false_ = SBDDFactory.falseSolver; state = sf.set(); @@ -86,13 +86,13 @@ BDDSolver b = n.toSBDD(sf); System.out.println(s); verify(b); - // System.out.println(sf.hash); System.out.println(); } class AllNext implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { + edge++; if (value!=null) { if (value==true_) satisfiable = true; SBDDEntry e = state.getEntry(value); @@ -110,34 +110,13 @@ } } - public ChoicePointList copy(ChoicePointList cplist) { - ChoicePointList newcp = new ChoicePointList(); - for(ITLSolver cp : cplist) { - newcp.add(new VariableSolver(cp.toString(),cp.value)); - } - return newcp; - } - - class FindNext extends LinkedList> implements Next { - private static final long serialVersionUID = 1L; - public SBDDEntry dest; - FindNext(SBDDEntry dest) { this.dest = dest; } - public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { - if (value!=null&&value!=true_) { - SBDDEntry e = state.getEntry(value); - if (e.expanded) { - add(copy(sat.cp)); - } - } - 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()+" -> "); + edge++; if (value!=null) { if (value==true_) { s="true";satisfiable = true; @@ -160,7 +139,14 @@ } } + /* + * Do tableau expansion on an ITL formula + * use develop to find out all possible next + * store them in SBDDSet. If no more new next + * states, all done. + */ public void verify(ITLSolver n) { + Date start = new Date(); queue = new LinkedList(); Next allNext = verbose? new AllNextVerbose() : new AllNext(); SBDDEntry b = state.getEntry(n); @@ -181,12 +167,21 @@ e.falsifiable = falsifiable; e.satisfiable = satisfiable; if (!verbose) System.out.println(); } + Date end = new Date(); + String time = Long.toString(end.getTime()-start.getTime()); + if (!verbose) System.out.println("done in "+time+"msec"); } public SBDDEntry getEntry(ITLSolver key) { return sf.hash.getEntry(key); } + /* SBDDEntry does not contains choice point set + * i.e. transition condition represented by true/false combination of + * variables. Choice point have to be generated on the fly. Condition + * Edge is 2^(number of variable), so it is not good to have all in + * memory. findNext generate choice point on the fly. + */ class FindOne implements Next { SBDDEntry dest; public ChoicePointList cp; @@ -207,5 +202,30 @@ develop(now.key, findOne); return findOne.cp; } + +// Find all possible choice points +// +// public ChoicePointList copy(ChoicePointList cplist) { +// ChoicePointList newcp = new ChoicePointList(); +// for(ITLSolver cp : cplist) { +// newcp.add(new VariableSolver(cp.toString(),cp.value)); +// } +// return newcp; +//// } +// +// class FindNext extends LinkedList> implements Next { +// private static final long serialVersionUID = 1L; +// public SBDDEntry dest; +// FindNext(SBDDEntry dest) { this.dest = dest; } +// public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { +// if (value!=null&&value!=true_) { +// SBDDEntry e = state.getEntry(value); +// if (e.expanded) { +// add(copy(sat.cp)); +// } +// } +// throw sat.backtrack; +// } +// } } diff -r 40d37728c803 -r 6b3535ea6958 src/sbdd/SBDDSet.java --- a/src/sbdd/SBDDSet.java Fri Jan 18 00:32:39 2008 +0900 +++ b/src/sbdd/SBDDSet.java Fri Jan 18 16:00:37 2008 +0900 @@ -24,7 +24,8 @@ int size = 0; // Multiple SBDDSet is not recomended, but just in case, we make variable // order is shared among existing SBDDSet. - private static int order = 10; + static final int INITIAL_SUBTERMS = 10; + static int subterms = INITIAL_SUBTERMS; SBDDSet() { sbddArray = new SBDDEntry [hashSize]; @@ -99,7 +100,7 @@ lastEntry = null; e.getValue().id = size++; ITLSolver var = ((BDDSolver)e.getKey()).var; - if (var.order==-1) var.order = order ++; + if (var.order==-1) var.order = subterms ++; return true; }