Fix #8121 : wfRandom() is not between 0 and 1