Cómo atrapar un gato con TLA +

Muchos programadores luchan cuando usan métodos formales para resolver problemas dentro de sus programas, ya que esos métodos, si bien son efectivos, pueden ser irrazonablemente complejos. Para entender por qué sucede esto, usemos el método de verificación del modelo para resolver un rompecabezas relativamente fácil:

Condiciones

Estás en un pasillo con siete puertas a un lado que conducen a siete habitaciones. Un gato se esconde en una de estas habitaciones. Tu tarea es atrapar al gato. Abrir una puerta da un paso. Si adivinas la puerta correcta, atrapas al gato. Si no adivina la puerta correcta, el gato corre a la habitación contigua.

TLA + y lógica temporal

Algunas herramientas pueden resolver problemas como este. Por ejemplo, los solucionadores SMT , que se usan con frecuencia en estos casos, usan la lógica de predicados para resolver el problema, pero eso requiere el uso de una matriz, lo cual es inconveniente para los programadores y a menudo resulta en una secuencia de acciones innecesariamente compleja. TLA + , por otro lado, usa la lógica temporal, que permite que un programa use el estado del sistema tanto en el paso actual como en el siguiente en una declaración.

CatDistr' = CatDistr \ {n} 

Esta condición indica que después de verificar detrás de la puerta N, el número de puertas donde se puede ubicar al gato, coincide con el conjunto de habitaciones de donde se extrajo N. (Si el gato estaba detrás de la puerta N, por supuesto, lo han atrapado).

En un lenguaje de programación imperativo, esto crea una nueva variable calculada a partir de la anterior.

Sobre conjuntos

La posición del gato está determinada por una variable dentro del conjunto de todas las habitaciones posibles, en lugar de una habitación específica como en un sistema de modelado de simulación. Los métodos formales de programación tienen en cuenta la pluralidad de valores posibles, en lugar del valor actual. Esto es a menudo demasiado complejo para los desarrolladores principiantes, por lo que simplificar este sistema ayudaría a esos desarrolladores a trabajar más rápidamente.

Estructura del programa en TLA +

El programa consta de declaraciones y declaraciones (predictores), que describen:

• El estado inicial
• El enlace entre estados reales
• El siguiente estado
• Un invariante que se ejecuta en todos los estados disponibles.

También puede haber predicados auxiliares (por ejemplo, parámetros) involucrados.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

En ese ejemplo:

• La primera y la última línea declaran que este es un módulo fuente.
• == significa 'igualmente por definición'.
• = significa que los valores de expresión calculados son iguales
• Doors es un conjunto constante en el archivo de configuración.
• CatDistr determina la habitación en la que se encuentra el gato.
• La variable LastDoor , que representa la última habitación marcada, lee convenientemente la salida del programa. Para modelos grandes, tales variables podrían ralentizar el flujo de trabajo del programa y aumentar el número de estados que deben analizarse. Sin embargo, en este modelo, el estado ahora contiene el historial de las puertas que se abrieron. Por lo tanto, los estados iguales creados de diferentes maneras ahora son diferentes.
• El predictor Init describe el estado inicial del programa; en este caso, todavía no se han abierto puertas.
• OpenDoor (n) describe lo que sucede cuando se abre la puerta n, ya sea que atrapaste al gato o no lo hiciste.
• El siguiente predictor existe porque TLA + no sabe en qué habitación podríamos ingresar a continuación, por lo que verificará si los invariantes son correctos en cada caso.
  
  Aquí hay una variante más clara:
  
  

   Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

  
  En este caso, el código funciona con un número fijo de habitaciones, lo que hace que el código se parametrice.
• Finalmente, la invasión CatWalk determina dónde se esconde el gato. Una violación invariable significa que el gato fue atrapado donde sea que se escondiera. Al verificar una especificación, un incumplimiento invariable es un error, pero dado que no estamos utilizando la herramienta para su propósito previsto, obtener un error en este caso significa resolver el problema.

Configuración del modelo

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Esta configuración incluye la condición inicial, el número de habitaciones, las condiciones para un cambio de estado y una prueba verificable.

Puede ejecutar este modelo desde la línea de comando usando este comando:
tlc2 -config cat.cfg cat.tla .

TLA + tiene una GUI avanzada y se inicia mediante el comando tla-toolbox . Desafortunadamente, no comprende los archivos .cfg , por lo que los parámetros del modelo deben configurarse a través del menú.

Conclusión

Crear este programa en particular fue bastante simple, pero en muchos casos, la aplicación de métodos formales requerirá modelos mucho más grandes y el uso de diversas construcciones de lenguaje. Esperamos que resolver acertijos más simples como este proporcione una manera fácil e interesante de aplicar métodos formales a los proyectos de trabajo.

• Aquí puede encontrar un programa simple para la verificación interactiva de soluciones.
• Obtenga más información sobre TLA + aquí .