For modeling probability there are three models which are relevant (none of which TLA+ supports):
- Discrete-Time Markov Chains (DTMCs) where every transition is labeled with a probability and the fan-out probabilities of all transitions from a state must sum to 1; you can ask questions like "what is the probability of reaching this state?" of the model, and it is fairly efficient to convert the DTMC into a matrix and solve for this probability as the solution to a set of linear equations.
- Markov Decision Processes (MDPs) which mix nondeterminism and probabilistic state transitions; this model is the most similar to TLA+ and if probability were ever to be added to TLA+ this is almost certainly the model that would be used. In this model some (usually most) of the transitions are ordinary nondeterministic transitions as in TLA+, but some states have probabilistic steps fanning out from them. For this model you can ask questions like "what is the maximum or minimum probability of entering this state?". Unfortunately this model is fairly inefficient; roughly speaking how it works is each possible execution trace generates a unique DTMC which the reachability probability needs to be solved for, then the maximum or minimum value is taken over all such DTMCs.
- Continuous-Time Markov Chains (CTMCs) where instead of each transition being labeled with a probability, it is labeled with a rate denoting the decay of an exponential function controlling how long the system is expected to remain in the source state without taking that transition. Since you seem to be coming from queueing theory this is probably the model you are most familiar with. You can ask questions like "how long do we expect the system to run before reaching this state?" and answering this requires solving some differential equations. Broadly speaking it is more tractable than MDPs and some researchers have used CTMCs to try to approximate MDPs and overcome their limitations.
As said at the start TLA+ does not support any of these models. There is a modeling language which does, called PRISM (http://www.prismmodelchecker.org/). The language is quite rough and is pretty much just a graph/matrix labeling DSL; the entire state space needs to be declared up front.
There is some very basic probability modeling that can be done with TLA+ as demonstrated here: https://github.com/tlaplus/Examples/tree/1f278eacdcf563a303856e82b609129f43923131/specifications/KnuthYao
I wrote a longer blog post talking about the various probabilistic models here: https://ahelwer.ca/post/2020-09-11-probabilistic-distsys/
Andrew Helwer