generous timeout gives more breath in parallel run on less luxury machines
authorhaftmann
Mon, 22 Nov 2010 14:27:42 +0100
changeset 40909f643399acab3
parent 40908 86a1f61d260e
child 40910 798aad2229c0
child 40921 3b9b39ac1f24
child 40922 54dbe6a1c349
generous timeout gives more breath in parallel run on less luxury machines
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 14:19:03 2010 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 14:27:42 2010 +0100
     1.3 @@ -50,8 +50,8 @@
     1.4  
     1.5  lemma
     1.6    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
     1.7 -quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample]
     1.8 -quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample]
     1.9 +quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
    1.10 +quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
    1.11  oops
    1.12  
    1.13