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

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

# 問題

> 男の子3人(与之助、一平、大介)、女の子4人(めぐみ、ゆかり、まどか、みゆき)の7人の園児が並んで写真を撮ることになった。
このうちの4人が次のような注文をつけた。
>
与之助 「両隣は女の子がいい」
一平   「女の子の隣はいや」
めぐみ 「ゆかりの隣がいい」
まどか 「右端がいい」
>
> これらの注文がすべて叶ったとすると、左端にいたのは誰？
>
> 出典: 新作論理パズル77 小野田 博一

# リスト

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

```alloy
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
```
# 結果

```txt:結果例
┌──────────┬───────────┐
│this/Photo│order      │
├──────────┼─┬─────────┤
│Photo⁰    │0│Ippei⁰   │
│          ├─┼─────────┤
│          │1│Daisuke⁰ │
│          ├─┼─────────┤
│          │2│Miyuki⁰  │
│          ├─┼─────────┤
│          │3│Yukari⁰  │
│          ├─┼─────────┤
│          │4│Megumi⁰  │
│          ├─┼─────────┤
│          │5│Yonosuke⁰│
│          ├─┼─────────┤
│          │6│Madoka⁰  │
└──────────┴─┴─────────┘
```
左端は一平になる（大介しか一平の隣になれず、右端はまどかなので）

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

# `util/ordering`でもやってみる

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

```alloy
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`を追加して良しとするか。

```alloy
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 {}
```

![7photo.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/838ecaef-ddd3-aae0-e2fb-f308e47924fa.png)

# どっちも使わない

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

```alloy
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 {}
```
![7photo-2.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/6f99abd9-9185-bdae-d99c-a781615c2107.png)

# `seq`版を書き換えてみる

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

```alloy
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`がわかりづらい気が..

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

```alloy
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`をうまく使えないのであった..

# 参考

- gist/umejam : [7人の写真2.als](https://gist.github.com/umejam/1301094)