|
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 |