Mercurial > hg > Applications > Lite

comparison problems @ 22:29cf617f49db default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
newer CVS version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 22 Apr 2016 16:47:13 +0900
parents e1d3145cff7a
children
comparison
equal deleted inserted replaced
21:8fb7b6f55b7e 22:29cf617f49db
1 Sat Jan 12 21:45:34 JST 2008
2
3 なんか、share は間違っているっぽいけど。
4
5 Sat Dec 1 11:08:27 JST 2007
6
7 finite interval だけど...
8 infinite =def (true & false )
9
10 finite をatomとして導入する。で、modelにfinite/infinite を入れる。
11 finite |- finite
12 finite |- ~infinite
13 infinite |- ~finite
14 |-/- infinite/\finite
15 |- infinite\/finite
16 finite \/ infinite |- p
17 finite /\ infinite |-\- p
18
19 finite |- @finite
20 finite |-/- @infinite
21 model のfinite/infiniteは、排他。
22
23 infinite がpositive occurence に一つあれば、式全体はinfinite。
24 finite がpositive occurence のみにあれば、式全体はinfinite。
25 正確ではないが、そんな感じ。
26
27 finite |-/- true & false
28 infinite |- true & false
29
30 である必要がある。(ふーん)
31 infinite |-/- finite & false
32 infinite |- infinite & false
33 finite |- finite & false
34 finite |-/- infinite & false
35
36 でも、これだと、[]<>(p) みたいなのは?
37
38 うーん、finite/infinite ではなくて、compact/open 見たいな感じだな。
39 まぁ、実際、そうだしね。
40 infinite |- fin(false)
41 だし。
42 infinite |- fin(p)から infinite |- []<>(p)
43
44 <finite>p = finite & p (on any finite, infinite)
45 [finite]p = ~(~finite & ~p)
46 []<finite>p = [](finite & p) = ~(true & ~(finite &p))
47
48 <infinite>p = infinite & p = true (on infintie)
49 [infinite]p = ~(~infinite & ~p)
50
51 <finite>p が、LTTLの<>pに相当するはず。いや、infinite /\ <finite>p
52 かな。
53
54 infinite |- [](finite & p)
55
56 自体が「pが無限回起きる」ってことを意味しているのでいいのかな。
57
58 これで出来るのかな? なんか、pathlogic な感じだが、こういう構文的な
59 もので finite/inifinite を区別できるものなの?
60
61
1 Sun Feb 10 21:30:04 JST 2002 62 Sun Feb 10 21:30:04 JST 2002
2 63
3 衣empty ϡɤ? kiss λϡ̵뤷... 64 あ、そうだよ。empty は、どうすんだ? kiss の時は、無視したんだが...
4 65
5 ⤽⡢2nd order 줿ǡʣˤʤꤹ 66 そもそも、2nd order を入れたおかげで、複雑になりすぎ。
6 67
7 ⤦ simple version ٤͡ 68 もう一度 simple なversion を作るべきだよね。
8 69
9 ѤǤǡ 70 状態生成を再利用できる形で。
10 71
11 о general abstraction 72 対称性 general abstraction
12 73
13 Thu Feb 7 12:12:21 JST 2002 74 Thu Feb 7 12:12:21 JST 2002
14 75
15 Verlog output for Prof. Fujita 76 Verlog output for Prof. Fujita
16 77
17 switch Ǥ⤤ɡäȵˤʤʤ? 78 switch でもいいんだけど、ちょっと巨大にならない?
18 79
19 module check001(clk,inputs..,outputs...) 80 module check001(clk,inputs..,outputs...)
20 input clk; 81 input clk;
21 input inputs; 82 input inputs;
22 output outputs; 83 output outputs;
32 end 93 end
33 endcase 94 endcase
34 end 95 end
35 endmodule 96 endmodule
36 97
37 äƤʴ? 98 ってな感じ?
38 99
39 äѤꡢ֤cubeΤ褦ʷΤϡɤʤ͡ 100 やっぱり、状態をcubeのような形で生成するのは、良くないよね。
40 ?(a,@a,@b) 101 ?(a,@a,@b)
41 ߤʷǡ䤹ޡϡJava Version 102 みたいな形で、生成した方が扱いやすい。ま、それは、Java Version
42 ǡ 103 で。
43 104
44 ɤ? BDD üƾ֤ˤ褦ˤ롣 105 特性方程式を生成する方が良い? BDD の末端が各状態にいくようにする。
45 ϡޤɤʤ... 106 それは、あんまり良くないか...
46 107
47 Sun Jan 21 00:42:39 JST 2001 108 Sun Jan 21 00:42:39 JST 2001
48 109
49 ? äѤꡢʤѤʡ 110 あれ? やっぱり、なんか変だな。
50 | ?- ex(finite & empty). 111 | ?- ex(finite & empty).
51 112
52 state(1 , not(true&false)&empty) 113 state(1 , not(true&false)&empty)
53 [][empty]->empty 114 [][empty]->empty
54 [][more]->1 115 [][more]->1
63 yes 124 yes
64 | ?- infinite. 125 | ?- infinite.
65 satisfiable in infinite interval: 126 satisfiable in infinite interval:
66 * 127 *
67 0: 1 128 0: 1
68 Ǥϡޤˡ 129 では、困ります。それに、
69 <>(p) = finite & p 130 <>(p) = finite & p
70 ˽񤭴ʤȤʤߤ͡ 131 に書き換えないといけないみたいね。
71 132
72 äƤȤϡϤꡢ 133 ってことは、やはり、
73 ξ֤顢ͣ졢more ˤȴ 134 その状態から、唯一、more にだけ抜ける状態
74 ʤΤʡ 135 なのかな。
75 136
76 Sat Jan 20 20:50:17 JST 2001 137 Sat Jan 20 20:50:17 JST 2001
77 138
78 true loopȤߤʤƤʤΤǡex(true) ǡinfinite 139 true をloopとみなしてないので、ex(true) で、infinite
79 satisfiable ˤʤʤ 140 が satisfiable にならない。
80 141
81 infinite ǡloop * 褦ˤ 142 infinite で、loop を * で明示するようにした。
82 143
83 Sat Jan 20 18:16:33 JST 2001 144 Sat Jan 20 18:16:33 JST 2001
84 145
85 Ȥꤢmore_only ϡmore ˤΤеȸȤ 146 とりあえず、more_only は、more にいくものが何かあれば許すと言うことに
86 ޤ 147 しました。
87 148
88 Sat Jan 20 03:38:14 JST 2001 149 Sat Jan 20 03:38:14 JST 2001
89 150
90 demo(15) infinite ߤޤʤloop detection η׻̤ 151 demo(15) の infinite が止まらない。loop detection の計算量が
91 ¿褦Ǥ͡ 152 多すぎるようですね。
92 153
93 ԤΤФƤƤȤȤȡrepeat fail loop 154 失敗したのを覚えておいてということだと、repeat fail loop
94 Dz󤹤櫓ˤϤޤ͡ 155 で回すわけにはいきませんね。
95 156
96 Sat Jan 20 02:33:17 JST 2001 157 Sat Jan 20 02:33:17 JST 2001
97 158
98 ˡmore_only(S) ȽǤƤޤäɤΤ? 159 本当に、more_only(S) で判断してしまって良いのか?
99 160
100 inifinite-> ⤢뤷... 161 inifinite-> の問題もあるし...
101 162
102 inifinite state sequence ǡITL satisfiy 163 ある特定のinifinite state sequence で、ITL式が satisfiy される
103 Ȥ -interval satisfiability äƸ󤸤ʤ? 164 ことを ω-interval satisfiability って言うんじゃないの?
104 165
105 Ȥȡ 166 だとすると、
106 ξ֤顢ͣ졢more ˤȴ 167 その状態から、唯一、more にだけ抜ける状態
107 ǤɤΤ? Ǥ⡢more/empty ǤʤʬषƤޤäƤΤǡ 168 であれば良いのか? でも、more/empty でいきなり分類してしまっているので、
108 ϡۤɴñȽǤǤʤʡITLϤ顢 169 それは、それほど簡単に判断できないかな。ITL式はあるんだから、
109 more դäŸɤΤ... 170 more を付け加えて展開すれば良いのだけど...
110 171
111 non-determistic empty ʪϡ~(<>empty) ˤʤʤΤ 172 non-determistic に empty に落ちる物は、~(<>empty) になり得ないので
112 ޤ 173 まずい。
113 174
114 13:+ac-bc-cc-dc 183 175 13:+ac-bc-cc-dc 183
115 14:-ac-bc-cc+dc 185 176 14:-ac-bc-cc+dc 185
116 15:-ac-bc-cc+dc 186 <---- 177 15:-ac-bc-cc+dc 186 <----
117 16:+ac-bc-cc-dc 187 178 16:+ac-bc-cc-dc 187
128 27:+ac-bc-cc-dc 218 189 27:+ac-bc-cc-dc 218
129 28:+ac-bc-cc-dc 221 190 28:+ac-bc-cc-dc 221
130 29:-ac+bc-cc-dc 226 191 29:-ac+bc-cc-dc 226
131 30:-ac-bc+cc-dc 186 192 30:-ac-bc+cc-dc 186
132 193
133 ! 194 おぉ!
134 195
135 Fri Jan 19 20:59:46 JST 2001 196 Fri Jan 19 20:59:46 JST 2001
136 197
137 | ?- ex((infinite -> @infinite)). 198 | ?- ex((infinite -> @infinite)).
138 199
149 210
150 yes 211 yes
151 | ?- infinite. 212 | ?- infinite.
152 unsatisfiable in infinite interval. 213 unsatisfiable in infinite interval.
153 214
154 ... ɤȤʤǤ礦? inifite ϴŪ 215 これは... どういうことなんでしょうね? inifite は基本的に
155 false 顢inifite-> פΤΤϡ٤ơinfinite unsatisfiable 216 false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable
156 ͡ 217 だね。
157 218
158 Fri Jan 19 20:40:37 JST 2001 219 Fri Jan 19 20:40:37 JST 2001
159 220
160 ȴñʥ르ꥺǡsatisfiabilityϡå 221 割りと簡単なアルゴリズムで、satisfiabilityは、チェック
161 Ǥޤ줬ɤ Moszkowski ˤ뤱... 222 できました。これが、正しいかどうかは Moszkowski によるけど...
162 inifnite 223 inifnite
163 *skip 224 *skip
164 *((skip&skip)) 225 *((skip&skip))
165 ʤɤ˴ؤƤϡޤư褦Ǥ͡ 226 などに関しては、うまく動くようですね。
166 227
167 vailidity checker ߤ... ɤΤvalidʤΤϡ 228 vailidity checker が欲しい所だけど... どういうものがvalidなのかは、
168 ɤ狼ʤ꤬ unsatisfiable ʤСvalid ʤ 229 良くわからない。もちろん、否定が unsatisfiable ならば、valid なの
169 230 だが。
170 231
171 Ǥ⡢ˡȡ 232 でも、この方法だと、
172 satisfiable in -interval implies 233 satisfiable in ω-interval implies
173 falsifiable in finite interval 234 falsifiable in finite interval
174 äƤȤˤʤ餷 235 ってことになるらしい。
175 236
176 Fri Jan 19 07:48:59 JST 2001 237 Fri Jan 19 07:48:59 JST 2001
177 238
178 Streett _i []<>L_i <>[]U _i 239 Streett ∩_i []<>L_i ⊃ <>[]U _i
179 Rabin ~(_i []<>L_i <>[]U _i) 240 Rabin ~(∩_i []<>L_i ⊃ <>[]U _i)
180 241
181 Ȥ¤äƤ롣ϡ 242 という構造を持っている。これは、
182 ̵²󷫤֤ L ϡĤä U ̤褦ˤʤ 243 ある無限回繰り返す所 L から先は、いつか、ずーっと U を通るようになる
183 ΤȡȤ¤ˤʤäƤ롣 244 のと、その否定という構造になっている。これを、
184 labeled tree Ρ꤫ϡäȡ֤ޡĤƤץ롼 245 labeled tree の、ある所から先は、ずーっと「あるマークがついている」ループ
185 ɽ 246 で表す。
186 247
187 ǡΥ르ꥺ... 248 で、そのアルゴリズムだけど...
188 249
189 depth first ˡֽи̵Ρɡפõޡ롣顢 250 depth first に「出口の無いノード」を探す。そこをマークする。そこから、
190 ΡɤФʤ顢и̵Ρɤ귫롣롼פФ褿鸡 251 ノードを覚えながら、出口の無いノードを手繰る。ループが出て来たら検出
191 λǸޤǤä顢ޡꡢνи̵Ρɤõ 252 完了。最後までいったら、マークに戻り、次の出口の無いノードを探す。
192 depth first search ޤǷ֤äơ׻̤ϡ 253 これをdepth first search が終るまで繰り返す。したがって、計算量は、
193 ΡɿN Фơǰ N^2/2 ( N+(N-1)+(N-2)...1 ) Ǥ롣ۤ 254 ノード数N に対して、最悪 N^2/2 ( N+(N-1)+(N-2)...1 ) である。それほど
194 ̵ 255 悪くは無いか。
195 256
196 Fri Jan 19 04:27:42 JST 2001 257 Fri Jan 19 04:27:42 JST 2001
197 258
198 ȡLICS paper ϡ䤿ʣפϡ-automaton 259 えーと、LICS のpaper は、やたら複雑だが、要は、ω-automatonの
199 ͡顢false loop detection ȡ 260 否定の問題だよね。だから、false loop detection が、ちゃんと、
200 ITL ˰פƤ뤳Ȥɤ 261 ITL の否定の定義に一致していることさえ見れば良い。
201 262
202 finite interval Ǥϡ˰פƤ櫓顢(true & false ) 263 finite interval では、既に一致しているわけだから、(true & false )
203 satisfiability̵ưפɬפ̵פʤС 264 のsatisfiabilityの定義を無理して一致させる必要は無い。一致しなければ、
204 ۤʤaxiomatiazation 򸫤ĤȤˤʤ롣顢false loop 265 異なるaxiomatiazation を見つけたことになる。だから、false loop
205 detection negetation consistent ʤС֤󡢰פ 266 detection が negetation consistent ならば、たぶん、一致するんだろう。
206 267
207 ɤϡRabin automatonacceptabilityå뤳Ȥˤʤ 268 結局は、Rabin automatonのacceptabilityをチェックすることになるんだろう。
208 äƤȤϡnon deterministic buchi automaton 򰷤äƤȤ 269 ってことは、non deterministic buchi automaton を扱うってことか。
209 270
210 Rabin <-> Streett complimentary 271 Rabin <-> Streett complimentary
211 272
212 (true & false)˴ؤƤϡ<>[](not_empty) ʡ 273 (true & false)に関しては、<>[](not_empty) だよな。
213 infinite -> <>[](more) 274 infinite -> <>[](more)
214 275
215 äƤȤ... äѤꡢfalse_loop detection Ǥ󤸤ʤʤ 276 ってことは... やっぱり、false_loop detection でいいんじゃないかなぁ。
216 277
217 ȡ 278 えーと、
218 ٤Ƥterminating loop ǡempty->true ʤ => infinite 279 すべてのterminating loop で、empty->true がない => infinite
219 顢ض֤ǽ­äƤΤϡ 280 だから、ω区間で充足ってのは、
220 terminating loop empty->trueʤΤ 281 terminating loop に empty->trueがないものがある
221 顢ض֤ǹäƤΤϡ 282 だから、ω区間で恒真ってのは、
222 terminating loop empty->trueʤ 283 terminating loop に empty->trueがない
223 284
224 Ȥʤ롣ȡtrue/false ž롣(Τ?) 285 となる。その否定を取ると、true/false が逆転する。(のか?)
225 286
226 terminating loop ǤʤƤ⡢ض֤¸뤳ȤϤǤ롣 287 しかし、terminating loop でなくても、ω区間を実現することはできる。
227 infinite & P -> infinite 288 infinite & P -> infinite
228 顣ξ⽼­äƤʡξϡɤ P 289 だから。この場合も充足っていうんだろうな。この場合は、どうせ P
229 ϡtableau ̵뤵Τ̵ 290 は、tableau で無視されるので問題無い。
230 291
231 äơȤϡterminating loop 򸫤Ф 292 って、ことは、terminating loop だけを見ればよろしい。
232 293
233 execution example ϡ 294 execution example は、
234 s s s s s s (s s s s s s)* 295 s s s s s s (s s s s s s)*
235 Ȥ롣ʤΤǡɬǾǥġ 296 という形を取る。なので、必ず最小モデルの性質を持つ。
236 ºݤˤϡ* ϡŪɤ 297 実際には、* の中は、非決定的で良い。
237 298
238 299
239 Fri Jan 19 02:18:39 JST 2001 300 Fri Jan 19 02:18:39 JST 2001
240 301
241 <>empty infinite = (true & false ) ϡξΩʤ 302 <>empty と infinite = (true & false ) は、両立しない。
242 <>empty = finite & empty = ~(true & false) & empty 303 <>empty = finite & empty = ~(true & false) & empty
243 304
244 ~(true & false ) Ϥʤˤ򼨤Ƥ뤫ȸ... 305 ~(true & false ) はなにを示しているかと言うと...
245 ĤǤֽפȤȡinfinite ϡֽʤ 306 いつでも「終れる」ということ。infinite は、「終れない」
246 307
247 ض֤ˤϡempty exit ¸ߤǤʤΤˤϡ 308 ω区間には、empty exit は存在できない。正確には、
248 ... [ no-empty loop ] .... 309 ... [ no-empty loop ] ....
249 Ȥȡsub ֤ɤ 310 ということ。そういうsub 区間があれば良い。
250 311
251 [](more) ? 󡢤ϡLite Ǥϡfalse. 312 [](more) は? もちろん、これは、Lite では、false.
252 ~(finite & ~more) 313 ~(finite & ~more)
253 ~(~(true & false) & ~more)) 314 ~(~(true & false) & ~more))
254 ~(~(true & false) & empty)) 315 ~(~(true & false) & empty))
255 줬 ض֤ true ˤʤ뤿ˤ... 316 これが ω区間で true になるためには...
256 317
257 []inifinite version? 318 []のinifinite versionは?
258 319
259 http://research.commpaq.com/SRC/esc/ 320 http://research.commpaq.com/SRC/esc/
260 321
261 Fri Jan 19 01:20:54 JST 2001 322 Fri Jan 19 01:20:54 JST 2001
262 323
263 ض֤ϡɬ(s_n...s_m)* ޤࡣdecidableʤС 324 ω区間は、必ず、(s_n...s_m)* を含む。decidableならば、そうだ。
264 ϡɬפɡ 325 が、それは、証明が必要がだけど。
265 326
266 դˡ(s_n...s_m)* ޤС򤺡äȷ֤Ȥˤꡢ 327 逆に、(s_n...s_m)* を含めば、そこをずーっと繰り返すことにより、
267 ض֤Ǥ롣顢롼פ򸫤ĤС 328 ω区間を実装できる。だから、そういうループを見つければ、
268 ض־ satisfiable ȤȤǤ롣 329 ω区間上で satisfiable だということができる。
269 330
270 ζ־ǡempty Τ褦exitΤ? ֤ 331 その区間上で、∨empty のようなexitが許されるのか? たぶん、
271 ʤȤȤϡϤꡢfalse loop 򸫤Ĥ 332 許されない。ということは、やはり、false loop を見つければ
272 ɤȸȤ 333 良いと言うことか。
273 334
274 Υ르ꥺ? 335 そのアルゴリズムは?
275 336
276 ض֤Ǥϡempty ȴФ뤳ȤǤʤ-> 337 ω区間では、empty で抜け出ることができない。->
277 <>empty false 338 <>empty がfalse
278 ɤʡ 339 どうも正しそうだな。
279 340
280 ȡʥ르ꥺबꤽ... 341 えーと、何か、安全なアルゴリズムがありそうだけど...
281 ñʤΤϡ٤ƤΥ롼פdepth first õȤʡ 342 簡単なのは、すべてのループをdepth first で探すことだな。
282 343
283 Ȥȡfinitarity åΤϷ빽ݤˤʤ롣 344 とすると、finitarity をチェックするのは結構面倒になる。
284 345
285 finitarity ȤϤʤ? 346 finitarity とはなに?
286 롼פˤɬtrue exit 347 ループには必ずtrue exitがある
287 infiniteness Ȥϡ 348 infiniteness とは、
288 exit Τʤ롼פ 349 exit のないループがある
289 350
290 []<>(p) = <>[](p) ϡɤʤ? 351 []<>(p) = <>[](p) は、どうなるんだろう?
291 <>(p) = finite & p 352 <>(p) = finite & p
292 ~(finite & ~(finite & p)) = finite & ~(finite & ~p) 353 ~(finite & ~(finite & p)) = finite & ~(finite & ~p)
293 Ǥ 354 ですか。
294 355
295 356
296 Fri Jan 19 00:33:43 JST 2001 357 Fri Jan 19 00:33:43 JST 2001
297 358
298 ȡ 359 えーと、
299 [](false) 360 [](false)
300 satisfiableˤʤ뤳ȤϤʤ 361 がsatisfiableになることはない。
301 ~(true & ~ false) 362 ~(true & ~ false)
302 ~(true & true) 363 ~(true & true)
303 顣 364 だから。
304 true & ~true 365 true & ~true
305 ϡ롣 366 は、許される。しかし、
306 ~true & ~true 367 ~true & ~true
307 ϵʤ켫Τϡverifier Ǥ⡢ʤ롣 368 は許されない。これ自体は、今のverifier でも、そうなる。
308 369
309 tableau expansion ΤƱȹͤɤΤ? 370 tableau expansion 自体は同じだと考えて良いのか?
310 ä˰ۤʤ inference rule 櫓ǤϤʤ餷 371 特に異なる inference rule があるわけではないらしい。
311 372
312 ȤСɬפʥɤϡfalse loop detector ? 373 だとすれば、必要なコードは、false loop detector だけか?
313 exe/diag ˡinfinite_exe,infinite_diag Τ 374 exe/diag の代りに、infinite_exe,infinite_diag を作るのだろうか。
314 375
315 infinite_exe ϡ롼פɽʤФʤʤɬ 376 infinite_exe は、ループを表示しなければならない。必ず、
316 Τ褦ʥ롼פ¸ߤΤ? Ȥȡinfinite 377 そのようなループが存在するのだろうか? とすると、infinite
317 interval ϡprefix Τ褦ʤΤˤʤ롣¤ϡprefix 378 interval は、prefix のようなものになる。実は、prefix
318 infinite interval Τ? prefix(finite,....) 379 がinfinite interval そのもの? prefix(finite,....)
319 ߤʤΤ͡ϡɤäǸȤ... 380 みたいなものだね。これは、どっかで見たことが...
320 381
321 382
322 Thu Jan 18 22:42:24 JST 2001 383 Thu Jan 18 22:42:24 JST 2001
323 384
324 | ?- ex(((true&false)->(<>(empty)))). 385 | ?- ex(((true&false)->(<>(empty)))).
325 386
326 ϡvalid ˤʤäƤޤºݤˤϡinfinite->not(<>(empty)). 387 は、valid になってしまう。実際には、infinite->not(<>(empty)).
327 388
328 Thu Jan 18 21:04:13 JST 2001 389 Thu Jan 18 21:04:13 JST 2001
329 390
330 ޤchop.pl ΡX & false falseѴƤΤ 391 まず、chop.pl の中の、X & false をfalseに変換しているのを
331 ȴɬפ롣 392 抜く必要がある。
332 393
333 Thu Jan 18 19:59:33 JST 2001 394 Thu Jan 18 19:59:33 JST 2001
334 395
335 in POPL01 396 in POPL01
336 397
337 LICS00 infinite 褦 Lite ĥ뤳Ȥ 398 LICS00 の infinite を入れるように Lite を拡張することが
338 ǤΤ? 399 できるのか?
339 400
340 ñʳĥˤϤʤʤ 401 単純な拡張にはならない。
341 infinite =def (true & false ) 402 infinite =def (true & false )
342 顣ϡμǤ unsatisfiable 403 だから。これは、今の実装では unsatisfiable。
343 404
344 P&Q ǡQ ñfalseȤäơʤϡnode ϡ 405 P&Q で、Q が単純にfalseだからといって、諦められない。今は、node は、
345 empty,false 406 empty,false
346 empty,true 407 empty,true
347 more,false 408 more,false
348 more,some_other 409 more,some_other
349 Ȥ褦ħդƤ롣­Τ? 410 というように特徴付けられている。これで足りるのか?
350 411
351 Eventurality check ɬ̵ɤɡ 412 Eventurality check が必要無いと良いんだけど。
352 413
353 Rabin automaton äƤʤ? Buchi Ʊʤ󤸤ʤ? 414 Rabin automaton ってなんだ? Buchi と同じなんじゃないの?
354 415
355 true & false ϡ 416 true & false は、
356 empy -> false 417 empy -> false
357 more -> true & false 418 more -> true & false
358 Ÿ롣ϡempty 򸫤ơvalidity/satisfiability 419 に展開される。今は、empty だけを見て、validity/satisfiability を
359 Ĵ٤Ƥ롣 420 調べている。しかし、これを、
360 ֤false exit 롼פsatisfiableȤߤʤ 421 「ある特定のfalse exit ループをsatisfiableだとみなす」
361 Ȥˤꡢinfinite interval Ƴ뤳ȤǤ롣 422 ことにより、infinite interval を導入することができる。
362 423
363 ϡɤΤ褦 false exit 롼פ satisfiable Ȥ 424 問題は、どのような false exit ループが satisfiable だという
364 ? Ȥϡ unsatisfiable ˤʤ formulaä 425 こと? というよりは、これで unsatisfiable になる formulaって
365 ? 426 何?
366 more -> false 427 more -> false
367 Τ? 428 のたぐいだけか?
368 finite 429 finite
369 empy -> true 430 empy -> true
370 more -> true & true 431 more -> true & true
371 ϡɤʤ? 432 は、どうなる?
372 ~infinite 433 ~infinite
373 empy -> true 434 empy -> true
374 more -> ~(true & false) 435 more -> ~(true & false)
375 Ȥʤ롣ʤΤǡ finite 436 となる。なので、これは finite に等しい。
376 437
377 infinite ϡfalse loop ɽƤȹͤ롣 438 infinite は、false loop を表していると考える。
378 439
379 ƤμPfinite -> P ǡåСfinite LITL ˤʤ롣 440 全ての式Pを、finite -> P で、チェックすれば、finite LITL になる。
380 (ʤʤФʤ) 441 (ならなければいけない)
381 442
382 äơȤϡfalse loop detectɤ? ϡ 443 って、ことは、false loop をdetectすれば良いだけか? これは、
383 빽פ׻ŪˤϡäѤʡ 444 結構易しいが、計算量的には、ちょっと大変かな。
384 finitely 445 finitely
385 valid, satisfiable, unsatisfiable... 446 valid, satisfiable, unsatisfiable...
386 inifinitly 447 inifinitly
387 valid, satisfiable... 448 valid, satisfiable...
388 infinitely satisfiable Ȥϡ 449 infinitely satisfiable とは、
389 flase loop ¸ߤ뤳 450 flase loop が存在すること
390 valid ϡ 451 valid は、
391 false loop ʳϡempty false Ǥ뤳(?) 452 false loop 以外は、empty false であること(?)
392 453
393 ȡȡinifinitly satisiable ʼϡfinitly unsatisfiable 454 えーと、それだと、inifinitly satisiable な式は、finitly unsatisfiable
394 ɡǤ? Ȥȡvalid ʼϤʤʤäƤޤ͡ 455 だけど、それでいいの? だとすると、valid な式はなくなってしまうね。
395 456
396 ϡäȤ줷ʤǤȤȤϡ 457 これは、ちょっとうれしくないであろう。ということは、
397 infinitely valid ϡ 458 infinitely valid は、
398 false loop ʳϡempty ture Ǥ뤳(?) 459 false loop 以外は、empty ture であること(?)
399 ޤȹͤΤȤȡ 460 を含むと考えるのが正しい。だとすると、
400 |= finitie /\ finite 461 |= finitie /\ finite
401 äƤȤˤʤ͡ϡäȤ줷ʤ 462 ってことになるね。それは、ちょっとうれしくないか。
402 463
403 ࡢMoszkowski ϡɤ򤷤? 464 うーむ、Moszkowski は、どういう選択をしたんだろう?
404 465
405 466
406 Wed Nov 22 16:27:45 JST 1995 467 Wed Nov 22 16:27:45 JST 1995
407 468
408 rstd ¦ limit 򰷤Ȥˤ롣 469 rstd 側で limit を扱うことにする。
409 rename_list limitꤹ뤳Ȥˤʤ롣singleton limit 470 rename_list でlimitを指定することになる。singleton のlimit
410 ϤʤȤʤover(r,N)ˤǤʤΤ 471 をはずさないといけないだろう。over(r,N)が外にでないのが
411 äȾ­ʡ 472 ちょっと情報不足だな。
412 473
413 itlstd idempotent ˤʤäƤʡ!!! 474 itlstd が idempotent になってなーい!!! しくしく。
414 itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) Y=Y1ˤʤ 475 itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) でY=Y1になる
415 ϤʤΤ... 476 はずなのだが...
416 477
417 itlstd2 Ǥϡsingleton remove, renaming ϹԤʤʤǡlimit over 478 itlstd2 では、singleton remove, renaming は行なわないで、limit over
418 갷ˤädetailed trace ǽȤʤ롣ˡ 479 だけを取り扱う。これによってdetailed trace が可能となる。これに、
419 itlstd򤫤СȤϤɤ⼺ԤƤ 480 従来のitlstdをかければ、もとに戻るはずだ。が、どうも失敗している
420 餷 481 らしい。
421 482
422 Tue Nov 21 18:33:19 JST 1995 483 Tue Nov 21 18:33:19 JST 1995
423 484
424 renaming trace original limit ǹԤʤ 485 renaming の trace は original limit で行なう。
425 detailed trace no limit ǹԤʤ 486 detailed trace は no limit で行なう。
426 itl/5 2ٸƤФ뤬ޤɤȤ뤫 487 itl/5 は2度呼ばれるが、まあ、良とするか。
427 488
428 rstd ¦limit֤򤹤Ф֤ޤʤ... 489 rstd 側でlimitの置き換えをすればだいぶましなんだが...
429 490
430 renmaing ǡover limit 갷Ū 491 renmaing で、over limit を取り扱う方が統一的か。
431 492
432 Wed Nov 15 12:58:28 JST 1995 493 Wed Nov 15 12:58:28 JST 1995
433 494
434 over(r,N) true/false ֤äƤơunify뤫? 495 over(r,N) が true/false に置き換わっていて、unifyするか?
435 496
436 ˤ衢äȵޤɤѿ֤뤫ϡ 497 いずれにせよ、ちょっと気まずい。どの変数が置き換わるかは、
437 renaming trace ʬ뤬... 498 renaming を trace すれば分かるが...
438 499
439 ֤rstd¦ǹԤʤäơoriginal/restrictedξ 500 この置き換えをrstd側で行なって、original/restrictedの両方を
440 ȤäƤơɤѿ֤äʬ褦ˤ롣 501 とっておく。そして、どの変数が置き換わったか分かるようにする。
441 (renaming informationƤ) Ǥ⡢ξɤ 502 (renaming informationに入れておく) でも、この情報もどうせ
442 lazy? ʤѤ 503 lazyに生成するんだよね? なんか変だ。
443 504
444 뤤ϡdetailed traceǤִʤ? true/false 505 あるいは、detailed traceの方では置換えしない? true/false に
445 ֤ƤƱstateǼ¸ǤϤunify Ϥʤ 506 置き換えても同じstateで実現できるはず。だが、unify はしないと
446 ʤ 507 いけない。
447 508
448 ˤ衢lazy state generation Ǥϡ 509 いずれにせよ、lazy state generation では、
449 full trace, restricted trace 510 full trace, restricted trace
450 ξ򤪤ʤΤˤϡover ֤rstd ǹԤʤä 511 の両方をおこなう。このためには、over の置き換えをrstd で行なった
451 ɤ 512 方が良いだろう。
452 513
453 ࡢǤ⡢ȡitlstd non-deterministic ˤʤä 514 うーむ、でも、そうすると、itlstd がnon-deterministic になって
454 ޤϡޤ 515 しまう。それは、いまいちだ。
455 516
456 Tue Nov 14 19:56:26 JST 1995 517 Tue Nov 14 19:56:26 JST 1995
457 518
458 Detailed trace λ Fromula state number ξ⤫ʤ 519 Detailed trace の時は Fromula と state number と両方持ち歩かないと
459 520 だめだ。
460 521
461 ȤȤϡdiag routine ľʤȥᤫndcomp 522 ということは、diag routine を書き直さないとダメか。ndcomp は
462 뤫? 523 あきらめるか?
463 524
464 Mon Nov 13 22:33:34 JST 1995 525 Mon Nov 13 22:33:34 JST 1995
465 526
466 trace Ȥrenaming ϡʤ󤸤ʤ? 527 trace するときにrenaming は、いらないんじゃない?
467 detailed traceɤȤȤ... С 528 detailed traceをどうせ使うとすれば... そうすれば、
468 choice ͤʤƤɤ 529 choice も考えなくても良い。
469 530
470 Sun Nov 12 23:37:36 JST 1995 531 Sun Nov 12 23:37:36 JST 1995
471 532
472 ^r trace 533 ^r のtrace
473 534
474 stateϷޤäƤ 535 stateは決まっている
475 duplicated rename inforamtion Ȥätrace Ǥ롣 536 duplicated は rename inforamtion を使ってtrace できる。
476 537
477 detailed expansion ơunify 롣Ūˤϡ 538 detailed expansion して、unify する。具体的には、
478 BDDˤäʬ򤹤롣ˤäơtrue_false r^n 539 BDDにそって分解する。これによって、true_false がr^nの
479 treeŸϤʤС̤ΤΤõ 540 treeに展開されるはず。されなければ、別のものを探す。
480 541
481 true_falsechoiceˤäͤۤʤ櫓...? 542 true_falseのchoiceによって値が異なるわけだけど...?
482 choice ϡĤBDD˴ؤưĤǤʤ(leafˤʤ 543 choice は、一つのBDDに関して一つしかでない。(leafにしかない
483 ) ȤȤϡʣchoice ϡ 544 から) ということは、複数のchoice は、
484 ۤʤ & empty 545 異なる & の empty
485 Ǥʤʤ餫identityĤɡ 546 でしか起きない。なんらかのidentityを残した方がいいんだけど。
486 ޡŪƱstateˤäơ٤Ƥξ郎Ԥʤ顢 547 ま、結果的に同じstateにいって、すべての条件が尽くされるなら、
487 ʤdetailed expansion Ϥ٤ƤޤǤΤ顢 548 構わないか。detailed expansion はすべてを含んでいるのだから、
488 ʤϤ 549 構わないはず。
489 550
490 ޤϡrenaming ΥĤ褦 551 まずは、renaming のカタをつけよう。
491 552
492 äŪ^rȥ졼ɤʤ? singleton ^r 553 もっと選択的に^rをトレースした方が良くない? singleton ^r
493 ʤ餫term˥ޥåפǤʤΤ? 554 をなんらかのtermにマップできなものか?
494 555
495 Sat Nov 11 09:55:41 JST 1995 556 Sat Nov 11 09:55:41 JST 1995
496 557
497 2path singleton removal 褦äȤǤ 558 2path singleton removal がようやっとできた。
498 ɤ⡢order sensitive ʤʡover @<,@> 559 ただし、どうも、order sensitive なんだよな。over が@<,@>に
499 äƤǤȤǤʤ롣 560 よってでる時とでない時がある。
500 561
501 sbdt_split, sbdt_ife ˤäremoval/renameˤorderʤ 562 sbdt_split, sbdt_ife によってremoval/renameによるorderを修正しない
502 Ȥʤä򤨤ʤȤ? 563 といけなかった。やむをえないところか?
503 564
504 singleton removal񤤤顢ȤɤʤäƤޤä 565 しかしsingleton removalを書いたら、もとの方も良くなってしまった。
505 ɤ⡢bdt routineˤ꤬äߤtrue & true 566 どうも、bdt routineには問題があったみたい。true & true を除く
506 褦ˤΤȤפʤ.... sbdt_opt Τ? 567 ようにしたのが効いたとも思えないんだが.... sbdt_opt のせいか?
507 568
508 state numberǤʤʤbugľ 569 state numberがでなくなるbugを直した
509 570
510 Ȥϡtrace ʡr^nμ¹Ԥȥȥ졼Ǥ 571 あとは、trace の問題だな。r^nの実行がちゃんとトレースできると
511 ɡ 572 いいんだけど。
512 573
513 Thu Nov 9 12:03:32 JST 1995 574 Thu Nov 9 12:03:32 JST 1995
514 575
515 P & Q sb(P_BDD & Q_BDD) ȤǻäƤ뤱.. 576 P & Q を、sb(P_BDD & Q_BDD) という形で持っているけど..
516 sb(P_BDD,PN) 577 sb(P_BDD,PN)
517 sb(Q_BDD,QN) 578 sb(Q_BDD,QN)
518 PN & QN Ȥɤʤ? ۤȤƱȤϻפ.... 579 PN & QN という方が良くない? ほとんど同じだとは思うけど....
519 ?(PN & QN,true,false) ȤʤΤ.... 580 ?(PN & QN,true,false) となるのか.... うーん。
520 581
521 QŸޤʤ? ? ̤ŸΥޡ 582 Qの展開を一回に抑えられない? ? を未展開のマークに
522 Ȥʤ? 583 使えないか?
523 584
524 Wed Nov 8 20:31:23 JST 1995 585 Wed Nov 8 20:31:23 JST 1995
525 586
526 ϤöBDD2pathǽ뤳ȤȤ롣 587 はやり一旦BDDに落して2pathで処理することとする。
527 588
528 first path: singleton varble detect 589 first path: singleton varble の detect
529 (regular variableʤϡΤޤstd_check 590 (regular variableがない場合は、そのままstd_check
530 singleton removal Ǿä뤳ȤϤʤ) 591 singleton removal で消えることはない)
531 regular variable ̵Сǽλ 592 regular variable が無ければ、これで終了
532 rename list ׻ 593 rename list を計算
533 second path path: 594 second path path:
534 singleton variable ä硢 595 singleton variable があった場合、
535 t/ftree parallel traverse 596 t/fのtree を parallel traverse
536 t/f ޤϡ[tf]/tf ȹ礻tf֤ 597 t/f または、[tf]/tf の組合せをtfに置き換える
537 ʣsingleton variableƱ˽ɤ 598 複数のsingleton variableを順不同に処理して良い
538 599
539 regular variable 뤫ɤϡsingleton removval 600 regular variable があるかどうかは、singleton removval の
540 ̤˰¸Τǡ1path Ǹ̩˼ȤϤǤʤ 601 結果に依存するので、1path で厳密に取り除くことはできない。
541 2nd path Ǥϳμ¤˼Ȥ롣 602 が、2nd path では確実に取り除くことが出来る。
542 603
543 ֤֡2nd path㤦!! sbdt ȶѤϤǤʤ 604 ぶぶ、2nd pathは全然処理が違う!! sbdt と共用はできない
544 605
545 Tue Nov 7 15:45:07 JST 1995 606 Tue Nov 7 15:45:07 JST 1995
546 607
547 chop Υ٥ʬСޤɤϡΤȡȡ 608 chop のレベルで分ければ、まあ、良い。問題は、そのあと。と、
548 ͤȡBDDѴ٥б˾ޤΤʤ 609 考えると、BDDに変換するレベルで対応する方が望ましいかも知れない。
549 󡢺ΤޤޤǤsafeʤɡƤΤ¿ 610 もちろん、今のままでもsafeなんだけど、落ちているものが多い。
550 ϷŪ˾֤䤷Ƥ뤳Ȥˤʤ롣 611 それは結果的に状態を増やしていることになる。
551 612
552 Ĥˡϡ 613 一つの方法は、
553 p(^r) => ?(^r,pt,pf) 614 p(^r) => ?(^r,pt,pf)
554 Ȥ롣 615 とする。
555 (pt,pf; tf), (pt;pf) 616 (pt,pf; tf), (pt;pf)
556 ѷ롣ȡʶ硣ϽŤʤ 617 と変形する。と、こんな具合。これは重いなぁ。
557 618
558 (~ ^r), ^r ܥȥॢåפǤfˤʤʤޡȤʤʡ 619 (~ ^r), ^r がボトムアップではfにならない。ま、そういうことなんだよな。
559 620
560 Tue Nov 7 10:38:59 JST 1995 621 Tue Nov 7 10:38:59 JST 1995
561 622
562 ɤ⡢singleton removal ȡ[a](^r = length(2)), f(^r) 623 どうも、singleton removal だと、[a](^r = length(2)), f(^r)
563 Τ褦ʤΤϴ˥ȥ졼Ǥ餷 624 のようなものは完璧にトレースできるらしい。
564 [a](^r = length(2)), *(^r) Ok ä 625 [a](^r = length(2)), *(^r) もOk だった。
565 626
566 Ǥ⡢ʸˡҤȯ롣 627 でも、さすがに文法記述は発散する。
567 628
568 ɡɤ¤ʤΤʤ? diag ˡfull trace Ǥɤ 629 結局、どういう制限なのかなぁ? diag 時に、full trace できたかどうかを
569 å뤫... 630 チェックするか...
570 631
571 ɤ⡢󥰥ȥåŤʡäȡȥå 632 どうも、シングルトンチェックが甘いな。もっと、ちゃんとチェックする
572 ˤ? 633 ためには?
573 634
574 Mon Nov 6 15:57:46 JST 1995 635 Mon Nov 6 15:57:46 JST 1995
575 636
576 [p_0,p_1,...,p_n] ϡ 637 [p_0,p_1,...,p_n] は、
577 p_0,p_1,...,p_n -> true 638 p_0,p_1,...,p_n -> true
578 ~ p_0,~ p_1,...,~ p_n -> false 639 ~ p_0,~ p_1,...,~ p_n -> false
579 else -> true_false 640 else -> true_false
580 ȤBDD(MTBDD)ˤʤ롣3 641 という形でBDD(MTBDD)になる。3値論理
581 642
582 ^r -> true_false 643 ^r -> true_false
583 644
584 true_false -> empty? choice ? true : fals 645 true_false -> empty? choice ? true : fals
585 : true_false 646 : true_false
589 tt;tf -> tf 650 tt;tf -> tf
590 f,tf -> f 651 f,tf -> f
591 f;tf -> tf 652 f;tf -> tf
592 tt,tf -> tf 653 tt,tf -> tf
593 654
594 (졢cross term?) 655 (あれ、cross termは?)
595 ΤˤǤޤޤϤ* ^r ⴰ 656 確かにこれでうまくいきます。はい。* ^r も完璧。
596 657
597 ϡ¹ԤtraceǤ뤫ɤʡ 658 問題は、実行をtraceできるかどうかだな。
598 659
599 Mon Nov 6 08:50:01 JST 1995 660 Mon Nov 6 08:50:01 JST 1995
600 661
601 singleton θ̤ͭ¤? 662 singleton の効果は有限か?
602 663
603 BDDsingleton duplicate ȤȡϻߤޤΤ? 664 BDDの中でsingleton duplicate を許すとすると、これは止まるのか?
604 selection(uniq set of subterm) 665 selection(uniq set of subterm)
605 ȤˤʤϤ顢ȤޤϤsubtermͭ¡singleton ˤϡ 666 という形になるはず。だから、とまるはず。subtermは有限。singleton には、
606 R̾ˤ̤ɬ̵ 667 R名による区別さえ必要無い。
607 ^r -> ^([false,true]) 668 ^r -> ^([false,true])
608 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n]) 669 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
609 ȤŸˤʤ? sortɬס 670 という展開になる? 再sortは必要。
610 671
611 Ūˡ^(r,[p_0,p_1...p_n]) ȤǼ«ʤ? r Ĥä... 672 一般的に、^(r,[p_0,p_1...p_n]) という形で収束しないの? r が一つだったら...
612 ͥȤoutǤnestϤäƤ顣 673 ネストしたらout。でもnestはあっても固定だから。
613 674
614 computationȥ졼ǤΤ? 䡢̤Ÿɬס 675 が、これでcomputationをトレースできるのか? いや、特別な展開が必要。
615 676
616 ȡdeterminization ʤȤ͡(ɤä?) 677 あと、determinization しないとね。(どうやって?)
617 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n]) 678 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
618 κݤˡpx_0 ˤ next Τߤ롣ɤ 679 の際に、px_0 には next のみが入る。そうすれば良い。
619 itl(p_0,more,..) 680 itl(p_0,more,..)
620 ǤνϤnext,true,falseOk 681 での出力はnext,true,false。Ok。
621 682
622 Sun Nov 5 21:34:33 JST 1995 683 Sun Nov 5 21:34:33 JST 1995
623 684
624 ʤ * ^R 礭ʾ֤롣 685 しかし、なんと * ^R は非常に大きな状態を生成する。
625 ^R true & ^R δĤ礭ʾ֤Ƥޤ(餷) 686 ^R と true & ^R の干渉が大きな状態を生成してしまう。(らしい)
626 ޤˤ? Ĥlength Ƭޤ뤳Ȥʡ 687 これを抑えるには? 一つはlength で頭を抑えることだな。
627 Ǥ⡢äѤ礭ޤꡢޤʤ 688 ああ、でも、やっぱり大きいか。あんまり、うまくない。
628 length(10) Ǥ빽礫.. 689 length(10) でも結構巨大か..
629 690
630 proj ǤƱ褦ϤäΤ... 691 proj でも同じような問題はあったのだけど...
631 692
632 ^r permuation о򲿤Ȥʤ¤͡ 693 ^r の permuation の対称性を何とかしない限りだめだね。
633 ѤʤǤ礦? ࡣ 694 しかし、順序は変えちゃダメなんでしょう? うーむ。
634 Ǥ⤵ǥ뼫ȤϾ.... ࡣ 695 でもさ、モデル自身は小さいんだが.... うーむ。
635 696
636 䡢ξ singleton removal ߤ 697 いや、この場合は singleton removal が効くみたい。そうか。
637 698
638 singleton νʤ餸ʤ? 699 これはsingleton の処理が正しくないからじゃない?
639 700
640 singleton θ̤ͭ¤? 701 singleton の効果は有限か?
641 f(r^1,....r^n) -> exists 702 f(r^1,....r^n) -> exists
642 Ȥͭ¡ɡꤷƤϤᡣ 703 だとすれば有限。だけど、固定してはだめ。
643 r^s ? length(1) : r^s ? length(2) : .... 704 r^s ? length(1) : r^s ? length(2) : ....
644 Ȥʤꤦ? 705 となりうる?
645 706
646 Wed Nov 1 21:12:04 JST 1995 707 Wed Nov 1 21:12:04 JST 1995
647 708
648 ͡... <>^R ȤʤȤʤ.... 709 例題ねー... しかし、<>^R が使えないとなると....
649 Ǥ⡢* ^R ϻȤ롣 710 あ、でも、* ^R は使える。
650 711
651 Mon Oct 16 16:05:31 JST 1995 712 Mon Oct 16 16:05:31 JST 1995
652 713
653 LITL ǡclosure, proj ȴpolynominal orderˡ!? 714 LITL で、closure, proj 抜きだとpolynominal orderの方法がある!?
654 ~(....&....(...&... ~(...&....))) 715 ~(....&....(...&... ~(...&....)))
655 Ȥǡvariable patternǤɤ 716 という形で、これにvariable patternを埋め込んでいけば良い。これだと
656 marking state space database Ϥʤ 717 marking だから state space database はいらない。
657 718
658 tableau expansion Ǥ⡢֤ƱŪpolynominal 719 tableau expansion でも、生成される状態は同じ数だから結果的にpolynominal
659 ˤʤäƤΤ.... ˡquantifier, closure, proj 720 になっていたのかも.... たしかに、quantifier, closure, proj を入れると
660 verification 񤷤ʤäƤ 721 verification は難しくなっていた。
661 722
662 䡢Ǥ⡢empty interval ȡ⤤ʤ? 723 いや、でも、empty interval があると、そうもいかないか?
663 ~(....&....(...&... ~(...&....))) 724 ~(....&....(...&... ~(...&....)))
664 Ǥդchopand,emptyѤ롣 exponential 725 の任意のchopをand,emptyに変える操作がいる。これは exponential。
665 p & p & p & p & p 726 p & p & p & p & p
666 p & p & p & p,empty , p 727 p & p & p & p,empty , p
667 chomp (non-empty interval chop) ä顢ס 728 chomp (non-empty interval chop) だったら、大丈夫。
668 729
669 Ǥ⡢closure, proj 򤤤ʤ餪ʤ 730 でも、closure, proj をいれるならおんなじか。
670 731
671 Mon Oct 9 19:51:27 BST 1995 732 Mon Oct 9 19:51:27 BST 1995
672 733
673 proj Ǥϡr^n n ز롣r^0 ϡ٤ƤγؤǶͭ롣 734 proj では、r^n の n を階層化する。r^0 は、すべての階層で共有される。
674 ¾length϶ͭʤȤߤΤΤlength(1) proj Q 735 他のlengthは共有されないとみるのが正しいのだろう。length(1) proj Q
675 ȡr^1^1 = r^0^1 ? 736 だと、r^1^1 = r^0^1 だよね?
676 737
677 P proj Q ǡQ part next part ϡ 738 P proj Q で、Q part のnext part は、
678 proj encupsulated ƤΤǡterm ϤɬפϤʤ 739 proj の中にencupsulated されているので、term はいじる必要はない。が、
679 condition Ϥɬפ롣renaming original clock 740 condition はいじる必要がある。ただし、renaming を original clock
680 level Ʊˤ limit ʣ 741 level と同じにすると limit が効きすぎるだろう。しかし、ここを複雑に
681 Τϡɤʤterm level ⳬزСϤʤ 742 するのは、どうかなぁ。term level も階層化すれば、問題はない。
682 (r^n)^n Ȥ... 743 (r^n)^n とか...
683 744
684 ɡsingleton removal ϡޤʤ͡줬ޤС 745 結局、singleton removal は、うまくいかないね。これがうまくいけば、だい
685 ϰϤޤΤ.... ơeventuality Ʊ餤ޤǤˤǤ 746 ぶ範囲が広まるのだが.... せめて、eventuality と同じぐらいまでにできな
686 ? r^s marking ȸФ櫓͡빽 747 いの? あ、そうか、r^s をmarking と見ればいいわけね。しかし、結構、めん
687 ɤȤФɤ 748 どくさいといえばめんどくさい。
688 749
689 Time constant regular variable 750 Time constant regular variable
690 751
691 renaming ʤʤСȼ 752 renaming なしならば、割と自明。
692 r^0 ... r^limit 753 r^0 ... r^limit
693 unifyɤrenaming ȡ⤦ʣˤʤ롣r^n state 754 をunifyすれば良い。renaming ありだと、もう少し複雑になる。r^n を state
694 ȸΤñˤ衢ʤ¤줿͡ 755 と見るのが簡単。いずれにせよ、かなり制限された感じだね。
695 756
696 renaming Ρäȵʹalgorithm... 757 renaming の、もっと気の聞いたalgorithmがあれば...
697 758
698 Mon Oct 9 05:48:38 BST 1995 759 Mon Oct 9 05:48:38 BST 1995
699 760
700 ^r -> true/false Ǥϡ[a](^r=length(2)) unsatisfiable. 761 ^r -> true/false では、[a](^r=length(2)) が unsatisfiable.
701 over(r) Ǥϡtrue/false ֤Ƥ롣^r -> +r/-r Ǥ⡢ 762 over(r) では、true/false に置き換えている。^r -> +r/-r でも、
702 [a](^r=length(2))Ϥᡣˤ˹פ롣 763 [a](^r=length(2))はだめ。これにさらに工夫がいる。
703 Ǥ⡢ϤäޤȤȤǤ⡢ɤ줯餤 764 でも、それはこっちの方がましだということだろう。でも、どれくらい
704 ޤʤ? local Ǥʤ餤? 765 ましなの? local でないぐらいか?
705 766
706 singleton ^(r,s) ֤Ƥ⡢[a](^r=lenth(2)) ϡ> length(4) 767 singleton を ^(r,s) で置き換えても、[a](^r=lenth(2)) は、> length(4)
707 fail 롣ʤ? 768 でfail する。なんで?
708 769
709 Sat Oct 7 17:20:17 BST 1995 770 Sat Oct 7 17:20:17 BST 1995
710 771
711 singleton removal r^s ǹԤʤȡlimit ĿФ̤ 772 singleton removal を r^s で行なうと、limit を一つ伸ばす効果が
712 餷älimitޤǤ褦ʾϾ֤롣 773 あるらしい。したがってlimitまでいくような場合は状態が増える。
713 r^s Ω˹Ԥʤ褦ˡǡȤǤΤ? 774 r^s の選択を独立に行なうような方法で、ちゃんとできるのか?
714 Ǥʤ褦ʵ⤹롣 775 できないような気もする。
715 776
716 Sat Oct 7 10:08:57 BST 1995 777 Sat Oct 7 10:08:57 BST 1995
717 778
718 (1) ֹͤ (ֹlimit) 779 (1) 番号を詰める (番号limitあり)
719 780
720 ϡäƤߤɡ^r ˤϸ̤ɡ¾ΤϤۤȤ 781 は、やってみたけど、^r には効果があるんだけど、他のはほとんど
721 طʤʤ[a](^r...) ߤʤΤˤϤʤΤ 782 関係ないなぁ。[a](^r...) みたいなものにはきかないのだろう。
722 783
723 Fri Oct 6 09:46:45 JST 1995 784 Fri Oct 6 09:46:45 JST 1995
724 785
725 (1) ֹͤ (ֹlimit) 786 (1) 番号を詰める (番号limitあり)
726 (2) singleton removal 787 (2) singleton removal
727 788
728 ĤǤʤꤤϤ(2)ɤˤʤʤ? 789 この二つでかなりいくはず。(2)どうにかなんないの?
729 790
730 (3) ֹ¤ low resolution? 791 (3) 番号を構造化する low resolution?
731 792
732 Edge driven logic ˤǤ뤫? 793 Edge driven な logic にできるか?
733 794
734 Thu Oct 5 18:27:29 JST 1995 795 Thu Oct 5 18:27:29 JST 1995
735 796
736 ࡣlength limit ϡޤʳ¤ޤ 797 うーむ。length limit は、うまくいくが、それ以外の制限がいまいち
737 ޤʤ͡ 798 うまくいかないね。
738 799
739 rename ^r ο¤ˡȡover ѴΤ 800 rename して ^r の数を制限する方法だと、over に変換されるものが
740 ޤ˥ɥۥå˷ޤäƤޤ 801 あまりにアドホックに決まってしまう。
741 r^n 802 r^n
742 n ˡ term äʤ? 803 の n に、何か term を持って来れないの?
743 804
744 total order ä뤫... ̤? ... 805 total order を持って来るか... 効果あるの? さぁ...
745 806
746 Sun Sep 24 01:14:36 JST 1995 807 Sun Sep 24 01:14:36 JST 1995
747 808
748 顢 809 だから、
749 810
750 ^r = false ˤȡ 811 ^r = false にすると、
751 812
752 [a](^r=legth(2)) -> [a](false=legth(2)) 813 [a](^r=legth(2)) -> [a](false=legth(2))
753 [a](false=legth(1)) 814 [a](false=legth(1))
754 [a](false=legth(0)) = unsatisfiable 815 [a](false=legth(0)) = unsatisfiable
755 816
756 ˤʤ뤫ʤΡ󤦤 817 になるからだめなの。うんうん。
757 true = length(2) false = length(2) 818 true = length(2) も false = length(2)
758 ⡢ξȤunsatisfiableɤ餫Ȥȡ 819 も、両方ともunsatisfiable。どちらかというと、
759 (length(2);not(length(2))) & true 820 (length(2);not(length(2))) & true
760 ȤʤΤ 821 となるのが正しい。
761 (length(2) & true) ; (not(length(2)) & true) 822 (length(2) & true) ; (not(length(2)) & true)
762 ? Ok ʤϤ 823 は? これは Ok なはず。
763 824
764 ä顢expansion singletonåơsingleton 825 だったら、expansion する前にsingletonをチェックして、singleton
765 ФƤ quantifiy ƤޤäƤΤ? ... 826 に対しては quantifiy してしまうってのは? うーむ...
766 827
767 㤢ʤ ^r -> ^r;not(^r) ǤϤʤΤ? 828 じゃあ、なんで ^r -> ^r;not(^r) ではだめなのか?
768 ϡͭΤ򤤤äˤƤ뤫顣 829 これは、終りを共有するものをいっしょにしているから。
769 830
770 ^r on n+1 831 ^r on n+1
771 |--| T 832 |--| T
772 |-| F 833 |-| F
773 || F 834 || F
774 |-| T 835 |-| T
775 || F 836 || F
776 || F 837 || F
777 838
778 Ȥ 839 とする
779 840
780 ^r on n 841 ^r on n
781 |---| 842 |---|
782 |--| 843 |--|
783 |-| 844 |-|
784 || 845 ||
785 846
786 ΡϡΩդդ 847 が新しいもの。これらは、独立。ふんふん。
787 848
788 Tue Sep 19 23:53:19 JST 1995 849 Tue Sep 19 23:53:19 JST 1995
789 850
790 ɤѤʡ 851 どうも変だな。
791 down(r^0) true;false ȤϤɤ㤦? 852 down(r^0) と true;false とはどこが違うんだ?
792 state(1 , not(true& ?(^r,not(@ @empty),@ @empty)&true)) 853 state(1 , not(true& ?(^r,not(@ @empty),@ @empty)&true))
793 [a](^r = length(2)) 854 [a](^r = length(2))
794 [empty,down(r,0),up(r)]->false 855 [empty,down(r,0),up(r)]->false
795 [empty,not(down(r,0)),up(r)]->empty 856 [empty,not(down(r,0)),up(r)]->empty
796 [empty,down(r,0),not(up(r))]->empty 857 [empty,down(r,0),not(up(r))]->empty
806 [a](^r = length(2)); 867 [a](^r = length(2));
807 not(@empty&true) 868 not(@empty&true)
808 not(length(1)&true) 869 not(length(1)&true)
809 [more,not(down(r,0)),not(up(r)),ev(r^0)]->3 870 [more,not(down(r,0)),not(up(r)),ev(r^0)]->3
810 871
811 äѤ㤦true ȡlength(1)true length(2)falseȤ 872 やっぱり違う。true だと、length(1)でtrue length(2)でfalseという
812 ʤϤξΩ򤷤ʤƤϤʤʤ 873 技が出来ない。この選択はこの場所で独立に選択しなくてはならない。
813 (?ɡtrue;false ʤ... ätrue?) 874 (ええ?だけど、true;false なんだから... だったらtrueか?)
814 +r, -r ޤ? 875 +r, -r の方がましか?
815 876
816 Sat Sep 16 11:44:25 JST 1995 877 Sat Sep 16 11:44:25 JST 1995
817 878
818 singleton ^r true, false ֤ȡ[]true,[]false ΰ̣ 879 singleton ^r を true, false に置き換えると、[]true,[]false の意味に
819 ʤäƤޤºݤϡtrue/false ʤΤˡ顢singleton removal 880 なってしまう。実際は、true/false なのに。だから、singleton removal
820 Ϥޤʤ 881 はうまくない。
821 882
822 t0: ^r = length(2) 883 t0: ^r = length(2)
823 t1: r^0 = length(1) empty/not(r^0) 884 t1: r^0 = length(1) empty/not(r^0)
824 t2: r^0 = mpty(1) empty/r^0 885 t2: r^0 = mpty(1) empty/r^0
825 886
826 Quantifier֤? äĤƤޤ? 887 Quantifierに置き換える? だったら残しておいた方がまし?
827 operator? 888 何かoperatorを作る?
828 some -> true/false 889 some -> true/false
829 quantified true? <>false ? not([](true)) = not(not(true & not true))). 890 quantified true? <>false かな? not([](true)) = not(not(true & not true))).
830 Ǥ⡢ȤĤfalseˤʤäƤޤoperatorˤȡdeterministic 891 でも、これだといつかはfalseになってしまう。operatorにすると、deterministic
831 Ǥʤʤ뤫Ϥޤnegation 892 でなくなるか。それはまずい。negationが。
832 893
833 Fri Sep 15 11:26:13 JST 1995 894 Fri Sep 15 11:26:13 JST 1995
834 895
835 singleton check itlˤ뤳ȤϤǤʤ? 896 singleton check をitl時にすることはできない?
836 897
837 Wed Sep 13 18:24:24 JST 1995 898 Wed Sep 13 18:24:24 JST 1995
838 899
839 ɡRITL CFG ޤǤΤ顢Regular Subset 뤳Ȥ 900 結局、RITLは CFG を含んでいるのだから、Regular Subset を決めることは
840 Ǥʤ 901 できない。
841 902
842 ^r depth¤С٤ϤǤ롣Ǥ 903 ^r のdepthを制限すれば、ある程度はできる。しかし、これでは
843 fairnessˤϤʤʤ͡ 904 fairnessにはならないね。
844 905
845 depth ʳ¤? ֿ¤˾ޤ 906 depth 以外の制限は? 状態数の制限が望ましい。
846 907
847 singleton remove ǤʤΤȤȸСʤΤ 908 singleton の remove でかなりのことが出来ると言えば、そうなのだが。
848 909
849 singleton remove Υߥ? 910 singleton remove のタイミング?
850 itlλ detect? 911 itlの時に detect?
851 itlstd λ detect? 912 itlstd の時に detect?
852 remove λ 913 remove の仕方
853 eventually(^r,N) 914 eventually(^r,N)
854 eventually(not(^r,N)) 915 eventually(not(^r,N))
855 롣ȤȤϡitldecomp show ľ 916 を挿入する。ということは、itldecomp の show の直前で
856 Ԥɤ 917 行えば良い。
857 918
858 ΤʾֽϤǤϤʤǤϤʤŪ˥ȥ졼 919 しかし、これだと正確な状態出力ではない。ではないが原理的にトレース
859 ǤʬϤäƤmark դΤǤƱˤʤäƤޤ 920 できる部分をはしょっているだけ。mark を付けるのでは同じになってしまう。
860 Ϥremove 921 やはりremoveしたい。
861 922
862 ^rνи٤򲡤뤳Ȥǡlogicˤʤ뤫? 㤨2ĤȤ? 923 ^rの出現頻度を押さえることで、logicになるか? 例えば2つとか?
863 924
864 * consistent ˤʤʤ==safeǤʤ(ɸפ...) 925 * consistent にならない==safeでない(標準形を工夫すれば...)
865 * ǤʤƤɤȤͤ⤢롣characterriseǤ? 926 * でなくても良いという考え方もある。characterriseできる?
866 927
867 ˤ衢singleton removal ǤɤޤǤʡ 928 いずれにせよ、singleton removal でどこまでいくかだな。
868 929
869 Sun Jul 23 10:16:02 JST 1995 930 Sun Jul 23 10:16:02 JST 1995
870 931
871 * ^r -> +r, -r depth ˤäΩ 932 * ^r -> +r, -r depth によって独立に選択
872 * +r r^depth ˤ 933 * +r も r^depth により選択
873 934
874 ȡ[a](^r),<>(not(^r))satisfiable 935 これだと、[a](^r),<>(not(^r))がsatisfiable
875 936
876 * ^r -> +r, -r depth ˤäΩ򤷤ʤ 937 * ^r -> +r, -r depth によって独立に選択しない
877 938
878 ȡ[a](^r=length(2))unsatisfiable 939 と、[a](^r=length(2))がunsatisfiable
879 940
880 ࡢޤ 941 うーむ、うまくいかん。
881 942
882 Sat Jul 22 12:52:11 JST 1995 943 Sat Jul 22 12:52:11 JST 1995
883 944
884 * depthΰ㤤chopνǹԤʤ 945 * depthの違いはchopの処理で行なう
885 * ^remptyȡ+r, -remptyΩ 946 * ^rのemptyと、+r, -rのemptyは独立
886 * ^rmoreȡ+r, -rδط 947 * ^rのmoreと、+r, -rの関係
887 948
888 +r, -r ϡۤʤdepthT/Fλ 949 +r, -r は、異なるdepthでT/Fの時に生じる
889 +r ϡ˹ήɤ 950 既に +r がある時は、それに合流して良い
890 +r/\-r Ȥʤ뤳ȤϤʤfalse 951 +r/\-r となることはない。それはfalse。
891 952
892 |-------| +r 953 |-------| +r
893 |---------| -r 954 |---------| -r
894 ^r +r Ȥ 955 ^r +r とする
895 not(^r)ä-rȤ 956 not(^r)があったら-rとする
896 957
897 Ǥ? 958 これでいいか?
898 tailͭrǤ not(^r),^rΰо 959 tailを共有するrである not(^r),と^rの扱いは対称
899 ^r/-rȹ礻? 960 ^r/-rの組合せは?
900 961
901 +r, -r ä 962 +r, -r が解消される場合
902 963
903 * +r or -r empryˤʤȤ 964 * +r or -r がempryになるとき
904 -r emptyˤʤʤ 965 -r はemptyにならない
905 966
906 +rĤäƳ뤫? -rʤдطʤ 967 +rが残って害があるか? -rがなければ関係ない
907 ֤뤱ɡ 968 状態は増えるけど。
908 969
909 Fri Jul 14 18:31:19 JST 1995 970 Fri Jul 14 18:31:19 JST 1995
910 971
911 ۤʤ chop ǡۤʤrֹդ롣 972 異なる chop で、異なるrの番号を付ける。
912 ֹ up(^r), down(r,n) Ԥʤ 973 その番号毎に up(^r), down(r,n) を行なう
913 974
914 ˤäơ٤Ƥȹ礻롣 975 これによって、すべての組合せが一応得られる。
915 976
916 ֹϾ֤ˤղäʤ(Τ?) 977 番号は状態には付加しない。(いいのか?)
917 ƱintervalǤϡ 978 同じinterval上では、
918 r, not(r) 979 r, not(r)
919 ... ... ޤ 980 があり得る... これは... 気まずいか。
920 ^r -> +^r, -^r 981 ^r -> +^r, -^r
921 Ȥ? ... +up, -up ? 982 とする? すると... +up, -up がある?
922 983
923 ޤƤߤ褦(äѤä...) 984 まあ、試してみよう。(やっぱりだめだった...)
924 985
925 Thu Jul 13 14:05:06 JST 1995 986 Thu Jul 13 14:05:06 JST 1995
926 987
927 r^n ο򸺤餹 988 r^n の数を減らす
928 => ǥˡɽ 989 => 等価でユニークな表現
929 990
930 singleton r^n Ͼä 991 singleton r^n は消せる
931 992
932 doubleton r^nɤͻ礷 993 doubleton r^nどうしを融合したい。
933 994
934 rr^nŪ (ϤǤΤ... +r/-r) 995 新しいrをr^nに相対的に定義する (それはできるのだが... +r/-r)
935 ΤϡޤäΤ­ʤΤ롣ֿ 996 のは、うまくいったのだが、足りないものがある。状態数が
936 ­ʤ 997 足りない。
937 998
938 * ɬפʾֿΤߤ̤ 999 * 必要な状態数のみを区別する
939 * Ʊ̤ѿ϶̤ʤ 1000 * 同じ結果を生じる変数は区別しない
940 1001
941 ʬȤƱɤ / 㤦ȤȤФʤȤʤ 1002 自分自身と同じかどうか / 違うということを覚えないといけない
942 Ʊäطʤ 1003 同じだったら関係ない
943 1004
944 What happen in next case? ([a](^r)) 1005 What happen in next case? ([a](^r))
945 1006
946 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true 1007 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true
947 1008
948 ---|-----| r^5 1009 ---|-----| r^5
949 ---|----| r 1010 ---|----| r
950 1011
951 r^5аĸ롣ʤr^6ǰ롣 1012 r^5が落ちれば一つ減る。減らなければr^6で一つ増える。しかし、
952 ξƤϤʤr^5 ^r Ȥϴط̵ 1013 この場合は増えてはいけない。r^5 と ^r 自身は関係が無い。
953 ̤ƱȤط롣( 狼ʤ褦.... ) 1014 が、結果は同じという関係がある。( うがー、わからないよう.... )
954 1015
955 st6: 1016 st6:
956 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true 1017 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true
957 1018
958 up(^r),down(r^5),down(^r) @not(r^5)&t, t, t, @not(r^6)&t 1019 up(^r),down(r^5),down(^r) @not(r^5)&t, t, t, @not(r^6)&t
965 Mon Jul 10 20:01:46 JST 1995 1026 Mon Jul 10 20:01:46 JST 1995
966 1027
967 f(^r) => contratint_1(^r) & continuation_1(^r) 1028 f(^r) => contratint_1(^r) & continuation_1(^r)
968 g(^r) => contratint_2(^r) & continuation_2(^r) 1029 g(^r) => contratint_2(^r) & continuation_2(^r)
969 1030
970 r(r^n)&c(r^n) n 1031 r(r^n)&c(r^n) がnを除いて等しい時、
971 r^n => r^n' 롣 1032 r^n => r^n' がいえる。
972 ɡ̤ɬʤ(...) 1033 けど、別に等しい必然性もない。(たしかに...)
973 1034
974 r^nquantifyɤȤȤϡƱʤäɤȤ? 1035 r^nはquantifyして良い。ということは、同じなら消して良いということ?
975 ȤȤcross term ? 1036 ということか。cross term は?
976 exists(^r, empty(^r)? ...) 1037 exists(^r, empty(^r)? ...)
977 1038
978 r0: { +r(const, continu), 1039 r0: { +r(const, continu),
979 -r(const, continu) } 1040 -r(const, continu) }
980 r1: { +r(const, continu), 1041 r1: { +r(const, continu),
981 -r(const, continu) } 1042 -r(const, continu) }
982 1043
983 Ĥ 1044 いつかは
984 +r(empty,continu) 1045 +r(empty,continu)
985 +r(true,continu) 1046 +r(true,continu)
986 Τɤ餫ˤ䡢ʤemptyʤ̵true(?) 1047 のどちらかにいく。いや、いかない。emptyなら問題無い。trueが問題(?)
987 +r(fixpoint,contiu) 1048 +r(fixpoint,contiu)
988 Ȥˤʤ롣줬¸ߤȤȤˤʤ롣 1049 という形になる。これがたくさん存在するということになる。
989 +/-r^n(fixpoint_k,continu_k_i) 1050 +/-r^n(fixpoint_k,continu_k_i)
990 Ȥ櫓ξr^nνŤʤ꤬äǤϲ衣 1051 というわけだ。この場合のr^nの重なりが解消できれば問題は解決。
991 ޤʤ... 1052 うまくいかないね...
992 1053
993 1054
994 ǡƱΤϾäɤ򤽤ʤȾäˤ 1055 で、同じものは消して良い。順序をそろえないと消しにくい。
995 㤦rǤƱåʤäɤ(reular variableϡ¼ 1056 違うrでも同じカッコなら消して良い。(reular variableは、実質は
996 , ^r => r,^common ˤ뤫? ϤäȰ㤦) 1057 一つ, ^r => r,^common にするか? それはちょっと違う)
997 ξϾäƤⴳĤΥѥѤʤĥѥ 1058 この場合は消しても干渉のパターンが変わらない。干渉パターン
998 Ȥ˥ޥå󥰤Ȥ뤫顣(ͭ¤ȹ礻ʤΤ?) 1059 ごとにマッチングをとるから。(有限の組合せなのか?)
999 1060
1000 äΤterm levelǤʤ? 1061 消すのはterm levelでおこなう?
1001 c(r^n, i_n...) & ... 1062 c(r^n, i_n...) & ...
1002 c(r^n, i_n...) 1063 c(r^n, i_n...)
1003 Ȥtermr^n˴ؤƤϤǤƤʤää顢¾ 1064 というtermしかr^nに関してはでてこない。消せるんだったら、他の
1004 ˡϤøǤס 1065 方法はいい加減でも大丈夫。
1005 1066
1006 f(r^n)f(r^n'1)δط 1067 f(r^n)とf(r^n'1)の関係
1007 |------|-| 1068 |------|-|
1008 |----|-| 1069 |----|-|
1009 r^n, r^n' ȤΩ 1070 r^n, r^n' 自身は独立
1010 1071
1011 r^1(r,c) 1072 r^1(r,c)
1012 r^2(r,c) 1073 r^2(r,c)
1013 empty(r^1),empty(r^2),empty(r) => c 1074 empty(r^1),empty(r^2),empty(r) => c
1014 cross term 1075 cross term
1015 empty(r^1),more(r^2), empty(r) => c,(more(r),r^1(@(r),c)) 1076 empty(r^1),more(r^2), empty(r) => c,(more(r),r^1(@(r),c))
1016 more(r^1),more(r^2), more(r) => 1077 more(r^1),more(r^2), more(r) =>
1017 more(r),r^1(@(r),c),r^2(@(r),c) 1078 more(r),r^1(@(r),c),r^2(@(r),c)
1018 == 1079 ==
1019 r^1(c);c,more(r),r^1(@(r),c);more(r),r^1(@(r),c),r^2(@(r),c) 1080 r^1(c);c,more(r),r^1(@(r),c);more(r),r^1(@(r),c),r^2(@(r),c)
1020 ¾r^nȴĤˡѤäƤޤ... 1081 他のr^nと干渉する方法が変わってしまう...
1021 1082
1022 1083
1023 Sun Jul 9 15:32:43 JST 1995 1084 Sun Jul 9 15:32:43 JST 1995
1024 1085
1025 r^1 & true; 1086 r^1 & true;
1026 r^2 & true; 1087 r^2 & true;
1027 r^3 & true 1088 r^3 & true
1028 1089
1029 ĤˤޤȤʤ? 1090 一つにまとめられない?
1030 1091
1031 f(+/- r^n) (ɬtopˤ/ŸƤ뤫) 1092 f(+/- r^n) (必ずtopにある/一度展開されているから)
1032 |-------------|-----------| 1093 |-------------|-----------|
1033 down(r^n) => true/false 1094 down(r^n) => true/false
1034 1095
1035 1096 性質
1036 f(+/- r^n) 1097 f(+/- r^n)
1037 down(r^n) => f((+/-true ,empty)) 1098 down(r^n) => f((+/-true ,empty))
1038 not(down(r^n)) => f(+/- r^n) 1099 not(down(r^n)) => f(+/- r^n)
1039 parallel term̵ʤޤŸ 1100 parallel termがある時は無くなるまで展開する
1040 r^n, *length(3) ʤɤ? ̵뤷ɤ 1101 r^n, *length(3) などは? これは無視して良い
1041 r^n, *length(3) & true 1102 r^n, *length(3) & true が問題
1042 => evenrually true + *length(3) 1103 => evenrually true + *length(3)
1043 1104
1044 顢nʣäƤ⡢f((+/-true ,empty))ƱʤƱǤ褤(?) 1105 だから、nが複数あっても、f((+/-true ,empty))が同じなら同じでよい(?)
1045 1106
1046 f(+/- r^n) => true & down(r^n),f(+/-true,empty) 1107 f(+/- r^n) => true & down(r^n),f(+/-true,empty)
1047 => down(r^n) = eventually(f(+/-true,empty)) 1108 => down(r^n) = eventually(f(+/-true,empty))
1048 1109
1049 ȤȤϡäѤdown(r^n)򳰤˽ФȤ? 1110 ということは、やっぱりdown(r^n)を外に出せるということ?
1050 r^n & true ʤ eventually(true) 1111 r^n & true なら eventually(true)
1051 not(r^n) & true ʤ? 1112 not(r^n) & true なら?
1052 1113
1053 դࡣ eventually(f) f ˤr^nʤ 1114 ふむ。そして eventually(f) の f にはr^nは入らない。これは
1054 뤫Τʤ 1115 いけるかも知れない。
1055 1116
1056 chopνλˡeventuality listbdtηdz˽Фɤ 1117 chopの処理の時に、eventuality listをbdtの形で外に出せば良い。
1057 eventuality 줿r^nΩ( 1118 eventuality が満たされた時がr^nが成立した時。(これも
1058 ͤ...) 1119 前考えたな...)
1059 ^r & .... 1120 ^r & ....
1060 Ȥ? 1121 という形だけ?
1061 1122
1062 (^r, g) & f => ev(f),(g & f) äȰ㤦... 1123 (^r, g) & f => ev(f),(g & f) ちょっと違う...
1063 (^r & f),(g & f) 1124 (^r & f),(g & f)
1064 1125
1065 ȤϾۤʤ衣not ޤʤϤ 1126 とは少し異なるよ。not がうまくないはず。
1066 not(ev(f)); not(g & f) (?) 1127 not(ev(f)); not(g & f) (?)
1067 1128
1068 ... ev(f)С^rɤ() 1129 そうか... ev(f)が満たされれば、^rは落ちて良い。(落ちれる)
1069 ʤƤ⤤ 1130 落ちなくてもいい。
1070 1131
1071 äevenruality formITL񤭴Τ? 1132 前もってevenruality formにITLを書き換えるのは?
1072 f(r) => g(eventualy(h)) 1133 f(r) => g(eventualy(h))
1073 1134
1074 diceidableʤΤ? 񤱤Ȥ... 1135 本当にdiceidableなのか? 整数方程式が書けるとすれば...
1075 1136
1076 Fri Jul 7 18:51:32 JST 1995 1137 Fri Jul 7 18:51:32 JST 1995
1077 1138
1078 true & ^r & true => 1139 true & ^r & true =>
1079 r^1 & true; 1140 r^1 & true;
1080 r^2 & true; 1141 r^2 & true;
1081 r^3 & true 1142 r^3 & true
1082 Ȥʤ롣ȤȤϡҤȤĤinterval򸫤Ƶۼ뤳ȤϽʤ 1143 となる。ということは、ひとつのintervalだけを見て吸収することは出来ない。
1083 1144
1084 t1 t2 1145 t1 t2
1085 up(r) down(r^1) 1146 up(r) down(r^1)
1086 r&true |-------------|-------------------- 1147 r&true |-------------|--------------------
1087 not(r&true) |----------------|not(down(r^1)---- 1148 not(r&true) |----------------|not(down(r^1)----
1088 |---|up(r)----|not(down(r^2)------- 1149 |---|up(r)----|not(down(r^2)-------
1089 1150
1090 r^1 ϶礹r^1طʤäñȤ 1151 r^1 は競合するr^1がある時しか関係しない。したがって単独に
1091 ФƤr^1ϸ߻ 1152 出てくるr^1は現在時点で
1092 fin(r^1) => true 1153 fin(r^1) => true
1093 fin(not(r^1)) => false 1154 fin(not(r^1)) => false
1094 ɤǡtrue & ^r & true ϼ«롣 1155 を決めて良い。これだけで、true & ^r & true は収束する。
1095 Ǽ«뤫? ֤󡢤ʤ 1156 が、それだけで収束するか? たぶん、しない。
1096 1157
1097 (1) 1158 (1)
1098 ʣλľ֤ĤˤޤȤФǤ롣+r, -r Ϥ 1159 複数の始点を持つ状態を一つにまとめられればできる。+r, -r はそういう
1099 ˡäĤˤϤʤʤͭ¤ȹ礻ˤʤ롣 1160 方法だった。が一つにはならない。有限な組合せになる。
1100 1161
1101 (2) 1162 (2)
1102 «ȤСͭ줿r^nȤͭ¤ʾǤ롣ϡfiniteness 1163 収束するとすれば、共有されたr^nの組が有限な場合である。これは、finiteness
1103 ξ롣äƶͭǽΤtermǤ뤫? ( 1164 の条件に相当する。前もって共有される可能性のあるtermを生成できるか? (
1104 ֤Ǥ) 1165 たぶんできる)
1105 1166
1106 äʣФ褿(㤦sytactical interval)^rֹդ 1167 前もって複数出て来た(違うsytactical interval上の)^rに番号を付けて
1107 ̤ƤϡۤʤֹǤʤ? 1168 識別しておく。競合は、異なる番号上でしか起きない?
1108 [](<>(^r)) = not(ture & not(true & ^r)) 1169 [](<>(^r)) = not(ture & not(true & ^r))
1109 Τ褦ʾ? Ʊֹζͭ+r, -rǹʤ 1170 のような場合は? そうか。同じ番号上の共有は+r, -rで構わない。
1110 (true or false ) 1171 (true or false だから)
1111 [](<>(^r)) <-> [](<>(^r)) 1172 [](<>(^r)) <-> [](<>(^r))
1112 Τ褦ʾ? 1173 のような場合は?
1113 1174
1114 Fri Jun 30 20:08:47 JST 1995 1175 Fri Jun 30 20:08:47 JST 1995
1115 1176
1116 f(r^1,r^2,r^3) & true, 1177 f(r^1,r^2,r^3) & true,
1117 g(r^1,r^2,r^3) & true 1178 g(r^1,r^2,r^3) & true
1118 1179
1119 f(r^1,r^2,r^3)g(r^1,r^2,r^3)򸫤ʤr^nο򸺤餵ʤȤʤ 1180 f(r^1,r^2,r^3)とg(r^1,r^2,r^3)を見ながらr^nの数を減らさないといけない。
1120 1181
1121 r^n ϡemptyλƶʤmoreλtrueƱ 1182 r^n は、emptyの時しか影響しない。moreの時はtrueと同じ。
1122 1183
1123 ^r Τߤr^n䤹򤤤˵ۼ뤫Ĵ٤ɤ? 1184 ^r のみが新しいr^nを増やす。これをいかに吸収するかを調べれば良い?
1124 1185
1125 f(r^cur,r^1,r^2,r^3) & true, 1186 f(r^cur,r^1,r^2,r^3) & true,
1126 => r^cur ? +f(r^1,r^2,r^3) : -f(r^1,r^2,r^3) & true 1187 => r^cur ? +f(r^1,r^2,r^3) : -f(r^1,r^2,r^3) & true
1127 g(r^cur,r^1,r^2,r^3) & true 1188 g(r^cur,r^1,r^2,r^3) & true
1128 => r^cur ? +g(r^1,r^2,r^3) : -g(r^1,r^2,r^3) & true 1189 => r^cur ? +g(r^1,r^2,r^3) : -g(r^1,r^2,r^3) & true
1129 1190
1130 1191
1131 Fri Jun 30 10:48:46 JST 1995 1192 Fri Jun 30 10:48:46 JST 1995
1132 1193
1133 stateˡregular variablemapƤ롣ˡޤ 1194 各stateに、regular variableのmapを割り当てる。方法がいまいち
1134 狼ʤ^r줿֤̤뤳Ȥɬס 1195 わからない。^rの生成された状態を識別することが必要。
1135 1196
1136 ^r(s) äƤߤ롣Τä 1197 ^r(s) をやってみる。昔もやった。
1137 true & ^r 1198 true & ^r
1138 ȯ 1199 が爆発する
1139 r^1 ; r^2; r^3; ... ; true & ^r 1200 r^1 ; r^2; r^3; ... ; true & ^r
1140 줬 1201 これが
1141 r^1 true & ^r 1202 r^1 true & ^r
1142 Ȥʤɤ 1203 となれば良い。
1143 r^1 .... r^2 1204 r^1 .... r^2
1144 Ͽr^nˤʤ롣(ߴط?) ^r ɤݻ 1205 は新しいr^nになる。(相互関係は?) ^r どうしの制約を保持した
1145 äȤ⾯ʤr^n򤹤ɤ(Ѵsafe & compete?) 1206 もっとも少ないr^nを選択すれば良い。(この変換はsafe & compete?)
1146 ߴط¸ʤʤ^r򤹤٤ƶ̤ˤɤ 1207 相互関係を保存しないなら^rをすべて共通にすれば良い。が、
1147 Ϥޤʤ 1208 それはうまくいかない。
1148 r^1 , not(r^2) -> r^1, not(r^1) -> false 1209 r^1 , not(r^2) -> r^1, not(r^1) -> false
1149 Τ褦ʾ礬뤫顣 1210 のような場合があるから。
1150 r^1 , not(r^2) -> r^1 1211 r^1 , not(r^2) -> r^1
1151 ? 1212 か?
1152 1213
1153 ¾ѿ? r^1 .. r^n ˰¸termѴ 1214 他の変数が入る場合は? r^1 .. r^n に依存するtermの変換を
1154 ׻롣= BDT leaf οɽǤǾr^n 1215 計算する。= BDT の leaf の数。それを表現できる最小のr^nを
1155 롣 1216 作る。
1156 1217
1157 Сtemporal operatorΥͥȤѤʤΤ顢 1218 そうすれば、temporal operatorのネストは変わらないのだから、
1158 Τͭ¤ˤʤϤ 1219 全体は有限になるはず。
1159 1220
1160 ǤʤfullǤʤregularˤʤ? ^r context dependent 1221 これでなんでfullでなくてregularになるの? ^r がcontext dependent
1161 Ǥʤ顣 r^1 , not(r^2) -> r^1 ϡcontext dependent Ǥ 1222 でないから。 r^1 , not(r^2) -> r^1 は、context dependent では
1162 Ǥʤ(ʤۤ...) 1223 できない。(なるほど...)
1163 1224
1164 Wed May 24 20:32:34 JST 1995 1225 Wed May 24 20:32:34 JST 1995
1165 1226
1166 ^rϡϤꡢ 1227 ^rは、やはり、
1167 ^r -> +r, -r 1228 ^r -> +r, -r
1168 ѴǤʤȤ٤ǥϡRITL 1229 の変換でなんとかするべき。こうして生成したモデルは、正しいRITLを
1169 ޤǤ롣ȤΥå򤹤ɤ 1230 含んでいる。あとは整合性のチェックをすれば良い。
1170 1231
1171 (1) local consstency check => regular variable 1232 (1) local consstency check => regular variable
1172 (2) global consistency check => regular constant 1233 (2) global consistency check => regular constant
1173 1234
1174 ɤ褦check? .... 1235 どういうようにcheckするの? ん....
1175 1236
1176 1237
1177 Τbdcomp.pl bddlibǽ񤭴롣 1238 昔のbdcomp.pl をbddlibで書き換える。
1178 1239
1179 characteristic function f(q) 1240 characteristic function f(q)
1180 f(q) = more,fx_q(sbn,sbx,P);empty,fn_q(P) 1241 f(q) = more,fx_q(sbn,sbx,P);empty,fn_q(P)
1181 1242
1182 f(p&q) = f(q) & q 1243 f(p&q) = f(q) & q
1183 1244
1184 1245
1185 Tue May 2 17:49:35 JST 1995 1246 Tue May 2 17:49:35 JST 1995
1186 1247
1187 BDDLIBȤ߹碌äѤ Prolog <-> BDD Ѵ 1248 BDDLIBを組み合わせたが、やっぱり Prolog <-> BDD の変換が入るだけ
1188 ٤ʤäbdtstd.pl ˤʤΤ 1249 遅くなるだけだった。bdtstd.pl は綺麗になるのだが。
1189 1250
1190 äBDD٤ʤä(BDT/*) ϡ 1251 前作ったBDDの方式も遅くなるだけだった。(BDT/*) それは、
1191 BDD leaf next leafŸ 1252 BDD の leaf をnext leafに展開
1192 BDDκƹ 1253 BDDの再構成
1193 next leaf2-3 treeϿ 1254 next leafを2-3 treeに登録
1194 next leaf 򤵤Ÿ 1255 新しいnext leaf をさらに展開
1195 ȤΤ٤ä顣 1256 というのがすごく遅かったから。
1196 1257
1197 Charcteristic Function 夲ˡϡǤBDDLIBʤ 1258 Charcteristic Function を作り上げる方法は、今一だ。でもBDDLIBなら
1198 ޤ⤷ʤ 1259 うまくいくかもしれない。
1199 1260
1200 Subtermäơ٤ơ 1261 Subtermを前もって、すべて、
1201 condition, next 1262 condition, next
1202 ȤBDDŸƤ? 1263 というBDDに展開しておいたら?
1203 1264
1204 QuantifierʤɤϡSubterm˾֤Ƥޤ顢 1265 Quantifierなどは、Subtermの中に状態が現れてしまう。だから、
1205 äơŸƤ 1266 前もって、中を展開しておく。
1206 1267
1207 СȤνϡBDDΤߤǤǤϤ(CFˡ 1268 そうすれば、あとの処理は、BDDのみでできるはずだ。(しかし、CF法と
1208 ̤Ʊ?) 1269 結果は同じ?)
1209 1270
1210 Wed Mar 29 17:22:43 JST 1995 1271 Wed Mar 29 17:22:43 JST 1995
1211 1272
1212 regular(r,....r....) 1273 regular(r,....r....)
1213 ȤȤ ( QPTL <-> RITL ... ) 1274 という形を使う ( QPTL <-> RITL だから... )
1214 1275
1215 QuantifierľܻȤΤ? 1276 Quantifierを直接使うのは?
1216 st(0) = exists(c, c->st(1),not(c)->st(2)) 1277 st(0) = exists(c, c->st(1),not(c)->st(2))
1217 ... 1278 さぁ...
1218 1279
1219 begin(r,formuala) -> T/F 1280 begin(r,formuala) -> T/F
1220 end(r,formula) -> T/F 1281 end(r,formula) -> T/F
1221 1282
1222 ۤʤ뤦formula¤Ʊä-> Ĥ regular(r, f) 1283 異なるうformulaが実は同じだった。-> いつか regular(r, f)
1223 ȤƱˤʤ롣 1284 という同じ形になる。
1224 1285
1225 regular(r,f(r)) 1286 regular(r,f(r))
1226 empty(f(r)) -> r=true,empty 1287 empty(f(r)) -> r=true,empty
1227 not(empty(f(r))) -> r=false,empty 1288 not(empty(f(r))) -> r=false,empty
1228 regular(r,f(r)) 1289 regular(r,f(r))
1229 more(f(r)) -> r=true,regular(r,fx(r)) 1290 more(f(r)) -> r=true,regular(r,fx(r))
1230 not(more(f(r))) -> r=false,regular(r,fx(r)) 1291 not(more(f(r))) -> r=false,regular(r,fx(r))
1231 1292
1232 äǥϾĹ 1293 したがって生成されるモデルは冗長。
1233 1294
1234 chop 褿 r reset ʤȤʤ 1295 chop が来た時に r をreset しないといけない。
1235 (...) ä顢regular(r,f(r))Ϥʤ? 1296 (だよね...) だったら、regular(r,f(r))はいらない?
1236 ɤä? r ääƤΤ? 1297 どうやって? r を前もって宣言するってのは?
1237 1298
1238 PDA Ȥδط? 1299 PDA との関係は?
1239 1300
1240 Thu Dec 15 20:21:58 JST 1994 1301 Thu Dec 15 20:21:58 JST 1994
1241 1302
1242 ModelȤб 1303 Modelとの対応
1243 1304
1244 t0 -[+-]-> t1 -[+-]-> t2 -[+-]-> t3 1305 t0 -[+-]-> t1 -[+-]-> t2 -[+-]-> t3
1245 1306
1246 |---------|-----------| 1307 |---------|-----------|
1247 r0 r1 r2 1308 r0 r1 r2
1248 |-----------|-----------| 1309 |-----------|-----------|
1249 r0' r1' r2' 1310 r0' r1' r2'
1250 1311
1251 r0 Ͼ0Ϥ롣 1312 r0 は常に要素0から始める。
1252 Ϥ롣 1313 から始める。
1253 r0 -[-]-> r1 ǽǤ˥եȤ롣 1314 r0 -[-]-> r1 で集合の要素にシフトする。
1254 r0 -[+]-> r1 Ǽλ֤ΤΤȰ㤦FAǤ뤳Ȥɽ 1315 r0 -[+]-> r1 で次の時間のものと違うFAであることを表す。
1255 1316
1256 Mon Nov 28 19:27:37 JST 1994 1317 Mon Nov 28 19:27:37 JST 1994
1257 1318
1258 RITLơȤITL formulaboolɽboolBDDɽ롣 1319 RITLステートをITL formulaのbool代数で表す。bool代数はBDDで表現する。
1259 1320
1260 ȤITL formulaȤsubtermν顢Ťboolˤʤ롣 1321 もともとITL formula自身がsubtermの集合だから、二重のbool代数になる。
1261 äơdouble exponential algorithmȤʤ롣 1322 したがって、double exponential algorithmとなる。
1262 1323
1263 r/not(r) flip Ǥϡ٤Ƥȹ礻뤬٤Ƥȹ礻 1324 r/not(r) flip では、すべての組合せは生じるが、すべての組合せの
1264 ϢɽǤʤäơ٤Ƥȹ礻Ȥä 1325 連結は表現できない。したがって、生じたすべての組合せをとって
1265 ɤ 1326 おけば良い。
1266 1327
1267 κ 1328 集合の作り方
1268 r/not(r) flip LITL򽸹Ȥƻ (implementation?) 1329 r/not(r) flip で生じたLITLを集合として持つ (implementationは?)
1269 1330
1270 r 1331 r の例
1271 [1] r -(+r)-> r, r -(-r)-> not(r) {r,not(r)} 1332 [1] r -(+r)-> r, r -(-r)-> not(r) {r,not(r)}
1272 [2] r -> {r,not(r)} -> {r,not(r)} () 1333 [2] r -> {r,not(r)} -> {r,not(r)} (終り)
1273 1334
1274 t & r (detailϰۤʤ롣emptyξ礬뤫) 1335 t & r の例 (detailは異なる。emptyの場合があるから)
1275 [1] t & r -(+r)-> r\/t & r, t & r -(-r)-> not(r)\/t & r 1336 [1] t & r -(+r)-> r\/t & r, t & r -(-r)-> not(r)\/t & r
1276 {r\/t&r, not(r)\/t&r} 1337 {r\/t&r, not(r)\/t&r}
1277 [2] {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} () 1338 [2] {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} (終り)
1278 [a](r=length(2)) 1339 [a](r=length(2))の例
1279 [1] [a](r=length(2)) -(+r)- > r =length(1)/\[a](r=length(2)) 1340 [1] [a](r=length(2)) -(+r)- > r =length(1)/\[a](r=length(2))
1280 -(-r)- > not(r)=length(1)/\[a](r=length(2)) 1341 -(-r)- > not(r)=length(1)/\[a](r=length(2))
1281 {r =length(1)/\[a](r=length(2)), 1342 {r =length(1)/\[a](r=length(2)),
1282 not(r)=length(1)/\[a](r=length(2))} 1343 not(r)=length(1)/\[a](r=length(2))}
1283 [2] {r =length(1)/\[a](r=length(2)), 1344 [2] {r =length(1)/\[a](r=length(2)),
1284 not(r)=length(1)/\[a](r=length(2))} => 1345 not(r)=length(1)/\[a](r=length(2))} =>
1285 { r =length(0)/\ r =length(1)/\[a](r=length(2)), F 1346 { r =length(0)/\ r =length(1)/\[a](r=length(2)), F
1286 r =length(0)/\ ~r =length(1)/\[a](r=length(2)), 1347 r =length(0)/\ ~r =length(1)/\[a](r=length(2)),
1287 ~r =length(0)/\ r =length(1)/\[a](r=length(2)), 1348 ~r =length(0)/\ r =length(1)/\[a](r=length(2)),
1288 ~r =length(0)/\ ~r =length(1)/\[a](r=length(2))} F 1349 ~r =length(0)/\ ~r =length(1)/\[a](r=length(2))} F
1289 [3] => [2] 1350 [3] => [2] へ
1290 or [1]' (r=length(1)trueξ) 1351 or [1]'へ (r=length(1)がtrueの場合)
1291 1352
1292 äȥѥȤˤʤ󤸤ʤ? (finiteness) 1353 もっとコンパクトになるんじゃない? (これだとfinitenessは明解だけど)
1293 ITL(r)ϡrr/not(r)ǤդִΤsubsetɤȤɤ줬פ뤫 1354 ITL(r)は、rをr/not(r)に任意に置換したもののsubset。どれとどれが一致するかを
1294 ФɤΤǤ? => ϻΤס 1355 覚えれば良いのでは? => 開始時点が等しいものが一致。
1295 IndexդΤϥᡣ=> ǥ뤬ͭ¤ˤʤʤ(ࡢ狼ʤ) 1356 Indexを付けるのはダメ。=> モデルが有限にならない。(うーむ、わからない)
1296 1357
1297 ITL(r) => Ÿ => subset 1358 ITL(r) => 展開 => subset
1298 1359
1299 1360
1300 ǥβ 1361 モデルの解釈
1301 1362
1302 boolϡrassignmentͿȲ褹롣Ĥ 1363 bool代数は、rのassignmentが与えられると解決する。しかし、一つの
1303 Ρɤ̤ʲͭ뤳Ȥ⤢롣 1364 ノードが別な解釈を共有することもあり得る。
1304 1365
1305 Term֤ǤդܤΤ? 1366 Term間は任意に遷移するのか?
1306 ǤϤʤơƱܤ롣 1367 そうではなくて、同時に遷移する。
1307 1368
1308 ۤʤ볫ϻrϡƱ˰ۤʤܤ 1369 異なる開始時点を持つrは、同時に異なる遷移を廻る
1309 ٤Ʋǽܤ櫓ǤϤʤĤFȤʤػߤȤʤ 1370 すべて可能な遷移があるわけではなく、いくつかはFとなり禁止となる
1310 => r Ф 1371 => r に対する制約
1311 1372
1312 ¹ԤǤ? 1373 実行できる?
1313 1374
1314 boolΰĤinstanceŬ˼¹Ԥɤ 1375 bool節の一つのinstanceを適当に実行すれば良い
1315 1376
1316 Rñautomaton꿶뤳Ȥϲǽ? 1377 Rに単一のautomatonを割り振ることは可能か?
1317 [a](R = r) where r is automaton constant 1378 [a](R = r) where r is automaton constant
1318 1379
1319 ֤̤äƥǥ 1380 時間を遡ってモデルを作る
1320 1381
1321 ˤäơstate minimizationƱ餻뤳ȤǤ 1382 これによって、state minimizationも同時に走らせることができる
1322 MinimizationΥƥȥץäƸ뤳 1383 Minimizationのテストプログラムを作って見ること
1323 1384
1324 Thu Nov 24 14:54:00 JST 1994 1385 Thu Nov 24 14:54:00 JST 1994
1325 1386
1326 LTTL = LITL < RE 1387 LTTL = LITL < RE
1327 LITL* = RE 1388 LITL* = RE
1328 RITL = RE RITL(= 2nd order LITL) 1389 RITL = RE RITL(= 2nd order LITL)
1329 RITL is decidable 1390 RITL is decidable
1330 1391
1331 LTTL = LITL on compact time 1392 LTTL = LITL on compact time
1332 1393
1333 Even(p)ϡLITLǤᡣ 1394 Even(p)は、LITLでもだめ。
1334 (p.)* Ǥʤ 1395 (p.)* ができない
1335 (abac)* -> (a[bc])* 1396 (abac)* -> (a[bc])*
1336 1397
1337 LITL -> LTTL converter 1398 LITL -> LTTL converter
1338 1399
1339 LITL/LTTLϡäѤ귲 1400 LITL/LTTLは、やっぱり群を構成する
1340 1401
1341 []a & []b & []a 1402 []a & []b & []a
1342 a...ab...ba...a -> a until (b until []a) 1403 a...ab...ba...a -> a until (b until []a)
1343 conversionǤ? 1404 だからconversionできる?
1344 a & b & a 1405 a & b & aは
1345 a, <>(b, <>a) 1406 a, <>(b, <>a)
1346 ... Ǥʵ... 1407 か... うう、できそうな気がする...
1347 1408
1348 P & Q -> start(P),(run(P) until lttl(Q)) ѷ 1409 P & Q -> start(P),(run(P) until lttl(Q)) に変形する
1349 run(P)ˤquantifierΤ? ʤ? 1410 run(P)にはquantifierが入るのか? 入らない?
1350 1411
1351 events continue 1412 events continue
1352 |----------|..........| 1413 |----------|..........|
1353 |-> <>(events) 1414 |-> <>(events)
1354 |-> [](continue) 1415 |-> [](continue)
1355 <>events, <>(continue until Q)) 1416 <>events, <>(continue until Q))
1356 Ȥ褦compile롣դࡣ 1417 というようにcompileする。ふむ。
1357 1418
1358 l(P) & Q l(P) = LTTL formula of P 1419 l(P) & Q l(P) = LTTL formula of P
1359 <>(P) -> <>(P,<>(l(Q))) 1420 <>(P) -> <>(P,<>(l(Q)))
1360 [](P) -> P until l(Q) 1421 [](P) -> P until l(Q)
1361 1422
1364 1425
1365 Reverse Specification 1426 Reverse Specification
1366 1427
1367 R -> +(R) -(R) on Start Time 1428 R -> +(R) -(R) on Start Time
1368 1429
1369 empty(R) hidden ɡ+R/-R ˴ؤƤƱ 1430 empty(R) は hidden だけど、+R/-R に関しては同期する
1370 ޤɤʬʤ 1431 ここがまだ良く分からない。
1371 1432
1372 Modelľܹʤfiltrationΰ̣Ǥ...礭뤫顣 1433 Modelを直接構成しない。filtrationの意味でも...大きすぎるから。
1373 ꡢModel constraint롣 1434 その代わり、Model constraintを構成する。
1374 1435
1375 Generating C / In-kernel implementation 1436 Generating C / In-kernel implementation
1376 1437
1377 Wed Oct 5 15:30:19 JST 1994 1438 Wed Oct 5 15:30:19 JST 1994
1378 1439
1545 status(a)-> ... ; status(b)-> ... status(f)-> .. ; status([])-> ... 1606 status(a)-> ... ; status(b)-> ... status(f)-> .. ; status([])-> ...
1546 generate n+1. 1607 generate n+1.
1547 1608
1548 Tue Sep 15 13:04:43 JST 1992 1609 Tue Sep 15 13:04:43 JST 1992
1549 1610
1550 ɡRegular variable state ͭʤȼ«ʤ 1611 結局、Regular variable state を共有しないと収束しないし、
1551 ͭǤ뤫ɤȽǤŪ顢ˡǤ 1612 共有できるかどうかの判断は大域的だから、この方法では
1552 Ǥʤ餷 1613 できないらしい。
1553 1614
1554 Tue Sep 15 11:36:36 JST 1992 1615 Tue Sep 15 11:36:36 JST 1992
1555 1616
1556 Regular variable must be non-deterministic. 1617 Regular variable must be non-deterministic.
1557 ^r 1618 ^r
1589 itl:3 [more,down(r,1),~down(r,0)]]-> stay(r,1);(stay(r,3)&^r),not(stay(r,3)) 3 1650 itl:3 [more,down(r,1),~down(r,0)]]-> stay(r,1);(stay(r,3)&^r),not(stay(r,3)) 3
1590 stay(2,1),stay(4,3) 1651 stay(2,1),stay(4,3)
1591 1652
1592 Mon Sep 14 00:25:08 JST 1992 1653 Mon Sep 14 00:25:08 JST 1992
1593 1654
1594 ^r automatonϡ^r̤ѿȸtableau 1655 ^r で生成されるautomatonは、^rを普通の変数と見て生成するtableauの
1595 subsetǤ롣äơtableaunodeؤȤ ^r Υǥ 1656 subsetである。従って、tableauのnodeを指し示すことで ^r のモデルを
1596 뤳Ȥ롣ޤʤ... 1657 作ることが出来る。しかし、うまくいかない...
1597 1658
1598 (^r & true),not(^r) ΥǥϤʤ 1659 (^r & true),not(^r) のモデルはないから
1599 1660
1600 ǡstay(r,N)Ȥ (up(r),emtpy & true & down(r),empty) ǤϤᡣ 1661 そこで、stay(r,N)を使う (up(r),emtpy & true & down(r),empty) ではだめ。
1601 ^r & ^r -> ^r ˤʤäƤޤ顣 1662 ^r & ^r -> ^r になってしまうから。
1602 1663
1603 ȥǥ빽ۤ«ʤ --> Full ITL 1664 するとモデル構築が収束しない --> これは Full ITL だから
1604 1665
1605 RITLΥǥͭ¤ stay(r,N)Τʤʬ 1666 しかしRITLのモデルは有限だから stay(r,N)のかなりの部分は
1606 ߤɤɤȽǤ뤫ꡣ 1667 相互に等しい。等しいかどうかをどう判断するかが問題。
1607 1668
1608 Deterministic PathƱstateȽǤΤǤ­ʤ 1669 Deterministic Pathが等しければ同じstateと判断するのでは足りない
1609 Loopʤ顣 1670 Loopが作れないから。
1610 1671
1611 ष٤ΤDefaultǡɬפʻʬΥΤ˾ޤ 1672 むしろすべて等しいのがDefaultで、必要な時だけ分離するのが望ましい
1612 1673
1613 Mon Jan 1 11:05:38 JST 1990 1674 Mon Jan 1 11:05:38 JST 1990
1614 1675
1615 ^r & ^r 1676 ^r & ^r
1616 itl:0 [empty,up(r),down(r)] -> empty 1677 itl:0 [empty,up(r),down(r)] -> empty
1936 [p,~q] -> [0]true +[~0,1]@true +[~0,~1]@~(true & q) 1997 [p,~q] -> [0]true +[~0,1]@true +[~0,~1]@~(true & q)
1937 [~p] -> []true 1998 [~p] -> []true
1938 a path must not contain false eventuality 1999 a path must not contain false eventuality
1939 2000
1940 2001
1941 iΤϼ&ο 2002 iのは式の中の&の数に等しい
1942 2003
1943 empty 2004 empty
1944 0 true 2005 0 true
1945 ~0 false 2006 ~0 false
1946 ~empty 2007 ~empty