#!/bin/bash



TIMEFORMAT=%R


short_header () {
    printf "\\\\begin{tabular}{|l|c|c|c|}\n\hline\n" >> $SHORT
    printf "Node name & \# guarantees , \# assumes of callees & k & Proof time\\\\\\\\\hline\hline\n" >> $SHORT
}

long_header () {
    printf "\\\begin{tabular}{|l|c|c|c|}\n\hline\n" >> $LONG
    printf "Node name & \# Property & Method & Proof time\\\\\\\\\hline\hline\n">> $LONG
}

short_null_version () {
    printf "\\\\verb!$node! & (0,0) & - & -\\\\\\\\\n" >> $SHORT
}

short_version () {
    nb_ass=`cat log | grep Success | grep assume | wc -l`
    nb_gua=`cat log | grep Success | grep guarantee | wc -l`
    max_k=`cat log | grep k= | sed "s/.*k=\([0-9]*\).*/\1/" | sort -n  | tail -1`
    printf "\\\\verb!$node! & ($nb_gua, $nb_ass) & ${max_k}  & ${TIME}s \\\\\\\\" >> $SHORT;
    }

long_null_version () {
    printf "\\\\verb!$node! & - & - & -\\\\\\\\ \\\\hline \n"  >> $LONG
}

long_version () {
    cat log
    props=`grep "<Success>" log`
    FIRST=0
    printf "\\\\verb!$node!" >> $LONG;
     # &&&\\\\\\\\\n" >> $LONG;
    while IFS= read -r line; do
	# DETECTING TYPE
	echo $line | grep "assume"  >& /dev/null
	retVal=$?
	if [ $retVal -eq 0 ]; then
	    kind="assume"
	else
	    echo $line | grep "guarantee"  >& /dev/null
	    retVal=$?
	    if [ $retVal -eq 0 ]; then
		kind="guarantee"
	    else
		kind="unknown type"
	    fi
	fi
	# DETECTION METHOD
	method=`echo $line | sed "s/.*is valid by \(.*\) after .*/\1/"`
	echo $method
	echo $method | grep "property directed reachability"  >& /dev/null
	retVal=$?
	if [ $retVal -eq 0 ]; then
	    method="PDR"
	else
	    echo $method | grep "inductive step"  >& /dev/null
	    retVal=$?
	    if [ $retVal -eq 0 ]; then
		method="induction"
	   # else
	#	echo $method | grep "\([0-9]*\)-induction"  >& /dev/null
	#	retVal=$?
	#	if [ $retVal -ne 0 ]; then
	#	    # doing nothing
	#	else
	#	    echo "unknown type: $method"
	#	fi
	    fi
	fi
	# TIME
	time=`echo $line | sed "s/.*after \(.*\)\./\1/"`
	# echo $time
	
	
	# echo "xxxx line = $line - $kind - $method - $time"
	printf "& $kind & $method & $time\\\\\\\\\n" >> $LONG;
    done <<< "$props"
    printf "\\\\hline\n" >> $LONG;
    
    }

analyse_file () {
for node in `grep ^node $file | grep -v foo | sed "s/node //;s/(.*//" |xargs`; do
    node_enc=`echo $node | sed "s/_/\\\\_/g"`
    rm -f log
    # killing kind2 and waiting 10 seconds to make sure all subprocesses are dead 
    killall kind2 >& /dev/null
    sleep 10
    TIME=$( { time kind2 --check_subproperties false --lus_main $node $file  | sed $'s,\x1b\\[[0-9;]*[a-zA-Z],,g' &> log; } 2>&1 )
    cat log | grep "has no property" > /dev/null
    retVal=$?
    if [ $retVal -ne 0 ]; then
	short_version;
	long_version;
    else
	short_null_version;
	long_null_version;
	
    fi
done

}

SHORT=1

SHORT=short.tex
LONG=long.tex
rm -f $SHORT
rm -f $LONG

printf "`kind2 --version`\n\n">> $SHORT
printf "`kind2 --version`\n\n">> $LONG

for file in eventually_cb.lus always_cb.lus until_cb_v3.lus; do
    printf " File $file\n\n" >> $SHORT
    printf " File $file\n\n" | tee -a $LONG
    short_header 
    long_header 
    
    analyse_file
    printf "\\\\hline\n\\\\end{tabular}\n\n\n" >> $SHORT
    printf "\\\\hline\n\\\\end{tabular}\n\n\n" >> $LONG

done

