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