PSharp
PSharp copied to clipboard
Randomness in StateMachineRuntime
The procedures GetNondeterministicBooleanChoice and GetNondeterministicIntegerChoice do the following: new Random(DateTime.Now.Millisecond). The use of DateTime.Now.Millisecond results in loss of randomness when the calls are close together in time, and in general only 1000 possible random values can be generated.
StateMachineRuntime should have its own random generator that is used over its entire lifetime. And initialized using the default constructor.