changeset 88:6b3535ea6958

*** empty log message ***
author kono
date Fri, 18 Jan 2008 16:00:37 +0900
parents 40d37728c803
children aed27c25859e
files Changes src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/lite/MainLoop.java src/sbdd/BDDDiagnosis.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDSet.java
diffstat 7 files changed, 147 insertions(+), 61 deletions(-) [+]
line wrap: on
line diff
--- 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
 からの読み込みも出来たし。ほとんど、終った気がする。いろいろ謎な
 部分は残っているけど。
--- 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<Node> lf;
 	private ITLNodeParser<Node> parser;
 	public BDDSatisfier sat;
-	private HashMap<Integer,Node> examples;
+	private TreeMap<Integer,Node> examples;
 	private BDDDiagnosis diag;
 
 	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
 		this.lf = lf;
 		this.parser = parser;
-		this.examples = new HashMap<Integer,Node>();
+		this.examples = new TreeMap<Integer,Node>();
 		
 		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() {
--- 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<Node>() {
@@ -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 @@
 	}
 
 
+
 }
--- 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,"-> ");
 	}
 }
--- 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<SBDDEntry> reachable;
 	public TreeSet<SBDDEntry> trueSet;
 	public TreeSet<SBDDEntry> 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<SBDDEntry> 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<SBDDEntry> findTrueEntry(SBDDEntry e, int length) {
 		SBDDEntry dest = true_;
@@ -150,8 +154,6 @@
 		//LinkedList<Iterable<SBDDEntry>> stack = new LinkedList<Iterable<SBDDEntry>>();
 		Iterable<SBDDEntry> 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());
 			}
 		}
--- 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<ITLSolver> {
 
@@ -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<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
+		p = new ITLNodeParser<ITLSolver>(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<ITLSolver> copy(ChoicePointList<ITLSolver> cplist) {
-		ChoicePointList<ITLSolver> newcp = new ChoicePointList<ITLSolver>();
-		for(ITLSolver cp : cplist) {
-			newcp.add(new VariableSolver(cp.toString(),cp.value));
-		}
-		return newcp;
-	}
-	
-	class FindNext extends LinkedList<ChoicePointList<ITLSolver>> 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<SBDDEntry>();
 		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<ITLSolver> cp;
@@ -207,5 +202,30 @@
 		develop(now.key, findOne);
 		return findOne.cp;
 	}
+
+//  Find all possible choice points
+//	
+//	public ChoicePointList<ITLSolver> copy(ChoicePointList<ITLSolver> cplist) {
+//		ChoicePointList<ITLSolver> newcp = new ChoicePointList<ITLSolver>();
+//		for(ITLSolver cp : cplist) {
+//			newcp.add(new VariableSolver(cp.toString(),cp.value));
+//		}
+//		return newcp;
+////	}
+//	
+//	class FindNext extends LinkedList<ChoicePointList<ITLSolver>> 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;
+//		}
+//	}
 	
 }
--- 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;
 	}