Aさん
外にいる
鍵は1本だけ
部屋では同時に1人しか作業できない。入るには鍵が要る。下のボタンは「その人が次にやること」。
ちゃんとしたルール。誰かが鍵を持っていたら、もう1人はそこで止まる。
2人とも外にいて、鍵は空いている。どちらかの「鍵を取りに行く」を押してみて。
Bさん
外にいる
これ、さっきの TLA+ の話？
同じものです。難しい名前を外しただけ。TLA+ は「やってよい動き」を全部機械に試させて、入っちゃいけない状態がないか探す書き方。この画面の部屋が臨界領域、鍵がロック、ボタン1回が原子ステップです。