Mercurial > hg > Applications > JavaLite

changeset 97:07a36431aa14

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Sat, 19 Jan 2008 00:45:24 +0900
parents 116a6afd11aa
children 5bd5c58edfd0
files src/lite/ITLCommander.java src/sbdd/BDDDiagnosis.java
diffstat 2 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/ITLCommander.java	Fri Jan 18 23:41:38 2008 +0900
+++ b/src/lite/ITLCommander.java	Sat Jan 19 00:45:24 2008 +0900
@@ -111,7 +111,8 @@
 			checkSat();
 			diag.counterExample(sat.last, length);
 		} else if (name == "clear") {
-			sat = new BDDSatisfier();
+			sat = null;
+			checkSat();
 		} else if (name == "states") {
 			// System.out.println(sat.sf.hash); too large
 			for(SBDDEntry e: sat.sf.hash.sbddArray) {
--- a/src/sbdd/BDDDiagnosis.java	Fri Jan 18 23:41:38 2008 +0900
+++ b/src/sbdd/BDDDiagnosis.java	Sat Jan 19 00:45:24 2008 +0900
@@ -29,6 +29,7 @@
 		this.true_ = sat.getEntry(sat.true_);
 		this.false_ = sat.getEntry(sat.false_);
 		this.empty_ = sat.getEntry(sat.empty);
+		last = true_;
 	}
 
 	public void execute(SBDDEntry e,int length) {
@@ -71,6 +72,7 @@
 		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));
+		if (last==null) return;
 		makeReachableEntry(entry);
 		System.out.println("Reachable state: "+reachable.size());
 		specialCase();