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