Alloyでパズル (12) ７人の写真

7224 ワード
AlloyAnalyzer どう書く どう書く テキストリンク

正直まだseqがうまく使えないので、練習に使えそうなパズルを。

問題

男の子3人(与之助、一平、大介)、女の子4人(めぐみ、ゆかり、まどか、みゆき)の7人の園児が並んで写真を撮ることになった。
このうちの4人が次のような注文をつけた。

与之助 「両隣は女の子がいい」
一平 「女の子の隣はいや」
めぐみ 「ゆかりの隣がいい」
まどか 「右端がいい」

これらの注文がすべて叶ったとすると、左端にいたのは誰？

出典: 新作論理パズル77 小野田 博一

リスト

できたけれど、読みやすい記述とは言いがたい。
これならutil/orderingを使った方が素直に読めそうだ。
もっとうまく書けないものだろうか。

abstract sig Child {}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

one sig Photo { order: seq Child } {    // 左から順に
    order[univ] = Child                 // 全員

    order[order.@Yonosuke.(prev+next)] in Girl  // 与之助 「両隣は女の子がいい」
    no order[order.@Ippei.(prev+next)] & Girl   // 一平   「女の子の隣はいや」
    Megumi in order[order.@Yukari.(prev+next)]  // めぐみ 「ゆかりの隣がいい」
    order.last = Madoka                         // まどか 「右端がいい」
}

run {} for 7

結果

結果例
┌──────────┬───────────┐
│this/Photo│order      │
├──────────┼─┬─────────┤
│Photo⁰    │0│Ippei⁰   │
│          ├─┼─────────┤
│          │1│Daisuke⁰ │
│          ├─┼─────────┤
│          │2│Miyuki⁰  │
│          ├─┼─────────┤
│          │3│Yukari⁰  │
│          ├─┼─────────┤
│          │4│Megumi⁰  │
│          ├─┼─────────┤
│          │5│Yonosuke⁰│
│          ├─┼─────────┤
│          │6│Madoka⁰  │
└──────────┴─┴─────────┘

左端は一平になる（大介しか一平の隣になれず、右端はまどかなので）

check { Photo.order.first = Ippei } for 7

util/orderingでもやってみる

記述はシンプルで読みやすくなったが..

open util/ordering [Child]

abstract sig Child {}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

fact {
    Yonosuke.(prev+next) in Girl    // 与之助 「両隣は女の子がいい」
    no Ippei.(prev+next) & Girl     // 一平   「女の子の隣はいや」
    Megumi in Yukari.(prev+next)    // めぐみ 「ゆかりの隣がいい」
    last = Madoka                   // まどか 「右端がいい」
}

run {}

Evaluator か Tree View でないと結果が見られない。
しかもたどりながら読まないとならない。
残念。

first
┌──────┐
│Ippei⁰│
└──────┘
Child<:next
┌─────────┬─────────┐
│Daisuke⁰ │Miyuki⁰  │
├─────────┼─────────┤
│Ippei⁰   │Daisuke⁰ │
├─────────┼─────────┤
│Megumi⁰  │Yukari⁰  │
├─────────┼─────────┤
│Miyuki⁰  │Megumi⁰  │
├─────────┼─────────┤
│Yonosuke⁰│Madoka⁰  │
├─────────┼─────────┤
│Yukari⁰  │Yonosuke⁰│
└─────────┴─────────┘
last
┌───────┐
│Madoka⁰│
└───────┘

（ただのnextだと「integer/nextとordering/nextのどっちかわかんない」と言われる）

表示のためChildにleft,rightを追加して良しとするか。

open util/ordering [Child]

abstract sig Child {left,right: lone Child}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

fact {
    right = next                    // 並び順の「次」は右側
    left = prev

    Yonosuke.(left+right) in Girl   // 与之助 「両隣は女の子がいい」
    no Ippei.(left+right) & Girl    // 一平   「女の子の隣はいや」
    Megumi in Yukari.(left+right)   // めぐみ 「ゆかりの隣がいい」
    Madoka.right = none             // まどか 「右端がいい」
}

run {}

どっちも使わない

seqもutil/orderingも使わなくても書ける。
反射推移閉包*を除けば、素直に読めるだろう。
（c.*rightは(c + c.right + c.right.right + ..)と思えばだいたいOK。
　c.^rightなら(c.right + c.right.right + ..)になる。）

abstract sig Child {left,right: lone Child}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

fact {
    one c:Child | c.*right = Child  // 左端からだけ、右にたどると全員いる
                                    // some だと輪になる場合も含む
                                    // all なら輪になる
    left = ~right                   // 左は右の反対

    Yonosuke.(left+right) in Girl   // 与之助 「両隣は女の子がいい」
    no Ippei.(left+right) & Girl    // 一平   「女の子の隣はいや」
    Megumi in Yukari.(left+right)   // めぐみ 「ゆかりの隣がいい」
    Madoka.right = none             // まどか 「右端がいい」
}

run {}

seq版を書き換えてみる

記述を長くしていた部分を置き換えてみる。

abstract sig Child {}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

one sig Photo { order: seq Child } {    // 左から順に
    order[univ] = Child                 // 全員
}
fact {
    let order = Photo.order {
        order.Yonosuke.(prev+next).order in Girl  // 与之助 「両隣は女の子がいい」
        no order.Ippei.(prev+next).order & Girl   // 一平   「女の子の隣はいや」
        Megumi in order.Yukari.(prev+next).order  // めぐみ 「ゆかりの隣がいい」
        order.last = Madoka                       // まどか 「右端がいい」
    }
}

run {} for 7

多少読みやすくはなったが、まだ与之助〜めぐみの.orderがわかりづらい気が..

頻出する「隣」をくくり出して良しとするか？

abstract sig Child {}
abstract sig Boy, Girl extends Child{}
one sig Yonosuke, Ippei, Daisuke extends Boy {}
one sig Megumi, Yukari, Madoka, Miyuki extends Girl {}

one sig Photo { order: seq Child } {    // 左から順に
    order[univ] = Child                 // 全員
}
let neighbor[child] = Photo.order[Photo.order.child.(prev+next)]
fact {
    Yonosuke.neighbor in Girl     // 与之助 「両隣は女の子がいい」
    no Ippei.neighbor & Girl      // 一平   「女の子の隣はいや」
    Megumi in Yukari.neighbor     // めぐみ 「ゆかりの隣がいい」
    Photo.order.last = Madoka     // まどか 「右端がいい」
}

run {} for 7

まとめ

結局seqをうまく使えないのであった..

参考