Modelo Funcional

O que Modelo Funcional faz?

Você escreve uma especificação pequena *.model.json: parâmetros (controles deslizantes), estado, regras em uma pequena linguagem segura, um cenário de eventos, partes visuais vinculadas ao estado, legendas e afirmações. O CLI simula em Node, verifica cada afirmação, faz lint do texto e compila uma página HTML offline que executa o mesmo motor e re-verifica as afirmações ao vivo enquanto o leitor arrasta os controles.

A ideia: uma explicação que é testada. Uma afirmação que o modelo não consegue sustentar falha antes mesmo do usuário vê-la.

Comandos

Todos os comandos rodam com Node 20 ou mais novo e não precisam de npm install. Mantenha as aspas: o caminho pode conter espaços.

node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers         # uma especificação que já passa
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json  # schema, simular, afirmações, lint
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate   # as afirmações pegam regras quebradas?
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   # precisa de Chrome ou Edge local
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png           # imagem opcional
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7          # busca de contraexemplo com semente
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json   # modelo versus um trace observado

Abaixo, working-model é abreviação para node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs". Em agentes que não substituem ${CLAUDE_SKILL_DIR}, use a pasta onde este arquivo está. Códigos de saída de check: 0 toda afirmação passa, 1 uma afirmação ou erro de lint falha, 2 a especificação é inválida. Adicione --json para saída legível por máquina e --set nome=valor para testar outras posições dos sliders. --mutate sai com 0 a menos que as afirmações falhem; adicione --mutate-strict (e --min-score 80) para sair com 1 quando uma afirmação nunca falha ou a pontuação é baixa. build --mutate armazena a pontuação na página.

Fluxo de Trabalho

1. Escolha o menor modelo que mostre a parte surpreendente. Um mecanismo, um cenário, 2 a 4 controles. Pergunte: o que um leitor inteligente entenderia errado? Construa o cenário para que esse momento aconteça na tela (a rajada que esvazia o balde, as retentativas que chegam juntas, a varredura que limpa o cache).
2. Estruture ou copie um exemplo. Comece de working-model new <nome> ou do arquivo mais próximo em examples/ (token bucket, backoff com jitter, cache LRU, TCP AIMD, circuit breaker, epidemia SIR, juros compostos, balanceamento de carga, filtro Bloom, eleição de líder Raft, ponto de reposição de estoque).
3. Escreva parâmetros, estado e regras. Tempo discreto: cada tick executa rules.tick, depois os eventos desse tick disparam seus manipuladores rules.on.<evento>. Mantenha as unidades honestas (timeUnit, slider unit). Use emit('nome', payload) para coisas que um link deve animar ou uma afirmação deve observar.
   • Tempo é ponto flutuante. t é tick × dt, então um tempo armazenado como t + lead nunca é exatamente igual a um t posterior. Para prazos e contagens regressivas, armazene números de tick (due = tick + round(lead / dt), depois tick >= due). references/spec.md tem mais dessas armadilhas em "Writing Rules That Behave".
   • Listas são valores: a = b copia. Altere uma lista aninhada através de um índice (push(queues[i], job)).
4. Escreva 3 a 8 afirmações que capturem os insights principais, não trivialidades. Uma afirmação que apenas repete uma regra ("tokens nunca excedem a capacidade" quando a regra é min(capacidade, ...)) não pode falhar e não ensina nada; as interessantes dizem algo que um leitor não adivinharia: "um loop uma chave maior que o cache não tem acertos", "jitter reduz o pico de carga de retentativas". Use o tipo certo (at, always, never, eventually, whenever, sweep, compare; veja references/claims.md).
   • Pelo menos uma afirmação deve ser válida nos padrões e falhar quando um slider se move, para que o leitor veja onde a explicação deixa de valer. check lista quais posições do slider quebram quais afirmações.
   • Cada afirmação deve ser verdadeira para o mecanismo real, não apenas para o seu modelo. Coloque a fonte dos fatos principais em sources e declare as suposições do modelo em summary. Escreva "nesta execução" quando uma afirmação só vale para esta semente.
   • Faça a frase dizer exatamente o que a expressão verifica. check prova a expressão, não a frase; o passo 7 testa se as afirmações podem falhar.
   • Faça a duration longa o suficiente para as configurações de slider mais lentas, ou as afirmações eventually falham apenas porque a execução terminou.
5. Vincule números no texto. Legendas e texto de afirmações aceitam buracos {expressão}: escreva {capacity}, nunca o literal 10 que fica desatualizado quando um slider se move. check avisa sobre números literais (W_LITERAL_NUMBER) e sugere a vinculação. Uma legenda deve citar as afirmações em que confia (cites); citar uma afirmação que falha é um erro.
6. Execute check até que diga N/N afirmações passam sem erros. Conserte também os avisos.
7. Depois execute check --mutate: teste as afirmações. Ele quebra as regras de propósito, uma pequena mudança por mutante (< por <=, pop por shift, uma linha deletada, um evento um tick atrasado), re-verifica cada afirmação contra cada mutante e relata quais afirmações pegam quais bugs.
   • Cada afirmação deve matar pelo menos um mutante. Uma afirmação listada em "Afirmações que nunca falharam" não pode falhar: ela repete uma regra, passa vacuamente, ou o cenário nunca a exercita. Reforce-a (faça a expressão dizer toda a sua frase) ou mude o cenário para que a afirmação seja colocada à prova (chegadas escalonadas em vez de uma rajada, um loop que não cabe). references/claims.md tem um exemplo trabalhado.
   • Para cada mutante sobrevivente, adicione ou reforce uma afirmação, ou explique em sua resposta por que a mudança não pode ser vista (por exemplo, só renomeia chaves). Apenas um mutante verdadeiramente inofensivo vai para mutate.ignore na especificação, com sua razão. Nunca enfraqueça uma afirmação ou uma asserção para aumentar a pontuação.
   • Mutantes marcados como equivalentes ou apenas visuais não mudam nada que uma afirmação possa ver; eles são deixados de fora da pontuação. Os apenas visuais mudam o que a página desenha, então verifique esses números na captura de tela.
8. Nunca enfraqueça ou delete uma afirmação só para fazê-la passar. Quando uma afirmação falha, decida qual está errada:
   • o modelo está errado (um bug na regra, um padrão errado, um mecanismo faltando): corrija o modelo;
   • a afirmação está errada (o mecanismo real não se comporta assim, ou só o faz sob uma condição): corrija a afirmação e diga o que estava errado. Informe ao usuário qual foi e por que, em uma ou duas frases. Afrouxar uma tolerância até passar, ou trocar uma afirmação por uma mais fácil, não é permitido.
9. Compile, depois execute layout. Corrija todo problema E_ (partes sobrepostas, texto vazando, texto colidindo, página rolando lateralmente a 390 px). Geralmente: dê à parte mais células da grade, encurte um rótulo ou mova uma parte. Corrija W_LINK_CROSSES também (uma seta desenhada sobre outra parte): mova uma parte ou adicione pontos via. Olhe a captura de tela que ele escreve e verifique se cada número mostrado é o que você pretendia: vinculações de parte não são testadas por nenhuma afirmação. Para um contador ou medidor no qual um leitor confiará, adicione um expect (uma maneira independente de computar o mesmo número, como "expect": "len(queue)"), e check falha se os dois diferirem.
10. Entregue: o caminho do HTML, a linha de resumo das afirmações (6/6 afirmações passam) e a pontuação de mutação, uma linha por afirmação, e qual slider quebra qual afirmação. Mencione qualquer suposição do modelo que o leitor deva saber.

Procurando Contraexemplos

Depois que check e check --mutate passam, working-model fuzz spec.model.json --cases 300 --seed 7 executa as mesmas afirmações em casos próximos semeados: valores de slider, a semente do modelo e os eventos que um bloco fuzz marca como fuzzyficáveis (deslocados, repetidos ou removidos). Depois, working-model minimize spec.model.json --case .working-model/fuzz/first-failure.json reduz o primeiro falha enquanto mantém a mesma afirmação falhando. Relate o caso minimizado em palavras claras ("solte os sucessos entre as falhas espalhadas e o disjuntor dispara"). Uma falha em uma configuração não padrão é uma descoberta sobre onde a explicação para de valer: corrija a afirmação ou o modelo com base substantiva, mantenha o contraexemplo e nunca enfraqueça uma afirmação para silenciá-lo. "Nenhuma falha encontrada" não é uma prova. Detalhes: docs/FUZZ.md.

Comparando com um Trace Observado

Use isso apenas quando o usuário tiver um trace do sistema real (JSONL, ou o subconjunto JSON OTLP), ou pedir a demonstração sintética em examples/reality-bridge/. Um trace nunca é obrigatório.

1. Diga primeiro que um trace pode conter dados privados (IDs de requisição, IDs de usuário, IPs, tokens) e trabalhe localmente. A importação mantém apenas os atributos que o mapeamento lê: working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json. Passe --complete apenas quando o usuário confirmar que a instrumentação registra todos os eventos dos tipos mapeados; caso contrário, a completude permanece unknown.
2. Mantenha quatro coisas separadas no que você escreve: suposições do modelo, fatos do mecanismo das fontes, afirmações dentro do modelo e asserções observadas. Coloque as suposições em reality.assumptions da especificação.
3. Escreva o mapeamento do que o trace realmente contém. Nunca invente um ID de correlação ou um evento que o trace não registra; uma saída sem um sujeito em ambos os lados é não correlacionada e sua asserção é inconclusiva. Cada evento do modelo é reproduzido ou listado em internalEvents.
4. Rode working-model check spec.model.json --trace trace.normalized.json --mapping trace-map.json. Relate a linha do modelo e a linha observada separadamente (Modelo: 4/4 afirmações passam | Observado: 1 passa, 2 falham, 0 inconclusivos), a primeira incompatibilidade com seus IDs de evento e cada razão inconclusiva como ela é. Saída 1 significa que uma afirmação ou asserção observada falhou; 2 um trace ou mapeamento inválido; 3 um arquivo ou limite faltando.
5. Quando o trace discorda, corrija a suposição com base substantiva, geralmente em um segundo modelo, e mantenha o contraexemplo. Nunca afrouxe minPrecision, minRecall ou withinMs só para passar.
6. Para uma página para visualizar, rode working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html: o explicador normal mais uma linha do tempo modelo-versus-observado, a primeira incompatibilidade e cada asserção. Ela contém o trace normalizado, então permanece local.
7. Apenas se o usuário pedir para publicar, rode working-model bundle spec.model.json --public ... --preview primeiro, mostre a lista de chaves, depois execute sem --preview. Um trace real precisa do seu --acknowledge-privacy explícito; nunca passe em nome dele.
8. Diga o que a evidência não mostra: estado não observado, traces amostrados, a janela de tempo coberta. É uma explicação executável com evidência de trace, nunca verificação formal.

Formatos, seletores e tipos de asserção: docs/REALITY-BRIDGE.md. Modelo de ameaça: docs/TRACE-SECURITY.md. Limites da evidência: docs/CONFORMANCE-LIMITS.md.

Mantendo a Honestidade em CI

Quando o usuário quiser que a explicação seja verificada em cada pull request, adicione .working-model-ci.json (modelos e quais de afirmações, mutação, fuzz, realidade e paridade executar, com limites explícitos) e copie .github/workflows/working-model-ci.example.yml. working-model ci --config .working-model-ci.json --format markdown imprime o resumo que um revisor lê. Nunca abaixe um limite para fazer o CI passar. Detalhes: docs/CI.md.

Especificação de relance

{
  "title": "Token Bucket Rate Limiter",
  "summary": "Um balde contém até {capacity} tokens e reabastece a {refill} por segundo.",
  "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": "Tamanho do balde", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "tokens" }],
  "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": "Balde", "level": "fill", "text": "{tokens:.1} de {capacity}" },
    { "id": "chart", "type": "chart", "at": [0, 5, 12, 3], "label": "Tokens", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "As primeiras {capacity} requisições gastam os tokens armazenados.", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "Um balde cheio deixa passar exatamente as primeiras {capacity} requisições." }]
}

• Strings em state são expressões ("capacity"); valores de texto precisam de aspas internas ("'closed'").
• Linguagem de regras: números, strings, listas, true/false, + - * / % **, comparações, and or not, c ? a : b, let, if / else if / else, while, for x in list, break, continue, operadores de atribuição e funções como 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. Sem acesso a membros, funções de usuário, eval. Referência completa: references/spec.md.
• Partes: box tank queue stack grid counter gauge lamp node link chart label group, colocadas na grade com at: [col, row, width, height]. Vinculações e opções: references/parts.md.
• Afirmações e como escrever boas: references/claims.md