Pegue um gato com TLA +

Os métodos formais são considerados uma maneira eficaz, mas excessivamente complexa, de garantir a confiabilidade do software. As ferramentas usadas para isso diferem significativamente daquelas familiares ao programador. Este artigo foi escrito com o objetivo de diminuir o limite para a inserção deste kit de ferramentas. Usarei o sistema de verificação de modelos não para resolver tarefas difíceis de serem especificadas na especificação de software, mas para resolver um quebra-cabeça compreensível até para crianças em idade escolar.

Você está em um corredor direto com sete quartos de um lado. Em um deles é um gato. Em uma etapa, você pode olhar para um dos quartos, se houver um gato, ele será pego. Assim que a porta se fechar, o gato passará para uma das salas vizinhas àquela em que estava. A tarefa é pegar o gato.

TLA + e lógica temporal

Existem muitas ferramentas que podem resolver esses problemas. Freqüentemente, nesses casos, os solucionadores SMT são usados. Como regra, esses sistemas usam a lógica predicada usual e expressar a sequência de ações é bastante complicado (você precisa usar algo como uma matriz, o que não é muito conveniente para se trabalhar). O TLA + usa a lógica temporal, que permite usar o estado do sistema em uma instrução na etapa atual e na próxima.

CatDistr' = CatDistr \ {n} 

Essa condição indica que o conjunto de salas em que o gato pode ser localizado após verificar a sala n coincide com o conjunto de salas de onde n foi tirado (se o gato estava lá, ele é pego e não há mais nada a fazer).

Nas linguagens de programação imperativas, isso corresponde aproximadamente à atribuição de uma variável a um novo valor, calculado a partir do antigo.

Um pouco sobre conjuntos

Como você entende, a posição do gato é modelada por uma variável com o conjunto de todas as salas possíveis, e não uma sala específica, como seria em um sistema de simulação. Usar o conjunto de valores possíveis em vez de um valor específico é uma técnica frequentemente usada em métodos formais, o que causa dificuldade para programadores iniciantes. Portanto, escolhi uma tarefa em que o uso de conjuntos é apropriado.

Estrutura do programa no TLA +

No caso mais simples, o programa consiste em declarações e instruções (predicados) descrevendo o estado inicial, o relacionamento entre o estado atual e o próximo e a invariante que deve ser executada em todos os estados disponíveis. Predicados auxiliares também podem estar presentes. Predicados podem ser parametrizados.

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

A primeira e a última linha são os recursos de sintaxe da declaração do módulo.

== significa "igual por definição", enquanto um único = é exatamente a igualdade dos valores calculados das expressões.

Doors é uma constante do modelo, precisará ser configurada no arquivo de configuração.
CatDistr - a distribuição do gato nos quartos.

A variável LastDoor, a última sala verificada, é inserida para facilitar a leitura do resultado do programa. Para modelos grandes, essas variáveis ​​podem desacelerar significativamente o programa aumentando o número de estados analisados ​​(já que o estado agora contém um histórico de como surgiu e os mesmos estados criados de maneiras diferentes agora serão diferentes).

O predicado Init descreve o estado inicial (0..Portas é o conjunto de todas as salas). OpenDoor (n) descreve o que acontece quando você abre a porta do quarto n (no pior dos casos, o gato não está lá - caso contrário, nós o pegamos).

O predicado Next parece um pouco estranho - há um espaço para analisar. O fato é que a existência de algo significa que o TLA + não sabe em qual sala examinaremos; portanto, ele verificará a exatidão do invariante em todos os casos.

Seria mais claro escrever

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

mas nosso código funcionará apenas com um número fixo de salas, e é melhor torná-lo parametrizado.

Finalmente, o invariante CatWalk é um monte de salas onde o gato pode não estar vazio. A violação do invariante significa que o gato foi pego, onde quer que estivesse originalmente. Ao verificar a especificação, a violação da invariável significa um erro, mas não estamos usando a ferramenta para a finalidade a que se destina e o “erro” encontrado significa resolver o problema.

Configuração do modelo

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Tudo é simples aqui - indicamos o número de quartos, as condições iniciais, as condições para a mudança de estado e a invariante em teste.

O modelo é iniciado a partir da linha de comandos tlc2 -config cat.cfg cat.tla .

O TLA + tem uma GUI avançada lançada pela equipe tla-toolbox. Infelizmente, ele não entende os arquivos .cfg e os parâmetros do modelo que precisam ser configurados através do menu.

Conclusão

Nesta tarefa, tudo acabou bem simples. Certamente, casos praticamente significativos de aplicação de métodos formais exigirão modelos muito mais volumosos e o uso de várias construções de linguagem. Mas espero que resolver tais quebra-cabeças forneça uma maneira simples e não chata de introduzir métodos formais em projetos de trabalho.

→ A tarefa foi encontrada aqui

Por precaução, um programa simples para verificação interativa de soluções . Materiais para o estudo do TLA + . Outro sistema de verificação de modelos, o Alloy, é descrito aqui .