#! /bin/make

CAESAR		= caesar -verbose -warning -gc -more '/bin/cat'
CAESAR_ADT	= caesar.adt -verbose -warning -more '/bin/cat'
OMIN		= aldebaran -omin -std
LOTOS_OPEN	= lotos.open -verbose -warning -gc
BCG_OPEN	= bcg_open

default: help

help:
	# Use this makefile to apply CADP tools to the CO4 specification.
	# Useful targets are:
	#   <scenario> - all results for scenario <scenario>,
	#     which is any of:
	# $(CO4_RESULTS)
	#
	#   <draw> - produce graph picture <draw>, which is any of:
	# $(CO4_DRAWS)
	#
	#   results - results for all scenarios.
	#   draws - all graph pictures.
	#   lotos - generate all LOTOS specs
	#   all - everything.
	#   showresults - display all results on tty.
	#   cleanresults - delete result files.
	#   clean - delete generated files 

################################################################

CO4_LIBS	= CO4_DATATYPES.lib CO4_PROCESSES.lib

co4_%.bcg: co4_%.lotos $(CO4_LIBS)
	$(CAESAR_ADT) $<
	$(CAESAR) $<

co4_%.xsimulator: co4_%.lotos $(CO4_LIBS)
	$(LOTOS_OPEN) $< xsimulator

%_omin.bcg: %.bcg
	$(OMIN) -output $@ $<

################################################################
# Validation work
################################################################

CO4_CASES = \
  co4_1_1 co4_1_2 \
  co4_1a_1 co4_1a_2 co4_1a_3 \
  co4_2_1 co4_2a_1 \
  co4_3_1 \
  co4_4_1 \
  co4_5_1 \
  co4_6_1

CO4_RESULTS = $(CO4_CASES:%=%.result)
CO4_LOTOS = $(CO4_CASES:%=%.lotos)

CO4_DRAWS = co4_1_1_draw.ps co4_1a_1_draw.ps

co4_1_1.result: co4_1_1.bcg co4_1_1_omin.bcg signotin.seq
	rm -f $@
	aldebaran -info co4_1_1.bcg >> $@
	aldebaran -info co4_1_1_omin.bcg >> $@
	for seqno in 1 2 3 4 5 ;\
	do	$(BCG_OPEN) co4_1_1_omin.bcg exhibitor -bfs -seqno $$seqno < signotin.seq >> $@ ;\
	done

co4_1_1_draw.ps: co4_1_1_omin.bcg short.rename
	aldebaran -rename short.rename -sort -output co4_1_1_draw.bcg co4_1_1_omin.bcg
	bcg_draw -ps co4_1_1_draw.bcg

co4_1_2.result: co4_1_2.bcg co4_1_2_omin.bcg inconsistent.seq
	rm -f $@
	aldebaran -info co4_1_2.bcg >> $@
	aldebaran -info co4_1_2_omin.bcg >> $@
	$(BCG_OPEN) co4_1_2_omin.bcg exhibitor -bfs -seqno 1 < inconsistent.seq >> $@

co4_1_3.result: co4_1_3.bcg co4_1_3_omin.bcg
	rm -f $@
	aldebaran -info co4_1_3.bcg >> $@
	aldebaran -info co4_1_3_omin.bcg >> $@

co4_1a_1.result: co4_1a_1.bcg co4_1a_1_omin.bcg dead.seq
	rm -f $@
	aldebaran -info co4_1a_1.bcg >> $@
	aldebaran -info co4_1a_1_omin.bcg >> $@
	$(BCG_OPEN) co4_1a_1.bcg exhibitor -dfs -all -seqno 1 < dead.seq >> $@

co4_1a_2.result: co4_1a_2.bcg co4_1a_2_omin.bcg
	rm -f $@
	aldebaran -info co4_1a_2.bcg >> $@
	aldebaran -info co4_1a_2_omin.bcg >> $@

co4_1a_3.result: co4_1a_3.bcg co4_1a_3_omin.bcg
	rm -f $@
	aldebaran -info co4_1a_3.bcg >> $@
	aldebaran -info co4_1a_3_omin.bcg >> $@

co4_1a_1_draw.ps: co4_1a_1_omin.bcg short.rename
	aldebaran -rename short.rename -sort -output co4_1a_1_draw.bcg co4_1a_1_omin.bcg
	bcg_draw -ps co4_1a_1_draw.bcg

co4_2_1.result: co4_2_1.bcg co4_2_1_omin.bcg signotin.seq
	rm -f $@
	aldebaran -info co4_2_1.bcg >> $@
	aldebaran -info co4_2_1_omin.bcg >> $@
	for seqno in 1 2 3 4 5 ;\
	do	$(BCG_OPEN) co4_2_1_omin.bcg exhibitor -bfs -seqno $$seqno < signotin.seq >> $@ ;\
	done

co4_2a_1.result: co4_2a_1.bcg
	rm -f $@
	aldebaran -info co4_2a_1.bcg >> $@

co4_3_1.result: co4_3_1.bcg co4_3_1_omin.bcg signotin.seq
	rm -f $@
	aldebaran -info co4_3_1.bcg >> $@
	aldebaran -info co4_3_1_omin.bcg >> $@
	for seqno in 1 2 3 4 5 ;\
	do	$(BCG_OPEN) co4_3_1_omin.bcg exhibitor -bfs -seqno $$seqno < signotin.seq >> $@ ;\
	done

co4_4_1.result: co4_4_1.lotos scenario_4_1.seq
	rm -f $@
	# pre-compile exhibitor to obtain significant timings in later calls
	$(LOTOS_OPEN) co4_4_1.lotos exhibitor < /dev/null
	$(LOTOS_OPEN) co4_4_1.lotos exhibitor -dfs -first -seqno 1 < scenario_4_1.seq >> $@
	# the next line was commented out to avoid excessive execution time
	# $(LOTOS_OPEN) co4_4_1.lotos terminator -first 0 2000000

co4_5_1.result: co4_5_1.bcg co4_5_1_omin.bcg signotin.seq unsafe.seq
	rm -f $@
	aldebaran -info co4_5_1.bcg >> $@
	aldebaran -info co4_5_1_omin.bcg >> $@
	for seqno in 1 2 3 4 5 ;\
	do	$(BCG_OPEN) co4_5_1_omin.bcg exhibitor -bfs -seqno $$seqno < signotin.seq >> $@ ;\
	done
	for seqno in 1 2 3 ;\
	do	$(BCG_OPEN) co4_5_1_omin.bcg exhibitor -bfs -seqno $$seqno < unsafe.seq >> $@ ;\
	done

co4_5_2.result: co4_5_2.bcg co4_5_2_omin.bcg signotin.seq unsafe.seq
	rm -f $@
	aldebaran -info co4_5_2.bcg >> $@
	aldebaran -info co4_5_2_omin.bcg >> $@
	for seqno in 1 2 3 4 5 ;\
	do	$(BCG_OPEN) co4_5_2_omin.bcg exhibitor -bfs -seqno $$seqno < signotin.seq >> $@ ;\
	done
	for seqno in 1 2 3 ;\
	do	$(BCG_OPEN) co4_5_2_omin.bcg exhibitor -bfs -seqno $$seqno < unsafe.seq >> $@ ;\
	done

co4_6_1.result: co4_6_1.bcg co4_6_1_omin.bcg dead.seq twogroups.seq
	rm -f $@
	aldebaran -info co4_6_1.bcg >> $@
	aldebaran -info co4_6_1_omin.bcg >> $@
	$(BCG_OPEN) co4_6_1_omin.bcg exhibitor -bfs -seqno 1 < dead.seq >> $@
	$(BCG_OPEN) co4_6_1_omin.bcg exhibitor -bfs -seqno 1 < twogroups.seq >> $@

################################################################
# global housecleaning rules
################################################################

results: $(CO4_RESULTS)

draws: $(CO4_DRAWS)

all: results draws

showresults: results
	more $(CO4_RESULTS)

cleanresults:
	rm -f co4_*.result

clean: cleanresults
	rm -f *.h *.x *err *.bcg *@1.o *.aut