diff --git a/src/Engine.ml b/src/Engine.ml index ee250601bf2438eb695eb1d0e74b5261e20dc59e..624a3df4fbe04c0f2a986368c4eebc80e94e3065 100644 --- a/src/Engine.ml +++ b/src/Engine.ml @@ -1419,8 +1419,8 @@ let log scenario fuel = (* -------------------------------------------------------------------------- *) -(* [main_random_loop prologue clock fuel] performs an unbounded number of test - runs in random mode. *) +(* [main_random_loop prologue clock fuel accu] performs an unbounded number of + test runs in random mode. *) (* While the tests run, we print information roughly every second. We print how many tests have been performed so far, our overall average speed, and @@ -1435,7 +1435,14 @@ let log scenario fuel = (* For each value of [fuel], we use an explicit infinite loop to perform an unbounded number of runs. *) -let rec main_random_loop prologue clock fuel = +(* If the clock [clock] has no time limit, then [main_random_loop] never + terminates. If this clock has a time limit then [main_random_loop] + terminates once the time limit has been reached, and it returns the number + of failure scenarios that have been discovered and logged along the way. + The accumulator [accu] records the number of failure scenarios discovered + so far. *) + +let rec main_random_loop prologue clock fuel (accu : int) : int = try (* An infinite loop. *) while true do @@ -1443,14 +1450,19 @@ let rec main_random_loop prologue clock fuel = run prologue fuel; (* Tick the clock and, once in a while, display statistics. *) tick clock fuel - done - with Abort (scenario, fuel) -> - log scenario fuel; - (* We have been able to find a problem with a certain amount of - fuel. Try again, with this amount. This restricts our search - space, and (with luck) we might now be able to find an even - shorter scenario. *) - main_random_loop prologue clock fuel + done; + (* This cannot happen. *) + assert false + with + | Abort (scenario, fuel) -> + log scenario fuel; + (* We have been able to find a problem with a certain amount of + fuel. Try again, with this amount. This restricts our search + space, and (with luck) we might now be able to find an even + shorter scenario. *) + main_random_loop prologue clock fuel (accu + 1) + | Clock.Timeout -> + accu (* [main_random prologue fuel] performs an unbounded number of test runs in random mode. *) @@ -1464,12 +1476,12 @@ let rec main_random_loop prologue clock fuel = The main reason for this change is to allow imposing a time limit on the whole process. *) -let main_random prologue fuel = +let main_random ?timeout prologue fuel : int = let source = None in Gen.with_source source @@ fun () -> let granularity = 1000 in - let clock = Clock.make granularity in - main_random_loop prologue clock fuel + let clock = Clock.make ?timeout granularity in + main_random_loop prologue clock fuel 0 (* -------------------------------------------------------------------------- *) @@ -1505,4 +1517,5 @@ let main ?prologue:(prologue=none) fuel = | Some _ -> main_afl source prologue fuel | None -> - main_random prologue fuel + let (failures : int) = main_random prologue fuel in + ignore failures