I see at least a few errors with the TLA+ code: - It says that `olddb = [k \in Keys |-> CHOOSE v \in Values: TRUE]` initializes olddb nondeterministically. Thi

I see at least a few errors with the TLA+ code: - It says that `olddb = [k \in Keys |-> CHOOSE v \in Values: TRUE]` initializes olddb nondeterministically. This is NOT true: `CHOOSE` is guaranteed to be a deterministic expression. The actual thing is `olddb \in [Keys -> Values]`. - `key \in Keys; val \in Values; newdb[key] := val;` is a syntax error. I think what it meant was `with key \in Keys, val \in Values { newdb[key] := val;` - `newdb[key] := val` is an error anyway, because `newdb` was initialized as a set. - ` for key \in DOMAIN(olddb) do` is straight up a syntax error, there's no for loop in PlusCal. - It's mixing p-syntax (`if then end if`) with c-syntax (`if {}`).