--- a/Changes	Sat Jan 19 10:45:09 2008 +0900
+++ b/Changes	Sat Jan 19 12:32:43 2008 +0900
@@ -1,3 +1,30 @@
+Sat Jan 19 12:18:24 JST 2008
+
+　　　　public interface ITLNodeFactoryInterface<T> 
+
+　　　　public class ITLNodeParser<Node extends ITLSolver>　　{
+　　　　　　　　public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) ;
+　　　　}
+　　　　public class ITLNodeFactory implements ITLNodeFactoryInterface<ITLSolver > ;
+
+で、
+
+　　　　p = new ITLNodeParser<ITLSolver>(new ITLNodeFactory());
+
+だと、Eclipse で生成すると動く。実行時エラーはでない。でも、ant でbuildすると、
+実行時に、
+
+　　　　 [java] Exception in thread "main" java.lang.VerifyError: (class: lite/ITLNodeParser, method: <init> signature: (Llite/ITLNodeFactoryInterface;)
+V) Bad type in putfield/putstatic
+
+うーん、これは何故だ。 動くわけなの
+で、一応、Generic は合ってはいるんだよな。
+
+　　　　public interface ITLNodeFactoryInterface<T extends ITLSolver> 
+
+とすると動くので、一種の型推論不足らしい。
+
+
 Fri Jan 18 22:44:54 JST 2008
 
 jar を作るようにCVSを直したが、危うくparser を消すところだった...

--- a/README	Sat Jan 19 10:45:09 2008 +0900
+++ b/README	Sat Jan 19 12:32:43 2008 +0900
@@ -23,17 +23,16 @@
 
 0.1 How to run
 
-    Try preload examples.
+    First, try preload examples.
 
-  ex(2).
+  do(2).
 
     It generates state machine. It also accepts an ITL formula.
 
-  ex( [](p) -> <> p ).
+  do( [](p) -> <> p ).
 
-    Please be careful about funny Prolog operator grammar.
-    Someday I will make a parser for Ben's notation. But not now...
-    After the state machine expansion, there are two diagnosis predicates.
+  ls.
+    Show all preload examples.
 
   diag.
 
@@ -42,7 +41,7 @@
 
   exe.
 
-    This shows an execution of ITL formula, if it is possible. It is
+    This shows an execution of ITL formula, if it is satisfiable. It is
     a counter example of negation of the original formula.   diag(N) or 
       exe(N) shows at least N length examples.  
    	1: +p-q   means "at clock 1, p is true and q is false". 
@@ -61,6 +60,24 @@
      .   transition to a registerd state
   verbose(on).
 
+  include('file name').
+     read from file.
+
+  ex(100,<> p).
+     define numbered example.
+
+  help.
+
+  show. 
+     show number of states.
+
+  clear.
+     Clear bdd database. Otherwise it remains for incremental
+     verification.
+
+  states.
+     show all subterm BDD, don't use it for large states.
+
 
 1. Syntax of ITL Formula
 
@@ -70,6 +87,9 @@
 To use existential quantifier, a form exists(R,f(R)) is used,
 here R have to be Prolog variable.
 
+   a,b         a and b
+   a;b         a or b
+
 Other definitions are found in chop.pl. If you want to see the expanding
 results ( chop normal form, cannot be readable...) use   expand(X,Y).
 

--- a/src/parser/LogicNodeParserTest.java	Sat Jan 19 10:45:09 2008 +0900
+++ b/src/parser/LogicNodeParserTest.java	Sat Jan 19 12:32:43 2008 +0900
@@ -21,7 +21,7 @@
 		n = p.parse();
 		if (n!=null) System.out.print(n); System.out.println(".");
 		
-		parser = new MacroNodeParser<ITLSolver>("exists(x,(a,x))",lf);
+		parser = (MacroNodeParser<ITLSolver>) p;
 		n = parser.parse();
 		if (n!=null) System.out.print(n); System.out.println(".");