What Stephan wrote is correct. Another way to do it would be to write:
\E a \in RangeA:
SignalA' = aThis 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
On 3/17/2025 8:22 AM, Stephan Merz wrote:
Just write
/\ SignalA’ \in RangeA/\ … (analogous for the other signals)
TLC will explore all possible choices.
Hope this helps,Stephan--
On 17 Mar 2025, at 14:13, Jinbao Chen <cheney...@xxxxxxxxx> wrote:
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!
--
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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/63c7f65a-2413-41e7-93e5-14c41e7773dbn%40googlegroups.com.
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...@xxxxxxxxxxxxxxxx.To view this discussion visit https://groups.google.com/d/msgid/tlaplus/DFFD7D9D-0101-4230-8FFE-3063B5852E2E%40gmail.com.