How to randomly select a value from a set?

[Jinbao Chen]

I am a beginner in TLA+, and while writing my specification, I tried to simulate signal changes in one of the steps. I attempted to use the CHOOSE operator to randomly select elements from a set to simulate this process, like this:

SigTrans == /\ pc = "SigTrans" 

                      /\ SignalA' = (CHOOSE x \in RangeA: TRUE) 

                      /\ SignalB' = (CHOOSE x \in RangeB: TRUE) 

                      /\ SignalC' = (CHOOSE x \in RangeC: TRUE) 

                      /\ SignalD' = (CHOOSE x \in RangeC: TRUE)

                      /\ \/ SignalA' # SignalA

                          \/ SignalB' # SignalB
                          \/ SignalC' # SignalC
                          \/ SignalD' # SignalD

                      /\ pc' = "Action" 

                      /\ UNCHANGED SignalOutput
 

Through this process, I am trying to simulate a scenario where four signals change randomly, and each time a change occurs, at least one of the signals must be different from before.  However, I found that the CHOOSE operator always selects a fixed element from the set (the first element in the set), rather than selecting randomly. As a result, I’m unable to simulate the above process. After reading previous discussions in this group about CHOOSE, I’ve learned that CHOOSE is actually a deterministic operator in TLA+.

Is there any way in TLA+ to achieve random (or pseudo-random) selection from a set?
Thank you for your help! 

[Stephan Merz]

Just write

/\ SignalA’ \in RangeA

/\  …  (analogous for the other signals)

TLC will explore all possible choices.

Hope this helps,

Stephan

--
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 visit https://groups.google.com/d/msgid/tlaplus/63c7f65a-2413-41e7-93e5-14c41e7773dbn%40googlegroups.com.

[Hillel Wayne]

What Stephan wrote is correct. Another way to do it would be to write:

\E a \in RangeA:
  SignalA' = a

This is more verbose but you can also have multiple clauses in the body of the `\E`. That's why it's the standard way to represent concurrency:

\E p \in Processes:
  \/ Action1(p)
  \/ Action2(p)
  \/ \* etc

H

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/DFFD7D9D-0101-4230-8FFE-3063B5852E2E%40gmail.com.

[Jinbao Chen]

Thanks for your help! That works!