Nesta secção pretende-se mostrar algumas das regras que foram especificadas para efectuar a transformação de modelos SATEL⊕EAPN em modelos MPrologTR. Não sendo frutífero ou vantajoso mostrar exaustivamente todas as regras (pela dimensão da transformação), apresentar-se-ão as regras que permitem obter as cláusulas corres- pondentes aos geradores dos ADT. Assim, por exemplo, para o ADT dos números na- turais, cujos geradores estão apresentados na listagem 4.15, estão envolvidas as regras apresentadas em seguida.
Listagem 4.15: Geradores para os números naturais ✶ zero −> nat
✷ suc : nat −> nat
No que diz respeito à primeira layer da execução da transformação, nesta está en- volvida a regra da figura 4.11 (listagem 4.16) que permite gerar o objecto ▼♦❞❡❧ conformante com o metamodelo MPrologTR a partir do objecto▼♦❞❡❧ da linguagem SATEL⊕EAPN. Este é o modelo que reúne em♦✇♥❡❞❈❧❛✉s❡s todas as cláusulas neces- sárias à geração dos testes. Por esse motivo é mantido o atributo (na listagem s❡❧❢ = ’Model’, na figura ’❆♣♣❧②❆tr✐❜✉t❡’ como átomo designado ’▼♦❞❡❧’) que permitirá refe- renciar este modelo nas layers subsequentes.
SatelModel2MPrologModel MatchModel Model ApplyModel Model ApplyAttribute Model name model
Figura 4.11: Regra: Transformação do modelo - Visual
✶ r u l e ’ SatelModel2MPrologModel ’ ✷ match w i t h
✸ any SATEL : : Model
✹ apply ✺ mprologTermReference : : Model ( ✻ s e l f = ’ Model ’ ✼ name = ’ model ’ ✽ ) ✾ end r u l e
Listagem 4.16: Regra: Transformação do modelo - Textual
Após a transformação do objecto▼♦❞❡❧ é necessário, a partir de cada par de objectos ❆❉❚ e ❖♣❡r❛t✐♦♥ relacionados pela relação ♦✇♥❡❞●❡♥❡r❛t♦r, obter uma cláusula (i.e. um objecto❈❧❛✉s❡). Isto é efectuado através da regra 4.12 (listagem 4.17), onde uma vez mais é etiquetado o objecto gerado a partir deste par, com o valor ’●❡♥❡r❛t♦r❈❧❛✉s❡’.
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação Generator2Clause MatchModel ADT Operation ApplyModel Clause ApplyAttribute GeneratorClause ownedGenerators
Figura 4.12: Regra: Cláusula do Gerador - Visual
✶ r u l e ’ Generator2Clause ’ ✷ match w i t h
✸ adt : any SATEL .APN. adtmm : : ADT ✹ op : any SATEL .APN. adtmm : : Operation ✺ ✻ s u b j e c t t o ✼ adt −−(ownedGenerators )−> op ✽ ✾ apply ✶✵ mprologTermReference : : Clause ( ✶✶ s e l f = ’ GeneratorClause ’ ✶✷ ) ✶✸ end r u l e
Listagem 4.17: Regra: Cláusula do Gerador - Textual
No mesmo sentido, gera-se também um objecto❍❡❛❞ e um objecto ❇♦❞② para cada par❆❉❚ e ❖♣❡r❛t✐♦♥ relacionados pela mesma relação da regra anterior (figura 4.13 e figura 4.14 respectivamente). Generator2Head MatchModel ADT Operation ApplyModel Head ApplyAttribute GeneratorHead ownedGenerators
Figura 4.13: Regra: Cabeça do Gerador - Visual
✶ r u l e’ Generator2Head ’ ✷ match w i t h
✸ adt : any SATEL .APN. adtmm : : ADT ✹ op : any SATEL .APN. adtmm : : Operation ✺ ✻ s u b j e c t t o ✼ adt −−(ownedGenerators )−> op ✽ ✾ apply ✶✵ mprologTermReference : : Head ( ✶✶ s e l f = ’ GeneratorHead ’ ✶✷ ) ✶✸ end r u l e
Listagem 4.18: Regra: Cabeça do Gerador - Textual
Em termos abstractos, com estas regras tem-se criada a estrutura de uma cláusula que representará um gerador (exceptuando-se as relações entre❈❧❛✉s❡ e ❇♦❞② e entre ❈❧❛✉s❡ e ❍❡❛❞).
Para dar seguimento à construção da cabeça da cláusula atente-se no exemplo do gerador s✉❝✿ ♥❛t ✲❃ ♥❛t. Quer-se agora que ♥❛t seja o nome do functor da cabeça da
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação Generator Body MatchModel ADT Operation ApplyModel Body ApplyAttribute GeneratorBody ownedGenerators
Figura 4.14: Regra: Corpo do Gerador - Visual
✶ r u l e ’ Generator Body ’ ✷ match w i t h
✸ adt : any SATEL .APN. adtmm : : ADT ✹ op : any SATEL .APN. adtmm : : Operation ✺ ✻ s u b j e c t t o ✼ adt −−(ownedGenerators )−> op ✽ ✾ apply ✶✵ mprologTermReference : : Body ( ✶✶ s e l f = ’ GeneratorBody ’ ✶✷ ) ✶✸ end r u l e
Listagem 4.19: Regra: Corpo do Gerador - Textual
cláusula para se obter algo como♥❛t✭✳✳✳✮✿✲ ✳✳✳ . Mais ainda, pretende-se que o functor ♥❛t imbrique outro functor, cujo nome é o nome da operação que constitui o gerador (s✉❝), obtendo-se algo como ♥❛t✭s✉❝✭✳✳✳✮✮✿✲✳✳✳ . Com a regra da figura 4.15 (listagem 4.20) identifica-se, tal como anteriormente, o padrão de gerador, conjuntamente com o atributo♥❛♠❡ da Operação e com o ❙♦rt do Resultado do gerador (e respectivo ♥❛♠❡ em❙♦rt❉❡❝❧❛r❛t✐♦♥). Tendo sido feita correspondência com o padrão geram-se os pre- tendidos functores: um, cujo nome (t❡①t) é o nome do respectivo sort do resultado e outro para ser imbricado no primeiro através da relação♦✇♥❡❞❚❡r♠). Neste, o atributo t❡①t é o nome da operação.
Desta forma obtém-se em termos abstractos algo como♥❛t✭s✉❝✭✳✳✳✮✮✿✲✳✳✳ . Repare-se que ambos os functores são rotulados como ’ResultFunctor’ e ’OperationFunctor’, pois serão utilizados futuramente.
Para finalizar a definição das regras da primeira layer resta definir uma que gera os objectos necessários em falta para se obter♥❛t✭s✉❝✭❳✮✮✿✲♥❛t✭❳✮. Daqui se depreende que serão criadas variáveis para cada um dos sorts (argumentos) do gerador para se- rem colocadas em ♦✇♥❡❞❚❡r♠ do functor s✉❝ e serão gerados também functores por cada um dos sorts para serem colocados no corpo da cláusula. Na regra da figura 4.16 é novamente identificado o padrão de gerador conjugado com cada❆t♦♠✐❝❙♦rt na lista de♦♣❡r❛t✐♦♥❙♦rts (argumentos do gerador). Repare-se que o facto de ser uma lista faz com que este padrão seja identificado uma vez por cada elemento em♦♣❡r❛t✐♦♥❙♦rts. Como se pode observar é gerado o functor com o nome do operationSort e é aninhado um objecto ❱❛r✐❛❜❧❡❘❡❢❡r❡♥❝❡ através da relação ♦✇♥❡❞❚❡r♠. Este objecto ❱❛r✐❛❜❧❡❘❡✲ ❢❡r❡♥❝❡ é um apontador para uma Variável (relação ✐❞❘❡❢❡r❡♥❝❡) que será colocada no functor s✉❝ (s❡❧❢❂❖♣❡r❛t✐♦♥❋✉♥❝t♦r), criado na regra anterior. Repare-se que o nome
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação OperationNameAndResultAtomicSort2HeadFunctors MatchModel Operation name AtomicSort SortDeclaration name ADT ApplyModel Functor ApplyAttribute OperationFunctor text Functor ApplyAttribute ResultFunctor text ownedGenerators result declaration ownedTerm
Figura 4.15: Regra: Constituintes da ca- beça - Visual
✶ r u l e ’ OperationNameEResultSort2HeadFuncs ’ ✷ match w i t h
✸ op : any SATEL .APN. adtmm : : Operation (
✹ opname : name
✺ )
✻ as : any SATEL .APN. adtmm : : AtomicSort ✼ sd : any SATEL .APN. adtmm : :
S o r t D e c l a r a t i o n (
✽ sdname : name
✾ )
✶✵ adt : any SATEL .APN. adtmm : : ADT ✶✶ ✶✷ s u b j e c t t o ✶✸ op −−( r e s u l t )−> as ✶✹ as −−(d e c l a r a t i o n )−> sd ✶✺ adt −−(ownedGenerators )−> op ✶✻ ✶✼ apply ✶✽ opFunc : ✶✾ mprologTermReference : : Functor ( ✷✵ s e l f = ’ OperationFunctor ’ ✷✶ t e x t = sameAs ( opname ) ✷✷ ) ✷✸ resSortFunc : ✷✹ mprologTermReference : : Functor ( ✷✺ s e l f = ’ ResultFunctor ’ ✷✻ t e x t = sameAs ( sdname ) ✷✼ ) ✷✽ s u b j e c t t o
✷✾ resSortFunc −−(ownedTerm )−> opFunc ✸✵ end r u l e
Listagem 4.20: Regra: Constituintes da cabeça - Textual
da variável é ✬★★✈❛r★★✬, pois após o modelo ser criado é necessário percorrê-lo de forma a dar nomes apropriados a cada variável que tenha este padrão como nome. Isto deve-se a uma limitação do DSLTrans, uma vez que este peca por não conter, até à data, sequenciadores que permitam especificar situações como esta. Note-se ainda os rótulos dos objectos criados: ❖♣❡r❛t✐♦♥❙♦rt❋✉♥❝t♦r, ❆t♦♠✐❝❙♦rt❱❛r✐❛❜❧❡❘❡❢, ❆t♦♠✐❝✲ ❙♦rt❱❛r✐❛❜❧❡.
A partir deste ponto, todos os objectos necessários estão criados e passa-se à se- gunda layer onde serão criadas as relações entre estes.
Primeiro que tudo é necessário ligar a cláusula criada inicialmente ao modelo. A re- gra da figura 4.17 (listagem 4.21) identifica cada uma das operações que se encontram em algum nó das sub-árvores que derivam do nó ❙❛t❡❧✿✿▼♦❞❡❧ e, por isso, utiliza-se uma conexão P♦s✐t✐✈❡■♥❞✐r❡❝t❆ss♦❝✐❛t✐♦♥, isto é, uma associação indirecta. Na parte de apply da regra liga-se o ▼♦❞❡❧, já criado na layer anterior, à ❈❧❛✉s❡ criada na layer anterior por via da mesma ❖♣❡r❛t✐♦♥. É para este efeito que são usados os P♦s✐t✐✈❡✲ ❇❛❝❦✇❛r❞▲✐♥❦s (a tracejado) que permitem forçar a que sejam utilizados exactamente
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação Foreach_OperationSort_in_Operation2HeadVariablesAndBodyFunctors MatchModel Operation name AtomicSort SortDeclaration name ADT ApplyModel Variable ApplyAttribute AtomicSortVariable name ##var## Functor ApplyAttribute OperationSortFunctor text VariableReference ApplyAttribute AtomicSortVariableRef ownedGenerators ownedTerm declaration operationSorts idReference
Figura 4.16: Regra: Variáveis à cabeça e functores do corpo da cláusula - Visual os mesmo objectos criados na layer anterior a partir do mesmo objecto. Não obstante, é ainda necessário referir que o ’ApplyAttribute’ tem o mesmo valor para que seja identificado o objecto. Neste caso✬●❡♥❡r❛t♦r❈❧❛✉s❡✬ para a cláusula gerada a partir da operação e✬▼♦❞❡❧✬ para o Model. Uma vez que há só um ▼♦❞❡❧ não seria necessário colocar o ’ApplyAttribute’, contudo colocou-se para reforçar a ideia de que é o mesmo ▼♦❞❡❧, e para que o leitor possa seguir melhor as regras seguintes.
Pode-se perguntar o que acontece quando é identificada uma ❖♣❡r❛t✐♦♥ acessível a partir de▼♦❞❡❧ e para a qual não existe uma ❈❧❛✉s❡ criada. Nesse caso a ❖♣❡r❛t✐♦♥ identificada não é um gerador e, portanto não existe nenhum ADT que a contenha (via relação♦✇♥❡❞●❡♥❡r❛t♦rs). Consequentemente não existe o objecto ❈❧❛✉s❡ com ❆♣✲ ♣❧②❆ttr✐❜✉t❡ ’GeneratorClause’. Neste caso a regra não se aplica simplesmente.
Da mesma forma associamos a cabeça (❍❡❛❞) da cláusula (❈❧❛✉s❡) à própria cláu- sula (através da relação♦✇♥❡❞❍❡❛❞), tal como se mostra na figura 4.18(listagem 4.22). Repare-se que nesta regra,❍❡❛❞ e ❈❧❛✉s❡, tanto foram geradas a partir de ❆❉❚ como de❖♣❡r❛t✐♦♥, no entanto basta colocar uma restrição. A restrição em relação a ❖♣❡r❛✲
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação
Generators inside Model
MatchModel Model Operation ApplyModel Clause ApplyAttribute GeneratorClause Model ApplyAttribute Model contains ownedClause
Figura 4.17: Regra: Cláusula no modelo - Visual
✶ r u l e ’ Generators i n s i d e Model ’ ✷ match w i t h
✸ sm : any SATEL : : Model ✹ sop : any SATEL .APN. adtmm : :
Operation ✺ ✻ s u b j e c t t o ✼ sm ~~( c o n t a i n s ) ~> m261 ✽ apply ✾ c l : ✶✵ mprologTermReference : : Clause ( ✶✶ s e l f = ’ GeneratorClause ’ ✶✷ ) ✶✸ mmodel : ✶✹ mprologTermReference : : Model ( ✶✺ A p p l y A t t r i b u t e = ’ Model ’ ✶✻ ) ✶✼ s u b j e c t t o ✶✽ mmodel −−(ownedClause )−> c l ✶✾ ✷✵ r e s t r i c t i o n s ✷✶ c l d e r i v e d from sop ✷✷ mmodel d e r i v e d from sm ✷✸ end r u l e
Listagem 4.21: Regra: Cláusula no modelo - Textual
t✐♦♥ seria sempre necessária, pelo que permaneceu apenas essa, até porque a partir do momento em que o padrão está identificado sabe-se que a ❖♣❡r❛t✐♦♥ é um gerador, e que, portanto, foi a partir desta gerado um objecto❍❡❛❞ e um objecto ❈❧❛✉s❡.
Na regra 4.19 ( 4.23), volta-se a identificar o❙♦rt do resultado do gerador e recupera- se tanto a cabeça gerada a partir desse gerador como o functor❘❡s✉❧t❋✉♥❝t♦r criado a partir da associaçãor❡s✉❧t entre ❖♣❡r❛t✐♦♥ e ❆t♦♠✐❝❙♦rt na regra da figura 4.15.
Com a regra 4.20(listagem 4.24) recupera-se cada uma das variáveis associadas a cada um dos sorts que se relacionam com❖♣❡r❛t✐♦♥ através da relação ♦♣❡r❛t✐♦♥❙♦rts e que foram criadas nas regras da layer anterior. Repare-se que se utilizam exactamente os mesmos valores para os ❆♣♣❧②❆ttr✐❜✉t❡. Em rigor, colocamos em ♦✇♥❡❞❚❡r♠ do functor (’OperationFunctor’), cada uma das variáveis. O laço no objecto❱❛r✐❛❜❧❡ serve para quando um gerador tem mais do que um argumento (♦♣❡r❛t✐♦♥❙♦rt). Nesse caso esta regra é aplicada tantas vezes quantos os elementos em ♦♣❡r❛t✐♦♥❙♦rt e, uma vez que o ♦✇♥❡❞❚❡r♠ não é uma lista/conjunto e por isso apenas suporta um elemento, então ordena-se o DSLTrans para que, a seguir ao processamento do primeiro♦♣❡r❛t✐✲ ♦♥❙♦rt, a ❱❛r✐❛❜❧❡ seja colocada como seguinte (nextTerm) da variável que se encontra já lá colocada. Isto significa que o DSLTrans itera sobre♥❡①t❚❡r♠ a partir do ♦✇♥❡❞❚❡r♠ do functor até encontrar o fim desta lista.
Até este ponto, em relação ao gerador de exemplo tem-se: ♥❛t✭s✉❝✭❳✮✮✿✲✳✳✳. 76
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.7. Modelo de transformação GenClauseHead MatchModel Operation ADT ApplyModel Clause ApplyAttribute GeneratorClause Head ApplyAttribute GeneratorHead ownedHead ownedGenerators
Figura 4.18: Regra: Cabeça na cláusula - Visual
✶ r u l e ’ Head i n s i d e Clause Gen ’ ✷ match w i t h
✸ m264 : any SATEL .APN. adtmm : : Operation
✹ m265 : any SATEL .APN. adtmm : : ADT ✺ s u b j e c t t o ✻ m265 −−(ownedGenerators )−> m264 ✼ apply ✽ m266 : mprologTermReference : : Clause ( ✾ s e l f = ’ GeneratorClause ’ ✶✵ ) ✶✶ m267 : mprologTermReference : : Head ( ✶✷ s e l f = ’ GeneratorHead ’ ✶✸ ) ✶✹ s u b j e c t t o ✶✺ m266 −−(ownedHead )−> m267 ✶✻ r e s t r i c t i o n s ✶✼ m266 d e r i v e d from m264 ✶✽ m267 d e r i v e d from m264 ✶✾ end r u l e
Listagem 4.22: Regra: Cabeça na cláusula - Textual
Em seguida é necessário colocar os functores no corpo da cláusula. Com a regra da figura 4.21(listagem 4.25), à semelhança do que acontece com a regra anterior, faz- se a identificação das relações ♦♣❡r❛t✐♦♥❙♦rt entre a ❖♣❡r❛t✐♦♥ do gerador e os ❙♦rt e recupera-se o objecto❇♦❞② que já lhe está associado e o Functor ’OperationSortFunc- tor’ associado à relação. Mais uma vez é utilizado o laço sobre o functor para os colocar em♥❡①t❚❡r♠ aquando de cada identificação de padrão.
Neste ponto tem-se o modelo da cláusula quase pronto, faltando apenas associar à cláusula o objecto❇♦❞② gerado a partir da regra da layer anterior. A regra da figura 4.22 (listagem 4.27) funciona da seguinte forma: tenta-se identificar o padrão em que exista um objecto❆t♦♠✐❝❙♦rt associado à ❖♣❡r❛t✐♦♥ de um gerador através da relação ♦♣❡r❛✲ t✐♦♥❙♦rt. Caso a relação exista pelo menos uma vez então o objecto Body é colocado na Clause, caso contrário não é, porque o padrão da regra não é aplicável. Um caso em que não é aplicável é o do gerador③❡r♦ ✲❃ ♥❛t que não contém quaisquer argumentos. Repare-se ainda que o❆t♦♠✐❝❙♦rt é agora um objecto da classe ❊①✐sts▼❛t❝❤❈❧❛ss do DSLTrans.
✶ nat ( zero ) .
✷ nat ( suc (X) ) :− nat (X) .
Listagem 4.26: Regra: Corpo da Cláusula - Textual
Após a aplicação desta regra tem-se finalmente a transformação de ambos os gera- dores num modelo MPrologTR, que após ser transformado num modelo MProlog (sem
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.8. Conclusões Generators Head.ownedFunctor MatchModel Operation AtomicSort ADT ApplyModel Functor ApplyAttribute ResultFunctor Head ApplyAttribute GeneratorHead ownedFunctor result ownedGenerators
Figura 4.19: Regra: OwnedFunctor da cabeça - Visual
✶ r u l e ’ GenClauseHead ’ ✷ match w i t h
✸ m264 : any SATEL .APN. adtmm : : Operation
✹ m265 : any SATEL .APN. adtmm : : ADT ✺ s u b j e c t t o ✻ m265 −−(ownedGenerators )−> m264 ✼ apply ✽ m266 : mprologTermReference : : Clause ( ✾ s e l f = ’ GeneratorClause ’ ✶✵ ) ✶✶ m267 : mprologTermReference : : Head ( ✶✷ s e l f = ’ GeneratorHead ’ ✶✸ ) ✶✹ s u b j e c t t o ✶✺ m266 −−(ownedHead )−> m267 ✶✻ r e s t r i c t i o n s ✶✼ m266 d e r i v e d from m264 ✶✽ m267 d e r i v e d from m264 ✶✾ end r u l e
Listagem 4.23: Regra: OwnedFunctor da cabeça - Textual
referências), de serem resolvidos os nomes das variáveis (##var##), e ser transformado em texto, resulta no contéudo da listagem 4.26.
Dá-se assim por concluída esta transformação dos geradores do ADT dos naturais.
4.8
Conclusões
Neste capítulo apresentou-se detalhadamente a abordagem proposta. Realçou-se que foram previamente abordadas outras soluções que foram descartadas por poderem comprometer o trabalho que se pretendia para esta dissertação. Apresentou-se uma solução metamodelada da linguagem Prolog com o fim de satisfazer a natureza de ori- entação a modelos em que este trabalho acenta. Mostrou-se como obter um modelo Prolog a partir do modelo SATEL⊕EAPN através de regras de transformação especi- ficadas em DSLTrans e foi ainda abordada a técnica de obtenção dos oráculos a partir dos testes abstractos gerados.
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.8. Conclusões
Generator HeadFunctor Variables
MatchModel Operation AtomicSort ADT ApplyModel Variable ApplyAttribute AtomicSortVariable Functor ApplyAttribute OperationFunctor ownedGenerators ownedTerm operationSorts nextTerm
Figura 4.20: Regra: Variáveis do functor da cabeça - Visual
✶ r u l e ’ Generator HeadFunctor Variables ’ ✷ match w i t h
✸ m273 : any SATEL .APN. adtmm : : Operation ✹ m274 : any SATEL .APN. adtmm : : AtomicSort ✺ m275 : any SATEL .APN. adtmm : : ADT ✻ s u b j e c t t o ✼ m273 −−(o p e r a t i o n S o r t s )−> m274 ✽ m275 −−(ownedGenerators )−> m273 ✾ apply ✶✵ m276 : mprologTermReference : : V a r i a b l e ( ✶✶ s e l f = ’ AtomicSortVariable ’ ✶✷ ) ✶✸ m277 : mprologTermReference : : Functor ( ✶✹ s e l f= ’ OperationFunctor ’ ✶✺ ) ✶✻ s u b j e c t t o ✶✼ m277 −−(ownedTerm )−> m276 ✶✽ m276 −−(nextTerm )−> m276 ✶✾ ✷✵ r e s t r i c t i o n s ✷✶ m276 d e r i v e d from m274 ✷✷ m277 d e r i v e d from m273 ✷✸ m276 d e r i v e d from m275 ✷✹ m276 d e r i v e d from m273 ✷✺ end r u l e
Listagem 4.24: Regra: Variáveis do functor da cabeça - Textual
Generators Body Functors
MatchModel Operation AtomicSort SortDeclaration ADT ApplyModel Body ApplyAttribute GeneratorBody Functor ApplyAttribute OperationSortFunctor ownedTerm operationSorts ownedGenerators nextTerm declaration
Figura 4.21: Regra: Functores do corpo da cláusula - Visual
✶ r u l e ’ Generators Body Functors ’ ✷ match w i t h
✸ m278 : any SATEL .APN. adtmm : : Operation ✹ m279 : any SATEL .APN. adtmm : : AtomicSort ✺ m280 : any SATEL .APN. adtmm : :
S o r t D e c l a r a t i o n
✻ m281 : any SATEL .APN. adtmm : : ADT ✼ s u b j e c t t o ✽ m278 −−(o p e r a t i o n S o r t s )−> m279 ✾ m279 −−(d e c l a r a t i o n )−> m280 ✶✵ m281 −−(ownedGenerators )−> m278 ✶✶ apply ✶✷ m282 : mprologTermReference : : Body ( ✶✸ s e l f = ’ GeneratorBody ’ ✶✹ ) ✶✺ m283 : mprologTermReference : : Functor ( ✶✻ s e l f= ’ OperationSortFunctor ’ ✶✼ ) ✶✽ s u b j e c t t o ✶✾ m282 −−(ownedTerm )−> m283 ✷✵ m283 −−(nextTerm )−> m283 ✷✶ r e s t r i c t i o n s ✷✷ m282 d e r i v e d from m278 ✷✸ m283 d e r i v e d from m281 ✷✹ m283 d e r i v e d from m280 ✷✺ m283 d e r i v e d from m278 ✷✻ end r u l e
Listagem 4.25: Regra: Functores do corpo da cláusula - Textual
4. ABORDAGEM PROPOSTA/SOLUÇÃO 4.8. Conclusões
Creates Body if there is some operationSort
MatchModel Operation AtomicSort ADT ApplyModel Clause ApplyAttribute GeneratorClause Body ApplyAttribute GeneratorBody operationSorts ownedGenerators ownedBody
Figura 4.22: Regra: Corpo da Cláusula - Visual
✶ r u l e’ Creates Body i f t h e r e i s some o p e r a t i o n S o r t ’
✷ match w i t h
✸ m284 : any SATEL .APN. adtmm : : Operation ✹ m285 : e x i s t i n g SATEL .APN. adtmm : :
AtomicSort
✺ m286 : any SATEL .APN. adtmm : : ADT ✻ ✼ s u b j e c t t o ✽ m284 −−(o p e r a t i o n S o r t s )−> m285 ✾ m286 −−(ownedGenerators )−> m284 ✶✵ ✶✶ apply ✶✷ m287 : mprologTermReference : : Clause ( ✶✸ s e l f = ’ GeneratorClause ’ ✶✹ ) ✶✺ m288 : mprologTermReference : : Body ( ✶✻ s e l f = ’ GeneratorBody ’ ✶✼ ) ✶✽ s u b j e c t t o ✶✾ m287 −−(ownedBody )−> m288 ✷✵ r e s t r i c t i o n s ✷✶ m288 d e r i v e d from m284 ✷✷ m287 d e r i v e d from m284 ✷✸ end r u l e
Listagem 4.27: Regra em sintaxe textual
5
Exemplo ilustrativo
Este capítulo serve para demonstrar a aplicação da técnica apresentada no capítulo anterior.
Para fins ilustrativos presuma-se a existência de um componente de software uti- lizado numa fábrica industrial que tem como propósito fazer a contagem de troncos de árvore que entram na máquina de processamento de madeira em toros. Sabe-se que a máquina não suporta mais de 10 troncos simultâneamente, pelo que ao décimo tronco tem de ser emitido um alarme para que a passadeira rolante pare. Por outro lado sabe-se que a madeira não vem sempre ao mesmo ritmo, apresentando latência elevada e, nesse sentido, o funcionário de controlo junto à entrada da máquina tem que cuidar para que nem a máquina, nem a passadeira passem tempos elevados sem produzir pelo que, em casos de grande latência, ele deve apertar o botão para que a máquina comece a trabalhar. Nesse momento a máquina inicia o funcionamento com a madeira que tem, a passadeira pára e é afixado e registado o numero de toros que es- tão em processamento. Obviamente quando o alarme dispara são também registados e acumulados à contabilidade os 10 troncos num outro componente que interpreta o output deste.
Antes da entrega do componente quer-se testar se este se comporta conforme os requisitos e para isso utilizar-se-á a abordagem apresentada na tese. É importante que o componente conte correctamente nas fases de intervenção humana, pelo que se quer aferir se o contador, quando resetado, lança para o exterior o número exacto de toros.
Obviamente este componente pode ser modelado através do modelo de contador da figura 5.1, que já tem vindo a ser utilizado. A partir deste modelo gerou-se testes
5. EXEMPLO ILUSTRATIVO
de acordo com as intenções de teste modeladas na listagem 5.5.
Nas listagens 5.1, 5.2 e 5.3 são definidas três álgebras (respectivamente naturais, booleanos, e listas que embora não sejam usadas, servem aqui para exemplificação da transformação de axiomas com condições). Encontra-se ainda na listagem 5.4 a especificação textual da EAPN apresentada na figura 5.1.
tick alarm mark time(counter) increment finished lt(counter ,suc^10(zero))=true counter zero suc(counter) eq(counter,suc^10(zero))=true counter counter zero
Figura 5.1: Rede de Petri Algébrica de um Contador
Na listagem 5.1 encontra-se a especificação dos naturais com dois geradores (já introduzidos anteriormente) e um conjunto de operações básicas sobre naturais algé- bricos e respectivos axiomas.
Listagem 5.1: Especificação de modelo: Álgebra dos naturais ✶ T e s t I n t e n t i o n S e t m y t e s t i n t e n t i o n ✷ Algebras ✸ ✹ 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 82
5. EXEMPLO ILUSTRATIVO ✷✺ ✷✻ X : nat ; ✷✼ Y : nat ; ✷✽ ✷✾ . . .
A listagem 5.2 define uma álgebra simples para os booleans. Apenas são definidos dois geradores (valores de verdade e falsidade) e uma operação de negação.
Listagem 5.2: Especificação de modelo: Álgebra dos Booleans ✶ . . . ✷ ADT Boolean ✸ Sor t bool ✹ Generators ✺ f a l s e −> bool ; ✻ t r u e −> bool ; ✼ Operations
✽ neg : bool −> bool ;
✾ Axioms
✶✵ neg ( f a l s e ) = t r u e ; ✶✶ neg ( t r u e ) = f a l s e ; ✶✷ . . .
Na listagem 5.3 é definida uma álgebra para listas. Como referido este ADT não é utilizado directamente na geração de testes para este modelo, porém, como utiliza construções mais sofisticadas na especificação dos axiomas pareceu revelar-se impor- tante para mostrar a potencialidade da ferramenta e da transformação. Nesta álgebra existem dois geradores, um para a lista vazia (linha 5), e outro que coloca um elemento à cabeça de uma lista existente (linha 6). Definiram-se duas operações e respectivos axiomas para calcular, respectivamente, o tamanho da lista (linha 9) e o número de ocorrências de um elemento na mesma (linha 10).
Listagem 5.3: Especificação de modelo: Álgebra das Lists ✶ . . . ✷ ADT L i s t ✸ Sor t l i s t ✹ Generators ✺ n i l −> l i s t ; ✻ cons : nat , l i s t −> l i s t ; ✼ ✽ Operations ✾ s i z e : l i s t −> nat ; ✶✵ nbOcurr : nat , l i s t −> nat ; ✶✶
✶✷ Axioms
✶✸ eq ( $E , $H) = t r u e => nbOcurr ( $E , cons ( $H , $L ) ) = suc ( nbOcurr ( $E , $L ) ) ; ✶✹ eq ( $E , $H) = f a l s e => nbOcurr ( $E , cons ( $H , $L ) ) = nbOcurr ( $E , $L ) ; ✶✺ s i z e ( n i l ) = zero ;
✶✻ s i z e ( cons ( $H , $L ) ) = suc ( s i z e ( $L ) ) ; ✶✼ nbOcurr ( $E , n i l ) =zero ;
5. EXEMPLO ILUSTRATIVO ✶✾ H: nat ; ✷✵ L : l i s t ; ✷✶ E : nat ; ✷✷ End Algebras ; ✷✸ . . .
Na listagem 5.4 foi definido o foco das intenções de teste - a EAPN apresentada na figura. Primeiramente são definidos os places Inc e Finished (linha 5 e 6), onde são definidos tokens para Inc: um MultiSet com o token algébrico natural③❡r♦. É também possível especificar o sort do place neste ponto. Em seguida definiram-se os arcos entre os places e as transições anotados com os respectivos pesos através de MultiSets. Especificaram-se as transições indicando um nome, os métodos que as despoletam e as gates de observação que lhe estão afectas. No caso das transições ’increment’ e ’alarmTrigger’ foram também especificadas as respectivas guardas concordando com o disparo se a variável❈♦✉♥t❡r excede ou iguala suc10(Counter).
Listagem 5.4: Especificação de modelo: APN ✶ . . .
✷ Focus
✸ APN Counter
✹ Places
✺ Place I n c tokens [ zero ] ✻ Place F in is hed
✼ Arcs
✽ Arc Inc2increment { I n c −−> increment tokens [ $Counter ] } ✾ Arc increment2Inc { increment −−> I n c tokens [ suc ( $Counter ) ] } ✶✵
✶✶ Arc r e s e t 2 I n c { r e s e t −−> I n c tokens [ $Counter ] } ✶✷ Arc I n c 2 r e s e t { I n c −−> r e s e t tokens [ zero ] } ✶✸
✶✹ Arc I n c 2 a l a r m T r i g g e r { I n c −−> a l a r m T r i g g e r tokens [ $Counter ] } ✶✺ Arc a l a r m T r i g g e r 2 I n c { a l a r m T r i g g e r −−> F ini sh ed }
✶✻
✶✼ T r a n s i t i o n s
✶✽ T r a n s i t i o n increment {
✶✾ Guard { l t ( $Counter , suc ^10( zero ) ) = t r u e } ✷✵ MethodCalls [ t i c k ]
✷✶ }
✷✷
✷✸ T r a n s i t i o n r e s e t {
✷✹ GateCalls [ time ( $Counter ) ] ✷✺ MethodCalls [ mark ]
✷✻ }
✷✼
✷✽ T r a n s i t i o n a l a r m T r i g g e r {
✷✾ Guard { eq ( $Counter , suc ^10( zero ) ) = t r u e } ✸✵ GateCalls [ alarm ]
✸✶ MethodCalls [ t i c k ]
✸✷ }
✸✸
✸✹ Methods [ t i c k , mark ] ✸✺ Gates [ alarm , time ]
5. EXEMPLO ILUSTRATIVO 5.1. Processo de obtenção de testes ✸✻ ✸✼ Where ✸✽ Counter : nat ; ✸✾ ✹✵ End Focus ; ✹✶ . . .
Por fim, são definidas as intenções de teste que têm vindo a ser utilizadas na lista- gem 5.5. Atente-se que a variável❈♦✉♥t❡r é, neste exemplo, restringida entre zero e suc3(zero), por uma questão de simplificar a apresentação de resultados.
Listagem 5.5: Especificação de modelo: Intenções de teste ✶ . . . ✷ I n t e r f a c e ✸ T e s t I n t e n t i o n T i c k I n t e n t i o n ; ✹ T e s t I n t e n t i o n M a r k I n t e n t i o n ; ✺ Body ✻ V a r i a b l e s ✼ t : primitiveHML ; ✽ Counter : nat ; ✾ x : p r i m i t i v e I n t e g e r ; ✶✵ y : p r i m i t i v e S t i m u l a t i o n ; ✶✶ Axioms ✶✷ HML( T ) in T i c k I n t e n t i o n ; ✶✸ $ t in T i c k I n t e n t i o n , nbEvents ( $ t ) <6 => $ t . HML ( { < t i c k > } T ) i n T i c k I n t e n t i o n ; ✶✹ { l t ( $Counter , suc ^3( zero ) ) } = { t r u e } , $ t in T i c k I n t e n t i o n => $ t .HML({ < mark w i t h time (
$Counter ) >} T ) in M a r k I n t e n t i o n ; ✶✺ End
5.1
Processo de obtenção de testes
Através da figura 5.2 revisita-se o plano para obtenção de testes. Primeiramente, após o modelo estar especificado, na etapa 1 faz-se unfolding das estruturas comprimidas; por exemplo, relativamente ao modelo, suc3(zero)é convertido em suc(suc(suc(zero))), os
nomes das gates são prefixados com ’gate_’ e dos métodos com ’method_’ para que iniciem com letra minúscula, pois no Prolog os functores devem iniciar por letra mi- núscula; e ainda, caso existissem multisets contendo algum elemento com multiplici- dade maior que 1 seriam gerados elementos iguais a esse com o fim de tornar todo o conjunto homogéneo no que diz respeito à multiplicidade.
Seguidamente na etapa 2 é feito o refinamento do modelo. No modelo, por exemplo no terceiro axioma das intenções de teste, a primeira condição (lt(Counter, suc3(zero)) =
true)terá a sua referência a apontar para a seguinte condiçãot ✐♥ ❚✐❝❦■♥t❡♥t✐♦♥. Isto é necessário para que o DSLTrans possa efectivamente processar listas.
Na etapa 3 seria gerado o modelo PrologTR a partir do modelo já refinado e nas etapas 4,5 e 6 obter-se-ia, por fim, o código Prolog tal como é apresentado na secção