working-model

Arbeitsmodell

Du schreibst eine kleine *.model.json-Spezifikation: Parameter (Schieberegler), Zustände, Regeln in einer winzigen sicheren Regelsprache, ein Szenario von Ereignissen, visuelle Teile, die an den Zustand gebunden sind, Beschriftungen und Behauptungen. Die CLI simuliert es in Node, prüft jede Behauptung, lintet den Text und erstellt eine einzelne Offline-HTML-Seite, die dieselbe Engine ausführt und die Behauptungen live erneut prüft, während der Leser die Schieberegler bewegt.

Der Punkt: eine Erklärung, die getestet ist. Eine Behauptung, die das Modell nicht stützen kann, scheitert, bevor der Benutzer sie überhaupt sieht.

Befehle

Alle Befehle werden mit Node 20 oder neuer ausgeführt und benötigen kein npm install. Behalte die Anführungszeichen: Der Pfad kann Leerzeichen enthalten.

node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers         # eine Spezifikation, die bereits besteht
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json  # Schema, Simulation, Behauptungen, Lint
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate   # Fangen die Behauptungen kaputte Regeln?
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" build ./explainers/token-bucket.model.json -o ./explainers/token-bucket.html
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" layout ./explainers/token-bucket.model.json --out ./explainers/shots   # benötigt lokales Chrome oder Edge
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png           # optionales Bild
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7          # gesäte Gegenbeispielsuche
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json   # Modell versus beobachteten Trace

Im Folgenden steht working-model kurz für node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs". In Agenten, die ${CLAUDE_SKILL_DIR} nicht ersetzen, verwende den Ordner, in dem sich diese Datei befindet. Exit-Codes von check: 0 jede Behauptung besteht, 1 eine Behauptung oder ein Lint-Fehler schlägt fehl, 2 die Spezifikation ist ungültig. Füge --json für maschinenlesbare Ausgabe und --set name=value hinzu, um andere Schiebereglerpositionen zu testen. --mutate beendet sich mit 0, es sei denn, die Behauptungen schlagen fehl; füge --mutate-strict (und --min-score 80) hinzu, um sich mit 1 zu beenden, wenn eine Behauptung nie fehlschlägt oder die Punktzahl niedrig ist. build --mutate speichert die Punktzahl in der Seite.

Arbeitsablauf

1. Wähle das kleinste Modell, das den überraschenden Teil zeigt. Ein Mechanismus, ein Szenario, 2 bis 4 Schieberegler. Frage: Was würde ein kluger Leser falsch verstehen? Baue das Szenario so, dass dieser Moment auf dem Bildschirm passiert (die Welle, die den Eimer leert, die Wiederholungen, die zusammenfallen, der Scan, der den Cache leert).
2. Gerüst erstellen oder ein Beispiel kopieren. Beginne mit working-model new <name> oder der nächstgelegenen Datei in examples/ (Token Bucket, Backoff mit Jitter, LRU-Cache, TCP AIMD, Circuit Breaker, SIR-Epidemie, Zinseszins, Lastausgleich, Bloom-Filter, Raft-Leaderwahl, Lagerbestellpunkt).
3. Schreibe Parameter, Zustand und Regeln. Diskrete Zeit: Jeder Tick führt rules.tick aus, dann feuern die Ereignisse dieses Ticks ihren rules.on.<event>-Handler. Halte Einheiten ehrlich (timeUnit, Schieberegler unit). Verwende emit('name', payload) für Dinge, die ein Link animieren oder eine Behauptung beobachten soll.
   • Zeit ist eine Gleitkommazahl. t ist tick × dt, daher ist eine als t + lead gespeicherte Zeit nie exakt gleich einem späteren t. Verwende für Fristen und Countdowns Tick-Nummern (due = tick + round(lead / dt), dann tick >= due). references/spec.md enthält weitere solche Fallstricke unter „Writing Rules That Behave".
   • Listen sind Werte: a = b kopiert. Ändere eine verschachtelte Liste über einen Index (push(queues[i], job)).
4. Schreibe 3 bis 8 Behauptungen, die die wichtigsten Erkenntnisse erfassen, keine Belanglosigkeiten. Eine Behauptung, die eine Regel zurückliest („Tokens überschreiten nie die Kapazität", wenn die Regel min(capacity, ...) ist), kann nicht fehlschlagen und lehrt nichts; die interessanten sagen etwas, das ein Leser nicht erraten würde: „Eine Schleife, die einen Schlüssel größer als der Cache ist, erhält überhaupt keine Treffer", „Jitter senkt die Spitzenlast bei Wiederholungen". Verwende die richtige Art (at, always, never, eventually, whenever, sweep, compare; siehe references/claims.md).
   • Mindestens eine Behauptung muss bei den Standardwerten gelten und fehlschlagen, wenn ein Schieberegler bewegt wird, damit der Leser sieht, wo die Erklärung nicht mehr gilt. check listet auf, welche Schiebereglerpositionen welche Behauptungen brechen.
   • Jede Behauptung muss für den realen Mechanismus wahr sein, nicht nur für dein Modell. Füge die Quelle für die Schlüsselfakten in sources ein und gib die Modellannahmen in der summary an. Schreibe „in diesem Lauf", wenn eine Behauptung nur für diesen Startwert gilt.
   • Formuliere den Satz genau so, dass er beschreibt, was der Ausdruck prüft. check beweist den Ausdruck, nicht den Satz; Schritt 7 testet, ob die Behauptungen überhaupt fehlschlagen können.
   • Mache die duration lang genug für die langsamsten Schiebereglereinstellungen, sonst schlagen eventually-Behauptungen nur fehl, weil der Durchlauf endete.
5. Binde Zahlen im Text ein. Beschriftungen und Behauptungstexte nehmen {expression}-Lücken: schreibe {capacity}, niemals eine wörtliche 10, die veraltet, wenn sich ein Schieberegler bewegt. check warnt vor wörtlichen Zahlen (W_LITERAL_NUMBER) und schlägt die Bindung vor. Eine Beschriftung muss die Behauptungen angeben, auf die sie sich stützt (cites); das Zitieren einer fehlschlagenden Behauptung ist ein Fehler.
6. Führe check aus, bis es „N/N claims pass" ohne Fehler ausgibt. Behebe auch Warnungen.
7. Führe dann check --mutate aus: teste die Behauptungen. Es bricht die Regeln absichtlich, eine kleine Änderung pro Mutant (< für <=, pop für shift, eine gelöschte Zeile, ein Ereignis einen Tick zu spät), prüft jede Behauptung gegen jeden Mutanten und meldet, welche Behauptungen welche Fehler abfangen.
   • Jede Behauptung muss mindestens einen Mutanten abtöten. Eine Behauptung, die unter „Claims that never failed" aufgeführt ist, kann nicht fehlschlagen: Sie wiederholt eine Regel, gilt leer (vakuum) oder das Szenario übt sie nie aus. Verschärfe sie (mache den Ausdruck so, dass er den gesamten Satz abdeckt) oder ändere das Szenario, damit die Behauptung auf die Probe gestellt wird (gestaffelte Ankünfte statt einer Welle, eine Schleife, die nicht passt). references/claims.md enthält ein durchgearbeitetes Beispiel.
   • Für jeden überlebenden Mutanten füge entweder eine Behauptung hinzu oder verschärfe eine, oder erkläre in deiner Antwort, warum die Änderung nicht sichtbar ist (z.B. benennt sie nur Schlüssel um). Nur ein wirklich harmloser kommt in mutate.ignore in der Spezifikation, mit Begründung. Schwäche niemals eine Behauptung oder eine Zusicherung, um die Punktzahl zu erhöhen.
   • Als äquivalent oder nur visuell gekennzeichnete Mutanten ändern nichts, was eine Behauptung sehen kann; sie werden von der Punktzahl ausgeschlossen. Nur visuelle ändern, was die Seite zeichnet, also überprüfe diese Zahlen im Screenshot.
8. Schwäche oder lösche niemals eine Behauptung, nur damit sie besteht. Wenn eine Behauptung fehlschlägt, entscheide, welche falsch ist:
   • das Modell ist falsch (ein Regel-Fehler, ein falscher Standardwert, ein fehlender Mechanismus): korrigiere das Modell;
   • die Behauptung ist falsch (der reale Mechanismus verhält sich nicht so oder nur unter einer Bedingung): korrigiere die Behauptung und sage, was falsch war. Sage dem Benutzer, welches es war und warum, in ein oder zwei Sätzen. Eine Toleranz zu lockern, bis sie besteht, oder eine Behauptung gegen eine einfachere auszutauschen, ist nicht erlaubt.
9. Baue, dann führe layout aus. Behebe jedes E_-Problem (überlappende Teile, überlaufender Text, kollidierender Text, Seite scrollt seitlich bei 390 px). Normalerweise: gib dem Teil mehr Gitterzellen, kürze eine Bezeichnung oder verschiebe ein Teil. Behebe W_LINK_CROSSES (ein Pfeil, der quer über ein anderes Teil gezeichnet wird): verschiebe ein Teil oder füge via-Punkte hinzu. Sieh dir den Screenshot an, den es erstellt, und überprüfe, ob jede angezeigte Zahl die ist, die du meinst: Teilbindungen werden durch keine Behauptung getestet. Füge für einen Zähler oder eine Anzeige, auf die sich ein Leser verlassen wird, eine expect hinzu (eine unabhängige Möglichkeit, dieselbe Zahl zu berechnen, z.B. "expect": "len(queue)"), und check schlägt fehl, wenn die beiden jemals abweichen.
10. Übergabe: der HTML-Pfad, die Zusammenfassungszeile der Behauptungen (6/6 claims pass) und die Mutationspunktzahl, eine Zeile pro Behauptung, und welcher Schieberegler welche Behauptung bricht. Erwähne alle Modellannahmen, die der Leser kennen sollte.

Auf der Suche nach Gegenbeispielen

Nachdem check und check --mutate bestanden haben, führt working-model fuzz spec.model.json --cases 300 --seed 7 dieselben Behauptungen auf gesäten benachbarten Fällen aus: Schiebereglerwerte, der Modell-Startwert und die Ereignisse, die ein fuzz-Block als fuzzbar markiert (verschoben, wiederholt oder ausgelassen). Dann verkleinert working-model minimize spec.model.json --case .working-model/fuzz/first-failure.json den ersten Fehler, während dieselbe Behauptung weiterhin fehlschlägt. Melde den minimierten Fall in einfachen Worten („lasse die Erfolge zwischen den verstreuten Fehlern und dem Auslösen des Schutzschalters weg"). Ein Fehler bei einer nicht standardmäßigen Einstellung ist ein Befund darüber, wo die Erklärung nicht mehr gilt: korrigiere die Behauptung oder das Modell aus sachlichen Gründen, behalte das Gegenbeispiel und schwäche niemals eine Behauptung, um es zum Schweigen zu bringen. „Kein Fehler gefunden" ist kein Beweis. Details: docs/FUZZ.md.

Vergleichen mit einem beobachteten Trace

Verwende dies nur, wenn der Benutzer einen Trace des realen Systems hat (JSONL oder das OTLP-JSON-Teilformat) oder nach der synthetischen Demo in examples/reality-bridge/ fragt. Ein Trace ist nie erforderlich.

1. Sage zuerst, dass ein Trace private Daten enthalten kann (Anfrage-IDs, Benutzer-IDs, IPs, Token) und lokal verarbeitet werden sollte. Der Import behält nur die Attribute, die das Mapping liest: working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json. Übergib --complete nur, wenn der Benutzer bestätigt, dass die Instrumentierung jedes Ereignis der abgebildeten Arten aufzeichnet; andernfalls bleibt die Vollständigkeit unknown.
2. Halte vier Dinge in dem, was du schreibst, auseinander: Modellannahmen, Mechanismus-Fakten aus Quellen, Behauptungen innerhalb des Modells und beobachtete Zusicherungen. Setze Annahmen in die reality.assumptions der Spezifikation.
3. Schreibe das Mapping basierend auf dem, was der Trace wirklich enthält. Erfinde niemals eine Korrelations-ID oder ein Ereignis, das der Trace nicht aufzeichnet; eine Ausgabe ohne Subjekt auf beiden Seiten ist unkorreliert und ihre Zusicherung ist nicht aussagekräftig. Jedes Modellereignis wird entweder wiederholt oder in internalEvents aufgeführt.
4. Führe working-model check spec.model.json --trace trace.normalized.json --mapping trace-map.json aus. Melde die Modellzeile und die beobachtete Zeile getrennt (Model: 4/4 claims pass | Observed: 1 pass, 2 fail, 0 inconclusive), die erste Abweichung mit ihren Ereignis-IDs und jeden nicht aussagekräftigen Grund wie er ist. Exit 1 bedeutet, dass eine Behauptung oder eine beobachtete Zusicherung fehlgeschlagen ist; 2 ein ungültiger Trace oder ein ungültiges Mapping; 3 eine fehlende Datei oder ein Limit.
5. Wenn der Trace nicht übereinstimmt, korrigiere die Annahme aus sachlichen Gründen, normalerweise in einem zweiten Modell, und behalte das Gegenbeispiel. Lockere niemals minPrecision, minRecall oder withinMs nur um zu bestehen.
6. Für eine Seite zum Anschauen führe working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html aus: der normale Erklärer plus eine Modell-gegenüber-beobachtet-Zeitleiste, die erste Abweichung und jede Zusicherung. Es enthält den normalisierten Trace, bleibt also lokal.
7. Nur wenn der Benutzer um Veröffentlichung bittet, führe zuerst working-model bundle spec.model.json --public ... --preview aus, zeige ihm die Schlüsselliste, dann führe es ohne --preview aus. Ein echter Trace benötigt sein explizites --acknowledge-privacy; gib es niemals in seinem Namen weiter.
8. Sage, was die Beweise nicht zeigen: nicht beobachteter Zustand, abgetastete Traces, der abgedeckte Zeitraum. Es ist eine ausführbare Erklärung mit Trace-Beweisen, niemals eine formale Verifikation.

Formate, Selektoren und Zusicherungsarten: docs/REALITY-BRIDGE.md. Bedrohungsmodell: docs/TRACE-SECURITY.md. Grenzen der Beweise: docs/CONFORMANCE-LIMITS.md.

Ehrlichkeit in CI wahren

Wenn der Benutzer möchte, dass die Erklärung bei jedem Pull-Request überprüft wird, füge .working-model-ci.json hinzu (Modelle und welche von Behauptungen, Mutation, Fuzz, Reality und Parity ausgeführt werden sollen, mit expliziten Schwellenwerten) und kopiere .github/workflows/working-model-ci.example.yml. working-model ci --config .working-model-ci.json --format markdown gibt die Zusammenfassung aus, die ein Prüfer liest. Senke niemals einen Schwellenwert, um CI bestehen zu lassen. Details: docs/CI.md.

Spezifikation auf einen Blick

{
  "title": "Token-Bucket-Rate-Limiter",
  "summary": "Ein Eimer fasst bis zu {capacity} Token und füllt sich mit {refill} pro Sekunde wieder auf.",
  "sources": [{ "title": "RFC 2697", "url": "https://www.rfc-editor.org/rfc/rfc2697" }],
  "timeUnit": "s", "dt": 0.1, "duration": 16, "seed": 7,
  "params": [{ "id": "capacity", "label": "Eimergröße", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "Token" }],
  "events": [{ "name": "request", "at": 1, "count": 15 }],
  "state": { "tokens": "capacity", "accepted": 0, "rejected": 0 },
  "derived": { "fill": "tokens / capacity" },
  "rules": {
    "tick": "tokens = min(capacity, tokens + 2 * dt)",
    "on": { "request": ["if tokens >= 1 {", "  tokens -= 1; accepted += 1; emit('accept')", "} else {", "  rejected += 1; emit('reject')", "}"] }
  },
  "layout": { "cols": 12, "rows": 8 },
  "parts": [
    { "id": "bucket", "type": "tank", "at": [4, 0, 4, 4], "label": "Eimer", "level": "fill", "text": "{tokens:.1} von {capacity}" },
    { "id": "chart", "type": "chart", "at": [0, 5, 12, 3], "label": "Token", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "Die ersten {capacity} Anfragen verbrauchen die gespeicherten Token.", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "Ein voller Eimer lässt genau die ersten {capacity} Anfragen durch." }]
}

• Zeichenketten in state sind Ausdrücke ("capacity"); Textwerte benötigen innere Anführungszeichen ("'closed'").
• Regelsprache: Zahlen, Zeichenketten, Listen, true/false, + - * / % **, Vergleiche, and or not, c ? a : b, let, if / else if / else, while, for x in list, break, continue, Zuweisungsoperatoren und Funktionen wie min max abs clamp round sqrt exp log rand randint chance pick len push pop shift unshift remove contains indexOf slice sum range fill emit. Kein Mitgliedszugriff, keine benutzerdefinierten Funktionen, kein eval. Vollständige Referenz: references/spec.md.
• Teile: box tank queue stack grid counter gauge lamp node link chart label group, platziert auf dem Gitter mit at: [col, row, width, height]. Bindungen und Optionen: references/parts.md.
• Behauptungen und wie man gute schreibt: references/claims.md