Makefile

# ==============================================================================
# File      : Makefile
# Author    : Max von Hippel
# Authored  : 13 March 2020
# Purpose   : provides various useful targets for running Korg
# How to run: see https://www.gnu.org/software/make/manual/make.html if you are
#             unfamiliar with Makefiles.
# ==============================================================================

# Deletes all the left-over files produced by running the other targets in this file.
clean:
	- rm -rf __pycache__
	- rm -rf tests/__pycache__
	- rm -rf out/*
	- rm *.trail
	- rm *.pml
	- rm ./*.pml
	- rm *pan*
	- rm *.tcl
	- rm .*.swp
	- rm *.pyc
	- rm test_exp*
	- rm ._n_i_p_s_
	- rm **.tmp
	- rm *.txt
	echo "All clean!"

# -------------------------------------------------------------------------------
# DCCP and TCP targets are canonical versions from Case Studies in RFC NLP paper.
# Choice of max_attacks=100 is because that's what we did in RFC NLP.
# -------------------------------------------------------------------------------

dccp-broken:
	for j in 1 2 3 4; do                                \
		python3 korg/Korg.py                            \
			--model=demo/DCCP/DCCP.no-client-server.pml \
			--phi=demo/DCCP/phi$$j.pml                  \
			--Q=demo/DCCP/network.pml                   \
			--IO=demo/DCCP/IO.txt                       \
			--max_attacks=100                           \
			--with_recovery=True                        \
			--name=DCCP.$$j                             \
			--characterize=False;                       \
	done;

dccp:
	for j in 1 2 3 4; do               \
		python3 korg/Korg.py           \
			--model=demo/DCCP/DCCP.pml \
			--phi=demo/DCCP/phi$$j.pml \
			--Q=demo/DCCP/network.pml  \
			--IO=demo/DCCP/IO.txt      \
			--max_attacks=100          \
			--with_recovery=True       \
			--name=DCCP.$$j            \
			--characterize=False;      \
	done;

tcp:
	for j in 1 2 3 4; do               \
		python3 korg/Korg.py           \
			--model=demo/TCP/TCP.pml   \
			--phi=demo/TCP/phi$$j.pml  \
			--Q=demo/TCP/network.pml   \
			--IO=demo/TCP/IO.txt       \
			--max_attacks=100          \
			--with_recovery=True       \
			--name=TCP.$$j             \
			--characterize=False;      \
	done;

# -------------------------------------------------------------------------------
# The remaining targets are from the original KORG paper.
# -------------------------------------------------------------------------------

# Tests on TCP w/ experiment1 (phi_1)
experiment1:
	time python3 korg/Korg.py                 \
			--model=demo/TCP/TCP.pml          \
			--phi=demo/TCP/phi1.pml 		  \
			--Q=demo/TCP/network.pml          \
			--IO=demo/TCP/IO.txt              \
			--max_attacks=100                 \
			--with_recovery=True              \
			--name=experiment1                \
			--characterize=False

experiment2:
	time python3 korg/Korg.py                 \
			--model=demo/TCP/TCP.pml          \
			--phi=demo/TCP/phi2.pml 		  \
			--Q=demo/TCP/network.pml          \
			--IO=demo/TCP/IO.txt              \
			--max_attacks=100                 \
			--with_recovery=True              \
			--name=experiment2                \
			--characterize=False

experiment3:
	time python3 korg/Korg.py                 \
			--model=demo/TCP/TCP.pml          \
			--phi=demo/TCP/phi3.pml 		  \
			--Q=demo/TCP/network.pml          \
			--IO=demo/TCP/IO.txt              \
			--max_attacks=100                 \
			--with_recovery=True              \
			--name=experiment3                \
			--characterize=False

experiment4:
	time python3 korg/Korg.py                 \
			--model=demo/TCP/TCP.pml          \
			--phi=demo/TCP/phi4.pml 		  \
			--Q=demo/TCP/network.pml          \
			--IO=demo/TCP/IO.txt              \
			--max_attacks=100                 \
			--with_recovery=True              \
			--name=experiment4                \
			--characterize=False

# Runs the semaphore demo
semaphoreDemo:
	python3 korg/Korg.py \
		--model=demo/smallDemo4/Alice.pml \
		--phi=demo/smallDemo4/Phi.pml     \
		--Q=demo/smallDemo4/Bob.pml       \
		--IO=demo/smallDemo4/IO.txt       \
		--max_attacks=1                   \
		--with_recovery=False             \
		--name=semaphoreDemo              \
		--characterize=True

# Comparable to Case Study in KORG paper, but notice that due to changed network 
# model (delay in only one direction) to support DCCP, no attacks are found 
# with phi3, and the number of attacks found is a little different.
avgExperiment:
	mkdir -p logs;                                                                   \
	for exp in 3 2 1; do                                                             \
		for b in False True; do                                                      \
			for n in 1 2 3 4 5 6 7 8 9 10; do                                        \
				echo "looking at ... demo/TCP/phi"$$exp".pml";                       \
				rm *.pml;                                                            \
				name="experiment"$$exp"_"$$n"_"$$b;                                  \
				echo "\n\n~~~~~~~~~~~~~ EXPERIMENT :: "$$name" ~~~~~~~~~~~~~~~\n\n"; \
				touch "logs/"$$name"_log.txt";                                       \
				/usr/bin/time -o "logs/"$$name"_log.txt" python3 korg/Korg.py        \
					--model=demo/TCP/TCP.pml                                         \
					--phi="demo/TCP/phi"$$exp".pml"                                  \
					--Q=demo/TCP/network.pml                                         \
					--IO=demo/TCP/IO.txt                                             \
					--max_attacks=10                                                 \
					--with_recovery=$$b                                              \
					--name=$$name                                                    \
					--characterize=False;                                            \
			done;                                                                    \
		done;                                                                        \
	done;

# Attempts to reproduce the original result from KORG, using the exact files from the
# unmodified repository, and with the same configuration of Spin (namely, partial order
# reduction is turned on -- to do this, need to re-compile with alternativeCharacterize
# instead of Characterize - please refer to the Dockerfile to see how this is done.
# The supported way to reproduce our results is with the Dockerfile!
experimentKorg:
	mkdir -p logs;                                                               \
	for exp in 3 2 1; do                                                         \
		for b in False True; do                                                  \
			echo "looking at ... demo/TCP.korg/phi"$$exp".pml";                  \
			rm *.pml;                                                            \
			name="experiment"$$exp"_"$$b;                                        \
			echo "\n\n~~~~~~~~~~~~~ EXPERIMENT :: "$$name" ~~~~~~~~~~~~~~~\n\n"; \
			touch "logs/"$$name"_log.txt";                                       \
			/usr/bin/time -o "logs/"$$name"_log.txt" python3 korg/Korg.py        \
				--model=demo/TCP.korg/TCP.pml                                    \
				--phi="demo/TCP.korg/phi"$$exp".pml"                             \
				--Q=demo/TCP.korg/network.pml                                    \
				--IO=demo/TCP.korg/IO.txt                                        \
				--max_attacks=10                                                 \
				--with_recovery=$$b                                              \
				--name=$$name                                                    \
				--characterize=False;                                            \
		done;                                                                    \
	done;

# Runs the primary test class for korg/Korg.py
testKorg: ; green tests/test_Korg.py

# Runs tests for Characterize.py
testChar: ; green tests/test_Characterize.py

# Runs tests for Construct.py
testCons: ; green tests/test_Construct.py

# Runs all tests
test: 
	rm -rf tests/__pycache__
	rm -rf __pycache__
	make clean testChar clean testKorg clean testCons

# create new example directory
# `make newExample dir=new_dir_name`
newExample: 
	- mkdir ${dir} 
	- cd ${dir}
	- touch P.pml Q.pml IO.txt Phi.pml

# Runs the piratical example from the tutorial.
# https://dev.to/maxvonhippel/automated-attacker-synthesis-for-distributed-protocols-45mn
pirates:
	python3 korg/Korg.py                \
		--model=demo/pirates/alice.pml  \
		--phi=demo/pirates/phi.pml 		\
		--Q=demo/pirates/bob.pml        \
		--IO=demo/pirates/IO.txt        \
		--max_attacks=1                 \
		--with_recovery=True            \
		--name=pirates                	\
		--characterize=True