# HG changeset patch # User Shinji KONO # Date 1461311233 -32400 # Node ID 29cf617f49dbf6c7a8c132a64bf4f70996812d05 # Parent 8fb7b6f55b7e88370c85a1c8882bc5d90732d865 newer CVS version diff -r 8fb7b6f55b7e -r 29cf617f49db bddcomp.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db bdditl.pl --- 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 % diff -r 8fb7b6f55b7e -r 29cf617f49db bdtstd.pl --- 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 % diff -r 8fb7b6f55b7e -r 29cf617f49db chop.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db diag.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db display.pl --- 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) diff -r 8fb7b6f55b7e -r 29cf617f49db dvcomp.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db ex.pl --- 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, diff -r 8fb7b6f55b7e -r 29cf617f49db exdev.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db infinite.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db itlstd.pl --- 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 diff -r 8fb7b6f55b7e -r 29cf617f49db kiss.pl --- 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. diff -r 8fb7b6f55b7e -r 29cf617f49db ndcomp.pl --- 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. diff -r 8fb7b6f55b7e -r 29cf617f49db problems --- 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) + + p = finite & p (on any finite, infinite) + [finite]p = ~(~finite & ~p) + []p = [](finite & p) = ~(true & ~(finite &p)) + + p = infinite & p = true (on infintie) + [infinite]p = ~(~infinite & ~p) + +p が、LTTLの<>pに相当するはず。いや、infinite /\ 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 diff -r 8fb7b6f55b7e -r 29cf617f49db rstd.pl --- 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 % diff -r 8fb7b6f55b7e -r 29cf617f49db verilog.pl --- 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.