日々の流転

λ. どうせなら、国会議員も一人一票とかやめて、選挙での投票数に応じて票数を割り振るとかしたらどうだろう。この国をもっと白痴的に出来るんじゃないだろうか。…とか選挙結果を見て思った。

λ. Gimp-Ruby 0.6.1リリース

0.6.1をリリース。なかなかやりたい事にたどり着けなくてちょっとイライラしてきたので、これ以上変更する前にスナップショットをだしとこと思って。

λ. 選挙制度

こんちわっす。ははっ、やっぱ僕が最初に考えたわけじゃないのか、残念。しかし世の中には色々考えてる人がいるんだな。ところで、市場制民主主義なんかを公約にする政党って何で無いんだろ。(笑)

λ. ありゃ

irb(main):001:0> method(:p) == method(:p)
false

λ. Gimp-Ruby その2

Gimp::mainとGimp::PLUG_IN_INFOとGimp::Fuの関係は色々いじって、かえって状況が悪化してる。結局、Chain of responsibilityをRubyでどう書くかというのが本質なのかな?　まあいいや、ゆっくり考えよ。

佐野さんの6月の日記に、

酒井さんにlambdaの世界を案内される。
面白いかも。
…心に
余裕があったら勉強しよう
その他のことは本気でつまらない。

と書かれているのを見つけて元気づけられる。

λ. 歯医者

詰め物がだいぶ前に取れてしまっていたのを思い出して、歯医者に言ってきた。で、泣きたくなる。詰め物が取れた部分が虫歯になっていたのはまぁ良いとして(いや良くはないけど)、右下の親知らずがヤバイ事になっているそうだ。この親知らずが手前に傾いて生えて、その手前の奥歯を圧迫してしまっていて、その奥歯のそっち側が結構溶けてしまってるとか。で、外科的な手術が必要そうで「両方抜いて奥歯の位置に親知らずを移植する」事が可能か大学病院の先生と相談とか……

夏休み気分が一気に吹き飛んだよ。(T_T)

λ. 萩野服部研　最終発表

.

λ. MSDN AA

夏休みに入るとあんま学校に来ないだろうから、今のうちにラップトップに Virtual PC, Visio, OneNote 等をインストール。

λ. hOp

Virtual PC をインストールしたので、とりあえず hOp を動かしてみた。普通に動いた。

λ. 打ち上げ

.

λ. みどりちゃん、おたんじょうび、おめでとう

ケーキ写真

λ. Sheep と Lamb

「羊たちの沈黙」の原題は「The Silence Of The Lambs」で、「羊たち」と訳されていたのは Sheeps ではなく Lambs だったということに偶然気づいた。そういや、SheepとLambの違いって何だろうな、と思い検索したら、What's the difference between a sheep and a lamb? というページを見つけた。なるほど……

λ. 4日で学ぶモデル検査: 2日目

今日は2日目の内容をやる。

Mini Life Game

普通に何の問題も無く出来た。しかし、各変数についてのnextでほとんど同じことを何度も書かなくてはならないのが嫌だな。DEFINEで関数(というかパラメータを持つ定義)を定義することが出来れば良いのに。

ウサギちゃんとオオカミくん

値域全体に非決定的に遷移する変数RbSMとWoSMを乱数のように(?)使って他の変数を遷移させているのに、「へぇ」と思った。

最初にモデルと論理式をNuSMVに食わせたときに「specification !(rule U goal) is true」といきなり言われて焦ったが、単なる入力ミスで、それを直したら問題なくなった。それから、Splaceの初期状態としてbankAではなく0という状態を加えているのは何故だろう。以下のようにすれば状態0は不要に思えるが……

VAR
  RbSM : 0..2;
  WoSM : 0..2;
  Splace : {bankA, AtoB, bankB, BtoA};

ASSIGN
  init(RbSM) := {0,1,2};
  next(RbSM) := {0,1,2};

  init(WoSM) := {0,1,2};
  next(WoSM) := {0,1,2};

  init(Splace) := bankA;
  next(Splace) := case
                    Splace = bankA : AtoB;
                    Splace = AtoB  : bankB;
                    Splace = bankB : BtoA;
                    Splace = BtoA  : bankA;
                  esac;

並行システムと排他制御

runという{0,1}に非決定的に遷移する変数を使って二つのプロセスのスケジューリングを行っているのが面白い。Spinと比較すると、明示的なスケジューリングを行わなくてはいけないのは面倒くさいが、その分LTLや通常の状態遷移系のレベルでの理解が容易なのはメリットと言えるだろう。ただまあ、複雑な並行システムを扱うに向いてないだろうな*1。

モデルの記述ではnext(semaphore)の記述が誤っているように思う。「run = 1 & proc1_state = entering : 0;」は「run = 1 & proc1_state = exiting : 0;」の誤りだろうし、proc2についても同じ。それから、テキストの方ではproc1_stateがstate_p1と書かれていて、コードとテキストが合っていない。

それから、演習問題の解答例がNuSMV側だけ読んでいると唐突過ぎるように感じた。SPIN側では「あるプロセスがクリティカルセクションから出た瞬間にクリティカルセクションに入ることを繰り返す」ことが最後に問題になっていたのに対して、NuSMV側では「セマフォを獲得したまま、クリティカルセクションから出てこないプロセス」が問題になっていたので、いきなりこの解答が出てきても……

練習問題

後で書く。

λ. “Ricsin: Ruby にCを埋め込むシステム”笹田 耕一

を読んだ。

• 笹田耕一/笹田研の研究業績リスト