changeset 22:29cf617f49db default tip

newer CVS version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 22 Apr 2016 16:47:13 +0900
parents 8fb7b6f55b7e
children
files bddcomp.pl bdditl.pl bdtstd.pl chop.pl diag.pl display.pl dvcomp.pl ex.pl exdev.pl infinite.pl itlstd.pl kiss.pl ndcomp.pl problems rstd.pl verilog.pl
diffstat 16 files changed, 887 insertions(+), 821 deletions(-) [+]
line wrap: on
line diff
--- a/bddcomp.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/bddcomp.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: bddcomp.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
 */
 
 % itl decomposition for DST
--- a/bdditl.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/bdditl.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -8,7 +8,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: bdditl.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
 */
 % ITL subterm standarization with BDT
 %
--- a/bdtstd.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/bdtstd.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -8,7 +8,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: bdtstd.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
 */
 % ITL subterm standarization with BDT
 %
--- a/chop.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/chop.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Header$
+ $Header: /Users/kono/src/CVS/Lite/chop.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
 */
 :-dynamic define/2.
 % ITL chop standard form
--- a/diag.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/diag.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: diag.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
 */
 
 % develop Local ITL formula into state diagram
--- a/display.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/display.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
 % use this wording to make the terms for other programs.
 %
 % Please, send your comments to kono@csl.sony.co.jp
-% $Id$
+% $Id: display.pl,v 1.1 2007/08/30 03:44:35 kono Exp $
 %
 % Display Interface for ITL Verifier
 %    Using SICStus Prolog's Graphic Manager ( InterViews Package)
--- a/dvcomp.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/dvcomp.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: dvcomp.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
 */
 
 % itl decomposition for DST
--- a/ex.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/ex.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: ex.pl,v 1.5 2007/08/30 03:44:35 kono Exp $
 
  Examples
 */
@@ -28,7 +28,12 @@
 % quantifier
 ex(12,exists(R,(R,keep(@R = ~R),'[]'((R->p))))).
 % temporal assignment
-ex(13,exists(R,(R = p,keep(@R = R),fin(R = p)))).
+ex(13,exists(R,(R = p,keep(@R = R),fin(R = q)))).
+
+ex(133,
+    (exists(R,(q = R,stable(R),fin(p = R))))
+   =
+    (q & (empty,p); ~q & (empty, ~p))).
 %
 ex(14,
 	exists(Q,(Q, 
--- a/exdev.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/exdev.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: exdev.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
 */
 
 % develop Local ITL formula into state diagram
--- a/infinite.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/infinite.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -6,7 +6,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@ie.u-ryukyu.ac.jp
- $Header$
+ $Header: /Users/kono/src/CVS/Lite/infinite.pl,v 1.11 2007/08/30 03:44:35 kono Exp $
 
  Infinite satisfiability/validity checker
 
--- a/itlstd.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/itlstd.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Header$
+ $Header: /Users/kono/src/CVS/Lite/itlstd.pl,v 1.3 2007/08/30 05:16:36 kono Exp $
 */
 
 % ITL standarization
--- a/kiss.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/kiss.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: kiss.pl,v 1.3 2007/08/30 05:16:36 kono Exp $
 */
 
 % :- dynamic st_variables/2.
--- a/ndcomp.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/ndcomp.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: ndcomp.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
 */
 
 :-dynamic verbose/0,state/2,links/2.
--- a/problems	Fri Nov 07 20:36:40 2008 +0000
+++ b/problems	Fri Apr 22 16:47:13 2016 +0900
@@ -1,20 +1,81 @@
+Sat Jan 12 21:45:34 JST 2008
+
+なんか、share は間違っているっぽいけど。
+
+Sat Dec  1 11:08:27 JST 2007
+
+finite interval だけど...
+    infinite =def (true & false )
+
+finite をatomとして導入する。で、modelにfinite/infinite を入れる。
+    finite |- finite
+    finite |- ~infinite
+    infinite |- ~finite
+    |-/- infinite/\finite
+    |- infinite\/finite
+    finite \/ infinite |- p
+    finite /\ infinite |-\- p
+
+    finite |- @finite
+    finite |-/- @infinite
+model のfinite/infiniteは、排他。
+
+infinite がpositive occurence に一つあれば、式全体はinfinite。
+finite がpositive occurence のみにあれば、式全体はinfinite。
+正確ではないが、そんな感じ。
+
+    finite   |-/- true & false
+    infinite |- true & false
+
+である必要がある。(ふーん)
+    infinite |-/- finite & false
+    infinite |- infinite & false
+    finite |- finite & false
+    finite |-/- infinite & false
+
+でも、これだと、[]<>(p) みたいなのは?
+
+うーん、finite/infinite ではなくて、compact/open 見たいな感じだな。
+まぁ、実際、そうだしね。
+    infinite |- fin(false)
+だし。
+    infinite |- fin(p)から infinite |- []<>(p)
+
+   <finite>p = finite & p (on any finite, infinite)
+   [finite]p = ~(~finite & ~p)
+   []<finite>p = [](finite & p) = ~(true & ~(finite &p))
+
+   <infinite>p = infinite & p = true (on infintie)
+   [infinite]p = ~(~infinite & ~p) 
+
+<finite>p が、LTTLの<>pに相当するはず。いや、infinite /\ <finite>p
+かな。
+
+        infinite |- [](finite & p)
+
+自体が「pが無限回起きる」ってことを意味しているのでいいのかな。
+
+これで出来るのかな? なんか、pathlogic な感じだが、こういう構文的な
+もので finite/inifinite を区別できるものなの?
+
+
 Sun Feb 10 21:30:04 JST 2002
 
-衣empty ϡɤ? kiss λϡ̵뤷...
-
-⤽⡢2nd order 줿ǡʣˤʤꤹ
-
-⤦ simple version ٤͡
-
-ѤǤǡ
-
-о     general abstraction
+あ、そうだよ。empty は、どうすんだ? kiss の時は、無視したんだが...
+
+そもそも、2nd order を入れたおかげで、複雑になりすぎ。
+
+もう一度 simple なversion を作るべきだよね。
+
+状態生成を再利用できる形で。
+
+対称性     general abstraction
 
 Thu Feb  7 12:12:21 JST 2002
 
 Verlog output for Prof. Fujita
 
-switch Ǥ⤤ɡäȵˤʤʤ?
+switch でもいいんだけど、ちょっと巨大にならない?
 
 module check001(clk,inputs..,outputs...)
 input clk;
@@ -34,19 +95,19 @@
     end
 endmodule
 
-äƤʴ?
-
-äѤꡢ֤cubeΤ褦ʷΤϡɤʤ͡
+ってな感じ?
+
+やっぱり、状態をcubeのような形で生成するのは、良くないよね。
     ?(a,@a,@b)
-ߤʷǡ䤹ޡϡJava Version

-
-ɤ? BDD üƾ֤ˤ褦ˤ롣
-ϡޤɤʤ...
+みたいな形で、生成した方が扱いやすい。ま、それは、Java Version
+で。
+
+特性方程式を生成する方が良い? BDD の末端が各状態にいくようにする。
+それは、あんまり良くないか...
 
 Sun Jan 21 00:42:39 JST 2001
 
-? äѤꡢʤѤʡ
+あれ? やっぱり、なんか変だな。
     | ?- ex(finite & empty).
 
     state(1 , not(true&false)&empty)
@@ -65,51 +126,51 @@
     satisfiable in infinite interval:
     *
     0:      1
-Ǥϡޤˡ
+では、困ります。それに、
     <>(p) = finite & p
-˽񤭴ʤȤʤߤ͡
-
-äƤȤϡϤꡢ
-    ξ֤顢ͣ졢more ˤȴ
-ʤΤʡ
+に書き換えないといけないみたいね。
+
+ってことは、やはり、
+    その状態から、唯一、more にだけ抜ける状態
+なのかな。
 
 Sat Jan 20 20:50:17 JST 2001
 
-true loopȤߤʤƤʤΤǡex(true) ǡinfinite 
- satisfiable ˤʤʤ
-
-infinite ǡloop  * 褦ˤ
+true をloopとみなしてないので、ex(true) で、infinite 
+が satisfiable にならない。
+
+infinite で、loop を * で明示するようにした。
 
 Sat Jan 20 18:16:33 JST 2001
 
-Ȥꤢmore_only ϡmore ˤΤеȸȤ

+とりあえず、more_only は、more にいくものが何かあれば許すと言うことに
+しました。
 
 Sat Jan 20 03:38:14 JST 2001
 
-demo(15)  infinite ߤޤʤloop detection η׻̤
-¿褦Ǥ͡
-
-ԤΤФƤƤȤȤȡrepeat fail loop
-Dz󤹤櫓ˤϤޤ͡
+demo(15) の infinite が止まらない。loop detection の計算量が
+多すぎるようですね。
+
+失敗したのを覚えておいてということだと、repeat fail loop
+で回すわけにはいきませんね。
 
 Sat Jan 20 02:33:17 JST 2001
 
-ˡmore_only(S) ȽǤƤޤäɤΤ?
-
-inifinite-> ⤢뤷...
-
-inifinite state sequence ǡITL satisfiy 
-Ȥ -interval satisfiability äƸ󤸤ʤ?
-
-Ȥȡ
-    ξ֤顢ͣ졢more ˤȴ
-ǤɤΤ? Ǥ⡢more/empty ǤʤʬषƤޤäƤΤǡ
-ϡۤɴñȽǤǤʤʡITLϤ顢
-more դäŸɤΤ...
-
-non-determistic  empty ʪϡ~(<>empty) ˤʤʤΤ

+本当に、more_only(S) で判断してしまって良いのか?
+
+inifinite-> の問題もあるし...
+
+ある特定のinifinite state sequence で、ITL式が satisfiy される
+ことを ω-interval satisfiability って言うんじゃないの?
+
+だとすると、
+    その状態から、唯一、more にだけ抜ける状態
+であれば良いのか? でも、more/empty でいきなり分類してしまっているので、
+それは、それほど簡単に判断できないかな。ITL式はあるんだから、
+more を付け加えて展開すれば良いのだけど...
+
+non-determistic に empty に落ちる物は、~(<>empty) になり得ないので
+まずい。
 
 13:+ac-bc-cc-dc 183
 14:-ac-bc-cc+dc 185
@@ -130,7 +191,7 @@
 29:-ac+bc-cc-dc 226
 30:-ac-bc+cc-dc 186
 
-!
+おぉ!
 
 Fri Jan 19 20:59:46 JST 2001
 
@@ -151,433 +212,433 @@
     | ?- infinite.
     unsatisfiable in infinite interval.
 
-... ɤȤʤǤ礦? inifite ϴŪ
-false 顢inifite-> פΤΤϡ٤ơinfinite unsatisfiable

+これは... どういうことなんでしょうね? inifite は基本的に
+false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable
+だね。
 
 Fri Jan 19 20:40:37 JST 2001
 
-ȴñʥ르ꥺǡsatisfiabilityϡå
-Ǥޤ줬ɤ Moszkowski ˤ뤱...
+割りと簡単なアルゴリズムで、satisfiabilityは、チェック
+できました。これが、正しいかどうかは Moszkowski によるけど...
    inifnite
    *skip
    *((skip&skip))
-ʤɤ˴ؤƤϡޤư褦Ǥ͡
-
-vailidity checker ߤ... ɤΤvalidʤΤϡ
-ɤ狼ʤ꤬ unsatisfiable ʤСvalid ʤ
-
-
-Ǥ⡢ˡȡ
-    satisfiable in -interval implies
+などに関しては、うまく動くようですね。
+
+vailidity checker が欲しい所だけど... どういうものがvalidなのかは、
+良くわからない。もちろん、否定が unsatisfiable ならば、valid なの
+だが。
+
+でも、この方法だと、
+    satisfiable in ω-interval implies
       falsifiable in finite interval
-äƤȤˤʤ餷
+ってことになるらしい。
 
 Fri Jan 19 07:48:59 JST 2001
 
-Streett     _i []<>L_i  <>[]U _i
-Rabin     ~(_i []<>L_i  <>[]U _i)
-
-Ȥ¤äƤ롣ϡ
-    ̵²󷫤֤ L ϡĤä U ̤褦ˤʤ
-ΤȡȤ¤ˤʤäƤ롣
-    labeled tree Ρ꤫ϡäȡ֤ޡĤƤץ롼

-
-ǡΥ르ꥺ...
-
-depth first ˡֽи̵Ρɡפõޡ롣顢
-ΡɤФʤ顢и̵Ρɤ귫롣롼פФ褿鸡
-λǸޤǤä顢ޡꡢνи̵Ρɤõ
-depth first search ޤǷ֤äơ׻̤ϡ
-ΡɿN  Фơǰ N^2/2 ( N+(N-1)+(N-2)...1 ) Ǥ롣ۤ

+Streett     ∩_i []<>L_i ⊃ <>[]U _i
+Rabin     ~(∩_i []<>L_i ⊃ <>[]U _i)
+
+という構造を持っている。これは、
+    ある無限回繰り返す所 L から先は、いつか、ずーっと U を通るようになる
+のと、その否定という構造になっている。これを、
+    labeled tree の、ある所から先は、ずーっと「あるマークがついている」ループ
+で表す。
+
+で、そのアルゴリズムだけど...
+
+depth first に「出口の無いノード」を探す。そこをマークする。そこから、
+ノードを覚えながら、出口の無いノードを手繰る。ループが出て来たら検出
+完了。最後までいったら、マークに戻り、次の出口の無いノードを探す。
+これをdepth first search が終るまで繰り返す。したがって、計算量は、
+ノード数N  に対して、最悪 N^2/2 ( N+(N-1)+(N-2)...1 ) である。それほど
+悪くは無いか。
 
 Fri Jan 19 04:27:42 JST 2001
 
-ȡLICS paper ϡ䤿ʣפϡ-automaton
-͡顢false loop detection ȡ
-ITL ˰פƤ뤳Ȥɤ
-
-finite interval Ǥϡ˰פƤ櫓顢(true  & false )
-satisfiability̵ưפɬפ̵פʤС
-ۤʤaxiomatiazation 򸫤ĤȤˤʤ롣顢false loop 
-detection  negetation consistent ʤС֤󡢰פ
-
-ɤϡRabin automatonacceptabilityå뤳Ȥˤʤ
-äƤȤϡnon deterministic buchi automaton 򰷤äƤȤ
+えーと、LICS のpaper は、やたら複雑だが、要は、ω-automatonの
+否定の問題だよね。だから、false loop detection が、ちゃんと、
+ITL の否定の定義に一致していることさえ見れば良い。
+
+finite interval では、既に一致しているわけだから、(true  & false )
+のsatisfiabilityの定義を無理して一致させる必要は無い。一致しなければ、
+異なるaxiomatiazation を見つけたことになる。だから、false loop 
+detection が negetation consistent ならば、たぶん、一致するんだろう。
+
+結局は、Rabin automatonのacceptabilityをチェックすることになるんだろう。
+ってことは、non deterministic buchi automaton を扱うってことか。
 
    Rabin <-> Streett  complimentary
 
-(true & false)˴ؤƤϡ<>[](not_empty) ʡ
+(true & false)に関しては、<>[](not_empty) だよな。
    infinite  -> <>[](more)
 
-äƤȤ... äѤꡢfalse_loop detection Ǥ󤸤ʤʤ
-

-	٤Ƥterminating loop ǡempty->true ʤ => infinite
-顢ض֤ǽ­äƤΤϡ
-	terminating loop  empty->trueʤΤ
-顢ض֤ǹäƤΤϡ
-	terminating loop  empty->trueʤ
-
-Ȥʤ롣ȡtrue/false ž롣(Τ?)
-
-terminating loop ǤʤƤ⡢ض֤¸뤳ȤϤǤ롣
+ってことは... やっぱり、false_loop detection でいいんじゃないかなぁ。
+
+えーと、
+	すべてのterminating loop で、empty->true がない => infinite
+だから、ω区間で充足ってのは、
+	terminating loop に empty->trueがないものがある
+だから、ω区間で恒真ってのは、
+	terminating loop に empty->trueがない
+
+となる。その否定を取ると、true/false が逆転する。(のか?)
+
+しかし、terminating loop でなくても、ω区間を実現することはできる。
 	infinite & P -> infinite
-顣ξ⽼­äƤʡξϡɤ P
-ϡtableau ̵뤵Τ̵
-
-äơȤϡterminating loop 򸫤Ф
-
-execution example ϡ
+だから。この場合も充足っていうんだろうな。この場合は、どうせ P
+は、tableau で無視されるので問題無い。
+
+って、ことは、terminating loop だけを見ればよろしい。
+
+execution example は、
     s s s s s s (s s s s s s)*
-Ȥ롣ʤΤǡɬǾǥġ
-ºݤˤϡ* ϡŪɤ
+という形を取る。なので、必ず最小モデルの性質を持つ。
+実際には、* の中は、非決定的で良い。
 
 
 Fri Jan 19 02:18:39 JST 2001
 
-<>empty  infinite = (true & false ) ϡξΩʤ
+<>empty と infinite = (true & false ) は、両立しない。
 <>empty = finite & empty = ~(true & false) & empty
 
-~(true & false ) Ϥʤˤ򼨤Ƥ뤫ȸ...
-ĤǤֽפȤȡinfinite ϡֽʤ
-
-ض֤ˤϡempty exit ¸ߤǤʤΤˤϡ
+~(true & false ) はなにを示しているかと言うと...
+いつでも「終れる」ということ。infinite は、「終れない」
+
+ω区間には、empty exit は存在できない。正確には、
     ... [ no-empty loop ] ....
-Ȥȡsub ֤ɤ
-
-[](more) ? 󡢤ϡLite Ǥϡfalse.
+ということ。そういうsub 区間があれば良い。
+
+[](more) は? もちろん、これは、Lite では、false.
      ~(finite & ~more)
      ~(~(true & false) & ~more))
      ~(~(true & false) & empty))
-줬 ض֤ true ˤʤ뤿ˤ...
-
-[]inifinite version?
+これが ω区間で true になるためには...
+
+[]のinifinite versionは?
 
 http://research.commpaq.com/SRC/esc/
 
 Fri Jan 19 01:20:54 JST 2001
 
-ض֤ϡɬ(s_n...s_m)* ޤࡣdecidableʤС
-ϡɬפɡ
-
-դˡ(s_n...s_m)* ޤС򤺡äȷ֤Ȥˤꡢ
-ض֤Ǥ롣顢롼פ򸫤ĤС
-ض־ satisfiable ȤȤǤ롣
-
-ζ־ǡempty Τ褦exitΤ? ֤
-ʤȤȤϡϤꡢfalse loop 򸫤Ĥ
-ɤȸȤ
-
-Υ르ꥺ?
-
-ض֤Ǥϡempty ȴФ뤳ȤǤʤ->
-   <>empty false
-ɤʡ
-
-ȡʥ르ꥺबꤽ...
-ñʤΤϡ٤ƤΥ롼פdepth first õȤʡ
-
-Ȥȡfinitarity åΤϷ빽ݤˤʤ롣
-
-finitarity ȤϤʤ?
-    롼פˤɬtrue exit
-infiniteness Ȥϡ
-    exit Τʤ롼פ
-
-[]<>(p) = <>[](p) ϡɤʤ?
+ω区間は、必ず、(s_n...s_m)* を含む。decidableならば、そうだ。
+が、それは、証明が必要がだけど。
+
+逆に、(s_n...s_m)* を含めば、そこをずーっと繰り返すことにより、
+ω区間を実装できる。だから、そういうループを見つければ、
+ω区間上で satisfiable だということができる。
+
+その区間上で、∨empty のようなexitが許されるのか? たぶん、
+許されない。ということは、やはり、false loop を見つければ
+良いと言うことか。
+
+そのアルゴリズムは?
+
+ω区間では、empty で抜け出ることができない。->
+   <>empty がfalse
+どうも正しそうだな。
+
+えーと、何か、安全なアルゴリズムがありそうだけど...
+簡単なのは、すべてのループをdepth first で探すことだな。
+
+とすると、finitarity をチェックするのは結構面倒になる。
+
+finitarity とはなに?
+    ループには必ずtrue exitがある
+infiniteness とは、
+    exit のないループがある
+
+[]<>(p) = <>[](p) は、どうなるんだろう?
    <>(p) = finite & p
    ~(finite & ~(finite  & p)) = finite & ~(finite & ~p)

+ですか。
 
 
 Fri Jan 19 00:33:43 JST 2001
 

+えーと、
 	[](false)
-satisfiableˤʤ뤳ȤϤʤ
+がsatisfiableになることはない。
 	~(true & ~ false)
 	~(true & true)
-顣
+だから。
 	true & ~true
-ϡ롣
+は、許される。しかし、
 	~true & ~true
-ϵʤ켫Τϡverifier Ǥ⡢ʤ롣
-
-tableau expansion ΤƱȹͤɤΤ?
-ä˰ۤʤ inference rule 櫓ǤϤʤ餷
-
-ȤСɬפʥɤϡfalse loop detector ?
-exe/diag ˡinfinite_exe,infinite_diag Τ
-
-infinite_exe ϡ롼פɽʤФʤʤɬ
-Τ褦ʥ롼פ¸ߤΤ? Ȥȡinfinite
-interval ϡprefix Τ褦ʤΤˤʤ롣¤ϡprefix
-infinite interval Τ? prefix(finite,....)
-ߤʤΤ͡ϡɤäǸȤ...
+は許されない。これ自体は、今のverifier でも、そうなる。
+
+tableau expansion 自体は同じだと考えて良いのか?
+特に異なる inference rule があるわけではないらしい。
+
+だとすれば、必要なコードは、false loop detector だけか?
+exe/diag の代りに、infinite_exe,infinite_diag を作るのだろうか。
+
+infinite_exe は、ループを表示しなければならない。必ず、
+そのようなループが存在するのだろうか? とすると、infinite
+interval は、prefix のようなものになる。実は、prefix
+がinfinite interval そのもの? prefix(finite,....)
+みたいなものだね。これは、どっかで見たことが...
 
 
 Thu Jan 18 22:42:24 JST 2001
 
 | ?- ex(((true&false)->(<>(empty)))).
  
-ϡvalid ˤʤäƤޤºݤˤϡinfinite->not(<>(empty)).
+は、valid になってしまう。実際には、infinite->not(<>(empty)).
 
 Thu Jan 18 21:04:13 JST 2001
 
-ޤchop.pl ΡX & false falseѴƤΤ
-ȴɬפ롣
+まず、chop.pl の中の、X & false をfalseに変換しているのを
+抜く必要がある。
 
 Thu Jan 18 19:59:33 JST 2001
 
 in POPL01
 
-LICS00  infinite 褦 Lite ĥ뤳Ȥ
-ǤΤ?
-
-ñʳĥˤϤʤʤ
+LICS00 の infinite を入れるように Lite を拡張することが
+できるのか?
+
+単純な拡張にはならない。
     infinite =def (true & false )
-顣ϡμǤ unsatisfiable
-
-P&Q ǡQ ñfalseȤäơʤϡnode ϡ
+だから。これは、今の実装では unsatisfiable。
+
+P&Q で、Q が単純にfalseだからといって、諦められない。今は、node は、
 	empty,false
 	empty,true
 	more,false
 	more,some_other
-Ȥ褦ħդƤ롣­Τ?
-
-Eventurality check ɬ̵ɤɡ
-
-Rabin automaton äƤʤ? Buchi Ʊʤ󤸤ʤ?
-
-true & false ϡ
+というように特徴付けられている。これで足りるのか?
+
+Eventurality check が必要無いと良いんだけど。
+
+Rabin automaton ってなんだ? Buchi と同じなんじゃないの?
+
+true & false は、
 	empy -> false
 	more -> true & false
-Ÿ롣ϡempty 򸫤ơvalidity/satisfiability 
-Ĵ٤Ƥ롣
-    ֤false exit 롼פsatisfiableȤߤʤ
-Ȥˤꡢinfinite interval Ƴ뤳ȤǤ롣
-
-ϡɤΤ褦 false exit 롼פ satisfiable Ȥ
-? Ȥϡ unsatisfiable ˤʤ formulaä
-?
+に展開される。今は、empty だけを見て、validity/satisfiability を
+調べている。しかし、これを、
+    「ある特定のfalse exit ループをsatisfiableだとみなす」
+ことにより、infinite interval を導入することができる。
+
+問題は、どのような false exit ループが satisfiable だという
+こと? というよりは、これで unsatisfiable になる formulaって
+何?
 	more -> false
-Τ?
+のたぐいだけか?
     finite
 	empy -> true
 	more -> true & true
-ϡɤʤ?
+は、どうなる?
     ~infinite
 	empy -> true
 	more -> ~(true & false)
-Ȥʤ롣ʤΤǡ finite 
-
-infinite ϡfalse loop ɽƤȹͤ롣
-
-ƤμPfinite -> P ǡåСfinite LITL ˤʤ롣
-(ʤʤФʤ)
-
-äơȤϡfalse loop detectɤ? ϡ
-빽פ׻ŪˤϡäѤʡ
+となる。なので、これは finite に等しい。
+
+infinite は、false loop を表していると考える。
+
+全ての式Pを、finite -> P で、チェックすれば、finite LITL になる。
+(ならなければいけない)
+
+って、ことは、false loop をdetectすれば良いだけか? これは、
+結構易しいが、計算量的には、ちょっと大変かな。
     finitely
 	valid, satisfiable, unsatisfiable...
     inifinitly
 	valid, satisfiable...
-infinitely satisfiable Ȥϡ
-    flase loop ¸ߤ뤳
-valid ϡ
-    false loop ʳϡempty false Ǥ뤳(?)
-
-ȡȡinifinitly satisiable ʼϡfinitly unsatisfiable
-ɡǤ? Ȥȡvalid ʼϤʤʤäƤޤ͡
-
-ϡäȤ줷ʤǤȤȤϡ
-    infinitely valid ϡ
-    false loop ʳϡempty ture Ǥ뤳(?)
-ޤȹͤΤȤȡ
+infinitely satisfiable とは、
+    flase loop が存在すること
+valid は、
+    false loop 以外は、empty false であること(?)
+
+えーと、それだと、inifinitly satisiable な式は、finitly unsatisfiable
+だけど、それでいいの? だとすると、valid な式はなくなってしまうね。
+
+これは、ちょっとうれしくないであろう。ということは、
+    infinitely valid は、
+    false loop 以外は、empty ture であること(?)
+を含むと考えるのが正しい。だとすると、
     |= finitie /\ finite
-äƤȤˤʤ͡ϡäȤ줷ʤ
-
-ࡢMoszkowski ϡɤ򤷤?
+ってことになるね。それは、ちょっとうれしくないか。
+
+うーむ、Moszkowski は、どういう選択をしたんだろう?
 
 
 Wed Nov 22 16:27:45 JST 1995
 
-rstd ¦ limit 򰷤Ȥˤ롣
-rename_list limitꤹ뤳Ȥˤʤ롣singleton limit
-ϤʤȤʤover(r,N)ˤǤʤΤ
-äȾ­ʡ
-
-itlstd  idempotent ˤʤäƤʡ!!! 
-itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) Y=Y1ˤʤ
-ϤʤΤ...
-
-itlstd2 Ǥϡsingleton remove, renaming ϹԤʤʤǡlimit over
-갷ˤädetailed trace ǽȤʤ롣ˡ
-itlstd򤫤СȤϤɤ⼺ԤƤ
-餷
+rstd 側で limit を扱うことにする。
+rename_list でlimitを指定することになる。singleton のlimit
+をはずさないといけないだろう。over(r,N)が外にでないのが
+ちょっと情報不足だな。
+
+itlstd が idempotent になってなーい!!! しくしく。
+itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) でY=Y1になる
+はずなのだが...
+
+itlstd2 では、singleton remove, renaming は行なわないで、limit over
+だけを取り扱う。これによってdetailed trace が可能となる。これに、
+従来のitlstdをかければ、もとに戻るはずだ。が、どうも失敗している
+らしい。
 
 Tue Nov 21 18:33:19 JST 1995
 
-renaming  trace  original limit ǹԤʤ
-detailed trace  no limit ǹԤʤ
-itl/5 2ٸƤФ뤬ޤɤȤ뤫
-
-rstd ¦limit֤򤹤Ф֤ޤʤ...
-
-renmaing ǡover limit 갷Ū
+renaming の trace は original limit で行なう。
+detailed trace は no limit で行なう。
+itl/5 は2度呼ばれるが、まあ、良とするか。
+
+rstd 側でlimitの置き換えをすればだいぶましなんだが...
+
+renmaing で、over limit を取り扱う方が統一的か。
 
 Wed Nov 15 12:58:28 JST 1995
 
-over(r,N)  true/false ֤äƤơunify뤫? 
-
-ˤ衢äȵޤɤѿ֤뤫ϡ
-renaming  trace ʬ뤬...
-
-֤rstd¦ǹԤʤäơoriginal/restrictedξ
-ȤäƤơɤѿ֤äʬ褦ˤ롣
-(renaming informationƤ) Ǥ⡢ξɤ
-lazy? ʤѤ
-
-뤤ϡdetailed traceǤִʤ? true/false 
-֤ƤƱstateǼ¸ǤϤunify Ϥʤ

-
-ˤ衢lazy state generation Ǥϡ
+over(r,N) が true/false に置き換わっていて、unifyするか? 
+
+いずれにせよ、ちょっと気まずい。どの変数が置き換わるかは、
+renaming を trace すれば分かるが...
+
+この置き換えをrstd側で行なって、original/restrictedの両方を
+とっておく。そして、どの変数が置き換わったか分かるようにする。
+(renaming informationに入れておく) でも、この情報もどうせ
+lazyに生成するんだよね? なんか変だ。
+
+あるいは、detailed traceの方では置換えしない? true/false に
+置き換えても同じstateで実現できるはず。だが、unify はしないと
+いけない。
+
+いずれにせよ、lazy state generation では、
    full trace, restricted trace
-ξ򤪤ʤΤˤϡover ֤rstd ǹԤʤä

-
-ࡢǤ⡢ȡitlstd non-deterministic ˤʤä
-ޤϡޤ
+の両方をおこなう。このためには、over の置き換えをrstd で行なった
+方が良いだろう。
+
+うーむ、でも、そうすると、itlstd がnon-deterministic になって
+しまう。それは、いまいちだ。
 
 Tue Nov 14 19:56:26 JST 1995
 
-Detailed trace λ Fromula  state number ξ⤫ʤ
-
-
-ȤȤϡdiag routine ľʤȥᤫndcomp 
-뤫?
+Detailed trace の時は Fromula と state number と両方持ち歩かないと
+だめだ。
+
+ということは、diag routine を書き直さないとダメか。ndcomp は
+あきらめるか?
 
 Mon Nov 13 22:33:34 JST 1995
 
-trace Ȥrenaming ϡʤ󤸤ʤ?
-detailed traceɤȤȤ... С
-choice ͤʤƤɤ
+trace するときにrenaming は、いらないんじゃない?
+detailed traceをどうせ使うとすれば... そうすれば、
+choice も考えなくても良い。
 
 Sun Nov 12 23:37:36 JST 1995
 
-^r trace
-
-stateϷޤäƤ
-duplicated  rename inforamtion Ȥätrace Ǥ롣
-
-detailed expansion ơunify 롣Ūˤϡ
-BDDˤäʬ򤹤롣ˤäơtrue_false r^n
-treeŸϤʤС̤ΤΤõ
-
-true_falsechoiceˤäͤۤʤ櫓...?
-choice ϡĤBDD˴ؤưĤǤʤ(leafˤʤ
-) ȤȤϡʣchoice ϡ
-    ۤʤ &  empty
-Ǥʤʤ餫identityĤɡ
-ޡŪƱstateˤäơ٤Ƥξ郎Ԥʤ顢
-ʤdetailed expansion Ϥ٤ƤޤǤΤ顢
-ʤϤ
-
-ޤϡrenaming ΥĤ褦
-
-äŪ^rȥ졼ɤʤ? singleton ^r
-ʤ餫term˥ޥåפǤʤΤ?
+^r のtrace
+
+stateは決まっている
+duplicated は rename inforamtion を使ってtrace できる。
+
+detailed expansion して、unify する。具体的には、
+BDDにそって分解する。これによって、true_false がr^nの
+treeに展開されるはず。されなければ、別のものを探す。
+
+true_falseのchoiceによって値が異なるわけだけど...?
+choice は、一つのBDDに関して一つしかでない。(leafにしかない
+から) ということは、複数のchoice は、
+    異なる & の empty
+でしか起きない。なんらかのidentityを残した方がいいんだけど。
+ま、結果的に同じstateにいって、すべての条件が尽くされるなら、
+構わないか。detailed expansion はすべてを含んでいるのだから、
+構わないはず。
+
+まずは、renaming のカタをつけよう。
+
+もっと選択的に^rをトレースした方が良くない? singleton ^r
+をなんらかのtermにマップできなものか?
 
 Sat Nov 11 09:55:41 JST 1995
 
-2path singleton removal 褦äȤǤ
-ɤ⡢order sensitive ʤʡover @<,@>
-äƤǤȤǤʤ롣
-
-sbdt_split, sbdt_ife ˤäremoval/renameˤorderʤ
-Ȥʤä򤨤ʤȤ?
-
-singleton removal񤤤顢ȤɤʤäƤޤä
-ɤ⡢bdt routineˤ꤬äߤtrue & true 
-褦ˤΤȤפʤ.... sbdt_opt Τ?
-
-state numberǤʤʤbugľ
-
-Ȥϡtrace ʡr^nμ¹Ԥȥȥ졼Ǥ

+2path singleton removal がようやっとできた。
+ただし、どうも、order sensitive なんだよな。over が@<,@>に
+よってでる時とでない時がある。
+
+sbdt_split, sbdt_ife によってremoval/renameによるorderを修正しない
+といけなかった。やむをえないところか?
+
+しかしsingleton removalを書いたら、もとの方も良くなってしまった。
+どうも、bdt routineには問題があったみたい。true & true を除く
+ようにしたのが効いたとも思えないんだが.... sbdt_opt のせいか?
+
+state numberがでなくなるbugを直した
+
+あとは、trace の問題だな。r^nの実行がちゃんとトレースできると
+いいんだけど。
 
 Thu Nov  9 12:03:32 JST 1995
 
-P & Q sb(P_BDD & Q_BDD) ȤǻäƤ뤱..
+P & Q を、sb(P_BDD & Q_BDD) という形で持っているけど..
 sb(P_BDD,PN)
 sb(Q_BDD,QN)
-PN & QN Ȥɤʤ? ۤȤƱȤϻפ....
-?(PN & QN,true,false) ȤʤΤ.... 
-
-QŸޤʤ? ? ̤ŸΥޡ
-Ȥʤ?
+PN & QN という方が良くない? ほとんど同じだとは思うけど....
+?(PN & QN,true,false) となるのか.... うーん。
+
+Qの展開を一回に抑えられない? ? を未展開のマークに
+使えないか?
 
 Wed Nov  8 20:31:23 JST 1995
 
-ϤöBDD2pathǽ뤳ȤȤ롣
-
-first path:  singleton varble  detect
-  (regular variableʤϡΤޤstd_check
-   singleton removal Ǿä뤳ȤϤʤ)
-regular variable ̵Сǽλ
-rename list ׻
+はやり一旦BDDに落して2pathで処理することとする。
+
+first path:  singleton varble の detect
+  (regular variableがない場合は、そのままstd_check
+   singleton removal で消えることはない)
+regular variable が無ければ、これで終了
+rename list を計算
 second path path:  
-  singleton variable ä硢
-  t/ftree  parallel traverse
-  t/f ޤϡ[tf]/tf ȹ礻tf֤
-  ʣsingleton variableƱ˽ɤ
-
-regular variable 뤫ɤϡsingleton removval 
-̤˰¸Τǡ1path Ǹ̩˼ȤϤǤʤ
-2nd path Ǥϳμ¤˼Ȥ롣
-
-֤֡2nd path㤦!! sbdt ȶѤϤǤʤ
+  singleton variable があった場合、
+  t/fのtree を parallel traverse
+  t/f または、[tf]/tf の組合せをtfに置き換える
+  複数のsingleton variableを順不同に処理して良い
+
+regular variable があるかどうかは、singleton removval の
+結果に依存するので、1path で厳密に取り除くことはできない。
+が、2nd path では確実に取り除くことが出来る。
+
+ぶぶ、2nd pathは全然処理が違う!! sbdt と共用はできない
 
 Tue Nov  7 15:45:07 JST 1995
 
-chop Υ٥ʬСޤɤϡΤȡȡ
-ͤȡBDDѴ٥б˾ޤΤʤ
-󡢺ΤޤޤǤsafeʤɡƤΤ¿
-ϷŪ˾֤䤷Ƥ뤳Ȥˤʤ롣
-
-Ĥˡϡ
+chop のレベルで分ければ、まあ、良い。問題は、そのあと。と、
+考えると、BDDに変換するレベルで対応する方が望ましいかも知れない。
+もちろん、今のままでもsafeなんだけど、落ちているものが多い。
+それは結果的に状態を増やしていることになる。
+
+一つの方法は、
    p(^r)  =>   ?(^r,pt,pf)
-Ȥ롣
+とする。
    (pt,pf; tf), (pt;pf)
-ѷ롣ȡʶ硣ϽŤʤ
-
-(~ ^r), ^r ܥȥॢåפǤfˤʤʤޡȤʤʡ
+と変形する。と、こんな具合。これは重いなぁ。
+
+(~ ^r), ^r がボトムアップではfにならない。ま、そういうことなんだよな。
 
 Tue Nov  7 10:38:59 JST 1995
 
-ɤ⡢singleton removal ȡ[a](^r = length(2)), f(^r)
-Τ褦ʤΤϴ˥ȥ졼Ǥ餷
-[a](^r = length(2)), *(^r) Ok ä
-
-Ǥ⡢ʸˡҤȯ롣
-
-ɡɤ¤ʤΤʤ? diag ˡfull trace Ǥɤ
-å뤫...
-
-ɤ⡢󥰥ȥåŤʡäȡȥå
-ˤ?
+どうも、singleton removal だと、[a](^r = length(2)), f(^r)
+のようなものは完璧にトレースできるらしい。
+[a](^r = length(2)), *(^r) もOk だった。
+
+でも、さすがに文法記述は発散する。
+
+結局、どういう制限なのかなぁ? diag 時に、full trace できたかどうかを
+チェックするか...
+
+どうも、シングルトンチェックが甘いな。もっと、ちゃんとチェックする
+ためには?
 
 Mon Nov  6 15:57:46 JST 1995
 
-[p_0,p_1,...,p_n] ϡ
+[p_0,p_1,...,p_n] は、
 p_0,p_1,...,p_n        -> true
 ~ p_0,~ p_1,...,~ p_n  -> false
 else                   -> true_false
-ȤBDD(MTBDD)ˤʤ롣3
+という形でBDD(MTBDD)になる。3値論理
 
 ^r -> true_false
 
@@ -591,181 +652,181 @@
 f;tf  -> tf
 tt,tf -> tf
 
-(졢cross term?)
-ΤˤǤޤޤϤ* ^r ⴰ
-
-ϡ¹ԤtraceǤ뤫ɤʡ
+(あれ、cross termは?)
+確かにこれでうまくいきます。はい。* ^r も完璧。
+
+問題は、実行をtraceできるかどうかだな。
 
 Mon Nov  6 08:50:01 JST 1995
 
-singleton θ̤ͭ¤?
-
-BDDsingleton duplicate ȤȡϻߤޤΤ?
+singleton の効果は有限か?
+
+BDDの中でsingleton duplicate を許すとすると、これは止まるのか?
    selection(uniq set of subterm)
-ȤˤʤϤ顢ȤޤϤsubtermͭ¡singleton ˤϡ
-R̾ˤ̤ɬ̵
+という形になるはず。だから、とまるはず。subtermは有限。singleton には、
+R名による区別さえ必要無い。
    ^r -> ^([false,true])
    ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
-ȤŸˤʤ? sortɬס
-
-Ūˡ^(r,[p_0,p_1...p_n]) ȤǼ«ʤ? r Ĥä...
-ͥȤoutǤnestϤäƤ顣
-
-computationȥ졼ǤΤ? 䡢̤Ÿɬס
-
-ȡdeterminization ʤȤ͡(ɤä?)
+という展開になる? 再sortは必要。
+
+一般的に、^(r,[p_0,p_1...p_n]) という形で収束しないの? r が一つだったら...
+ネストしたらout。でもnestはあっても固定だから。
+
+が、これでcomputationをトレースできるのか? いや、特別な展開が必要。
+
+あと、determinization しないとね。(どうやって?)
    ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
-κݤˡpx_0 ˤ next Τߤ롣ɤ
+の際に、px_0 には next のみが入る。そうすれば良い。
     itl(p_0,more,..)
-ǤνϤnext,true,falseOk
+での出力はnext,true,false。Ok。
 
 Sun Nov  5 21:34:33 JST 1995
 
-ʤ * ^R 礭ʾ֤롣
-^R  true & ^R δĤ礭ʾ֤Ƥޤ(餷)
-ޤˤ? Ĥlength Ƭޤ뤳Ȥʡ
-Ǥ⡢äѤ礭ޤꡢޤʤ
-length(10) Ǥ빽礫..
-
-proj ǤƱ褦ϤäΤ...
-
-^r  permuation о򲿤Ȥʤ¤͡
-ѤʤǤ礦? ࡣ
-Ǥ⤵ǥ뼫ȤϾ.... ࡣ
-
-䡢ξ singleton removal ߤ
-
-singleton νʤ餸ʤ?
-
-singleton θ̤ͭ¤?
+しかし、なんと * ^R は非常に大きな状態を生成する。
+^R と true & ^R の干渉が大きな状態を生成してしまう。(らしい)
+これを抑えるには? 一つはlength で頭を抑えることだな。
+ああ、でも、やっぱり大きいか。あんまり、うまくない。
+length(10) でも結構巨大か..
+
+proj でも同じような問題はあったのだけど...
+
+^r の permuation の対称性を何とかしない限りだめだね。
+しかし、順序は変えちゃダメなんでしょう? うーむ。
+でもさ、モデル自身は小さいんだが.... うーむ。
+
+いや、この場合は singleton removal が効くみたい。そうか。
+
+これはsingleton の処理が正しくないからじゃない?
+
+singleton の効果は有限か?
       f(r^1,....r^n) -> exists
-Ȥͭ¡ɡꤷƤϤᡣ
+だとすれば有限。だけど、固定してはだめ。
       r^s ? length(1) : r^s ? length(2) : ....
-Ȥʤꤦ?
+となりうる?
 
 Wed Nov  1 21:12:04 JST 1995
 
-͡... <>^R ȤʤȤʤ....
-Ǥ⡢* ^R ϻȤ롣
+例題ねー... しかし、<>^R が使えないとなると....
+あ、でも、* ^R は使える。
 
 Mon Oct 16 16:05:31 JST 1995
 
-LITL ǡclosure, proj ȴpolynominal orderˡ!?
+LITL で、closure, proj 抜きだとpolynominal orderの方法がある!?
     ~(....&....(...&... ~(...&....)))
-Ȥǡvariable patternǤɤ
-marking  state space database Ϥʤ
-
-tableau expansion Ǥ⡢֤ƱŪpolynominal
-ˤʤäƤΤ....  ˡquantifier, closure, proj 
-verification 񤷤ʤäƤ
-
-䡢Ǥ⡢empty interval ȡ⤤ʤ?
+という形で、これにvariable patternを埋め込んでいけば良い。これだと
+marking だから state space database はいらない。
+
+tableau expansion でも、生成される状態は同じ数だから結果的にpolynominal
+になっていたのかも....  たしかに、quantifier, closure, proj を入れると
+verification は難しくなっていた。
+
+いや、でも、empty interval があると、そうもいかないか?
      ~(....&....(...&... ~(...&....)))
-Ǥդchopand,emptyѤ롣 exponential
+の任意のchopをand,emptyに変える操作がいる。これは exponential。
      p & p & p & p        & p
      p & p & p & p,empty  , p
-chomp (non-empty interval chop) ä顢ס
-
-Ǥ⡢closure, proj 򤤤ʤ餪ʤ
+chomp (non-empty interval chop) だったら、大丈夫。
+
+でも、closure, proj をいれるならおんなじか。
 
 Mon Oct  9 19:51:27 BST 1995
 
-proj Ǥϡr^n  n ز롣r^0 ϡ٤ƤγؤǶͭ롣
-¾length϶ͭʤȤߤΤΤlength(1) proj Q
-ȡr^1^1 = r^0^1 ?
-
-P proj Q ǡQ part next part ϡ
-proj encupsulated ƤΤǡterm ϤɬפϤʤ
-condition Ϥɬפ롣renaming  original clock
-level Ʊˤ limit ʣ
-Τϡɤʤterm level ⳬزСϤʤ
-(r^n)^n Ȥ...
-
-ɡsingleton removal ϡޤʤ͡줬ޤС
-ϰϤޤΤ.... ơeventuality Ʊ餤ޤǤˤǤ
-? r^s marking ȸФ櫓͡빽
-ɤȤФɤ
+proj では、r^n の n を階層化する。r^0 は、すべての階層で共有される。
+他のlengthは共有されないとみるのが正しいのだろう。length(1) proj Q
+だと、r^1^1 = r^0^1 だよね?
+
+P proj Q で、Q part のnext part は、
+proj の中にencupsulated されているので、term はいじる必要はない。が、
+condition はいじる必要がある。ただし、renaming を original clock
+level と同じにすると limit が効きすぎるだろう。しかし、ここを複雑に
+するのは、どうかなぁ。term level も階層化すれば、問題はない。
+(r^n)^n とか...
+
+結局、singleton removal は、うまくいかないね。これがうまくいけば、だい
+ぶ範囲が広まるのだが.... せめて、eventuality と同じぐらいまでにできな
+いの? あ、そうか、r^s をmarking と見ればいいわけね。しかし、結構、めん
+どくさいといえばめんどくさい。
 
 Time constant regular variable
 
-renaming ʤʤСȼ
+renaming なしならば、割と自明。
   r^0 ... r^limit
-unifyɤrenaming ȡ⤦ʣˤʤ롣r^n  state
-ȸΤñˤ衢ʤ¤줿͡
-
-renaming Ρäȵʹalgorithm...
+をunifyすれば良い。renaming ありだと、もう少し複雑になる。r^n を state
+と見るのが簡単。いずれにせよ、かなり制限された感じだね。
+
+renaming の、もっと気の聞いたalgorithmがあれば...
 
 Mon Oct  9 05:48:38 BST 1995
 
-^r -> true/false Ǥϡ[a](^r=length(2))  unsatisfiable.
-over(r) Ǥϡtrue/false ֤Ƥ롣^r -> +r/-r Ǥ⡢
-[a](^r=length(2))Ϥᡣˤ˹פ롣
-Ǥ⡢ϤäޤȤȤǤ⡢ɤ줯餤
-ޤʤ? local Ǥʤ餤?
-
-singleton  ^(r,s) ֤Ƥ⡢[a](^r=lenth(2)) ϡ> length(4)
-fail 롣ʤ?
+^r -> true/false では、[a](^r=length(2)) が unsatisfiable.
+over(r) では、true/false に置き換えている。^r -> +r/-r でも、
+[a](^r=length(2))はだめ。これにさらに工夫がいる。
+でも、それはこっちの方がましだということだろう。でも、どれくらい
+ましなの? local でないぐらいか?
+
+singleton を ^(r,s) で置き換えても、[a](^r=lenth(2)) は、> length(4)
+でfail する。なんで?
 
 Sat Oct  7 17:20:17 BST 1995
 
-singleton removal  r^s ǹԤʤȡlimit ĿФ̤
-餷älimitޤǤ褦ʾϾ֤롣
-r^s Ω˹Ԥʤ褦ˡǡȤǤΤ?
-Ǥʤ褦ʵ⤹롣
+singleton removal を r^s で行なうと、limit を一つ伸ばす効果が
+あるらしい。したがってlimitまでいくような場合は状態が増える。
+r^s の選択を独立に行なうような方法で、ちゃんとできるのか?
+できないような気もする。
 
 Sat Oct  7 10:08:57 BST 1995
 
-(1) ֹͤ (ֹlimit)
-
-ϡäƤߤɡ^r ˤϸ̤ɡ¾ΤϤۤȤ
-طʤʤ[a](^r...) ߤʤΤˤϤʤΤ
+(1) 番号を詰める (番号limitあり)
+
+は、やってみたけど、^r には効果があるんだけど、他のはほとんど
+関係ないなぁ。[a](^r...) みたいなものにはきかないのだろう。
 
 Fri Oct  6 09:46:45 JST 1995
 
-(1) ֹͤ (ֹlimit)
+(1) 番号を詰める (番号limitあり)
 (2) singleton removal
 
-ĤǤʤꤤϤ(2)ɤˤʤʤ?
-
-(3) ֹ¤ low resolution?
-
-Edge driven  logic ˤǤ뤫?
+この二つでかなりいくはず。(2)どうにかなんないの?
+
+(3) 番号を構造化する low resolution?
+
+Edge driven な logic にできるか?
 
 Thu Oct  5 18:27:29 JST 1995
 
-ࡣlength limit ϡޤʳ¤ޤ
-ޤʤ͡
-
-rename  ^r ο¤ˡȡover ѴΤ
-ޤ˥ɥۥå˷ޤäƤޤ
+うーむ。length limit は、うまくいくが、それ以外の制限がいまいち
+うまくいかないね。
+
+rename して ^r の数を制限する方法だと、over に変換されるものが
+あまりにアドホックに決まってしまう。
     r^n
-  n  ˡ term äʤ?
-
-total order ä뤫... ̤?  ...
+の  n  に、何か term を持って来れないの?
+
+total order を持って来るか... 効果あるの?  さぁ...
 
 Sun Sep 24 01:14:36 JST 1995
 
-顢
-
-^r = false ˤȡ
+だから、
+
+^r = false にすると、
 
 [a](^r=legth(2)) -> [a](false=legth(2))
 [a](false=legth(1))
 [a](false=legth(0)) = unsatisfiable
 
-ˤʤ뤫ʤΡ󤦤
-true = length(2)  false = length(2)
-⡢ξȤunsatisfiableɤ餫Ȥȡ
+になるからだめなの。うんうん。
+true = length(2) も false = length(2)
+も、両方ともunsatisfiable。どちらかというと、
     (length(2);not(length(2)))  & true
-ȤʤΤ
+となるのが正しい。
     (length(2) & true) ; (not(length(2))  & true)
-?  Ok ʤϤ
-
-ä顢expansion singletonåơsingleton
-ФƤ quantifiy ƤޤäƤΤ? ...
-
-㤢ʤ ^r -> ^r;not(^r) ǤϤʤΤ?
-ϡͭΤ򤤤äˤƤ뤫顣
+は? これは Ok なはず。
+
+だったら、expansion する前にsingletonをチェックして、singleton
+に対しては quantifiy してしまうってのは? うーむ...
+
+じゃあ、なんで ^r -> ^r;not(^r) ではだめなのか?
+これは、終りを共有するものをいっしょにしているから。
 
 ^r on n+1
    |--|   T
@@ -775,7 +836,7 @@
     ||    F
      ||   F
 

+とする
 
 ^r on n
   |---|
@@ -783,12 +844,12 @@
   |-|    
   ||
 
-ΡϡΩդդ
+が新しいもの。これらは、独立。ふんふん。
 
 Tue Sep 19 23:53:19 JST 1995
 
-ɤѤʡ
-down(r^0)      true;false ȤϤɤ㤦?
+どうも変だな。
+down(r^0)  と    true;false とはどこが違うんだ?
 state(1 , not(true& ?(^r,not(@ @empty),@ @empty)&true))
                       [a](^r = length(2))
 [empty,down(r,0),up(r)]->false
@@ -808,138 +869,138 @@
                       not(length(1)&true)
 [more,not(down(r,0)),not(up(r)),ev(r^0)]->3
 
-äѤ㤦true ȡlength(1)true length(2)falseȤ
-ʤϤξΩ򤷤ʤƤϤʤʤ
-(?ɡtrue;false ʤ... ätrue?)
-+r, -r ޤ?
+やっぱり違う。true だと、length(1)でtrue length(2)でfalseという
+技が出来ない。この選択はこの場所で独立に選択しなくてはならない。
+(ええ?だけど、true;false なんだから... だったらtrueか?)
++r, -r の方がましか?
 
 Sat Sep 16 11:44:25 JST 1995
 
-singleton ^r  true, false ֤ȡ[]true,[]false ΰ̣
-ʤäƤޤºݤϡtrue/false ʤΤˡ顢singleton removal
-Ϥޤʤ
+singleton ^r を true, false に置き換えると、[]true,[]false の意味に
+なってしまう。実際は、true/false なのに。だから、singleton removal
+はうまくない。
 
 t0:   ^r  = length(2)
 t1:   r^0 = length(1)    empty/not(r^0)
 t2:   r^0 = mpty(1)      empty/r^0
 
-Quantifier֤? äĤƤޤ?
-operator?
+Quantifierに置き換える? だったら残しておいた方がまし?
+何かoperatorを作る?
   some -> true/false
-quantified true? <>false ? not([](true)) = not(not(true & not true))). 
-Ǥ⡢ȤĤfalseˤʤäƤޤoperatorˤȡdeterministic
-Ǥʤʤ뤫Ϥޤnegation
+quantified true? <>false かな? not([](true)) = not(not(true & not true))). 
+でも、これだといつかはfalseになってしまう。operatorにすると、deterministic
+でなくなるか。それはまずい。negationが。
 
 Fri Sep 15 11:26:13 JST 1995
 
-singleton check itlˤ뤳ȤϤǤʤ?
+singleton check をitl時にすることはできない?
 
 Wed Sep 13 18:24:24 JST 1995
 
-ɡRITL CFG ޤǤΤ顢Regular Subset 뤳Ȥ
-Ǥʤ
-
-^r depth¤С٤ϤǤ롣Ǥ
-fairnessˤϤʤʤ͡
-
-depth ʳ¤? ֿ¤˾ޤ
-
-singleton  remove ǤʤΤȤȸСʤΤ
-
-singleton remove Υߥ?
-   itlλ detect?
-   itlstd λ detect?
-remove λ
+結局、RITLは CFG を含んでいるのだから、Regular Subset を決めることは
+できない。
+
+^r のdepthを制限すれば、ある程度はできる。しかし、これでは
+fairnessにはならないね。
+
+depth 以外の制限は? 状態数の制限が望ましい。
+
+singleton の remove でかなりのことが出来ると言えば、そうなのだが。
+
+singleton remove のタイミング?
+   itlの時に detect?
+   itlstd の時に detect?
+remove の仕方
    eventually(^r,N)
    eventually(not(^r,N))
-롣ȤȤϡitldecomp  show ľ
-Ԥɤ
-
-ΤʾֽϤǤϤʤǤϤʤŪ˥ȥ졼
-ǤʬϤäƤmark դΤǤƱˤʤäƤޤ
-Ϥremove
-
-^rνи٤򲡤뤳Ȥǡlogicˤʤ뤫? 㤨2ĤȤ?
-
-*  consistent ˤʤʤ==safeǤʤ(ɸפ...)
-*  ǤʤƤɤȤͤ⤢롣characterriseǤ?
-
-ˤ衢singleton removal ǤɤޤǤʡ
+を挿入する。ということは、itldecomp の show の直前で
+行えば良い。
+
+しかし、これだと正確な状態出力ではない。ではないが原理的にトレース
+できる部分をはしょっているだけ。mark を付けるのでは同じになってしまう。
+やはりremoveしたい。
+
+^rの出現頻度を押さえることで、logicになるか? 例えば2つとか?
+
+*  consistent にならない==safeでない(標準形を工夫すれば...)
+*  でなくても良いという考え方もある。characterriseできる?
+
+いずれにせよ、singleton removal でどこまでいくかだな。
 
 Sun Jul 23 10:16:02 JST 1995
 
-* ^r ->  +r, -r   depth ˤäΩ
-* +r  r^depth ˤ
-
-ȡ[a](^r),<>(not(^r))satisfiable
-
-* ^r ->  +r, -r   depth ˤäΩ򤷤ʤ
-
-ȡ[a](^r=length(2))unsatisfiable
-
-ࡢޤ
+* ^r ->  +r, -r   depth によって独立に選択
+* +r も r^depth により選択
+
+これだと、[a](^r),<>(not(^r))がsatisfiable
+
+* ^r ->  +r, -r   depth によって独立に選択しない
+
+と、[a](^r=length(2))がunsatisfiable
+
+うーむ、うまくいかん。
 
 Sat Jul 22 12:52:11 JST 1995
 
-* depthΰ㤤chopνǹԤʤ
-* ^remptyȡ+r, -remptyΩ
-* ^rmoreȡ+r, -rδط
-
-  +r, -r ϡۤʤdepthT/Fλ
- +r ϡ˹ήɤ
-+r/\-r Ȥʤ뤳ȤϤʤfalse
+* depthの違いはchopの処理で行なう
+* ^rのemptyと、+r, -rのemptyは独立
+* ^rのmoreと、+r, -rの関係
+
+  +r, -r は、異なるdepthでT/Fの時に生じる
+既に +r がある時は、それに合流して良い
++r/\-r となることはない。それはfalse。
 
 |-------|       +r
 |---------|     -r
-   ^r  +r Ȥ
-   not(^r)ä-rȤ
-
-Ǥ?
-   tailͭrǤ not(^r),^rΰо
-   ^r/-rȹ礻?
-
-+r, -r ä
-
-* +r or -r empryˤʤȤ
-      -r emptyˤʤʤ
-
-+rĤäƳ뤫? -rʤдطʤ
-֤뤱ɡ
+   ^r  +r とする
+   not(^r)があったら-rとする
+
+これでいいか?
+   tailを共有するrである not(^r),と^rの扱いは対称
+   ^r/-rの組合せは?
+
++r, -r が解消される場合
+
+* +r or -r がempryになるとき
+      -r はemptyにならない
+
++rが残って害があるか? -rがなければ関係ない
+状態は増えるけど。
 
 Fri Jul 14 18:31:19 JST 1995
 
-ۤʤ chop ǡۤʤrֹդ롣
-ֹ up(^r), down(r,n) Ԥʤ
-
-ˤäơ٤Ƥȹ礻롣
-
-ֹϾ֤ˤղäʤ(Τ?)
-ƱintervalǤϡ
+異なる chop で、異なるrの番号を付ける。
+その番号毎に up(^r), down(r,n) を行なう
+
+これによって、すべての組合せが一応得られる。
+
+番号は状態には付加しない。(いいのか?)
+同じinterval上では、
     r, not(r)
-... ... ޤ
+があり得る... これは... 気まずいか。
     ^r ->   +^r, -^r
-Ȥ? ... +up, -up ?
-
-ޤƤߤ褦(äѤä...)
+とする? すると... +up, -up がある?
+
+まあ、試してみよう。(やっぱりだめだった...)
 
 Thu Jul 13 14:05:06 JST 1995
 
-r^n ο򸺤餹
-  => ǥˡɽ
-
-singleton r^n Ͼä
-
-doubleton r^nɤͻ礷
-
-rr^nŪ (ϤǤΤ... +r/-r)
-ΤϡޤäΤ­ʤΤ롣ֿ
-­ʤ
-
-* ɬפʾֿΤߤ̤
-* Ʊ̤ѿ϶̤ʤ
-
-ʬȤƱɤ / 㤦ȤȤФʤȤʤ
-   Ʊäطʤ
+r^n の数を減らす
+  => 等価でユニークな表現
+
+singleton r^n は消せる
+
+doubleton r^nどうしを融合したい。
+
+新しいrをr^nに相対的に定義する (それはできるのだが... +r/-r)
+のは、うまくいったのだが、足りないものがある。状態数が
+足りない。
+
+* 必要な状態数のみを区別する
+* 同じ結果を生じる変数は区別しない
+
+自分自身と同じかどうか / 違うということを覚えないといけない
+   同じだったら関係ない
 
 What happen in next case? ([a](^r))
 
@@ -948,9 +1009,9 @@
     ---|-----| r^5
     ---|----| r
 
-r^5аĸ롣ʤr^6ǰ롣
-ξƤϤʤr^5  ^r Ȥϴط̵
-̤ƱȤط롣( 狼ʤ褦.... )
+r^5が落ちれば一つ減る。減らなければr^6で一つ増える。しかし、
+この場合は増えてはいけない。r^5 と ^r 自身は関係が無い。
+が、結果は同じという関係がある。( うがー、わからないよう.... )
 
 st6:
 not(r^5) & true, r^5 & true, ^r  & true, not(^r) & true
@@ -967,12 +1028,12 @@
 f(^r) =>   contratint_1(^r) & continuation_1(^r)
 g(^r) =>   contratint_2(^r) & continuation_2(^r)
 
-r(r^n)&c(r^n) n
-r^n => r^n' 롣
-ɡ̤ɬʤ(...)
-
-r^nquantifyɤȤȤϡƱʤäɤȤ?
-ȤȤcross term ?
+r(r^n)&c(r^n) がnを除いて等しい時、
+r^n => r^n' がいえる。
+けど、別に等しい必然性もない。(たしかに...)
+
+r^nはquantifyして良い。ということは、同じなら消して良いということ?
+ということか。cross term は?
    exists(^r, empty(^r)? ...)
 
 r0: {    +r(const, continu), 
@@ -980,33 +1041,33 @@
 r1: {    +r(const, continu), 
          -r(const, continu)  }
 

+いつかは
 	+r(empty,continu)
 	+r(true,continu)
-Τɤ餫ˤ䡢ʤemptyʤ̵true(?)
+のどちらかにいく。いや、いかない。emptyなら問題無い。trueが問題(?)
      +r(fixpoint,contiu)
-Ȥˤʤ롣줬¸ߤȤȤˤʤ롣
+という形になる。これがたくさん存在するということになる。
      +/-r^n(fixpoint_k,continu_k_i)
-Ȥ櫓ξr^nνŤʤ꤬äǤϲ衣
-ޤʤ...
+というわけだ。この場合のr^nの重なりが解消できれば問題は解決。
+うまくいかないね...
     
 
-ǡƱΤϾäɤ򤽤ʤȾäˤ
-㤦rǤƱåʤäɤ(reular variableϡ¼
-, ^r =>  r,^common ˤ뤫? ϤäȰ㤦)
-ξϾäƤⴳĤΥѥѤʤĥѥ
-Ȥ˥ޥå󥰤Ȥ뤫顣(ͭ¤ȹ礻ʤΤ?)
-
-äΤterm levelǤʤ?
+で、同じものは消して良い。順序をそろえないと消しにくい。
+違うrでも同じカッコなら消して良い。(reular variableは、実質は
+一つ, ^r =>  r,^common にするか? それはちょっと違う)
+この場合は消しても干渉のパターンが変わらない。干渉パターン
+ごとにマッチングをとるから。(有限の組合せなのか?)
+
+消すのはterm levelでおこなう?
       c(r^n, i_n...) & ...
       c(r^n, i_n...)
-Ȥtermr^n˴ؤƤϤǤƤʤää顢¾
-ˡϤøǤס
-
-f(r^n)f(r^n'1)δط
+というtermしかr^nに関してはでてこない。消せるんだったら、他の
+方法はいい加減でも大丈夫。
+
+f(r^n)とf(r^n'1)の関係
   |------|-|
     |----|-|
-r^n, r^n' ȤΩ
+r^n, r^n' 自身は独立
 
 r^1(r,c)
 r^2(r,c)
@@ -1017,7 +1078,7 @@
     more(r),r^1(@(r),c),r^2(@(r),c)
 ==
   r^1(c);c,more(r),r^1(@(r),c);more(r),r^1(@(r),c),r^2(@(r),c)
-¾r^nȴĤˡѤäƤޤ...
+他のr^nと干渉する方法が変わってしまう...
 
 
 Sun Jul  9 15:32:43 JST 1995
@@ -1026,52 +1087,52 @@
   r^2 & true;
   r^3 & true
 
-ĤˤޤȤʤ?
-
-   f(+/- r^n)                    (ɬtopˤ/ŸƤ뤫)
+一つにまとめられない?
+
+   f(+/- r^n)                    (必ずtopにある/一度展開されているから)
    |-------------|-----------|
                down(r^n) => true/false
 
-
+性質
    f(+/- r^n)
        down(r^n)      =>  f((+/-true ,empty))
        not(down(r^n)) =>  f(+/- r^n)
-         parallel term̵ʤޤŸ
-	     r^n, *length(3) ʤɤ? ̵뤷ɤ
-	     r^n, *length(3) & true 
+         parallel termがある時は無くなるまで展開する
+	     r^n, *length(3) などは? これは無視して良い
+	     r^n, *length(3) & true が問題
                 => evenrually true + *length(3)
 
-顢nʣäƤ⡢f((+/-true ,empty))ƱʤƱǤ褤(?)
+だから、nが複数あっても、f((+/-true ,empty))が同じなら同じでよい(?)
 
    f(+/- r^n)  => true & down(r^n),f(+/-true,empty)
       => down(r^n) =  eventually(f(+/-true,empty))
 
-ȤȤϡäѤdown(r^n)򳰤˽ФȤ?  
-r^n & true ʤ         eventually(true)
-not(r^n) & true ʤ?
-
-դࡣ eventually(f)  f ˤr^nʤ
-뤫Τʤ
-
-chopνλˡeventuality listbdtηdz˽Фɤ
-eventuality 줿r^nΩ(
-ͤ...)
+ということは、やっぱりdown(r^n)を外に出せるということ?  
+r^n & true なら         eventually(true)
+not(r^n) & true なら?
+
+ふむ。そして eventually(f) の f にはr^nは入らない。これは
+いけるかも知れない。
+
+chopの処理の時に、eventuality listをbdtの形で外に出せば良い。
+eventuality が満たされた時がr^nが成立した時。(これも
+前考えたな...)
   ^r & ....
-Ȥ?
-
-   (^r, g) & f  => ev(f),(g & f)   äȰ㤦...
+という形だけ?
+
+   (^r, g) & f  => ev(f),(g & f)   ちょっと違う...
    (^r & f),(g & f)
 
-ȤϾۤʤ衣not ޤʤϤ
+とは少し異なるよ。not がうまくないはず。
     not(ev(f)); not(g & f)  (?)
 
-... ev(f)С^rɤ()
-ʤƤ⤤
-
-äevenruality formITL񤭴Τ?
+そうか... ev(f)が満たされれば、^rは落ちて良い。(落ちれる)
+落ちなくてもいい。
+
+前もってevenruality formにITLを書き換えるのは?
     f(r) => g(eventualy(h))
 
-diceidableʤΤ? 񤱤Ȥ...  
+本当にdiceidableなのか? 整数方程式が書けるとすれば...  
 
 Fri Jul  7 18:51:32 JST 1995
 
@@ -1079,7 +1140,7 @@
   r^1 & true;
   r^2 & true;
   r^3 & true
-Ȥʤ롣ȤȤϡҤȤĤinterval򸫤Ƶۼ뤳ȤϽʤ 
+となる。ということは、ひとつのintervalだけを見て吸収することは出来ない。 
 
             t1  t2
             up(r)         down(r^1)
@@ -1087,40 +1148,40 @@
 not(r&true)  |----------------|not(down(r^1)----
              |---|up(r)----|not(down(r^2)-------
 
-r^1 ϶礹r^1طʤäñȤ
-ФƤr^1ϸ߻
+r^1 は競合するr^1がある時しか関係しない。したがって単独に
+出てくるr^1は現在時点で
   fin(r^1)      => true
   fin(not(r^1)) => false
-ɤǡtrue & ^r & true ϼ«롣
-Ǽ«뤫? ֤󡢤ʤ
+を決めて良い。これだけで、true & ^r & true は収束する。
+が、それだけで収束するか? たぶん、しない。
 
 (1)
-ʣλľ֤ĤˤޤȤФǤ롣+r, -r Ϥ
-ˡäĤˤϤʤʤͭ¤ȹ礻ˤʤ롣
+複数の始点を持つ状態を一つにまとめられればできる。+r, -r はそういう
+方法だった。が一つにはならない。有限な組合せになる。
 
 (2)
-«ȤСͭ줿r^nȤͭ¤ʾǤ롣ϡfiniteness
-ξ롣äƶͭǽΤtermǤ뤫? (
-֤Ǥ) 
-
-äʣФ褿(㤦sytactical interval)^rֹդ
-̤ƤϡۤʤֹǤʤ? 
+収束するとすれば、共有されたr^nの組が有限な場合である。これは、finiteness
+の条件に相当する。前もって共有される可能性のあるtermを生成できるか? (
+たぶんできる) 
+
+前もって複数出て来た(違うsytactical interval上の)^rに番号を付けて
+識別しておく。競合は、異なる番号上でしか起きない? 
    [](<>(^r))  = not(ture & not(true & ^r))
-Τ褦ʾ? Ʊֹζͭ+r, -rǹʤ
-(true or false )
+のような場合は? そうか。同じ番号上の共有は+r, -rで構わない。
+(true or false だから)
    [](<>(^r))  <-> [](<>(^r)) 
-Τ褦ʾ?
+のような場合は?
 
 Fri Jun 30 20:08:47 JST 1995
 
 f(r^1,r^2,r^3) & true, 
 g(r^1,r^2,r^3) & true
 
-f(r^1,r^2,r^3)g(r^1,r^2,r^3)򸫤ʤr^nο򸺤餵ʤȤʤ 
-
-r^n ϡemptyλƶʤmoreλtrueƱ
-
-^r Τߤr^n䤹򤤤˵ۼ뤫Ĵ٤ɤ?
+f(r^1,r^2,r^3)とg(r^1,r^2,r^3)を見ながらr^nの数を減らさないといけない。 
+
+r^n は、emptyの時しか影響しない。moreの時はtrueと同じ。
+
+^r のみが新しいr^nを増やす。これをいかに吸収するかを調べれば良い?
 
 f(r^cur,r^1,r^2,r^3) & true, 
   =>   r^cur ? +f(r^1,r^2,r^3) : -f(r^1,r^2,r^3)  & true
@@ -1130,51 +1191,51 @@
 
 Fri Jun 30 10:48:46 JST 1995
 
-stateˡregular variablemapƤ롣ˡޤ
-狼ʤ^r줿֤̤뤳Ȥɬס
-
-^r(s)  äƤߤ롣Τä
+各stateに、regular variableのmapを割り当てる。方法がいまいち
+わからない。^rの生成された状態を識別することが必要。
+
+^r(s)  をやってみる。昔もやった。
    true & ^r 

+が爆発する
    r^1 ; r^2; r^3;  ...  ; true & ^r 
-줬
+これが
    r^1 true & ^r 
-Ȥʤɤ
+となれば良い。
    r^1 .... r^2
-Ͽr^nˤʤ롣(ߴط?) ^r ɤݻ
-äȤ⾯ʤr^n򤹤ɤ(Ѵsafe & compete?)
-ߴط¸ʤʤ^r򤹤٤ƶ̤ˤɤ
-Ϥޤʤ
+は新しいr^nになる。(相互関係は?) ^r どうしの制約を保持した
+もっとも少ないr^nを選択すれば良い。(この変換はsafe & compete?)
+相互関係を保存しないなら^rをすべて共通にすれば良い。が、
+それはうまくいかない。
    r^1 , not(r^2)  -> r^1, not(r^1) -> false
-Τ褦ʾ礬뤫顣
+のような場合があるから。
    r^1 , not(r^2)  -> r^1
-? 
-
-¾ѿ? r^1 .. r^n ˰¸termѴ
-׻롣= BDT  leaf οɽǤǾr^n
-롣
-
-Сtemporal operatorΥͥȤѤʤΤ顢
-Τͭ¤ˤʤϤ
-
-ǤʤfullǤʤregularˤʤ? ^r context dependent
-Ǥʤ顣 r^1 , not(r^2)  -> r^1 ϡcontext dependent Ǥ
-Ǥʤ(ʤۤ...)
+か? 
+
+他の変数が入る場合は? r^1 .. r^n に依存するtermの変換を
+計算する。= BDT の leaf の数。それを表現できる最小のr^nを
+作る。
+
+そうすれば、temporal operatorのネストは変わらないのだから、
+全体は有限になるはず。
+
+これでなんでfullでなくてregularになるの? ^r がcontext dependent
+でないから。 r^1 , not(r^2)  -> r^1 は、context dependent では
+できない。(なるほど...)
 
 Wed May 24 20:32:34 JST 1995
 
-^rϡϤꡢ
+^rは、やはり、
     ^r -> +r, -r
-ѴǤʤȤ٤ǥϡRITL
-ޤǤ롣ȤΥå򤹤ɤ
+の変換でなんとかするべき。こうして生成したモデルは、正しいRITLを
+含んでいる。あとは整合性のチェックをすれば良い。
 
 (1) local consstency check   => regular variable
 (2) global consistency check => regular constant
 
-ɤ褦check? ....
-
-
-Τbdcomp.pl bddlibǽ񤭴롣
+どういうようにcheckするの? ん....
+
+
+昔のbdcomp.pl をbddlibで書き換える。
 
 characteristic function f(q)
    f(q) = more,fx_q(sbn,sbx,P);empty,fn_q(P)
@@ -1184,43 +1245,43 @@
 
 Tue May  2 17:49:35 JST 1995
 
-BDDLIBȤ߹碌äѤ Prolog <-> BDD Ѵ
-٤ʤäbdtstd.pl ˤʤΤ
-
-äBDD٤ʤä(BDT/*) ϡ
-    BDD  leaf next leafŸ
-    BDDκƹ
-    next leaf2-3 treeϿ
-    next leaf 򤵤Ÿ
-ȤΤ٤ä顣
-
-Charcteristic Function 夲ˡϡǤBDDLIBʤ
-ޤ⤷ʤ
-
-Subtermäơ٤ơ
+BDDLIBを組み合わせたが、やっぱり Prolog <-> BDD の変換が入るだけ
+遅くなるだけだった。bdtstd.pl は綺麗になるのだが。
+
+前作ったBDDの方式も遅くなるだけだった。(BDT/*) それは、
+    BDD の leaf をnext leafに展開
+    BDDの再構成
+    next leafを2-3 treeに登録
+    新しいnext leaf をさらに展開
+というのがすごく遅かったから。
+
+Charcteristic Function を作り上げる方法は、今一だ。でもBDDLIBなら
+うまくいくかもしれない。
+
+Subtermを前もって、すべて、
     condition, next
-ȤBDDŸƤ?
-
-QuantifierʤɤϡSubterm˾֤Ƥޤ顢
-äơŸƤ
-
-СȤνϡBDDΤߤǤǤϤ(CFˡ
-̤Ʊ?)
+というBDDに展開しておいたら?
+
+Quantifierなどは、Subtermの中に状態が現れてしまう。だから、
+前もって、中を展開しておく。
+
+そうすれば、あとの処理は、BDDのみでできるはずだ。(しかし、CF法と
+結果は同じ?)
 
 Wed Mar 29 17:22:43 JST 1995
 
 regular(r,....r....)
-ȤȤ ( QPTL <-> RITL ... )
-
-QuantifierľܻȤΤ?
+という形を使う ( QPTL <-> RITL だから... )
+
+Quantifierを直接使うのは?
    st(0) = exists(c, c->st(1),not(c)->st(2))
-...
+さぁ...
 
 begin(r,formuala) -> T/F
 end(r,formula)    -> T/F
 
-ۤʤ뤦formula¤Ʊä-> Ĥ regular(r, f)
-ȤƱˤʤ롣
+異なるうformulaが実は同じだった。-> いつか regular(r, f)
+という同じ形になる。
 
 regular(r,f(r))
     empty(f(r))      ->  r=true,empty
@@ -1229,17 +1290,17 @@
     more(f(r))      ->   r=true,regular(r,fx(r))
     not(more(f(r))) ->   r=false,regular(r,fx(r))
 
-äǥϾĹ
-
-chop 褿 r reset ʤȤʤ
-(...)  ä顢regular(r,f(r))Ϥʤ?
-ɤä? r ääƤΤ?
-
-PDA Ȥδط?
+したがって生成されるモデルは冗長。
+
+chop が来た時に r をreset しないといけない。
+(だよね...)  だったら、regular(r,f(r))はいらない?
+どうやって? r を前もって宣言するってのは?
+
+PDA との関係は?
 
 Thu Dec 15 20:21:58 JST 1994
 
-ModelȤб
+Modelとの対応
 
      t0 -[+-]-> t1 -[+-]-> t2 -[+-]-> t3 
 
@@ -1248,34 +1309,34 @@
                 |-----------|-----------|
                 r0'        r1'         r2'
 
-r0 Ͼ0Ϥ롣
-Ϥ롣
-r0 -[-]-> r1 ǽǤ˥եȤ롣
-r0 -[+]-> r1 Ǽλ֤ΤΤȰ㤦FAǤ뤳Ȥɽ
+r0 は常に要素0から始める。
+から始める。
+r0 -[-]-> r1 で集合の要素にシフトする。
+r0 -[+]-> r1 で次の時間のものと違うFAであることを表す。
 
 Mon Nov 28 19:27:37 JST 1994
 
-RITLơȤITL formulaboolɽboolBDDɽ롣
-
-ȤITL formulaȤsubtermν顢Ťboolˤʤ롣
-äơdouble exponential algorithmȤʤ롣
-
-r/not(r) flip Ǥϡ٤Ƥȹ礻뤬٤Ƥȹ礻
-ϢɽǤʤäơ٤Ƥȹ礻Ȥä

-

-   r/not(r) flip LITL򽸹Ȥƻ (implementation?)
-
-   r 
+RITLステートをITL formulaのbool代数で表す。bool代数はBDDで表現する。
+
+もともとITL formula自身がsubtermの集合だから、二重のbool代数になる。
+したがって、double exponential algorithmとなる。
+
+r/not(r) flip では、すべての組合せは生じるが、すべての組合せの
+連結は表現できない。したがって、生じたすべての組合せをとって
+おけば良い。
+
+集合の作り方
+   r/not(r) flip で生じたLITLを集合として持つ (implementationは?)
+
+   r の例
        [1]    r -(+r)->     r, r -(-r)-> not(r)    {r,not(r)}
-       [2]    r -> {r,not(r)} -> {r,not(r)}   ()
-
-   t & r  (detailϰۤʤ롣emptyξ礬뤫)
+       [2]    r -> {r,not(r)} -> {r,not(r)}   (終り)
+
+   t & r の例 (detailは異なる。emptyの場合があるから)
        [1]    t & r -(+r)-> r\/t & r, t & r -(-r)-> not(r)\/t & r
               {r\/t&r, not(r)\/t&r}
-       [2]    {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} ()
-   [a](r=length(2))
+       [2]    {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} (終り)
+   [a](r=length(2))の例
        [1]     [a](r=length(2)) -(+r)- >     r =length(1)/\[a](r=length(2))
                                 -(-r)- > not(r)=length(1)/\[a](r=length(2))
                {r =length(1)/\[a](r=length(2)),
@@ -1286,40 +1347,40 @@
                  r =length(0)/\ ~r =length(1)/\[a](r=length(2)),
                 ~r =length(0)/\  r =length(1)/\[a](r=length(2)),
                 ~r =length(0)/\ ~r =length(1)/\[a](r=length(2))}   F
-       [3]      =>    [2] 
-                   or [1]' (r=length(1)trueξ)
-
-äȥѥȤˤʤ󤸤ʤ? (finiteness)
-ITL(r)ϡrr/not(r)ǤդִΤsubsetɤȤɤ줬פ뤫
-ФɤΤǤ? => ϻΤס
-IndexդΤϥᡣ=> ǥ뤬ͭ¤ˤʤʤ(ࡢ狼ʤ)
-
-    ITL(r) => Ÿ => subset
-
-
-ǥβ
-
-   boolϡrassignmentͿȲ褹롣Ĥ
-   Ρɤ̤ʲͭ뤳Ȥ⤢롣
-
-   Term֤ǤդܤΤ?
-   ǤϤʤơƱܤ롣
-
-   ۤʤ볫ϻrϡƱ˰ۤʤܤ
-   ٤Ʋǽܤ櫓ǤϤʤĤFȤʤػߤȤʤ
-       => r Ф
-
-¹ԤǤ?
-
-   boolΰĤinstanceŬ˼¹Ԥɤ
-
-Rñautomaton꿶뤳Ȥϲǽ?
+       [3]      =>    [2] へ
+                   or [1]'へ (r=length(1)がtrueの場合)
+
+もっとコンパクトになるんじゃない? (これだとfinitenessは明解だけど)
+ITL(r)は、rをr/not(r)に任意に置換したもののsubset。どれとどれが一致するかを
+覚えれば良いのでは? => 開始時点が等しいものが一致。
+Indexを付けるのはダメ。=> モデルが有限にならない。(うーむ、わからない)
+
+    ITL(r) => 展開 => subset
+
+
+モデルの解釈
+
+   bool代数は、rのassignmentが与えられると解決する。しかし、一つの
+   ノードが別な解釈を共有することもあり得る。
+
+   Term間は任意に遷移するのか?
+   そうではなくて、同時に遷移する。
+
+   異なる開始時点を持つrは、同時に異なる遷移を廻る
+   すべて可能な遷移があるわけではなく、いくつかはFとなり禁止となる
+       => r に対する制約
+
+実行できる?
+
+   bool節の一つのinstanceを適当に実行すれば良い
+
+Rに単一のautomatonを割り振ることは可能か?
    [a](R = r)  where r is automaton constant
 
-֤̤äƥǥ
-
-   ˤäơstate minimizationƱ餻뤳ȤǤ
-   MinimizationΥƥȥץäƸ뤳
+時間を遡ってモデルを作る
+
+   これによって、state minimizationも同時に走らせることができる
+   Minimizationのテストプログラムを作って見ること
 
 Thu Nov 24 14:54:00 JST 1994
 
@@ -1330,30 +1391,30 @@
 
 LTTL = LITL on compact time
 
-Even(p)ϡLITLǤᡣ
-    (p.)* Ǥʤ
+Even(p)は、LITLでもだめ。
+    (p.)* ができない
     (abac)* -> (a[bc])*
 
 LITL -> LTTL converter
 
-LITL/LTTLϡäѤ귲
+LITL/LTTLは、やっぱり群を構成する
 
 []a & []b & []a
 a...ab...ba...a ->  a until (b until []a)
-    conversionǤ?
-a & b & a
+    だからconversionできる?
+a & b & aは
      a, <>(b, <>a)
-... Ǥʵ...
-
-P & Q ->   start(P),(run(P) until lttl(Q)) ѷ
-           run(P)ˤquantifierΤ? ʤ?
+か... うう、できそうな気がする...
+
+P & Q ->   start(P),(run(P) until lttl(Q)) に変形する
+           run(P)にはquantifierが入るのか? 入らない?
 
 events      continue
 |----------|..........|
 |-> <>(events)
            |-> [](continue)
 <>events,  <>(continue until Q))
-Ȥ褦compile롣դࡣ
+というようにcompileする。ふむ。
 
 l(P) & Q    l(P) = LTTL formula of P
    <>(P) ->  <>(P,<>(l(Q)))
@@ -1366,11 +1427,11 @@
 
     R -> +(R) -(R) on Start Time
 
-    empty(R)  hidden ɡ+R/-R ˴ؤƤƱ
-    ޤɤʬʤ
-
-    Modelľܹʤfiltrationΰ̣Ǥ...礭뤫顣
-    ꡢModel constraint롣
+    empty(R) は hidden だけど、+R/-R に関しては同期する
+    ここがまだ良く分からない。
+
+    Modelを直接構成しない。filtrationの意味でも...大きすぎるから。
+    その代わり、Model constraintを構成する。
 
 Generating C / In-kernel implementation
 
@@ -1547,9 +1608,9 @@
 
 Tue Sep 15 13:04:43 JST 1992
 
-ɡRegular variable state ͭʤȼ«ʤ
-ͭǤ뤫ɤȽǤŪ顢ˡǤ
-Ǥʤ餷
+結局、Regular variable state を共有しないと収束しないし、
+共有できるかどうかの判断は大域的だから、この方法では
+できないらしい。
 
 Tue Sep 15 11:36:36 JST 1992
 
@@ -1591,24 +1652,24 @@
 
 Mon Sep 14 00:25:08 JST 1992
 
-^r automatonϡ^r̤ѿȸtableau
-subsetǤ롣äơtableaunodeؤȤ ^r Υǥ
-뤳Ȥ롣ޤʤ...
-
-(^r & true),not(^r) ΥǥϤʤ
-
-ǡstay(r,N)Ȥ  (up(r),emtpy & true & down(r),empty) ǤϤᡣ
-^r & ^r -> ^r ˤʤäƤޤ顣
-
-ȥǥ빽ۤ«ʤ  -->  Full ITL 
-
-RITLΥǥͭ¤ stay(r,N)Τʤʬ
-ߤɤɤȽǤ뤫ꡣ
-
-Deterministic PathƱstateȽǤΤǤ­ʤ
-Loopʤ顣
-
-ष٤ΤDefaultǡɬפʻʬΥΤ˾ޤ
+^r で生成されるautomatonは、^rを普通の変数と見て生成するtableauの
+subsetである。従って、tableauのnodeを指し示すことで ^r のモデルを
+作ることが出来る。しかし、うまくいかない...
+
+(^r & true),not(^r) のモデルはないから
+
+そこで、stay(r,N)を使う  (up(r),emtpy & true & down(r),empty) ではだめ。
+^r & ^r -> ^r になってしまうから。
+
+するとモデル構築が収束しない  --> これは Full ITL だから
+
+しかしRITLのモデルは有限だから stay(r,N)のかなりの部分は
+相互に等しい。等しいかどうかをどう判断するかが問題。
+
+Deterministic Pathが等しければ同じstateと判断するのでは足りない
+Loopが作れないから。
+
+むしろすべて等しいのがDefaultで、必要な時だけ分離するのが望ましい
 
 Mon Jan  1 11:05:38 JST 1990
 
@@ -1938,7 +1999,7 @@
       a path must not contain false eventuality
 
 
-iΤϼ&ο
+iのは式の中の&の数に等しい
 
 empty
    0  true
--- a/rstd.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/rstd.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -8,7 +8,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@csl.sony.co.jp
- $Id$
+ $Id: rstd.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
 */
 % ITL subterm standarization with BDT
 %
--- a/verilog.pl	Fri Nov 07 20:36:40 2008 +0000
+++ b/verilog.pl	Fri Apr 22 16:47:13 2016 +0900
@@ -7,7 +7,7 @@
  use this wording to make the terms for other programs.
 
  send your comments to kono@ie.u-ryukyu.ac.jp
- $Id$
+ $Id: verilog.pl,v 1.1 2007/08/30 03:44:35 kono Exp $
 */
 
 :- dynamic st_variables/2.