author | wenzelm |
Thu, 10 Mar 2016 17:30:04 +0100 | |
changeset 62589 | b5783412bfed |
parent 62588 | cd266473b81b |
child 62676 | 1792f8ed2b04 |
permissions | -rwxr-xr-x |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
2 |
# |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
3 |
# Author: Lukas Bulwahn |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
4 |
# |
41309
2e9bf718a7a1
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents:
41191
diff
changeset
|
5 |
# DESCRIPTION: mutant-testing for counterexample generators and automated tools |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
6 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
7 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
8 |
PRG="$(basename "$0")" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
9 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
10 |
function usage() { |
42119
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
11 |
[ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
12 |
echo |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
13 |
echo "Usage: isabelle $PRG [OPTIONS] THEORY" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
14 |
echo |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
15 |
echo " Options are:" |
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
16 |
echo " -L LOGIC parent logic to use (default $MUTABELLE_LOGIC)" |
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
17 |
echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)" |
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
18 |
echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)" |
46310 | 19 |
echo " -N NUMBER number of lemmas to choose randomly, if not given all lemmas are chosen" |
46453
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
20 |
echo " -M NUMBER number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)" |
46454
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
21 |
echo " -X NUMBER number of mutations in a mutant (default $MUTABELLE_NUMBER_OF_MUTATIONS)" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
22 |
echo |
41309
2e9bf718a7a1
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents:
41191
diff
changeset
|
23 |
echo " THEORY is the name of the theory of which all theorems should be" |
2e9bf718a7a1
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents:
41191
diff
changeset
|
24 |
echo " mutated and tested." |
41077 | 25 |
echo |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
26 |
exit 1 |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
27 |
} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
28 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
29 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
30 |
## process command line |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
31 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
32 |
# options |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
33 |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
34 |
MUTABELLE_IMPORTS="" |
41077 | 35 |
|
46454
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
36 |
while getopts "L:T:O:N:M:X:" OPT |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
37 |
do |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
38 |
case "$OPT" in |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
39 |
L) |
41021 | 40 |
MUTABELLE_LOGIC="$OPTARG" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
41 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
42 |
T) |
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
43 |
MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\"" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
44 |
;; |
41077 | 45 |
O) |
41021 | 46 |
MUTABELLE_OUTPUT_PATH="$OPTARG" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
47 |
;; |
46310 | 48 |
N) |
49 |
NUMBER_OF_LEMMAS="$OPTARG" |
|
50 |
;; |
|
46453
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
51 |
M) |
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
52 |
MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG" |
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
53 |
;; |
46454
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
54 |
X) |
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
55 |
MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG" |
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
56 |
;; |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
57 |
\?) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
58 |
usage |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
59 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
60 |
esac |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
61 |
done |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
62 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
63 |
shift $(($OPTIND - 1)) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
64 |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
65 |
if [ "$MUTABELLE_IMPORTS" = "" ] |
41077 | 66 |
then |
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
67 |
MUTABELLE_IMPORTS="$MUTABELLE_IMPORT_THEORY" |
41077 | 68 |
fi |
69 |
||
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
70 |
[ "$#" -ne 1 ] && usage |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
71 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
72 |
MUTABELLE_TEST_THEORY="$1" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
73 |
|
42119
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
74 |
if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
75 |
MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$" |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
76 |
PURGE_OUTPUT="true" |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
77 |
fi |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
78 |
|
41077 | 79 |
export MUTABELLE_OUTPUT_PATH |
80 |
||
46310 | 81 |
if [ "$NUMBER_OF_LEMMAS" != "" ]; then |
82 |
MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS" |
|
83 |
fi |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
84 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
85 |
## main |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
86 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
87 |
echo "Starting Mutabelle..." |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
88 |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
89 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
90 |
# setup |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
91 |
|
41077 | 92 |
mkdir -p "$MUTABELLE_OUTPUT_PATH" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
93 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
94 |
echo "theory Mutabelle_Test |
46499 | 95 |
imports $MUTABELLE_IMPORTS |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
96 |
uses |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
97 |
\"$MUTABELLE_HOME/mutabelle.ML\" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
98 |
\"$MUTABELLE_HOME/mutabelle_extra.ML\" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
99 |
begin |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
100 |
|
45040
8570623e3b6d
changing quickcheck_timeout to 30 seconds in mutabelle's testing
bulwahn
parents:
43912
diff
changeset
|
101 |
declare [[quickcheck_timeout = 30]] |
8570623e3b6d
changing quickcheck_timeout to 30 seconds in mutabelle's testing
bulwahn
parents:
43912
diff
changeset
|
102 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
103 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
104 |
val mtds = [ |
43912
13e6a4e70219
exporting function in quickcheck; adapting mutabelle script
bulwahn
parents:
43380
diff
changeset
|
105 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", |
46453
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
106 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\", |
43912
13e6a4e70219
exporting function in quickcheck; adapting mutabelle script
bulwahn
parents:
43380
diff
changeset
|
107 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", |
46453
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
108 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\", |
45165
f4896c792316
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
bulwahn
parents:
45040
diff
changeset
|
109 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\", |
46453
9e83b7c24b05
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn
parents:
46452
diff
changeset
|
110 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\", |
43912
13e6a4e70219
exporting function in quickcheck; adapting mutabelle script
bulwahn
parents:
43380
diff
changeset
|
111 |
MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false |
45165
f4896c792316
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
bulwahn
parents:
45040
diff
changeset
|
112 |
#> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\" |
46452
e4f1cda51df6
increase timeout to 30 seconds; changing mutabelle script
bulwahn
parents:
46310
diff
changeset
|
113 |
(*, MutabelleExtra.refute_mtd, *) |
e4f1cda51df6
increase timeout to 30 seconds; changing mutabelle script
bulwahn
parents:
46310
diff
changeset
|
114 |
, MutabelleExtra.nitpick_mtd |
e4f1cda51df6
increase timeout to 30 seconds; changing mutabelle script
bulwahn
parents:
46310
diff
changeset
|
115 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
116 |
] |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
117 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
118 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
119 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
120 |
fun mutation_testing_of thy = |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
121 |
(MutabelleExtra.random_seed := 1.0; |
46310 | 122 |
MutabelleExtra.thms_of false thy $MUTABELLE_FILTER |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
123 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
46454
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
124 |
@{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
125 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
126 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
127 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
128 |
mutation_testing_of @{theory $MUTABELLE_TEST_THEORY} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
129 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
130 |
|
41077 | 131 |
end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
132 |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
133 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
134 |
# execution |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
135 |
|
62589
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents:
62588
diff
changeset
|
136 |
isabelle process -o auto_time_limit=10.0 \ |
62573 | 137 |
-e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1 |
41077 | 138 |
|
139 |
||
140 |
[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed" |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
141 |
|
41949
f9a2e10c49cb
more conventional Mutabelle settings -- similar to Mirabelle;
wenzelm
parents:
41309
diff
changeset
|
142 |
|
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
143 |
# make statistics |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
144 |
|
41077 | 145 |
function count() { |
45397 | 146 |
cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l | sed "s/ //" |
41077 | 147 |
} |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
148 |
|
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
149 |
function mk_stat() { |
45397 | 150 |
printf "%-40s C:$(count $1 "GenuineCex") P:$(count $1 "PotentialCex") N:$(count $1 "NoCex") T:$(count $1 "Timeout") D:$(count $1 "Donno") E: $(count $1 "Error")\n" "$1" |
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
151 |
} |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
152 |
|
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
153 |
mk_stat "quickcheck_random" |
46499 | 154 |
mk_stat "quickcheck_random_int" |
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
155 |
mk_stat "quickcheck_exhaustive" |
46499 | 156 |
mk_stat "quickcheck_exhaustive_int" |
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
157 |
mk_stat "quickcheck_narrowing" |
46499 | 158 |
mk_stat "quickcheck_narrowing_int" |
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
159 |
mk_stat "quickcheck_narrowing_nat" |
46499 | 160 |
##mk_stat "refute" |
43149
9675d631df3d
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
bulwahn
parents:
43148
diff
changeset
|
161 |
mk_stat "nitpick" |
42119
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
162 |
|
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
163 |
## cleanup |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
164 |
|
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
165 |
if [ -n "$PURGE_OUTPUT" ]; then |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
166 |
rm -rf "$MUTABELLE_OUTPUT_PATH" |
21714b0de625
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
krauss
parents:
41949
diff
changeset
|
167 |
fi |