# HG changeset patch
# User bulwahn
# Date 1292495467 -3600
# Node ID 4aa6465fec65e0abcef7618e57c899270ed79260
# Parent  0bdc6fac5f48e5fff5545a0fae418ece50117f0d
added nitpick to mutabelle script

diff -r 0bdc6fac5f48 -r 4aa6465fec65 src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Dec 16 11:31:06 2010 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Dec 16 11:31:07 2010 +0100
@@ -80,7 +80,8 @@
 ML {*
 val mtds = [
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
-  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\"
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
+  MutabelleExtra.nitpick_mtd
 ]
 *}
 
@@ -108,11 +109,13 @@
 # make statistics
 
 function count() {
-  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "quickcheck_$1: $2" | wc -l
+  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l
 }
 
-echo "random      : C: $(count "random" "GenuineCex") N: $(count "random" "NoCex") \
-T: $(count "random" "Timeout") E: $(count "random" "Error")"
-echo "exhaustive  : C: $(count "exhaustive" "GenuineCex") N: $(count "exhaustive" "NoCex") \
-T: $(count "exhaustive" "Timeout") E: $(count "exhaustive" "Error")"
+echo "random      : C: $(count "quickcheck_random" "GenuineCex") N: $(count "quickcheck_random" "NoCex") \
+T: $(count "quickcheck_random" "Timeout") E: $(count "quickcheck_random" "Error")"
+echo "exhaustive  : C: $(count "quickcheck_exhaustive" "GenuineCex") N: $(count "quickcheck_exhaustive" "NoCex") \
+T: $(count "quickcheck_exhaustive" "Timeout") E: $(count "quickcheck_exhaustive" "Error")"
+echo "nitpick     : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
+T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")"