日々の流転

λ. 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側では「セマフォを獲得したまま、クリティカルセクションから出てこないプロセス」が問題になっていたので、いきなりこの解答が出てきても……

練習問題

後で書く。