Mercurial > hg > Applications > JavaLite

changeset 70:416e4d272e79 main-loop

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Mon, 14 Jan 2008 16:48:48 +0900
parents 5fd456b0a073
children 01356168f25f
files src/data/example src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDEntry.java src/sbdd/SBDDHash.java src/sbdd/SBDDTest.java
diffstat 7 files changed, 149 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/src/data/example	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/data/example	Mon Jan 14 16:48:48 2008 +0900
@@ -41,7 +41,7 @@
 % dining philosopher
 %   note: unspecified resource increase states
 %   ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * 
-ex0(19,(more,
+ex(19,(more,
 % three philosophers 
         *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
         *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
@@ -63,7 +63,7 @@
 	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
 )). % :-fail.  % too big to verify (sigh...)
 %
-ex0(21,(more,
+ex(21,(more,
 	share([ar,bl]),share([br,cl]),share([cr,dl]),
 	share([dr,el]),share([er,al]),
         *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
@@ -73,7 +73,7 @@
         *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
 true)).  % :-fail.  % too big to verify (sigh...)
 
-ex0(22,(more,
+ex(22,(more,
 %% three philosophers  with no iteration
         ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
         ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
@@ -161,52 +161,52 @@
 def("demo(X,Y)","ex(X,Y)").
 % def("demo(X,Y)","true").
 % length 5 interval
-demo(1, length(5)).
+demo(1001, length(5)).
 
 % p is trun at the top of a interval
-demo(2, (length(5),p)).
+demo(1002, (length(5),p)).
 
 % @ meas next time.
-demo(3, (length(5),@p,@ @q,@ @ @r)).
+demo(1003, (length(5),@p,@ @q,@ @ @r)).
 
 % &(chop) devides an interval into to parts
-demo(4, ((length(2),p)) & (length(3),q)).
+demo(1004, ((length(2),p)) & (length(3),q)).
 
 %  there are several ways of division.
-demo(5, (length(5),(p&q))).
+demo(1005, (length(5),(p&q))).
 
 % sometime usinng chop
-demo(6, (length(5),(true & p))).
+demo(1006, (length(5),(true & p))).
 
 % always: dual of sometime
-demo(7, (length(5),not(true & not(p)))).
+demo(1007, (length(5),not(true & not(p)))).
 
 % counter intutive theorem
-demo(8, '<>' '[]'(p) = '[]'('<>'(p))).
+demo(1008, '<>' '[]'(p) = '[]'('<>'(p))).
 
 % shared resource / exclusive condition
-demo(9, (length(5),
+demo(1009, (length(5),
         '[]'(((    ac ,not(bc),not(cc),not(dc));
             (not(ac),    bc ,not(cc),not(dc));
             (not(ac),not(bc),    cc ,not(dc));
             (not(ac),not(bc),not(cc),    dc ))))).
 
 % periodical task by Projection
-demo(10, (more,
+demo(1010, (more,
 	proj((@ '<>'(q),length(2)),true))).
 
 % time sharing taks by Projection
-demo(11, (more,length(7),
+demo(1011, (more,length(7),
 	proj(true,('[]'(p),length(4))))).
 
 % combination of periodical task
-demo(12, (more,
+demo(1012, (more,
 	proj(length(2),'[]'(ac)),
 	proj(length(3),'[]'(bc)),
 	proj(length(5),'[]'(cc)))).
 
 % periodical task with shared resources
-demo(13, (more,
+demo(1013, (more,
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
 	proj((length(5),@ '<>'(cc)),true),
@@ -214,7 +214,7 @@
 	true)).
 
 % combination of periodical taks and aperiodical task with shared resource
-demo(14, (
+demo(1014, (
 	((proj(true,(length(5),'[]'(dc))),length(15) )&true),
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
@@ -226,7 +226,7 @@
 	true)).
 % combination of periodical taks and aperiodical task with shared resource
 %  schedulable case
-demo(15, (
+demo(1015, (
 	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
@@ -239,14 +239,14 @@
 
 
 % model restriction by share predicate ( a little smaller.... :-)
-demo(16, (
+demo(1016, (
 	share([ac,bc,cc,dc]),
 	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
 	proj((length(5),@ '<>'(cc)),true),
 	true)).
-demo(17, (
+demo(1017, (
 ((proj(true,(length(5),'[]'(c))),length(15))&true),
 (proj((length(3),@ '<>'(a)),true)&less(3)),
 (proj((length(5),@ '<>'(b)),true)&less(5)),
--- a/src/lite/ITLCommander.java	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/lite/ITLCommander.java	Mon Jan 14 16:48:48 2008 +0900
@@ -1,6 +1,8 @@
 package lite;
 
+import java.util.HashMap;
 import java.util.LinkedList;
+
 import sbdd.BDDSatisfier;
 import logicNode.parser.Command;
 
@@ -10,10 +12,12 @@
 	private ITLNodeFactoryInterface<Node> lf;
 	private ITLNodeParser<Node> parser;
 	public BDDSatisfier sat;
+	private HashMap<Integer,Node> examples;
 
 	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
 		this.lf = lf;
 		this.parser = parser;
+		this.examples = new HashMap<Integer,Node>();
 	}
 
 	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
@@ -36,20 +40,44 @@
 				n = lf.orNode(lf.emptyNode(),lf.nextNode(n));
 			}
 			return (Node)n;
-		} else if (name == "ex") {
-			if (sat==null) sat = new BDDSatisfier();
-			// System.out.println(args.get(0)+":"+args.get(1));
-			System.out.println(args.get(0));
-			sat.verify(args.get(1));
-			return lf.trueNode();
+		} else if (name == "ex"|| name=="do") {
+			checkSat();
+			if (args.size()<1) {
+				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
+				return lf.trueNode();
+			}
+			Node n = args.get(0);
+			int index = -1;
+			if (n.getClass()==NumberSolver.class) {
+				index = Integer.parseInt(n.toString()); 
+			}
+			if (args.size()==1) {
+				// System.out.println(args.get(0)+":"+args.get(1));
+				if (index>=0) {
+					n = examples.get(index);
+					if (n==null) {
+						parser.error("Unknown registered example");
+						return lf.trueNode();
+					}
+				}
+				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 == "def") {
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
 		} else if (name == "verbose") {
-			if (Integer.parseInt(args.get(0).toString())==0) {
-				sat.verbose = false;
-			} else {
-				sat.verbose = true;
+			Node n= null;
+			checkSat();
+			try {
+				int i = Integer.parseInt((n=args.get(0)).toString());
+				sat.verbose =  (i==0)? false:true;
+			} catch (NumberFormatException e) {
+				sat.verbose = (n==lf.trueNode())?true:false;
 			}
 			return lf.trueNode();
 		} else if (name == "include") {
@@ -61,4 +89,8 @@
 		return value;
 	}
 
+	private void checkSat() {
+		if (sat==null) sat = new BDDSatisfier();
+	}
+
 }
--- a/src/lite/ITLNodeParser.java	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Mon Jan 14 16:48:48 2008 +0900
@@ -85,6 +85,7 @@
 			define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");
 
 			define("ex(N,Exp)","true",50,parseCommand);
+			define("do(N)","true",50,parseCommand);
 			define("def(Head,Body,Order)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
 			
@@ -139,6 +140,7 @@
 		// parseCommand requires reserved word for string comparison
 		dict.reserve("less");
 		dict.reserve("ex");
+		dict.reserve("do");
 		dict.reserve("include");
 		dict.reserve("def");
 		dict.reserve("verbose");
@@ -250,4 +252,5 @@
 		return emptyNode;
 	}
 
+
 }
--- a/src/sbdd/BDDSatisfier.java	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Mon Jan 14 16:48:48 2008 +0900
@@ -12,8 +12,9 @@
 import lite.ITLSatisfier;
 import lite.ITLSolver;
 import lite.Next;
+import logicNode.parser.ExecutorInterface;
 
-public class BDDSatisfier extends ITLSatisfier {
+public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface<ITLSolver> {
 
 
 	public ITLNodeParser<ITLSolver> p;
@@ -21,6 +22,13 @@
 
 	public  LinkedList<SBDDEntry> queue;
 	public  SBDDSet state;
+	public SBDDEntry currentState;
+	
+
+	private boolean satisfiable;
+	private boolean falsfiable;
+	public SBDDEntry last;
+
 
 	/**
 	 * 
@@ -31,6 +39,7 @@
 	public void init() {
 		lf = new ITLNodeFactory();
 		p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
+		// p.setExecutor(this);
 		sf = new SBDDFactory();
 		// empty = ITLNodeFactory.emptySolver;
 		// empty = SBDDFactory.emptySolver;
@@ -98,14 +107,21 @@
 			String s = "null";
 			System.out.print(" "+sat.choicePoint()+" -> ");
 			if (value!=null) {
-				SBDDEntry e = state.getEntry(value);
-				s = value.toString(); s = Integer.toString(e.id)+":"+s;
-				if (e.expanded) {
+				if (value==true_) {
+					satisfiable = true; s="true";
+				} else {
+					SBDDEntry e = state.getEntry(value);
+					currentState.addNext(e);
+					s = value.toString(); s = Integer.toString(e.id)+":"+s;
+					if (e.expanded) {
 						// skip
-				} else 	{
-					queue.add(e); e.expanded = true;
-					s = "!"+s;
-				} 
+					} else 	{
+						queue.add(e); e.expanded = true;
+						s = "!"+s;
+					} 
+				}
+			} else {
+				falsfiable = true;
 			}
 			System.out.println(s);
 			throw sat.backtrack;
@@ -113,9 +129,12 @@
 	}
 
 	public void verify(ITLSolver n) {
+		falsfiable = false;
+		satisfiable = false;
 		queue = new LinkedList<SBDDEntry>();
 		Next allNext = verbose? new AllNextVerbose() : new AllNext();
 		SBDDEntry b = state.getEntry(n);
+		last = b;
 		if (b.expanded) {
 			// already checked
 			System.out.println("   already checked.");
@@ -124,10 +143,18 @@
 		queue.add(b); b.expanded = true;
 		for(SBDDEntry e;(e = queue.poll())!=null; ) {
 			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
+			currentState = e;
 			develop(e.key, allNext);
 			if (!verbose) System.out.println();
 		}
+		if (!verbose) {
+			if (!falsfiable) {
+				System.out.println("valid");
+			}
+			if (!satisfiable) {
+				System.out.println("unsatisfiable");
+			}
+		}
 	}
-		
 	
 }
--- a/src/sbdd/SBDDEntry.java	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/sbdd/SBDDEntry.java	Mon Jan 14 16:48:48 2008 +0900
@@ -7,6 +7,7 @@
 import java.util.Map.Entry;
 
 
+
 public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> {
 
 	public ITLSolver key;
@@ -16,6 +17,7 @@
 	
 	public SBDDEntry(ITLSolver now) {
 		this.key = now;
+		nexts = new LinkedList<SBDDEntry>();
 	}
 
 	public boolean	equals(Object e0) {
@@ -42,5 +44,9 @@
 		return this;
 	}
 	
+	public boolean addNext(SBDDEntry e) {
+		if (nexts.contains(e)) return false;
+		return nexts.add(e);
+	}
 
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDHash.java	Mon Jan 14 16:48:48 2008 +0900
@@ -0,0 +1,32 @@
+package sbdd;
+
+import java.util.AbstractMap;
+import java.util.Set;
+
+import lite.ITLSolver;
+
+public class SBDDHash extends AbstractMap<ITLSolver,SBDDEntry> {
+
+	SBDDSet set;
+	SBDDHash() {
+		set = new SBDDSet();
+	}
+	
+	
+
+	@Override public boolean containsKey(Object o) {
+		set.hash = o.hashCode();
+		return super.containsKey(o);
+	}
+	
+	@Override public SBDDEntry get(Object o) {
+		set.hash = o.hashCode();
+		return super.get(o);
+	}
+
+	@Override
+	public Set<Entry<ITLSolver, SBDDEntry>> entrySet() {
+		return set;
+	}
+
+}
--- a/src/sbdd/SBDDTest.java	Mon Jan 14 03:01:45 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Mon Jan 14 16:48:48 2008 +0900
@@ -18,9 +18,12 @@
 		
 		//test.bddTest();
 		//test.satTest();
-		test.verifyTest();
+		//test.verifyTest();
+		test.mainLoop();
 	}
 	
+	
+	
 	SBDDTest() {
 		sat = new BDDSatisfier();
 		p = sat.p;
@@ -88,8 +91,13 @@
 		// sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
 		sat.p.parse("include('data/example').");
-		System.out.println(p.parseCommand.sat.state);
+		//System.out.println(p.parseCommand.sat.state);
 	}
 
+	public void mainLoop() {
+		BDDSatisfier sat = new BDDSatisfier();
+		sat.p.parseFile("data/example");
+		sat.p.parse(System.in);
+	}
 		
 }