
all: tools results-aspic results-reps smt-ai smt-ai-call kind-ai kind-ai-multi comparison final_table

lustre: fastConv-tool
	@echo Generate lustre files >&2
	@mkdir -p lustre
	@for i in fst/*.fst; do \
	  ./tools/fastConv < $$i > lustre/`basename $$i .fst`.lus 2>/dev/null; \
	done

# Doing it for Ch79, Ch79v2 and ASPIC
#		| grep "\-\-\-\-" | sed "s/-----> {/=> (/g;s/}/)/g;s/, / and /g" | grep -v "__bad" > results/`basename $$i .fst`.$$t.result; 

results-aspic: tools/aspicV3.1
	@mkdir -p results
	@mkdir -p runtime
	@for i in fst/*.fst; do \
	  for t in "ch79" "ch79v2" "aspic"; do \
	    case $${t} in \
	      ch79) options="-noaccel -nouptos";; \
	      ch79v2) options="-noaccel";; \
	      aspic) options="";; \
	    esac; \
	    /usr/bin/time --output=runtime/`basename $$i .fst`.$$t.time ./tools/aspicV3.1 $$options $$i > results/`basename $$i .fst`.$$t.raw; \
	    rm -f results/`basename $$i .fst`.$$t.result; touch results/`basename $$i .fst`.$$t.result; \
	    for v in `cat $$i | grep states | sed "s/states //;s/;//;s/,/ /g"`; do \
		grep $${v}__split results/`basename $$i .fst`.$$t.raw > /dev/null; \
		if [ $$? -eq 0 ]; then \
		   cat results/`basename $$i .fst`.$$t.raw | xargs | sed "s/.*\($${v}\)__split + $${v} == {.*} U {.*} = {\([^}]*\)}.*/\1 => \2/;s/, / and /g" >> results/`basename $$i .fst`.$$t.result;\
		else \
		   cat results/`basename $$i .fst`.$$t.raw | grep "$$v \-\-\-\-" | sed "s/-----> {/=> (/g;s/}/)/g;s/, / and /g" | grep -v "__bad" >> results/`basename $$i .fst`.$$t.result; \
		fi; \
	    done; \
	    cat $$i | grep states | sed "s/states //;s/;//;s/,/ or /g" >> results/`basename $$i .fst`.$$t.result; \
	  done;\
	done

results-reps: tools/aspicV3.1
	@mkdir -p results
	@cd fst; for i in *.fst; do \
	  /usr/bin/time --output=../runtime/`basename $$i .fst`.lookahead.time ../tools/aspicV3.1 -log -reps $$i > /dev/null; \
	  cat `basename $$i .fst`.log | xargs | sed "s/.*output=\[ \(.*\) ]/\1/;s/{ v = \([^,]*\), attrvertex = {\([^}]*\)}{[^}]*} } /\1 => \2\n/g;" | grep -v "__bad" | grep -v "info =" | sed "s/=> /=> true and \n/;s/,/ and \n/g" | grep -v "$$>=0" | grep -v "1>0" | xargs | sed "s/ \([^' ' =]*\) =>/\n\1 =>/g;s/ and$$/ and true/g;s/ and\n/ and true\n/g" > ../results/`basename $$i .fst`.lookahead.result; \
	cat $$i | grep states | sed "s/states //;s/;//;s/,/ or /g" >> ../results/`basename $$i .fst`.lookahead.result; \
	done

kind-ai: lustre
	@echo "Running kind-ai against lustre files" >&2
	@mkdir -p results
	@mkdir -p runtime
	@for i in lustre/*.lus; do \
	  echo $$i >&2; \
	  fst="fst/`basename $$i .lus`.fst"; \
	  sed_rule=`cat $$fst | grep states | sed "s/states //;s/;//;s/,/\n/g;s/ //g" | nl -v0 - | sed "s/\([0-9]\)\t\(.*\)/s\/(F2L_state) = \1 => \/\\2 => \/g;/g"|xargs`; \
	  /usr/bin/time --output=runtime/`basename $$i .lus`.kind-ai.time kind-ai -packs "{F2L_state:()}" -full-packs -min-k 1 -max-k 4 -lustre-output -verbose-level 0 $$i | sed "$${sed_rule}" > results/`basename $$i .lus`.kind-ai.raw;\
	  line=""; \
	  while read line; do \
	    echo "$$line" | sed "s/=> (/=>\n(/g;s/) and (/)\n(/g" | grep -v F2L_state | xargs | sed "s/) (/) and (/g;s/^.*=>[' ']*$$//g"; \
	  done < results/`basename $$i .lus`.kind-ai.raw | sed "/^$$/d" > results/`basename $$i .lus`.kind-ai.result;  \
          cat $${fst} | grep states | sed "s/states //;s/;//;s/,/ or /g" >> results/`basename $$i .lus`.kind-ai.result; \
	done

kind-ai-multi: lustre
	@echo "Running kind-ai against lustre files" >&2
	@mkdir -p results
	@mkdir -p runtime
	@for i in lustre/*.lus; do \
	  echo $$i >&2; \
	  fst="fst/`basename $$i .lus`.fst"; \
	  sed_rule=`cat $$fst | grep states | sed "s/states //;s/;//;s/,/\n/g;s/ //g" | nl -v0 - | sed "s/\([0-9]\)\t\(.*\)/s\/(F2L_state) = \1 => \/\\2 => \/g;/g"|xargs`; \
	  finish=0; \
	  cpt=0; \
	  while [ $${finish} -eq 0 ]; do \
	    echo $${cpt}; \
	    /usr/bin/time --output=runtime/`basename $$i .lus`.kind-ai.$${cpt}.time kind-ai -packs "{F2L_state:()}" -full-packs -min-k 1 -max-k 4 -lustre-output -verbose-level 0 -online -max-flush $$cpt $$i | sed "$${sed_rule}" > /tmp/log; \
	    tail -n 1 /tmp/log | grep flush > /dev/null; finish=$$?; \
	    cat /tmp/log | grep -v flush | grep -v "()" > results/`basename $$i .lus`.kind-ai.$${cpt}.raw;\
	    rm /tmp/log; \
	    line=""; \
	    while read line; do \
	      echo "$$line" | sed "s/=> (/=>\n(/g;s/) and (/)\n(/g" | grep -v F2L_state | xargs | sed "s/) (/) and (/g;s/^.*=>[' ']*$$//g"; \
	    done < results/`basename $$i .lus`.kind-ai.$${cpt}.raw | sed "/^$$/d" > results/`basename $$i .lus`.kind-ai.$${cpt}.result;  \
            cat $${fst} | grep states | sed "s/states //;s/;//;s/,/ or /g" >> results/`basename $$i .lus`.kind-ai.$${cpt}.result; \
	    cpt=$$(( $${cpt} + 1 )); \
	  done; \
	done

smt-ai: lustre
	@echo "Generating smt2/packing/partitioning files for each lustre model" >&2
	@mkdir -p results
	@mkdir -p runtime
	@for i in lustre/*.lus; do \
	  echo "$$i" >&2; \
	  fst="fst/`basename $$i .lus`.fst"; \
	  smt2="lustre/`basename $$i .lus`.smt2"; \
	  nodename=`cat $$i | grep node | sed "s/node //;s/ .*$$//"`; \
	  java -jar tools/stuff-lustre_2.9.2-0.1-one-jar.jar $$i `cat $$i | grep node | sed "s/node //;s/ .*$$//"` $${smt2}; \
	  ./tools/fastConv < $${fst} 2>&1 | grep Variables | sed "s/Variables are: //;s/, /\n/g" | grep ": int" | sed "s/: int//" | sed "s/^/$${nodename}_0_/" | xargs > /tmp/log; \
	  echo "(`cat $$i | grep node | sed "s/node //;s/ .*$$//"`_0_F2L_state `cat /tmp/log`)" > lustre/`basename $$i .lus`.packing; \
	  rm /tmp/log; \
	  fresh=`cat $${smt2} | grep assert | sed "s/(.*memu  \(fresh_[0-9]*\) $${nodename}_0_F2L_state).*/\1/"`; \
	  nb_states=`cat $${fst} | grep states | sed "s/states //;s/;//;s/,/\n/g"| wc -l`; \
	  echo "(or " > lustre/`basename $$i .lus`.partitioning; \
	  while [ $${nb_states} -ne 0 ]; do \
	   nb_states=$$(( $${nb_states}-1 )); \
	    echo "(= $${nodename}_0_F2L_state $${nb_states} )" >> lustre/`basename $$i .lus`.partitioning; \
	  done; \
	  echo ")">> lustre/`basename $$i .lus`.partitioning; \
	done

smt-ai-call:
	@echo "Calling smt-ai" >&2
	for i in lustre/*.smt2; do \
	  echo "$$i"; \
	  fst="fst/`basename $$i .smt2`.fst"; \
	  nodename=`cat lustre/\`basename $$i .smt2\`.lus | grep node | sed "s/node //;s/ .*$$//"`; \
	  sed_rule=`cat $$fst | grep states | sed "s/states //;s/;//;s/,/\n/g;s/ //g" | nl -v0 - | sed "s/\([0-9]\)\t\(.*\)/s\/(v_$${nodename}_0_F2L_state = \1) =>\/\\2 =>\/g;/g"|xargs`; \
	  echo "$${sed_rule}" >&2;  \
	  echo "$${nodename}" >&2; \
	  /usr/bin/time --output=runtime/`basename $$i .smt2`.smt-ai.time timeout 60s ./tools/smt-ai -output lustre $$i |grep "OK =" | \
	    sed "s/OK = (() or (\(.*\));/\1/;s/ or /\n/g" | \
	    sed "s/^\((*(v_`echo $${nodename}`_0_F2L_state = [^)]*)\) and/\1 =>/g;s/()/(true)/g" \
	    > results/`basename $$i .smt2`.smt-ai.raw; \
	  rm -f results/`basename $$i .smt2`.smt-ai.result; \
	  echo "Raw generated" >&2; \
	  cat results/`basename $$i .smt2`.smt-ai.raw; \
	  while read line; do \
	    echo "$${line}" | sed "s/ => / =>\n/g;s/ and /\n/g" | grep "v_$${nodename}_0"| sed "$${sed_rule};s/v_$${nodename}_0_//g"  |grep -v "F2L" > /tmp/log;\
	    echo "Property `cat /tmp/log`" >&2;\
	    while read line2; do\
	      echo Cleaning line "$${line2}" >&2; \
	      tmp1=`echo "$${line2}" | sed "s/[^(]//g" | wc -m`; \
	      tmp2=`echo "$${line2}" | sed "s/[^)]//g" | wc -m`; \
	      diff_val=$$(( $$tmp1 - $$tmp2 )); \
	      echo Difference $${diff_val} >&2;\
	      if [ $$diff_val -ge 0 ]; \
	         then \
	           newline=`echo "$${line2}" | sed "s/^.\{$$diff_val\}//"`; \
	         else \
	           newline=`echo "$${line2}" | sed "s/.\{$$(( - $$diff_val ))\}$$//"`; \
	      fi; \
	      echo "$${newline}"; \
	    done < /tmp/log | sed "s/$$/ and /g;s/=> and/=>/g" | xargs | sed "s/and$$//g" | sed "s/^.*=>$$//g" | sed "/^$$/d" >> results/`basename $$i .smt2`.smt-ai.result; \
	    rm /tmp/log; \
	  done < results/`basename $$i .smt2`.smt-ai.raw; \
	  cat $${fst} | grep states | sed "s/states //;s/;//;s/,/ or /g" >> results/`basename $$i .smt2`.smt-ai.result; \
	done

tools: fastConv-tool arith-tool

fastConv-tool:
	@make -C tools fastConv-tool

arith-tool:
	@make -C tools arith-tool

comparison: results-aspic results-reps
	@rm -rf generated_comp
	@echo Generating comparison files >&2
	@./tools/generate_comparison_multi > /dev/null

synthesis: comparison
	@echo Building resulting file >&2
	@./tools/table_latex

final_table:
	@./tools/table_latex_paper > table_comparison.tex

distclean:
	make -C tools clean
	rm -rf fst/*.log
	rm -rf lustre
	rm -rf generated_comp
	rm -rf results runtime
	rm -rf tools/arith tools/fastConv
