34965
|
1 |
theory MutabelleExtra
|
|
2 |
imports Complex_Main SML_Quickcheck
|
|
3 |
(*
|
|
4 |
"~/Downloads/Jinja/J/TypeSafe"
|
|
5 |
"~/Downloads/Jinja/J/Annotate"
|
|
6 |
(* FIXME "Example" *)
|
|
7 |
"~/Downloads/Jinja/J/execute_Bigstep"
|
|
8 |
"~/Downloads/Jinja/J/execute_WellType"
|
|
9 |
"~/Downloads/Jinja/JVM/JVMDefensive"
|
|
10 |
"~/Downloads/Jinja/JVM/JVMListExample"
|
|
11 |
"~/Downloads/Jinja/BV/BVExec"
|
|
12 |
"~/Downloads/Jinja/BV/LBVJVM"
|
|
13 |
"~/Downloads/Jinja/BV/BVNoTypeError"
|
|
14 |
"~/Downloads/Jinja/BV/BVExample"
|
|
15 |
"~/Downloads/Jinja/Compiler/TypeComp"
|
|
16 |
*)
|
|
17 |
(*"~/Downloads/NormByEval/NBE"*)
|
|
18 |
uses "mutabelle.ML"
|
|
19 |
"mutabelle_extra.ML"
|
|
20 |
begin
|
|
21 |
|
|
22 |
ML {* val old_tr = !Output.tracing_fn *}
|
|
23 |
ML {* val old_wr = !Output.writeln_fn *}
|
|
24 |
ML {* val old_pr = !Output.priority_fn *}
|
|
25 |
ML {* val old_wa = !Output.warning_fn *}
|
|
26 |
|
|
27 |
quickcheck_params [size = 5, iterations = 1000]
|
|
28 |
(*
|
|
29 |
nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
|
|
30 |
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
|
|
31 |
*)
|
|
32 |
ML {* Auto_Counterexample.time_limit := 10 *}
|
|
33 |
|
|
34 |
|
|
35 |
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
|
|
36 |
|
|
37 |
ML {*
|
|
38 |
(*
|
|
39 |
MutabelleExtra.random_seed := 1.0;
|
|
40 |
MutabelleExtra.thms_of true @{theory Complex_Main}
|
|
41 |
|> MutabelleExtra.take_random 1000000
|
|
42 |
|> (fn thms => List.drop (thms, 1000))
|
|
43 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
|
|
44 |
@{theory} [MutabelleExtra.quickcheck_mtd "SML",
|
|
45 |
MutabelleExtra.quickcheck_mtd "code"
|
|
46 |
(*MutabelleExtra.refute_mtd,
|
|
47 |
MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
|
|
48 |
*)
|
|
49 |
*}
|
|
50 |
|
|
51 |
ML {* Output.tracing_fn := old_tr *}
|
|
52 |
ML {* Output.writeln_fn := old_wr *}
|
|
53 |
ML {* Output.priority_fn := old_pr *}
|
|
54 |
ML {* Output.warning_fn := old_wa *}
|
|
55 |
|
|
56 |
end |