I have a constant set called clients = {"c1","c2","c3"}. clients is an index set for clientState. The values in the array clientState can be {"working", "attempting", "acknowledged"}.
E.g. clientState["c1"] = "working".
Here's what I want to do: I want to replace all appearances of "attempting" in clientState array by "working". (I know TLA checks variables and doesn't perform executions, but you get what I mean to check for)
This is what I've tried, using a nested set constructor:
The pretty printed version is attached.
E.g. clientState["c1"] = "working".
Here's what I want to do: I want to replace all appearances of "attempting" in clientState array by "working". (I know TLA checks variables and doesn't perform executions, but you get what I mean to check for)
This is what I've tried, using a nested set constructor:
\A r \in {\A s \in clients: clientState[s] = "attempting"} : clientState' = [clientState EXCEPT ![r] = "working"]
The pretty printed version is attached.
TLA returns this error:
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to check equality of string "c1" with non-string:
FALSE
I would greatly appreciate your help.