I have been trying to model a set of concurrent chemical reactions in Dafny. Since these reactions occur with non-zero probabilities once they are enabled, I would like to model the probabilistic behavior. I might just need a simple uniform random function in Dafny, but could not seem to find much information. Any help would be appreciated.

I searched the Dafny online tutorial (https://dafny.org/dafny/OnlineTutorial/guide) and the language reference (https://dafny.org/dafny/DafnyRef/DafnyRef).