Ejecuta cualquier Skill en Manus
con un clic

Ejecuta cualquier Skill en Manus con un clic

tlaplus-performance

Estrellas0

Forks0

Actualizado15 de junio de 2026 a las 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.

Instalación

Instalar con Codex o Claude Copia este prompt, pégalo en Codex, Claude u otro asistente, y deja que revise la página de la skill y la instale por ti.

Ejecutar en Manus

Fuente

jackfoxy

jackfoxy/foxy-skills

Abrir repositorio de GitHub Ver repositorios del creador

Descarga

Ejecutar en Manus

Ocupaciones relacionadasSOC

Basado en la clasificación ocupacional SOC

Desarrolladores de softwareOcupaciones informáticas y matemáticas·SOC 15-1252

Explorador de archivos

4 archivos

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/

Más de este repositorio

mismo repositorio

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/