I've been toying with spec'ing the snowflake/snowball/avalanche byzantine consensus protocols in TLA+: https://muratbuffalo.blogspot.com/2018/06/snowflake-to-avalanche-novel-metastable.html
These protocols are probabilistic; quoting from Murat's post:
To perform a query, a node picks a small, constant-sized (k)
sample of the network uniformly at random, and sends a query message.
Upon receiving a query, an uncolored node adopts the color in the query,
responds with that color, and initiates its own query, whereas a
colored node simply responds with its current color.
The naive way to spec this in TLA+ is as follows:
QuerySample(k) ==
/\ \E sample \in SUBSET Node :
/\ Cardinality(sample) = k
/\ ...
This obviously leads to a HUGE explosion in number of states and all but guarantees infeasibility of model-checking. What other approaches exist for modeling probabilistic properties such as this in TLA+?
Andrew