Makefile

GO2PINS=../go2pins

NBTHREADS?=1
OUTPUT=benchs-${NBTHREADS}.csv
OUTPUT_BB=benchs-bb-${NBTHREADS}.csv
OUTPUT_REACH=benchs-reach-${NBTHREADS}.csv
OUTPUT_LTL=benchs-ltl-${NBTHREADS}.csv

LTLFILES=RERS/2016-Problem1-ltl.go RERS/2016-Problem2-ltl.go RERS/2016-Problem4-ltl.go RERS/2016-Problem5-ltl.go RERS/2016-Problem7-ltl.go RERS/2017-Problem1-ltl.go RERS/2017-Problem2-ltl.go RERS/2017-Problem4-ltl.go RERS/2017-Problem5-ltl.go RERS/2017-Problem7-ltl.go RERS/2018-Problem1-ltl.go RERS/2018-Problem2-ltl.go RERS/2018-Problem4-ltl.go RERS/2018-Problem5-ltl.go RERS/2018-Problem7-ltl.go RERS/2019-Problem1-ltl.go RERS/2019-Problem2-ltl.go RERS/2019-Problem4-ltl.go RERS/2019-Problem5-ltl.go RERS/2019-Problem7-ltl.go RERS/2020-Problem1-ltl.go RERS/2020-Problem2-ltl.go RERS/2020-Problem4-ltl.go RERS/2020-Problem5-ltl.go RERS/2020-Problem7-ltl.go
LTLDIR=${LTLFILES:RERS/%.go=%}
LTLOUTPUT=${LTLDIR:%=%/${OUTPUT_LTL}}
LTLGLOBAL=${LTLDIR:%=%/global.csv}
LTLBB=${LTLDIR:%=%/${OUTPUT_BB}}

REACHFILES=RERS/2016-Problem10-reach.go  RERS/2016-Problem11-reach.go RERS/2016-Problem12-reach.go RERS/2016-Problem14-reach.go RERS/2016-Problem15-reach.go RERS/2017-Problem10-reach.go RERS/2017-Problem11-reach.go RERS/2017-Problem12-reach.go RERS/2017-Problem14-reach.go RERS/2017-Problem15-reach.go RERS/2018-Problem10-reach.go RERS/2018-Problem11-reach.go RERS/2019-Problem11-reach.go RERS/2019-Problem12-reach.go RERS/2019-Problem14-reach.go RERS/2019-Problem15-reach.go
REACHDIR=${REACHFILES:RERS/%.go=%}
REACHOUTPUT=${REACHDIR:%=%/${OUTPUT_REACH}}
REACHGLOBAL=${REACHDIR:%=%/global.csv}
REACHBB=${REACHDIR:%=%/${OUTPUT_BB}}

all: ${OUTPUT_LTL} ${OUTPUT_REACH} ${OUTPUT}
	@echo "Benchs is over using ${NBTHREADS} thread(s):"
	@echo -e "\t- Global values: ${OUTPUT}"
	@#echo -e "\t- Blackbox evaluations: ${OUTPUT_BB}"
	@echo -e "\t- Reachability evaluations: ${OUTPUT_REACH}"
	@echo -e "\t- LTL evaluations: ${OUTPUT_LTL}"

${OUTPUT}: ${LTLGLOBAL} ${REACHGLOBAL}
	@echo "file,transpile_time, transpile_memory, states, transitions, time, memory" > $@
	@if [ ! -z $^ ]; then\
		tail -q -n +2 $^ >> $@;\
	fi

${LTLGLOBAL}: ${LTLOUTPUT}
${REACHGLOBAL}: ${REACHGLOBAL}

blackbox: ${OUTPUT_BB}

${OUTPUT_BB}: ${LTLBB} ${REACHBB}
	@echo "model,isempty,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $@
	@if [ ! -z $< ]; then\
		tail -q -n +2 $< >> $@;\
	fi

${LTLBB}: %-ltl/${OUTPUT_BB}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl
	@echo Processing blackbox $<
	@./run-ltl-bb.sh $@ $^ ${NBTHREADS}
	@echo End of Processing blackbox

${OUTPUT_LTL}: ${LTLOUTPUT}
	@echo "model,isempty,spottime,ltsmintime,formulae" > $@
	@if [ ! -z $< ]; then\
		echo here;\
		tail -q -n +2 $< >> $@;\
	fi

${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl/output/go2pins-mc %-ltl
	@echo Processing $<
	@./run-ltl.sh $@ $^ ${NBTHREADS}
	@echo End of processing $<

%-ltl/output/go2pins-mc: %-ltl
	@if [ ! -f $@ ]; then\
		echo Building RERS/$<.go output;\
		./build.sh ${GO2PINS} $<;\
		echo End of building RERS/$<.go, use $@;\
	fi

%-ltl:
	@mkdir $@ $@/log

${REACHBB}: %-reach/${OUTPUT_BB}: RERS/%-reach.go %-reach
	@echo Processing blackbox $< if it exists
	@./run-reach-bb.sh $@ $^ ${NBTHREADS}
	@echo End of Processing blackbox

${OUTPUT_REACH}: ${REACHOUTPUT}
	@echo "model,isempty,spottime,ltsmintime,formulae" > $@
	@if [ ! -z $< ]; then\
		tail -q -n +2 $< >> $@;\
	fi

${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-mc %-reach
	@echo Processing $<.formulae.txt if it exists
	@./run-reach.sh $@ $^ ${NBTHREADS}
	@echo End of processing $<

%-reach/output/go2pins-mc: %-reach
	@if [ ! -f $@ ]; then\
		echo Building RERS/$<.go output;\
		./build.sh ${GO2PINS} $<;\
		echo End of building RERS/$<.go, use $@;\
	fi

%-reach:
	@mkdir $@ $@/log

clean:
	rm -rf ${LTLDIR} ${REACHDIR}

distclean:
	rm -rf ${OUTPUT} ${OUTPUT_LTL} ${OUTPUT_REACH} ${OUTPUT_BB}

.PRECIOUS: ${LTLDIR} ${REACHDIR}
.PHONY: all clean