Run two processes, wait for the fastest one and kill another. (Used for SYNTCOMP'21.)

run_sdf.sh

#!/bin/bash

# Run two processes of tlsf-sdf in parallel:
# - one for the original spec,
# - one for the dualized spec.
# All agruments are relayed to tlsf-sdf-opt.


set -m  # enable 'job control'

fileR=$(mktemp)
fileU=$(mktemp)

function check_and_exit() {
    pR_dead=0
    pU_dead=0

    if ! kill -0 $pR > /dev/null 2>&1; then
        pR_dead=1
    fi

    if ! kill -0 $pU > /dev/null 2>&1; then
        pU_dead=1
    fi

    if (($pR_dead == 1)); then
        #echo "pR dead"
        status=$(tail -n1 $fileR)
        if [ "$status" = "REALIZABLE" ]; then
            cat $fileR
            kill -9 $pU > /dev/null 2>&1
            exit 10
        fi
    fi

    if (($pU_dead == 1)); then
        #echo "pU dead"
        status=$(tail -n1 $fileU)
        if [ "$status" = "UNREALIZABLE" ]; then
            cat $fileU
            kill -9 $pR > /dev/null 2>&1
            exit 20
        fi
    fi

    if (($pR_dead == 1)) && (($pU_dead == 1)); then
        # reaching this point means both statuses are UNKNOWN
        echo UNKNOWN
        exit 30
    fi
}

#cmdR="sleep 0.1; echo hihihi; echo REALIZABLE"
#cmdU="sleep 1; echo hohoho; echo UNKNOWN"

cmdR="./tlsf-sdf-opt $@ -s"
cmdU="./tlsf-sdf-opt $@ -s -d"

(eval "$cmdR") > $fileR &  # start synthesizer for the original spec
pR=$!

(eval "$cmdU") > $fileU &  # start synthesizer for the dualized spec
pU=$!

wait -n -f   # wait for the next job to terminate
check_and_exit

wait -n -f   # wait for the next job to terminate
check_and_exit



echo "UNREACHABLE"