## All measurements assume a 64-bit linux system

all:	safety liveness results

safety:
	spin -a tpc.pml
	gcc -DSAFETY -DNOREDUCE -DMEMLIM=4000 -o pan pan.c
	./pan -n -w25 -c0 -m300000 | tee Data/L1_d_S
	gcc -DSAFETY -DNOREDUCE -DMEMLIM=4000 -DNCORE=2 -o pan pan.c
	./pan -n -c0 -w25 -m600000 -z15 | tee Data/L2_d_S
	gcc -DSAFETY -DNOREDUCE -DMEMLIM=5000 -DNCORE=2 -DVMAX=92 -DPMAX=4 -DQMAX=6 -o pan pan.c
	./pan -n -c0 -w25 -m600000 -z15 | tee Data/L2_t_S

liveness:
	spin -a tpc.pml
	gcc -DNP -DNOREDUCE -DMEMLIM=9000 -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 | tee Data/L1_d_L
	gcc -DNP -DNOREDUCE -DMEMLIM=9000 -DNCORE=2 -DSEP_STATE -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 -z20 | tee Data/L2_d_L
	gcc -DNP -DNOREDUCE -DMEMLIM=20000 -DNCORE=2 -DSEP_STATE -DVMAX=100 -DPMAX=5 -DQMAX=6 -DUSE_DISK -DSET_WQ_SIZE=1024 -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 -z20 | tee Data/L2_t_L

safety_o2:
	spin -a tpc.pml
	gcc -O2 -DSAFETY -DNOREDUCE -DMEMLIM=4000 -o pan pan.c
	./pan -n -w25 -c0 -m300000 | tee Data/L1_d_S_O2
	gcc -O2 -DSAFETY -DNOREDUCE -DMEMLIM=4000 -DNCORE=2 -o pan pan.c
	./pan -n -c0 -w25 -m600000 -z15 | tee Data/L2_d_S_O2
	gcc -O2 -DSAFETY -DNOREDUCE -DMEMLIM=5000 -DNCORE=2 -DVMAX=92 -DPMAX=4 -DQMAX=6 -o pan pan.c
	./pan -n -c0 -w25 -m600000 -z15 | tee Data/L2_t_S_O2

liveness_o2:
	spin -a tpc.pml
	gcc -O2 -DNP -DNOREDUCE -DMEMLIM=9000 -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 | tee Data/L1_d_L_O2
	gcc -O2 -DNP -DNOREDUCE -DMEMLIM=9000 -DNCORE=2 -DSEP_STATE -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 -z20 | tee Data/L2_d_L_O2
	gcc -O2 -DNP -DNOREDUCE -DMEMLIM=20000 -DNCORE=2 -DSEP_STATE -DVMAX=100 -DPMAX=5 -DQMAX=6 -DUSE_DISK -DSET_WQ_SIZE=1024 -o pan pan.c
	./pan -l -w27 -n -c0 -m600000 -z20 | tee Data/L2_t_L_O2

results:
	@echo PhoneSwitch Model
	@echo ================================
	@echo -n S_N1_Deflt: "	"
	@keys < Data/L1_d_S
	@echo -n L_N1_Deflt: "	"
	@keys < Data/L1_d_L
	@echo
	@echo -n S_N2_Deflt: "	"
	@keys < Data/L2_d_S
	@echo -n L_N2_Deflt: "	"
	@keys < Data/L2_d_L
	@echo
	@echo -n S_N2_Tuned: "	"
	@keys < Data/L2_t_S
	@echo -n L_N2_Tuned: "	"
	@keys < Data/L2_t_L
	@echo
	@echo "Optimized:"
	@echo ================================
	@echo -n S_N1_Deflt: "	"
	@keys < Data/L1_d_S_O2
	@echo -n L_N1_Deflt: "	"
	@keys < Data/L1_d_L_O2
	@echo
	@echo -n S_N2_Deflt: "	"
	@keys < Data/L2_d_S_O2
	@echo -n L_N2_Deflt: "	"
	@keys < Data/L2_d_L_O2
	@echo
	@echo -n S_N2_Tuned: "	"
	@keys < Data/L2_t_S_O2
	@echo -n L_N2_Tuned: "	"
	@keys < Data/L2_t_L_O2

clean:
	rm -f pan.? pan pan.o