#!/bin/sh
# -*- sh -*-
set -e
. util

complain() {
    echo "### $@" > complaint
}

die() {
    test -f progress && cat progress
    rm progress
    complain "$@"
    exit 1
}

report() {
    test -f report || return 0
    if [ "$1" = '-q' ]; then
        shift;
        local QUIET=1
    fi
    v=`grep "^$1:" report | cut -f2- -d: | cut -c2-`
    test -n "$3" && op="$3" || op="=";

    if test -n "$2" && ! test "$2" "$op" "$v"; then
        test "$QUIET" = 1 || complain "Expected $1 $op '$2' but got '$v' instead"
        return 1
    fi
    echo "$v" > value;
    return 0
}

report_print() {
    report "$@"
    cat value
}

ltl_algorithm() {
    report -q Algorithm OWCTY && return 0
    report -q Algorithm "Nested DFS" && return 0
    report -q Algorithm MAP && return 0
    return 1
}

reach_algorithm() {
    report -q Algorithm Reachability && return 0
    report -q Algorithm "Weak Reachability" && return 0
    report -q Algorithm CSDR && return 0
    return 1
}

ltl_valid() {
    report Finished Yes
    report -q Property-Type neverclaim || return 0
    ltl_algorithm || return 0
    report Property-Holds Yes
}

ltl_invalid() {
    report Finished Yes
    report -q Property-Type neverclaim || return 0
    ltl_algorithm || return 0
    report Property-Holds No
}

reachability_valid() {
    report Finished Yes
    reach_algorithm || return 0
    report Property-Holds Yes
}

reachability_deadlock() {
    report Finished Yes
    report -q Property-Type deadlock || return 0
    reach_algorithm || return 0
    report Property-Holds No
    report CE-Type deadlock
}

reachability_goal() {
    report Finished Yes
    report -q Property-Type goal || return 0
    reach_algorithm || return 0
    report Property-Holds No
    report CE-Type goal
}

statespace() {
    test -f report || return 0

    report Finished Yes
    op=-eq
    report -q Full-State-Space No && op=-le
    grep "^Transformations:.*POR" report && op=-le

    states=`report_print States-Visited`
    trans=`report_print Transition-Count`
    accept=`report_print States-Accepting`
    dead=`report_print Deadlock-Count`

    test $states $op $1 || die "States-Visited: $1 expected, $states got"
    test "$trans" = "-" || test $trans $op $2 || die "Transition-Count: $2 expected, $trans got"
    test $accept $op $3 || die "States-Accepting: $3 expected, $accept got"
    test "$dead" = "-" || test $dead $op $4 || die "Deadlock-Count: $4 expected, $dead got"
}

cleanup() {
    rm -f progress report testcase.{c,cpp,dve,dess} complaint *.core core*
}

clear() {
    cleanup
    echo "#### PASSED"
    echo
}

owcty_sizes() {
    test -f report || return 0
    test -f progress || return 0

    if ! grep -q "^Algorithm: OWCTY" report; then return 0; fi
    if grep -q "^Full-State-Space: No" report; then return 0; fi
    if grep -q "^Transformations:.*POR" report; then return 0; fi

    grep '|S| = ' progress | $esed -e 's,[^0-9]*([0-9]+).*,\1,' > numbers
    rm -f numbers-right
    for n in $@; do echo $n >> numbers-right; done
    diff -u numbers-right numbers
}

debris() {
    test -f progress && (cat progress; echo) || true

    for T in testcase.{c,cpp,dve}; do
        test -f $T && (nl -ba $T; echo) || true
    done

    if which gdb > /dev/null; then
        for core in $(ls *.core core* 2>/dev/null); do
            bin=$(gdb -batch -c "$core" 2>&1 | grep "generated by" | \
                  sed -e "s,.*generated by \`\([^ ']*\).*,\1,")
            if which lldb > /dev/null; then
                echo bt all | lldb -c "$core" $(which "$bin")
            else
                echo thread apply all bt full > gdb_commands.txt
                echo l >> gdb_commands.txt
                echo quit >> gdb_commands.txt
                gdb -batch -c "$core" -x gdb_commands.txt $(which "$bin")
            fi
        done
    fi || true

    test -f complaint && cat complaint || true
    cleanup
}

verify() {
    if fgrep -q '/* ERRSPEC:' "$1"; then
        spec=$(fgrep '/* ERRSPEC:' $1 | cut -d: -f2- | sed -e "s,^ *,," -e "s, *\*/,,")
        echo spec: $spec
        if ! grep -q "^      [^ .][a-z]*:.*$spec" verify.out; then
            echo "# expected error to be found in $spec, but it was not"
            exit 1
        fi
    elif fgrep -q '/* ERROR' "$1"; then
        location=`fgrep -Hn '/* ERROR' "$1" | cut -d: -f1-2`
        if ! grep -q "^      location: $location" verify.out; then
            nl -ba "$1"
            echo "# expected error to be found at $location, but it was not"
            exit 1
        fi
        if ! grep -q "^      location: $location" sim.out; then
            nl -ba "$1"
            echo "# expected error to be found in divine sim at $location, but it was not"
            exit 1
        fi
    else
        if ! grep -q "error found: no" verify.out &&
           ! grep -q "error found: boot" verify.out; then
            nl -ba "$1"
            grep '^      location' verify.out || true
            echo "# no errors were expected but one was found anyway"
            exit 1
        fi
    fi
}

sim()
{
    cat > expected
    if ! ordgrep expected < sim.out; then exit 1; fi
}

"$@"