付録A.5 の小さなケーススタディからA.5.1 の Unix ファイルシステムは 10個のアドレスを扱うというのが Alloy の設定でデフォルト 4bit までしか扱えないので断念(設定で増やせると思いますが)。 A.5.2 の鉄道のスイッチングをやってみます。 A.5.2 (a), (b…

付録A.4 のメタモデル続き。 A.4.2 状態機械の模倣関係 状態機械の遷移にラベルをつけて、遷移経路をラベルの配列の「トレース」で表現する sig Label { trans: State-> State } { one trans } sig State {} sig StateMachine { states: some State, first: …

付録A.4 のメタモデルに入ります。 A.4.1 状態機械の定義 ライブロックの定義は「全ての状態からある状態に到達できる経路がある」かつ「そのある状態に到達しない無限の経路もある」という意味に読みとったのですがちょっと違うかもしれませんね。 sig Stat…

付録A.3 の古典的パズル終わりました。まだ A.4、A.5、A.6 があります…… A.3.6 外科医のグローブ まず普通にモデリングしてみてグローブを重ねて使わないと解がないことはわかるのと、内側のグローブ(医者の手に触れる面)は変更しないほうが利用効率がいいこ…

付録A 練習問題続きます。A.3 の古典的パズル最後の問題です。 A.3.6 外科医のグローブ 手術用のグローブが2つしかないのに3人の手術をしないといけない、どうするか、という問題 問題自体は既知だったので重ねないといけないのはわかったのですが、知らない…

付録A 練習問題続きます。A.3 の古典的パズル続きです。 A.3.4 Halmos の握手問題 カップルが集まったパーティで Alice 以外の全員が握手した回数がばらばらの時に、Alice のパートナーの Bob が握手した回数は何回か？ この問題は Alloy でモデリングしてて…

付録A 練習問題続きます。A.3 の古典的パズルに入ります。 A.3.1 驚くような三段論法 まず歌詞の通りにモデル化してみる sig Person { like: set Person } pred doris_day (i, he: Person) { // みんな彼(he)が好き all p: Person | he in p.like // 彼(he)…

付録A 練習問題続きます。 A.2.3 囚人の割り当て 刑務所で異なるギャングのメンバーを同じ監房に入れないようにする 問題には書いてありませんが、空っぽの Cell(監房)が表示されも無意味なので fact で全ての Cell には誰かが割り当てられているものとして…

付録A 練習問題まだまだ続きます。 A.2.2 アドレス帳の不変条件を保存する (a) 不変条件の述語 inv について説明せよ 「Book b においてすべての Name はそれ自身から addr でたどれるない。つまり addr で循環する関係は存在しない。また addr に存在する N…

付録A 練習問題続きます。今日は雨で時間がなかったので1つだけ。 A.2.1 (c) 通話転送機能をくみこむ 転送先が接続元だったら？と思いましたが、相互の接続は禁止していないのでそのままにしました。うーん、こういう細かいところ悩みますね。 module exerci…

付録A 練習問題続きます。 A.1.10 の地下鉄路線のモデリングの (f), (g), (h) なんですが、あれ多分それ以前の問題で出てきた記述を使ってやれってことだったんですね。というわけで別解を作りました。インスタンスを減らすために駅の順番のヒントは少し増や…

付録A 練習問題続きます。ようやく A.1 は終わりそうです。 (f), (g), (h) はまとめて。(g) の「順番のヒント」という表現や (h) の「対称的な解が数多くある」というところから、解答はこういう書き方じゃないと思います(これだとインスタンスは1つだけ)。…

付録A 練習問題続きます。先はまだまだ長いです。 A.1.11 地下鉄をモデリングする (続き) 一昨日書いたのだと line が二項関係になっていたので少し変更 (a) 路線 line にある駅の集合が S 「路線 line」というのがどういう意味かよくわからないので単に Sta…