#!/bin/bash

PMLFILE=$1
FORMULA=$2
NEVERFILE=never.$$
TMPFILE=pan.$$

spin -f "!($2)" > $NEVERFILE
spin -a -N $NEVERFILE $1
cc -o pan pan.c > /dev/null
./pan -a -n | tee $TMPFILE

if grep "errors: 0" $TMPFILE > /dev/null
then
	echo "===> NO ERRORS FOUND; PROPERTY HOLDS."
else
	echo "===> THE PROPERTY DOES NOT HOLD, AS SHOWN BY THIS COUNTEREXAMPLE:"
	spin -p -t $1
	rm $1.trail
fi

rm $NEVERFILE
rm $TMPFILE
rm pan pan.*