諸事情からwindowsでmobility workbenchを動かさないといけなくなった．smlnjのwindowsバイナリをからサイトしてきて，READMEの通りにやったらうまくいかなかったのでメモ． まずTextIO.inputLineの戻り値がoptionな感じになってるのでそれを全部修正(case文…

あえて教科書とかを見ないでやってみる． agent Constant1(x,a) = 'x<a>.Constant1(x,a) agent Constant2(x,a,b) = 'x<a,b>.Constant2(x,a,b) agent Cons(cons) = cons(r,hd,tl).(Cons(cons) | Constant2(r,hd,tl)) agent Head(head) = head(r,list).list(hd,tl).(He</a,b></a>…

Bisimulation は，お互いがお互いを simulate するものかと思っていたのだけど，そうじゃなかったらしい． つまり， P と Q が bisimilar であることを判定するのに， P が Q を simulate し，かつ Q が P を simulate することを確認すればいい，というわけ…

Mobility Workbench もどきを作っている。もちろん Haskell で。1日とちょいでとりあえずステップ実行まではできるようになった。 あとは structural congruence を使った簡単化とかをやれば(ステップ実行に関してだけは)本家に遜色ない。 > agent P(a,b) = …

またも id:syd_syd さんに教えていただく。 しばらく遊んでいたところ Sigma, Bsigma, Pi の使い方は理解できたが、その意味はわかっていない。やっぱり本を読んで勉強しないといけない。 直感的には、 Sigma は送信データにマッチし、 Bsigma はプロセス内…

Hennessy-Milner logic は、プロセスの性質を表現するための論理式。ちょっと複雑な性質を表現するためには Recursive Hennessy-Milner logic を使うことになる*1。これに関する資料が少ないので一応。 id:syd_syd さんに非常に感謝。 π計算のモデルチェッカ…

サンプルプログラムはほぼ完成。 ただ、 windowOnIdle で登録したアクション(消費者)が、なかなか実行されないという問題点が。複数のスレッドで生産者と消費者がひとつのキューを扱うのだけど、 idle イベントが発生した段階でキューにデータがないと、なか…

π計算でプログラム書くのは死ぬほどめんどくせぇぇ…。絶対に、なんかのツールによるサポートが必要と思われる。

π計算でキャンセルできるファイルコピーユーティリティを書く、というのをやっている。ちょっとした頭の体操。 Haskell を勉強し始めた頃と近いものを感じるかもしれない。 非同期π計算だと、送信をしたあとには何もできないという制約がつく。チャネル a で…

Pict をビルドしようとしましたが、ライブラリのビルドに失敗しました。どうしよ、粘るべきかな…。 Building Std/Random.px from Std/Random.pi Uncaught exception: Failure("int_of_string") make: *** [Std/Random.px] Error 2てか Pict って X も扱える…

タイトルの通り。ややくじけそうである。 昨日から、自分で定義したデータ型を使って書いた構文を、Template Haskell でコンパイル時に Haskell ソースに変換するというようなメタプログラミングをしている。とはいえ、今日は一日遊んできたからほとんど何も…

なんだかよくわからないながらも、 Mobility Workbench の使い方と Hennessy-Milner logic の勉強をしています。 id:syd_syd さんに貸してもらった Reactive Systems という本は、(今のところは)わかりやすくていい感じ。最後までこのペースで進めればなと思…

できたー。値をチャネルに投げ込むときは、がっちり型を書くほうが無難みたいです。 module Main where import PiMonad hiding (piStart) import PiMonad.IO.Console import PiMonad.Channel import PiMonad.Network main = piStart False Nothing mainPr ma…

なぜだめなんだろうか。眠くてもうだめ。 main = piStart False Nothing mainPr mainPr :: Maybe (I (), NewP) -> PiMonad () mainPr _ = do s <- new fork $ fib 10 s s' <- recv s cout

やべぇ、意味わかんない。bisimulation という関係は常識なのだろうか。少なくともこの本には説明がない気がする…。 example a.(b.stop + b.stop) + a.b.stop 〜bis a.b.stop because the following is a bisimulation: a.(b.stop + b.stop) + a.b.stop a.b.…