CC=${CBC_COMPILER}
MCC=${CBC_COMPILER}
TARGET=dpp dpp2 tableau tableau2 tableau3
MCCFLAGS=-c -g
CFLAGS=-I. -g -Wall

.SUFFIXES:	.cbc .c .o

.cbc.o:
	$(MCC) $(MCCFLAGS) $<

all: $(TARGET)

# single running
dpp: dpp.o main.o
	$(CC) $(CFLAGS) -o $@ $^

# multiple running
dpp2: dpp2.o queue.o scheduler.o memory.o crc32.o
	$(CC) $(CFLAGS) -o $@ $^

# tableau expansion
tableau: dpp2.o queue.o tableau.o memory.o state_db.o crc32.o
	$(CC) $(CFLAGS) -o $@ $^

# tableau expansion with LTL
tableau2: dpp2.o queue.o ltl.o tableau2.o memory.o state_db.o crc32.o
	$(CC) $(CFLAGS) -o $@ $^

# tableau expansion with LTL (reduced the number of states)
tableau3: dpp3.o queue.o ltl.o tableau3.o memory.o state_db.o crc32.o
	$(CC) $(CFLAGS) -o $@ $^

#

test:   memory_test state_test

memory_test: test/memory_test
	test/memory_test
state_test: test/state_test
	test/state_test

test/memory_test: test/memory_test.o memory.o crc32.o
	$(CC) $(CFLAGS) -I. $^ -o $@
test/state_test: test/state_test.o memory.o  state_db.o crc32.o
	$(CC) $(CFLAGS) -I. $^ -o $@

clean:
	$(RM) -f $(TARGET)
	$(RM) -f *.s *.o
	$(RM) -f test/*.s test/*.o test/state_test test/memory_test


depend:
	makedepend *.cbc *.[hc] test/*.c

# DO NOT DELETE

dpp.o: dpp.h
dpp2.o: dpp2.h queue.h dpp.h state_db.h scheduler.h
main.o: dpp.h
queue.o: queue.h dpp.h state_db.h