Modèle de Travail (Working Model)
Vous écrivez une petite spécification *.model.json : paramètres (curseurs), état, règles dans un petit langage sûr, un scénario d'événements, des parties visuelles liées à l'état, des légendes et des affirmations. La CLI le simule dans Node, vérifie chaque affirmation, lint le texte, et construit une page HTML hors ligne qui exécute le même moteur et re-vérifie les affirmations en direct pendant que le lecteur manipule les curseurs.
Le but : une explication qui est testée. Une affirmation que le modèle ne peut pas justifier échoue avant même que l'utilisateur ne la voie.
Commandes
Toutes les commandes s'exécutent avec Node 20 ou plus récent et n'ont pas besoin de npm install. Conservez les guillemets : le chemin peut contenir des espaces.
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers # une spécification qui réussit déjà
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json # schéma, simulation, affirmations, lint
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate # les affirmations attrapent-elles les règles cassées ?
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 # nécessite Chrome ou Edge local
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png # image optionnelle
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7 # recherche de contre-exemples avec graine
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json # modèle versus trace observée
Ci-dessous, working-model est l'abréviation de node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs". Dans les agents qui ne substituent pas ${CLAUDE_SKILL_DIR}, utilisez le dossier où se trouve ce fichier. Codes de sortie de check : 0 chaque affirmation réussit, 1 une affirmation ou une erreur de lint échoue, 2 la spécification est invalide. Ajoutez --json pour une sortie lisible par machine et --set nom=valeur pour essayer d'autres positions de curseur. --mutate sort avec 0 sauf si les affirmations échouent ; ajoutez --mutate-strict (et --min-score 80) pour sortir avec 1 quand une affirmation n'échoue jamais ou que le score est bas. build --mutate stocke le score dans la page.
Flux de travail
- Choisissez le plus petit modèle qui montre la partie surprenante. Un mécanisme, un scénario, 2 à 4 curseurs. Demandez : qu'est-ce qu'un lecteur intelligent comprendrait de travers ? Construisez le scénario pour que ce moment se produise à l'écran (la rafale qui vide le seau, les tentatives qui atterrissent ensemble, le scan qui vide le cache).
- Échafaudez ou copiez un exemple. Commencez par
working-model new <nom>ou le fichier le plus proche dansexamples/(token bucket, backoff avec jitter, cache LRU, TCP AIMD, circuit breaker, épidémie SIR, intérêts composés, équilibrage de charge, filtre de Bloom, élection de leader Raft, point de réapprovisionnement d'inventaire). - Écrivez paramètres, état et règles. Temps discret : chaque tick exécute
rules.tick, puis les événements de ce tick déclenchent leur gestionnairerules.on.<événement>. Gardez les unités honnêtes (timeUnit, curseurunit). Utilisezemit('nom', payload)pour les choses qu'un lien devrait animer ou qu'une affirmation devrait surveiller.- Le temps est en virgule flottante.
testtick × dt, donc un temps stocké commet + leadn'atteint jamais exactement untultérieur. Pour les délais et les comptes à rebours, stockez les numéros de tick (due = tick + round(lead / dt), puistick >= due).references/spec.mdcontient d'autres pièges dans "Writing Rules That Behave". - Les listes sont des valeurs :
a = bcopie. Modifiez une liste imbriquée via un index (push(queues[i], job)).
- Le temps est en virgule flottante.
- Écrivez 3 à 8 affirmations qui capturent les idées clés, pas des banalités. Une affirmation qui répète une règle ("les jetons ne dépassent jamais la capacité" alors que la règle est
min(capacity, ...)) ne peut pas échouer et n'apprend rien ; les affirmations intéressantes disent quelque chose qu'un lecteur ne devinerait pas : "une boucle d'une clé plus grande que le cache n'obtient aucun hit du tout", "le jitter abaisse le pic de charge de tentatives". Utilisez le bon type (at,always,never,eventually,whenever,sweep,compare; voirreferences/claims.md).- Au moins une affirmation doit être valable avec les valeurs par défaut et échouer lorsqu'un curseur bouge, afin que le lecteur voie où l'explication cesse d'être valable.
checkliste quelles positions de curseur brisent quelles affirmations. - Chaque affirmation doit être vraie pour le mécanisme réel, pas seulement pour votre modèle. Mettez la source des faits clés dans
sources, et indiquez les hypothèses du modèle dans lesummary. Écrivez "dans cette exécution" quand une affirmation n'est valable que pour cette graine. - Faites en sorte que la phrase dise exactement ce que l'expression vérifie.
checkprouve l'expression, pas la phrase ; l'étape 7 teste si les affirmations peuvent échouer du tout. - Faites en sorte que
durationsoit suffisamment long pour les réglages de curseur les plus lents, sinon les affirmationseventuallyéchouent seulement parce que l'exécution s'est terminée.
- Au moins une affirmation doit être valable avec les valeurs par défaut et échouer lorsqu'un curseur bouge, afin que le lecteur voie où l'explication cesse d'être valable.
- Liez les nombres dans le texte. Les légendes et le texte des affirmations prennent des trous
{expression}: écrivez{capacity}, jamais un littéral10qui deviendrait obsolète lorsqu'un curseur bouge.checkavertit des nombres littéraux (W_LITERAL_NUMBER) et suggère la liaison. Une légende doit citer les affirmations sur lesquelles elle s'appuie (cites) ; citer une affirmation qui échoue est une erreur. - Exécutez
checkjusqu'à ce qu'il diseN/N claims passsans erreurs. Corrigez aussi les avertissements. - Ensuite, exécutez
check --mutate: testez les affirmations. Il casse les règles intentionnellement, un petit changement par mutant (<pour<=,poppourshift, une ligne supprimée, un événement en retard d'un tick), re-vérifie chaque affirmation contre chaque mutant, et rapporte quelles affirmations attrapent quels bogues.- Chaque affirmation doit tuer au moins un mutant. Une affirmation listée sous "Claims that never failed" ne peut pas échouer : elle reformule une règle, réussit par vacuité, ou le scénario ne l'exerce jamais. Renforcez-la (faites en sorte que l'exprime tout ce que dit sa phrase) ou changez le scénario pour que l'affirmation soit mise à l'épreuve (arrivées échelonnées au lieu d'une rafale, une boucle qui ne tient pas).
references/claims.mdcontient un exemple travaillé. - Pour chaque mutant survivant, soit ajoutez ou renforcez une affirmation, soit expliquez dans votre réponse pourquoi le changement ne peut pas être vu (par exemple, il ne fait que renommer des clés). Seul un mutant vraiment inoffensif va dans
mutate.ignoredans la spécification, avec sa raison. N'affaiblissez jamais une affirmation ou une assertion pour augmenter le score. - Les mutants marqués équivalents ou seulement visuels ne changent rien que l'affirmation puisse voir ; ils sont exclus du score. Ceux qui sont seulement visuels changent ce que la page dessine, donc vérifiez ces nombres dans la capture d'écran.
- Chaque affirmation doit tuer au moins un mutant. Une affirmation listée sous "Claims that never failed" ne peut pas échouer : elle reformule une règle, réussit par vacuité, ou le scénario ne l'exerce jamais. Renforcez-la (faites en sorte que l'exprime tout ce que dit sa phrase) ou changez le scénario pour que l'affirmation soit mise à l'épreuve (arrivées échelonnées au lieu d'une rafale, une boucle qui ne tient pas).
- N'affaiblissez ni ne supprimez jamais une affirmation juste pour la faire réussir. Quand une affirmation échoue, décidez lequel est erroné :
- le modèle est erroné (un bogue de règle, une valeur par défaut erronée, un mécanisme manquant) : corrigez le modèle ;
- l'affirmation est erronée (le mécanisme réel ne se comporte pas ainsi, ou seulement sous une condition) : corrigez l'affirmation et dites ce qui n'allait pas. Dites à l'utilisateur lequel c'était et pourquoi, en une ou deux phrases. Assouplir une tolérance jusqu'à ce qu'elle réussisse, ou échanger une affirmation pour une plus facile, n'est pas autorisé.
- Construisez, puis exécutez
layout. Corrigez tout problèmeE_(parties qui se chevauchent, texte qui déborde, texte qui entre en collision, page qui défile latéralement à 390 px). Généralement : donnez à la partie plus de cellules de grille, raccourcissez une étiquette, ou déplacez une partie. CorrigezW_LINK_CROSSESaussi (une flèche dessinée à travers une autre partie) : déplacez une partie ou ajoutez des pointsvia. Regardez la capture d'écran qu'elle écrit, et vérifiez que chaque nombre affiché est celui que vous vouliez : les liaisons de parties ne sont testées par aucune affirmation. Pour un compteur ou un indicateur sur lequel un lecteur se fiera, ajoutez uneexpect(une manière indépendante de calculer le même nombre, comme"expect": "len(queue)"), etcheckéchoue si les deux diffèrent jamais. - Passez le relais : le chemin du fichier HTML, la ligne de résumé des affirmations (
6/6 claims pass) et le score de mutation, une ligne par affirmation, et quel curseur brise quelle affirmation. Mentionnez toute hypothèse du modèle que le lecteur devrait connaître.
Recherche de contre-exemples
Une fois check et check --mutate réussis, working-model fuzz spec.model.json --cases 300 --seed 7 exécute les mêmes affirmations sur des cas proches avec graine : valeurs de curseur, la graine du modèle, et les événements qu'un bloc fuzz marque comme fuzzables (décalés, répétés ou supprimés). Ensuite working-model minimize spec.model.json --case .working-model/fuzz/first-failure.json réduit le premier échec tout en gardant la même affirmation en échec. Rapportez le cas minimisé en termes simples ("supprimez les succès entre les échecs dispersés et le déclenchement du disjoncteur"). Un échec à un réglage non par défaut est une découverte sur où l'explication cesse d'être valable : corrigez l'affirmation ou le modèle sur des bases substantielles, conservez le contre-exemple, et n'affaiblissez jamais une affirmation pour la faire taire. "Aucun échec trouvé" n'est pas une preuve. Détails : docs/FUZZ.md.
Comparaison avec une trace observée
Utilisez ceci seulement lorsque l'utilisateur dispose d'une trace du système réel (JSONL, ou le sous-ensemble JSON OTLP), ou demande la démo synthétique dans examples/reality-bridge/. Une trace n'est jamais obligatoire.
- Dites d'abord qu'une trace peut contenir des données privées (identifiants de requête, identifiants d'utilisateur, IP, jetons) et travaillez dessus localement. L'import ne conserve que les attributs que le mappage lit :
working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json. Passez--completeseulement lorsque l'utilisateur confirme que l'instrumentation enregistre chaque événement des types mappés ; sinon, l'exhaustivité resteunknown. - Gardez quatre choses séparées dans ce que vous écrivez : les hypothèses du modèle, les faits du mécanisme issus de sources, les affirmations dans le modèle, et les assertions observées. Mettez les hypothèses dans
reality.assumptionsde la spécification. - Écrivez le mappage à partir de ce que la trace contient réellement. N'inventez jamais un identifiant de corrélation ou un événement que la trace n'enregistre pas ; une sortie sans sujet des deux côtés est non corrélée et son assertion est non concluante. Chaque événement du modèle est soit rejoué, soit listé dans
internalEvents. - Exécutez
working-model check spec.model.json --trace trace.normalized.json --mapping trace-map.json. Rapportez la ligne du modèle et la ligne observée séparément (Modèle : 4/4 affirmations réussies | Observé : 1 réussie, 2 échouées, 0 non concluante), la première divergence avec ses identifiants d'événement, et chaque raison non concluante telle qu'elle est. Le code de sortie 1 signifie qu'une affirmation ou une assertion observée a échoué ; 2 une trace ou un mappage invalide ; 3 un fichier manquant ou une limite. - Quand la trace est en désaccord, corrigez l'hypothèse sur des bases substantielles, généralement dans un deuxième modèle, et conservez le contre-exemple. N'assouplissez jamais
minPrecision,minRecallouwithinMsjuste pour réussir. - Pour une page à visualiser, exécutez
working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html: l'interface d'explication normale plus une chronologie modèle vs observé, la première divergence et chaque assertion. Elle contient la trace normalisée, donc elle reste locale. - Seulement si l'utilisateur demande à publier, exécutez d'abord
working-model bundle spec.model.json --public ... --preview, montrez-lui la liste des clés, puis exécutez-la sans--preview. Une trace réelle nécessite son--acknowledge-privacyexplicite ; ne le passez jamais en son nom. - Dites ce que la preuve ne montre pas : état non observé, traces échantillonnées, la fenêtre temporelle couverte. C'est une explication exécutable avec preuve par trace, jamais une vérification formelle.
Formats, sélecteurs et types d'assertions : docs/REALITY-BRIDGE.md. Modèle de menace : docs/TRACE-SECURITY.md. Limites de la preuve : docs/CONFORMANCE-LIMITS.md.
Rester honnête dans l'intégration continue (CI)
Quand l'utilisateur veut que l'explication soit vérifiée à chaque pull request, ajoutez .working-model-ci.json (modèles, et quels aspects exécuter parmi affirmations, mutation, fuzz, réalité et parité, avec des seuils explicites) et copiez .github/workflows/working-model-ci.example.yml. working-model ci --config .working-model-ci.json --format markdown imprime le résumé qu'un relecteur lit. N'abaissez jamais un seuil pour faire passer la CI. Détails : docs/CI.md.
Spécification en un coup d'œil
{
"title": "Limiteur de débit à seau de jetons",
"summary": "Un seau contient jusqu'à {capacity} jetons et se remplit à {refill} par seconde.",
"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": "Taille du seau", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "jetons" }],
"events": [{ "name": "requête", "at": 1, "count": 15 }],
"state": { "tokens": "capacity", "accepted": 0, "rejected": 0 },
"derived": { "fill": "tokens / capacity" },
"rules": {
"tick": "tokens = min(capacity, tokens + 2 * dt)",
"on": { "requête": ["if tokens >= 1 {", " tokens -= 1; accepted += 1; emit('accept')", "} else {", " rejected += 1; emit('reject')", "}"] }
},
"layout": { "cols": 12, "rows": 8 },
"parts": [
{ "id": "seau", "type": "tank", "at": [4, 0, 4, 4], "label": "Seau", "level": "fill", "text": "{tokens:.1} sur {capacity}" },
{ "id": "graphique", "type": "chart", "at": [0, 5, 12, 3], "label": "Jetons", "series": [{ "expr": "tokens" }] }
],
"narration": [{ "from": 1, "to": 3, "text": "Les {capacity} premières requêtes dépensent les jetons stockés.", "cites": ["rafale-passe"] }],
"claims": [{ "id": "rafale-passe", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "Un seau plein laisse passer exactement les {capacity} premières requêtes." }]
}
- Les chaînes dans
statesont des expressions ("capacity") ; les valeurs textuelles ont besoin de guillemets intérieurs ("'fermé'"). - Langage des règles : nombres, chaînes, listes,
true/false,+ - * / % **, comparaisons,and or not,c ? a : b,let,if / else if / else,while,for x in list,break,continue, opérateurs d'affectation, et fonctions telles quemin max abs clamp round sqrt exp log rand randint chance pick len push pop shift unshift remove contains indexOf slice sum range fill emit. Pas d'accès aux membres, pas de fonctions utilisateur, pas deeval. Référence complète :references/spec.md. - Parties :
box tank queue stack grid counter gauge lamp node link chart label group, placées sur la grille avecat: [col, line, width, height]. Liaisons et options :references/parts.md. - Affirmations et comment en écrire de bonnes :
references/claims.md