diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -16,15 +16,19 @@ verify: # (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md. verify-model: java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ - -metadir /tmp/tlc-algorithms \ + -metadir /tmp/tlc-sleepsort \ -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-parallelsort \ + -config formal/tla/ParallelSort.cfg formal/tla/ParallelSort.tla # verify-formal: machine-checked deductive proof of a monomorphized insertion # sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image. # See formal/README.md. verify-formal: podman run --rm -v $(PWD)/formal:/gobra/formal:z \ - ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: |