# HG changeset patch
# User kono
# Date 1200378306 -32400
# Node ID 01356168f25f8423604eccc3ad1937b171524bb7
# Parent  416e4d272e7932621801ed1895a1ab7384220709
*** empty log message ***

diff -r 416e4d272e79 -r 01356168f25f src/data/example
--- a/src/data/example	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/data/example	Tue Jan 15 15:25:06 2008 +0900
@@ -109,7 +109,7 @@
 ex(203,(^r,length(4))).		% distinguish different state?
 ex(204,('[a]'(^r))).		% non-deterministic?
 ex(205,('[a]'(^r = length(2)))). 		% imitate length?
-ex(206,('[a]'(^r = length(4)),(^r& ^r))).
+ex(206,('[a]'(^(r) = length(4)),(^(r)& ^(r)))).
 ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
 ex(208,('[]'(^r = (
          a,@ ^r;
diff -r 416e4d272e79 -r 01356168f25f src/lite/ITLCommander.java
--- a/src/lite/ITLCommander.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/lite/ITLCommander.java	Tue Jan 15 15:25:06 2008 +0900
@@ -71,6 +71,7 @@
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
 		} else if (name == "verbose") {
+			// verbose(true) / verbose(off)
 			Node n= null;
 			checkSat();
 			try {
diff -r 416e4d272e79 -r 01356168f25f src/lite/ITLNodeParser.java
--- a/src/lite/ITLNodeParser.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Tue Jan 15 15:25:06 2008 +0900
@@ -86,7 +86,7 @@
 
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("do(N)","true",50,parseCommand);
-			define("def(Head,Body,Order)","true",50,parseCommand);
+			define("def(Head,Body)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
 			
 			define("ex0(N,Exp)","skipped");
@@ -158,6 +158,10 @@
 
 	@Override
 	public Node expr3() {
+		if (nextToken.type == TokenID.Next) {
+			nextToken();
+			return logicNodeFactory.nextNode(expr3());
+		}
 		Node n = super.expr3();
 		while(nextToken.type==TokenID.Question) {
 			nextToken();
@@ -176,14 +180,6 @@
 		return n;
 	}
 
-	@Override
-	public Node expr4() {
-		if (nextToken.type == TokenID.Next) {
-			nextToken();
-			return logicNodeFactory.nextNode(expr4());
-		}
-		return super.expr4();
-	}
 	
 	@Override
 	public Node term() {
@@ -224,30 +220,7 @@
 		}
 		return arg;
 	}
-	/*
-	@Override
-	protected Node term() {
-		Node n;
-		switch (nextToken.type) {
-		case Next:
-		case Empty:
-		case Chop:
-		case Length:
-		case Less:
-		case Exec:
-		case Define:
-		case Include:
-		case Closure:
-		case Projection:
-			n = makeVariable(nextToken);
-			break;
-		default:
-			return super.term();
-		}
-		nextToken();
-		return n;
-	}
-     */
+	
 	public ITLSolver emptyNode() {
 		return emptyNode;
 	}
diff -r 416e4d272e79 -r 01356168f25f src/sbdd/BDDSatisfier.java
--- a/src/sbdd/BDDSatisfier.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Tue Jan 15 15:25:06 2008 +0900
@@ -147,7 +147,7 @@
 			develop(e.key, allNext);
 			if (!verbose) System.out.println();
 		}
-		if (!verbose) {
+		if (verbose) {
 			if (!falsfiable) {
 				System.out.println("valid");
 			}