[EM MANUTENÇÃO]
A verificação de modelos ( do inglês model checking ) é um processo para verificar que um dado modelo satisfaz determinada especificação. Ambos os parâmetros são passados como input ao verificador, e um de dois possíveis outputs é retornado: um ou mais contra-exemplos são apresentados (e o modelo é inválido) ou nenhum contra-exemplo é encontrado ( e o modelo é válido ). A busca por contra-exemplos é exaustiva, sendo visitados todos os estados possíveis.
Um verificador de modelos muito comum é o Spin (Simple Promela Interpreter). Desenvolvido nos anos 80 e distribuído livremente desde os 90, o Spin é um verificador de modelos escritos na linguagem Promela (duh!). Na verdade não é o próprio Spin que realiza a verificação: ele gera um ficheiro .c específico para resolver o problema em questão. É esse ficheiro que faz a verificação exaustiva do modelo. Quando um (ou mais) contra-exemplos são encontrados, é gerado um ficheiro .trail com o caminho de estados que levam ao estado problemático. Caso contrário, temos a tão desejada mensagem "errors:0".
Simular com o Spin
Antes de avançar para os exemplos e para os bonecos, comecemos por instalar o Spin. Este tutorial é para sistemas operativos OS X (para Windows e Linux também encontram facilmente por aí, mas se tiverem problemas talvez se consiga arranjar qualquer coisinha).
Para quem já usa o homebrew como packet manager, instalar o Spin é tão fácil como fazer:
Quem não usa/conhece o homebrew, deve vir aqui e tratar do assunto rapidamente. Quem preferir não o fazer ( por questões religiosas, perhaps? ), pode sempre seguir as instruções do site do Spin.
Instalado o Spin, vamos brincar um bocado com ele. Para alem de verificar modelos, o Spin pode também funcionar como um simples simulador, que é o que vamos começar por fazer. Temos de começar por ir até à pasta onde está o executável do Spin. Se instalaram com o homebrew, é fácil encontrá-lo.
Vamos simular os dois exemplos seguintes, bastante simples.
Pela lógica a que estamos habituados, ambos os exemplos deveriam dar erro,
A verificação de modelos ( do inglês model checking ) é um processo para verificar que um dado modelo satisfaz determinada especificação. Ambos os parâmetros são passados como input ao verificador, e um de dois possíveis outputs é retornado: um ou mais contra-exemplos são apresentados (e o modelo é inválido) ou nenhum contra-exemplo é encontrado ( e o modelo é válido ). A busca por contra-exemplos é exaustiva, sendo visitados todos os estados possíveis.
Um verificador de modelos muito comum é o Spin (Simple Promela Interpreter). Desenvolvido nos anos 80 e distribuído livremente desde os 90, o Spin é um verificador de modelos escritos na linguagem Promela (duh!). Na verdade não é o próprio Spin que realiza a verificação: ele gera um ficheiro .c específico para resolver o problema em questão. É esse ficheiro que faz a verificação exaustiva do modelo. Quando um (ou mais) contra-exemplos são encontrados, é gerado um ficheiro .trail com o caminho de estados que levam ao estado problemático. Caso contrário, temos a tão desejada mensagem "errors:0".
Simular com o Spin
Antes de avançar para os exemplos e para os bonecos, comecemos por instalar o Spin. Este tutorial é para sistemas operativos OS X (para Windows e Linux também encontram facilmente por aí, mas se tiverem problemas talvez se consiga arranjar qualquer coisinha).
Para quem já usa o homebrew como packet manager, instalar o Spin é tão fácil como fazer:
~$brew install spin
Quem não usa/conhece o homebrew, deve vir aqui e tratar do assunto rapidamente. Quem preferir não o fazer ( por questões religiosas, perhaps? ), pode sempre seguir as instruções do site do Spin.
Instalado o Spin, vamos brincar um bocado com ele. Para alem de verificar modelos, o Spin pode também funcionar como um simples simulador, que é o que vamos começar por fazer. Temos de começar por ir até à pasta onde está o executável do Spin. Se instalaram com o homebrew, é fácil encontrá-lo.
~$brew info spin spin: stable 6.4.5 (bottled) The efficient verification tool of multi-threaded software https://spinroot.com/spin/whatispin.html //usr/local/Cellar/spin/6.4.5 (12 files, 1.5M) Poured from bottle From: https://github.com/Homebrew/homebrew-core/blob/master/Formula/spin.rb ~$cd /usr/local/Cellar/spin/6.4.5/bin
Vamos simular os dois exemplos seguintes, bastante simples.
active proctype Exemplo() { int a = 13, b = 31,c; c = b-a; assert( c == 17) }
~$spin example.pml spin: example.pml:5, Error: assertion violated spin: text of failed assertion: assert((c==17)) #processes: 1 2: proc 0 (Exemplo:1) example.pml:5 (state 2) 1 process created
Pela lógica a que estamos habituados, ambos os exemplos deveriam dar erro,
