Mercurial > hg > Members > kono > jpf-core
view doc/user/config/random.md @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
line wrap: on
line source
## Randomization Options in JPF ## The randomization options in JPF allow the user to experiment in randomizing the order of choices explored. `cg.randomize_choices` can have three possible values: random, path, def. * `random`: It explores random choices during program execution with **varying results among different trials**. The default seed used to generate different results is the **system time in milliseconds** * `path`: It explores random choices during program execution with **reproducible results among different trials**. The default seed used to generate reproducible results is **42**. The value of the seed can be changed by setting the seed config option. * `def`: No randomization, choices are explored using the default search order imposed by the model checker. `cg.seed (_INT_)`: The user can specify a particular seed for the random number generator in order to obtain reproducible results in the presence of randomization. Note that this is effective only when the `path` option of `randomize_choices` is selected.