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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit
https://groups.google.com/d/msgid/tlaplus/63c7f65a-2413-41e7-93e5-14c41e7773dbn%40googlegroups.com.