David Gries の Coffee Can Problemを TLA+ でモデル化しようとしていますが、この部分で行き詰っています。
「最初に缶に入っていた黒豆と白豆の数の関数として、最終的に残った豆の色について何が言えますか?」
これにアプローチする方法がわかりません。アドバイスやヒントを教えてください。（方法論も大歓迎です）
これは TLA+ の私のコードです:
------------------------------ MODULE CanBean ------------------------------
EXTENDS Naturals, FiniteSets, Sequences
\* filter <- 2 | max_can <- 5
CONSTANT filter, max_can
VARIABLES picked, Can, Whites, Blacks
vars == <<picked, Can, Whites, Blacks>>
IsBlack(i) == i % filter = 0
IsWhite(i) == i % filter /= 0
GetWhite(a,b) == IF IsWhite(a) THEN a ELSE b
GetBlack(a,b) == IF IsBlack(a) THEN a ELSE b
AreBothWhite(a,b) == IsWhite(a) /\ IsWhite(b)
Pick == /\ picked = <<>>
/\ \E a,b \in Can : a/= b /\ picked' = <<a,b>>
/\ UNCHANGED <<Whites, Blacks, Can>>
Process == /\ picked /= <<>>
/\ LET a == picked[1] b == picked[2] IN
/\ \/ AreBothWhite(a,b) /\ Whites' = Whites \ {a,b} /\ \E m \in Nat \cap Can : Blacks' = Blacks \cup { filter * m }
\/ ~AreBothWhite(a,b) /\ Blacks' = Blacks \ { GetBlack(a,b) } /\ UNCHANGED Whites
/\ picked' = <<>>
/\ Can' = Blacks' \cup Whites'
Terminating == /\ Cardinality(Can) = 1
/\ UNCHANGED vars
TypeInvariantOK == /\ \A n \in Can : n \in Nat
/\ LET length == Len(picked)
IN length = 2 \/ length = 0
Init == /\ picked = <<>>
/\ Can = 1..max_can
/\ Blacks = { n \in Can : n % filter = 0 }
/\ Whites = { n \in Can : n % filter /= 0 }
Next == Pick \/ Process \/ Terminating
=============================================================================
\* Modification History
\* Last modified Sun Feb 21 14:53:34 CET 2021
\* Created Sat Feb 20 19:50:01 CET 2021