Mercurial > hg > Applications > Lite

comparison problems @ 10:f2aa38ce0787

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add state display.
author kono
date Fri, 19 Jan 2001 23:14:00 +0900
parents 9b86eb10b61c
children 66d0522d46e8
comparison
equal deleted inserted replaced
9:95897517e464 10:f2aa38ce0787
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
1 Fri Jan 19 07:48:59 JST 2001 42 Fri Jan 19 07:48:59 JST 2001
2 43
3 Streett ∩_i []<>L_i ⊃ <>[]U _i 44 Streett ∩_i []<>L_i ⊃ <>[]U _i
4 Rabin ~(∩_i []<>L_i ⊃ <>[]U _i) 45 Rabin ~(∩_i []<>L_i ⊃ <>[]U _i)
5 46