modelo-funcional

Modelo Funcional

Escribes una pequeña especificación *.model.json: parámetros (controles deslizables), estado, reglas en un pequeño lenguaje seguro, un escenario de eventos, partes visuales vinculadas al estado, leyendas y afirmaciones. La CLI lo simula en Node, verifica cada afirmación, analiza el texto y genera una página HTML autónoma que ejecuta el mismo motor y vuelve a verificar las afirmaciones en vivo mientras el lector arrastra los controles.

La idea: una explicación que se prueba. Una afirmación que el modelo no puede respaldar falla antes de que el usuario la vea.

Comandos

Todos los comandos se ejecutan con Node 20 o más reciente y no necesitan npm install. Mantén las comillas: la ruta puede contener espacios.

node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers         # una especificación que ya pasa
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json  # esquema, simula, afirmaciones, análisis
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate   # ¿las afirmaciones atrapan reglas rotas?
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   # necesita Chrome o Edge local
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png           # imagen opcional
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7          # búsqueda de contraejemplos con semilla
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json   # modelo versus una traza observada

En adelante, modelo-funcional es abreviatura de node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs". En agentes que no sustituyen ${CLAUDE_SKILL_DIR}, usa la carpeta donde está este archivo. Códigos de salida de check: 0 si toda afirmación pasa, 1 si falla una afirmación o un error de análisis, 2 si la especificación no es válida. Añade --json para salida legible por máquina y --set nombre=valor para probar otras posiciones de los controles. --mutate sale con 0 a menos que las afirmaciones fallen; añade --mutate-strict (y --min-score 80) para salir con 1 cuando una afirmación nunca falla o la puntuación es baja. build --mutate guarda la puntuación en la página.

Flujo de trabajo

1. Elige el modelo más pequeño que muestre la parte sorprendente. Un mecanismo, un escenario, de 2 a 4 controles deslizables. Pregunta: ¿qué entendería mal un lector inteligente? Construye el escenario para que ese momento ocurra en pantalla (la ráfaga que vacía el cubo, los reintentos que caen juntos, el escaneo que vacía el caché).
2. Andamia o copia un ejemplo. Empieza desde modelo-funcional new <nombre> o el archivo más cercano en examples/ (cubo de fichas, retroceso con fluctuación, caché LRU, TCP AIMD, interruptor de circuito, epidemia SIR, interés compuesto, balanceo de carga, filtro Bloom, elección de líder Raft, punto de reorden de inventario).
3. Escribe parámetros, estado y reglas. Tiempo discreto: cada tick ejecuta rules.tick, luego los eventos de ese tick ejecutan su manejador rules.on.<evento>. Mantén las unidades honestas (timeUnit, slider unit). Usa emit('nombre', carga) para cosas que un enlace deba animar o una afirmación deba observar.
   • El tiempo es punto flotante. t es tick × dt, por lo que un tiempo almacenado como t + lead nunca es exactamente igual a un t posterior. Para plazos y cuentas regresivas, almacena números de tick (due = tick + round(lead / dt), luego tick >= due). references/spec.md tiene más trampas de este tipo en "Writing Rules That Behave".
   • Las listas son valores: a = b copia. Cambia una lista anidada a través de un índice (push(queues[i], job)).
4. Escribe de 3 a 8 afirmaciones que capturen las ideas clave, no trivialidades. Una afirmación que repite una regla ("las fichas nunca superan la capacidad" cuando la regla es min(capacity, ...)) no puede fallar y no enseña nada; las interesantes dicen algo que un lector no adivinaría: "un bucle con una clave más grande que el caché no obtiene ningún acierto en absoluto", "la fluctuación reduce el pico de carga de reintentos". Usa el tipo correcto (at, always, never, eventually, whenever, sweep, compare; consulta references/claims.md).
   • Al menos una afirmación debe cumplirse en los valores predeterminados y fallar cuando se mueve un control, para que el lector vea dónde deja de cumplirse la explicación. check lista qué posiciones de los controles rompen qué afirmaciones.
   • Cada afirmación debe ser verdadera para el mecanismo real, no solo para tu modelo. Pon la fuente de los datos clave en sources y expresa los supuestos del modelo en summary. Escribe "en esta ejecución" cuando una afirmación solo se cumple para esta semilla.
   • Haz que la oración diga exactamente lo que verifica la expresión. check prueba la expresión, no la oración; el paso 7 prueba si las afirmaciones pueden fallar en absoluto.
   • Haz que duration sea lo suficientemente larga para los ajustes más lentos de los controles, o las afirmaciones eventually fallarán solo porque la ejecución terminó.
5. Vincula números en el texto. Las leyendas y el texto de las afirmaciones aceptan espacios {expression}: escribe {capacity}, nunca un literal 10 que quede obsoleto cuando se mueve un control. check advierte sobre números literales (W_LITERAL_NUMBER) y sugiere la vinculación. Una leyenda debe citar las afirmaciones en las que se basa (cites); citar una afirmación que falla es un error.
6. Ejecuta check hasta que diga N/N claims pass sin errores. También corrige las advertencias.
7. Luego ejecuta check --mutate: prueba las afirmaciones. Rompe las reglas a propósito, un pequeño cambio por mutante (< por <=, pop por shift, una línea eliminada, un evento un tick tarde), vuelve a verificar cada afirmación contra cada mutante e informa qué afirmaciones atrapan qué errores.
   • Cada afirmación debe matar al menos un mutante. Una afirmación listada bajo "Afirmaciones que nunca fallaron" no puede fallar: repite una regla, pasa de forma vacua o el escenario nunca la ejercita. Refuérzala (haz que la expresión diga toda su oración) o cambia el escenario para que la afirmación se ponga a prueba (arribos escalonados en lugar de una ráfaga, un bucle que no cabe). references/claims.md tiene un ejemplo trabajado.
   • Para cada mutante que sobrevive, añade o refuerza una afirmación, o explica en tu respuesta por qué el cambio no se puede ver (por ejemplo, solo renombra claves). Solo uno verdaderamente inofensivo va a mutate.ignore en la especificación, con su motivo. Nunca debilites una afirmación o una aserción para subir la puntuación.
   • Los mutantes marcados equivalentes o solo visuales no cambian nada que una afirmación pueda ver; quedan fuera de la puntuación. Los solo visuales cambian lo que dibuja la página, así que verifica esos números en la captura de pantalla.
8. Nunca debilites ni elimines una afirmación solo para que pase. Cuando una afirmación falla, decide cuál está mal:
   • el modelo está mal (un error de reglas, un valor predeterminado incorrecto, un mecanismo faltante): corrige el modelo;
   • la afirmación está mal (el mecanismo real no se comporta así, o solo lo hace bajo una condición): corrige la afirmación y di qué estaba mal. Dile al usuario cuál fue y por qué, en una o dos oraciones. Aflojar una tolerancia hasta que pase, o intercambiar una afirmación por una más fácil, no está permitido.
9. Construye, luego ejecuta layout. Corrige cada problema E_ (partes superpuestas, texto desbordado, texto colisionando, página desplazándose lateralmente a 390 px). Generalmente: dale a la parte más celdas de cuadrícula, acorta una etiqueta o mueve una parte. Corrige W_LINK_CROSSES (una flecha dibujada a través de otra parte): mueve una parte o añade puntos via. Mira la captura de pantalla que escribe y verifica que cada número mostrado sea el que pretendías: los enlaces de partes no son probados por ninguna afirmación. Para un contador o indicador en el que el lector confiará, añade un expect (una forma independiente de calcular el mismo número, por ejemplo "expect": "len(queue)"), y check falla si alguna vez difieren.
10. Entrega: la ruta del HTML, la línea de resumen de afirmaciones (6/6 claims pass) y la puntuación de mutación, una línea por afirmación, y qué control rompe qué afirmación. Menciona cualquier suposición del modelo que el lector deba conocer.

Búsqueda de contraejemplos

Después de que check y check --mutate pasen, modelo-funcional fuzz spec.model.json --cases 300 --seed 7 ejecuta las mismas afirmaciones en casos cercanos con semilla: valores de controles, la semilla del modelo y los eventos que un bloque fuzz marca como difusibles (desplazados, repetidos u omitidos). Luego modelo-funcional minimize spec.model.json --case .working-model/fuzz/first-failure.json reduce el primer fallo mientras mantiene la misma afirmación fallando. Informa el caso minimizado en palabras simples ("elimina los éxitos entre los fallos dispersos y el interruptor se dispara"). Un fallo en un ajuste no predeterminado es un hallazgo sobre dónde la explicación deja de cumplirse: corrige la afirmación o el modelo por razones sustanciales, conserva el contraejemplo y nunca debilites una afirmación para silenciarlo. "No se encontraron fallos" no es una prueba. Detalles: docs/FUZZ.md.

Comparación con una traza observada

Usa esto solo cuando el usuario tenga una traza del sistema real (JSONL, o el subconjunto JSON de OTLP), o pida la demo sintética en examples/reality-bridge/. Una traza nunca es obligatoria.

1. Di primero que una traza puede contener datos privados (ids de solicitud, ids de usuario, IPs, tokens) y trabaja localmente. La importación conserva solo los atributos que lee el mapeo: modelo-funcional trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json. Pasa --complete solo cuando el usuario confirme que la instrumentación registra cada evento de los tipos mapeados; de lo contrario, la completitud permanece unknown.
2. Mantén cuatro cosas separadas en lo que escribes: supuestos del modelo, datos del mecanismo de las fuentes, afirmaciones dentro del modelo y aserciones observadas. Pon los supuestos en reality.assumptions de la especificación.
3. Escribe el mapeo a partir de lo que realmente contiene la traza. Nunca inventes un id de correlación o un evento que la traza no registra; una salida sin un sujeto en ambos lados no está correlacionada y su aserción no es concluyente. Cada evento del modelo se reproduce o se lista en internalEvents.
4. Ejecuta modelo-funcional check spec.model.json --trace trace.normalized.json --mapping trace-map.json. Informa la línea del modelo y la línea observada por separado (Modelo: 4/4 afirmaciones pasan | Observado: 1 pasa, 2 fallan, 0 no concluyentes), la primera discrepancia con sus ids de evento y cada razón no concluyente tal cual. Salida 1 significa que una afirmación o una aserción observada falló; 2 una traza o mapeo no válido; 3 un archivo faltante o un límite.
5. Cuando la traza discrepe, corrige el supuesto por razones sustanciales, generalmente en un segundo modelo, y conserva el contraejemplo. Nunca aflojes minPrecision, minRecall o withinMs solo para pasar.
6. Para una página que ver, ejecuta modelo-funcional build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html: el explicador normal más una línea de tiempo modelo versus observado, la primera discrepancia y cada aserción. Contiene la traza normalizada, por lo que permanece local.
7. Solo si el usuario pide publicar, ejecuta modelo-funcional bundle spec.model.json --public ... --preview primero, muéstrales la lista clave, luego ejecútalo sin --preview. Una traza real necesita su --acknowledge-privacy explícito; nunca lo pases en su nombre.
8. Di lo que la evidencia no muestra: estado no observado, trazas muestreadas, la ventana de tiempo cubierta. Es una explicación ejecutable con evidencia de traza, nunca una verificación formal.

Formatos, selectores y tipos de aserción: docs/REALITY-BRIDGE.md. Modelo de amenazas: docs/TRACE-SECURITY.md. Límites de la evidencia: docs/CONFORMANCE-LIMITS.md.

Mantener la honestidad en CI

Cuando el usuario quiera que la explicación se verifique en cada pull request, añade .working-model-ci.json (modelos, y cuáles de afirmaciones, mutación, fuzz, realidad y paridad ejecutar, con umbrales explícitos) y copia .github/workflows/working-model-ci.example.yml. modelo-funcional ci --config .working-model-ci.json --format markdown imprime el resumen que un revisor lee. Nunca bajes un umbral para que CI pase. Detalles: docs/CI.md.

Especificación de un vistazo

{
  "title": "Limitador de velocidad de cubo de fichas",
  "summary": "Un cubo contiene hasta {capacity} fichas y se rellena 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": "Tamaño del cubo", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "fichas" }],
  "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": "cubo", "type": "tank", "at": [4, 0, 4, 4], "label": "Cubo", "level": "fill", "text": "{tokens:.1} de {capacity}" },
    { "id": "grafico", "type": "chart", "at": [0, 5, 12, 3], "label": "Fichas", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "Las primeras {capacity} solicitudes gastan las fichas almacenadas.", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "Un cubo lleno deja pasar exactamente las primeras {capacity} solicitudes." }]
}

• Las cadenas en state son expresiones ("capacity"); los valores de texto necesitan comillas internas ("'closed'").
• Lenguaje de reglas: números, cadenas, listas, true/false, + - * / % **, comparaciones, and or not, c ? a : b, let, if / else if / else, while, for x in list, break, continue, operadores de asignación y funciones 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. Sin acceso a miembros, sin funciones de usuario, sin eval. Referencia completa: references/spec.md.
• Partes: box tank queue stack grid counter gauge lamp node link chart label group, colocadas en la cuadrícula con at: [col, row, width, height]. Vinculaciones y opciones: references/parts.md.
• Afirmaciones y cómo escribir buenas: references/claims.md

…

[truncado para traducción]