PSharp icon indicating copy to clipboard operation
PSharp copied to clipboard

Randomness in StateMachineRuntime

Open akashlal opened this issue 7 years ago • 0 comments

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.

akashlal avatar Apr 17 '18 05:04 akashlal