model-checker : fix MC_RANDOM simcall
Time doesn't exist in model-checking. However, there are some
protocols, such as Chord, with some periodics operations (random
lookup, check predecessors, ...). If the model-checker is used with
these examples, these operations are never executed because of the
time which doesn't progress. With MC_RANDOM simcall, the
model-checker will explore the two cases : the case in which the
periodic operation is executed and the other case in which it is not
executed. In this way, the verification is exhaustive whatever the
period.