verify.sh

#!/bin/sh


FILENAME=""

SAFETY=false
NOTENDSTATE=false
TRAIL=false
VERIFY=false


for arg in ${@:1}; do
        if [ "$arg" == "s" ]; then
                echo "#### SAFETY ####"
                VERIFY=true
                SAFETY=true

        elif [ "$arg" == "e" ]; then
                echo "#### NOT VERIFY ENDSTATE ####"
                VERIFY=true
                NOTENDSTATE=true

        elif [ "$arg" == "t" ]; then
                echo "#### PRINT TRAIL ####"
                VERIFY=true
                TRAIL=true

        elif [ "$arg" == "v" ]; then
                echo "#### VERIFY ####"
                VERIFY=true

        else
                FILENAME="$arg"
        fi
done

FILENAME="$FILENAME"

echo "#### FILENAME IS $FILENAME ####"

if [ ! -e $FILENAME ]; then
        echo "### ERROR: $FILENAME DOES NOT EXIST ###";
        exit 1
fi

mkdir -p /tmp/verify
cp $FILENAME /tmp/verify
cd /tmp/verify

if $VERIFY; then
        # compile pml file to c
        echo "### COMPILE PML TO C ###"
        spin -a "$FILENAME"

        # compile pan
        echo "### COMPILE C ###"
        if $SAFETY; then
                gcc -DSAFETY -o pan pan.c
        else
                gcc -o pan pan.c
        fi

        # verify
        echo ""; echo ""
        echo "### VERIFY ###"
        if $NOTENDSTATE; then
                ./pan -E
        else
                ./pan
        fi

        # trail
        if $TRAIL; then
                echo ""; echo ""
                echo "### TRAIL ###"

                spin -t -p $FILENAME
        fi
else
        # run pml
        echo "### RUNNING PML ###"
        spin "$FILENAME"
fi


rm -fr /tmp/verify