src/HOL/Mutabelle/lib/Tools/mutabelle
changeset 40975 498f272b4bcb
child 41021 3efa0ec42ed4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Dec 06 10:52:46 2010 +0100
     1.3 @@ -0,0 +1,107 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Author: Lukas Bulwahn
     1.7 +#
     1.8 +# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
     1.9 +
    1.10 +
    1.11 +PRG="$(basename "$0")"
    1.12 +
    1.13 +function usage() {
    1.14 +  echo
    1.15 +  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
    1.16 +  echo
    1.17 +  echo "  Options are:"
    1.18 +  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
    1.19 +  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
    1.20 +  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
    1.21 +  echo
    1.22 +  echo "  THEORY is the name of the theory of which all theorems should be mutated and tested"
    1.23 +  exit 1
    1.24 +}
    1.25 +
    1.26 +
    1.27 +## process command line
    1.28 +
    1.29 +# options
    1.30 +
    1.31 +while getopts "L:T:O:t:q?" OPT
    1.32 +do
    1.33 +  case "$OPT" in
    1.34 +    L)
    1.35 +      MIRABELLE_LOGIC="$OPTARG"
    1.36 +      ;;
    1.37 +    T)
    1.38 +      MIRABELLE_IMPORT_THEORY="$OPTARG"
    1.39 +      ;;
    1.40 +    O)
    1.41 +      MIRABELLE_OUTPUT_PATH="$OPTARG"
    1.42 +      ;;
    1.43 +    \?)
    1.44 +      usage
    1.45 +      ;;
    1.46 +  esac
    1.47 +done
    1.48 +
    1.49 +shift $(($OPTIND - 1))
    1.50 +
    1.51 +[ "$#" -ne 1 ] && usage
    1.52 +
    1.53 +MUTABELLE_TEST_THEORY="$1"
    1.54 +
    1.55 +## main
    1.56 +
    1.57 +echo "Starting Mutabelle..."
    1.58 +
    1.59 +# setup
    1.60 +
    1.61 +mkdir -p "$MIRABELLE_OUTPUT_PATH"
    1.62 +
    1.63 +echo "theory Mutabelle_Test
    1.64 +imports $MUTABELLE_IMPORT_THEORY
    1.65 +uses     
    1.66 +  \"$MUTABELLE_HOME/mutabelle.ML\"
    1.67 +  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
    1.68 +begin
    1.69 +
    1.70 +ML {*
    1.71 +val mtds = [
    1.72 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
    1.73 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\"
    1.74 +]
    1.75 +*}
    1.76 +
    1.77 +ML {*
    1.78 +fun mutation_testing_of thy =
    1.79 +  (MutabelleExtra.random_seed := 1.0;
    1.80 +  MutabelleExtra.thms_of false thy
    1.81 +  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    1.82 +         @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
    1.83 +*}
    1.84 +
    1.85 +ML {*
    1.86 +  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
    1.87 +*}
    1.88 +
    1.89 +end" > $MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy
    1.90 +
    1.91 +# execution
    1.92 +
    1.93 +$ISABELLE_PROCESS -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC  > /dev/null 2>&1
    1.94 +
    1.95 +# make statistics
    1.96 +
    1.97 +GenuineCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: GenuineCex" | wc -l)
    1.98 +NoCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: NoCex" | wc -l)
    1.99 +Timeout_random=$(cat /$MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Timeout" | wc -l)
   1.100 +Errors_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Error" | wc -l)
   1.101 +
   1.102 +GenuineCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: GenuineCex" | wc -l)
   1.103 +NoCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: NoCex" | wc -l)
   1.104 +Timeout_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Timeout" | wc -l)
   1.105 +Errors_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Error" | wc -l)
   1.106 +
   1.107 +
   1.108 +echo "random      :" C: $GenuineCex_random N: $NoCex_random T: $Timeout_random E: $Errors_random
   1.109 +echo "exhaustive  :" C: $GenuineCex_exh N: $NoCex_exh T: $Timeout_exh E: $Errors_exh
   1.110 +