Makefile

.PHONY: help test run verify clean check-quint

# Usage: make test SPEC=bft (or omit SPEC to run all)
SPEC ?=
QUINT := $(shell command -v quint 2>/dev/null)

# Suppress Java warnings from Apalache
export JAVA_TOOL_OPTIONS := --enable-native-access=ALL-UNNAMED --sun-misc-unsafe-memory-access=allow -Dcom.google.protobuf.use_unsafe_pre22_gencode=true -XX:+EnableDynamicAgentLoading

# Find .qnt file in a spec directory
qnt_file = $(wildcard $(1)/*.qnt)

# List spec directories (those containing .qnt files)
SPECS := $(shell for dir in */; do [ -n "$$(ls $$dir*.qnt 2>/dev/null)" ] && echo $${dir%/}; done)

help: ## Show this help
	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = ":.*?## "}; {printf "  %-12s %s\n", $$1, $$2}'
	@echo ""
	@echo "Usage: make <target> SPEC=<spec-name>"
	@echo "  Omit SPEC to run on all specs"
	@echo ""
	@echo "Available specs:"
	@for spec in $(SPECS); do echo "  $$spec"; done

check-quint:
ifndef QUINT
	@echo "quint not found, installing..."
	npm install -g @informalsystems/quint
endif

test: check-quint ## Run tests (SPEC=name or all)
ifdef SPEC
	quint test $(call qnt_file,$(SPEC))
else
	@for spec in $(SPECS); do \
		echo "=== Testing $$spec ===" && quint test $$(ls $$spec/*.qnt); \
	done
endif

run: check-quint ## Random simulation (SPEC=name required)
ifndef SPEC
	@echo "Usage: make run SPEC=<spec-name>"
	@exit 1
endif
	quint run $(call qnt_file,$(SPEC)) --max-steps=20

verify: check-quint ## Verify safety (SPEC=name or all)
ifdef SPEC
	quint verify $(call qnt_file,$(SPEC)) --invariant=safety
else
	@for spec in $(SPECS); do \
		echo "=== Verifying $$spec ===" && quint verify $$(ls $$spec/*.qnt) --invariant=safety; \
	done
endif

clean: ## Clean generated files
	rm -rf target