proper treatment of absolute deadline vs. relative timeout;
authorwenzelm
Sat, 22 Aug 2020 14:48:00 +0200
changeset 72190 8009c4b5db5e
parent 72189 7a213affdc10
child 72191 d436ba9ac9aa
proper treatment of absolute deadline vs. relative timeout;
src/HOL/Nitpick_Examples/minipick.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Nitpick_Examples/minipick.ML	Sat Aug 22 13:55:42 2020 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML	Sat Aug 22 14:48:00 2020 +0200
@@ -430,10 +430,11 @@
 fun solve_any_kodkod_problem thy problems =
   let
     val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
+    val deadline = Time.now () + timeout
     val max_threads = 1
     val max_solutions = 1
   in
-    case solve_any_problem debug overlord timeout max_threads max_solutions
+    case solve_any_problem debug overlord deadline max_threads max_solutions
                            problems of
       JavaNotFound => "unknown"
     | JavaTooOld => "unknown"
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Aug 22 13:55:42 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Aug 22 14:48:00 2020 +0200
@@ -211,10 +211,11 @@
 fun run_all_tests () =
   let
     val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params \<^theory> []
+    val deadline = Time.now () + timeout
     val max_threads = 1
     val max_solutions = 1
   in
-    case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
+    case Kodkod.solve_any_problem debug overlord deadline max_threads max_solutions
                                   (map (problem_for_nut \<^context>) tests) of
       Kodkod.Normal ([], _, _) => ()
     | _ => error "Tests failed"