spotPath="~/spot-2.9.7/bin"

if [ "$#" -le 3 ]; then
	echo "Need 4 parameters :\n <directory of .smv files> <LTLSPEC : safety, persistence,...> <Number of random LTL> <output directory>";
	exit 1;
fi


DIRECTORY=$1"/"
ltlType=$2
number=$3
outputdir=$4
number=$((number+1))




echo "dirname "$DIRECTORY

for f in $DIRECTORY*.smv; do 
	
	echo $f"\n"

	if [ ! -f "$f" ]; then
		continue;
	fi

	f_no_extension=$(echo "$f" | sed -e 's/\.[^.]*$//');

	SMVName=$(basename $f_no_extension)
	SMVfile=$DIRECTORY"/"$SMVName

	LTLfilename=$SMVfile"_LTLSPEC.txt"

	modelNameUnparsed="varnames"$ltlType".txt"

	modelNameParsed="modelNames"$ltlType".txt"

	./bmctool -tool=c -conv=1 -k=40 -show-var $SMVfile > $modelNameUnparsed

	python3 scripts/benchmark_preprocess.py $modelNameUnparsed > $modelNameParsed

	if [ $ltlType = "reactivity" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) |  ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --persistence --unabbreviate=R | ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --recurrence --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename
	elif [ $ltlType = "obligation" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) |  ~/spot-2.9.7/bin/ltlfilt -p -r --remove-wm --obligation --unabbreviate=R | ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --safety --unabbreviate=R | ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --guarantee --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename;
	elif [ $ltlType = "recurrence" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) | ~/spot-2.9.7/bin/ltlfilt -p -r --remove-wm --recurrence --unabbreviate=R | ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --obligation --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename;
	elif [ $ltlType = "safety" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) | ~/spot-2.9.7/bin/ltlfilt -p -r --remove-wm --safety --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename;
	elif [ $ltlType = "guarantee" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) | ~/spot-2.9.7/bin/ltlfilt -p -r --remove-wm --guarantee --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename;
	elif [ $ltlType = "persistence" ]; then
		~/spot-2.9.7/bin/randltl --ltl --simplify -p -n $number $(cat $modelNameParsed) | ~/spot-2.9.7/bin/ltlfilt -p -r --remove-wm --persistence --unabbreviate=R | ~/spot-2.9.7/bin/ltlfilt -v -p -r --remove-wm --obligation --unabbreviate=R | sed '/1/d' | tr \" " " > $LTLfilename;
	else
		echo "Eroor ltl type "$ltlType
		exit 1 
	fi;

	rm $modelNameUnparsed $modelNameParsed

	i=0
	while read ltl; do
		new_smv_file=$outputdir"/"$SMVName"_"$ltlType"_"$i".smv"
		sed '/LTLSPEC/Q' $SMVfile".smv" > $new_smv_file
		echo "\nLTLSPEC "$ltl"\n" >> $new_smv_file
		i=$((i+1));
	done < $LTLfilename

	echo $SMVNAME" "$i": done.\n"
done;