#ltl formulae definition
DEF_FILE = def.ltl

#property name
PROPERTY = reply_consistency

#ltl formula 
FORMULA_FILE = $(PROPERTY).ltl

#result directory
RESULT_DIR = $(PROPERTY)_result

#never claim file 
NEVER_FILE = $(PROPERTY).never

#spin verification log
EXEC_LOG = $(PROPERTY).log

#time log
TIME_LOG = $(PROPERTY).time

#verifier name
VERIFIER = $(PROPERTY).verif

#model file
PROMELA_FILE = kernel-model-echo.spin

#verifier compilation options
CC_OPT = -DCOLLAPSE -D_POSIX_SOURCE -DMEMLIM=16000 -DMA=1000 -DVECTORSZ=2048 -DSC -DSAFETY

#verifier generation definition
SPIN_DEF = -DSPIN_PROC_N=11

#verifier option
VERIF_OPT = -v -X -m100000 -w23 -c1 # -f

#verifier generation option
SPIN_OPT = -a

#lunch verifier in BG
BG = 0



all: mk_res_dir build_formula extract build exec

mk_res_dir:
	@echo "Building result directory ..."
	@mkdir -p $(RESULT_DIR)

build_formula: mk_res_dir
#***************************
# Copy the definition
#***************************
	@echo "Building never claim formula ..."	
	@cd $(RESULT_DIR); \
	cat ../$(DEF_FILE) > $(NEVER_FILE)

#***************************
# FORMULA_FILE contains the never claims formula
#***************************
	@cd $(RESULT_DIR); \
	spin -F ../$(FORMULA_FILE) >> $(NEVER_FILE)


extract: build_formula

#***************************
# Extraction of the model checker
#***************************
	@echo "Extracting verifier ..."	
	@cd $(RESULT_DIR); \
	spin $(SPIN_OPT) $(SPIN_DEF) -N $(NEVER_FILE) ../$(PROMELA_FILE)


build: extract

#***************************
# compitation of the model checker
#***************************
	@echo "Building verifier ..."
	@cd $(RESULT_DIR); \
	gcc -w -o $(VERIFIER) $(CC_OPT)  pan.c

exec: build

#***************************
# execution of the model checker
#***************************
	@echo "Running verification ..."

ifeq ($(BG),1)
	@cd $(RESULT_DIR); \
	/usr/bin/time -o $(TIME_LOG) -p ./$(VERIFIER) $(VERIF_OPT) > $(EXEC_LOG) &
else	
	@cd $(RESULT_DIR); \
	/usr/bin/time -o $(TIME_LOG) -p ./$(VERIFIER) $(VERIF_OPT) > $(EXEC_LOG)
endif

trail:
	@spin $(SPIN_DEF) -v -c -t $(PROMELA_FILE) | less

clean: 
	@rm -Rf $(RESULT_DIR)

stop: 
	@killall $(VERIFIER)