# by default, the target system is the same as the compiling system TARGET_SYSTEM := $(shell uname -s) # Under MinGW, Cygwin, MSYS2, etc. on Windows, # uname -s has the format "_NT-", # e. g. "MINGW64_NT-10.0-19044" or "CYGWIN_NT-10.0". # To simplify checking for Windows, # we detect this format and replace it with simply "Windows". ifneq ($(findstring NT-,$(TARGET_SYSTEM)),) TARGET_SYSTEM := Windows endif ifeq ($(TARGET_SYSTEM),Linux) ISLINUX=1 PROBTAR=ProB.linux64.tar.gz else ifeq ($(TARGET_SYSTEM),Darwin) # macOS ISDARWIN=1 PROBTAR=ProB.macos.zip else ifeq ($(TARGET_SYSTEM),Windows) ISWINDOWS=1 PROBTAR=ProB.windows64.zip else # Unknown system - use generic Unix-like defaults PROBTAR=ProB.linux64.tar.gz endif endif endif OPTS=-p kodkod_for_components full -p TIME_OUT 15000 -p KODKOD_SAT_SOLVER glucose SOLVER=bench .PHONY: bench bench_path: ### Run benchmarks with (your own version of) probcli on PATH -rm bench_$(SOLVER).csv probcli $(OPTS) -solve_file $(SOLVER) pigeon/pigeon_10_bv.eval -solve_file $(SOLVER) pigeon/pigeon_30_bv.eval -solve_file $(SOLVER) pigeon/pigeon_100_bv.eval -solve_file $(SOLVER) trans_closure/transitive_closure_50_bv.eval -solve_file $(SOLVER) queens/queens_14_curry.eval -solve_file $(SOLVER) queens/queens_24_curry.eval -solve_file $(SOLVER) sat/blocksworld_medium.eval -solve_file $(SOLVER) sat/blocksworld_medium_unsat.eval -solve_file $(SOLVER) sat/uuf-250-016.eval -solve_file $(SOLVER) graphs/DominatingSet_BV_Middle_lt13.eval -solve_file $(SOLVER) graphs/DominatingSet_BV_Middle_lt12.eval -solve_file $(SOLVER) graphs/OSLO_no_card.eval -solve_file $(SOLVER) graphs/OSLO_card_lt_135.eval -solve_file $(SOLVER) graphs/OSLO_dom_edge_lt_181.eval -solve_file $(SOLVER) crowded/CrowdedChessBoard_BV.eval -solve_file $(SOLVER) turing/TuringMachine_Cook_20.eval -bench-csv bench_$(SOLVER).csv cat $(SOLVER).csv PDIR=PROB PROB=$(PDIR)/probcli VERS=1.13.1-beta1 VERSION=releases/$(VERS) .PHONY: install_prob version $(PDIR)/$(PROBTAR): ### Download ProB ($VERSION) @echo "Downloading ProB ($VERSION) from ProB's own website" @echo "If this version is no longer available you can manually download it in version 1.13.1-beta1 for Linux and the ifm2022 VirtualBox machine at https://doi.org/10.5281/zenodo.12166295" curl -L https://www3.hhu.de/stups/downloads/prob/tcltk/$(VERSION)/$(PROBTAR) -o $(PROBTAR) install_prob_linux_zenodo: ### Download ProB 1.13.1-beta1 for Linux from Zenodo curl -L https://zenodo.org/records/12166295/files/ProB.linux64.tar.gz?download=1 -o ProB.linux64.tar.gz mkdir -p $(PDIR) tar -xvzf ProB.linux64.tar.gz -C $(PDIR) @echo "Downloaded ProB for Linux from Zenodo, probcli is now available as $(PROB)" $(PROB): $(PDIR)/$(PROBTAR) ### Unpack downloaded version mkdir -p $(PDIR) tar -xvzf $(PROBTAR) -C $(PDIR) @echo "Downloaded ProB, probcli is now available as $(PROB)" @echo "On macOS you need to run make post_install" install_prob: $(PROB) ### Install ProB from the ProB download site in this directory post_install: ### Remove macos quarantine flag as beta version not notarized xattr -r -d com.apple.quarantine $(PDIR)/* version: ### Obtain information about the installed ProB version $(PROB) -version SOLVER=bench .PHONY: bench bench: ### Run FM'2024 benchmarks with probcli downloaded by make install_prob -rm bench_$(VERS)_$(SOLVER).csv @echo "Generating benchmark file bench_$(VERS)_$(SOLVER).csv" @echo "Using ProB version $(VERS) and solver $(SOLVER) (bench means a variety of solvers will be run)" $(PROB) $(OPTS) -solve_file $(SOLVER) pigeon/pigeon_10_bv.eval -solve_file $(SOLVER) pigeon/pigeon_30_bv.eval -solve_file $(SOLVER) trans_closure/transitive_closure_50_bv.eval -solve_file $(SOLVER) queens/queens_14_curry.eval -solve_file $(SOLVER) queens/queens_24_curry.eval -solve_file $(SOLVER) sat/blocksworld_medium.eval -solve_file $(SOLVER) sat/blocksworld_medium_unsat.eval -solve_file $(SOLVER) sat/uuf-250-016.eval -solve_file $(SOLVER) graphs/DominatingSet_BV_Middle_lt13.eval -solve_file $(SOLVER) graphs/DominatingSet_BV_Middle_lt12.eval -solve_file $(SOLVER) graphs/OSLO_no_card.eval -solve_file $(SOLVER) graphs/OSLO_card_lt_135.eval -solve_file $(SOLVER) graphs/OSLO_dom_edge_lt_181.eval -solve_file $(SOLVER) crowded/CrowdedChessBoard_BV.eval -solve_file $(SOLVER) turing/TuringMachine_Cook_20.eval -bench-csv bench_$(VERS)_$(SOLVER).csv cat bench_$(VERS)_$(SOLVER).csv @echo "The benchmark results are in file bench_$(VERS)_$(SOLVER).csv" SOLVER2=sat .PHONY: sat sat: ### Run FM'2024 benchmarks with just b2sat (Glucose) using probcli downloaded by make install_prob -rm bench_$(VERS)_b2sat.csv @echo "Generating benchmark file bench_$(VERS)_$(SOLVER2).csv" @echo "Using ProB version $(VERS) and solver $(SOLVER2) (bench means a variety of solvers will be run)" $(PROB) $(OPTS) -solve_file $(SOLVER2) pigeon/pigeon_10_bv.eval -solve_file $(SOLVER2) pigeon/pigeon_30_bv.eval -solve_file $(SOLVER2) trans_closure/transitive_closure_50_bv.eval -solve_file $(SOLVER2) queens/queens_14_curry.eval -solve_file $(SOLVER2) queens/queens_24_curry.eval -solve_file $(SOLVER2) sat/blocksworld_medium.eval -solve_file $(SOLVER2) sat/blocksworld_medium_unsat.eval -solve_file $(SOLVER2) sat/uuf-250-016.eval -solve_file $(SOLVER2) graphs/DominatingSet_BV_Middle_lt13.eval -solve_file $(SOLVER2) graphs/DominatingSet_BV_Middle_lt12.eval -solve_file $(SOLVER2) graphs/OSLO_no_card.eval -solve_file $(SOLVER2) graphs/OSLO_card_lt_135.eval -solve_file $(SOLVER2) graphs/OSLO_dom_edge_lt_181.eval -solve_file $(SOLVER2) crowded/CrowdedChessBoard_BV.eval -solve_file $(SOLVER2) turing/TuringMachine_Cook_20.eval -bench-csv bench_$(VERS)_b2sat.csv cat bench_$(VERS)_b2sat.csv @echo "The benchmark results are in file bench_$(VERS)_b2sat.csv" SOLVER3=cdclt .PHONY: cdclt cdclt: ### Run FM'2024 benchmarks with Prolog CDCLT solver using probcli downloaded by make install_prob -rm bench_$(VERS)_b2sat.csv @echo "Generating benchmark file bench_$(VERS)_$(SOLVER3).csv" @echo "Using ProB version $(VERS) and solver $(SOLVER3) (bench means a variety of solvers will be run)" $(PROB) $(OPTS) -solve_file $(SOLVER3) pigeon/pigeon_10_bv.eval -solve_file $(SOLVER3) pigeon/pigeon_30_bv.eval -solve_file $(SOLVER3) trans_closure/transitive_closure_50_bv.eval -solve_file $(SOLVER3) queens/queens_14_curry.eval -solve_file $(SOLVER3) queens/queens_24_curry.eval -solve_file $(SOLVER3) sat/blocksworld_medium.eval -solve_file $(SOLVER3) sat/blocksworld_medium_unsat.eval -solve_file $(SOLVER3) sat/uuf-250-016.eval -solve_file $(SOLVER3) graphs/DominatingSet_BV_Middle_lt13.eval -solve_file $(SOLVER3) graphs/DominatingSet_BV_Middle_lt12.eval -solve_file $(SOLVER3) graphs/OSLO_no_card.eval -solve_file $(SOLVER3) graphs/OSLO_card_lt_135.eval -solve_file $(SOLVER3) graphs/OSLO_dom_edge_lt_181.eval -solve_file $(SOLVER3) crowded/CrowdedChessBoard_BV.eval -solve_file $(SOLVER3) turing/TuringMachine_Cook_20.eval -bench-csv bench_$(VERS)_$(SOLVER3).csv cat bench_$(VERS)_$(SOLVER3).csv @echo "The benchmark results are in file bench_$(VERS)_$(SOLVER3).csv" simple: ### Run b2sat on the simple formula in Section 3 of the FM'2024 paper $(PROB) $(OPTS) -eval ':sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1))' clean: ### Remove generated CSV and .prob files -rm -rf bench_*.csv -rm -rf *.tar.gz *.zip help: ## Display this help @awk 'BEGIN {FS = ":.*##"; printf "\nUsage:\n make \033[36m\033[0m\n"} /^[a-zA-Z_-]+:.*?##/ { printf " \033[36m%-15s\033[0m %s\n", $$1, $$2 } /^##@/ { printf "\n\033[1m%s\033[0m\n", substr($$0, 5) } ' $(MAKEFILE_LIST)