Mercurial > hg > Applications > JavaLite

changeset 69:5fd456b0a073

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 03:01:45 +0900
parents e769488a5d78
children 416e4d272e79
files src/data/example src/lite/ITLNodeParser.java src/sbdd/SBDDFactory.java src/sbdd/SBDDTest.java
diffstat 4 files changed, 26 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/data/example	Mon Jan 14 03:01:42 2008 +0900
+++ b/src/data/example	Mon Jan 14 03:01:45 2008 +0900
@@ -41,7 +41,7 @@
 % dining philosopher
 %   note: unspecified resource increase states
 %   ex ((true & al,skip & al,ar,skip & ar,~al,skip) ;empty) * 
-ex(19,(more,
+ex0(19,(more,
 % three philosophers 
         *( ('[]'((~al, ~ar)) & @ (al, ~ar,@ (al,ar, @ (ar,'[]'( ~al)))) ;empty) ) ,
         *( ('[]'((~bl, ~br)) & @ (bl, ~br,@ (bl,br, @ (br,'[]'( ~bl)))) ;empty) ) ,
@@ -64,8 +64,8 @@
 )). % :-fail.  % too big to verify (sigh...)
 %
 ex0(21,(more,
-	share(ar,bl),share(br,c),share(cr,dl),
-	share(dr,el),share(er,a),
+	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) ) ,
@@ -73,7 +73,7 @@
         *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) ,
 true)).  % :-fail.  % too big to verify (sigh...)
 
-ex(22,(more,
+ex0(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) ) ,
@@ -158,8 +158,8 @@
 
 
 % demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL).
-%def("demo(X,Y)","ex(X,Y)").
-def("demo(X,Y)","true").
+def("demo(X,Y)","ex(X,Y)").
+% def("demo(X,Y)","true").
 % length 5 interval
 demo(1, length(5)).
 
@@ -240,7 +240,7 @@
 
 % model restriction by share predicate ( a little smaller.... :-)
 demo(16, (
-	share(ac,bc,cc,dc),
+	share([ac,bc,cc,dc]),
 	((proj(true,(length(4),'[]'(dc))),length(15) )&true),
 	proj((length(3),@ '<>'(ac)),true),
 	proj((length(5),@ '<>'(bc)),true),
--- a/src/lite/ITLNodeParser.java	Mon Jan 14 03:01:42 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Mon Jan 14 03:01:45 2008 +0900
@@ -72,8 +72,8 @@
 // def(P<=Q,Q=>P)");
 // loop stuff and quantifiers
 			define("*(A) ","proj(A,true),fin(A)");  // weak closure
-			define("+(A) ","A& *(empty;A)");   // strong closure
-			//define("+(A) ","A & proj(A,true)");   // strong closure
+			// define("+(A) ","A& *(empty;A)");   // strong closure (difficult one)
+			define("+(A) ","A & proj(A,true)");   // strong closure
 			define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
 			define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
 			define("all(P,Q)","not(exists(P,not(Q)))");
@@ -102,6 +102,10 @@
 					Node allFalse = (Node)SBDDFactory.trueSolver;
 					value= (Node)SBDDFactory.falseSolver;
 					LinkedList<ITLSolver> list = args.get(0).arguments();
+					if (list==null) {
+						error("sahre: missing [] argument");
+						return value;
+					}
 					if (list.isEmpty()) return value;
 					for(ITLSolver n:  list) {
 						Node n1 = (Node)n;
--- a/src/sbdd/SBDDFactory.java	Mon Jan 14 03:01:42 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Mon Jan 14 03:01:45 2008 +0900
@@ -49,6 +49,10 @@
 	}
 
 	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2) {
+		BDDSolver former = solver.toSBDD(this);
+		BDDSolver later = solver2.toSBDD(this);
+		if (former==emptySolver) return hash.put(later); 
+		if (later==emptySolver) return hash.put(former); 
 		ITLSolver v =  itlf.chopNode(solver.toSBDD(this),solver2.toSBDD(this));
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Chop);
 		return hash.put(b);
--- a/src/sbdd/SBDDTest.java	Mon Jan 14 03:01:42 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Mon Jan 14 03:01:45 2008 +0900
@@ -72,24 +72,23 @@
 		sat.showVerify("~(true& ~q)");
 		// sat.showVerify("@(@(@(empty)))");
 		sat.showVerify("fin(p)=([](<>(p)))");
-		sat.showVerify("fin(p)");
-		sat.showVerify("all(x,@y)");
-		sat.showVerify("exists(x,@@x = ~x)");
-		sat.showVerify("all(x,@@x)");
-		sat.showVerify("even(p)");
-		sat.showVerify("Q, keep( @Q = ~Q)");
+		//sat.showVerify("fin(p)");
+		//sat.showVerify("all(x,@y)");
+		//sat.showVerify("exists(x,@@x = ~x)");
+		//sat.showVerify("all(x,@@x)");
+		//sat.showVerify("even(p)");
+		//sat.showVerify("Q, keep( @Q = ~Q)");
+		sat.showVerify("even(p)=evenp(p)");
 		}
 		//sat.showVerify("share([a,b,c])");
 		//sat.showVerify("less(3)");
 		//sat.showVerify("*(a)");
 
 		//sat.showVerify("a?(x;(b?x:c)):false");
-		sat.showVerify("+(a & b)");
+		// sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
-		sat.showVerify("ex(10,p)");
-		sat.p.parseCommand.sat.verbose=false;
 		sat.p.parse("include('data/example').");
-		// System.out.println(p.parseCommand.sat.state);
+		System.out.println(p.parseCommand.sat.state);
 	}