2001-07-10
λ. dRuby
ちょっと苦戦。リモートから取ってきたDRbObjectを引数に同じリモートのメソッドに渡す場合とかに元のオブジェクトに差し替えて呼び出したり出来ないのかなぁ?
λ. Delphi 6 Personal が無料 (foolより)
素晴らしい!
λ. Gimp-Ruby 0.5.0
0.5.0を公開。DRb方面ではまり気味。
λ. 帰り
まだ2時半頃だったのに帰りのバスが混んでてビックリした。中学と高校の方の授業が学期末で早く終るようになったのかな。まあいいや。
λ. 『Rubyを256倍使う本 無道編』 青木峰郎
を買った。
λ. dRuby
複数の値を返そうとしてはまった。配列は、含まれるオブジェクトがdump出来ないとdumpに失敗するので、dump出来ないオブジェクトが一つでも含まれていると、配列自体がDRbObjectになっちゃう… (T_T)
λ. Rouge
もうちょっと実装を進めてから公開しようと思っていたんだけど、情報処理TAの清水さんが「すっごく興味がある」との事なので、ちょっと恥ずかしいけど、メールで送ってみる。
まあ、JavaでもCでも大抵の言語ならLispは実装できると思います。そういえば、「記号処理プログラミング」のSAかTAの人で、「Javaで実装しようとした事がある」と言ってた人がいたな〜 個人的にはJavaは「ちょっと勘弁」だけど。
λ. ところで、Raccをマスターしたら、今度はPascal辺りの処理系を作ってみたいなり。
2006-07-10
λ. アーサー空白の１５年間を語る
うはwww カプコン最高です。(あろはさんのmixi日記より)
λ. めがまり (3)
幽々子ステージを何度かプレイし、E缶を四個収集した。
紫を倒せた。やっぱ、時間がかかるとそれだけ落ちる機会も増えるので瞬殺するのが良い。まず、開始直後にフォースクライシスを三発当てて三分の一くらい削る。藍と橙はリンカネーションゴーストを使いつつ相手の位置に応じてメンタルサクリファイスと紅色マジックも使い瞬殺。紫が姿を現したら紅色マジックとリンカネーションゴーストとメンタルサクリファイスを同時に使って一気にダメージを与える。本当はフォースクライシスをもっと活用できるといいんだけどね……
萃香はだいぶ楽。小さい萃香が集まって大きな萃香になった瞬間に紅色マジックを発射し、即座にリンカネーションゴーストに切り替えて発動しながら接近。
マリサランド版魔理沙は苦手。紅色マジックで速攻でダメージを与える。八頭身になった後は更に苦手。落ちてくるブロックがどうしても避けられないときがあるし、マスタースパークと突進の判断が遅れて避けるのに失敗することもあり。E缶を一個使ってしまう。
四季映姫ステージは、変な乗り物にのったウサギが上から降りてくるところが苦手。ボスにたどり着くまでに結構ダメージを受けてしまう。四季映姫は上から降ってくる塔婆(?)を見落として大ダメージを受けてしまいがち。通常ショットとメンタルサクリファイスである程度ダメージを与えたら、あとは上海人形まかせ。またE缶を一個使ってしまう。
お次はお約束のボスラッシュだが、ボスの弱点をまだ良くわかっていないので、あっさり撃沈。しょぼーん。
E缶四個のパスワード
● ●● ● ● ● ● ● ●
2007-07-10
λ. ヘッダにしかない関数
mkmf.rb を濫用して調べてみる([ruby-dev:31176])。 ささださんが「他にも、いろいろあるようですね」と言っていたが、本当に色々あるなw
λ. 油売り算
キミならどう書く 2.0 - 2007 - その 1。 どうせHaskellプログラムとかは誰か書くだろうから、モデル検査で解を探してみる。「プログラムを書け」という問題の回答にはならないけど、プログラムなんか書かずに済むのなら書かないほうが良いだろう。
モデル検査ツールにも色々あるのだけど、いつも使っているNuSMVだと変数別に規則を書かなくてはならないのが面倒だったので、今回はよりプログラミング言語っぽい記述が可能なSpinに初挑戦してみた。
Spin(Promela)でモデルを記述すると以下のような感じになる。 aburaというプロセスが非決定的に油を移している。
#define A 10
#define B 7
#define C 3
int a = 10
int b = 0
int c = 0
inline move(from, to, cap)
{
atomic{
if
:: from > 0 && to < cap ->
if
::from+to<cap -> to = from+to; from = 0
::else -> from = from+to-cap; to = cap
fi
:: else -> skip
fi
}
}
active proctype abura()
{
do
:: true -> move(a, b, B)
:: true -> move(a, c, C)
:: true -> move(b, a, A)
:: true -> move(b, c, C)
:: true -> move(c, a, A)
:: true -> move(c, b, B)
od
}
で、ここで何を検証するかというと、「任意有限ステップ後に a=5 かつ b=5 の状態に到達しない」こと。これをSpinにかけてやると、本当に到達しないなら検証に成功し、もし到達する可能性があるなら「反例」として「到達するパス」を教えてくれる。
というわけで、XSpinで「!<>(p && q)」を検査。 ただし、ここで p と q は以下のような定義。
#define p (a==5) #define q (b==5)
そうすると、「Verification Result: not valid」とか言われるので、「Run Guided Simulation」で「Run」を選んで反例のトレース見てみる。
preparing trail, please wait...done Starting abura with pid 0 spin: couldn't find claim (ignored) 2: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] 4: proc 0 (abura) line 13 "pan_in" (state 2) [(((a>0)&&(b<7)))] 5: proc 0 (abura) line 16 "pan_in" (state 6) [else] 6: proc 0 (abura) line 16 "pan_in" (state 7) [a = ((a+b)-7)] < 6: proc 0 (abura) line 16 "pan_in" (state 8) [b = 7] < 8: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 10: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 11: proc 0 (abura) line 16 "pan_in" (state 22) [else] 12: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 12: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 14: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 16: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 17: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 17: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 17: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 19: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 21: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 22: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 22: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 22: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 24: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 26: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 27: proc 0 (abura) line 16 "pan_in" (state 22) [else] 28: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 28: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 30: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 32: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 33: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 33: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 33: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 35: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 37: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 38: proc 0 (abura) line 16 "pan_in" (state 22) [else] 39: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 39: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 41: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 43: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 44: proc 0 (abura) line 16 "pan_in" (state 86) [else] 45: proc 0 (abura) line 16 "pan_in" (state 87) [c = ((c+b)-7)] < 45: proc 0 (abura) line 16 "pan_in" (state 88) [b = 7] < 47: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 49: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 50: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 50: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 50: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 52: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 54: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 55: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 55: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 55: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 57: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 59: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 60: proc 0 (abura) line 16 "pan_in" (state 22) [else] 61: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 61: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 63: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 65: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 66: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 66: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 66: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 68: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] spin: trail ends after 69 steps #processes: 1 69: proc 0 (abura) line 21 "pan_in" (state 16) 1 processes created
思ったよりもだいぶ長いトレースが出てきたけど、 代入文を追いかけてみると、こんな感じになっている。
a から b に 7 升移す ((10,0,0) → (3,7,0)) a から c に 3 升移す ((3,7,0) → (0,7,3)) b から a に 7 升移す ((0,7,3) → (7,0,3)) c から b に 3 升移す ((7,0,3) → (7,3,0)) a から c に 3 升移す ((7,3,0) → (4,3,3)) c から b に 3 升移す ((4,3,3) → (4,6,0)) a から c に 3 升移す ((4,6,0) → (1,6,3)) c から b に 1 升移す ((1,6,3) → (1,7,2)) b から a に 7 升移す ((1,7,2) → (8,0,2)) c から b に 2 升移す ((8,0,2) → (8,2,0)) a から c に 3 升移す ((8,2,0) → (5,2,3)) c から b に 3 升移す ((5,2,3) → (5,5,0))
というわけで、探索をプログラムせずとも答えを得れたと。 これくらい単純な例だと探索を自分でプログラムしても大したことはないけど、扱う状態遷移系が複雑になると、自分で探索を行うプログラムを書くのは結構しんどいことになる。 そんな時にはモデル検査は非常に便利。
詳しくは4日で学ぶモデル検査 (初級編) (CVS教程 (1))(産業技術総合研究所システム検証研究センター)でもどうぞ(読書記録)。
ところで、ところで使ってみて知ったのだけど、Spinでモデル検査するときって、一回C言語のコードを出力してコンパイルして、それを使って検査しているんだな。 なんというか、それだけやっても十分割りにあうということか。
追記
masateruさんという方のmixi日記にて、別の回答が紹介されている。 assertを使う方法など、初心者の私には大変勉強になりました。
2008-07-05追記
「NuSMVだと変数別に規則を書かなくてはならない」と書いたが、これは間違い。これを書いた時点では ASSIGN で init(x) と next(x) に対する代入という形で書く方法しか知らず、その場合には変数別に規則を書く必要があるが、実際にはTRANSを使って遷移関係を直接記述する方法もあり、その場合にはこういった問題は無い。
2008-07-10
λ. “Reasoning support for Semantic Web ontology family languages using Alloy” by Hai H. Wang, Jin Song Dong, Jing Sun and Jun Sun
Semantic Web (SW), commonly regarded as the next generation of the Web, is an emerging vision of the new Web from the Knowledge Representation and the Web communities. To realize this vision, a series of techniques has been proposed. Semantic Web Ontology Langauge (OWL) and its extension Semantic Web rule Language (SWRL) and Semantic Web Logic Language (SWRL-FOL) are some of the most important outputs from the SW activities. However the existing reasoning and consistency checking tools for those languages are primitive. This paper proposes using the existing formal modelling tool, in particular Alloy, to provide an automatic reasoning service for the Semantic Web ontology family languages (OWL/SWRL/SWRL-FOL).
ふと、「OWL から Alloy に変換して Alloy Analyzer を推論に活用したら面白いんじゃなかろうか。両方とも二項関係がベースだし、Semantic Web では厳密な推論よりは実用性が重要から、相性良さそうだし」とか思ったのだけど、探したらやってる人は既がいた。残念。
Alloyへの変換は straight forward だけど、当時の Alloy は今と少し違っていて、extend した signature 同士を排反(disjoint)にするために、明示的に disj を書く必要があったようだ。
ψ 咳 [dRubyの二件なんですが、前者はRWiki公式サイトのdRuby開発版の ページの1.3.3にかいたDRbObje..]