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