ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair

Resumo Técnico: ModelWisdom

1. O Problema

A verificação de modelos em TLA+ (Temporal Logic of Actions) oferece garantias robustas de correção, mas os praticantes enfrentam desafios significativos na interpretação dos resultados. As principais dificuldades incluem:

• Interpretação de Contraintuitivos: Os gráficos de transição de estado gerados pelos verificadores (como o TLC) são frequentemente grandes, complexos e difíceis de navegar.
• Falta de Explicabilidade: A saída bruta do verificador carece de explicações semânticas. Os usuários precisam rastrear manualmente as violações de volta para o código-fonte e conectar estados violadores às propriedades temporais quebradas.
• Limitações das Ferramentas Atuais: A "TLA+ Toolbox" possui um visualizador de diagramas de estado, mas ele é estático, exibe o gráfico totalmente expandido (sem dobragem de nós/arestas), não possui destaque de cor para violações e não oferece explicações semânticas. Isso limita a escalabilidade e a usabilidade em modelos não triviais.

2. Metodologia

O ModelWisdom é um ambiente interativo que integra visualização de gráficos, otimização estrutural e Modelos de Linguagem Grandes (LLMs) para tornar o processo de verificação de TLA+ mais interpretável e acionável. A ferramenta é composta por duas partes principais: um aplicativo web e um servidor que executa o verificador TLC.

A abordagem metodológica baseia-se em quatro pilares interconectados:

1. Visualização e Mapeamento Semântico: Integração direta entre o gráfico de estado e o código TLA+.
2. Otimização de Performance: Técnicas de renderização preguiçosa (lazy rendering) e estruturas hierárquicas para lidar com grandes volumes de dados.
3. Digestão via LLM: Uso de LLMs (como GPT-4 e Claude 3.7 Sonnet) para resumir e explicar subgrafos e o modelo como um todo.
4. Reparo Iterativo: Um ciclo de feedback automatizado onde o LLM analisa erros e propõe correções no código.

3. Principais Contribuições

O artigo apresenta quatro funcionalidades centrais do ModelWisdom:

• A. Visualização de Modelos e Explicabilidade:

  • Destaque de Violação: Nós que violam propriedades são coloridos distintamente.
  • Navegação Click-through: Links clicáveis nas transições que levam diretamente às linhas correspondentes do código TLA+.
  • Mapeamento Direto: Conexão explícita entre estados violadores e as propriedades temporais específicas que foram quebradas.

• B. Otimização Orientada a Performance:

  • Estrutura em Árvore: Layouts hierárquicos para clareza.
  • Dobragem (Folding): Capacidade de dobrar nós e arestas para reduzir o ruído visual e focar em caminhos relevantes.
  • Renderização sob Demanda: Apenas as partes do gráfico com as quais o usuário interage são geradas e renderizadas, permitindo a exploração de modelos massivos.

• C. Digestão de Modelos (Model Digest):

  • Resumo Automático: Antes de enviar ao LLM, a ferramenta extrai informações estruturais chave (estados iniciais/finais, ciclos, transições frequentes).
  • Explicação Semântica: O LLM gera explicações em linguagem natural sobre a estrutura do modelo, variáveis de estado, constantes, ações e invariantes, traduzindo a lógica formal para texto compreensível.

• D. Assistência de Reparo de Modelos (Model Repair):

  • Extração Estruturada de Erros: O sistema captura mensagens de erro do TLC e as prepara para o LLM.
  • Fluxos de Reparo: Suporta modos de "reparo único" (one-shot) e "reparo iterativo" (multi-pass), onde o sistema alterna entre o LLM e o verificador TLC até que o erro seja resolvido ou um limite seja atingido.
  • Histórico de Depuração: Um painel registra cada tentativa de reparo, permitindo que o usuário rastreie a evolução do modelo e entenda as mudanças propostas.

4. Resultados e Demonstração

O sistema foi implementado com aproximadamente 7.000 linhas de código (TypeScript e Python) e está disponível publicamente.

• Caso de Uso (CoffeeCan): O artigo demonstra a ferramenta usando o exemplo oficial "CoffeeCan" do TLA+.
  • Foi possível visualizar a árvore de estados incrementalmente.
  • Ao modificar propositalmente uma condição pós (de -2 para -1), o sistema destacou o estado violado, explicou a violação e, através do módulo ModelRepair, corrigiu automaticamente o erro no código, revertendo a alteração para o valor correto.
  • O módulo ModelDigest forneceu uma explicação natural detalhada das ações do modelo (ex: remover feijões pretos e adicionar um de volta) baseada no estado inicial e final.

5. Significado e Impacto

O ModelWisdom representa um avanço significativo na adoção industrial da verificação formal ao abordar a barreira cognitiva da interpretação de resultados.

• Ponte entre Formalismo e Intuição: Ao combinar visualização interativa com a capacidade explicativa dos LLMs, a ferramenta transforma saídas brutas e complexas em fluxos de trabalho interativos e compreensíveis.
• Redução de Esforço: Diminui drasticamente o tempo necessário para depurar especificações complexas, automatizando a identificação de erros e a geração de correções.
• Escalabilidade: As técnicas de otimização gráfica permitem analisar modelos que seriam intratáveis visualmente nas ferramentas atuais.
• Futuro: A arquitetura é projetada para ser generalizável, com planos futuros de estender o suporte para outras linguagens de verificação (como Promela, Alloy, NuSMV), criando um ambiente agnóstico à linguagem para assistência de verificação formal.

Em suma, o ModelWisdom não é apenas um visualizador, mas um assistente de depuração inteligente que integra a precisão da verificação formal com a usabilidade moderna impulsionada por IA.