Re: [tlaplus] How do I replace elements of a certain value in an array?

Thanks friend! That worked. I also got to learn this very useful notation of DOMAIN and IF ELSE. Thank you.

I was creating a spec for TCP Handshaking. I finished it successfully.

On Thursday, January 9, 2020 at 7:13:01 PM UTC+5:30, Saksham Chand wrote:

Short answer: What would work:
clientState' = [r \in DOMAIN clientState |-> IF clientState[r] = "attempting" THEN "working"
ELSE clientState[r]]

Long answer:
What's wrong with \A r \in {\A s \in clients: clientState[s] = "attempting"} : clientState' = [clientState EXCEPT ![r] = "working"]:

1) \A s \in clients: clientState[s] = "attempting" is a boolean _expression_. Therefore {\A s \in clients: clientState[s] = "attempting"} will be either the set {TRUE} or the set {FALSE}. That is the first mistake. You were probably thinking of {s \in clients: clientState[s] = "attempting"}, that is, without the quantification in the beginning. But even that would be wrong.
2) To understand why \A r \in {s \in clients: clientState[s] = "attempting"} : clientState' = [clientState EXCEPT ![r] = "working"] is wrong, I suggest reading an earlier mail-chain "Merging EXCEPT statements" (https://groups.google.com/d/msg/tlaplus/35F5YiVxWHQ/qDyO16mwAgAJ)

Best,
Saksham

On Thu, Jan 9, 2020 at 7:56 AM Curious Student <vedantp...@xxxxxxxxx> wrote:
Hello.

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:

\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.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/053966d9-5b4e-4ba5-b0e3-ad04b03436a8%40googlegroups.com.