Mercurial > hg > Applications > JavaLite

changeset 46:bdb6f31782d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Sun, 06 Jan 2008 08:58:07 +0900
parents 0258fcdf488c
children cbe1b120cb53
files src/lite/BDDSolver.java src/lite/ChopSolver.java src/lite/EmptySolver.java src/lite/ExistsSolver.java src/lite/FalseSolver.java src/lite/ITLSolver.java src/lite/NextSolver.java src/lite/ProjectionSolver.java src/lite/TrueSolver.java src/lite/VariableSolver.java
diffstat 10 files changed, 77 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/BDDSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/BDDSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -12,8 +12,6 @@
 	public ITLSolver var;
 	public BDDSolver high; // true
 	public BDDSolver low;  // flase
-	public int hash;
-	
 	public BDDID id;
 	
 	
@@ -48,7 +46,17 @@
 		this.id = id;
 	}
 
+	public BDDSolver(ITLSolver v, BDDID id, int hash) {
+		this(v,null,null);
+		this.id = id;
+		this.hash = hash;
+	}
+
 	public String toString() {
+		if (var==null) {
+			if (id!=null) return id.toString();
+			else return "null";
+		}
 		return var.toString();
 	}
 	
@@ -166,8 +174,25 @@
 		return this;
 	}
 	
+
+    static final int PAIR(int a, int b) {
+        return ((a + b) * (a + b + 1) / 2 + a);
+    }
+    static final int TRIPLE(int a, int b, int c) {
+        return (PAIR(c, PAIR(a, b)));
+    }
+
+    static final int NODEHASH(int lvl, int l, int h) {
+        return Math.abs(TRIPLE(lvl, l, h));
+    }
+	
 	public int hashCode() {
-		return this.hash;
+		if (hash!=-1) return hash;
+		switch(id) {
+		case BDD: return hash = NODEHASH(var.hashCode(),low.hashCode(),high.hashCode());
+		default:
+			return hash = var.hashCode();
+		}
 	}
 
 	public BDDSolver high() {
--- a/src/lite/ChopSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/ChopSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -143,4 +144,9 @@
 	public boolean isModal() {
 		return true;
 	}
+	
+	public int hashCode() {
+		if (hash!=-1) return hash;
+		return hash = BDDSolver.NODEHASH(TokenID.Chop.hash,former.hashCode(),later.hashCode());
+	}
 }
--- a/src/lite/EmptySolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/EmptySolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -21,4 +22,8 @@
 	public boolean isModal() {
 		return true;
 	}
+	
+	public int hashCode() {
+		return TokenID.Empty.hash;
+	}
 }
--- a/src/lite/ExistsSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/ExistsSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -2,6 +2,8 @@
 
 import java.util.LinkedList;
 
+import logicNode.parser.TokenID;
+
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -92,4 +94,10 @@
 	public boolean isModal() {
 		return true;
 	}
+	
+
+	public int hashCode() {
+		if (hash!=-1) return hash;
+		return hash = BDDSolver.NODEHASH(TokenID.Exists.hash,var.hashCode(),node.hashCode());
+	}
 }
--- a/src/lite/FalseSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/FalseSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -22,4 +23,8 @@
 	public boolean isModal() {
 		return true;
 	}
+
+	public int hashCode() {
+		return TokenID.False.hash;
+	}
 }
--- a/src/lite/ITLSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/ITLSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -12,7 +12,7 @@
 public class ITLSolver extends LogicNode
 	implements MacroNodeInterface<ITLSolver>,Next,BDDInterface {
 	
-	public int hash;
+	public int hash=-1;
 	
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return null;
--- a/src/lite/NextSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/NextSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -34,4 +35,10 @@
 	public boolean isModal() {
 		return true;
 	}
+	
+
+	public int hashCode() {
+		if (hash!=-1) return hash;
+		return hash = BDDSolver.NODEHASH(TokenID.Next.hash,node.hashCode(),0);
+	}
 }
--- a/src/lite/ProjectionSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/ProjectionSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -93,4 +94,9 @@
 	public boolean isModal() {
 		return true;
 	}
+
+	public int hashCode() {
+		if (hash!=-1) return hash;
+		return hash = BDDSolver.NODEHASH(TokenID.Projection.hash,clock.hashCode(),interval.hashCode());
+	}
 }
--- a/src/lite/TrueSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/TrueSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import logicNode.parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
@@ -23,4 +24,9 @@
 	public boolean isModal() {
 		return true;
 	}
+	
+
+	public int hashCode() {
+		return TokenID.True.hash;
+	}
 }
--- a/src/lite/VariableSolver.java	Sat Jan 05 21:25:50 2008 +0900
+++ b/src/lite/VariableSolver.java	Sun Jan 06 08:58:07 2008 +0900
@@ -50,4 +50,9 @@
 		return sf.variableNode(name, value).toSBDD(sf);
 	}
 	
+	public int hashCode() {
+		if (hash!=-1) return hash;
+		return hash = name.hashCode();
+	}
+	
 }