Seguir aprendiendo: Harel, SCXML, model checking y lo que viene

Hay una asimetría entre lo que dura una librería y lo que dura una idea que conviene tener presente al decidir en qué invertir horas de estudio. El artículo en el que Harel definió los statecharts se publicó en 1987 y se lee hoy sin adaptación ninguna; el modelo de actores es de 1973 y describe con precisión lo que hace un sistema de mensajería moderno; los autómatas finitos son de los años cincuenta y siguen siendo el objeto sobre el que se construye todo lo demás. En ese mismo periodo han nacido y muerto varias decenas de bibliotecas de gestión de estado, algunas dominantes durante años. La conclusión práctica no es despreciar las herramientas —hay que usarlas y usarlas bien— sino repartir el estudio con conocimiento de causa: lo que se aprende de la API caduca, lo que se aprende del formalismo no. Esta lección es el mapa de lo que no caduca, y de las tres direcciones por donde este campo se está moviendo ahora mismo.

Las fuentes primarias que siguen valiendo el tiempo

No hay que leerlo todo y desde luego no en este orden por obligación. La lista siguiente está ordenada por lo que resuelve cada texto, para que se pueda ir a buscar la respuesta concreta.

Si quieres entender de dónde salieron los statecharts y por qué tienen esa forma, la fuente es David Harel, Statecharts: A Visual Formalism for Complex Systems, en Science of Computer Programming, volumen 8, 1987. Es un artículo escrito para ingenieros de sistemas aeronáuticos, no para académicos, y ese origen se nota: cada construcción se justifica con un problema real que la notación plana no podía expresar sin explotar. Se lee en una tarde y reordena la cabeza.

Si lo que te interesa es el orden exacto en que ocurren las cosas, hay que ir a Harel y Naamad, The STATEMATE Semantics of Statecharts, en ACM TOSEM, 1996. Ahí es donde la notación deja de ser un dibujo y se convierte en un objeto ejecutable con reglas: qué estados se abandonan, en qué orden, cuándo se ejecutan las acciones y qué significa que dos transiciones compitan.

Si alguna vez discutes con alguien sobre qué hace un statechart en un caso raro, el texto que zanja la discusión —revelando que no hay una única respuesta— es Michael von der Beeck, A Comparison of Statecharts Variants, de 1994, que cataloga más de veinte variantes con semánticas distintas e incompatibles entre sí. La lección es incómoda y liberadora: statechart es una familia de notaciones, no una especificación, y por eso hace falta una norma.

Para el modelo de actores, la fuente es Hewitt, Bishop y Steiger, en IJCAI 1973, y sobre todo el libro de Gul Agha, Actors: A Model of Concurrent Computation in Distributed Systems, de 1986, que es donde el modelo adquiere su forma matemática. Para la teoría de autómatas, Hopcroft, Motwani y Ullman es la referencia canónica y Sipser es la puerta de entrada más amable. Y para saber qué hizo Harel después, su libro Come, Let’s Play de 2003 propone especificar por escenarios en lugar de por estados, que es la crítica más seria que se le ha hecho al propio formalismo desde dentro.

La norma y por qué existe

SCXML es Recomendación del W3C desde el 1 de septiembre de 2015, y su valor no está en el formato XML —que casi nadie escribe a mano— sino en su apéndice algorítmico: un pseudocódigo normativo que define paso a paso cómo se interpreta un statechart. Ahí quedan fijados el conjunto de estados que se abandonan y el que se entra, el orden documental para las acciones de entrada y el inverso para las de salida, el bucle de microsteps hasta alcanzar una configuración estable, y la regla que resuelve dos transiciones en conflicto a favor de la declarada en el estado más profundo.

Su utilidad práctica es la de cualquier norma: convierte una discusión de opiniones en una consulta. Cuando dos personas del equipo no se ponen de acuerdo sobre si una acción de salida debe ejecutarse antes que una de entrada, existe una respuesta normativa que no depende de la librería que uses. XState sigue esa semántica de cerca, y conocer el algoritmo permite predecir el comportamiento en los casos límite sin experimentar a base de pruebas.

Conviene saber que no es el único estándar. Las máquinas de estado de UML, definidas en la especificación de UML 2.5, cubren un territorio parecido con diferencias reales en los detalles —el tratamiento de los eventos diferidos, la semántica de los pseudoestados de unión y bifurcación— y son las que se encuentran en herramientas de modelado empresarial y en dominios regulados. Y hay implementaciones industriales vivas de SCXML fuera del mundo web, desde Apache Commons SCXML hasta el módulo de Qt, lo que significa que un modelo escrito con esta disciplina puede viajar entre plataformas mucho más lejos de lo que uno supondría.

La escalera de la verificación

Entre la prueba unitaria y la demostración formal hay cuatro peldaños, y la elección correcta casi nunca es el más alto.

flowchart TD
A[1 test de transicion: casos que se te ocurren] --> B[2 recorrido exhaustivo del grafo]
B --> C[3 propiedades: invariantes sobre entradas generadas]
C --> D[4 model checking: logica temporal sobre todos los entrelazados]
A --> E[coste minutos]
B --> F[coste horas]
C --> G[coste dias]
D --> H[coste semanas y formacion]
style B fill:#a6e3a1,color:#11111b
style D fill:#cba6f7,color:#11111b

El peldaño dos es el que casi nadie usa y el que mejor relación de coste tiene. Si la máquina es finita y su contexto está acotado, un recorrido exhaustivo del grafo es un model checker de andar por casa: enumera todos los caminos y comprueba invariantes en cada uno. Con eso ya se demuestran propiedades reales —que ningún camino llega a un estado sin salida, que no existe secuencia que cobre dos veces— sin aprender ninguna herramienta nueva.

// Un model checker de veinte lineas: todos los caminos, un invariante.
import { getSimplePaths } from '@xstate/graph'
import { cobro } from './cobro'

const caminos = getSimplePaths(cobro, {
  events: [{ type: 'PAGAR' }, { type: 'CANCELAR' }, { type: 'CADUCA' }],
})

for (const camino of caminos) {
  // Seguridad: en ningun camino se cobra dos veces.
  const cobros = camino.steps.filter((s) => s.state.matches('cobrando')).length
  const exitos = camino.steps.filter((s) => s.state.matches('hecho')).length
  if (exitos > 0 && cobros > 1) {
    throw new Error(`Camino inseguro: ${camino.steps.map((s) => s.event.type).join(' ')}`)
  }
  // Ausencia de agujeros negros: todo final del camino sale o es final.
  const ultimo = camino.state
  if (!ultimo.status.includes('done') && ultimo.can({ type: 'PAGAR' }) === false) {
    console.warn('Estado sin salida alcanzable', ultimo.value)
  }
}

La razón por la que este peldaño se salta tan a menudo es puramente cultural: se percibe como testing exótico cuando es lo contrario, un bucle sobre una lista. Merece la pena instalarlo en el proceso de integración continua desde el primer día, porque su valor crece justo cuando más falta hace: cada estado nuevo que alguien añade multiplica los caminos, y es exactamente entonces cuando el recorrido exhaustivo encuentra lo que nadie iba a probar a mano.

El peldaño cuatro empieza a justificarse cuando varias máquinas se coordinan y el fallo cuesta dinero o seguridad, porque ahí el problema deja de ser el grafo de una máquina y pasa a ser el entrelazado de varias. La lógica temporal, que Pnueli introdujo en 1977 para razonar sobre programas, distingue dos familias de propiedades que conviene saber nombrar. Las de seguridad dicen que algo malo no ocurre nunca: nunca se cobra dos veces, nunca se entrega sin haber cobrado. Las de viveza dicen que algo bueno acaba ocurriendo: toda solicitud acaba resuelta, ningún reembolso queda pendiente para siempre. Los tests corrientes cubren razonablemente las primeras y son casi ciegos a las segundas, porque una propiedad de viveza se viola con una ejecución infinita que ninguna prueba concreta recorre.

Las herramientas del último peldaño son estables y bien documentadas: TLA+ con su verificador TLC, que Lamport describió en Specifying Systems, es el estándar de facto para protocolos distribuidos y su uso industrial está documentado en el artículo de Newcombe y otros sobre métodos formales en Amazon Web Services, publicado en CACM en 2015. SPIN con Promela y NuSMV son las alternativas clásicas del mundo académico e industrial. Todas chocan contra el mismo muro —la explosión del espacio de estados— y todas lo esquivan con las mismas dos familias de trucos: métodos simbólicos y verificación acotada.

Hacia dónde va el modelado de estado

La primera línea merece un apunte porque es la que hoy tiene el hueco más visible. Un statechart en memoria muere con su proceso, y buena parte de los procesos de negocio duran días o semanas: una devolución, una contratación, una verificación de identidad. Los motores de ejecución durable resuelven la persistencia y la reanudación pero ofrecen un modelo de comportamiento pobre, normalmente código secuencial con puntos de guardado; los statecharts ofrecen el modelo y no la durabilidad. La convergencia entre ambos —un grafo revisable cuya configuración se persiste y se reanuda— es un espacio de diseño todavía abierto, y quien sepa modelar bien va a encontrarlo cómodo cuando madure.

De las cuatro, la tercera es la que más conviene interiorizar porque cambia el valor relativo de las habilidades. Durante décadas el cuello de botella fue producir código; en esa economía, una especificación formal era un coste añadido que había que justificar. Cuando el código se genera barato, el cuello de botella se desplaza a decidir qué debe hacer el sistema y a comprobar que lo generado lo hace. Un statechart pequeño, con nombres de dominio y sin celdas vacías, es exactamente el artefacto que sirve para las dos cosas: es lo bastante formal para generar desde él y lo bastante legible para que una persona lo apruebe. La habilidad que sube de precio no es escribir la máquina, es saber cuál es la máquina correcta.