CIVL=civl
VERIFY=$(CIVL) verify
COMPARE=$(CIVL) compare

all: compare1 compare2 compare1_7 compare2_7  memleak_cp memleak_rt memleak_cp_7 memleak_rt_7

## naive vs. real time
compare1: treebuffer-driver.cvl treebuffer-naive.c treebuffer-realtime.c treebuffer.h
	$(COMPARE) -inputN=6 -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-realtime.c

## naive vs. caterpillar
compare2: treebuffer-driver.cvl treebuffer-naive.c treebuffer-caterpillar.c treebuffer.h
	$(COMPARE) -inputN=6 -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-caterpillar.c

compare1_7: treebuffer-driver.cvl treebuffer-naive.c treebuffer-realtime.c treebuffer.h
	$(COMPARE) -inputn=7 -inputN=7 -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-realtime.c

compare2_7: treebuffer-driver.cvl treebuffer-naive.c treebuffer-caterpillar.c treebuffer.h
	$(COMPARE) -inputn=7 -inputN=7 -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-caterpillar.c

## caterpillar and real time (with memory leak check)
memleak_cp: treebuffer-driver.cvl treebuffer-caterpillar.c treebuffer.h
	$(VERIFY) -inputN=6 treebuffer-driver.cvl treebuffer-caterpillar.c

memleak_rt: treebuffer-driver.cvl treebuffer-realtime.c treebuffer.h
	$(VERIFY) -inputN=6 treebuffer-driver.cvl treebuffer-realtime.c

memleak_cp_7: treebuffer-driver.cvl treebuffer-caterpillar.c treebuffer.h
	$(VERIFY) -inputn=7 -inputN=7 treebuffer-driver.cvl treebuffer-caterpillar.c

memleak_rt_7: treebuffer-driver.cvl treebuffer-realtime.c treebuffer.h
	$(VERIFY) -inputn=7 -inputN=7 treebuffer-driver.cvl treebuffer-realtime.c 

## check if the memory usage of the real-time implementation is bounded
bound: treebuffer-driver-bound.cvl treebuffer-realtime-bound.cvl
	$(VERIFY) -enablePrintf=false treebuffer-driver-bound.cvl treebuffer-realtime-bound.cvl

clean:
	rm -rf CIVLREP .sarl *~
