for fun, I popped it into ChatGPT o3-mini-high, had it generate the TLA+ code then compare its version to the human-written version:
https://chatgpt.com/share/67d0390c-4208-8007-a39d-8d9bfa7886...
https://chatgpt.com/share/67d0390c-4208-8007-a39d-8d9bfa7886...
- 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 {}`).