農夫 山羊 キャベツ 狼

  • 1
    いいね
  • 0
    コメント

Alloy本の練習問題にある古典的なパズル

農夫が山羊1頭,キャベツ1玉,狼1頭を川の向こう岸に連れていきたい
山羊とキャベツを一緒にしちゃって農夫が離れると山羊がキャベツ食べちゃう
狼と山羊を一緒にしちゃって農夫が離れると狼が山羊を食べちゃう
舟には農夫以外にもうひとつしか乗せる余裕なし

あー小学生のころに...
という古から伝承されてきたパズルです.

解いた

Farmer.als
module Test

open util/ordering[Time]

sig Time{}

abstract sig 乗組員{}
one sig 農夫 extends 乗組員{}
one sig キャベツ extends 乗組員{}
one sig 山羊 extends 乗組員{}
one sig  extends 乗組員{}

abstract sig 場所{
    居る: 乗組員 -> Time
}
one sig 彼岸 extends 場所{}
one sig 此岸 extends 場所{}
one sig  extends 場所{
    : (彼岸 + 此岸) one -> Time
}

fact 常に一箇所に存在する{
    all t: Time, x: 乗組員 | one 居る.t.x
}

fact ヤギとキャベツ{
    all t: Time | no p: 場所 | (山羊 + キャベツ) in p.居る.t and 農夫 not in p.居る.t
}
fact ヤギと狼{
    all t: Time | no p: 場所 | (山羊 + ) in p.居る.t and 農夫 not in p.居る.t
}
fact 定員{
    all t: Time - first | #.居る.t <= 2
}

pred init(t: Time){
    (農夫 + 山羊 + キャベツ + ) in 此岸.居る.t
    ..t in 此岸
}
pred done(t: Time){
    (農夫 + 山羊 + キャベツ + ) in 彼岸.居る.t
}

fun 対岸(p: 場所 - ) : one 場所 -  {
    (場所 - ) - p
}

fact Traces{
    first.init
    all t: Time - last | let t' = t.next {
        -- 農夫が乗らなきゃ移動はない
        農夫 in .居る.t' => ..t' = 対岸[..t] else ..t' = ..t
        -- 乗り換え
        let 舟着岸 = ..t |
            (+舟着岸).居る.t' = (+舟着岸).居る.t and 対岸[舟着岸].居る.t' = 対岸[舟着岸].居る.t
        }
    some t: Time | t.done
}

pred show {}
run show for 10 Time

シミュレーション

Timeで射影します.
あとは適当に属性っぽくメンバーを表示したりして.

Farmer.thm
<?xml version="1.0"?>
<alloy>

<view nodetheme="Martha">

<projection> <type name="Time"/> </projection>

<defaultnode/>

<defaultedge/>

<node>
   <type name="Int"/>
   <type name="String"/>
   <type name="Time"/>
   <type name="univ"/>
   <type name="&#x30ad;&#x30e3;&#x30d9;&#x30c4;"/>
   <type name="&#x5c71;&#x7f8a;"/>
   <type name="&#x72fc;"/>
   <type name="&#x8fb2;&#x592b;"/>
   <type name="seq/Int"/>
</node>

<node shape="Box" color="Yellow">
   <type name="&#x5f7c;&#x5cb8;"/>
</node>

<node shape="House" color="Blue">
   <type name="&#x821f;"/>
</node>

<node shape="Trapezoid" color="Green">
   <type name="&#x6b64;&#x5cb8;"/>
</node>

<node style="Bold">
   <set name="First" type="ordering/Ord"/>
   <set name="Next" type="ordering/Ord"/>
</node>

<node visible="no">
   <type name="&#x4e57;&#x7d44;&#x54e1;"/>
   <type name="ordering/Ord"/>
</node>

<node visible="yes">
   <type name="&#x5834;&#x6240;"/>
</node>

<edge visible="no" attribute="yes">
   <relation name="&#x5c45;&#x308b;"> <type name="&#x5834;&#x6240;"/> <type name="&#x4e57;&#x7d44;&#x54e1;"/> </relation>
</edge>

</view>

</alloy>

これで表示してみると次のような感じ.

  1. 最初は皆此岸
    2016-12-22-102634_440x352_scrot.png

  2. 農夫が山羊を連れて向岸へ
    2016-12-22-102734_440x352_scrot.png

  3. 山羊を向岸に置いて戻ってくると思ったら一回降りやがった
    2016-12-22-102757_440x352_scrot.png

  4. 今度こそ山羊を向岸に置いて戻ってきた
    2016-12-22-102925_440x352_scrot.png

  5. 農夫がキャベツを連れて向岸へ
    2016-12-22-103011_440x352_scrot.png

  6. キャベツを置いて山羊を連れて戻ってくる
    2016-12-22-103205_440x352_scrot.png

  7. 山羊を置いて狼を連れて向岸へ
    2016-12-22-103321_440x352_scrot.png

  8. 狼を置いて農夫一人で戻る
    2016-12-22-103353_440x352_scrot.png

  9. 農夫は山羊を連れて向岸へ行くと勢揃い
    2016-12-22-103421_440x352_scrot.png

  10. あらためて上陸
    2016-12-22-103529_440x352_scrot.png

でおしまい.

感想

まぁこの程度の遊びなら軽いと言える程度にはなってきた.

この投稿は Formal Method Advent Calendar 201622日目の記事です。