Run any Skill in Manus with one click

tlaplus-performance

Stars0

Forks0

UpdatedJune 15, 2026 at 22:10

Work with large-scale / real-world TLA+ models and TLC performance measurement - the general/performance case studies (Paxos, Bookkeeper, SwarmKit, ...), the measure.tla/measure.sh harness, the perf.yml regression job, the JMH benchmark target, and state-explosion tuning. Use when scaling TLC, studying perf case studies, or running performance measurements. For routine checking see tlaplus-model-checking.

Installation

Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.

Run Skill in Manus

Source

jackfoxy

jackfoxy/foxy-skills

View GitHub Repository View Creator Repositories

Download

Run Skill in Manus

Related occupationsSOC

Based on SOC occupation classification

Software DevelopersComputer and Mathematical Occupations·SOC 15-1252

File Explorer

4 files

SKILL.md

readonly

name	tlaplus-performance
description	Work with large-scale / real-world TLA+ models and TLC performance measurement - the general/performance case studies (Paxos, Bookkeeper, SwarmKit, ...), the measure.tla/measure.sh harness, the perf.yml regression job, the JMH benchmark target, and state-explosion tuning. Use when scaling TLC, studying perf case studies, or running performance measurements. For routine checking see tlaplus-model-checking.
user-invocable	true
disable-model-invocation	false

TLC Performance & Scaling

Covers general/performance/ and perf tooling. Routine checking + flags: [[tlaplus-model-checking]]; OOM/explosion diagnosis: [[tlaplus-debugging]].

Run a measurement (validated harness)

cd general/performance
# orchestrated run -> out_run-stats.csv (what perf CI runs):
java -jar ../../tlatools/org.lamport.tlatools/dist/tla2tools.jar -config measure.tla measure.tla
# parameterized model with explicit tuning knobs (default spec Grid5k):
./measure.sh 04 01 10 04   # K L N C [WORKERS] [HEAP] [DIRECT]; defaults nproc/8G/8g

The case-study corpus (Paxos, Bookkeeper, SwarmKit, Ghostferry, …), the harness files, the perf CI job, the JMH target, and the full tuning table are in references/case-studies-and-tuning.md.

JMH micro-benchmarks

ant -f customBuild.xml benchmark        # -> target/benchmarks.jar
java -jar target/benchmarks.jar

For hot-path Java (value enumeration, fingerprinting), not whole-spec timing.

Tuning at a glance

-workers (throughput), -Xmx/-fpmem + OffHeap FPSet (capacity), -fpbits (collisions vs memory), CONSTRAINT/smaller constants (shrink space), SYMMETRY (safety only — unsound with liveness), -simulate/-dfid (sampling/deep). Methodology: snapshot a real spec → choose constants/constraints → measure → tune → compare CSV vs baseline. Details: the reference file.

Validation

Reproduce one case study's measurement run, capture out_run-stats.csv, and explain how a chosen knob (workers/symmetry/constraint) changed the state count or runtime.

References (local)

references/case-studies-and-tuning.md — corpus, harness, perf CI, JMH, tuning table
general/performance/ — case-study dirs (README.md, LINK.md), measure.{tla,sh}, Grid5k.tla, stats.{R,tla}
.github/workflows/perf.yml, tlatools/org.lamport.tlatools/customBuild.xml (benchmark), test-benchmark/

More from this repository

same repository

gviz-dot-syntax

jackfoxy/foxy-skills

Complete reference for the Graphviz DOT language — grammar, statements, identifiers, graph/node/edge/subgraph attributes, colors, ports, engines, and lexical edge cases — as accepted by the pure-Hoon %graph-viz renderer.

2026-07-100

gviz-gall-api

jackfoxy/foxy-skills

API reference for the %graph-viz Gall agent — the stateless subscribe-then-poke protocol, %gviz-command/%gviz-result marks, $command/$render-opts/$result/$err/$diag types, the run:lib gate, and the positioned-graph noun.

2026-07-100

gviz-patterns

jackfoxy/foxy-skills

Practical recipes and best practices for %graph-viz — rendering from Hoon, building graphs programmatically, worked diagram templates (org charts, dependency/architecture/state/data-flow/UML), styling and accessibility guidance, performance limits, pitfalls, integration (clay/caching), and debugging with verbose diagnostics.

2026-07-100

tlaplus-overview

jackfoxy/foxy-skills

High-level orientation to the tlaplus/tlaplus repository (TLA+ CLI tools + Eclipse Toolbox IDE), its tool entrypoints, and which sibling skill to use for a given task. Use when first interacting with the TLA+ toolchain repo, deciding between CLI/editor/build paths, or routing to the right tlaplus-* skill. Points to the shared external-link inventory and source-map for the whole pack.

2026-06-170

tlaplus-build-workflow

jackfoxy/foxy-skills

Build, package, test, and develop the TLA+ tools and Toolbox locally or in CI - Ant targets for tla2tools.jar, Maven/Tycho for the Toolbox, the test-set/test targets, the devcontainer, and the GitHub CI matrix. Use to compile the jar, run the test suite or a single test, set up a dev environment, or understand the CI pipeline. Owns every ant/mvn command line for the pack.

2026-06-150

tlaplus-contribution

jackfoxy/foxy-skills

Follow the tlaplus/tlaplus contribution conventions - engage maintainers early, make surgical diffs, write tests first, split PRs, use commit categorization tags and DCO sign-off. Use before any edit or PR, when authoring tests/docs, or crafting commit messages for this repo. For the mechanics of building/running tests see tlaplus-build-workflow.

2026-06-150

name	tlaplus-performance
description	Work with large-scale / real-world TLA+ models and TLC performance measurement - the general/performance case studies (Paxos, Bookkeeper, SwarmKit, ...), the measure.tla/measure.sh harness, the perf.yml regression job, the JMH benchmark target, and state-explosion tuning. Use when scaling TLC, studying perf case studies, or running performance measurements. For routine checking see tlaplus-model-checking.
user-invocable	true
disable-model-invocation	false

TLC Performance & Scaling

Covers general/performance/ and perf tooling. Routine checking + flags: [[tlaplus-model-checking]]; OOM/explosion diagnosis: [[tlaplus-debugging]].

Run a measurement (validated harness)

cd general/performance
# orchestrated run -> out_run-stats.csv (what perf CI runs):
java -jar ../../tlatools/org.lamport.tlatools/dist/tla2tools.jar -config measure.tla measure.tla
# parameterized model with explicit tuning knobs (default spec Grid5k):
./measure.sh 04 01 10 04   # K L N C [WORKERS] [HEAP] [DIRECT]; defaults nproc/8G/8g

The case-study corpus (Paxos, Bookkeeper, SwarmKit, Ghostferry, …), the harness files, the perf CI job, the JMH target, and the full tuning table are in references/case-studies-and-tuning.md.

JMH micro-benchmarks

ant -f customBuild.xml benchmark        # -> target/benchmarks.jar
java -jar target/benchmarks.jar

For hot-path Java (value enumeration, fingerprinting), not whole-spec timing.

Tuning at a glance

Validation

Reproduce one case study's measurement run, capture out_run-stats.csv, and explain how a chosen knob (workers/symmetry/constraint) changed the state count or runtime.

References (local)

references/case-studies-and-tuning.md — corpus, harness, perf CI, JMH, tuning table
general/performance/ — case-study dirs (README.md, LINK.md), measure.{tla,sh}, Grid5k.tla, stats.{R,tla}
.github/workflows/perf.yml, tlatools/org.lamport.tlatools/customBuild.xml (benchmark), test-benchmark/