Understanding CHOOSE

[Park Lay]

Hello,

I am new to TLA+ and I'm trying to understand the how does the keyword CHOOSE work in TLA+. I have already read the available documentation but I don't think I fully grasp how it works.

I have this in my module :

CHOOSE sub \in ClaimsData : TRUE such that ClaimsData <- {0..10}

Can you please help me understand what really is happening here ? What I'm trying to achieve is to pick a "random" value... but I know that this is not non-deterministic.. I'm really confused..

Thank you!

[Alex Weisberger]

CHOOSE is definitely a confusing operator, many people have problems with it including myself. The idea is that CHOOSE always picks the same value, it does not represent arbitrary values.

If you're trying to say "sub can be any element of ClaimsData", then the "there exists" operator (existential quantification) is what you're looking for, i.e.

\E sub \in ClaimsData: SomePredicate(sub)

or something thereabout. If we are thinking in terms of predicates on the state space, this returns true for _every_ next state where sub is an element of ClaimsData and SomePredicate(sub) is true. Which path the algorithm takes during a single algorithm execution is the "random" part, but the specification should describe all possible paths with no randomness. 

--
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 tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/efa2ccc2-0fe0-49ad-b893-d7fd286193f0n%40googlegroups.com.

--

- Alex Weisberger, Senior Software Engineer: House Manage

[John]

Hi Alex,

Thank you for your message.

1 - Is  CHOOSE sub \in ClaimsData : TRUE   the correct way to say that I want TLA+ to pick a value from ClaimsData and label it sub ? How would you have expressed it ?

2 - In my module, I'm trying to represent the bahviour of an external API (which may respond with a 200 HTTP status or a 4XX or 5XX HTTP status : 2 states => Success OR Failure). Briefly put, how would you describe an external API that your system consumes and needs to react predictably according to the API's response (success or failure) ? (the "randomness" part is how often do you get a Successful/Failed response. The difficulty is how do I describe this beahviour ?

Thank you!

[sadraskol (Thomas Bracher)]

Hello John,

I think Alex answered your first point, but I'll try to express by my own words for you to see how it translates to a formal description.

Say your system is a simple increment/decrement of a global state :

CallToApi(answer) == \/ /\ answer = "200"
                                   /\ i' = i + 1
                               \/ /\ answer = "400"
                                   /\ i' = i - 1

As you mentioned, you can use CHOOSE :

Init == i = 0

Next == LET answer == CHOOSE code \in {"200", "400"}: TRUE

              IN CallToApi(answer)

But as mentioned by Alex and yourself, this would not yield the expected behavior. CHOOSE having no guarantees, all possible outputs are not covered by TLC.
The existential quantifier is the correct way of exploring all possible behavior :

Init == i = 0

Next == \E answer \in {"200", "400"}: CallToApi(answer)

The operator \E corresponds to the correct way of introducing non-determinist behavior in your specifications. TLC will check all possible behaviors for you.

I hope it helped,

Thomas

[Younes]

Thank you Thomas. I am reading Specifying Systems, and I think I know understand better CHOOSE.

Thank you for your explanation. It helped me as well figure out how this keyword functions. Leslie Lamport says in his book that CHOOSE is the equivalent of Hilbert's epsilon.

[Hillel Wayne]

These days I just teach that CHOOSE picks the least value that matches the predicate. Once people are comfortable with that I then explain it's a TLC implementation detail to guarantee the formal CHOOSE properties. It leads to a lot less confusion that way.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC7YZZkjf4pZ9hYsHoNF7Uvn63eBC34wzix5Dyv983SU6zmJMg%40mail.gmail.com.

[ron.pr...@gmail.com]

You are correct, but this is a result of neither TLC nor even TLA+, but of how we describe things in mathematics. A CHOOSE expression is equal to some value that satisfies the condition (I think SOME would have been a better name). In mathematics, A = A for any expression A, and therefore it is always the case that (CHOOSE x ∈ S : P(x)) = (CHOOSE x ∈ S : P(x)); all occurrence of this expression are equal to one another. ∃ x ∈ S : P(x) is also a mathematical expression, but one that can only be equal to either TRUE or FALSE. As with CHOOSE, always (∃ x ∈ S : P(x)) = (∃ x ∈ S : P(x)), but while the value (TRUE/FALSE) of these two expressions is equal, the x in both cases might not be the same; the expressions -- while equal -- can be talking about different xs. 

-- Ron