40 |
40 |
41 instance .. |
41 instance .. |
42 |
42 |
43 end |
43 end |
44 |
44 |
45 ML {* |
45 ML \<open> |
46 val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false); |
46 val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false); |
47 val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false); |
47 val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false); |
48 *} |
48 \<close> |
49 |
49 |
50 setup {* |
50 setup \<open> |
51 Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14", |
51 Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14", |
52 (small_14_active, Predicate_Compile_Quickcheck.test_goals |
52 (small_14_active, Predicate_Compile_Quickcheck.test_goals |
53 (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14)))) |
53 (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14)))) |
54 #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15", |
54 #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15", |
55 (small_15_active, Predicate_Compile_Quickcheck.test_goals |
55 (small_15_active, Predicate_Compile_Quickcheck.test_goals |
56 (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15)))) |
56 (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15)))) |
57 *} |
57 \<close> |
58 |
58 |
59 lemma |
59 lemma |
60 "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
60 "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
61 (*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*) |
61 (*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*) |
62 quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample] |
62 quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample] |