|
22
|
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
|
|
19
|
62 Sun Feb 10 21:30:04 JST 2002
|
|
|
63
|
|
22
|
64 あ、そうだよ。empty は、どうすんだ? kiss の時は、無視したんだが...
|
|
|
65
|
|
|
66 そもそも、2nd order を入れたおかげで、複雑になりすぎ。
|
|
|
67
|
|
|
68 もう一度 simple なversion を作るべきだよね。
|
|
|
69
|
|
|
70 状態生成を再利用できる形で。
|
|
|
71
|
|
|
72 対称性 general abstraction
|
|
19
|
73
|
|
|
74 Thu Feb 7 12:12:21 JST 2002
|
|
|
75
|
|
|
76 Verlog output for Prof. Fujita
|
|
|
77
|
|
22
|
78 switch でもいいんだけど、ちょっと巨大にならない?
|
|
19
|
79
|
|
|
80 module check001(clk,inputs..,outputs...)
|
|
|
81 input clk;
|
|
|
82 input inputs;
|
|
|
83 output outputs;
|
|
|
84 reg state;
|
|
|
85 initial state = 0;
|
|
|
86 always @(posedge clk) begin
|
|
|
87 case (state)
|
|
|
88 0: if (inputs condtion) begin
|
|
|
89 outputs set
|
|
|
90 end else if (inputs condtion) begin
|
|
|
91 outputs set
|
|
|
92 ...
|
|
|
93 end
|
|
|
94 endcase
|
|
|
95 end
|
|
|
96 endmodule
|
|
|
97
|
|
22
|
98 ってな感じ?
|
|
|
99
|
|
|
100 やっぱり、状態をcubeのような形で生成するのは、良くないよね。
|
|
19
|
101 ?(a,@a,@b)
|
|
22
|
102 みたいな形で、生成した方が扱いやすい。ま、それは、Java Version
|
|
|
103 で。
|
|
|
104
|
|
|
105 特性方程式を生成する方が良い? BDD の末端が各状態にいくようにする。
|
|
|
106 それは、あんまり良くないか...
|
|
19
|
107
|
|
16
|
108 Sun Jan 21 00:42:39 JST 2001
|
|
|
109
|
|
22
|
110 あれ? やっぱり、なんか変だな。
|
|
16
|
111 | ?- ex(finite & empty).
|
|
|
112
|
|
|
113 state(1 , not(true&false)&empty)
|
|
|
114 [][empty]->empty
|
|
|
115 [][more]->1
|
|
|
116
|
|
|
117 0.019000000000005457 sec.
|
|
|
118 1 states
|
|
|
119 2 subterms
|
|
|
120 2 state transions
|
|
|
121 verbose,renaming,singleton,length limit 5
|
|
|
122 valid
|
|
|
123
|
|
|
124 yes
|
|
|
125 | ?- infinite.
|
|
|
126 satisfiable in infinite interval:
|
|
|
127 *
|
|
|
128 0: 1
|
|
22
|
129 では、困ります。それに、
|
|
16
|
130 <>(p) = finite & p
|
|
22
|
131 に書き換えないといけないみたいね。
|
|
|
132
|
|
|
133 ってことは、やはり、
|
|
|
134 その状態から、唯一、more にだけ抜ける状態
|
|
|
135 なのかな。
|
|
16
|
136
|
|
15
|
137 Sat Jan 20 20:50:17 JST 2001
|
|
|
138
|
|
22
|
139 true をloopとみなしてないので、ex(true) で、infinite
|
|
|
140 が satisfiable にならない。
|
|
|
141
|
|
|
142 infinite で、loop を * で明示するようにした。
|
|
16
|
143
|
|
14
|
144 Sat Jan 20 18:16:33 JST 2001
|
|
|
145
|
|
22
|
146 とりあえず、more_only は、more にいくものが何かあれば許すと言うことに
|
|
|
147 しました。
|
|
14
|
148
|
|
12
|
149 Sat Jan 20 03:38:14 JST 2001
|
|
|
150
|
|
22
|
151 demo(15) の infinite が止まらない。loop detection の計算量が
|
|
|
152 多すぎるようですね。
|
|
|
153
|
|
|
154 失敗したのを覚えておいてということだと、repeat fail loop
|
|
|
155 で回すわけにはいきませんね。
|
|
12
|
156
|
|
|
157 Sat Jan 20 02:33:17 JST 2001
|
|
|
158
|
|
22
|
159 本当に、more_only(S) で判断してしまって良いのか?
|
|
|
160
|
|
|
161 inifinite-> の問題もあるし...
|
|
|
162
|
|
|
163 ある特定のinifinite state sequence で、ITL式が satisfiy される
|
|
|
164 ことを ω-interval satisfiability って言うんじゃないの?
|
|
|
165
|
|
|
166 だとすると、
|
|
|
167 その状態から、唯一、more にだけ抜ける状態
|
|
|
168 であれば良いのか? でも、more/empty でいきなり分類してしまっているので、
|
|
|
169 それは、それほど簡単に判断できないかな。ITL式はあるんだから、
|
|
|
170 more を付け加えて展開すれば良いのだけど...
|
|
|
171
|
|
|
172 non-determistic に empty に落ちる物は、~(<>empty) になり得ないので
|
|
|
173 まずい。
|
|
12
|
174
|
|
|
175 13:+ac-bc-cc-dc 183
|
|
|
176 14:-ac-bc-cc+dc 185
|
|
|
177 15:-ac-bc-cc+dc 186 <----
|
|
|
178 16:+ac-bc-cc-dc 187
|
|
|
179 17:+ac-bc-cc-dc 191
|
|
|
180 18:+ac-bc-cc-dc 194
|
|
|
181 19:-ac+bc-cc-dc 198
|
|
|
182 20:-ac-bc+cc-dc 201
|
|
|
183 21:+ac-bc-cc-dc 202
|
|
|
184 22:+ac-bc-cc-dc 203
|
|
|
185 23:+ac-bc-cc-dc 207
|
|
|
186 24:-ac+bc-cc-dc 211
|
|
|
187 25:-ac-bc+cc-dc 213
|
|
|
188 26:+ac-bc-cc-dc 214
|
|
|
189 27:+ac-bc-cc-dc 218
|
|
|
190 28:+ac-bc-cc-dc 221
|
|
|
191 29:-ac+bc-cc-dc 226
|
|
|
192 30:-ac-bc+cc-dc 186
|
|
|
193
|
|
22
|
194 おぉ!
|
|
12
|
195
|
|
10
|
196 Fri Jan 19 20:59:46 JST 2001
|
|
|
197
|
|
|
198 | ?- ex((infinite -> @infinite)).
|
|
|
199
|
|
|
200 state(1 , not(true&false),@ (true&false))
|
|
|
201 [][empty]->empty
|
|
|
202 [][more]->true
|
|
|
203
|
|
|
204 0.021000000000000796 sec.
|
|
|
205 1 states
|
|
|
206 2 subterms
|
|
|
207 2 state transions
|
|
|
208 verbose,renaming,singleton,length limit 5
|
|
|
209 valid
|
|
|
210
|
|
|
211 yes
|
|
|
212 | ?- infinite.
|
|
|
213 unsatisfiable in infinite interval.
|
|
|
214
|
|
22
|
215 これは... どういうことなんでしょうね? inifite は基本的に
|
|
|
216 false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable
|
|
|
217 だね。
|
|
10
|
218
|
|
|
219 Fri Jan 19 20:40:37 JST 2001
|
|
|
220
|
|
22
|
221 割りと簡単なアルゴリズムで、satisfiabilityは、チェック
|
|
|
222 できました。これが、正しいかどうかは Moszkowski によるけど...
|
|
10
|
223 inifnite
|
|
|
224 *skip
|
|
|
225 *((skip&skip))
|
|
22
|
226 などに関しては、うまく動くようですね。
|
|
|
227
|
|
|
228 vailidity checker が欲しい所だけど... どういうものがvalidなのかは、
|
|
|
229 良くわからない。もちろん、否定が unsatisfiable ならば、valid なの
|
|
|
230 だが。
|
|
|
231
|
|
|
232 でも、この方法だと、
|
|
|
233 satisfiable in ω-interval implies
|
|
10
|
234 falsifiable in finite interval
|
|
22
|
235 ってことになるらしい。
|
|
10
|
236
|
|
6
|
237 Fri Jan 19 07:48:59 JST 2001
|
|
|
238
|
|
22
|
239 Streett ∩_i []<>L_i ⊃ <>[]U _i
|
|
|
240 Rabin ~(∩_i []<>L_i ⊃ <>[]U _i)
|
|
|
241
|
|
|
242 という構造を持っている。これは、
|
|
|
243 ある無限回繰り返す所 L から先は、いつか、ずーっと U を通るようになる
|
|
|
244 のと、その否定という構造になっている。これを、
|
|
|
245 labeled tree の、ある所から先は、ずーっと「あるマークがついている」ループ
|
|
|
246 で表す。
|
|
|
247
|
|
|
248 で、そのアルゴリズムだけど...
|
|
|
249
|
|
|
250 depth first に「出口の無いノード」を探す。そこをマークする。そこから、
|
|
|
251 ノードを覚えながら、出口の無いノードを手繰る。ループが出て来たら検出
|
|
|
252 完了。最後までいったら、マークに戻り、次の出口の無いノードを探す。
|
|
|
253 これをdepth first search が終るまで繰り返す。したがって、計算量は、
|
|
|
254 ノード数N に対して、最悪 N^2/2 ( N+(N-1)+(N-2)...1 ) である。それほど
|
|
|
255 悪くは無いか。
|
|
6
|
256
|
|
|
257 Fri Jan 19 04:27:42 JST 2001
|
|
|
258
|
|
22
|
259 えーと、LICS のpaper は、やたら複雑だが、要は、ω-automatonの
|
|
|
260 否定の問題だよね。だから、false loop detection が、ちゃんと、
|
|
|
261 ITL の否定の定義に一致していることさえ見れば良い。
|
|
|
262
|
|
|
263 finite interval では、既に一致しているわけだから、(true & false )
|
|
|
264 のsatisfiabilityの定義を無理して一致させる必要は無い。一致しなければ、
|
|
|
265 異なるaxiomatiazation を見つけたことになる。だから、false loop
|
|
|
266 detection が negetation consistent ならば、たぶん、一致するんだろう。
|
|
|
267
|
|
|
268 結局は、Rabin automatonのacceptabilityをチェックすることになるんだろう。
|
|
|
269 ってことは、non deterministic buchi automaton を扱うってことか。
|
|
6
|
270
|
|
|
271 Rabin <-> Streett complimentary
|
|
|
272
|
|
22
|
273 (true & false)に関しては、<>[](not_empty) だよな。
|
|
6
|
274 infinite -> <>[](more)
|
|
|
275
|
|
22
|
276 ってことは... やっぱり、false_loop detection でいいんじゃないかなぁ。
|
|
|
277
|
|
|
278 えーと、
|
|
|
279 すべてのterminating loop で、empty->true がない => infinite
|
|
|
280 だから、ω区間で充足ってのは、
|
|
|
281 terminating loop に empty->trueがないものがある
|
|
|
282 だから、ω区間で恒真ってのは、
|
|
|
283 terminating loop に empty->trueがない
|
|
|
284
|
|
|
285 となる。その否定を取ると、true/false が逆転する。(のか?)
|
|
|
286
|
|
|
287 しかし、terminating loop でなくても、ω区間を実現することはできる。
|
|
6
|
288 infinite & P -> infinite
|
|
22
|
289 だから。この場合も充足っていうんだろうな。この場合は、どうせ P
|
|
|
290 は、tableau で無視されるので問題無い。
|
|
|
291
|
|
|
292 って、ことは、terminating loop だけを見ればよろしい。
|
|
|
293
|
|
|
294 execution example は、
|
|
6
|
295 s s s s s s (s s s s s s)*
|
|
22
|
296 という形を取る。なので、必ず最小モデルの性質を持つ。
|
|
|
297 実際には、* の中は、非決定的で良い。
|
|
6
|
298
|
|
|
299
|
|
5
|
300 Fri Jan 19 02:18:39 JST 2001
|
|
|
301
|
|
22
|
302 <>empty と infinite = (true & false ) は、両立しない。
|
|
5
|
303 <>empty = finite & empty = ~(true & false) & empty
|
|
|
304
|
|
22
|
305 ~(true & false ) はなにを示しているかと言うと...
|
|
|
306 いつでも「終れる」ということ。infinite は、「終れない」
|
|
|
307
|
|
|
308 ω区間には、empty exit は存在できない。正確には、
|
|
5
|
309 ... [ no-empty loop ] ....
|
|
22
|
310 ということ。そういうsub 区間があれば良い。
|
|
|
311
|
|
|
312 [](more) は? もちろん、これは、Lite では、false.
|
|
5
|
313 ~(finite & ~more)
|
|
|
314 ~(~(true & false) & ~more))
|
|
|
315 ~(~(true & false) & empty))
|
|
22
|
316 これが ω区間で true になるためには...
|
|
|
317
|
|
|
318 []のinifinite versionは?
|
|
4
|
319
|
|
|
320 http://research.commpaq.com/SRC/esc/
|
|
|
321
|
|
|
322 Fri Jan 19 01:20:54 JST 2001
|
|
|
323
|
|
22
|
324 ω区間は、必ず、(s_n...s_m)* を含む。decidableならば、そうだ。
|
|
|
325 が、それは、証明が必要がだけど。
|
|
|
326
|
|
|
327 逆に、(s_n...s_m)* を含めば、そこをずーっと繰り返すことにより、
|
|
|
328 ω区間を実装できる。だから、そういうループを見つければ、
|
|
|
329 ω区間上で satisfiable だということができる。
|
|
|
330
|
|
|
331 その区間上で、∨empty のようなexitが許されるのか? たぶん、
|
|
|
332 許されない。ということは、やはり、false loop を見つければ
|
|
|
333 良いと言うことか。
|
|
|
334
|
|
|
335 そのアルゴリズムは?
|
|
|
336
|
|
|
337 ω区間では、empty で抜け出ることができない。->
|
|
|
338 <>empty がfalse
|
|
|
339 どうも正しそうだな。
|
|
|
340
|
|
|
341 えーと、何か、安全なアルゴリズムがありそうだけど...
|
|
|
342 簡単なのは、すべてのループをdepth first で探すことだな。
|
|
|
343
|
|
|
344 とすると、finitarity をチェックするのは結構面倒になる。
|
|
|
345
|
|
|
346 finitarity とはなに?
|
|
|
347 ループには必ずtrue exitがある
|
|
|
348 infiniteness とは、
|
|
|
349 exit のないループがある
|
|
|
350
|
|
|
351 []<>(p) = <>[](p) は、どうなるんだろう?
|
|
5
|
352 <>(p) = finite & p
|
|
|
353 ~(finite & ~(finite & p)) = finite & ~(finite & ~p)
|
|
22
|
354 ですか。
|
|
5
|
355
|
|
|
356
|
|
4
|
357 Fri Jan 19 00:33:43 JST 2001
|
|
|
358
|
|
22
|
359 えーと、
|
|
4
|
360 [](false)
|
|
22
|
361 がsatisfiableになることはない。
|
|
4
|
362 ~(true & ~ false)
|
|
|
363 ~(true & true)
|
|
22
|
364 だから。
|
|
4
|
365 true & ~true
|
|
22
|
366 は、許される。しかし、
|
|
4
|
367 ~true & ~true
|
|
22
|
368 は許されない。これ自体は、今のverifier でも、そうなる。
|
|
|
369
|
|
|
370 tableau expansion 自体は同じだと考えて良いのか?
|
|
|
371 特に異なる inference rule があるわけではないらしい。
|
|
|
372
|
|
|
373 だとすれば、必要なコードは、false loop detector だけか?
|
|
|
374 exe/diag の代りに、infinite_exe,infinite_diag を作るのだろうか。
|
|
|
375
|
|
|
376 infinite_exe は、ループを表示しなければならない。必ず、
|
|
|
377 そのようなループが存在するのだろうか? とすると、infinite
|
|
|
378 interval は、prefix のようなものになる。実は、prefix
|
|
|
379 がinfinite interval そのもの? prefix(finite,....)
|
|
|
380 みたいなものだね。これは、どっかで見たことが...
|
|
4
|
381
|
|
|
382
|
|
2
|
383 Thu Jan 18 22:42:24 JST 2001
|
|
|
384
|
|
|
385 | ?- ex(((true&false)->(<>(empty)))).
|
|
|
386
|
|
22
|
387 は、valid になってしまう。実際には、infinite->not(<>(empty)).
|
|
2
|
388
|
|
|
389 Thu Jan 18 21:04:13 JST 2001
|
|
|
390
|
|
22
|
391 まず、chop.pl の中の、X & false をfalseに変換しているのを
|
|
|
392 抜く必要がある。
|
|
2
|
393
|
|
|
394 Thu Jan 18 19:59:33 JST 2001
|
|
|
395
|
|
|
396 in POPL01
|
|
|
397
|
|
22
|
398 LICS00 の infinite を入れるように Lite を拡張することが
|
|
|
399 できるのか?
|
|
|
400
|
|
|
401 単純な拡張にはならない。
|
|
2
|
402 infinite =def (true & false )
|
|
22
|
403 だから。これは、今の実装では unsatisfiable。
|
|
|
404
|
|
|
405 P&Q で、Q が単純にfalseだからといって、諦められない。今は、node は、
|
|
2
|
406 empty,false
|
|
|
407 empty,true
|
|
|
408 more,false
|
|
|
409 more,some_other
|
|
22
|
410 というように特徴付けられている。これで足りるのか?
|
|
|
411
|
|
|
412 Eventurality check が必要無いと良いんだけど。
|
|
|
413
|
|
|
414 Rabin automaton ってなんだ? Buchi と同じなんじゃないの?
|
|
|
415
|
|
|
416 true & false は、
|
|
2
|
417 empy -> false
|
|
|
418 more -> true & false
|
|
22
|
419 に展開される。今は、empty だけを見て、validity/satisfiability を
|
|
|
420 調べている。しかし、これを、
|
|
|
421 「ある特定のfalse exit ループをsatisfiableだとみなす」
|
|
|
422 ことにより、infinite interval を導入することができる。
|
|
|
423
|
|
|
424 問題は、どのような false exit ループが satisfiable だという
|
|
|
425 こと? というよりは、これで unsatisfiable になる formulaって
|
|
|
426 何?
|
|
2
|
427 more -> false
|
|
22
|
428 のたぐいだけか?
|
|
2
|
429 finite
|
|
|
430 empy -> true
|
|
|
431 more -> true & true
|
|
22
|
432 は、どうなる?
|
|
2
|
433 ~infinite
|
|
|
434 empy -> true
|
|
|
435 more -> ~(true & false)
|
|
22
|
436 となる。なので、これは finite に等しい。
|
|
|
437
|
|
|
438 infinite は、false loop を表していると考える。
|
|
|
439
|
|
|
440 全ての式Pを、finite -> P で、チェックすれば、finite LITL になる。
|
|
|
441 (ならなければいけない)
|
|
|
442
|
|
|
443 って、ことは、false loop をdetectすれば良いだけか? これは、
|
|
|
444 結構易しいが、計算量的には、ちょっと大変かな。
|
|
2
|
445 finitely
|
|
|
446 valid, satisfiable, unsatisfiable...
|
|
|
447 inifinitly
|
|
|
448 valid, satisfiable...
|
|
22
|
449 infinitely satisfiable とは、
|
|
|
450 flase loop が存在すること
|
|
|
451 valid は、
|
|
|
452 false loop 以外は、empty false であること(?)
|
|
|
453
|
|
|
454 えーと、それだと、inifinitly satisiable な式は、finitly unsatisfiable
|
|
|
455 だけど、それでいいの? だとすると、valid な式はなくなってしまうね。
|
|
|
456
|
|
|
457 これは、ちょっとうれしくないであろう。ということは、
|
|
|
458 infinitely valid は、
|
|
|
459 false loop 以外は、empty ture であること(?)
|
|
|
460 を含むと考えるのが正しい。だとすると、
|
|
2
|
461 |= finitie /\ finite
|
|
22
|
462 ってことになるね。それは、ちょっとうれしくないか。
|
|
|
463
|
|
|
464 うーむ、Moszkowski は、どういう選択をしたんだろう?
|
|
2
|
465
|
|
|
466
|
|
|
467 Wed Nov 22 16:27:45 JST 1995
|
|
|
468
|
|
22
|
469 rstd 側で limit を扱うことにする。
|
|
|
470 rename_list でlimitを指定することになる。singleton のlimit
|
|
|
471 をはずさないといけないだろう。over(r,N)が外にでないのが
|
|
|
472 ちょっと情報不足だな。
|
|
|
473
|
|
|
474 itlstd が idempotent になってなーい!!! しくしく。
|
|
|
475 itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) でY=Y1になる
|
|
|
476 はずなのだが...
|
|
|
477
|
|
|
478 itlstd2 では、singleton remove, renaming は行なわないで、limit over
|
|
|
479 だけを取り扱う。これによってdetailed trace が可能となる。これに、
|
|
|
480 従来のitlstdをかければ、もとに戻るはずだ。が、どうも失敗している
|
|
|
481 らしい。
|
|
2
|
482
|
|
|
483 Tue Nov 21 18:33:19 JST 1995
|
|
|
484
|
|
22
|
485 renaming の trace は original limit で行なう。
|
|
|
486 detailed trace は no limit で行なう。
|
|
|
487 itl/5 は2度呼ばれるが、まあ、良とするか。
|
|
|
488
|
|
|
489 rstd 側でlimitの置き換えをすればだいぶましなんだが...
|
|
|
490
|
|
|
491 renmaing で、over limit を取り扱う方が統一的か。
|
|
2
|
492
|
|
|
493 Wed Nov 15 12:58:28 JST 1995
|
|
|
494
|
|
22
|
495 over(r,N) が true/false に置き換わっていて、unifyするか?
|
|
|
496
|
|
|
497 いずれにせよ、ちょっと気まずい。どの変数が置き換わるかは、
|
|
|
498 renaming を trace すれば分かるが...
|
|
|
499
|
|
|
500 この置き換えをrstd側で行なって、original/restrictedの両方を
|
|
|
501 とっておく。そして、どの変数が置き換わったか分かるようにする。
|
|
|
502 (renaming informationに入れておく) でも、この情報もどうせ
|
|
|
503 lazyに生成するんだよね? なんか変だ。
|
|
|
504
|
|
|
505 あるいは、detailed traceの方では置換えしない? true/false に
|
|
|
506 置き換えても同じstateで実現できるはず。だが、unify はしないと
|
|
|
507 いけない。
|
|
|
508
|
|
|
509 いずれにせよ、lazy state generation では、
|
|
2
|
510 full trace, restricted trace
|
|
22
|
511 の両方をおこなう。このためには、over の置き換えをrstd で行なった
|
|
|
512 方が良いだろう。
|
|
|
513
|
|
|
514 うーむ、でも、そうすると、itlstd がnon-deterministic になって
|
|
|
515 しまう。それは、いまいちだ。
|
|
2
|
516
|
|
|
517 Tue Nov 14 19:56:26 JST 1995
|
|
|
518
|
|
22
|
519 Detailed trace の時は Fromula と state number と両方持ち歩かないと
|
|
|
520 だめだ。
|
|
|
521
|
|
|
522 ということは、diag routine を書き直さないとダメか。ndcomp は
|
|
|
523 あきらめるか?
|
|
2
|
524
|
|
|
525 Mon Nov 13 22:33:34 JST 1995
|
|
|
526
|
|
22
|
527 trace するときにrenaming は、いらないんじゃない?
|
|
|
528 detailed traceをどうせ使うとすれば... そうすれば、
|
|
|
529 choice も考えなくても良い。
|
|
2
|
530
|
|
|
531 Sun Nov 12 23:37:36 JST 1995
|
|
|
532
|
|
22
|
533 ^r のtrace
|
|
|
534
|
|
|
535 stateは決まっている
|
|
|
536 duplicated は rename inforamtion を使ってtrace できる。
|
|
|
537
|
|
|
538 detailed expansion して、unify する。具体的には、
|
|
|
539 BDDにそって分解する。これによって、true_false がr^nの
|
|
|
540 treeに展開されるはず。されなければ、別のものを探す。
|
|
|
541
|
|
|
542 true_falseのchoiceによって値が異なるわけだけど...?
|
|
|
543 choice は、一つのBDDに関して一つしかでない。(leafにしかない
|
|
|
544 から) ということは、複数のchoice は、
|
|
|
545 異なる & の empty
|
|
|
546 でしか起きない。なんらかのidentityを残した方がいいんだけど。
|
|
|
547 ま、結果的に同じstateにいって、すべての条件が尽くされるなら、
|
|
|
548 構わないか。detailed expansion はすべてを含んでいるのだから、
|
|
|
549 構わないはず。
|
|
|
550
|
|
|
551 まずは、renaming のカタをつけよう。
|
|
|
552
|
|
|
553 もっと選択的に^rをトレースした方が良くない? singleton ^r
|
|
|
554 をなんらかのtermにマップできなものか?
|
|
2
|
555
|
|
|
556 Sat Nov 11 09:55:41 JST 1995
|
|
|
557
|
|
22
|
558 2path singleton removal がようやっとできた。
|
|
|
559 ただし、どうも、order sensitive なんだよな。over が@<,@>に
|
|
|
560 よってでる時とでない時がある。
|
|
|
561
|
|
|
562 sbdt_split, sbdt_ife によってremoval/renameによるorderを修正しない
|
|
|
563 といけなかった。やむをえないところか?
|
|
|
564
|
|
|
565 しかしsingleton removalを書いたら、もとの方も良くなってしまった。
|
|
|
566 どうも、bdt routineには問題があったみたい。true & true を除く
|
|
|
567 ようにしたのが効いたとも思えないんだが.... sbdt_opt のせいか?
|
|
|
568
|
|
|
569 state numberがでなくなるbugを直した
|
|
|
570
|
|
|
571 あとは、trace の問題だな。r^nの実行がちゃんとトレースできると
|
|
|
572 いいんだけど。
|
|
2
|
573
|
|
|
574 Thu Nov 9 12:03:32 JST 1995
|
|
|
575
|
|
22
|
576 P & Q を、sb(P_BDD & Q_BDD) という形で持っているけど..
|
|
2
|
577 sb(P_BDD,PN)
|
|
|
578 sb(Q_BDD,QN)
|
|
22
|
579 PN & QN という方が良くない? ほとんど同じだとは思うけど....
|
|
|
580 ?(PN & QN,true,false) となるのか.... うーん。
|
|
|
581
|
|
|
582 Qの展開を一回に抑えられない? ? を未展開のマークに
|
|
|
583 使えないか?
|
|
2
|
584
|
|
|
585 Wed Nov 8 20:31:23 JST 1995
|
|
|
586
|
|
22
|
587 はやり一旦BDDに落して2pathで処理することとする。
|
|
|
588
|
|
|
589 first path: singleton varble の detect
|
|
|
590 (regular variableがない場合は、そのままstd_check
|
|
|
591 singleton removal で消えることはない)
|
|
|
592 regular variable が無ければ、これで終了
|
|
|
593 rename list を計算
|
|
2
|
594 second path path:
|
|
22
|
595 singleton variable があった場合、
|
|
|
596 t/fのtree を parallel traverse
|
|
|
597 t/f または、[tf]/tf の組合せをtfに置き換える
|
|
|
598 複数のsingleton variableを順不同に処理して良い
|
|
|
599
|
|
|
600 regular variable があるかどうかは、singleton removval の
|
|
|
601 結果に依存するので、1path で厳密に取り除くことはできない。
|
|
|
602 が、2nd path では確実に取り除くことが出来る。
|
|
|
603
|
|
|
604 ぶぶ、2nd pathは全然処理が違う!! sbdt と共用はできない
|
|
2
|
605
|
|
|
606 Tue Nov 7 15:45:07 JST 1995
|
|
|
607
|
|
22
|
608 chop のレベルで分ければ、まあ、良い。問題は、そのあと。と、
|
|
|
609 考えると、BDDに変換するレベルで対応する方が望ましいかも知れない。
|
|
|
610 もちろん、今のままでもsafeなんだけど、落ちているものが多い。
|
|
|
611 それは結果的に状態を増やしていることになる。
|
|
|
612
|
|
|
613 一つの方法は、
|
|
2
|
614 p(^r) => ?(^r,pt,pf)
|
|
22
|
615 とする。
|
|
2
|
616 (pt,pf; tf), (pt;pf)
|
|
22
|
617 と変形する。と、こんな具合。これは重いなぁ。
|
|
|
618
|
|
|
619 (~ ^r), ^r がボトムアップではfにならない。ま、そういうことなんだよな。
|
|
2
|
620
|
|
|
621 Tue Nov 7 10:38:59 JST 1995
|
|
|
622
|
|
22
|
623 どうも、singleton removal だと、[a](^r = length(2)), f(^r)
|
|
|
624 のようなものは完璧にトレースできるらしい。
|
|
|
625 [a](^r = length(2)), *(^r) もOk だった。
|
|
|
626
|
|
|
627 でも、さすがに文法記述は発散する。
|
|
|
628
|
|
|
629 結局、どういう制限なのかなぁ? diag 時に、full trace できたかどうかを
|
|
|
630 チェックするか...
|
|
|
631
|
|
|
632 どうも、シングルトンチェックが甘いな。もっと、ちゃんとチェックする
|
|
|
633 ためには?
|
|
2
|
634
|
|
|
635 Mon Nov 6 15:57:46 JST 1995
|
|
|
636
|
|
22
|
637 [p_0,p_1,...,p_n] は、
|
|
2
|
638 p_0,p_1,...,p_n -> true
|
|
|
639 ~ p_0,~ p_1,...,~ p_n -> false
|
|
|
640 else -> true_false
|
|
22
|
641 という形でBDD(MTBDD)になる。3値論理
|
|
2
|
642
|
|
|
643 ^r -> true_false
|
|
|
644
|
|
|
645 true_false -> empty? choice ? true : fals
|
|
|
646 : true_false
|
|
|
647
|
|
|
648 t,tf -> tf
|
|
|
649 t;tf -> t
|
|
|
650 tt;tf -> tf
|
|
|
651 f,tf -> f
|
|
|
652 f;tf -> tf
|
|
|
653 tt,tf -> tf
|
|
|
654
|
|
22
|
655 (あれ、cross termは?)
|
|
|
656 確かにこれでうまくいきます。はい。* ^r も完璧。
|
|
|
657
|
|
|
658 問題は、実行をtraceできるかどうかだな。
|
|
2
|
659
|
|
|
660 Mon Nov 6 08:50:01 JST 1995
|
|
|
661
|
|
22
|
662 singleton の効果は有限か?
|
|
|
663
|
|
|
664 BDDの中でsingleton duplicate を許すとすると、これは止まるのか?
|
|
2
|
665 selection(uniq set of subterm)
|
|
22
|
666 という形になるはず。だから、とまるはず。subtermは有限。singleton には、
|
|
|
667 R名による区別さえ必要無い。
|
|
2
|
668 ^r -> ^([false,true])
|
|
|
669 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
|
|
22
|
670 という展開になる? 再sortは必要。
|
|
|
671
|
|
|
672 一般的に、^(r,[p_0,p_1...p_n]) という形で収束しないの? r が一つだったら...
|
|
|
673 ネストしたらout。でもnestはあっても固定だから。
|
|
|
674
|
|
|
675 が、これでcomputationをトレースできるのか? いや、特別な展開が必要。
|
|
|
676
|
|
|
677 あと、determinization しないとね。(どうやって?)
|
|
2
|
678 ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n])
|
|
22
|
679 の際に、px_0 には next のみが入る。そうすれば良い。
|
|
2
|
680 itl(p_0,more,..)
|
|
22
|
681 での出力はnext,true,false。Ok。
|
|
2
|
682
|
|
|
683 Sun Nov 5 21:34:33 JST 1995
|
|
|
684
|
|
22
|
685 しかし、なんと * ^R は非常に大きな状態を生成する。
|
|
|
686 ^R と true & ^R の干渉が大きな状態を生成してしまう。(らしい)
|
|
|
687 これを抑えるには? 一つはlength で頭を抑えることだな。
|
|
|
688 ああ、でも、やっぱり大きいか。あんまり、うまくない。
|
|
|
689 length(10) でも結構巨大か..
|
|
|
690
|
|
|
691 proj でも同じような問題はあったのだけど...
|
|
|
692
|
|
|
693 ^r の permuation の対称性を何とかしない限りだめだね。
|
|
|
694 しかし、順序は変えちゃダメなんでしょう? うーむ。
|
|
|
695 でもさ、モデル自身は小さいんだが.... うーむ。
|
|
|
696
|
|
|
697 いや、この場合は singleton removal が効くみたい。そうか。
|
|
|
698
|
|
|
699 これはsingleton の処理が正しくないからじゃない?
|
|
|
700
|
|
|
701 singleton の効果は有限か?
|
|
2
|
702 f(r^1,....r^n) -> exists
|
|
22
|
703 だとすれば有限。だけど、固定してはだめ。
|
|
2
|
704 r^s ? length(1) : r^s ? length(2) : ....
|
|
22
|
705 となりうる?
|
|
2
|
706
|
|
|
707 Wed Nov 1 21:12:04 JST 1995
|
|
|
708
|
|
22
|
709 例題ねー... しかし、<>^R が使えないとなると....
|
|
|
710 あ、でも、* ^R は使える。
|
|
2
|
711
|
|
|
712 Mon Oct 16 16:05:31 JST 1995
|
|
|
713
|
|
22
|
714 LITL で、closure, proj 抜きだとpolynominal orderの方法がある!?
|
|
2
|
715 ~(....&....(...&... ~(...&....)))
|
|
22
|
716 という形で、これにvariable patternを埋め込んでいけば良い。これだと
|
|
|
717 marking だから state space database はいらない。
|
|
|
718
|
|
|
719 tableau expansion でも、生成される状態は同じ数だから結果的にpolynominal
|
|
|
720 になっていたのかも.... たしかに、quantifier, closure, proj を入れると
|
|
|
721 verification は難しくなっていた。
|
|
|
722
|
|
|
723 いや、でも、empty interval があると、そうもいかないか?
|
|
2
|
724 ~(....&....(...&... ~(...&....)))
|
|
22
|
725 の任意のchopをand,emptyに変える操作がいる。これは exponential。
|
|
2
|
726 p & p & p & p & p
|
|
|
727 p & p & p & p,empty , p
|
|
22
|
728 chomp (non-empty interval chop) だったら、大丈夫。
|
|
|
729
|
|
|
730 でも、closure, proj をいれるならおんなじか。
|
|
2
|
731
|
|
|
732 Mon Oct 9 19:51:27 BST 1995
|
|
|
733
|
|
22
|
734 proj では、r^n の n を階層化する。r^0 は、すべての階層で共有される。
|
|
|
735 他のlengthは共有されないとみるのが正しいのだろう。length(1) proj Q
|
|
|
736 だと、r^1^1 = r^0^1 だよね?
|
|
|
737
|
|
|
738 P proj Q で、Q part のnext part は、
|
|
|
739 proj の中にencupsulated されているので、term はいじる必要はない。が、
|
|
|
740 condition はいじる必要がある。ただし、renaming を original clock
|
|
|
741 level と同じにすると limit が効きすぎるだろう。しかし、ここを複雑に
|
|
|
742 するのは、どうかなぁ。term level も階層化すれば、問題はない。
|
|
|
743 (r^n)^n とか...
|
|
|
744
|
|
|
745 結局、singleton removal は、うまくいかないね。これがうまくいけば、だい
|
|
|
746 ぶ範囲が広まるのだが.... せめて、eventuality と同じぐらいまでにできな
|
|
|
747 いの? あ、そうか、r^s をmarking と見ればいいわけね。しかし、結構、めん
|
|
|
748 どくさいといえばめんどくさい。
|
|
2
|
749
|
|
|
750 Time constant regular variable
|
|
|
751
|
|
22
|
752 renaming なしならば、割と自明。
|
|
2
|
753 r^0 ... r^limit
|
|
22
|
754 をunifyすれば良い。renaming ありだと、もう少し複雑になる。r^n を state
|
|
|
755 と見るのが簡単。いずれにせよ、かなり制限された感じだね。
|
|
|
756
|
|
|
757 renaming の、もっと気の聞いたalgorithmがあれば...
|
|
2
|
758
|
|
|
759 Mon Oct 9 05:48:38 BST 1995
|
|
|
760
|
|
22
|
761 ^r -> true/false では、[a](^r=length(2)) が unsatisfiable.
|
|
|
762 over(r) では、true/false に置き換えている。^r -> +r/-r でも、
|
|
|
763 [a](^r=length(2))はだめ。これにさらに工夫がいる。
|
|
|
764 でも、それはこっちの方がましだということだろう。でも、どれくらい
|
|
|
765 ましなの? local でないぐらいか?
|
|
|
766
|
|
|
767 singleton を ^(r,s) で置き換えても、[a](^r=lenth(2)) は、> length(4)
|
|
|
768 でfail する。なんで?
|
|
2
|
769
|
|
|
770 Sat Oct 7 17:20:17 BST 1995
|
|
|
771
|
|
22
|
772 singleton removal を r^s で行なうと、limit を一つ伸ばす効果が
|
|
|
773 あるらしい。したがってlimitまでいくような場合は状態が増える。
|
|
|
774 r^s の選択を独立に行なうような方法で、ちゃんとできるのか?
|
|
|
775 できないような気もする。
|
|
2
|
776
|
|
|
777 Sat Oct 7 10:08:57 BST 1995
|
|
|
778
|
|
22
|
779 (1) 番号を詰める (番号limitあり)
|
|
|
780
|
|
|
781 は、やってみたけど、^r には効果があるんだけど、他のはほとんど
|
|
|
782 関係ないなぁ。[a](^r...) みたいなものにはきかないのだろう。
|
|
2
|
783
|
|
|
784 Fri Oct 6 09:46:45 JST 1995
|
|
|
785
|
|
22
|
786 (1) 番号を詰める (番号limitあり)
|
|
2
|
787 (2) singleton removal
|
|
|
788
|
|
22
|
789 この二つでかなりいくはず。(2)どうにかなんないの?
|
|
|
790
|
|
|
791 (3) 番号を構造化する low resolution?
|
|
|
792
|
|
|
793 Edge driven な logic にできるか?
|
|
2
|
794
|
|
|
795 Thu Oct 5 18:27:29 JST 1995
|
|
|
796
|
|
22
|
797 うーむ。length limit は、うまくいくが、それ以外の制限がいまいち
|
|
|
798 うまくいかないね。
|
|
|
799
|
|
|
800 rename して ^r の数を制限する方法だと、over に変換されるものが
|
|
|
801 あまりにアドホックに決まってしまう。
|
|
2
|
802 r^n
|
|
22
|
803 の n に、何か term を持って来れないの?
|
|
|
804
|
|
|
805 total order を持って来るか... 効果あるの? さぁ...
|
|
2
|
806
|
|
|
807 Sun Sep 24 01:14:36 JST 1995
|
|
|
808
|
|
22
|
809 だから、
|
|
|
810
|
|
|
811 ^r = false にすると、
|
|
2
|
812
|
|
|
813 [a](^r=legth(2)) -> [a](false=legth(2))
|
|
|
814 [a](false=legth(1))
|
|
|
815 [a](false=legth(0)) = unsatisfiable
|
|
|
816
|
|
22
|
817 になるからだめなの。うんうん。
|
|
|
818 true = length(2) も false = length(2)
|
|
|
819 も、両方ともunsatisfiable。どちらかというと、
|
|
2
|
820 (length(2);not(length(2))) & true
|
|
22
|
821 となるのが正しい。
|
|
2
|
822 (length(2) & true) ; (not(length(2)) & true)
|
|
22
|
823 は? これは Ok なはず。
|
|
|
824
|
|
|
825 だったら、expansion する前にsingletonをチェックして、singleton
|
|
|
826 に対しては quantifiy してしまうってのは? うーむ...
|
|
|
827
|
|
|
828 じゃあ、なんで ^r -> ^r;not(^r) ではだめなのか?
|
|
|
829 これは、終りを共有するものをいっしょにしているから。
|
|
2
|
830
|
|
|
831 ^r on n+1
|
|
|
832 |--| T
|
|
|
833 |-| F
|
|
|
834 || F
|
|
|
835 |-| T
|
|
|
836 || F
|
|
|
837 || F
|
|
|
838
|
|
22
|
839 とする
|
|
2
|
840
|
|
|
841 ^r on n
|
|
|
842 |---|
|
|
|
843 |--|
|
|
|
844 |-|
|
|
|
845 ||
|
|
|
846
|
|
22
|
847 が新しいもの。これらは、独立。ふんふん。
|
|
2
|
848
|
|
|
849 Tue Sep 19 23:53:19 JST 1995
|
|
|
850
|
|
22
|
851 どうも変だな。
|
|
|
852 down(r^0) と true;false とはどこが違うんだ?
|
|
2
|
853 state(1 , not(true& ?(^r,not(@ @empty),@ @empty)&true))
|
|
|
854 [a](^r = length(2))
|
|
|
855 [empty,down(r,0),up(r)]->false
|
|
|
856 [empty,not(down(r,0)),up(r)]->empty
|
|
|
857 [empty,down(r,0),not(up(r))]->empty
|
|
|
858 [empty,not(down(r,0)),not(up(r))]->empty
|
|
|
859 [more,down(r,0),up(r),ev(r^0)]->false
|
|
|
860 [more,not(down(r,0)),up(r),ev(r^0)]->2
|
|
|
861 not(true& ?(^r,not(@ @empty),@ @empty)&true);
|
|
|
862 [a](^r = length(2));
|
|
|
863 not(not(@empty)&true),not(@empty&true)
|
|
|
864 [i](length(1)),not(length(1)&true)
|
|
|
865 [more,down(r,0),not(up(r)),ev(r^0)]->3
|
|
|
866 not(true& ?(^r,not(@ @empty),@ @empty)&true);
|
|
|
867 [a](^r = length(2));
|
|
|
868 not(@empty&true)
|
|
|
869 not(length(1)&true)
|
|
|
870 [more,not(down(r,0)),not(up(r)),ev(r^0)]->3
|
|
|
871
|
|
22
|
872 やっぱり違う。true だと、length(1)でtrue length(2)でfalseという
|
|
|
873 技が出来ない。この選択はこの場所で独立に選択しなくてはならない。
|
|
|
874 (ええ?だけど、true;false なんだから... だったらtrueか?)
|
|
|
875 +r, -r の方がましか?
|
|
2
|
876
|
|
|
877 Sat Sep 16 11:44:25 JST 1995
|
|
|
878
|
|
22
|
879 singleton ^r を true, false に置き換えると、[]true,[]false の意味に
|
|
|
880 なってしまう。実際は、true/false なのに。だから、singleton removal
|
|
|
881 はうまくない。
|
|
2
|
882
|
|
|
883 t0: ^r = length(2)
|
|
|
884 t1: r^0 = length(1) empty/not(r^0)
|
|
|
885 t2: r^0 = mpty(1) empty/r^0
|
|
|
886
|
|
22
|
887 Quantifierに置き換える? だったら残しておいた方がまし?
|
|
|
888 何かoperatorを作る?
|
|
2
|
889 some -> true/false
|
|
22
|
890 quantified true? <>false かな? not([](true)) = not(not(true & not true))).
|
|
|
891 でも、これだといつかはfalseになってしまう。operatorにすると、deterministic
|
|
|
892 でなくなるか。それはまずい。negationが。
|
|
2
|
893
|
|
|
894 Fri Sep 15 11:26:13 JST 1995
|
|
|
895
|
|
22
|
896 singleton check をitl時にすることはできない?
|
|
2
|
897
|
|
|
898 Wed Sep 13 18:24:24 JST 1995
|
|
|
899
|
|
22
|
900 結局、RITLは CFG を含んでいるのだから、Regular Subset を決めることは
|
|
|
901 できない。
|
|
|
902
|
|
|
903 ^r のdepthを制限すれば、ある程度はできる。しかし、これでは
|
|
|
904 fairnessにはならないね。
|
|
|
905
|
|
|
906 depth 以外の制限は? 状態数の制限が望ましい。
|
|
|
907
|
|
|
908 singleton の remove でかなりのことが出来ると言えば、そうなのだが。
|
|
|
909
|
|
|
910 singleton remove のタイミング?
|
|
|
911 itlの時に detect?
|
|
|
912 itlstd の時に detect?
|
|
|
913 remove の仕方
|
|
2
|
914 eventually(^r,N)
|
|
|
915 eventually(not(^r,N))
|
|
22
|
916 を挿入する。ということは、itldecomp の show の直前で
|
|
|
917 行えば良い。
|
|
|
918
|
|
|
919 しかし、これだと正確な状態出力ではない。ではないが原理的にトレース
|
|
|
920 できる部分をはしょっているだけ。mark を付けるのでは同じになってしまう。
|
|
|
921 やはりremoveしたい。
|
|
|
922
|
|
|
923 ^rの出現頻度を押さえることで、logicになるか? 例えば2つとか?
|
|
|
924
|
|
|
925 * consistent にならない==safeでない(標準形を工夫すれば...)
|
|
|
926 * でなくても良いという考え方もある。characterriseできる?
|
|
|
927
|
|
|
928 いずれにせよ、singleton removal でどこまでいくかだな。
|
|
2
|
929
|
|
|
930 Sun Jul 23 10:16:02 JST 1995
|
|
|
931
|
|
22
|
932 * ^r -> +r, -r depth によって独立に選択
|
|
|
933 * +r も r^depth により選択
|
|
|
934
|
|
|
935 これだと、[a](^r),<>(not(^r))がsatisfiable
|
|
|
936
|
|
|
937 * ^r -> +r, -r depth によって独立に選択しない
|
|
|
938
|
|
|
939 と、[a](^r=length(2))がunsatisfiable
|
|
|
940
|
|
|
941 うーむ、うまくいかん。
|
|
2
|
942
|
|
|
943 Sat Jul 22 12:52:11 JST 1995
|
|
|
944
|
|
22
|
945 * depthの違いはchopの処理で行なう
|
|
|
946 * ^rのemptyと、+r, -rのemptyは独立
|
|
|
947 * ^rのmoreと、+r, -rの関係
|
|
|
948
|
|
|
949 +r, -r は、異なるdepthでT/Fの時に生じる
|
|
|
950 既に +r がある時は、それに合流して良い
|
|
|
951 +r/\-r となることはない。それはfalse。
|
|
2
|
952
|
|
|
953 |-------| +r
|
|
|
954 |---------| -r
|
|
22
|
955 ^r +r とする
|
|
|
956 not(^r)があったら-rとする
|
|
|
957
|
|
|
958 これでいいか?
|
|
|
959 tailを共有するrである not(^r),と^rの扱いは対称
|
|
|
960 ^r/-rの組合せは?
|
|
|
961
|
|
|
962 +r, -r が解消される場合
|
|
|
963
|
|
|
964 * +r or -r がempryになるとき
|
|
|
965 -r はemptyにならない
|
|
|
966
|
|
|
967 +rが残って害があるか? -rがなければ関係ない
|
|
|
968 状態は増えるけど。
|
|
2
|
969
|
|
|
970 Fri Jul 14 18:31:19 JST 1995
|
|
|
971
|
|
22
|
972 異なる chop で、異なるrの番号を付ける。
|
|
|
973 その番号毎に up(^r), down(r,n) を行なう
|
|
|
974
|
|
|
975 これによって、すべての組合せが一応得られる。
|
|
|
976
|
|
|
977 番号は状態には付加しない。(いいのか?)
|
|
|
978 同じinterval上では、
|
|
2
|
979 r, not(r)
|
|
22
|
980 があり得る... これは... 気まずいか。
|
|
2
|
981 ^r -> +^r, -^r
|
|
22
|
982 とする? すると... +up, -up がある?
|
|
|
983
|
|
|
984 まあ、試してみよう。(やっぱりだめだった...)
|
|
2
|
985
|
|
|
986 Thu Jul 13 14:05:06 JST 1995
|
|
|
987
|
|
22
|
988 r^n の数を減らす
|
|
|
989 => 等価でユニークな表現
|
|
|
990
|
|
|
991 singleton r^n は消せる
|
|
|
992
|
|
|
993 doubleton r^nどうしを融合したい。
|
|
|
994
|
|
|
995 新しいrをr^nに相対的に定義する (それはできるのだが... +r/-r)
|
|
|
996 のは、うまくいったのだが、足りないものがある。状態数が
|
|
|
997 足りない。
|
|
|
998
|
|
|
999 * 必要な状態数のみを区別する
|
|
|
1000 * 同じ結果を生じる変数は区別しない
|
|
|
1001
|
|
|
1002 自分自身と同じかどうか / 違うということを覚えないといけない
|
|
|
1003 同じだったら関係ない
|
|
2
|
1004
|
|
|
1005 What happen in next case? ([a](^r))
|
|
|
1006
|
|
|
1007 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true
|
|
|
1008
|
|
|
1009 ---|-----| r^5
|
|
|
1010 ---|----| r
|
|
|
1011
|
|
22
|
1012 r^5が落ちれば一つ減る。減らなければr^6で一つ増える。しかし、
|
|
|
1013 この場合は増えてはいけない。r^5 と ^r 自身は関係が無い。
|
|
|
1014 が、結果は同じという関係がある。( うがー、わからないよう.... )
|
|
2
|
1015
|
|
|
1016 st6:
|
|
|
1017 not(r^5) & true, r^5 & true, ^r & true, not(^r) & true
|
|
|
1018
|
|
|
1019 up(^r),down(r^5),down(^r) @not(r^5)&t, t, t, @not(r^6)&t
|
|
|
1020 up(^r),down(r^5),not(down(^r)) @not(r^5)&t, t, @(r^6)&t, t
|
|
|
1021 up(^r),not(down(r^5)),down(^r) t, @not(r^5)&t, t, @not(r^6)&t
|
|
|
1022 up(^r),not(down(r^5)),not(down(^r))
|
|
|
1023 t, @not(r^5)&t, @(r^6)&t, t
|
|
|
1024
|
|
|
1025
|
|
|
1026 Mon Jul 10 20:01:46 JST 1995
|
|
|
1027
|
|
|
1028 f(^r) => contratint_1(^r) & continuation_1(^r)
|
|
|
1029 g(^r) => contratint_2(^r) & continuation_2(^r)
|
|
|
1030
|
|
22
|
1031 r(r^n)&c(r^n) がnを除いて等しい時、
|
|
|
1032 r^n => r^n' がいえる。
|
|
|
1033 けど、別に等しい必然性もない。(たしかに...)
|
|
|
1034
|
|
|
1035 r^nはquantifyして良い。ということは、同じなら消して良いということ?
|
|
|
1036 ということか。cross term は?
|
|
2
|
1037 exists(^r, empty(^r)? ...)
|
|
|
1038
|
|
|
1039 r0: { +r(const, continu),
|
|
|
1040 -r(const, continu) }
|
|
|
1041 r1: { +r(const, continu),
|
|
|
1042 -r(const, continu) }
|
|
|
1043
|
|
22
|
1044 いつかは
|
|
2
|
1045 +r(empty,continu)
|
|
|
1046 +r(true,continu)
|
|
22
|
1047 のどちらかにいく。いや、いかない。emptyなら問題無い。trueが問題(?)
|
|
2
|
1048 +r(fixpoint,contiu)
|
|
22
|
1049 という形になる。これがたくさん存在するということになる。
|
|
2
|
1050 +/-r^n(fixpoint_k,continu_k_i)
|
|
22
|
1051 というわけだ。この場合のr^nの重なりが解消できれば問題は解決。
|
|
|
1052 うまくいかないね...
|
|
2
|
1053
|
|
|
1054
|
|
22
|
1055 で、同じものは消して良い。順序をそろえないと消しにくい。
|
|
|
1056 違うrでも同じカッコなら消して良い。(reular variableは、実質は
|
|
|
1057 一つ, ^r => r,^common にするか? それはちょっと違う)
|
|
|
1058 この場合は消しても干渉のパターンが変わらない。干渉パターン
|
|
|
1059 ごとにマッチングをとるから。(有限の組合せなのか?)
|
|
|
1060
|
|
|
1061 消すのはterm levelでおこなう?
|
|
2
|
1062 c(r^n, i_n...) & ...
|
|
|
1063 c(r^n, i_n...)
|
|
22
|
1064 というtermしかr^nに関してはでてこない。消せるんだったら、他の
|
|
|
1065 方法はいい加減でも大丈夫。
|
|
|
1066
|
|
|
1067 f(r^n)とf(r^n'1)の関係
|
|
2
|
1068 |------|-|
|
|
|
1069 |----|-|
|
|
22
|
1070 r^n, r^n' 自身は独立
|
|
2
|
1071
|
|
|
1072 r^1(r,c)
|
|
|
1073 r^2(r,c)
|
|
|
1074 empty(r^1),empty(r^2),empty(r) => c
|
|
|
1075 cross term
|
|
|
1076 empty(r^1),more(r^2), empty(r) => c,(more(r),r^1(@(r),c))
|
|
|
1077 more(r^1),more(r^2), more(r) =>
|
|
|
1078 more(r),r^1(@(r),c),r^2(@(r),c)
|
|
|
1079 ==
|
|
|
1080 r^1(c);c,more(r),r^1(@(r),c);more(r),r^1(@(r),c),r^2(@(r),c)
|
|
22
|
1081 他のr^nと干渉する方法が変わってしまう...
|
|
2
|
1082
|
|
|
1083
|
|
|
1084 Sun Jul 9 15:32:43 JST 1995
|
|
|
1085
|
|
|
1086 r^1 & true;
|
|
|
1087 r^2 & true;
|
|
|
1088 r^3 & true
|
|
|
1089
|
|
22
|
1090 一つにまとめられない?
|
|
|
1091
|
|
|
1092 f(+/- r^n) (必ずtopにある/一度展開されているから)
|
|
2
|
1093 |-------------|-----------|
|
|
|
1094 down(r^n) => true/false
|
|
|
1095
|
|
22
|
1096 性質
|
|
2
|
1097 f(+/- r^n)
|
|
|
1098 down(r^n) => f((+/-true ,empty))
|
|
|
1099 not(down(r^n)) => f(+/- r^n)
|
|
22
|
1100 parallel termがある時は無くなるまで展開する
|
|
|
1101 r^n, *length(3) などは? これは無視して良い
|
|
|
1102 r^n, *length(3) & true が問題
|
|
2
|
1103 => evenrually true + *length(3)
|
|
|
1104
|
|
22
|
1105 だから、nが複数あっても、f((+/-true ,empty))が同じなら同じでよい(?)
|
|
2
|
1106
|
|
|
1107 f(+/- r^n) => true & down(r^n),f(+/-true,empty)
|
|
|
1108 => down(r^n) = eventually(f(+/-true,empty))
|
|
|
1109
|
|
22
|
1110 ということは、やっぱりdown(r^n)を外に出せるということ?
|
|
|
1111 r^n & true なら eventually(true)
|
|
|
1112 not(r^n) & true なら?
|
|
|
1113
|
|
|
1114 ふむ。そして eventually(f) の f にはr^nは入らない。これは
|
|
|
1115 いけるかも知れない。
|
|
|
1116
|
|
|
1117 chopの処理の時に、eventuality listをbdtの形で外に出せば良い。
|
|
|
1118 eventuality が満たされた時がr^nが成立した時。(これも
|
|
|
1119 前考えたな...)
|
|
2
|
1120 ^r & ....
|
|
22
|
1121 という形だけ?
|
|
|
1122
|
|
|
1123 (^r, g) & f => ev(f),(g & f) ちょっと違う...
|
|
2
|
1124 (^r & f),(g & f)
|
|
|
1125
|
|
22
|
1126 とは少し異なるよ。not がうまくないはず。
|
|
2
|
1127 not(ev(f)); not(g & f) (?)
|
|
|
1128
|
|
22
|
1129 そうか... ev(f)が満たされれば、^rは落ちて良い。(落ちれる)
|
|
|
1130 落ちなくてもいい。
|
|
|
1131
|
|
|
1132 前もってevenruality formにITLを書き換えるのは?
|
|
2
|
1133 f(r) => g(eventualy(h))
|
|
|
1134
|
|
22
|
1135 本当にdiceidableなのか? 整数方程式が書けるとすれば...
|
|
2
|
1136
|
|
|
1137 Fri Jul 7 18:51:32 JST 1995
|
|
|
1138
|
|
|
1139 true & ^r & true =>
|
|
|
1140 r^1 & true;
|
|
|
1141 r^2 & true;
|
|
|
1142 r^3 & true
|
|
22
|
1143 となる。ということは、ひとつのintervalだけを見て吸収することは出来ない。
|
|
2
|
1144
|
|
|
1145 t1 t2
|
|
|
1146 up(r) down(r^1)
|
|
|
1147 r&true |-------------|--------------------
|
|
|
1148 not(r&true) |----------------|not(down(r^1)----
|
|
|
1149 |---|up(r)----|not(down(r^2)-------
|
|
|
1150
|
|
22
|
1151 r^1 は競合するr^1がある時しか関係しない。したがって単独に
|
|
|
1152 出てくるr^1は現在時点で
|
|
2
|
1153 fin(r^1) => true
|
|
|
1154 fin(not(r^1)) => false
|
|
22
|
1155 を決めて良い。これだけで、true & ^r & true は収束する。
|
|
|
1156 が、それだけで収束するか? たぶん、しない。
|
|
2
|
1157
|
|
|
1158 (1)
|
|
22
|
1159 複数の始点を持つ状態を一つにまとめられればできる。+r, -r はそういう
|
|
|
1160 方法だった。が一つにはならない。有限な組合せになる。
|
|
2
|
1161
|
|
|
1162 (2)
|
|
22
|
1163 収束するとすれば、共有されたr^nの組が有限な場合である。これは、finiteness
|
|
|
1164 の条件に相当する。前もって共有される可能性のあるtermを生成できるか? (
|
|
|
1165 たぶんできる)
|
|
|
1166
|
|
|
1167 前もって複数出て来た(違うsytactical interval上の)^rに番号を付けて
|
|
|
1168 識別しておく。競合は、異なる番号上でしか起きない?
|
|
2
|
1169 [](<>(^r)) = not(ture & not(true & ^r))
|
|
22
|
1170 のような場合は? そうか。同じ番号上の共有は+r, -rで構わない。
|
|
|
1171 (true or false だから)
|
|
2
|
1172 [](<>(^r)) <-> [](<>(^r))
|
|
22
|
1173 のような場合は?
|
|
2
|
1174
|
|
|
1175 Fri Jun 30 20:08:47 JST 1995
|
|
|
1176
|
|
|
1177 f(r^1,r^2,r^3) & true,
|
|
|
1178 g(r^1,r^2,r^3) & true
|
|
|
1179
|
|
22
|
1180 f(r^1,r^2,r^3)とg(r^1,r^2,r^3)を見ながらr^nの数を減らさないといけない。
|
|
|
1181
|
|
|
1182 r^n は、emptyの時しか影響しない。moreの時はtrueと同じ。
|
|
|
1183
|
|
|
1184 ^r のみが新しいr^nを増やす。これをいかに吸収するかを調べれば良い?
|
|
2
|
1185
|
|
|
1186 f(r^cur,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
|
|
|
1188 g(r^cur,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
|
|
|
1190
|
|
|
1191
|
|
|
1192 Fri Jun 30 10:48:46 JST 1995
|
|
|
1193
|
|
22
|
1194 各stateに、regular variableのmapを割り当てる。方法がいまいち
|
|
|
1195 わからない。^rの生成された状態を識別することが必要。
|
|
|
1196
|
|
|
1197 ^r(s) をやってみる。昔もやった。
|
|
2
|
1198 true & ^r
|
|
22
|
1199 が爆発する
|
|
2
|
1200 r^1 ; r^2; r^3; ... ; true & ^r
|
|
22
|
1201 これが
|
|
2
|
1202 r^1 true & ^r
|
|
22
|
1203 となれば良い。
|
|
2
|
1204 r^1 .... r^2
|
|
22
|
1205 は新しいr^nになる。(相互関係は?) ^r どうしの制約を保持した
|
|
|
1206 もっとも少ないr^nを選択すれば良い。(この変換はsafe & compete?)
|
|
|
1207 相互関係を保存しないなら^rをすべて共通にすれば良い。が、
|
|
|
1208 それはうまくいかない。
|
|
2
|
1209 r^1 , not(r^2) -> r^1, not(r^1) -> false
|
|
22
|
1210 のような場合があるから。
|
|
2
|
1211 r^1 , not(r^2) -> r^1
|
|
22
|
1212 か?
|
|
|
1213
|
|
|
1214 他の変数が入る場合は? r^1 .. r^n に依存するtermの変換を
|
|
|
1215 計算する。= BDT の leaf の数。それを表現できる最小のr^nを
|
|
|
1216 作る。
|
|
|
1217
|
|
|
1218 そうすれば、temporal operatorのネストは変わらないのだから、
|
|
|
1219 全体は有限になるはず。
|
|
|
1220
|
|
|
1221 これでなんでfullでなくてregularになるの? ^r がcontext dependent
|
|
|
1222 でないから。 r^1 , not(r^2) -> r^1 は、context dependent では
|
|
|
1223 できない。(なるほど...)
|
|
2
|
1224
|
|
|
1225 Wed May 24 20:32:34 JST 1995
|
|
|
1226
|
|
22
|
1227 ^rは、やはり、
|
|
2
|
1228 ^r -> +r, -r
|
|
22
|
1229 の変換でなんとかするべき。こうして生成したモデルは、正しいRITLを
|
|
|
1230 含んでいる。あとは整合性のチェックをすれば良い。
|
|
2
|
1231
|
|
|
1232 (1) local consstency check => regular variable
|
|
|
1233 (2) global consistency check => regular constant
|
|
|
1234
|
|
22
|
1235 どういうようにcheckするの? ん....
|
|
|
1236
|
|
|
1237
|
|
|
1238 昔のbdcomp.pl をbddlibで書き換える。
|
|
2
|
1239
|
|
|
1240 characteristic function f(q)
|
|
|
1241 f(q) = more,fx_q(sbn,sbx,P);empty,fn_q(P)
|
|
|
1242
|
|
|
1243 f(p&q) = f(q) & q
|
|
|
1244
|
|
|
1245
|
|
|
1246 Tue May 2 17:49:35 JST 1995
|
|
|
1247
|
|
22
|
1248 BDDLIBを組み合わせたが、やっぱり Prolog <-> BDD の変換が入るだけ
|
|
|
1249 遅くなるだけだった。bdtstd.pl は綺麗になるのだが。
|
|
|
1250
|
|
|
1251 前作ったBDDの方式も遅くなるだけだった。(BDT/*) それは、
|
|
|
1252 BDD の leaf をnext leafに展開
|
|
|
1253 BDDの再構成
|
|
|
1254 next leafを2-3 treeに登録
|
|
|
1255 新しいnext leaf をさらに展開
|
|
|
1256 というのがすごく遅かったから。
|
|
|
1257
|
|
|
1258 Charcteristic Function を作り上げる方法は、今一だ。でもBDDLIBなら
|
|
|
1259 うまくいくかもしれない。
|
|
|
1260
|
|
|
1261 Subtermを前もって、すべて、
|
|
2
|
1262 condition, next
|
|
22
|
1263 というBDDに展開しておいたら?
|
|
|
1264
|
|
|
1265 Quantifierなどは、Subtermの中に状態が現れてしまう。だから、
|
|
|
1266 前もって、中を展開しておく。
|
|
|
1267
|
|
|
1268 そうすれば、あとの処理は、BDDのみでできるはずだ。(しかし、CF法と
|
|
|
1269 結果は同じ?)
|
|
2
|
1270
|
|
|
1271 Wed Mar 29 17:22:43 JST 1995
|
|
|
1272
|
|
|
1273 regular(r,....r....)
|
|
22
|
1274 という形を使う ( QPTL <-> RITL だから... )
|
|
|
1275
|
|
|
1276 Quantifierを直接使うのは?
|
|
2
|
1277 st(0) = exists(c, c->st(1),not(c)->st(2))
|
|
22
|
1278 さぁ...
|
|
2
|
1279
|
|
|
1280 begin(r,formuala) -> T/F
|
|
|
1281 end(r,formula) -> T/F
|
|
|
1282
|
|
22
|
1283 異なるうformulaが実は同じだった。-> いつか regular(r, f)
|
|
|
1284 という同じ形になる。
|
|
2
|
1285
|
|
|
1286 regular(r,f(r))
|
|
|
1287 empty(f(r)) -> r=true,empty
|
|
|
1288 not(empty(f(r))) -> r=false,empty
|
|
|
1289 regular(r,f(r))
|
|
|
1290 more(f(r)) -> r=true,regular(r,fx(r))
|
|
|
1291 not(more(f(r))) -> r=false,regular(r,fx(r))
|
|
|
1292
|
|
22
|
1293 したがって生成されるモデルは冗長。
|
|
|
1294
|
|
|
1295 chop が来た時に r をreset しないといけない。
|
|
|
1296 (だよね...) だったら、regular(r,f(r))はいらない?
|
|
|
1297 どうやって? r を前もって宣言するってのは?
|
|
|
1298
|
|
|
1299 PDA との関係は?
|
|
2
|
1300
|
|
|
1301 Thu Dec 15 20:21:58 JST 1994
|
|
|
1302
|
|
22
|
1303 Modelとの対応
|
|
2
|
1304
|
|
|
1305 t0 -[+-]-> t1 -[+-]-> t2 -[+-]-> t3
|
|
|
1306
|
|
|
1307 |---------|-----------|
|
|
|
1308 r0 r1 r2
|
|
|
1309 |-----------|-----------|
|
|
|
1310 r0' r1' r2'
|
|
|
1311
|
|
22
|
1312 r0 は常に要素0から始める。
|
|
|
1313 から始める。
|
|
|
1314 r0 -[-]-> r1 で集合の要素にシフトする。
|
|
|
1315 r0 -[+]-> r1 で次の時間のものと違うFAであることを表す。
|
|
2
|
1316
|
|
|
1317 Mon Nov 28 19:27:37 JST 1994
|
|
|
1318
|
|
22
|
1319 RITLステートをITL formulaのbool代数で表す。bool代数はBDDで表現する。
|
|
|
1320
|
|
|
1321 もともとITL formula自身がsubtermの集合だから、二重のbool代数になる。
|
|
|
1322 したがって、double exponential algorithmとなる。
|
|
|
1323
|
|
|
1324 r/not(r) flip では、すべての組合せは生じるが、すべての組合せの
|
|
|
1325 連結は表現できない。したがって、生じたすべての組合せをとって
|
|
|
1326 おけば良い。
|
|
|
1327
|
|
|
1328 集合の作り方
|
|
|
1329 r/not(r) flip で生じたLITLを集合として持つ (implementationは?)
|
|
|
1330
|
|
|
1331 r の例
|
|
2
|
1332 [1] r -(+r)-> r, r -(-r)-> not(r) {r,not(r)}
|
|
22
|
1333 [2] r -> {r,not(r)} -> {r,not(r)} (終り)
|
|
|
1334
|
|
|
1335 t & r の例 (detailは異なる。emptyの場合があるから)
|
|
2
|
1336 [1] t & r -(+r)-> r\/t & r, t & r -(-r)-> not(r)\/t & r
|
|
|
1337 {r\/t&r, not(r)\/t&r}
|
|
22
|
1338 [2] {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} (終り)
|
|
|
1339 [a](r=length(2))の例
|
|
2
|
1340 [1] [a](r=length(2)) -(+r)- > r =length(1)/\[a](r=length(2))
|
|
|
1341 -(-r)- > not(r)=length(1)/\[a](r=length(2))
|
|
|
1342 {r =length(1)/\[a](r=length(2)),
|
|
|
1343 not(r)=length(1)/\[a](r=length(2))}
|
|
|
1344 [2] {r =length(1)/\[a](r=length(2)),
|
|
|
1345 not(r)=length(1)/\[a](r=length(2))} =>
|
|
|
1346 { r =length(0)/\ r =length(1)/\[a](r=length(2)), F
|
|
|
1347 r =length(0)/\ ~r =length(1)/\[a](r=length(2)),
|
|
|
1348 ~r =length(0)/\ r =length(1)/\[a](r=length(2)),
|
|
|
1349 ~r =length(0)/\ ~r =length(1)/\[a](r=length(2))} F
|
|
22
|
1350 [3] => [2] へ
|
|
|
1351 or [1]'へ (r=length(1)がtrueの場合)
|
|
|
1352
|
|
|
1353 もっとコンパクトになるんじゃない? (これだとfinitenessは明解だけど)
|
|
|
1354 ITL(r)は、rをr/not(r)に任意に置換したもののsubset。どれとどれが一致するかを
|
|
|
1355 覚えれば良いのでは? => 開始時点が等しいものが一致。
|
|
|
1356 Indexを付けるのはダメ。=> モデルが有限にならない。(うーむ、わからない)
|
|
|
1357
|
|
|
1358 ITL(r) => 展開 => subset
|
|
|
1359
|
|
|
1360
|
|
|
1361 モデルの解釈
|
|
|
1362
|
|
|
1363 bool代数は、rのassignmentが与えられると解決する。しかし、一つの
|
|
|
1364 ノードが別な解釈を共有することもあり得る。
|
|
|
1365
|
|
|
1366 Term間は任意に遷移するのか?
|
|
|
1367 そうではなくて、同時に遷移する。
|
|
|
1368
|
|
|
1369 異なる開始時点を持つrは、同時に異なる遷移を廻る
|
|
|
1370 すべて可能な遷移があるわけではなく、いくつかはFとなり禁止となる
|
|
|
1371 => r に対する制約
|
|
|
1372
|
|
|
1373 実行できる?
|
|
|
1374
|
|
|
1375 bool節の一つのinstanceを適当に実行すれば良い
|
|
|
1376
|
|
|
1377 Rに単一のautomatonを割り振ることは可能か?
|
|
2
|
1378 [a](R = r) where r is automaton constant
|
|
|
1379
|
|
22
|
1380 時間を遡ってモデルを作る
|
|
|
1381
|
|
|
1382 これによって、state minimizationも同時に走らせることができる
|
|
|
1383 Minimizationのテストプログラムを作って見ること
|
|
2
|
1384
|
|
|
1385 Thu Nov 24 14:54:00 JST 1994
|
|
|
1386
|
|
|
1387 LTTL = LITL < RE
|
|
|
1388 LITL* = RE
|
|
|
1389 RITL = RE RITL(= 2nd order LITL)
|
|
|
1390 RITL is decidable
|
|
|
1391
|
|
|
1392 LTTL = LITL on compact time
|
|
|
1393
|
|
22
|
1394 Even(p)は、LITLでもだめ。
|
|
|
1395 (p.)* ができない
|
|
2
|
1396 (abac)* -> (a[bc])*
|
|
|
1397
|
|
|
1398 LITL -> LTTL converter
|
|
|
1399
|
|
22
|
1400 LITL/LTTLは、やっぱり群を構成する
|
|
2
|
1401
|
|
|
1402 []a & []b & []a
|
|
|
1403 a...ab...ba...a -> a until (b until []a)
|
|
22
|
1404 だからconversionできる?
|
|
|
1405 a & b & aは
|
|
2
|
1406 a, <>(b, <>a)
|
|
22
|
1407 か... うう、できそうな気がする...
|
|
|
1408
|
|
|
1409 P & Q -> start(P),(run(P) until lttl(Q)) に変形する
|
|
|
1410 run(P)にはquantifierが入るのか? 入らない?
|
|
2
|
1411
|
|
|
1412 events continue
|
|
|
1413 |----------|..........|
|
|
|
1414 |-> <>(events)
|
|
|
1415 |-> [](continue)
|
|
|
1416 <>events, <>(continue until Q))
|
|
22
|
1417 というようにcompileする。ふむ。
|
|
2
|
1418
|
|
|
1419 l(P) & Q l(P) = LTTL formula of P
|
|
|
1420 <>(P) -> <>(P,<>(l(Q)))
|
|
|
1421 [](P) -> P until l(Q)
|
|
|
1422
|
|
|
1423
|
|
|
1424 RITL decidability
|
|
|
1425
|
|
|
1426 Reverse Specification
|
|
|
1427
|
|
|
1428 R -> +(R) -(R) on Start Time
|
|
|
1429
|
|
22
|
1430 empty(R) は hidden だけど、+R/-R に関しては同期する
|
|
|
1431 ここがまだ良く分からない。
|
|
|
1432
|
|
|
1433 Modelを直接構成しない。filtrationの意味でも...大きすぎるから。
|
|
|
1434 その代わり、Model constraintを構成する。
|
|
2
|
1435
|
|
|
1436 Generating C / In-kernel implementation
|
|
|
1437
|
|
|
1438 Wed Oct 5 15:30:19 JST 1994
|
|
|
1439
|
|
|
1440 Regular variable.
|
|
|
1441
|
|
|
1442 ^r -> more(^r), @( ^r)
|
|
|
1443 not(more(^r)),@(not(^r))
|
|
|
1444 ^r -> empty(^r), empty
|
|
|
1445 not(empty(^r), not(empty)
|
|
|
1446
|
|
|
1447 This gives ^r constraints, and produce finite state.
|
|
|
1448
|
|
|
1449 Meaning of regular variable.
|
|
|
1450
|
|
|
1451 Mij(^r) = f(Mi(more(^r),empty(^r)),Mi+1j(^r))
|
|
|
1452
|
|
|
1453 ^r's automaton is depend on clock, and fin time is controled
|
|
|
1454 in finite state machine's way. Mij(^r) is f(Mi(p)...Mj(p)).
|
|
|
1455 ^r = lenght(3) & ^r = length(2) is statisfiable.
|
|
|
1456 Is this different from interval variable? Yes. But How?
|
|
|
1457
|
|
|
1458 If we need all regular variable act the same automaton,
|
|
|
1459 exists(^c) [a](^r= ^c),...
|
|
|
1460 where ^c is a time stable automaton.
|
|
|
1461
|
|
|
1462 It is ok to show:,
|
|
|
1463 M |= not(^r),(^r & true)
|
|
|
1464
|
|
|
1465 Problem.
|
|
|
1466
|
|
|
1467 [a](^r=lenth(2)) , lenth(4) is unsatisfiable
|
|
|
1468
|
|
|
1469 empty(^r),(empty =^r) => ^r (true)
|
|
|
1470 empty(^r),(len(1)=^r) => not(^r) (false)
|
|
|
1471
|
|
|
1472 ((empty = ^r)&true), ((length(1) = ^r)&true)
|
|
|
1473 but this is satisfiable.... ?-?
|
|
|
1474
|
|
|
1475
|
|
|
1476 Let's think about,
|
|
|
1477 exists_automatic(R) f(R) = g
|
|
|
1478 automatic unification = boolean unification?
|
|
|
1479
|
|
|
1480 Sat Jun 12 10:41:24 JST 1993
|
|
|
1481
|
|
|
1482 dvcomp uses subterm tree for decomposition and
|
|
|
1483 ndcomp uses chop normal form. Since development
|
|
|
1484 result is not the same, lazy generation of
|
|
|
1485 state is not allowed.
|
|
|
1486
|
|
|
1487 sb's and itl_state's hash and sharing is important.
|
|
|
1488 Time to write C version?
|
|
|
1489
|
|
|
1490 Sun Jun 6 14:15:42 JST 1993
|
|
|
1491
|
|
|
1492 Now module system is supported.
|
|
|
1493 tgen/0 generates Tokio program and
|
|
|
1494 kiss/0 generates KISS format for SIS.
|
|
|
1495
|
|
|
1496 ex(300,X),ex(true proj ~X) becomes very large. Terminates?
|
|
|
1497 ex(300,(X,Y)),ex(true proj (X;Y)) is still very large, but
|
|
|
1498 ex(300,(X,Y)),ex(true proj X) is Ok.
|
|
|
1499
|
|
|
1500 old/bdcomp does not check sbterm early. This is the reason why this
|
|
|
1501 method is slow.
|
|
|
1502 expansion ; subterm check is bad
|
|
|
1503 expansion with subterm check will be ok.
|
|
|
1504
|
|
|
1505 How about permutation?
|
|
|
1506 Declare permutation from the begining.
|
|
|
1507
|
|
|
1508 |- permute V on F <-> F
|
|
|
1509
|
|
|
1510 How about anti-symmetry?
|
|
|
1511
|
|
|
1512 |- odd-permute V on F <-> ~ F
|
|
|
1513 |- even-permute V on F <-> ~ F
|
|
|
1514
|
|
|
1515 Mon Nov 9 15:18:49 JST 1992
|
|
|
1516
|
|
|
1517 prefix operator is wrong.
|
|
|
1518 length(2),prefix((length(3),fin(false)))
|
|
|
1519 must be false.
|
|
|
1520
|
|
|
1521 Mon Sep 21 20:16:39 JST 1992
|
|
|
1522
|
|
|
1523
|
|
|
1524 I'm very sorry to send you rather large example. But it is
|
|
|
1525 a little dificult to extract simple example.
|
|
|
1526
|
|
|
1527 To compile and load,
|
|
|
1528
|
|
|
1529 | ?- [bddi].
|
|
|
1530
|
|
|
1531
|
|
|
1532 In next example, fixpoint predicates find a subtle counter example of ITL
|
|
|
1533 formula.
|
|
|
1534 (p&&p&&p&&p&&p&& ~p&&p)->[](<>p)
|
|
|
1535
|
|
|
1536 is tested by
|
|
|
1537
|
|
|
1538 | ?- ex(10,X),fixpoint(X).
|
|
|
1539
|
|
|
1540 First, this formula is translated into a finite state automaton.
|
|
|
1541 Like this.
|
|
|
1542
|
|
|
1543 +----------+
|
|
|
1544 E,PL -------| Logic |---> E,PL
|
|
|
1545 | |
|
|
|
1546 Sn +------| |--->+ Sx
|
|
|
1547 | | | |
|
|
|
1548 | +----------+ |
|
|
|
1549 | +----------+ |
|
|
|
1550 +-<----| Latch |----+
|
|
|
1551 +----------+
|
|
|
1552
|
|
|
1553 In this case, Sn/Sx pairs are vector of ITL subterm. "Logic" is
|
|
|
1554 defined in boolean constraint on Sn/Sx.
|
|
|
1555
|
|
|
1556 In fixpoint/10, fixpoint(F,Fix,Fix1,E,P,PL,Sn,Sx,S,N),
|
|
|
1557 F current possible state (boolean constraint of Sn)
|
|
|
1558 Fix disjunction of visit state
|
|
|
1559 Fix1 previous visit state, if it is eqaul to Fix, everything is done.
|
|
|
1560 E,P,PL Input/Output value of variable in state diagram
|
|
|
1561 Sn state variable
|
|
|
1562 Sx next state variable
|
|
|
1563 S for display subterm state.
|
|
|
1564 N depth count
|
|
|
1565
|
|
|
1566 fixpoint(_,Fix,Fix1,_E,_P,_PL,_Sn,_Sx,_S,_N):-
|
|
|
1567 bool:taut(Fix=:=Fix1,1),!,write('end'),nl.
|
|
|
1568 fixpoint(F0,_,Fix,E,P,PL,Sn,Sx,S,N):-
|
|
|
1569 quantify(Sn,F0,F0S),bool:sat(F00=:=F0S), % take all possible state
|
|
|
1570 display_state(E,E*F00,P,PL,S,_,Sn), % find counter example
|
|
|
1571 quantify([E|PL], ~E*F00,F0P), % for all possible I/O
|
|
|
1572 bool:sat(F0Q=:=F0P),
|
|
|
1573 copy_term([E,Sx,F0Q],[0,Sn,F1]), % replace Sn/Sx
|
|
|
1574 bool:sat(Fix1=:=Fix+F1), % for termination
|
|
|
1575 write_state_number(N,N1,'depth:'),!,
|
|
|
1576 fixpoint(F1,Fix,Fix1,E,P,PL,Sn,Sx,S,N1).
|
|
|
1577
|
|
|
1578 So this traces all possible execution in finite state automaton.
|
|
|
1579
|
|
|
1580 | ?- ex(10,X),fixpoint(X).
|
|
|
1581 depth:0 % it becomes slower and slower...
|
|
|
1582 depth:1
|
|
|
1583 depth:2
|
|
|
1584 depth:3
|
|
|
1585 depth:4
|
|
|
1586 depth:5
|
|
|
1587 depth:6
|
|
|
1588 depth:7
|
|
|
1589 empty,[t(p,0)],[...] % find one counter example
|
|
|
1590 |: % a return is required
|
|
|
1591 depth:8
|
|
|
1592 end
|
|
|
1593
|
|
|
1594 X = ((p&&p&&p&&p&&p&& ~p&&p)->[](<>p)) ?
|
|
|
1595
|
|
|
1596 yes
|
|
|
1597 | ?-
|
|
|
1598
|
|
|
1599 I think I need something like setarg in boolean constraint.
|
|
|
1600 Sun Sep 20 18:10:30 JST 1992
|
|
|
1601
|
|
|
1602 Why not add exclusive status as a primitive?
|
|
|
1603 states([a,b,c,d,e,f]) -> [](( ~(( a,b)), ... )
|
|
|
1604 2^n ... Wow!
|
|
|
1605 It generates
|
|
|
1606 status(a)-> ... ; status(b)-> ... status(f)-> .. ; status([])-> ...
|
|
|
1607 generate n+1.
|
|
|
1608
|
|
|
1609 Tue Sep 15 13:04:43 JST 1992
|
|
|
1610
|
|
22
|
1611 結局、Regular variable state を共有しないと収束しないし、
|
|
|
1612 共有できるかどうかの判断は大域的だから、この方法では
|
|
|
1613 できないらしい。
|
|
2
|
1614
|
|
|
1615 Tue Sep 15 11:36:36 JST 1992
|
|
|
1616
|
|
|
1617 Regular variable must be non-deterministic.
|
|
|
1618 ^r
|
|
|
1619 [more,up(r),down(r)] is not false
|
|
|
1620
|
|
|
1621 If we don't care about down, we cannot distinguish
|
|
|
1622 ^r& ^r ,not( ^r )
|
|
|
1623
|
|
|
1624 up(r) down(1) ~down(1)
|
|
|
1625 | | |
|
|
|
1626 |----------------|-------|
|
|
|
1627 up(r) down(2)
|
|
|
1628
|
|
|
1629 Mon Sep 14 14:07:52 JST 1992
|
|
|
1630
|
|
|
1631 (^r & ^r),not(^r)
|
|
|
1632 itl:0 [empty,up(r),down(r,0)] -> false
|
|
|
1633 itl:0 [more,up(r),down(r,0)] -> false
|
|
|
1634 itl:0 [more,up(r),~down(r,0)] -> (stay(r,now)&^r),not(stay(r,now)) now=1
|
|
|
1635 stay(^r,0)
|
|
|
1636
|
|
|
1637 (stay(r,now)&^r),not(stay(r,now))
|
|
|
1638 itl:1 [empty]->false
|
|
|
1639 itl:1 [more,down(r,1),up(r),down(r)]->false
|
|
|
1640 itl:1 [more,~down(r,1)]-> (stay(r,now)&^r),not(stay(r,now)) now = 1 2
|
|
|
1641 itl:1 [more,down(r,1),~down(r,0)]]->
|
|
|
1642 stay(r,1);(stay(r,now)&^r),not(stay(r,now)) 3
|
|
|
1643 stay(2,1)
|
|
|
1644
|
|
|
1645 stay(r,1);(stay(r,3)&^r),not(stay(r,3))
|
|
|
1646 itl:3 [empty,down(1)]->empty
|
|
|
1647 itl:3 [empty,~down(1)]->false
|
|
|
1648 itl:3 [more,down(r,1)]->true
|
|
|
1649 itl:3 [more,~down(r,1)]-> stay(r,2);(stay(r,4)&^r),not(stay(r,4)) = 3
|
|
|
1650 itl:3 [more,down(r,1),~down(r,0)]]-> stay(r,1);(stay(r,3)&^r),not(stay(r,3)) 3
|
|
|
1651 stay(2,1),stay(4,3)
|
|
|
1652
|
|
|
1653 Mon Sep 14 00:25:08 JST 1992
|
|
|
1654
|
|
22
|
1655 ^r で生成されるautomatonは、^rを普通の変数と見て生成するtableauの
|
|
|
1656 subsetである。従って、tableauのnodeを指し示すことで ^r のモデルを
|
|
|
1657 作ることが出来る。しかし、うまくいかない...
|
|
|
1658
|
|
|
1659 (^r & true),not(^r) のモデルはないから
|
|
|
1660
|
|
|
1661 そこで、stay(r,N)を使う (up(r),emtpy & true & down(r),empty) ではだめ。
|
|
|
1662 ^r & ^r -> ^r になってしまうから。
|
|
|
1663
|
|
|
1664 するとモデル構築が収束しない --> これは Full ITL だから
|
|
|
1665
|
|
|
1666 しかしRITLのモデルは有限だから stay(r,N)のかなりの部分は
|
|
|
1667 相互に等しい。等しいかどうかをどう判断するかが問題。
|
|
|
1668
|
|
|
1669 Deterministic Pathが等しければ同じstateと判断するのでは足りない
|
|
|
1670 Loopが作れないから。
|
|
|
1671
|
|
|
1672 むしろすべて等しいのがDefaultで、必要な時だけ分離するのが望ましい
|
|
2
|
1673
|
|
|
1674 Mon Jan 1 11:05:38 JST 1990
|
|
|
1675
|
|
|
1676 ^r & ^r
|
|
|
1677 itl:0 [empty,up(r),down(r)] -> empty
|
|
|
1678 itl:0 [more,up(r),down(r)] -> false
|
|
|
1679 itl:0 [more,up(r),~down(r)] -> stay(r,[true])&^r 1
|
|
|
1680 stay(r,[]) -> down,empty
|
|
|
1681 stay(r,[]) -> ~down,more
|
|
|
1682
|
|
|
1683 stay(r,[])&^r
|
|
|
1684 itl:1 [empty,down(r,[]),down(r,[true]),up(r)]
|
|
|
1685 itl:1 [more,down(r,[true]),up(r),down(r,[])]->false
|
|
|
1686 itl:1 [more,~down(r,[true])]-> stay(r,[true,true])&^r 2
|
|
|
1687 itl:1 [more,down(r,[true]),up(r),down(r,[])]->false
|
|
|
1688 itl:1 [more,down(r,[true]),up(r),~down(r,[])]->stay(r,[true]) 3 -> false
|
|
|
1689 itl:1 [more,down(r,[true]),~up(r)])]->false
|
|
|
1690 stay(r,[]) -> down,empty
|
|
|
1691 stay(r,[true]) -> down,up(r),empty
|
|
|
1692 stay(r,[true]) -> more, ~down, stay(r,[true,true])
|
|
|
1693 stay(r,[true]) ?why not
|
|
|
1694 stay(r,[true]) -> more, down, up(r), stay(r,[true]) -> false
|
|
|
1695
|
|
|
1696 stay(r,[true,true]) -> down,up(r),empty
|
|
|
1697 itl:2 [empty,down(r,[]),down(r,[true,true]),up(r)]
|
|
|
1698 itl:2 [more,down(r,[true,true]),up(r),down(r,[])]->false
|
|
|
1699 itl:2 [more,~down(r,[true,true])]-> stay(r,[true,true,true])&^r 4
|
|
|
1700 itl:2 [more,down(r,[true,true]),up(r),down(r,[])]->false
|
|
|
1701 itl:2 [more,down(r,[true,true]),up(r),~down(r,[])]->stay(r,[true]) 3 -> false
|
|
|
1702 itl:2 [more,down(r,[true,true]),~up(r)])]->false
|
|
|
1703 stay(r,[true,true]) -> down,up(r),empty
|
|
|
1704 stay(r,[true,true]) -> more, ~down, stay(r,[true,true,true])
|
|
|
1705 stay(r,[true,true]) ?why
|
|
|
1706 stay(r,[true,true]) -> more, down.
|
|
|
1707
|
|
|
1708 Sat Sep 12 18:05:26 JST 1992
|
|
|
1709
|
|
|
1710 How about contiion-history list?
|
|
|
1711
|
|
|
1712 (p->^r),@((q->^r),@empty)
|
|
|
1713 itl:0 [more,p,up(r),~down(r,[])] -> stay(r,[p]),(q->^r,@empty) 1
|
|
|
1714 itl:0 [more,~p]-> true
|
|
|
1715 stay(r,[]) p ->stay([p]),~down
|
|
|
1716 ~p->true
|
|
|
1717
|
|
|
1718 stay(r,[p]),q->^r,@empty
|
|
|
1719 itl:1 [more,p,q,up(r),~down(r,[p]),~down(r,[])]
|
|
|
1720 -> empty,stay(r,[(p,q),p]),stay(r,[p]),stay(r,[q]) 2
|
|
|
1721 itl:1 [more,~p,q,up(r),~down(r,[p]),~down(r,[])]
|
|
|
1722 -> empty,stay(r,[(~p,q),p]),stay(r,[q]) 3
|
|
|
1723 itl:1 [more,~q] -> empty,stay(r,[~q,p]) 4
|
|
|
1724 stay(r,[]) q ->stay(r,[q]),~down
|
|
|
1725 ~q ->true
|
|
|
1726 stay(r,[p]) q ->stay(r,[(p,q),p]),~down
|
|
|
1727 q ->stay(r,[(~p,q),p]),~down
|
|
|
1728 ~q->true
|
|
|
1729
|
|
|
1730 empty,stay(r,[(p,q),p]),stay(r,[p]),stay(r,[q])
|
|
|
1731 itl:2 [empty,q] -> false
|
|
|
1732 itl:2 [empty,~q,down(r,1),down(r,0)] -> true
|
|
|
1733 stay(r,[(p,q),p]) ->down
|
|
|
1734 stay(r,[p]) ~q->down
|
|
|
1735 stay(r,[q]) ~q->down
|
|
|
1736 stay(r,[(p,q),p]) ~q->down
|
|
|
1737
|
|
|
1738 empty,stay(r,[(~p,q),p]),stay(r,[q])
|
|
|
1739 itl:3 [empty,down(r,1),down(r,0)] -> true
|
|
|
1740 stay(r,[(p,q),p]) ->down
|
|
|
1741 stay(r,[q]) ->down
|
|
|
1742
|
|
|
1743 empty,stay(r,[~q,p])
|
|
|
1744 itl:3 [empty,down(r,1)] -> true
|
|
|
1745 stay(r,[~q,p]) ->: down
|
|
|
1746
|
|
|
1747 Fri Sep 11 16:13:48 JST 1992
|
|
|
1748
|
|
|
1749 Parallel Regular variable construction
|
|
|
1750
|
|
|
1751 itl:0 [up(r),~down(r,0)] -> ... stay(r,0).... 1 -> stay(r,N1)
|
|
|
1752 [up(r),~down(r,0)] -> ... stay(r,0).... 2 -> stay(r,N2)
|
|
|
1753
|
|
|
1754 ^r:0 [up(r),~down(r,0)] -> ... stay(r,N1).... 1
|
|
|
1755 [up(r),~down(r,0)] -> ... stay(r,N2).... 2
|
|
|
1756
|
|
|
1757 equivalence list
|
|
|
1758 stay(r,i) = stay(r,j)
|
|
|
1759 if stay(r,4) -f-> stay(r,i)
|
|
|
1760 stay(r,4) -g-> stay(r,j), f->g
|
|
|
1761
|
|
|
1762 stay(r,n) .... itl:n -> [x0,x1,x2...xk]
|
|
|
1763
|
|
|
1764 Tue Sep 8 22:13:51 JST 1992
|
|
|
1765
|
|
|
1766 true & ^r
|
|
|
1767 [empty,up(r),down(r)]->true
|
|
|
1768 [more,up(r),down(r)]->(stay(r,1);true & ^r)
|
|
|
1769 [more,up(r),~down(r)]->(stay(r,1);true & ^r) = 3
|
|
|
1770 [more,~up(r)]->(true & ^r)
|
|
|
1771
|
|
|
1772 How to prevent stay(r,N) multiplier?
|
|
|
1773
|
|
|
1774 state(3) = (stay(r,1);true & ^r)
|
|
|
1775 [empty,down(r,1)]->empty
|
|
|
1776 [empty,down(r,3),up(r),not(down(r,1))]->empty
|
|
|
1777 [empty,not(down(r,3)),up(r),not(down(r,1))]->false
|
|
|
1778 [empty,down(r,3),not(up(r)),not(down(r,1))]->false
|
|
|
1779 [empty,not(down(r,3)),not(up(r)),not(down(r,1))]->false
|
|
|
1780 [more,up(r)]->(stay(r,1);stay(r,3);true & ^r)
|
|
|
1781 [more,not(up(r))]->3
|
|
|
1782
|
|
|
1783 Why stay(3) = stay(1)? .... Finitarity?
|
|
|
1784
|
|
|
1785 state(1 , ^r& ^r,not(^r))
|
|
|
1786 [empty,down(r,1),up(r)]->false
|
|
|
1787 [empty,not(down(r,1)),up(r)]->false
|
|
|
1788 [empty,down(r,1),not(up(r))]->false
|
|
|
1789 [empty,not(down(r,1)),not(up(r))]->false
|
|
|
1790 [more,down(r,1),up(r)]->3 (stay(r,1);stay(r,1)& ^r),not(stay(r,1))
|
|
|
1791 [more,not(down(r,1)),up(r)]->4 stay(r,1)& ^r,not(stay(r,1))
|
|
|
1792 [more,down(r,1),not(up(r))]->false
|
|
|
1793 [more,not(down(r,1)),not(up(r))]->false
|
|
|
1794
|
|
|
1795 state(3 , (stay(r,1);stay(r,1)& ^r),not(stay(r,1)))
|
|
|
1796 [empty,down(r,1)]->false
|
|
|
1797 [empty,not(down(r,1))]->false
|
|
|
1798 [more,up(r),down(r,1)]->3
|
|
|
1799 [more,not(up(r)),down(r,1)]->3
|
|
|
1800 [more,not(down(r,1))]->3
|
|
|
1801
|
|
|
1802 state(4 , stay(r,1)& ^r,not(stay(r,1)))
|
|
|
1803 [empty,down(r,4),up(r),down(r,1)]->false
|
|
|
1804 [empty,not(down(r,4)),up(r),down(r,1)]->false
|
|
|
1805 [empty,down(r,4),not(up(r)),down(r,1)]->false
|
|
|
1806 [empty,not(down(r,4)),not(up(r)),down(r,1)]->false
|
|
|
1807 [empty,not(down(r,1))]->false
|
|
|
1808 [more,up(r),down(r,1)]->3
|
|
|
1809 [more,not(up(r)),down(r,1)]->4
|
|
|
1810 [more,not(down(r,1))]->4
|
|
|
1811
|
|
|
1812 1.4510000000000002 sec.
|
|
|
1813
|
|
|
1814
|
|
|
1815 Tue Jun 30 17:01:37 JST 1992
|
|
|
1816
|
|
|
1817 Quantifier does not works well.
|
|
|
1818 ?-fixpoint(even(p)=evenp(p)).
|
|
|
1819 Projection looks like difficult.
|
|
|
1820
|
|
|
1821 Tue Jun 30 08:58:27 JST 1992
|
|
|
1822
|
|
|
1823 fixpoint((a,(more = (more & more)))) terminates. why?
|
|
|
1824 fixpoint(more = (more & more)) causes loop. why?
|
|
|
1825
|
|
|
1826 It looks like SICSuts's bug. Some how I avoid that.
|
|
|
1827
|
|
|
1828 Sun Mar 01 01:01:57 1992 BST
|
|
|
1829
|
|
|
1830 Yes, I almost finish BDD version.
|
|
|
1831
|
|
|
1832 Quantification is very subtle in SICStus.
|
|
|
1833
|
|
|
1834 ?-bool:sat(_A=:= B*C),bool:sat(_A=:=A),bool:sat(E =:= ~B*A^A).
|
|
|
1835 ?-bool:sat(_A=:= B*C),bool:sat(A=:=_A),bool:sat(E =:= ~B*A^A).
|
|
|
1836 give us different result.
|
|
|
1837
|
|
|
1838 ?-fixpoint(p-> [](<>(p)) causes quantifier failure.
|
|
|
1839
|
|
|
1840 exists(p,..) is now working, but closure is not.
|
|
|
1841
|
|
|
1842 Mon Feb 10 20:06:36 1992 BST
|
|
|
1843
|
|
|
1844 ?-fixpoint(p,X).
|
|
|
1845 subterm(p,N,_,[p(N)],[]) p =:= N
|
|
|
1846 ?-tableau(N,F1,[],[])
|
|
|
1847 F1 = exists(p,F*R)/replace(S,S')
|
|
|
1848 N=p, F1=nil?
|
|
|
1849 copy_term([],[],N],[[],[],F]), no constrain on N/F
|
|
|
1850 ?-bool:sat(F1=:=(N+F)).
|
|
|
1851 ?-bool:taut(N=:=F1,1) N=:=(N+F) x
|
|
|
1852
|
|
|
1853
|
|
|
1854 Wed Nov 06 21:56:57 1991 BST
|
|
|
1855
|
|
|
1856 Dense time modification.
|
|
|
1857
|
|
|
1858 more <-> more & more
|
|
|
1859 discrete time:
|
|
|
1860 more -> empty->false;more->true
|
|
|
1861 true -> empty->true; more->true
|
|
|
1862 more&more -> empty->false;more->true&more
|
|
|
1863 true&more -> empty->false; <---- This makes difference
|
|
|
1864 more->true
|
|
|
1865 dense time:
|
|
|
1866 more&more* > empty->false;more->more*
|
|
|
1867 more* -> empty->true ;more->more*
|
|
|
1868
|
|
|
1869 more -> empty->false;more->true
|
|
|
1870 true -> empty->true; more->true
|
|
|
1871 more&more -> empty->false;more->true
|
|
|
1872 true -> empty->true; more->true
|
|
|
1873
|
|
|
1874
|
|
|
1875 Tue Jun 25 07:21:11 1991 BST
|
|
|
1876
|
|
|
1877 2nd order local variable is also easily implemented. Notation?
|
|
|
1878 regurlar
|
|
|
1879
|
|
|
1880 Tue Jun 25 07:06:28 1991 BST
|
|
|
1881
|
|
|
1882 For verification,
|
|
|
1883 Information hiding is bad. Necessary information muse be accessed by
|
|
|
1884 everyone for reliability. Only useless information is allow to hide.
|
|
|
1885 If some information does not change world, it is useless. Higer
|
|
|
1886 abstraction makes many information useless, which can be hide.
|
|
|
1887
|
|
|
1888 Tue Jun 25 06:52:32 1991 BST
|
|
|
1889
|
|
|
1890 Closure is easily implemented.
|
|
|
1891 Single varible quantifier is also easy. These are effectively
|
|
|
1892 equivalent in expressiveness.
|
|
|
1893
|
|
|
1894 But nested quantifier is very different. Its decomposition is
|
|
|
1895 same as sigle variable case, but to make a standard form, it
|
|
|
1896 requires P-space. Quantifier impelentation of bdtstd/itlstd
|
|
|
1897 will be difficult.
|
|
|
1898
|
|
|
1899 Derivation tree generation method is much suitable for quantifier.
|
|
|
1900 But is it worth implement? It is better to find out another
|
|
|
1901 abstraction mechanism, such as multi-linear projection.
|
|
|
1902
|
|
|
1903 The important this is not what IS existing, but how it DOES exists.
|
|
|
1904 Quantifier lacks synchronization type.
|
|
|
1905
|
|
|
1906 Tue Jun 21 21:08:31 BST 1991
|
|
|
1907
|
|
|
1908 Problem on Theorem prover
|
|
|
1909
|
|
|
1910 1) it does not handle eventuality
|
|
|
1911 |= true & empty ( compact interval )
|
|
|
1912 |= finite -> (true & empty) <- eventuality axiom
|
|
|
1913 ( open interval ) introducing topology? and differencial?
|
|
|
1914 d/dt f(x,t) is related to scheduling? very close to ....
|
|
|
1915 2) dense time
|
|
|
1916 what's wrong?
|
|
|
1917 3) 3-stages: itlstd, decomposition, checking are redundant each other.
|
|
|
1918 -> derivation tree construction ( do this first )
|
|
|
1919 (bdcomp.pl must work faster)
|
|
|
1920 4) extensions
|
|
|
1921 infinite interval
|
|
|
1922 interval variable
|
|
|
1923 projection
|
|
|
1924 framing
|
|
|
1925 multi-linear
|
|
|
1926 scheduler
|
|
|
1927 other standard form
|
|
|
1928 interactive proof/protocol design
|
|
|
1929 rational length operator
|
|
|
1930 5) overupping interval (minus length)
|
|
|
1931
|
|
|
1932 Tue Jun 18 16:45:35 BST 1991
|
|
|
1933
|
|
|
1934 true & q ->
|
|
|
1935 NDST
|
|
|
1936 e0, e1 q->true
|
|
|
1937 m0, e1 q->@true
|
|
|
1938 m0, m1 ->@(true & q)
|
|
|
1939 else false
|
|
|
1940 DST
|
|
|
1941 [e0,q] -> true
|
|
|
1942 [m0,q] -> @true ;@(true & q)
|
|
|
1943 [e0,~q] -> false
|
|
|
1944 [m0,~q] -> @false;@(true & q)
|
|
|
1945
|
|
|
1946 ~(true & q) ->
|
|
|
1947 NDST
|
|
|
1948 e0, e1 q->false
|
|
|
1949 m0, e1 q->@false
|
|
|
1950 m0, m1 ->@~(true & q)
|
|
|
1951 else true
|
|
|
1952 DST
|
|
|
1953 [e0,q] -> false
|
|
|
1954 [m0,q] -> ~(@true ;@(true & q))
|
|
|
1955 [e0,~q] -> true
|
|
|
1956 [m0,~q] -> ~(@false;@(true & q))
|
|
|
1957
|
|
|
1958 Tue Jun 18 15:49:21 BST 1991
|
|
|
1959
|
|
|
1960
|
|
|
1961 %
|
|
|
1962 % London 23:38 36.52 Newyork 18:38 Tokyo 07:38
|
|
|
1963 %
|
|
|
1964 p & q
|
|
|
1965 -> |-----|-----|
|
|
|
1966 1 0
|
|
|
1967
|
|
|
1968 ifEmpty(p) 1->p
|
|
|
1969 ifNotEmpty(p) ~1->p
|
|
|
1970
|
|
|
1971
|
|
|
1972 P & Q ->
|
|
|
1973 0 P,Q
|
|
|
1974 ~0, 1 beg(P),Q
|
|
|
1975 ~0,~1 Pn, @(Px,Q)
|
|
|
1976
|
|
|
1977 p & q ->
|
|
|
1978 NDST
|
|
|
1979 0 p,q->true
|
|
|
1980 ~0, 1 p,q->@true
|
|
|
1981 ~0,~1 p->@(true & q)
|
|
|
1982 else false
|
|
|
1983 DST
|
|
|
1984 [p,q] -> [0]true +[~0,1]@true +[~0,~1]@(true & q) <- sometime?
|
|
|
1985 [p,~q] -> [0]false+[~0,1]@false+[~0,~1]@(true & q)
|
|
|
1986 [~p] -> []false
|
|
|
1987 a path must contain true eventuality
|
|
|
1988
|
|
|
1989 ~(p & q) ->
|
|
|
1990 NDST
|
|
|
1991 0 p,q->false
|
|
|
1992 ~0, 1 p,q->@false
|
|
|
1993 ~0,~1 p->@~(true & q)
|
|
|
1994 else true
|
|
|
1995 DST
|
|
|
1996 [p,q] -> [0]false+[~0,1]@false+[~0,~1]@~(true & q) <- never?
|
|
|
1997 [p,~q] -> [0]true +[~0,1]@true +[~0,~1]@~(true & q)
|
|
|
1998 [~p] -> []true
|
|
|
1999 a path must not contain false eventuality
|
|
|
2000
|
|
|
2001
|
|
22
|
2002 iのは式の中の&の数に等しい
|
|
2
|
2003
|
|
|
2004 empty
|
|
|
2005 0 true
|
|
|
2006 ~0 false
|
|
|
2007 ~empty
|
|
|
2008 0 false
|
|
|
2009 ~0 true
|
|
|
2010 fin(p)
|
|
|
2011 [p] -> [0]true +[~0]@fin(p)
|
|
|
2012 [~p] -> [0]false+[~0]@fin(p)
|
|
|
2013 keep(p)
|
|
|
2014 [p] -> [0]true+[~0]@keep(p)
|
|
|
2015 [~p] -> [0]true+[~0]false
|
|
|
2016 p & q & r ->
|
|
|
2017 NDST
|
|
|
2018 2, 1, 0 p,q,r->true
|
|
|
2019 2, 1,~0 p,q,r->@true
|
|
|
2020 2,~1,~0 p,q->@(true & r)
|
|
|
2021 ~2,~1,~0 p->@(true & q & r)
|
|
|
2022 DST
|
|
|
2023 [~p] -> []false
|
|
|
2024 [p,~q] -> [ 0]false
|
|
|
2025 +[ 2, 1,~0]@false
|
|
|
2026 +[ 2,~1,~0]@(true & r)
|
|
|
2027 +[~2,~1,~0]@(true & q & r)
|
|
|
2028 [p,q,~r] -> [ 0]false
|
|
|
2029 +[ 2, 1,~0]@false
|
|
|
2030 +[ 2,~1,~0]@(true & r)
|
|
|
2031 +[~2,~1,~0]@(true & q & r)
|
|
|
2032 [p,q,r] -> [ 0]true
|
|
|
2033 +[ 2, 1,~0]@true
|
|
|
2034 +[ 2,~1,~0]@(true & r)
|
|
|
2035 +[~2,~1,~0]@(true & q & r)
|
|
|
2036
|
|
|
2037 ~(p & q & r) ->
|
|
|
2038 NDST
|
|
|
2039 2, 1, 0 p,q,r->false
|
|
|
2040 2, 1,~0 p,q,r->@false
|
|
|
2041 2,~1,~0 p,q->@~(true & r)
|
|
|
2042 ~2,~1,~0 p->@~(true & q & r)
|
|
|
2043 DST
|
|
|
2044 [~p] -> []true
|
|
|
2045 [p,~q] -> [ 0]true
|
|
|
2046 +[ 2, 1,~0]@true
|
|
|
2047 +[ 2,~1,~0]@~(true & r)
|
|
|
2048 +[~2,~1,~0]@~(true & q & r)
|
|
|
2049 [p,q,~r] -> [ 0]true
|
|
|
2050 +[ 2, 1,~0]@true
|
|
|
2051 +[ 2,~1,~0]@~(true & r)
|
|
|
2052 +[~2,~1,~0]@~(true & q & r)
|
|
|
2053 [p,q,r] -> [ 0]false
|
|
|
2054 +[ 2, 1,~0]@false
|
|
|
2055 +[ 2,~1,~0]@~(true & r)
|
|
|
2056 +[~2,~1,~0]@~(true & q & r)
|
|
|
2057
|
|
|
2058
|
|
|
2059 Thu Jun 13 12:00:39 BST 1991
|
|
|
2060
|
|
|
2061 Empty Queue should be incoporated into Cond part.
|
|
|
2062 Only true/false remains in Em_j part.
|
|
|
2063
|
|
|
2064 S = \Sum_j Cond_j -> ( \Sum_i empty_i->Em_{i,j} -> More_j )
|
|
|
2065 ~S = \Sum_j Cond_j -> ( \Sum_i empty_i->Em_{i,j} -> ~More_j )
|
|
|
2066
|
|
|
2067 Thu Jun 13 11:32:44 BST 1991
|
|
|
2068
|
|
|
2069 S = \Sum Cond_j -> ( empty->Em_j ; ~empty->More_j )
|
|
|
2070 ~S = \Sum Cond_j -> ( empty->~Em_j ; ~empty->~More_j )
|
|
|
2071 since empty is invisible, ; means non deterministic choice
|
|
|
2072 More_j = Keep \and @ More => troubled on negation
|
|
|
2073
|
|
|
2074 Cond_j -> ( empty->Em_j + (Keep_j \and @ More_j) )
|
|
|
2075 =>
|
|
|
2076 Cond_j + Keep_j -> ( empty->Em_j + ~empty->@ More_j )
|
|
|
2077 Cond_j + ~Keep_j -> ( empty->Em_j + ~empty->false )
|
|
|
2078
|
|
|
2079 Example
|
|
|
2080
|
|
|
2081 empty -> true -> (empty->true + ~empty->false)
|
|
|
2082 ~empty -> true -> (empty->false+ ~empty->true)
|
|
|
2083 fin(p) -> true -> (empty->p+ ~empty->@fin(p))
|
|
|
2084 keep(p) -> p -> (empty->true + ~empty->@keep(p))
|
|
|
2085 + ~p -> (empty->true + ~empty->false)
|
|
|
2086
|
|
|
2087 Wed Jun 12 16:05:31 BST 1991
|
|
|
2088
|
|
|
2089 ITL->DST converter using BDT
|
|
|
2090
|
|
|
2091 varialbe order
|
|
|
2092 p & q
|
|
|
2093 ~p -> []
|
|
|
2094 p,q -> [e0, (t & q)] e0 = (t & q)
|
|
|
2095 p,~q -> [~e0,(t & q)]
|
|
|
2096 t & q (contains both ~e0, e0)
|
|
|
2097 ~q -> [~e0,(t & q)]
|
|
|
2098 q -> [e0,t,(t & q)]
|
|
|
2099 t -> [e1,(~e1,t)] e1 = (t)
|
|
|
2100
|
|
|
2101 ITL model checker
|
|
|
2102
|
|
|
2103 Wed May 22 15:37:30 BST 1991
|
|
|
2104
|
|
|
2105 The problem is negation of state digram is time consuming task.
|
|
|
2106 To make a symmetrical treatment of negation on state digram,
|
|
|
2107 exclusion normal form is good.
|
|
|
2108
|
|
|
2109 P == (ab -> empty) + ((~a)b -> false) + (a(~b)+~a~b -> @next)
|
|
|
2110 ~P == (ab -> false) + ((~a)b -> empty) + (a(~b)+~a~b -> @~next)
|
|
|
2111
|
|
|
2112 True-Set + False-Set + Next-Set
|
|
|
2113
|
|
|
2114 It requires 2^numver(variables on expression) terms. (Sad..)
|
|
|
2115
|
|
|
2116 P,Q -> PQ
|
|
|
2117 P;Q -> PQ + ~PQ + P~Q
|
|
|
2118
|
|
|
2119 Tue May 21 19:16:12 BST 1991
|
|
|
2120
|
|
|
2121 Extenstion of state diagram is necessary.
|
|
|
2122
|
|
|
2123 true & p = <>p
|
|
|
2124 s0 -empty-> p
|
|
|
2125 s0 -e(true)-> s0
|
|
|
2126 s0 -e(p)-> true
|
|
|
2127 ~(true & ~p) = #p
|
|
|
2128 s0 -empty-> p
|
|
|
2129 s0 -a(~p)-> false
|
|
|
2130 s0 -e(true)-> s1(~true & ~p)
|
|
|
2131 ~(p & ~q) = #p
|
|
|
2132 s0 -empty-> ~p;q
|
|
|
2133 s0 -a(p)-> s1(~(true & ~q))
|
|
|
2134 s1 -a(~q)-> false
|
|
|
2135 p & q
|
|
|
2136 s0 -empty-> p,q
|
|
|
2137 s0 -p-> s1(true&q)
|
|
|
2138 s1 -e(true)-> s1
|
|
|
2139 s1 -e(q)-> true = s1 -a(~q)-> false
|
|
|
2140
|
|
|
2141 Tue May 21 15:08:51 BST 1991
|
|
|
2142
|
|
|
2143 The point is the concurrent development of negation form.
|
|
|
2144 |- ~(On Some interval, P) <->
|
|
|
2145 |- For all interval, ~P <->
|
|
|
2146 |\- On Some interval, P
|
|
|
2147 |- ~~P <-> |-P
|
|
|
2148
|
|
|
2149 |-P,|\-Q => |-P0,@Pnext , |\-Q0,@Qnext
|
|
|
2150 => |\-Q0,@Qnext
|
|
|
2151 |-(P0,~Q0),@Pnext
|
|
|
2152 |-(P0,Q0),@(Pnext,~Qnext)
|
|
|
2153 example
|
|
|
2154 |- ~(q & ~p) =>
|
|
|
2155 |\- q,~p,empty
|
|
|
2156 |- empty,~(q,~p)
|
|
|
2157 |\- empty(q),~p,~empty =>
|
|
|
2158 |- q,p
|
|
|
2159 |- ~q
|
|
|
2160 |\- q,@(q & ~p) =>
|
|
|
2161 |- ~q
|
|
|
2162 |- q, @~(true & ~p)
|
|
|
2163 Anther problem is Empty/More state.
|
|
|
2164 An interval can be empty/~empty
|
|
|
2165 ~(empty,P) -> ~empty;~P this is funny
|
|
|
2166 |- ~(empty,P) <-> |\- empty,P
|
|
|
2167 ~P,~(empty,P),empty is Ok
|
|
|
2168 This means false transision has separate Empty flag
|
|
|
2169 empty,(P&Q) -> empty,P,Q
|
|
|
2170 Global variables maps
|
|
|
2171 local variable state diagram -> {true, false}
|
|
|
2172 How to calculate it comformity?
|
|
|
2173
|
|
|
2174 Thu May 16 12:54:27 BST 1991
|
|
|
2175
|
|
|
2176 Decomposition Rule for Model Checking
|
|
|
2177 ~ , ; & @
|
|
|
2178 Failure Set
|
|
|
2179 Success Set
|
|
|
2180 ?-de(Proposition,Now,Next).
|
|
|
2181
|
|
|
2182 de((P,Q),(NP,NQ),(XP,XQ),F) :- de(P,NP,XP,F),de(Q,NQ,XQ,F).
|
|
|
2183 de((P;Q),Now,Next,F) :- de(P,Now,Next,F).
|
|
|
2184 de((P;Q),Now,Next,F) :- de(Q,Now,Next,F).
|
|
|
2185 de(~P,Now,Next,(FN,FX)) :- de(P,FN,FX,(Now,Next)).
|
|
|
2186 de(@P,true,P,(FN,FX)) :- de(P,FN,FX,(Now,Next)). % weak?
|
|
|
2187 de((P&Q),(PN,Now),Next,F) :- % empty case
|
|
|
2188 de(P,PN,true,PF),de(Q,Now,Next).
|
|
|
2189 de((P&Q),Now,Next,F) :- % non empty case
|
|
|
2190 de(P,PN,true,PF),de(Q,Now,Next).
|
|
|
2191
|
|
|
2192 Now is allways classical/local.
|
|
|
2193
|
|
|
2194 Using Binary Decision Tree on Interval Variable
|
|
|
2195
|
|
|
2196 <t>P = true & P
|
|
|
2197 [t]P = ~<t>~P = ~(true & ~P)
|
|
|
2198 while i do j = i-> j&(while i do j) ; empty
|
|
|
2199
|
|
|
2200 so everything is & and ~ and ; and ,.
|
|
|
2201
|
|
|
2202 Formula = { Interval Variable, Local Variable, connectives }
|
|
|
2203
|
|
|
2204 P = set of BDT on Interval Variables
|
|
|
2205 P
|
|
|
2206 /\
|
|
|
2207 P ~P
|
|
|
2208 There is only a finite number of interval variables.
|
|
|
2209
|
|
|
2210 Clausal Form:
|
|
|
2211 P :- x ; y ; P.
|
|
|
2212 P :- empty.
|
|
|
2213
|
|
|
2214 P
|
|
|
2215 x
|
|
|
2216 /\
|
|
|
2217
|
|
|
2218 it is better to make BDT primitives...
|
|
|
2219
|
|
|
2220 variablesBDT
|
|
|
2221 compBDT
|
|
|
2222 andBDT
|
|
|
2223 orBDT
|
|
|
2224 negBDT
|
|
|
2225 hashBDT
|
|
|
2226
|
|
|
2227 Mon May 20 14:24:59 BST 1991
|
|
|
2228
|
|
|
2229 ITL decomposition Rule for Model Checker
|
|
|
2230
|
|
|
2231 choices
|
|
|
2232
|
|
|
2233 interval is finite / infinite
|
|
|
2234 interval is open / close
|
|
|
2235 interval is empty / non-empty
|
|
|
2236
|
|
|
2237 ITL finite/close and has empty
|
|
|
2238
|
|
|
2239 p,q
|
|
|
2240 p;q
|
|
|
2241 ~p
|
|
|
2242 p&q
|
|
|
2243
|
|
|
2244 local variable
|
|
|
2245 non local variable
|
|
|
2246
|
|
|
2247 ~(true & ~p)
|
|
|
2248
|
|
|
2249 s0
|
|
|
2250 Success: nil
|
|
|
2251 Failure: true & ~p
|
|
|
2252
|
|
|
2253 decompositon( Formula , Local State, Next Intervals )
|
|
|
2254 Formula -> (Local-0, empty);
|
|
|
2255 (Local-1, ~empty) & Next Intervals ( with eventuality )
|
|
|
2256 ~empty contains eventuality (OK?)
|
|
|
2257
|
|
|
2258 local variable
|
|
|
2259 p -> p,empty ; (p,~empty & true)
|
|
|
2260 P & Q -> (empty,P,Q); ( empty,P & ~empty,Q ); ( ~empty, P & Q )
|
|
|
2261
|
|
|
2262 local part should have standard form
|
