Mercurial > hg > Applications > JavaLite

changeset 42:ddd38f16b014 sbdd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
SBDD
author kono
date Sat, 05 Jan 2008 09:47:04 +0900
parents a6b6e2ea7792
children 089665ec08ee
files src/lite/AndSolver.java 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/NotSolver.java src/lite/NumberSolver.java src/lite/OrSolver.java src/lite/PredicateSolver.java src/lite/ProjectionSolver.java src/lite/TrueSolver.java src/lite/VariableSolver.java
diffstat 15 files changed, 329 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/AndSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/AndSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 
@@ -50,5 +51,10 @@
 			}
 		}
 	}
+
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return left.toSBDD(sf).and(sf, right.toSBDD(sf));
+	}
+
 	
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/BDDSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -0,0 +1,160 @@
+package lite;
+
+import sbdd.SBDDFactory;
+import verifier.Backtrack;
+
+public class BDDSolver extends ITLSolver {
+	
+	/*
+	 * var?high:low
+	 */
+	public ITLSolver var;
+	public BDDSolver high; // true
+	public BDDSolver low;  // flase
+	public int hash;
+	
+	
+	public BDDSolver(ITLSolver var, BDDSolver high, BDDSolver low) {
+		this.var = var;
+		this.high = high;
+		this.low  = low;
+	}
+
+	public BDDSolver(ITLSolver var, ITLSolver high, ITLSolver low) {
+		this.var = var;
+		this.high = (BDDSolver) high;
+		this.low  = (BDDSolver) low;
+	}
+
+	public String toString() {
+		/*
+		if (var==SBDDFactory.trueSolver) {
+			return "true";
+		} else if (var==SBDDFactory.falseSolver ) {
+			return "false";
+		} else if (var==SBDDFactory.chopSolver  ) {
+			return "("+high+" & "+low+")";
+		} else if (var==SBDDFactory.existsSolver) {
+			return "exists("+high+" , "+low+")";
+		} else if (var==SBDDFactory.nextSolver  ) {
+			return "@("+high+")";
+		} else if (var==SBDDFactory.emptySolver ) {
+			return "empty";
+		} else if (var==SBDDFactory.projSolver  ) {
+			return "proj("+high+" , "+low+")";
+		} */
+		return var.toString();
+	}
+	
+	public boolean value() {
+		return var.value()? high.value() : low.value();
+	}
+
+
+	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		return var.sat(sat, new Continuation(sat,next,this));
+	}
+
+	@Override
+	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+		if (value==null) {
+			return low.sat(sat, next);
+		} else if (value==ITLSatisfier.true_) {
+			return high.sat(sat, next);
+		} else {
+			return high.sat(sat, new Continuation(sat,next,
+					new BDDSolver2(value)));
+		}
+	}
+
+	class BDDSolver2 implements Next {
+		ITLSolver cond;
+		public BDDSolver2(ITLSolver value) {
+			cond = value;
+		}
+
+		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
+			return low.sat(sat, new Continuation(sat,next,
+					new BDDSolver3(cond,value)));
+		}
+	}
+
+	class BDDSolver3 implements Next {
+		ITLSolver cond, high;
+		public BDDSolver3(ITLSolver cond, ITLSolver value) {
+			this.cond = cond;
+			high = value;
+		}
+
+		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver low) throws Backtrack {
+			if (low==ITLSatisfier.true_ && high==ITLSatisfier.true_) 
+				return next.sat(low);
+			if (low==null && high==null) 
+				return next.sat(null);
+			if (low == high) {
+				return next.sat(low);
+			} else {
+				// lf.bddNode(cond,high,low) won't work
+				return next.sat(sat.lf.orNode(
+						sat.lf.andNode(cond, high),
+						sat.lf.andNode(sat.lf.notNode(cond), low)));
+			}
+		}
+	}
+
+
+	BDDSolver and(SBDDFactory sf,BDDSolver right) {
+		BDDSolver lvar=var.toSBDD(sf),rvar=right.var.toSBDD(sf);
+		switch(order(lvar,rvar)) {
+		case 0:
+			return sf.bddNode(lvar,high.and(sf,right.high),low.and(sf,right.low));
+		case 1:
+			return right.and(sf,this);
+		case -1:
+		default:
+			return sf.bddNode(lvar,high.and(sf,right),low.and(sf,right));
+		}
+	}
+
+	BDDSolver or(SBDDFactory sf,BDDSolver right) {
+		BDDSolver lvar=var.toSBDD(sf),rvar=right.var.toSBDD(sf);
+		switch(order(lvar,rvar)) {
+		case 0:
+			return sf.bddNode(lvar,high.or(sf,right.high),low.or(sf,right.low));
+		case 1:
+			return right.or(sf,this);
+		case -1:
+		default:
+			return sf.bddNode(lvar,high.or(sf,right),low.or(sf,right));
+		}
+	}
+
+
+	BDDSolver not(SBDDFactory sf) {
+		return  sf.bddNode(var.toSBDD(sf),low.toSBDD(sf),high.toSBDD(sf));
+	}
+
+	int order(BDDSolver a,BDDSolver b) {
+		return a.toString().compareTo(b.toString());
+	}
+	
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return this;
+	}
+	
+	public int hashCode() {
+		return this.hash;
+	}
+
+	public BDDSolver high() {
+		return high;
+	}
+
+	public BDDSolver low() {
+		return low;
+	}
+
+	public ITLSolver var() {
+		return var;
+	}
+}
--- a/src/lite/ChopSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/ChopSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class ChopSolver extends ITLSolver {
@@ -8,6 +9,7 @@
 	private ITLSolver later;
 	private VariableSolver innerEmpty;
 	private ITLSolver outerEmpty;
+	ITLSolver later1;
 
 	/*
 	 *    Interval Temporal Logic Chop Operator
@@ -25,13 +27,13 @@
 	 *   
 	 *   case 2  inner empty (outer ~ empty)
 	 *   former (t/f)
-	 *   later  (t/f)
+	 *   later  (t/f/@later)
 	 *   ||----------------------------|
 	 *   next:   @later
 	 *       
 	 *   case 3  inner more
-	 *   former (t/f)
-	 *       later (t/f)
+	 *   former (t/f/@former)
+	 *       later
 	 *   |--|--------------------------|
 	 *   next:   @former&later
 	 *   
@@ -113,17 +115,13 @@
 				return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
 			} else {
 				// try innerMore case with this next term
-				return former.sat(sat,  new Continuation(sat,next, new ChopSolver6(value)));
+				later1 = value;
+				return former.sat(sat,  new Continuation(sat,next, new ChopSolver6()));
 			}
 		}
 	}
 	
 	class ChopSolver6 implements Next {
-		ITLSolver later1;
-		public ChopSolver6(ITLSolver value) {
-			later1 = value;
-		}
-
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			sat.restoreEmpty(outerEmpty); // all done
 			if (value==null) {  // former is fail on more inerval
@@ -136,4 +134,20 @@
 			}
 		}
 	}
+
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.chopNode(former.toSBDD(sf), later.toSBDD(sf));
+	}
+
+	public BDDSolver high() {
+		return (BDDSolver)former;
+	}
+
+	public BDDSolver low() {
+		return (BDDSolver)later;
+	}
+
+	public ITLSolver var() {
+		return SBDDFactory.chopSolver;
+	}
 }
--- a/src/lite/EmptySolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/EmptySolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class EmptySolver extends ITLSolver {
@@ -12,4 +13,20 @@
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return sat.empty.sat(sat, next);
 	}
+
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.emptyNode();
+	}
+
+	public BDDSolver high() {
+		return SBDDFactory.trueSolver;
+	}
+
+	public BDDSolver low() {
+		return SBDDFactory.falseSolver;
+	}
+
+	public ITLSolver var() {
+		return SBDDFactory.emptySolver;
+	}
 }
--- a/src/lite/ExistsSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/ExistsSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -2,6 +2,7 @@
 
 import java.util.LinkedList;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class ExistsSolver extends ITLSolver {
@@ -9,6 +10,7 @@
 	ITLSolver node;
 	ITLSolver var;
 	LinkedList<ITLSolver> oldVarList;
+	ITLSolver residue;
 
 	public ExistsSolver(ITLSolver var, ITLSolver node) {
 		this.node = node;
@@ -55,17 +57,13 @@
 			return next.sat(sat.true_());
 		} else {
 			var.setValue(false);
+			residue = value;
 			return node.sat(sat, new Continuation(sat,next,
-					new ExistsSolver2(value)));
+					new ExistsSolver2()));
 		}
 	}
 
 	class ExistsSolver2 implements Next {
-		ITLSolver residue;
-		public ExistsSolver2(ITLSolver value) {
-			residue = value;
-		}
-
 		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
 			restoreLocal(sat);
 			if (value==null) {
@@ -85,4 +83,19 @@
 			return next.sat(value);
 		}
 	}
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.existsNode(var.toSBDD(sf), node.toSBDD(sf));
+	}
+
+	public BDDSolver high() {
+		return (BDDSolver)var;
+	}
+
+	public BDDSolver low() {
+		return (BDDSolver)node;
+	}
+
+	public ITLSolver var() {
+		return SBDDFactory.existsSolver;
+	}
 }
--- a/src/lite/FalseSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/FalseSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class FalseSolver extends ITLSolver {
@@ -14,4 +15,8 @@
 		return "false";
 	}
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.falseNode();
+	}
+
 }
--- a/src/lite/ITLSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/ITLSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -5,11 +5,19 @@
 import logicNode.LogicNode;
 import logicNode.MacroNodeInterface;
 
+import sbdd.BDDInterface;
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class ITLSolver extends LogicNode
-	implements MacroNodeInterface<ITLSolver>,Next {
+	implements MacroNodeInterface<ITLSolver>,Next,BDDInterface {
+	
+	public int hash;
 
+	ITLSolver() {
+		hash = this.hashCode();
+	}
+	
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return null;
 	}
@@ -49,5 +57,23 @@
 		return false;
 	}
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return null;
+	}
 
+	public BDDSolver high() {
+		return null;
+	}
+
+	public BDDSolver low() {
+		return null;
+	}
+
+	public ITLSolver var() {
+		return null;
+	}
+	
+	public int hashCode() {
+		return hash;
+	}
 }
--- a/src/lite/NextSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/NextSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class NextSolver extends ITLSolver {
@@ -27,4 +28,19 @@
 		}
 	}
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.nextNode(node.toSBDD(sf));
+	}
+
+	public BDDSolver high() {
+		return (BDDSolver)node;
+	}
+
+	public BDDSolver low() {
+		return (BDDSolver)node;
+	}
+
+	public ITLSolver var() {
+		return SBDDFactory.nextSolver;
+	}
 }
--- a/src/lite/NotSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/NotSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 
@@ -31,4 +32,8 @@
 		return next.sat(sat.lf.notNode(value));
 	}
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return node.toSBDD(sf).not(sf);
+	}
+
 }
--- a/src/lite/NumberSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/NumberSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+
 public class NumberSolver extends ITLSolver {
 
 	int num;
@@ -11,4 +12,5 @@
 	public String toString() {
 		return Integer.toString(num);
 	}
+
 }
--- a/src/lite/OrSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/OrSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class OrSolver extends ITLSolver {
@@ -52,4 +53,7 @@
 		}
 	}
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return left.toSBDD(sf).or(sf, right.toSBDD(sf));
+	}
 }
--- a/src/lite/PredicateSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/PredicateSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -2,7 +2,6 @@
 
 import java.util.LinkedList;
 
-
 public class PredicateSolver extends ITLSolver {
 
 	private LinkedList<ITLSolver> arg;
--- a/src/lite/ProjectionSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/ProjectionSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,10 +1,12 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class ProjectionSolver extends ITLSolver {
 
 	ITLSolver clock,interval;
+	ITLSolver clock1;
 
 	/*
 	 *      On interval's every clock, clock is true on clock's sub clock.
@@ -66,17 +68,13 @@
 				return next.sat(value);
 			} else {
 				// try interval keeping @clock
-				return interval.sat(sat, new Continuation(sat,next, new ProjectionSolver3(value)));
+				clock1 = value;
+				return interval.sat(sat, new Continuation(sat,next, new ProjectionSolver3()));
 			}
 		}
 	}
 	
 	class ProjectionSolver3 implements Next {
-		ITLSolver clock1;
-		public ProjectionSolver3(ITLSolver value) {
-			clock1 = value;
-		}
-
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			if (value==null) {  // interval is failed, return null
 				return next.sat(value);
@@ -87,4 +85,20 @@
 			}
 		}
 	}
+
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.projectionNode(clock.toSBDD(sf),interval.toSBDD(sf));
+	}
+
+	public BDDSolver high() {
+		return (BDDSolver)clock;
+	}
+
+	public BDDSolver low() {
+		return (BDDSolver)interval;
+	}
+
+	public ITLSolver var() {
+		return SBDDFactory.projSolver;
+	}
 }
--- a/src/lite/TrueSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/TrueSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class TrueSolver extends ITLSolver {
@@ -15,4 +16,8 @@
 	}
 
 
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.trueNode();
+	}
+
 }
--- a/src/lite/VariableSolver.java	Fri Jan 04 12:07:12 2008 +0900
+++ b/src/lite/VariableSolver.java	Sat Jan 05 09:47:04 2008 +0900
@@ -1,5 +1,6 @@
 package lite;
 
+import sbdd.SBDDFactory;
 import verifier.Backtrack;
 
 public class VariableSolver extends ITLSolver {
@@ -43,4 +44,23 @@
 			}
 		}
 	}
+	
+
+	public BDDSolver toSBDD(SBDDFactory sf) {
+		return sf.variableNode(name, value);
+	}
+	
+
+
+	public BDDSolver high() {
+		return SBDDFactory.trueSolver;
+	}
+
+	public BDDSolver low() {
+		return SBDDFactory.falseSolver;
+	}
+
+	public ITLSolver var() {
+		return this;
+	}
 }