--- a/Changes	Fri Nov 07 20:36:28 2008 +0000
+++ b/Changes	Tue Dec 15 01:07:22 2009 +0900
@@ -1,3 +1,42 @@
+Wed May 21 18:39:24 JST 2008
+
+LTTL だと、eventuality を考慮する必要がある。eventuality が対称ではない
+のが少し変だが...
+
+      <>p ->  〇 <> p  [p,[]]
+      []p ->  p /\ 〇 [] p  [[],p] 
+
+という感じなわけだが... 否定をどうするかという問題があるのか。
+
+      ¬ <>p ->  〇 ¬ <> p  [p]
+
+negative と positive があるのかな?
+
+      loop が在ったときに、loop 内の状態の
+           すべてで、negative eventuality は成立していない
+           どこかで、positive eventuality が成立している
+
+かな? eventuality は状態に付く。
+
+      <>p ->   p /\ 〇 <> p  
+              ¬p /\ 〇 <> p  [p]  => <>p [p] のループは false
+
+そもそも、Deterministic Buchi Automaton 自体が普通のBuchi automaton
+と違うんじゃない? 昔から進歩がないね〜
+
+ω Automaton と考えるのが良くなくて、反例生成器と考えるのが良いんじゃないか?
+ってことは、2nd order automaton と見るわけか? ある automaton x に対して、
+      p(x)  = t/f
+
+まぁ、同じものなんだろうけど。
+
+生成するのはRegular expression または finite automaton。
+
+[]<>(p) と、その否定、¬ [] <> (p) = <>[](¬ p) の例題を考えれば
+良いんでしょ?
+
+
+
 Sun Jan 20 10:44:41 JST 2008
 
 うーん、たぶん、class Continuation を取り除くことは可能なんだろうな。

--- a/build.xml	Fri Nov 07 20:36:28 2008 +0000
+++ b/build.xml	Tue Dec 15 01:07:22 2009 +0900
@@ -38,6 +38,7 @@
 
     <target name="jar" depends="build" >
     <mkdir dir="build/data"/> 
+    <mkdir dir="jar"/> 
     <copy todir="build/data" file="src/data/README" />
     <copy todir="build/data" file="src/data/example" />
     <jar jarfile="jar/Lite.jar" basedir="build" manifest="src/Lite.mf"/> 

--- a/src/parser/LogicNodeScanner.java	Fri Nov 07 20:36:28 2008 +0000
+++ b/src/parser/LogicNodeScanner.java	Tue Dec 15 01:07:22 2009 +0900
@@ -134,7 +134,9 @@
 				// no extension.
 			}
 			if (match) {
-				s = scan.group(1);
+				// This won't work in Java 6
+				// s = scan.group(1);
+				s = cb.toString().substring(scan.start(1),scan.end(1));
 				// fix position in CharBuffer
 				// scan.end() is relative position
 				cb.position(cb.position()+scan.end());