Alloyでパズル (7) 数取りゲーム、石取りゲーム

簡単なゲームを題材に、ルールの読み替えと戦略の組み込みを試そう。


# ルール

バリエーションや呼び方は色々あるが、見やすくまとまっていた [こちら](http://bokuso.blogspot.com/2014/09/blog-post.html) にあるものを基本とする。

[基本ルール]

1. １から順に連なる数字を、２人のプレイヤーが交互に言う  
    一度に言える数字は３つまで
2. 30を言った方が負け

そのままモデル化しようとすると少々書きづらいこともあり、もう少し抽象度を上げたい。
数字を使うのはおそらく道具なしで遊ぶための工夫で、意味的には次のルールと等価だろう。

[石取りルール]

1. 29個の石がある
2. ２人で交互に、１〜３個の石を取る
3. 最後の石を取った方が勝ち　（３人以上になった場合を想定し、勝者の定義に変えた）

参照先にもある通り、基本ルールのままだと簡単な必勝法がある。
ルールにある各数字は簡単に変えて、必勝法が通用するか試せるようにしたい。

# リスト

一度に取れる石の範囲はリスト内マクロとした。
その他のパラメータは、実行時にスコープ指定で与える。

```alloy
// 石取りゲーム
//
// 各プレイヤーは順に、場にある石を取る
// 一度に取れる石数の範囲は決まっている
// 最後の石を取った人が勝ち

open util/ordering [Turn]
open util/ordering [Player]

let minTake = 1     // 一度に取れる最少石数
let maxTake = 3     // 一度に取れる最多石数

sig Stone {}
sig Player {}
sig Turn {
    player: lone Player,
    stone: set Stone,
    take: set stone
} {
    no stone <=> no player
    some stone => (minTake =< #take) && (#take =< maxTake)
}

fact {
    #Stone < #Turn  // スコープ妥当性確認

    first.player = first
    first.stone = Stone
    no last.stone

    all t,t':Turn | t'=t.next => {
        t'.stone = t.stone - t.take
        some t'.stone => t'.player = (t.player=last => first else t.player.next)

        t.player = first => t.takeToWin     // 最初のプレイヤーのみ勝とうとする
    }
}

pred takeToWin[t:Turn] {
    some t.stone => let want = rem[#t.stone, add[minTake,maxTake]] {
        #t.take = max[minTake + want]
    }
}

run {} for 6 int, exactly 9 Stone, 2 Player, 10 Turn

let lastTaker = take.univ.max.player  // takeが空でない最後のTurnのplayer
先手必勝: check {lastTaker = first} for 6 int, exactly 19 Stone, 2 Player, 20 Turn
```

- 任意数のプレイヤー順を扱うために、２つめの`util/ordering`を利用した。  
この場合`first`や`last`には複数の候補があることになるが、Alloy は文脈からどの候補を指すか読み取ってくれる。  
リスト内にある`first.player = first`の場合、前者はフィールド`player`を持つ`Turn`の`first`であり、それと比較される後者は`Turn.player`と同じ型である`Player`の`first`と判断される。  
明記したい場合や文脈から読み取れない場合は`Turn<:first`と書くことで`Turn`の`first`に限定できる。  
Evaluatorで単に`first`や`last`を確認したい場合も、`Turn<:first`や`Player<:last`と指定する。
- 石の数やターン数範囲を実行時にスコープ指定するので、スコープ妥当性確認の行を入れた。  
入れてもそれほどうれしいことが起こるわけではないが、19石なのに10ターン範囲などと明らかに足りない指定をした場合に即`No instance found. Predicate may be inconsistent.`と終了してくれる。  
戦略を入れたことにより石数と同じターン数かかることはないのだが、戦略を無効化した場合には多少の安心感がある。
- 最初のプレイヤーのみ、必勝法を使って勝とうとする。  
ここでの必勝法とは、「相手番の石数が（最少個数＋最多個数）の倍数になるように取る。」  
無理な場合は、相手のミスする可能性をなるべく多く残すため最少個数だけ取る。

# 結果

```
┌──────────┬──────┬──────┬──────┬──────┬──────┬──────┬──────┬──────┬──────┐⁻¹
│this/Stone│Stone⁰│Stone¹│Stone²│Stone³│Stone⁴│Stone⁵│Stone⁶│Stone⁷│Stone⁸│  
└──────────┴──────┴──────┴──────┴──────┴──────┴──────┴──────┴──────┴──────┘  

┌───────────┐
│this/Player│
├───────────┤
│Player⁰    │
├───────────┤
│Player¹    │
└───────────┘

┌─────────┬───────┬──────┬──────┐
│this/Turn│player │stone │take  │
├─────────┼───────┼──────┼──────┤
│Turn⁰    │Player⁰│Stone⁰│Stone⁰│
│         ├───────┼──────┼──────┤
│         │       │Stone¹│      │
│         │       ├──────┤      │
│         │       │Stone²│      │
│         │       ├──────┤      │
│         │       │Stone³│      │
│         │       ├──────┤      │
│         │       │Stone⁴│      │
│         │       ├──────┤      │
│         │       │Stone⁵│      │
│         │       ├──────┤      │
│         │       │Stone⁶│      │
│         │       ├──────┤      │
│         │       │Stone⁷│      │
│         │       ├──────┤      │
│         │       │Stone⁸│      │
├─────────┼───────┼──────┼──────┤
│Turn¹    │Player¹│Stone¹│Stone¹│
│         ├───────┼──────┼──────┤
│         │       │Stone²│Stone²│
│         │       ├──────┼──────┤
│         │       │Stone³│Stone³│
│         │       ├──────┼──────┤
│         │       │Stone⁴│      │
│         │       ├──────┤      │
│         │       │Stone⁵│      │
│         │       ├──────┤      │
│         │       │Stone⁶│      │
│         │       ├──────┤      │
│         │       │Stone⁷│      │
│         │       ├──────┤      │
│         │       │Stone⁸│      │
├─────────┼───────┼──────┼──────┤
│Turn²    │Player⁰│Stone⁴│Stone⁴│
│         ├───────┼──────┼──────┤
│         │       │Stone⁵│      │
│         │       ├──────┤      │
│         │       │Stone⁶│      │
│         │       ├──────┤      │
│         │       │Stone⁷│      │
│         │       ├──────┤      │
│         │       │Stone⁸│      │
├─────────┼───────┼──────┼──────┤
│Turn³    │Player¹│Stone⁵│Stone⁵│
│         ├───────┼──────┼──────┤
│         │       │Stone⁶│      │
│         │       ├──────┤      │
│         │       │Stone⁷│      │
│         │       ├──────┤      │
│         │       │Stone⁸│      │
├─────────┼───────┼──────┼──────┤
│Turn⁴    │Player⁰│Stone⁶│Stone⁶│
│         ├───────┼──────┼──────┤
│         │       │Stone⁷│Stone⁷│
│         │       ├──────┼──────┤
│         │       │Stone⁸│Stone⁸│
├─────────┼───────┼──────┼──────┤
│Turn⁵    │       │      │      │
├─────────┼───────┼──────┼──────┤
│Turn⁶    │       │      │      │
├─────────┼───────┼──────┼──────┤
│Turn⁷    │       │      │      │
├─────────┼───────┼──────┼──────┤
│Turn⁸    │       │      │      │
├─────────┼───────┼──────┼──────┤
│Turn⁹    │       │      │      │
└─────────┴───────┴──────┴──────┘
```
スコープを変えて「先手必勝」を試すと、以下の場合に反例があることがわかる。

- プレイヤーが３人以上の場合
- ゲーム開始時の石数が（最少石数＋最多石数）の倍数だった場合

一度に取れる石数を２〜４とした場合なども試してみるとよいだろう。


# 参考

- [数取りゲームの必勝法を考える。](http://bokuso.blogspot.com/2014/09/blog-post.html)
- [Alloyのorderingで意図した順にならない現象に遭遇](https://qiita.com/cutsea110/items/aa88c3e80a0a7499a3b8)