ボウリングの第 10 フレームの定式化を Alloy と TLA+ (PlusCal) でやってみる
Alloy と TLA+ (PlusCal) の使い方が徐々にわかってきたので，実際に仕様を書いてみます．
ボウリングの第 10 フレームは最大 3 回投げられます．
2 回しか投げられないこともあれば，3 回投げられることもあります．
投球可否について，仕様を形式記述してみます．
まず，Alloy 編で試行錯誤しながら仕様を記述していき，その後その仕様を TLA+ (PlusCal) でも記述してみます．
あえて試行錯誤しているのは，業務アプリの仕様記述がおそらくトライ・アンド・エラーで進んでいくはずで，それの実践というか感覚を掴んでおきたいからです．
かなり長くなりますが，どうぞお付き合いくださいませ．
Alloy 編
書き方は色々あると思いますが，ここではプレーヤと，第 10 フレームでの投球結果を定義してみます．
// 投げる人
one sig Player {
, first: TryFirst
, second: TrySecond
, third: TryThird
}
// 投球の抽象シグネチャ
abstract sig Try{}
// 第 10 フレームの 1 投目から 3 投目
one sig TryFirst, TrySecond, TryThird extends Try {
, result: TryResult
}
// 各投球の結果
enum TryResult {
Ordinal // 0 - 9 本であり，かつスペアでない
, Spare // スペア
, Strike // ストライク
, NotTried // 投球せず
}まだ「どういう場合に 3 回投げられるか」とか，「何が起こればスペアか」とかを定義していませんので，当然変な例が沢山出てきます．
1 投目でスペアなんてありえないし，1 投目が 0 - 9 本のどれかだとしたら 3 投目は投げられません．
まずは，スペアとなる条件を考え，以下の制約を書いていきます．
- Spare は 2 投目以降にしか現れない
- Spare となる前の投球結果は Ordinal のみ
// スペアに関する制約条件
fact SpareConstraint {
TryFirst.result != Spare // Spare は 2 投目以降にしか現れない
TrySecond.result = Spare implies TryFirst.result = Ordinal // 2 投目がスペアなら 1 投目は 0 - 9 本
TryThird.result = Spare implies TrySecond.result = Ordinal // 3 投目がスペアなら 2 投目は 0 - 9 本
}
例をパラパラめくっていくと，確かにスペアの前は必ず Ordinal になっています．
ただ，この例では，スペアを出したのに 3 投目を投げていません．3 投目を投げられる条件を追加します．
- 1 投目または 2 投目にスペアまたはストライクを出していれば，3 投目も投げる
- 1 投目にも 2 投目にスペアまたはストライクを出していなければ，3 投目は投げない
条件が二つあるように見えますが，これは次のように一つの条件にまとめられます．
- 1 投目または 2 投目にスペアまたはストライクを出していれば (iff.)，そのときに限り 3 投目も投げる
// 3 投目を投げる条件
fact ThirdTryConstraint {
(TryFirst.result in Spare + Strike || TrySecond.result in Spare + Strike)
iff TryThird.result != NotTried
}ちなみに，1 投目はスペアにはならないので TryFirst.result = Strike でも OK です．
また，TrySecnd.reslt = Strike の場合，TryFirst.result = Strike しかありえませんから，TrySecond.result = Spare と書くだけでも OK と思われます．実際には，最終的に記述が完成したらその仕様の中で TrySecond.result = Strike => TryFirst.result = Strike が推論可能かどうか確認しないといけませんので，ここでは一旦 TrySecond.result in Spare + Strike のままで行こうと思います．
2 投目を投げてないのに 3 投目を投げてしまった……．次を追加します．
- 1, 2 投目は必ず投げる
// 1, 2 投目は必ず投げる
fact FirstAndSecndTryMustBeDone {
TryFirst.result != NotTried
TrySecond.result != NotTried
}
2 投目でピン残しがあったのに 3 投目がストライクになっています．これはありえないので，ストライクが起こるための条件を記述します．
- ストライクになるのは "1 投目である"か，または "2 投目以降かつその前の投球がストライクまたはスペアのとき" である
// ストライクが出るための条件
fact StrikeConstraint {
TrySecond.result = Strike implies TryFirst.result in Spare + Strike
TryThird.result = Strike implies TrySecond.result in Spare + Strike
}
や
が出力されます．
これで想定通りの結果だけが出力されます！
全体像は以下の通り：
// 投げる人
one sig Player {
, first: TryFirst
, second: TrySecond
, third: TryThird
}
// 投球の抽象シグネチャ
abstract sig Try{}
// 第 10 フレームの 1 投目から 3 投目
one sig TryFirst, TrySecond, TryThird extends Try {
, result: TryResult
}
// 各投球の結果
enum TryResult {
Ordinal // 0 - 9 本であり，かつスペアでない
, Spare // スペア
, Strike // ストライク
, NotTried // 投球せず
}
// スペアに関する制約条件
fact SpareConstraint {
TryFirst.result != Spare // 1 投目はスペアになりえない
TrySecond.result = Spare implies TryFirst.result = Ordinal // 2 投目がスペアなら 1 投目は 0 - 9 本
TryThird.result = Spare implies TrySecond.result = Ordinal // 3 投目がスペアなら 2 投目は 0 - 9 本
}
// 3 投目を投げる条件
fact ThirdTryConstraint {
(TryFirst.result in Spare + Strike || TrySecond.result in Spare + Strike)
iff TryThird.result != NotTried
}
// 1, 2 投目は必ず投げる
fact FirstAndSecndTryMustBeDone {
TryFirst.result != NotTried
TrySecond.result != NotTried
}
// ストライクが出るための条件
fact StrikeConstraint {
TrySecond.result = Strike implies TryFirst.result in Spare + Strike
TryThird.result = Strike implies TrySecond.result in Spare + Strike
}しかしまあ，問題だらけのコードです．
たとえば，
First とか Second とかをハードコーディングしているので，
試行回数が任意有限回となったときに対応できないおそらく，ordering モジュールをインポートし，施行を順序づけて記述することが必要と思います．
一応言い訳すると，TLA+ との対比として，ここでは ordering を使わずに静的条件として記述したかったというのもありますが．
Player が不要
余計な定義をしてました……．
論理の再利用ができない
// 1, 2 投目は必ず投げる
fact FirstAndSecndTryMustBeDone {
TryFirst.result != NotTried
TrySecond.result != NotTried
}
// ストライクが出るための条件
fact StrikeConstraint {
TrySecond.result = Strike implies TryFirst.result in Spare + Strike
TryThird.result = Strike implies TrySecond.result in Spare + Strike
}のように，TryFirst と TrySecond，TrySecond と TryThird に対してほぼ同じ条件を何書いています．これはプログラマならちゃぶ台をひっくり返して怒り狂うところでしょう．
以上の問題点に対する修正は，次回の記事にしたいと思います．とりあえずは，正しそうな仕様記述が得られたので，これで OK とさせてください（逃げ）．
PlusCal 編
PlusCal ではプログラミングライクな記述をし，Alloy 編で見つかったような問題点がないことを検査していこうと思います．
ただし，PlusCal は手続き的に記述できるので，今回のような高々 3 回の試行であれば非常に記述しやすいため，一気に記述しきってしまいます．
EXTENDS Sequences, Integers
(*--algorithm bowling
variables result = <<>>;
begin
\* 1st try
either
\* ordinal
result := Append(result, "Ordinal");
or
\* strike
result := Append(result, "Strike");
end either;
\* 2nd try
if Head(result) = "Ordinal" then
either
\* ordinal
result := Append(result, "Ordinal");
or
\* spare
result := Append(result, "Spare");
end either;
else
either
\* ordinal
result := Append(result, "Ordinal");
or
\* Strike
result := Append(result, "Strike");
end either;
end if;
\* 3rd try
\* do 3rd try?
if result[1] \in {"Strike"} \/ result[2] \in {"Spare"} then
\* do 3rd try
if result[2] \in {"Strike", "Spare"} then
either
\* ordinal
result := Append(result, "Ordinal");
or
\* Strike
result := Append(result, "Strike");
end either;
else
either
\* ordinal
result := Append(result, "Ordinal");
or
\* Spare
result := Append(result, "Spare");
end either;
end if;
else
result := Append(result, "NotTried");
end if;
end algorithm;*)なお，モデル検査で result の要素数を数えないといけないので，Integers を EXTENDS しています．
Alloy 編で見つかったような内容を検査します：
- Spare は 2 投目以降にしか現れない
- Spare となる前の投球結果は Ordinal のみ
- 1 投目または 2 投目にスペアまたはストライクを出していれば (iff.)，そのときに限り 3 投目も投げる
- 1, 2 投目は必ず投げる
- ストライクになるのは "1 投目である"か，または "2 投目以降かつその前の投球がストライクまたはスペアのとき" である
これらを記述していきましょう．
Spare は 2 投目以降にしか現れない
検査するまでもないですが……．一応こうなります：pc = "Done" => result[1] /= "Spare"Spare となる前の投球結果は Ordinal のみ
2 投目と 3 投目で分けて書きます．pc = "Done" /\ result[2] = "Spare" => result[1] = "Ordinal"および
pc = "Done" /\ Len(result) = 3 /\ result[3] = "Spare" => result[2] = "Ordinal"とします．
1 投目または 2 投目にスペアまたはストライクを出していれば (iff.)，そのときに限り 3 投目も投げる
pc = "Done" /\ (result[1] = "Strike" \/ result[2] = "Spare") => Len(result) = 31, 2 投目は必ず投げる
pc = "Done" => Len(result) >= 2ストライクになるのは "1 投目である"か，または "2 投目以降かつその前の投球がストライクまたはスペアのとき" である
pc = "Done" => (result[2] = "Strike" => result[1] \in {"Strike", "Spare"}) /\ (result[3] = "Strike" => result[2] \in {"Strike", "Spare"})
検査を実行しても，エラーは出力されませんでした！
二つの言語で書いた所感
やはり，ボウリングは時制の絡む試行ですので，Alloy で静的表現をするよりも，TLA+ でステートマシンを記述するほうがよっぽど楽なようです．
Future Work
Alloy 編で述べたように，次の記事ではもっとコードの再利用をできるような記述に直そうと思います．
以上！
コメント