# HG changeset patch
# User bulwahn
# Date 1285836492 -7200
# Node ID fdbea66eae4bd3ad46e678e4179e4c8d222225e3
# Parent  9e7a0a9d194eab984e98ac48c39c43e7b6609b82
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)

diff -r 9e7a0a9d194e -r fdbea66eae4b src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 30 10:48:11 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 30 10:48:12 2010 +0200
@@ -86,6 +86,7 @@
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [],
   replacing = [],
@@ -97,7 +98,7 @@
 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 100000, report]
+(*quickcheck[generator = code, iterations = 100000, report]*)
 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
 oops
 
@@ -112,8 +113,24 @@
    s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
 
+section {* Manual setup to find the counterexample *}
+
 setup {* Code_Prolog.map_code_options (K 
   {ensure_groundness = true,
+   limit_globally = NONE,
+   limited_types = [],
+   limited_predicates = [(["hotel"], 4)],
+   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+   manual_reorder = []}) *}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+setup {* Code_Prolog.map_code_options (K 
+  {ensure_groundness = true,
+   limit_globally = NONE,
    limited_types = [],
    limited_predicates = [(["hotel"], 5)],
    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
@@ -124,4 +141,75 @@
 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
 oops
 
+section {* Simulating a global depth limit manually by limiting all predicates *}
+
+setup {*
+  Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limit_globally = NONE,
+  limited_types = [],
+  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
+  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+  manual_reorder = []})
+*}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+
+setup {*
+  Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limit_globally = NONE,
+  limited_types = [],
+  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
+  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+  manual_reorder = []})
+*}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+section {* Using a global limit for limiting the execution *} 
+
+text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+
+setup {*
+  Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limit_globally = SOME 13,
+  limited_types = [],
+  limited_predicates = [],
+  replacing = [],
+  manual_reorder = []})
+*}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+text {* But a global depth limit of 14 does. *}
+
+setup {*
+  Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limit_globally = SOME 14,
+  limited_types = [],
+  limited_predicates = [],
+  replacing = [],
+  manual_reorder = []})
+*}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
 end
\ No newline at end of file