Hello,
I cannot reproduce your error: when copying and pasting your spec into the Toolbox, creating a model with Z=10 and checking the invariant NUMCHECK (+ absence of deadlock), TLC computes 80 states (60 distinct states) and terminates normally without finding an error. May I suggest that you delete the specification from the Toolbox (in the sidebar, click on the icon "T+", right-click on module Testing in the list, choose "Delete" and confirm), then reload it.
Two observations:
- The TLA+ translation doesn't correspond to the PlusCal algorithm (the statement labeled A adds Z to alice_account whereas the TLA+ translation subtracts Z). When you edit your PlusCal algorithm, you have to regenerate the TLA+ (File -> Translate PlusCal Algorithm).
- NUMCHECK only mentions the constant Z, it is independent of the reachable states of your specification. Better make it an assumption
ASSUME Z \in Nat /\ Z < 1000
that TLC will check only once at startup instead of at every state that it computes.
Regards,
Stephan