Mercurial > hg > Applications > JavaLite

changeset 59:f97d0d631992

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Wed, 09 Jan 2008 12:40:01 +0900
parents 4102a550bd52
children ff125345619d
files src/data/example src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/sbdd/SBDDSet.java src/sbdd/SBDDTest.java
diffstat 5 files changed, 58 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/src/data/example	Tue Jan 08 17:01:21 2008 +0900
+++ b/src/data/example	Wed Jan 09 12:40:01 2008 +0900
@@ -41,40 +41,40 @@
 % dining philosopher
 %   note: unspecified resource increase states
 %   ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * 
-ex(19,(more,
-% three philosophers 
-        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
-        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
-        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
-% shared resources
-	'[]'( ~ ( ar, bl)),
-	'[]'( ~ ( br, cl)),
-	'[]'( ~ ( cr, al))
-)).
-ex(20,(more,
-% five philosophers 
-        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
-        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
-        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
-        *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
-        *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
-% shared resources
-	'[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
-	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
-)). % :-fail.  % too big to verify (sigh...)
-
-ex(21,(more,
-	share([ar,bl]),share([br,cl]),share([cr,dl]),
-	share([dr,el]),share([er,al]),
-        *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
-        *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
-        *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
-        *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
-        *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
-true)).  % :-fail.  % too big to verify (sigh...)
+%ex(19,(more,
+%% three philosophers 
+%        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
+%        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
+%        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
+%% shared resources
+%	'[]'( ~ ( ar, bl)),
+%	'[]'( ~ ( br, cl)),
+%	'[]'( ~ ( cr, al))
+%)).
+%ex(20,(more,
+%% five philosophers 
+%        *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
+%        *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
+%        *( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
+%        *( ('[]'((~dl, ~dr)) & @ (dl, ~dr,@ (dl,dr, @ (dr,'[]'( ~dl)))) ;empty) ) ,
+%        *( ('[]'((~el, ~er)) & @ (el, ~er,@ (el,er, @ (er,'[]'( ~el)))) ;empty) ) ,
+%% shared resources
+%	'[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)),
+%	'[]'( ~ ( dr, el)), '[]'( ~ ( er, al))
+%)). % :-fail.  % too big to verify (sigh...)
+%
+%ex(21,(more,
+%	share([ar,bl]),share([br,cl]),share([cr,dl]),
+%	share([dr,el]),share([er,al]),
+%        *( ((true && '[]'(al) && '[]'((al,ar)) && '[]'(ar));empty) ) ,
+%        *( ((true && '[]'(bl) && '[]'((bl,br)) && '[]'(br));empty) ) ,
+%        *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) ,
+%        *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) ,
+%        *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
+%true)).  % :-fail.  % too big to verify (sigh...)
 
 ex(22,(more,
-% three philosophers  with no iteration
+%% three philosophers  with no iteration
         ( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
         ( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
         ( ('[]'((~cl, ~cr)) & @ (cl, ~cr,@ (cl,cr, @ (cr,'[]'( ~cl)))) ;empty) ) ,
@@ -100,7 +100,7 @@
 
 ex(110,(more-> (more&more))).                   	%   our dense time
 
-ex(demo(X),Y) :- demo(X,Y).
+% ex(demo(X),Y) :- demo(X,Y).
 % Regular variable examples ( doesnot work now....)
 
 ex(200,^r).
@@ -139,9 +139,9 @@
 
 % State Diagram Support
 
-ex(300,(((length(2), @ '<>'(q)) proj true),
-      st(ns0)
-      )) :- ensure_loaded(kiss_ex).
+%ex(300,(((length(2), @ '<>'(q)) proj true),
+%      st(ns0)
+%      )) :- ensure_loaded(kiss_ex).
 
 % Infinite Interval
 
@@ -152,13 +152,13 @@
 ex(404,~('<>'(empty))).
 ex(405,('<>'(empty))).   % unsatisfiable 
 ex(406,(infinite-> @infinite)).
-ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
+% ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
 ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))).  % satisfiable
 ex(409,finite).   % unsatisfiable
 
 
-demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
-
+% demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
+def("demo(X,Y)","true").
 % length 5 interval
 demo(1, length(5)).
 
--- a/src/lite/ITLCommander.java	Tue Jan 08 17:01:21 2008 +0900
+++ b/src/lite/ITLCommander.java	Wed Jan 09 12:40:01 2008 +0900
@@ -8,11 +8,8 @@
 
 
 	private ITLNodeFactoryInterface<Node> lf;
-	
-	BDDSatisfier sat;
-
 	private ITLNodeParser<Node> parser;
-
+	public BDDSatisfier sat;
 
 	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
 		this.lf = lf;
@@ -21,14 +18,14 @@
 
 	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
 		if (predicate.toString() == "length") {
-			Node n = lf.trueNode();
+			Node n = lf.emptyNode();
 			int length = Integer.parseInt(args.get(0).toString());
 			for(int i =0;i<length;i++) {
 				n = lf.nextNode(n);
 			}
 			return (Node)n;
 		} else if (predicate.toString() == "less") {
-			Node n = lf.trueNode();
+			Node n = lf.falseNode();
 			int length = Integer.parseInt(args.get(0).toString());
 			for(int i =0;i<length;i++) {
 				n = lf.orNode(lf.emptyNode(),lf.nextNode(n));
--- a/src/lite/ITLNodeParser.java	Tue Jan 08 17:01:21 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Wed Jan 09 12:40:01 2008 +0900
@@ -13,7 +13,7 @@
 
 	public ITLNodeFactoryInterface<Node> logicNodeFactory;
 	public ITLNodeScanner<Node> scanner;
-	private Command<Node> parseCommand;
+	public ITLCommander<Node> parseCommand;
 	public Node emptyNode;
 	
 	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
@@ -45,8 +45,8 @@
 			define("skip"," @(empty))");                            // 1 length interval
 			define("infinite"," (true & false))");                  // 
 			define("finite"," ~((true & false)))");                 // 
-			// define("length(I)", "true",50,parseCommand);            // length operator
-			define("length(I)", "true",50,                          // length operator
+			// define("length(I)", "true",50,command);            // length operator
+			define("length(I)", "empty",50,                          // length operator
 					new Command<Node>() {
 						public Node exec(Node predicate, Node value, LinkedList<Node> args) {
 	                        Node n = value;
@@ -57,7 +57,7 @@
 	                        return (Node)n;
 						}
 			});
-			define("less(I)","true",50,parseCommand);               // less than N length
+			define("less(I)","false",50,parseCommand);               // less than N length
 			define("next(P)","(empty; @(P)))");
 // temporal assignments
 			define("gets(A,B)","keep(@A<->B))");
@@ -83,6 +83,8 @@
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("def(Head,Body,Order)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
+			
+			define("^(r)","r"); // interval variable (we cannot handle now)
 
 	}
 
@@ -155,7 +157,7 @@
 		}
 		return arg;
 	}
-	
+	/*
 	@Override
 	protected Node term() {
 		Node n;
@@ -178,7 +180,7 @@
 		nextToken();
 		return n;
 	}
-
+     */
 	public ITLSolver emptyNode() {
 		return emptyNode;
 	}
--- a/src/sbdd/SBDDSet.java	Tue Jan 08 17:01:21 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Wed Jan 09 12:40:01 2008 +0900
@@ -12,7 +12,7 @@
 	public SBDDEntry[] sbddArray ;
 	public int hash;
 	private int hash0;
-	private int hashSize = 1024;
+	private int hashSize = 1024*256;
 	public Object lastEntry;
 	SBDDFactory sf;
 	int size = 0;
--- a/src/sbdd/SBDDTest.java	Tue Jan 08 17:01:21 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Wed Jan 09 12:40:01 2008 +0900
@@ -5,7 +5,6 @@
 import lite.ITLNodeParser;
 import lite.ITLSolver;
 
-
 public class SBDDTest {
 
 
@@ -42,11 +41,16 @@
 		sat.showAllNext("true&q");
 		sat.showAllNext("~(true& ~q)");
 		sat.showAllNext("proj(length(3),<>(p))");
+		
 
 	}
 	
 	public void verifyTest() {
+		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");
+
 		if (true) {
+		sat.showVerify("skip");
+		sat.showVerify(" '<>'p");
 		sat.showVerify("<>(p) = <>(p)");
 		sat.showVerify("~(@(q))");
 		sat.showVerify("p&q");
@@ -58,8 +62,9 @@
 		sat.showVerify("fin(p)=([](<>(p)))");
 		}
 		sat.showVerify("fin(p)");
+		System.out.println(sat.state);
 		sat.p.parse("include('data/example').");
-		System.out.println(sat.state);
+		System.out.println(p.parseCommand.sat.state);
 	}