報國挺身日記 このページをアンテナに追加 RSSフィード

2011/10/25

[] ヤギ、キャベツ、狼 22:09

前回に続いて、抽象によるソフトウェア設計−Alloyではじめる形式手法− の練習問題を考える。


A.3.5 「ヤギ、キャベツ、狼」

一人の農夫が、一頭のヤギと、一玉のキャベツと、一匹の狼を川の向こう側に運びたい。しかし彼のボートには一度に一つしか載せるスペースがない。もしヤギをキャベツと一緒にしたまま農夫が離れると、ヤギがキャベツを食べてしまう。もしヤギと狼を一緒にしておくと、ヤギが食べられてしまう。彼はどうすべきか? Alloyで解け。

(ヒント: Alloyの標準ディストリビューションにはモジュールutil/orderingがあり、全順序を定義できる。)


util/orderingの使い方を知らなかったが、他のサンプルプログラムを見てわかった。firstとlastに最初と最後の状態を指定、ある状態から次の状態の変化はnextで指定すればよいらしい。

各状態で可能な農夫の動作は四通りある。(手ぶらで移動、三通りの荷物のどれかと一緒に移動)

nextの状態として、この四通りの状態を選言で並べればよい。

open util/ordering [S]
enum 岸 {こちら, あちら}

-- 状態
sig S {
  人: 岸,
  狼: 岸,
  山羊: 岸,
  キャベツ: 岸
} {
  -- 安全な状態の条件
  狼 != 山羊 or 人 = 狼
  山羊 != キャベツ or 人 = 山羊
}

one sig スタート extends S {} {
  人 = こちら
  狼 = こちら
  山羊 = こちら
  キャベツ = こちら
}
one sig ゴール extends S {} {
  人 = あちら
  狼 = あちら
  山羊 = あちら
  キャベツ = あちら
}

-- 境界条件
fact {
  first = スタート
  last = ゴール
}

-- 移動
fact move {
  all a: S, b: a.next {
    (b.人 != a.人) and (
      (b.狼 = a.狼 && b.山羊 = a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 != a.狼 && b.山羊 = a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 = a.狼 && b.山羊 != a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 = a.狼 && b.山羊 = a.山羊 && b.キャベツ != a.キャベツ)
    )
  }
}

pred show {}
run show for 8

パズル自体の答えは、川渡り問題に載っている。

2011/10/22

[] 驚くような三段論法 12:57

「抽象によるソフトウェア設計」を読んだ。

内容が難しい上にAlloyの記述形式に馴染めないので、読むのに時間が掛かった。

説明のための例としてアドレス帳を取り上げているのだが、アドレス帳の仕様記述には何の興味も湧かないので退屈だった。説明する側からすれば、ものすごく合理的で適切な例なんだろうと思うが。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−


付録に載っている練習問題を考えてみる。

A.3.1「驚くような三段論法」

Doris Dayの歌

Everybody loves my baby

but my baby don't love nobody but me.

これは「私は私の彼だ」を含意していることになる。検査せよ。

sig 人 {
  愛する: set 人
}
sig 彼 in 人 {}
one sig 私 in 人 {}

pred 歌の主張 {
  all x: 人 | 彼 in x.愛する                    -- Everybody loves my baby
  all b: 彼 | no (b.愛する & (人 - 私))     -- but my baby don’t love nobody but me.
}

fact { #彼 > 0 }
check { 歌の主張 => 私 in 彼 }

Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20

162 vars. 18 primary vars. 243 clauses. 114ms.

No counterexample found. Assertion may be valid. 11ms.

となって反例は見つからない。

fact {...}を消して、彼が存在しない場合も許すと、歌の主張に意味がなくなるので反例が生じる。