As APN são utilizadas essencialmente para fins de simulação de sistemas concorrentes e são a base de outros formalismos mais complexos, como o CO-OPN sobre o qual a linguagem SATEL foi desenvolvida. Por este motivo utilizar as APN nesta disserta- ção é um primeiro passo para se poder estender a abordagem a outros formalismos
3. TRABALHO RELACIONADO 3.1. APN - Redes de Petri algébricas
mais sofisticados, tendo-se em conta que para este trabalho o objectivo maior é fazer prova de conceito sobre as potencialidades da SATEL, fornecendo-lhe uma possível semântica operacional.
3.1.1.1 Tipos de dados algébricos (ADT)
As Redes de Petri Algébricas, como já referido, recorrem-se de tipos de dados algébri- cos para representar os seus tokens e para poder expressar condições sobre as transi- ções.
Os ADT são formalismos que permitem descrever tipos de dados de uma forma totalmente abstracta. São definidos através de uma assinatura que contém a definição das operações e geradores e por um conjunto de axiomas, que podem incluir formu- las algébricas e teoremas. São um formalismo muito útil para representar estruturas de dados porque com ele se define não só a sintaxe do tipo de dados, como também se consegue definir as propriedades de uma forma puramente declarativa e indepen- dente de qualquer implementação. É exactamente por este motivo (a independência em relação à implementação) que com o trabalho desta dissertação - geração de tes- tes abstractos - se poderá facilmente realizar futuramente a fase de concretização dos testes para qualquer linguagem.
Listagem 3.1: ADT naturals ✶ ADT n a t u r a l s
✷ Sor t nat
✸ Generators
✹ zero −> nat ; ✺ suc : nat −> nat ;
✻ Operations
✼ plu s : nat , nat −> nat ; ✽ sum : nat , nat −> nat ; ✾ eq : nat , nat −> bool ; ✶✵ l t : nat , nat −> bool ;
✶✶ Axioms
✶✷ sum(X , zero ) = zero ;
✶✸ sum(X , suc (Y) ) = suc (sum(X , Y) ) ; ✶✹ eq ( zero , suc (X) ) = f a l s e ; ✶✺ eq ( suc (Y) , zero ) = f a l s e ; ✶✻ eq ( zero , zero ) = t r u e ;
✶✼ eq ( suc (X) , suc (Y) ) = eq (X , Y) ; ✶✽ l t ( zero , suc (X) ) = t r u e ; ✶✾ l t ( suc (X) , zero ) = f a l s e ; ✷✵ l t ( suc (X) , suc (Y) ) = l t (X , Y) ;
✷✶ Where
✷✷ X : nat ;
✷✸ Y : nat ;
A listagem 3.1 mostra um exemplo de definição de um ADT para os números naturais. Nesta definição começou-se por definir o título do ADT (linha 2), e o Sort (i.e
3. TRABALHO RELACIONADO 3.1. APN - Redes de Petri algébricas
o tipo) que este ADT define (linha 3). Nas linhas (4-6) definiu-se os geradores do ADT. zeroé um gerador de base, e suc é um gerador recursivo, que tem um argumento do tipo nat. Com estes geradores, na prática, pode-se construir todos os naturais a partir do valor zero, da seguinte forma:
1. zero 2. suc(zero) 3. suc(suc(zero) 4. suc(suc(suc(zero) 5. sucn(zero)... 1
De seguida, nas linhas 7 a 11 tem-se a assinatura das operações que pertencem ao ADT. Cada uma das operações é definida através do nome, dos tipos dos argumentos e do tipo do resultado. Da linha 12 à linha 21 têm-se os axiomas sobre as operações do ADT, que definem as propriedades do próprio Sort e que fornecem semânticas às assinaturas anteriormente definidas. Por fim, no final da definição declaram-se os sorts das variáveis utilizadas nos axiomas.
Pode-se observar que é recorrente a utilização do sort bool. Neste trabalho, os ADT podem referenciar sorts já definidos. Neste caso pode-se ver uma definição de várias álgebras no início do apêndice A.3 como parte integrante de um exercício maior expli- cado nos próximos capítulos.
3.1.1.2 Petri nets algébricas (APN)
Tendo já visto o que são ADTs, como se definem e para que servem, pode-se então relacioná-los com as APN. Atente-se na figura 3.1.
increment finished lt(counter ,suc^10(zero))=true counter zero suc(counter) eq(counter,suc^10(zero))=true counter counter zero
Figura 3.1: Rede de Petri Algébrica de um Contador
3. TRABALHO RELACIONADO 3.1. APN - Redes de Petri algébricas
Na figura tem-se uma APN representada graficamente. Com os círculos representam- se Places que contêm um multiset (estrutura comparável a um conjunto que pode con- ter elementos repetidos do mesmo tipo). Este multiset contém termos algébricos cons- truídos recorrendo a uma determinada álgebra, cujo sort é também o sort do place.
Com as setas definem-se arcos entre os places e as transições. Estes arcos contêm pesos, tal como os arcos das Redes Petri tradicionais, sendo que neste caso estes pesos são também multisets que contêm termos algébricos à semelhança dos multisets dos places. Os termos, aqui, podem ser variáveis instanciáveis com qualquer valor ou termos concretizados, gerados a partir dos geradores de um ADT.
Com os rectângulos representam-se Transições que são eventos passíveis de ser disparados quando existem recursos suficientes (no multiset) no place de origem dos arcos de entrada que possam satisfazer os pesos dos multisets destes arcos.
Para que uma transição seja disparada é necessário ainda que as guardas definidas a partir dos axiomas dos ADT, e que estão associadas às transições, sejam também satisfeitas. Após o disparo, o conteúdo do multiset do arco de saída, cujos termos livres estão já instanciados, deve ser depositado nos places associados aos arcos de saída da transição.
Para o cálculo dos termos de saída e para verificar se as condições são satisfazíveis é muitas vezes utilizada a reescrita de termos [10, 11], com a qual é verificável imedi- atamente se um determinado termo algébrico corresponde a outro através da redução de ambos por aplicação sucessiva dos axiomas do ADT correspondente, que podem ser aplicados a cada momento.
Após esta explanação pode-se então verificar que a APN da figura 3.1 descreve o comportamento de um contador. A APN contém dois places cujo o sort é nat( anteri- ormente definido na listagem 3.1): o place increment e o place finished. Inicialmente
incrementcontém um token zero e finished não contém tokens. Neste contador existe
uma transição que consome do place increment um term do tipo nat - counter - e que, caso este term seja inferior a {suc10(zero)} (lt(counter, suc10(zero)) = true), então co-
loca no mesmo place o sucessor de counter (suc(counter)). Existe ainda outra transição que apenas consome o mesmo token - counter - e deposita o token zero no mesmo place (equivalente a um reset).
Semanticamente, a escolha de qual destas duas transições é disparada é não de- terminística, i.e., a dado momento, sendo o token inferior a suc10(zero), qualquer uma
delas pode ser disparada.
Por fim, existe outra transição, que consome o token counter mas que apenas é dis- parada se esse token for suc10(zero), (eq(counter, suc10(zero)) = true). Nesse caso ne-
nhum token é depositado em finished, e a APN estagna, não evoluindo para nenhum 32
3. TRABALHO RELACIONADO 3.1. APN - Redes de Petri algébricas
estado.
Como se pode observar, uma APN não recebe qualquer tipo de estímulos externos, sendo completamente ’hermética’, servindo essencialmente para efeitos de simulação, i.e., dada uma marcação inicial obtêm-se os estados sucessivos da APN por aplicação não determinística das transições passíveis de serem disparadas.
Nos trabalhos desta dissertação necessita-se que a APN responda a estímulos ex- ternos, e por isso, ir-se-á propôr uma extensão de forma a que isso seja possível.