15:15 それは、ベレー帽と呼ぶにはあまりに大きすぎた 大きく分厚く重くそして大雑把すぎた。 ―――それはまさにブルマだった。

SRCでモデル検査をやる場合、Timed Automataを使えばターン数の表現がごにょごにょごにょ…。