equal
deleted
inserted
replaced
|
1 (* Title: Tools/Spec_Check/random.ML |
|
2 Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
|
3 Author: Christopher League |
|
4 |
|
5 Random number engine. |
|
6 *) |
|
7 |
|
8 signature RANDOM = |
|
9 sig |
|
10 type rand |
|
11 val new : unit -> rand |
|
12 val range : int * int -> rand -> int * rand |
|
13 val split : rand -> rand * rand |
|
14 end |
|
15 |
|
16 structure Random : RANDOM = |
|
17 struct |
|
18 |
|
19 type rand = real |
|
20 |
|
21 val a = 16807.0 |
|
22 val m = 2147483647.0 |
|
23 |
|
24 fun nextrand seed = |
|
25 let |
|
26 val t = a * seed |
|
27 in |
|
28 t - m * real(floor(t/m)) |
|
29 end |
|
30 |
|
31 val new = nextrand o Time.toReal o Time.now |
|
32 |
|
33 fun range (min, max) = |
|
34 if min > max then raise Domain (* TODO: raise its own error *) |
|
35 else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r) |
|
36 |
|
37 fun split r = |
|
38 let |
|
39 val r = r / a |
|
40 val r0 = real(floor r) |
|
41 val r1 = r - r0 |
|
42 in |
|
43 (nextrand r0, nextrand r1) |
|
44 end |
|
45 |
|
46 end |