Tutorial de Spin e jSpin ( instalação em Mac OS X )

[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:

~$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,

Read More

Complexidade de Algoritmos

Para todo o problema há uma solução, não é o que se diz? Assim sendo, porquê preocuparmo-nos tanto? Existem até, em muitos casos, várias soluções para o mesmo problema. E para esses casos será acertado dizermos: para toda a solução há um problema. Vendo as coisas desta maneira, diria que quanto mais soluções existirem, mais difícil é resolver o problema, afinal, qual a melhor solução a escolher?

Um caso tão geral como o anterior que podemos particularizar para o mundo da programação e da algoritmia. São diversos os problemas com que nos deparamos e também várias as maneiras que temos de os resolver. Se pretendemos pesquisar informação o que será melhor, sequential search, binary search ou outro? E se quisermos calcular o caminho mais curto entre dois pontos, será mais vantajoso recorrer ao algoritmo de Djikstra ou ao algoritmo de Bellman-Ford?

Porquê que é que existem tantos algoritmos para um mesmo problema, porque não definir um algoritmo padrão e aplicar sempre o mesmo? Acontece que na área da informática (e não só, mas é o que nos interessa aqui) a performance é muito importante, e bons programadores e engenheiros não se preocupam apenas com a validade de um algoritmo, mas também a sua rapidez de execução e a sua eficiência na utilização dos recursos do computador. Assim sendo, a eficiência de um algoritmo deve ser medida tanto em termos temporais como em termos espaciais. Posto tudo isto, podemos definir a complexidade de um algoritmo como a medida de tempo - complexidade temporal - ou espaço em memória - complexidade espacial - requerida pelo algoritmo em questão para um input de tamanho (n).

The Big O Notation

Uma boa questão que poderíamos colocar por esta altura: será a medida do tempo de execução uma das variáveis mais importantes a ter em conta aquando da escolha do algoritmo, estando ele tão dependente de factores externos? Sim, é verdade, o tempo de execução de um algoritmo para o mesmo input de tamanho (n) depende não só da estrutura do código mas também da rapidez do processador, da rapidez do disco, o tipo de compilador, etc. Desse modo, deve-se estimar a eficiência de um algoritmo assimptoticamente, medindo o tempo T(n) como o número de passos elementares realizados, onde cada passo leva um tempo constante a correr. FIX ME!

A complexidade de um algoritmo passa agora a ser expressa pela notação O-grande (big O notation), uma medida da ordem de grandeza da função para inputs grandes ( (n) grande, daí ser assimptótico ).

Por ser uma notação que lida com n grande (assimptótica), a complexidade de uma função O(n + c), onde c é uma constante, é a mesma que O(n), pois considera-se o termo da função que mais rapidamente cresce, isto é, o que tem a maior ordem de grandeza). Pela mesma razão se considera O(cn) igual a O(n); ambas possuem o mesmo ritmo de crescimento e para n infinitamente grande terão a mesma ordem de grandeza.

No gráfico abaixo representado encontram-se traçadas as principais ordens de complexidade algorítmica de onde podemos discernir claramente a taxa de crescimento de cada uma.
                      

Definição

       f(n) é O(g(n)) se existirem valores c e N0 tais que f(n)≤cg(n) para todo o n≥N0

Intuitivamente, a função f(n) não cresce mais que a função cg(n), com c > 0, a partir de um dado valor N0 > 0, para um n a tender para o infinitamente grande. Graficamente:

Melhor Caso, Pior Caso e Caso Médio

Voltando a olhar para os exemplos apresentados acima sobre análise de complexidade podemos perguntar-nos: e se não forem percorridas n iterações (por exemplo, pela existência de uma condição que o justifique)? A complexidade passaria a ser outra diferente? Por norma a complexidade de um algoritmo é referente ao seu pior caso (worst case) - quando o algoritmo tem de fazer o maior número de operações possível -, mas pode ser útil conhecer os seus comportamentos e complexidade para casos mais simples.

Temos exactamente o oposto, isto é, quando o algoritmo tem de fazer o mínimo de operações, que é chamado o melhor caso(best case). Acontece, por exemplo, quando queremos pesquisar a ocorrência de um número num dado input e ele ser logo o primeiro elemento.

No meio temos ainda o caso médio(average case), onde o número de operações difere para cada execução. É por isso o mais difícil de determinar dos três casos por estar dependente de uma maior quantidade de testes e de uma posterior análise estatística para determinar o número médio de operações efectuadas pelo algoritmo.


Um Caso Prático

Vamos pegar numa operação tão comum como o ordenamento de dados, utilizando um dos algoritmos mais simples de implementar, o Insertion Sort, para ilustrar como cada tipo de input influencia o tempo de execução e a correspondente complexidade para cada caso.

Foram usados inputs de 100 000 elementos e os resultados, em milissegundos, estão apresentados na tabela abaixo; o melhor caso corresponde a um array ordenado, o pior caso a um array ordenado ao contrário (do maior para o menor) e o caso médio à média de vários arrays com os elementos aleatórios.

Para os mesmos inputs corremos o algoritmo de ordenamento QuickSort, e estes foram os resultados:

Através desta análise experimental mostramos que não podemos só depender da complexidade O(n) de um algoritmo para determinar se é o melhor a usar ou não. Apesar do Quicksort apresentar uma complexidade O(nlog(n)), inferior à O(n2) do Insertion, vimos que claramente há situações específicas em que o Insertion seria uma melhor aposta. É por estas mesmas razões que várias optimizações de algoritmos consistem em utilizar um algoritmo auxiliar quando detectamos que o input é de um determinado tipo mais favorável a esse mesmo auxiliar. 

  

Teste

 

Se achas que percebeste, não terás problemas em descobrir a complexidade nos seguintes casos: 

                  

                               O(log(n))

                                                                   

O(nlog(n))

                                    

Read More

Algoritmos de Ordenamento #1 QuickSort

Desenvolvido em 1962 por Tony Hoare, o quicksort é um dos métodos de ordenamento mais rápidos e eficientes quando comparado com outros algoritmos de complexidade O(n*log(n)). No pior dos casos a complexidade sobe para O(n² ) mas isso é bastante raro e actualmente o quicksort destaca-se como um dos melhores algoritmos de ordenamento.

O ALGORITMO

1. Escolher um elemento do array de entrada para ser o pivot. A maneira mais simples seria utilizar o elemento que está no meio do array. Apesar de não estar errada, é uma opção que por vezes está na origem do aumento da complexidade do algoritmo (já deu para perceber que pivot e complexidade estão relacionados aqui, right?). Uma melhor opção seria a mediana entre o valor central e os valores extremos do array, como exemplificamos mais abaixo. 

2. Reordenar o array de modo a que a parte esquerda seja apenas composta por elementos menores que o pivot  e a parte direita por elementos maiores que o pivot. No fim deste processo de partição temos um array reordenado onde o pivot se encontra rodeado em ambos os lados por uma sub-lista não ordenada. 

3. De forma recursiva ir dividindo sucessivamente cada uma das sub-listas e aplicar as operações acima descritas (encontrar o pivot e fazer a partição) a cada nova sub-lista que vai surgindo. No final teremos uma sequência ordenada por ordem crescente. 

 

 ALGORITMO DE PARTIÇÃO

A operação de partição é crucial no quicksort, assim sendo, é importante aplicar um algoritmo rápido e eficiente.  Aqui abordamos o chamado Algoritmo de Partição de Hoare com algumas optimizações acrescentadas. Para além de eficiente, é um algoritmo relativamente fácil de compreender e de implementar. A acompanhar os passos do algoritmo vai um exemplo baseado no array de entrada da figura anterior. 

1.  A função de partição recebe três argumentos: o array de entrada e os indíces que delimitam a sub-lista desse array a que será aplicada a partição. O indíce inferior será denominado por left e o superior por right. A sub-lista será identificada como A. O primeiro passo será encontrar o pivot para essa sub-lista e, posteriormente, trocá-lo com o elemento que está na última posição ( A[right] ). Deverão ser declaradas duas variáveis auxiliares: uma variável i para percorrer A da esquerda para direita e uma variável j para percorrer a sub-lista no sentido contrário.

2. Enquanto A[i] < pivot, o i é incrementado, parando quando essa condição se deixa de verificar. Por outro lado, o j é decrementado enquanto A[j] > pivot. Quando ambas as condições se deixarem de verificar, e se i e j ainda não se tiverem cruzado, trocamos os dois elementos. Caso i>= j, a sub-lista já está reordenada, por isso voltamos a colocar o pivot no sítio certo e retornamos o indíce i em que parámos.

3. Temos então duas sub-listas que, apesar de já terem sofrido partição, não estão ainda ordenadas por ordem crescente, que é o objectivo do quicksort. Tal objectivo será alcançado através das inúmeras divisões que vamos fazendo ao array inicial, como já foi explicado em cima, aplicando este método de partição a cada nova sub-lista. A divisão é sempre feita no índice onde ficou o pivot - por isso é que retornamos a variável i no fim de toda a partição feita. Por cada divisão que fazemos são duas novas partições que temos de fazer: uma para a sub-lista que vai de A[0] a A[i-1] e outra para a sub-lista que vai de A[i+1] a A[len(A)].



PSEUDO-CÓDIGO

Read More