Por qué importa la semántica formal

Toda la maquinaria de este nivel —el bucle de dos colas, la preempción por profundidad, el ancestro compuesto común más bajo, las tres reglas de consistencia— existe para producir una sola propiedad, y conviene enunciarla sin adornos: dada una configuración estable y un evento, el resultado está determinado. No probablemente determinado, no determinado salvo condiciones de carrera, no determinado si el intérprete está bien escrito. Determinado por definición, y comprobable contra una especificación pública. Esa propiedad parece modesta hasta que uno enumera lo que se deriva de ella, porque de ella salen la capacidad de predecir una traza con un lápiz, la generación automática de casos de prueba, la verificación de propiedades temporales, la reproducibilidad exacta de un informe de error y la portabilidad del mismo modelo entre lenguajes que no comparten nada más. Esta lección es el inventario de esas consecuencias, y también de sus límites.

Predecir sin ejecutar: la máquina como objeto analizable

Un programa imperativo corriente no se puede analizar de forma exhaustiva: su estado es la memoria entera, sus transiciones son cualquier asignación y su grafo de control depende de valores que solo se conocen ejecutando. Una máquina de estado invierte las tres cosas. Su espacio de configuraciones es finito y enumerable, sus transiciones están declaradas en el documento, y la función que las aplica está normalizada. Eso la convierte en un objeto matemático sobre el que se pueden hacer preguntas y obtener respuestas antes de escribir una sola prueba.

flowchart LR
M[documento del statechart] --> G[grafo de configuraciones]
G --> A[alcanzabilidad y estados muertos]
G --> T[generacion de trazas de prueba]
G --> V[verificacion de propiedades temporales]
G --> D[documentacion siempre exacta]
style M fill:#cba6f7,color:#11111b
style G fill:#89b4fa,color:#11111b
style V fill:#a6e3a1,color:#11111b

La transformación clave es la primera flecha: del documento al grafo. Un statechart declara estados y transiciones, pero lo que se puede analizar no es esa declaración sino el grafo que induce, cuyos nodos son configuraciones legales completas y cuyas aristas son macrosteps etiquetados con eventos. Construir ese grafo es mecánico precisamente por todo lo visto en las lecciones anteriores: se parte de la configuración inicial, se prueban todos los eventos posibles, se aplica el algoritmo para obtener la configuración siguiente, y se repite hasta que no aparezcan configuraciones nuevas. Sin una semántica determinista ese procedimiento no terminaría en un grafo sino en un árbol de posibilidades, que es otra manera de decir que no serviría de nada.

Las cuatro ramas del diagrama son cuatro clases de pregunta que se responden sin ejecutar el programa real, y ninguna de ellas requiere que la aplicación exista todavía: se responden sobre el modelo, que suele estar escrito mucho antes que la interfaz que lo consume. La alcanzabilidad pregunta si existe alguna secuencia de eventos que lleve de la configuración inicial a una dada; su complemento identifica estados muertos y transiciones inalcanzables, que son casi siempre errores de modelado o restos de un refactor. La generación de trazas recorre el grafo produciendo caminos que después se ejecutan contra la implementación real: eso son las pruebas basadas en modelo, donde no escribes los casos sino el modelo del que se derivan. La verificación de propiedades temporales pregunta cosas de la forma nunca ocurre esto o siempre acaba pasando aquello, que es el terreno de los verificadores de modelos. Y la documentación deja de desincronizarse porque se genera del mismo artefacto que se ejecuta.

// Las trazas no se escriben: se derivan del grafo.
import { getShortestPaths } from '@xstate/graph'

const caminos = getShortestPaths(maquinaCheckout, {
  events: [{ type: 'AÑADIR' }, { type: 'PAGAR' }, { type: 'CANCELAR' }],
})

// Cada camino es una secuencia de eventos que alcanza una configuracion.
// Ejecutarlos todos contra la UI real es cobertura por construccion,
// no por buena voluntad de quien escribe los tests.

Hay una quinta consecuencia que rara vez se menciona y que en un equipo grande vale más que las otras cuatro juntas: la reproducibilidad de los errores. En un sistema con estado implícito, un informe de error es una narración —estaba editando, se me fue el internet, le di dos veces y se quedó colgado— que el siguiente ingeniero debe traducir a hipótesis. En un sistema con semántica determinista, un informe de error es un dato: la configuración de partida y la secuencia de eventos. Ese par reproduce el fallo siempre, en la máquina de cualquiera, sin depender del momento de llegada de los mensajes ni de la carga del sistema. Un error que se reproduce a voluntad ya está medio arreglado, y la diferencia entre las dos situaciones no es de disciplina del equipo sino de si el modelo subyacente es una función o una acumulación de accidentes.

Conviene también señalar el límite de esta primera mitad. Todo lo anterior vale para el grafo de configuraciones, es decir, para el control. En cuanto el context guarda datos con dominio amplio, el grafo deja de ser finito y las cuatro clases de pregunta se vuelven aproximaciones: los generadores de caminos necesitan que le acotes los eventos y los valores, y la verificación necesita que agrupes estados en clases equivalentes. La analizabilidad no es una propiedad binaria de la máquina sino una propiedad de la parte que hayas conseguido mantener en el control en lugar de en los datos, lo cual es, de paso, un argumento técnico a favor de modelar con estados lo que estarías tentado de guardar en una variable.

Interoperabilidad: el mismo grafo en muchos runtimes

La segunda mitad del argumento no es sobre análisis sino sobre portabilidad, y depende de que la semántica no solo sea precisa sino compartida. El W3C publicó junto a la Recomendación una suite de conformidad con más de un centenar de casos automatizados, cada uno diseñado para fijar un punto concreto del algoritmo: qué ocurre si dos transiciones compiten, en qué orden se ejecutan las acciones de salida, si un evento levantado en un entry se procesa antes de estabilizar. Un intérprete pasa esos tests o no los pasa, y esa binariedad convierte una discusión de diseño en una medición.

La lista tiene además un valor histórico que se pierde de vista: son implementaciones escritas por equipos que no se conocían, en lenguajes con modelos de memoria y concurrencia radicalmente distintos, a lo largo de una década larga, y aun así coinciden en cómo resuelven un conflicto entre un hijo y su padre. Esa coincidencia no es cultural ni casual: es lo que ocurre cuando existe un documento que zanja la cuestión y una suite que comprueba que lo has leído bien.

Que exista esa tabla es lo que permite un patrón de trabajo que sería impensable sin estándar: modelar una vez y ejecutar en varios sitios. El comportamiento de un dispositivo puede diseñarse como statechart, ejecutarse compilado en el firmware, simularse en una interfaz web que reproduce exactamente las mismas transiciones, y probarse con las mismas trazas en ambos lados. La equivalencia no es aproximada ni depende de que dos equipos hayan interpretado igual un documento de requisitos: está garantizada por el algoritmo y verificada por la suite.

Hay además un beneficio más silencioso y quizá más valioso, que es el vocabulario. Cuando un equipo dice que una transición es interna, que un evento va a la cola interna, que dos transiciones están en conflicto o que la configuración es estable, esas palabras tienen definición única y consultable. Las discusiones de diseño dejan de ser negociaciones entre intuiciones y pasan a ser desacuerdos sobre hechos, que son mucho más fáciles de cerrar.

La interoperabilidad se extiende también a las herramientas, y ahí es donde un equipo de producto la nota antes. Como la estructura del modelo está normalizada, un editor visual puede leer una máquina escrita a mano, un inspector puede reconstruir la traza de una sesión en producción, un exportador puede generar documentación y un simulador puede ejecutar la máquina sin la aplicación alrededor. Todas esas herramientas hablan del mismo objeto porque el objeto tiene una definición pública. Sin ella, cada herramienta necesitaría su propio formato y ninguna podría leer lo que produce la anterior, que es exactamente la situación en la que vive la mayoría del tooling de gestión de estado.

Los límites: lo que la formalidad no te da

Un inventario honesto tiene que incluir el pasivo, y aquí hay cuatro partidas que conviene tener presentes antes de que la elegancia del aparato produzca falsas expectativas. Las cuatro comparten una raíz común: la semántica formal define con exactitud una relación entre símbolos, y todo lo que quede fuera de esa relación queda también fuera de sus garantías.

Hay además un límite de escala que conviene anticipar. La enumeración exhaustiva del grafo de configuraciones es viable mientras el espacio sea pequeño, pero el context con datos arbitrarios lo vuelve infinito de inmediato: una máquina de ocho estados con un contador entero tiene tantas configuraciones extendidas como valores admita el contador. Las técnicas serias de verificación resuelven esto con abstracción —agrupar valores en clases equivalentes— y eso es trabajo humano y difícil. La formalidad del control no te regala la formalidad de los datos.

El primer límite es el que más equivocaciones produce y merece un ejemplo. Una máquina de compra que permite confirmar el pago dos veces porque nadie modeló el estado intermedio es una máquina impecable desde el punto de vista de la semántica: cada transición está bien definida, cada configuración es legal, la traza es determinista y reproducible. El error no está en la ejecución sino en el modelo, y ningún algoritmo de interpretación lo detectará jamás, porque el algoritmo no sabe qué es un pago. La formalidad garantiza fidelidad entre el modelo y su ejecución, nunca entre el modelo y el mundo; ese segundo puente lo cruza el diseñador o no lo cruza nadie.

Por qué esto sobrevive a la librería

Este nivel es el más abstracto del track y también el que más tarda en caducar, y la razón es estructural. Lo que has aprendido aquí no es cómo funciona XState: es qué es una máquina de estado jerárquica cuando se la define con precisión suficiente para ejecutarla. XState es una encarnación de esa definición, buena y actual, pero sustituible. La definición no.

La asimetría de vidas útiles es fácil de comprobar mirando hacia atrás. En las tres décadas que separan el artículo de Harel de esta lección han pasado y desaparecido decenas de herramientas de modelado, media docena de lenguajes dominantes y varias generaciones enteras de frameworks de interfaz. Las ideas de aquel artículo —jerarquía, ortogonalidad, historia— siguen intactas, y el algoritmo que las ejecuta lleva estable desde 2015 sin una sola revisión de fondo. Apostar el tiempo de aprendizaje al nivel de la idea en lugar de al nivel de la herramienta no es purismo académico: es el cálculo con mejor rendimiento disponible en esta profesión.

// El invariante que sobrevive a cualquier API:
// una funcion total y determinista entre configuraciones estables.
type Semantica = (
  configuracion: ConjuntoDeEstados,
  evento: Evento,
) => { siguiente: ConjuntoDeEstados; acciones: Accion[] }

// Total: definida para todo par configuracion-evento, aunque el
// resultado sea quedarse donde estaba y no producir accion alguna.
// Determinista: dos invocaciones con los mismos argumentos
// devuelven exactamente lo mismo, hoy y dentro de diez anios.

Esa firma es el resumen del nivel entero. Todo lo demás —la sintaxis de setup, los nombres de los eventos automáticos, si el modelo de datos se llama datamodel o context— es superficie que cambia cada pocos años. Quien entiende la firma reconoce la misma estructura en la máquina de estados de Qt, en el reductor jerárquico que alguien escribió a mano en un proyecto legado, en la especificación de un protocolo de red descrito con diagramas, y en la librería que reemplace a XState en 2032.

Ese reconocimiento tiene un valor práctico inmediato cuando aterrizas en código ajeno. Un sistema heredado rara vez anuncia que contiene una máquina de estado, pero si encuentras un objeto que guarda un modo, un conjunto de funciones que lo cambian según reglas y una colección de comprobaciones defensivas contra combinaciones prohibidas, estás mirando una máquina implícita mal escrita. Saber qué forma debería tener te da un mapa para leerla, un vocabulario para describirla y un destino claro si algún día hay que reescribirla.

Hay una comprobación sencilla de si el nivel ha calado, y es preguntarse qué respondes ahora ante un comportamiento inesperado. Antes de este nivel, la respuesta razonable era buscar en la documentación de la librería o abrir una incidencia. Después, la respuesta es simular a mano: identificar la configuración de partida, listar las transiciones habilitadas, aplicar la regla de preempción, calcular el dominio y desplegar los conjuntos de salida y entrada. Si tu simulación coincide con lo observado, el modelo estaba mal y ya sabes dónde. Si no coincide, tienes un informe de error con un argumento formal detrás en lugar de una sospecha. Esa capacidad de arbitrar entre tu expectativa y el runtime sin depender de nadie es, en la práctica, lo que este nivel compra.