Como pegar um gato com TLA +

Muitos programadores enfrentam dificuldades ao usar métodos formais para resolver problemas em seus programas, pois esses métodos, embora eficazes, podem ser excessivamente complexos. Para entender por que isso acontece, vamos usar o método de verificação de modelo para resolver um quebra-cabeça relativamente fácil:

Condições

Você está em um corredor com sete portas de um lado, levando a sete quartos. Um gato está escondido em uma dessas salas. Sua tarefa é pegar o gato. Abrir uma porta dá um passo. Se você adivinhar a porta correta, você pega o gato. Se você não adivinhar a porta correta, o gato corre para a próxima sala.

TLA + e lógica temporal

Algumas ferramentas podem resolver problemas como este. Por exemplo, os solucionadores SMT , que são usados ​​com frequência nesses casos, usam lógica de predicado para resolver o problema, mas isso requer o uso de uma matriz, o que é inconveniente para programadores e geralmente resulta em uma sequência de ações desnecessariamente complexa. O TLA + , por outro lado, usa a lógica temporal, que permite que um programa use o estado do sistema na etapa atual e na próxima etapa de uma instrução.

CatDistr' = CatDistr \ {n} 

Esta condição afirma que, depois de verificar atrás da porta N, o número de portas onde o gato pode ser localizado coincide com o conjunto de salas de onde N foi retirado. (Se o gato estava atrás da porta N, é claro, ele foi pego.)

Em uma linguagem de programação imperativa, isso cria uma nova variável calculada a partir da antiga.

Sobre conjuntos

A posição do gato é determinada por uma variável dentro do conjunto de todas as salas possíveis, em vez de uma sala específica, como em um sistema de modelagem de simulação. Os métodos formais de programação levam em consideração a pluralidade de valores possíveis, em vez do valor atual. Isso geralmente é muito complexo para desenvolvedores iniciantes, portanto, simplificar esse sistema ajudaria esses desenvolvedores a trabalhar mais rapidamente.

Estrutura do programa em TLA +

O programa consiste em declarações e declarações (preditores), que descrevem:

• O estado inicial
• O link entre estados reais
• O próximo estado
• Um invariante que é executado em todos os estados disponíveis.

Também pode haver predicados auxiliares (por exemplo, parâmetros) envolvidos.

 ---- 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 /= {} ============================================================================= 

Nesse exemplo:

• A primeira e a última linha declaram que este é um módulo de origem.
• == significa 'igualmente por definição'.
• = significa que os valores calculados da expressão são iguais
• Doors é um conjunto constante no arquivo de configuração.
• CatDistr determina a sala em que o gato está localizado.
• A variável LastDoor , que representa a última sala verificada, lê convenientemente a saída do programa. Para modelos grandes, essas variáveis ​​podem diminuir o fluxo de trabalho do programa e aumentar o número de estados que precisam ser analisados. Nesse modelo, no entanto, o estado agora contém o histórico de quais portas foram abertas. Assim, estados iguais criados de maneiras diferentes agora são diferentes.
• O preditor de Init descreve o estado inicial do programa - nesse caso, nenhuma porta foi aberta ainda.
• OpenDoor (n) descreve o que acontece quando a porta n é aberta - você pegou o gato ou não.
• O preditivo Next existe porque o TLA + não sabe em qual sala poderemos entrar a seguir, portanto, ele verificará se os invariantes estão corretos em cada caso.
  
  Aqui está uma variante mais clara:
  
  

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

  
  Nesse caso, o código funciona com um número fixo de salas, tornando o código parametrizado.
• Por fim, o invariante CatWalk determina onde o gato está escondido. Uma violação invariável significa que o gato foi pego onde quer que ele se escondesse. Ao verificar uma especificação, uma violação invariável é um erro, mas como não estamos usando a ferramenta para a finalidade a que se destina, obter um erro nesse caso significa resolver o problema.

Configuração do modelo

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Essa configuração inclui a condição inicial, o número de salas, as condições para uma mudança de estado e um teste verificável.

Você pode executar este modelo na linha de comando usando este comando:
tlc2 -config cat.cfg cat.tla .

O TLA + possui uma GUI avançada e é iniciado pelo comando tla-toolbox . Infelizmente, ele não entende os arquivos .cfg , portanto os parâmetros do modelo devem ser configurados através do menu.

Conclusão

A criação deste programa em particular foi bastante simples, mas em muitos casos, a aplicação de métodos formais exigirá modelos muito maiores e o uso de várias construções de linguagem. Esperamos que resolver quebra-cabeças mais simples como esse forneça uma maneira fácil e interessante de aplicar métodos formais nos projetos de trabalho.

• Um programa simples para verificação interativa de soluções pode ser encontrado aqui .
• Saiba mais sobre o TLA + aqui .