--- 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;