class interface P_RANDOM creation make (seed: INTEGER) -- Initialise pseudo-random machine from seed. feature(s) from P_RANDOM -- Initialisation make (seed: INTEGER) -- Initialise pseudo-random machine from seed. feature(s) from P_RANDOM -- Initialisation reset (seed: INTEGER) -- Initialise pseudo-random machine from seed. feature(s) from P_RANDOM -- Random number get_number (min_range, max_range: INTEGER) -- Get a new random integer inside specified range. require positive: min_range >= 0; in_order: min_range < max_range ensure inside: last_number >= min_range and last_number <= max_range; -- last_number set done: last_number: INTEGER -- Last result. end of P_RANDOM