Alloyでパズル (8) 石取りゲーム（別解）

発想を変えて、util/orderingを使わずにやってみよう。
今度はプレイヤーの行動ではなく、取られた石の方に着目する。

考え方

ゲーム終了時、各石にはどのターンで取られたかが記されていることにする。

sig Stone { taken: Int }

石に記されたターンの一覧はStone.takenやtaken[univ]で得られる。

let turns = Stone.taken

パスはできないので、turnsで得られる結果は(1+2+3+...n)と決着ターンまですべて含んでいるはず。
Int についてはこれまで使ってきたmin, maxの他に、ソース を見るとわかるように next, prev, nexts, prevs といった便利関数が使える。
対象数未満をすべて含む集合prevs[Int]を使うと、上の内容はこう表せる。

fact { turns = prevs[(#turns).next] - prevs[1] }

リスト

結果が見やすいように、パラメータと結果をGameにまとめた。

// 石取りゲーム（別解）

// 石には何ターン目で取られたかが記される (1〜)
sig Stone { taken: Int }

one sig Game {
    players: 3,     // 参加者数
    minTake: 1,     // 一度に取れる最少石数
    maxTake: 3,     // 一度に取れる最多石数
    turn: Int,      // 結果： 何ターンで決着したか
    winner: Int     // 結果： 勝ったのはどちらか (1..players)
} {
    turn = #turns
    winner = turns.max.player
}

// ターン一覧
let turns = Stone.taken

// ターンプレイヤー (1〜Game.players)
let player[turn] = turn.prev.rem[Game.players].next

fact {
    // パス不可： turnsには 1～最終ターンまで全て含まれる
    turns = prevs[(#turns).next] - prevs[1]

    // １ターンに取れる石の数
    all t:turns | (Game.minTake =< #taken.t) && (#taken.t =< Game.maxTake)
}

run {} for 6 int, exactly 9 Stone


// 勝ちパターンを狙う取り方
fun takeToWin[turn:Int] : Int {
    let leftStone = #(Stone - taken.(prevs[turn])) |
        max[ Game.minTake + leftStone.rem[Game.minTake+Game.maxTake] ]
}

// 先手は勝ちパターンを狙う
pred p1WantsToWin {
    all t:turns | t.player=1 => #taken.t = takeToWin[t]
}
run p1WantsToWin for 6 int, exactly 29 Stone

// 「先手必勝」を崩せるか
check { p1WantsToWin => Game.winner=1 } for 6 int, exactly 29 Stone

結果

（９石、３人、考えない例）
　　

補足：+,-の誤用について

leftStone.rem[Game.minTake+Game.maxTake]の場合rem[]の引数だから+は整数加算なのかと思うかもしれないが、実は違う
ここでの+も集合の和である
いったん２要素の集合になった上で、暗黙にsum[]で合計値が求められている

通常の算術演算式は以下の組み込み関数を使って、関数適用の構文（すなわちボックス演算子またはドット演算子）で構成される。
　plus [a,b] aとbの和を返す
　minus [a,b] aとbの差を返す
　mul [a,b] aとbの積を返す
　div [a,b] aをbで割った結果を返す
　rem [a,b] aをbで割った剰余を返す
これらの関数の引数に対してはsum関数が暗黙に適用される。

Evaluator で確認してみよう
rem[]の引数だから+, -が算術演算になるのなら、rem[5, 1+3] = 1, rem[5, 3-1] = 3になるはずだ。
　　
+の方は1+3 = {1,3}のためたまたま整数加算と同じ結果になっているが、-の方は3-1 = {3}であるため整数減算と同じ結果にはならない。
（1+3だから同じ結果になったが、1+3+3だったらどうか）
　
数値の加減算を書きたいときについ+や-を使ってしまうことがあるが（実のところ今回の例もそうだ）、謎挙動に悩まされないためにも意識してadd[], sub[]もしくはplus[], minus[]を使おう。

参考

• Daniel Jackson：抽象によるソフトウェア設計 ―Alloyではじめる形式手法