# HG changeset patch # User bulwahn # Date 1328956583 -3600 # Node ID 9e83b7c24b05bb7923d3b9713a06e611158ec6fc # Parent e4f1cda51df6d043550964cd3ddfa9ce35a23512 making max_mutants an option that can be changed in the Mutabelle-script diff -r e4f1cda51df6 -r 9e83b7c24b05 src/HOL/Mutabelle/MutabelleExtra.thy --- a/src/HOL/Mutabelle/MutabelleExtra.thy Sat Feb 11 11:36:21 2012 +0100 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy Sat Feb 11 11:36:23 2012 +0100 @@ -42,7 +42,7 @@ MutabelleExtra.thms_of false thy |> MutabelleExtra.take_random 200 |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report - @{theory} mtds thms (log_directory ^ "/" ^ name))) + @{theory} 50 mtds thms (log_directory ^ "/" ^ name))) *} diff -r e4f1cda51df6 -r 9e83b7c24b05 src/HOL/Mutabelle/etc/settings --- a/src/HOL/Mutabelle/etc/settings Sat Feb 11 11:36:21 2012 +0100 +++ b/src/HOL/Mutabelle/etc/settings Sat Feb 11 11:36:23 2012 +0100 @@ -4,5 +4,6 @@ MUTABELLE_LOGIC=HOL MUTABELLE_IMPORT_THEORY=Complex_Main +MUTABELLE_NUMBER_OF_MUTANTS=4 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools" diff -r e4f1cda51df6 -r 9e83b7c24b05 src/HOL/Mutabelle/lib/Tools/mutabelle --- a/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Feb 11 11:36:21 2012 +0100 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Feb 11 11:36:23 2012 +0100 @@ -17,6 +17,7 @@ echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)" echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)" echo " -N NUMBER number of lemmas to choose randomly, if not given all lemmas are chosen" + echo " -M NUMBER number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)" echo echo " THEORY is the name of the theory of which all theorems should be" echo " mutated and tested." @@ -31,7 +32,7 @@ MUTABELLE_IMPORTS="" -while getopts "L:T:O:N:" OPT +while getopts "L:T:O:N:M:" OPT do case "$OPT" in L) @@ -46,6 +47,9 @@ N) NUMBER_OF_LEMMAS="$OPTARG" ;; + M) + MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG" + ;; \?) usage ;; @@ -95,13 +99,13 @@ ML {* val mtds = [ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", - MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\", - MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\" - (*, MutabelleExtra.refute_mtd, *) , MutabelleExtra.nitpick_mtd @@ -113,7 +117,7 @@ (MutabelleExtra.random_seed := 1.0; MutabelleExtra.thms_of false thy $MUTABELLE_FILTER |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report - @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) + @{theory} $MUTABELLE_NUMBER_OF_MUTANTS mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) *} ML {* diff -r e4f1cda51df6 -r 9e83b7c24b05 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Feb 11 11:36:21 2012 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Feb 11 11:36:23 2012 +0100 @@ -38,7 +38,7 @@ val string_for_report : report -> string val write_report : string -> report -> unit val mutate_theorems_and_write_report : - theory -> mtd list -> thm list -> string -> unit + theory -> int -> mtd list -> thm list -> string -> unit val random_seed : real Unsynchronized.ref end; @@ -51,7 +51,6 @@ (* mutation options *) -val max_mutants = 4 val num_mutations = 1 (* soundness check: *) (*val max_mutants = 10 @@ -396,7 +395,7 @@ end (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *) -fun mutate_theorem create_entry thy mtds thm = +fun mutate_theorem create_entry thy max_mutants mtds thm = let val exec = is_executable_thm thy thm val _ = tracing (if exec then "EXEC" else "NOEXEC") @@ -434,7 +433,7 @@ end (* theory -> mtd list -> thm list -> report *) -val mutate_theorems = map ooo mutate_theorem +val mutate_theorems = map oooo mutate_theorem fun string_of_mutant_subentry thy thm_name (t, results) = "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^ @@ -499,7 +498,7 @@ File.write (Path.explode file_name) o string_for_report (* theory -> mtd list -> thm list -> string -> unit *) -fun mutate_theorems_and_write_report thy mtds thms file_name = +fun mutate_theorems_and_write_report thy max_mutants mtds thms file_name = let val _ = Output.urgent_message "Starting Mutabelle..." val ctxt = Proof_Context.init_global thy @@ -522,7 +521,7 @@ "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^ "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^ "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n"); - map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms; + map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy max_mutants mtds) thms; () end