#!/bin/bash

set -e

SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)

cc="gcc-13"

time_out="time.txt"

# $1: property
# $2: N value
# $3: LENGTH value
# $4: R value
test-property() {
    id="${1}_${2}_${3}_${4}"
    filename="reversal_$id.pml"
    pan_name="pan_$id"
    trace="trace_$id.txt"

    rm -fv "$SCRIPT_DIR/$filename.trail" || true
    m4 -I"$SCRIPT_DIR" -DN="$2" -DLENGTH="$3" -DR="$4" -DLTL="$1" reversal.pml.m4 > "$filename"
    spin -a "$filename"

    "$cc" -Wno-format-overflow -o "$pan_name" pan.c
    rm pan.*

    echo "${1},${2},${3},${4}," >> "$time_out"
    /usr/bin/time -a -o "$time_out" "./$pan_name" -a -N "$1" | tee "$trace"

    if [ -f "$SCRIPT_DIR/$filename.trail" ]; then
        # rerun with printf
        spin -a "$filename"
        "$cc" -Wno-format-overflow -DPRINTF -o "$pan_name" pan.c
        rm ./pan.*
        "./$pan_name" -a -N "$1" | tee "$trace"

        echo "VERIFICATION FAILED, exiting..." >2
        exit 1
    fi

    rm "$pan_name" "$filename"
}

# grid search fixed parameters
max=8
prop="seq_eq_parallel"

cd "$SCRIPT_DIR"

for n in $(seq 2 "$max"); do
    for length in 8; do
        for r in $(seq 2 "$max"); do
            echo ">>> test-property $prop n=$n length=$length r=$r"
            test-property "$prop" "$n" "$length" "$r"
        done
    done
done