Dos semáforos en verde a la vez
Un invariante es una condición que debe cumplirse en todos los estados por los que puede pasar un sistema. TLA+ es un lenguaje para describir un sistema como estados y pasos, y TLC es el programa que comprueba un invariante en todos ellos.
Un cruce tiene dos semáforos, A y B. Un técnico programa cada uno para ponerse en verde cuando está en rojo. Nadie miró qué pasa si el segundo se pone en verde mientras el primero ya lo está.
Al final de esta lección
Nota
Puedo escribir un invariante y leer el contraejemplo cuando un modelo lo rompe.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Estado | los valores de todas las variables en un instante | greenA = TRUE |
| Paso | un cambio de un estado al siguiente | |
| Especificación | la descripción de los estados iniciales y de los pasos | |
| Invariante | una condición que debe cumplirse en todos los estados | |
| Contraejemplo | la secuencia de estados que rompe el invariante | |
| TLC | el programa que recorre todos los estados de una especificación |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Un sistema son estados y pasos
Un estado es una foto de todas las variables. Un paso lleva de una foto a la siguiente.
En el cruce hay dos variables, greenA y greenB, cada una verdadera o falsa. Eso da cuatro estados posibles. El invariante que se quiere comprobar es que nunca estén las dos verdaderas.
Ejemplo: los cuatro estados del cruce
| greenA | greenB | Qué ven los coches | ¿Cumple el invariante? |
|---|---|---|---|
| FALSE | FALSE | Los dos semáforos en rojo | Sí |
| TRUE | FALSE | A pasa, B espera | Sí |
| FALSE | TRUE | B pasa, A espera | Sí |
| TRUE | TRUE | Pasan los dos y chocan | No |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Cómo se leen los signos de TLA+
| Signo | Se lee | Ejemplo |
|---|---|---|
| /\ | y | greenA /\ greenB |
| \/ | o | SetGreenA \/ SetRedA |
| ~ | no | ~greenA |
| greenA' | el valor de greenA después del paso | greenA' = TRUE |
| UNCHANGED x | x no cambia en este paso | UNCHANGED greenB |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
La especificación del cruce
---- MODULE Crossing ----
VARIABLES greenA, greenB
vars == <<greenA, greenB>>
Init == greenA = FALSE /\ greenB = FALSE
SetGreenA == greenA = FALSE /\ greenA' = TRUE /\ UNCHANGED greenB
SetGreenB == greenB = FALSE /\ greenB' = TRUE /\ UNCHANGED greenA
SetRedA == greenA /\ greenA' = FALSE /\ UNCHANGED greenB
SetRedB == greenB /\ greenB' = FALSE /\ UNCHANGED greenA
Next == SetGreenA \/ SetGreenB \/ SetRedA \/ SetRedB
Spec == Init /\ [][Next]_vars
Safe == ~(greenA /\ greenB)
NeverGreenA == ~greenA
====Crea una carpeta para la especificación
mkdir -p ~/crossingSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Escribe la especificación en un archivo
printf '%s\n' "---- MODULE Crossing ----" "VARIABLES greenA, greenB" "vars == <<greenA, greenB>>" "Init == greenA = FALSE /\ greenB = FALSE" "SetGreenA == greenA = FALSE /\ greenA' = TRUE /\ UNCHANGED greenB" "SetGreenB == greenB = FALSE /\ greenB' = TRUE /\ UNCHANGED greenA" "SetRedA == greenA /\ greenA' = FALSE /\ UNCHANGED greenB" "SetRedB == greenB /\ greenB' = FALSE /\ UNCHANGED greenA" "Next == SetGreenA \/ SetGreenB \/ SetRedA \/ SetRedB" "Spec == Init /\ [][Next]_vars" "Safe == ~(greenA /\ greenB)" "NeverGreenA == ~greenA" "====" > ~/crossing/Crossing.tlaSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Comprueba que nunca haya dos verdes
tlc ~/crossing/Crossing Safe | grep -E '^(Error|State)'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
El contraejemplo es el camino más corto
TLC recorre los estados por niveles, así que el contraejemplo que enseña es de los más cortos. Cada estado va numerado, con el nombre del paso que lo produjo.
Aquí son tres estados: los dos semáforos en rojo, A en verde, y los dos en verde. Leerlos dice qué falta: el paso que pone B en verde no mira a A.
Un error frecuente
Advertencia
Mucha gente cree que, si TLC no encuentra ningún error, el sistema funciona. Un modelo que nunca se mueve cumple cualquier invariante. Comprueba también que se llega a los estados que esperas, por ejemplo con un invariante que sabes que se rompe.
Arregla los dos pasos de poner verde
sed -i 's|^SetGreenA == |SetGreenA == greenB = FALSE /\\ |; s|^SetGreenB == |SetGreenB == greenA = FALSE /\\ |' ~/crossing/Crossing.tlaSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Comprueba de nuevo el invariante
tlc ~/crossing/Crossing Safe | grep -E 'No error|states generated'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un invariante falso demuestra que se llega
El invariante NeverGreenA dice que A nunca se pone en verde. Es falso a propósito. Si TLC lo rompe, sabes que el modelo arregla el fallo sin quedarse parado.
Es la comprobación que falta tras cada arreglo.
Comprueba que A todavía puede ponerse verde
tlc ~/crossing/Crossing NeverGreenA | grep -E '^(Error|State)'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.