Listagem 5.12: Soluções obtidas ✶ Sol = [ ( mark , time( zero ) ) , top ] ;
✷ Sol = [ ( mark , time( suc ( zero ) ) ) , top ] ; ✸ Sol = [ ( mark , time( suc ( suc ( zero ) ) ) ) , top ] ; ✹ Sol = [ ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] ; ✺ Sol = [ ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] ; ✻ Sol = [ ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] ; ✼ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] ; ✽ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] ; ✾ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] ; ✶✵ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] ; ✶✶ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] ; ✶✷ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] ; ✶✸ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] ; ✶✹ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ]
;
✶✺ Sol = [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] ;
5.4
Obtenção dos oráculos
Após a obtenção dos testes calcularam-se os oráculos da forma que foi exposta no capítulo anterior, tal como apresentado na listagem 5.13.
Listagem 5.13: Testes abstractos anotados com oráculo ✶ SolO = ( [ ( mark , time( zero ) ) , top ] , t r u e) ;
✷ SolO = ( [ ( mark , time( suc ( zero ) ) ) , top ] , f a l s e ) ; ✸ SolO = ( [ ( mark , time( suc ( suc ( zero ) ) ) ) , top ] , f a l s e ) ; ✹ SolO = ( [ ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] , f a l s e ) ; ✺ SolO = ( [ ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] , t r u e) ; ✻ SolO = ( [ ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] , f a l s e ) ; ✼ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] , f a l s e ) ; ✽ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] , f a l s e ) ; ✾ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] , t r u e) ; ✶✵ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] , f a l s e ) ; ✶✶ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] , f a l s e ) ; ✶✷ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] , f a l s e )
;
✶✸ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( zero ) ) , top ] , f a l s e ) ;
✶✹ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( zero ) ) ) , top ] , f a l s e ) ;
✶✺ SolO = ( [ ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( t i c k , n u l l ) , ( mark , time( suc ( suc ( zero ) ) ) ) , top ] , f a l s e ) ;
Pode-se verificar que os oráculos foram calculados correctamente. Note-se que para as linhas 1, 5 e 9, em que oráculo é verdadeiro indicando que o teste deverá passar, o número de invocações t✐❝❦ ocorridas até à invocação da gate t✐♠❡ corresponde ao parâmetro deste; isto é, zero invocações det✐❝❦ na primeira solução, uma invocação na solução da linha número 5, e duas invocações na solução da linha número 9.
5. EXEMPLO ILUSTRATIVO 5.5. Conclusões
Note-se que para este exemplo foi desactivado o pré-processamento que prefixa os métodos com ’meth’ e as gates com ’gate’, com o fim de melhorar a apresentação.
5.5
Conclusões
Neste capítulo apresentou-se uma concretização da abordagem com um exemplo ilus- trativo - o timer - que acompanhou a tese desde a introdução da linguagem SATEL no Capítulo 3. Serviu, deste modo, para demonstrar o processo de geração de testes abstractos anotados com oráculo a que se propunha a tese e que reflecte totalmente a abordagem Model-Based Testing.
Como discutido, a ferramenta em questão centra-se numa abordagem totalmente baseada em modelos (compreendendo técnicas de transformação de modelos, ou seja, alguns pré e pós processamentos dos modelos em causa). De facto, utilizam-se mode- los para modelar o SUT e também para guiar a geração por entre os diversos traços/ca- minhos de execução do sistema que se queira cobrir. Tendo em conta o estado da arte, com falta de implementações concretas, considera-se ter desenvolvido uma ferramenta inovadora neste estilo de Model-Based Testing.
Numa análise mais pormenorizada, viu-se que perante este exemplo o tempo de execução da ferramenta é infinitésimal. Isto justifica-se com a dimensão do problema, que é significativamente reduzida, e pelas condições envolvidas. Obviamente com o relaxamento da profundidade de pesquisa e alterações das condições (e.g. eliminando a restrição sobre Counter) o tempo de execução é infinito e a ferramenta corrompe-se pois o Prolog não encontra um ponto de terminus (fixo); isto é, em certas situações o Prolog pode não conseguir concluir que a pesquisa pode ser parada (e.g. nos naturais algébricos não existe forçosamente uma relação de ordem entre os elementos; o Prolog, perante uma condição que é satisfeita para qualquer número ’inferior’ a suc3(zero),
não consegue concluir que existem apenas 3 alternativas, e irá continuar a procurar). Uma forma de limitar esta questão é a de apenas utilizar geradores monótonos e não ambíguos nos ADT, no entanto seria ainda necessário procurar que a semântica das operações seguisse essa regra também, e que a pesquisa tivesse isso em conta; não sendo possível, resta usar heurísticas que limitem a pesquisa.
De qualquer forma, problemas como estes são bem conhecidos da geração de testes, dado que a geração exaustiva é, em problemas relaxados e em geral, impraticável.
Trata-se de trabalho futuro tentar lidar com estes problemas de uma forma efici- ente, utilizando heurísticas apropriadas e, possivelmente, estendendo o metamodelo do SATEL com construções que possam informar a ferramenta de novas condições de paragem e/ou dados que promovam a truncatura da árvore de pesquisa em nós a
5. EXEMPLO ILUSTRATIVO 5.5. Conclusões
6
Conclusões
Ao longo desta dissertação foi apresentada a semântica operacional e implementação da linguagem SATEL validando a hipótese proposta de o conseguir em conformidade com o trabalho feito previamente, de especificação formal da sua semântica de um modo denotacional. Deste modo, foi conseguida a geração de testes abstractos a partir de modelos APN com extensões mínimas; testes esses que constituem traços de execu- ção do Sistema sob Teste.
Conseguiu-se uma implementação para a linguagem SATEL, que em detrimento de outras abordagens tentadas, e devidamente discutidas no capítulo 4 e por ser usado o Prolog como veículo de especificação dos testes e obtenção de soluções, se apro- xima da especificação da semântica denotacional original. Acrescenta-se ainda que a utilização de uma sintaxe textual através do EMFText que compreende apenas algu- mas extensões mínimas à linguagem original, contribui também para a forte ligação à sua definição formal. Esta implementação permite-nos validar a SATEL enquanto linguagem que gera efectivamente testes abstractos. Em sumário, a implementação permite-nos fechar o ciclo da abordagem MBT, dando-nos garantias relativamente à SATEL enquanto abordagem baseada em modelos para geração de testes sendo esta, em nossa opinião, uma grande contribuição desta dissertação.
Para a obtenção da implementação foi proposta uma abordagem de desenvolvi- mento orientada a modelos em que os modelos SATEL⊕EAPN sofrem sucessivas trans- formações automáticas até se obter um conjunto de cláusulas Prolog que permitem, finalmente, a pesquisa de soluções. Esta abordagem está submetida obviamente às idi- osincrasias do Prolog, como a pesquisa em profundidade para a qual a nossa solução
6. CONCLUSÕES 6.1. Trabalho futuro
propõe uma heurística simples de limitação.
6.1
Trabalho futuro
Ao longo da dissertação foram feitas algumas referências em relação a trabalho futuro. Não obstante de se ter implementado uma semântica operacional do SATEL, houve alguns aspectos da linguagem que não pertenceram ao foco da implementação. Assim sendo, como trabalho futuro aponta-se:
• a implementação das hipóteses de uniformidade e subuniformidade sobre variá- veis;
• melhoria da obtenção de valores para as variáveis algébricas, possivelmente com algum unfolding prévio das estruturas algébricas, contracção dos geradores base dos ADT (i.e., limitar à partida com base nas condições dos axiomas, o primeiro valor a ser gerado), e ainda com extensão do satel, para que o engenheiro de teste possa anotar os ADT com indicações de restrição mais efectivas;
• prever as fórmulas❍▼▲◆♦t, e ❍▼▲❆♥❞ nos caminhos de execução;
• possível extensão da abordagem a modelos especificados em CO-OPN, à seme- lhança do que foi proposto originalmente;
• concretização dos testes abstractos gerados;
• tendo em vista a optimização, portar a implementação para linguagens de ou- tros paradigmas(e.g. imperativo), com implementação implícita de algoritmos de backtracking, pesquisa e resolução de restrições que consigam melhorar o de- sempenho e que façam face às idiosincrasias do Prolog (eg. pesquisa em depth- first search ).
• integração com o model-checker ALPiNa 1 desenvolvido pelo grupo SMV 2 da Universidade de Genebra3
1http://alpina.unige.ch 2https://smv.unige.ch 3https://www.unige.ch
A
Appendix
A.1
Metamodelo do SATEL em OCLinEcore
1✶ i m p o r t ecore_0 : ’ h t t p : / / www. e c l i p s e . org / emf / 2 0 0 2 / Ecore # / ’ ; ✷
✸ package SATEL : SATEL = ’SATEL ’ ✹ { ✺ c l a s s Model ✻ { ✼ p r o p e r t y t e s t I n t e n t i o n M o d u l e : T e s t I n t e n t i o n M o d u l e [ + ] { !ordered,composes } ; ✽ } ✾ c l a s s T e s t I n t e n t i o n M o d u l e ✶✵ { ✶✶ p r o p e r t y t e s t I n t e n t i o n B o d y : T e s t I n t e n t i o n B o d y [ 1 ] { !ordered,composes } ; ✶✷ p r o p e r t y t e s t I n t e n t i o n I n t e r f a c e : T e s t I n t e n t i o n I n t e r f a c e [ ? ] { !ordered,composes } ; ✶✸ a t t r i b u t e name : S t r i n g [ 1 ] { !ordered, !unique } ;
✶✹ p r o p e r t y focus : apnmm : : APN[ 1 ] { composes } ; ✶✺ p r o p e r t y algebra : adtmm : : ADT [ ∗ ] { composes } ;
✶✻ } ✶✼ c l a s s T e s t I n t e n t i o n I n t e r f a c e ✶✽ { ✶✾ p r o p e r t y i n t e n t i o n : I n t e n t i o n D e c [ + ] { !ordered,composes } ; ✷✵ } ✷✶ c l a s s I n t e n t i o n D e c ✷✷ {
✷✸ a t t r i b u t e name : S t r i n g [ 1 ] { !ordered, !unique } ;
✷✹ }
✷✺ c l a s s T e s t I n t e n t i o n B o d y
✷✻ {
✷✼ p r o p e r t y axiomDeclaration : AxiomDeclaration [ 1 ] { !ordered,composes } ;
✷✽ p r o p e r t y v a r i a b l e D e c l a r a t i o n : V a r i a b l e D e c l a r a t i o n s : : V a r i a b l e D e c l a r a t i o n [ ? ] { !ordered ,composes } ;
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✷✾ }
✸✵ c l a s s AxiomDeclaration
✸✶ {
✸✷ p r o p e r t y axiom : Axiom [ + ] { !ordered,composes } ;
✸✸ } ✸✹ c l a s s Axiom ✸✺ { ✸✻ p r o p e r t y c o n d i t i o n : C o n d i t i o n [ ? ] { !ordered,composes } ; ✸✼ p r o p e r t y i n c l u s i o n : I n c l u s i o n [ 1 ] { !ordered,composes } ; ✸✽ } ✸✾ c l a s s I n c l u s i o n extends ConditionAtom ✹✵ {
✹✶ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ; ✹✷ p r o p e r t y _ ’ i n ’ : I n t e n t i o n D e c [ 1 ] { !ordered, !unique } ;
✹✸ }
✹✹ c l a s s C o n d i t i o n
✹✺ {
✹✻ p r o p e r t y d o m a i n Q u a n t i f i e r : DomainQuantifier [ ? ] { !ordered,composes } ; ✹✼ p r o p e r t y conditionBody : ConditionBody [ 1 ] { !ordered,composes } ;
✹✽ }
✹✾ c l a s s DomainQuantifier { a b s t r a c t }
✺✵ {
✺✶ p r o p e r t y l i s t : NameList [ 1 ] { !ordered,composes } ;
✺✷ }
✺✸ c l a s s U n i f o r m i t y L i s t extends DomainQuantifier ; ✺✹ c l a s s S u b u n i f o r m i t y L i s t extends DomainQuantifier ; ✺✺ c l a s s ConditionBody
✺✻ {
✺✼ p r o p e r t y conditionAtom : ConditionAtom [ + ] { composes } ;
✺✽ } ✺✾ c l a s s ConditionAtom { a b s t r a c t } ✻✵ { ✻✶ p r o p e r t y next : ConditionAtom [ ? ] ; ✻✷ } ✻✸ c l a s s NameList ✻✹ {
✻✺ p r o p e r t y nameRef : V a r i a b l e D e c l a r a t i o n s : : VariableDec [ + ] { !ordered, !unique } ;
✻✻ }
✻✼ package HMLFormula : HMLFormula = ’SATEL . HMLFormula ’
✻✽ {
✻✾ c l a s s HMLTerm
✼✵ {
✼✶ p r o p e r t y hmlFormula : HMLFormula [ + ] { !ordered,composes } ;
✼✷ }
✼✸ c l a s s HMLFormula { a b s t r a c t }
✼✹ {
✼✺ p r o p e r t y next : HMLFormula [ ? ] ;
✼✻ }
✼✼ c l a s s HMLFormulaHMLFormulaContent extends HMLFormula
✼✽ {
✼✾ p r o p e r t y hmlFormulaContent : HMLFormulaContent [ 1 ] { composes } ;
✽✵ }
✽✶ c l a s s HMLFormulaPrimitiveHMLVarDec extends HMLFormula
✽✷ {
✽✸ p r o p e r t y primitiveHMLVarDec : V a r i a b l e D e c l a r a t i o n s : : PrimitiveHMLVarDec [ 1 ] ;
✽✹ }
✽✺ c l a s s HMLFormulaContent { a b s t r a c t } ; 96
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✽✻ c l a s s HMLNext extends HMLFormulaContent
✽✼ {
✽✽ p r o p e r t y hmlFormulaContent : HMLFormulaContent [ 1 ] { !ordered,composes } ; ✽✾ p r o p e r t y hmlEvent : HMLEvent [ 1 ] { !ordered,composes } ;
✾✵ }
✾✶ c l a s s HMLNot extends HMLFormulaContent
✾✷ {
✾✸ p r o p e r t y hmlFormulaContent : HMLFormulaContent [ 1 ] { !ordered,composes } ;
✾✹ }
✾✺ c l a s s HMLAnd extends HMLFormulaContent
✾✻ {
✾✼ p r o p e r t y hmlFormulaContentL : HMLFormulaContent [ 1 ] { !ordered,composes } ; ✾✽ p r o p e r t y hmlFormulaContentR : HMLFormulaContent [ 1 ] { !ordered,composes } ;
✾✾ }
✶✵✵ c l a s s HMLTop extends HMLFormulaContent ; ✶✵✶ c l a s s HMLEvent
✶✵✷ {
✶✵✸ p r o p e r t y inputTerm : SynchronizationInputTerm [ 1 ] { !ordered,composes } ; ✶✵✹ p r o p e r t y outputTerm : SynchronizationOutputTerm [ ? ] { !ordered,composes } ;
✶✵✺ }
✶✵✻ c l a s s SynchronizationTerm { a b s t r a c t } ;
✶✵✼ c l a s s SynchronizationInputTerm extends SynchronizationTerm { a b s t r a c t } ; ✶✵✽ c l a s s SynchronizationEventInputTerm extends SynchronizationInputTerm
✶✵✾ {
✶✶✵ p r o p e r t y event : InputEvent [ 1 ] ;
✶✶✶ p r o p e r t y parameters : Parameter [ ? ] { composes } ;
✶✶✷ }
✶✶✸ c l a s s SynchronizationOutputTerm extends SynchronizationTerm { a b s t r a c t } ; ✶✶✹ c l a s s SynchronizationEventOutputTerm extends SynchronizationOutputTerm
✶✶✺ {
✶✶✻ p r o p e r t y event : OutputEvent [ 1 ] ;
✶✶✼ p r o p e r t y parameters : Parameter [ ? ] { composes } ;
✶✶✽ }
✶✶✾ c l a s s WPrimitiveObservationVarDec extends SynchronizationOutputTerm
✶✷✵ {
✶✷✶ p r o p e r t y p r i m i t i v e O b s e r v a t i o n : V a r i a b l e D e c l a r a t i o n s : : PrimitiveObservationVarDec [ 1 ] ;
✶✷✷ }
✶✷✸ c l a s s WPrimitiveStimulationVarDec extends SynchronizationInputTerm
✶✷✹ { ✶✷✺ p r o p e r t y p r i m i t i v e S t i m u l a t i o n : V a r i a b l e D e c l a r a t i o n s : : P r i m i t i v e S t i m u l a t i o n V a r D e c [ 1 ] ; ✶✷✻ } ✶✷✼ c l a s s Parameter ✶✷✽ {
✶✷✾ p r o p e r t y value : algterms : : AlgebraicTerm [ 1 ] { composes } ; ✶✸✵ p r o p e r t y next : Parameter [ ? ] { composes } ;
✶✸✶ } ✶✸✷ c l a s s InputEvent { a b s t r a c t } ; ✶✸✸ c l a s s OutputEvent { a b s t r a c t } ; ✶✸✹ } ✶✸✺ package A lg e br a ic Ex p re s si on s : A l ge br a ic E xp re s si o ns = ’SATEL . Al ge b ra i cE xp r es s io ns ’ ✶✸✻ {
✶✸✼ c l a s s A l g e b r a i c E q u a l i t y extends SATEL : : ConditionAtom { a b s t r a c t } ; ✶✸✽ c l a s s A l g E q u a l i t y extends A l g e b r a i c E q u a l i t y
✶✸✾ {
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✶✹✶ p r o p e r t y algebraicTermR : algterms : : AlgebraicTerm [ 1 ] { !ordered,composes } ;
✶✹✷ }
✶✹✸ c l a s s SyncEquality extends A l g e b r a i c E q u a l i t y
✶✹✹ {
✶✹✺ p r o p e r t y synchronizationTermL : HMLFormula : : SynchronizationTerm [ 1 ] { !ordered, composes } ;
✶✹✻ p r o p e r t y synchronizationTermR : HMLFormula : : SynchronizationTerm [ 1 ] { !ordered, composes } ;
✶✹✼ }
✶✹✽ c l a s s HMLEquality extends A l g e b r a i c E q u a l i t y
✶✹✾ {
✶✺✵ p r o p e r t y hmlTermL : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ; ✶✺✶ p r o p e r t y hmlTermR : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✶✺✷ }
✶✺✸ c l a s s BooleanEquality extends A l g e b r a i c E q u a l i t y
✶✺✹ {
✶✺✺ p r o p e r t y booleanTermR : booleanterms : : BooleanTerm [ 1 ] { !ordered,composes } ; ✶✺✻ p r o p e r t y booleanTermL : booleanterms : : BooleanTerm [ 1 ] { !ordered,composes } ;
✶✺✼ }
✶✺✽ c l a s s A r i t h m e t i c E q u a l i t y extends A l g e b r a i c E q u a l i t y
✶✺✾ {
✶✻✵ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✶✻✶ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✶✻✷ }
✶✻✸ package booleanterms : booleanterms = ’SATEL . A l ge b ra ic E xp r es si o ns . booleanterms ’
✶✻✹ {
✶✻✺ c l a s s BooleanTerm extends SATEL : : ConditionAtom { a b s t r a c t } ; ✶✻✻ c l a s s Not extends BooleanTerm
✶✻✼ {
✶✻✽ p r o p e r t y booleanTerm : BooleanTerm [ 1 ] { !ordered,composes } ;
✶✻✾ }
✶✼✵ c l a s s _ ’ Sequence ’ extends BooleanTerm
✶✼✶ {
✶✼✷ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✶✼✸ }
✶✼✹ c l a s s P o s i t i v e extends BooleanTerm
✶✼✺ {
✶✼✻ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✶✼✼ }
✶✼✽ c l a s s Trace extends BooleanTerm
✶✼✾ {
✶✽✵ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✶✽✶ }
✶✽✷ c l a s s BooleanVariable extends BooleanTerm
✶✽✸ {
✶✽✹ p r o p e r t y booleanVariable : V a r i a b l e D e c l a r a t i o n s : : PrimitiveBooleanVarDec [ 1 ] { ! ordered, !unique } ;
✶✽✺ }
✶✽✻ c l a s s BooleanValue extends BooleanTerm
✶✽✼ {
✶✽✽ a t t r i b u t e value : Boolean [ 1 ] { !ordered, !unique } ;
✶✽✾ }
✶✾✵ c l a s s BOPAnd extends BooleanTerm
✶✾✶ {
✶✾✷ p r o p e r t y booleanTermL : BooleanTerm [ 1 ] { !ordered,composes } ; 98
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✶✾✸ p r o p e r t y booleanTermR : BooleanTerm [ 1 ] { !ordered,composes } ;
✶✾✹ }
✶✾✺ c l a s s BOPOr extends BooleanTerm
✶✾✻ {
✶✾✼ p r o p e r t y booleanTermL : BooleanTerm [ 1 ] { !ordered,composes } ; ✶✾✽ p r o p e r t y booleanTermR : BooleanTerm [ 1 ] { !ordered,composes } ;
✶✾✾ }
✷✵✵ c l a s s Equals extends BooleanTerm
✷✵✶ {
✷✵✷ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✵✸ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✵✹ }
✷✵✺ c l a s s NotEquals extends BooleanTerm
✷✵✻ {
✷✵✼ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✵✽ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✵✾ }
✷✶✵ c l a s s GT extends BooleanTerm
✷✶✶ {
✷✶✷ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✶✸ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✶✹ }
✷✶✺ c l a s s LT extends BooleanTerm
✷✶✻ {
✷✶✼ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✶✽ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✶✾ }
✷✷✵ c l a s s GTE extends BooleanTerm
✷✷✶ {
✷✷✷ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✷✸ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✷✹ }
✷✷✺ c l a s s LTE extends BooleanTerm
✷✷✻ {
✷✷✼ p r o p e r t y arithmeticTermR : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ;
✷✷✽ p r o p e r t y arithmeticTermL : a r i t h m e t i c t e r m s : : ArithmeticTerm [ 1 ] { !ordered, composes } ; ✷✷✾ } ✷✸✵ } ✷✸✶ package a r i t h m e t i c t e r m s : a r i t h m e t i c t e r m s = ’SATEL . A l ge b ra ic E xp r es si o ns . a r i t h m e t i c t e r m s ’ ✷✸✷ { ✷✸✸ c l a s s ArithmeticTerm { a b s t r a c t } ; ✷✸✹ c l a s s I n t e g e r V a r i a b l e extends ArithmeticTerm ✷✸✺ {
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore ✷✸✻ p r o p e r t y i n t e g e r V a r i a b l e : V a r i a b l e D e c l a r a t i o n s : : P r i m i t i v e I n t e g e r V a r D e c [ 1 ] { ! ordered, !unique } ; ✷✸✼ } ✷✸✽ c l a s s I n t e g e r V a l u e extends ArithmeticTerm ✷✸✾ {
✷✹✵ a t t r i b u t e value : ecore_0 : : E I n t [ 1 ] { !ordered, !unique } ;
✷✹✶ }
✷✹✷ c l a s s BOPPlus extends ArithmeticTerm
✷✹✸ {
✷✹✹ p r o p e r t y arithmeticTermL : ArithmeticTerm [ 1 ] { !ordered,composes } ; ✷✹✺ p r o p e r t y arithmeticTermR : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✷✹✻ }
✷✹✼ c l a s s BOPMinus extends ArithmeticTerm
✷✹✽ {
✷✹✾ p r o p e r t y arithmeticTermL : ArithmeticTerm [ 1 ] { !ordered,composes } ; ✷✺✵ p r o p e r t y arithmeticTermR : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✷✺✶ }
✷✺✷ c l a s s BOPTimes extends ArithmeticTerm
✷✺✸ {
✷✺✹ p r o p e r t y arithmeticTermR : ArithmeticTerm [ 1 ] { !ordered,composes } ; ✷✺✺ p r o p e r t y arithmeticTermL : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✷✺✻ }
✷✺✼ c l a s s BOPDiv extends ArithmeticTerm
✷✺✽ {
✷✺✾ p r o p e r t y arithmeticTermL : ArithmeticTerm [ 1 ] { !ordered,composes } ; ✷✻✵ p r o p e r t y arithmeticTermR : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✷✻✶ }
✷✻✷ c l a s s NBEvents extends ArithmeticTerm
✷✻✸ {
✷✻✹ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✷✻✺ }
✷✻✻ c l a s s Depth extends ArithmeticTerm
✷✻✼ {
✷✻✽ p r o p e r t y hmlTerm : HMLFormula : : HMLTerm [ 1 ] { !ordered,composes } ;
✷✻✾ }
✷✼✵ c l a s s UOPMinus extends ArithmeticTerm
✷✼✶ {
✷✼✷ p r o p e r t y a r i t h m e t i c T e r m : ArithmeticTerm [ 1 ] { !ordered,composes } ;
✷✼✸ }
✷✼✹ }
✷✼✺ package algterms : algterms = ’SATEL . A l ge b ra ic E xp r es si o ns . algterms ’
✷✼✻ { ✷✼✼ c l a s s AlgebraicTerm { a b s t r a c t } ✷✼✽ { ✷✼✾ p r o p e r t y next : AlgebraicTerm [ ? ] ; ✷✽✵ } ✷✽✶ c l a s s V a r i a b l e R e f extends AlgebraicTerm ✷✽✷ {
✷✽✸ p r o p e r t y var : V a r i a b l e D e c l a r a t i o n s : : AlgebraicSortVarDec [ 1 ] { !ordered, !unique } ;
✷✽✹ }
✷✽✺ c l a s s AbstractCompositeTerm extends AlgebraicTerm { a b s t r a c t }
✷✽✻ {
✷✽✼ p r o p e r t y terms : AlgebraicTerm [ ∗ ] { !ordered,composes } ; ✷✽✽ p r o p e r t y op : adtmm : : Operation [ 1 ] { !ordered, !unique } ; ✷✽✾ a t t r i b u t e i t e r : ecore_0 : : E I n t [ ? ] = ’ 0 ’ ;
✷✾✵ }
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✷✾✶ c l a s s CompositeTerm extends AbstractCompositeTerm ;
✷✾✷ } ✷✾✸ } ✷✾✹ package V a r i a b l e D e c l a r a t i o n s : V a r i a b l e D e c l a r a t i o n s = ’SATEL . V a r i a b l e D e c l a r a t i o n s ’ ✷✾✺ { ✷✾✻ c l a s s V a r i a b l e D e c l a r a t i o n ✷✾✼ {
✷✾✽ p r o p e r t y v a r i a b l e : VariableDec [ ∗ ] { !ordered,composes } ;
✷✾✾ }
✸✵✵ c l a s s VariableDec { a b s t r a c t }
✸✵✶ {
✸✵✷ a t t r i b u t e name : S t r i n g [ 1 ] { !ordered, !unique } ;
✸✵✸ }
✸✵✹ c l a s s PrimitiveHMLVarDec extends VariableDec
✸✵✺ {
✸✵✻ p r o p e r t y type : Types : : PrimitiveHML [ ? ] { !ordered,composes } ;
✸✵✼ }
✸✵✽ c l a s s P r i m i t i v e S t i m u l a t i o n V a r D e c extends VariableDec
✸✵✾ {
✸✶✵ p r o p e r t y type : Types : : P r i m i t i v e S t i m u l a t i o n [ ? ] { !ordered,composes } ;
✸✶✶ }
✸✶✷ c l a s s PrimitiveObservationVarDec extends VariableDec
✸✶✸ {
✸✶✹ p r o p e r t y type : Types : : P r i m i t i v e O b s e r v a t i o n [ ? ] { !ordered,composes } ;
✸✶✺ }
✸✶✻ c l a s s P r i m i t i v e I n t e g e r V a r D e c extends VariableDec
✸✶✼ {
✸✶✽ p r o p e r t y type : Types : : P r i m i t i v e I n t e g e r [ ? ] { !ordered,composes } ;
✸✶✾ }
✸✷✵ c l a s s PrimitiveBooleanVarDec extends VariableDec
✸✷✶ {
✸✷✷ p r o p e r t y type : Types : : P r i m i t i v e B o o l e a n [ ? ] { !ordered,composes } ;
✸✷✸ }
✸✷✹ c l a s s AlgebraicSortVarDec extends VariableDec
✸✷✺ {
✸✷✻ p r o p e r t y type : adtmm : : S o r t D e c l a r a t i o n [ 1 ] { !ordered } ;
✸✷✼ }
✸✷✽ package Types : Types = ’SATEL . V a r i a b l e D e c l a r a t i o n s . Types ’
✸✷✾ {
✸✸✵ c l a s s VarDecType { a b s t r a c t } ;
✸✸✶ c l a s s PrimitiveHML extends VarDecType ;
✸✸✷ c l a s s P r i m i t i v e S t i m u l a t i o n extends VarDecType ; ✸✸✸ c l a s s P r i m i t i v e O b s e r v a t i o n extends VarDecType ; ✸✸✹ c l a s s P r i m i t i v e I n t e g e r extends VarDecType ; ✸✸✺ c l a s s P r i m i t i v e B o o l e a n extends VarDecType ; ✸✸✻ } ✸✸✼ }
✸✸✽ package APN : APN = ’SATEL .APN ’
✸✸✾ {
✸✹✵ package apnmm : apnmm = ’SATEL .APN.apnmm ’
✸✹✶ {
✸✹✷ c l a s s APN extends environmentmm : : Environment
✸✹✸ {
✸✹✹ p r o p e r t y ownedPlaces : Place [ + ] { composes } ; ✸✹✺ p r o p e r t y ownedArcs : Arc [ ∗ ] { composes } ;
✸✹✻ p r o p e r t y ownedVariables : adtmm : : V a r i a b l e [ ∗ ] { composes } ; ✸✹✼ a t t r i b u t e name : S t r i n g [ 1 ] ;
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✸✹✽ p r o p e r t y methods : Method [ ∗ ] { composes } ; ✸✹✾ p r o p e r t y gates : Gate [ ∗ ] { composes } ;
✸✺✵ p r o p e r t y ownedTransitions : T r a n s i t i o n [ + ] { composes } ; ✸✺✶ } ✸✺✷ c l a s s Node { a b s t r a c t } ✸✺✸ { ✸✺✹ a t t r i b u t e name : S t r i n g [ 1 ] ; ✸✺✺ } ✸✺✻ c l a s s Arc ✸✺✼ { ✸✺✽ p r o p e r t y from : Node [ 1 ] ; ✸✺✾ p r o p e r t y t o : Node [ 1 ] ;
✸✻✵ p r o p e r t y ownedArcMultiset : multisetmm : : M u l t i s e t [ 1 ] { composes } ; ✸✻✶ a t t r i b u t e Name : S t r i n g [ ? ] ;
✸✻✷ }
✸✻✸ c l a s s Place extends Node
✸✻✹ {
✸✻✺ p r o p e r t y ownedPlaceMultiset : multisetmm : : M u l t i s e t [ 1 ] { composes } ; ✸✻✻ p r o p e r t y s o r t : adtmm : : Sort [ 1 ] { composes } ;
✸✻✼ }
✸✻✽ c l a s s T r a n s i t i o n extends Node
✸✻✾ {
✸✼✵ p r o p e r t y ownedGuard : guardmm : : Guard [ ? ] { composes } ; ✸✼✶ p r o p e r t y g a t e C a l l s : GateCall [ ∗ ] { composes } ; ✸✼✷ p r o p e r t y methodCall : MethodCall [ ? ] { composes } ;
✸✼✸ }
✸✼✹ c l a s s Method extends HMLFormula : : InputEvent
✸✼✺ {
✸✼✻ a t t r i b u t e name : S t r i n g [ 1 ] ;
✸✼✼ }
✸✼✽ c l a s s Gate extends HMLFormula : : OutputEvent
✸✼✾ { ✸✽✵ a t t r i b u t e name : S t r i n g [ 1 ] ; ✸✽✶ } ✸✽✷ c l a s s GateCall ✸✽✸ { ✸✽✹ p r o p e r t y gate : Gate [ 1 ] ;
✸✽✺ p r o p e r t y params : adtmm : : Term [ ∗ ] { composes } ; ✸✽✻ p r o p e r t y next : GateCall [ ? ] ;
✸✽✼ }
✸✽✽ c l a s s MethodCall
✸✽✾ {
✸✾✵ p r o p e r t y method : Method [ 1 ] ;
✸✾✶ p r o p e r t y params : adtmm : : Term [ ∗ ] { composes } ;
✸✾✷ }
✸✾✸ a n n o t a t i o n S t a t i c _ c h e c k s ( ’ 0 ’ = ’ an arc must go from a t r a n s i t i o n t o a place , or from a place t o a t r a n s i t i o n ’ , ’ 1 ’ =
✸✾✹ ’ Check t h a t t h e r e i s a t l e a s t one place ’ , ’ 2 ’ = ’ Check arc s o r t ’ , ’ 3 ’ = ✸✾✺ ’ Check t h a t the v a r i a b l e s i n the post c o n d i t i o n s and guards are present i n the
p r e c o n d i t i o n s ’ ) ;
✸✾✻ }
✸✾✼ package environmentmm : environmentmm = ’SATEL .APN. environmentmm ’
✸✾✽ {
✸✾✾ c l a s s Environment { a b s t r a c t } ;
✹✵✵ }
✹✵✶ package guardmm : guardmm = ’SATEL .APN. guardmm ’
✹✵✷ {
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore
✹✵✸ c l a s s Guard extends environmentmm : : Environment
✹✵✹ {
✹✵✺ p r o p e r t y ownedEquations : adtmm : : A b s t r a c t E q u a t i o n [ + ] { composes } ; ✹✵✻ p r o p e r t y ownedVariables : adtmm : : V a r i a b l e [ ∗ ] { composes } ;
✹✵✼ }
✹✵✽ }
✹✵✾ package adtmm : adtmm = ’SATEL .APN. adtmm ’
✹✶✵ {
✹✶✶ c l a s s ADT extends environmentmm : : Environment
✹✶✷ {
✹✶✸ p r o p e r t y ownedSorts : S o r t D e c l a r a t i o n [ ∗ ] { composes } ; ✹✶✹ p r o p e r t y ownedOperations : Operation [ ∗ ] { composes } ; ✹✶✺ p r o p e r t y ownedGenerators : Operation [ ∗ ] { composes } ; ✹✶✻ p r o p e r t y ownedVariables : V a r i a b l e [ ∗ ] { composes } ; ✹✶✼ p r o p e r t y ownedAxioms : CondEquation [ ∗ ] { composes } ; ✹✶✽ a t t r i b u t e name : S t r i n g [ 1 ] ; ✹✶✾ } ✹✷✵ c l a s s Sor t extends A b s t r a c t S o r t ; ✹✷✶ c l a s s Operation extends A b s t r a c t O p e r a t i o n ✹✷✷ { ✹✷✸ p r o p e r t y o p e r a t i o n S o r t s : Sort [ ∗ ] { composes } ; ✹✷✹ p r o p e r t y r e s u l t : Sort [ 1 ] { composes } ; ✹✷✺ } ✹✷✻ c l a s s V a r i a b l e ✹✷✼ { ✹✷✽ a t t r i b u t e name : S t r i n g [ 1 ] ; ✹✷✾ p r o p e r t y v a r i a b l e S o r t : Sort [ ? ] { composes } ; ✹✸✵ } ✹✸✶ c l a s s CondEquation ✹✸✷ { ✹✸✸ p r o p e r t y ownedConditions : A b s t r a c t E q u a t i o n [ ∗ ] { composes } ; ✹✸✹ p r o p e r t y ownedEquation : Equation [ 1 ] { composes } ;
✹✸✺ } ✹✸✻ c l a s s Term { a b s t r a c t } ✹✸✼ { ✹✸✽ p r o p e r t y next : Term [ ? ] ; ✹✸✾ } ✹✹✵ c l a s s V a r i a b l e R e f extends Term ✹✹✶ { ✹✹✷ p r o p e r t y v a r i a b l e : V a r i a b l e [ 1 ] ; ✹✹✸ }
✹✹✹ c l a s s CTerm extends Term
✹✹✺ {
✹✹✻ a t t r i b u t e i t e r : ecore_0 : : E I n t [ ? ] ;
✹✹✼ p r o p e r t y ownedTerms : Term [ ∗ ] { composes } ; ✹✹✽ p r o p e r t y op : Operation [ 1 ] ;
✹✹✾ }
✹✺✵ c l a s s A b s t r a c t E q u a t i o n { a b s t r a c t }
✹✺✶ {
✹✺✷ p r o p e r t y ownedRightTerm : Term [ 1 ] { composes } ; ✹✺✸ p r o p e r t y ownedLeftTerm : Term [ 1 ] { composes } ; ✹✺✹ p r o p e r t y next : A b s t r a c t E q u a t i o n [ ? ] ;
✹✺✺ }
✹✺✻ c l a s s Equation extends A b s t r a c t E q u a t i o n ; ✹✺✼ c l a s s I n e q u a t i o n extends A b s t r a c t E q u a t i o n ; ✹✺✽ c l a s s A b s t r a c t S o r t { a b s t r a c t,i n t e r f a c e } ; ✹✺✾ c l a s s AtomicSort extends Sor t
A. APPENDIX A.1. Metamodelo do SATEL em OCLinEcore ✹✻✵ { ✹✻✶ p r o p e r t y d e c l a r a t i o n : S o r t D e c l a r a t i o n [ 1 ] ; ✹✻✷ } ✹✻✸ c l a s s S o r t D e c l a r a t i o n ✹✻✹ { ✹✻✺ a t t r i b u t e name : S t r i n g [ 1 ] ; ✹✻✻ } ✹✻✼ c l a s s A b s t r a c t O p e r a t i o n { a b s t r a c t,i n t e r f a c e } ✹✻✽ { ✹✻✾ a t t r i b u t e name : S t r i n g [ 1 ] ; ✹✼✵ } ✹✼✶ c l a s s AbstractGenericOp extends A b s t r a c t O p e r a t i o n { a b s t r a c t,i n t e r f a c e } ;
✹✼✷ a n n o t a t i o n StaticChecks ( ’ 1 ’ = ’ Check t h a t a composite term has as many subterms as i t s Operation has s o r t s . ’ , ’ 2 ’ =
✹✼✸ ’ Check t h a t the i t e r t h e o r y i s o nly a p p l i e d i f t h e r e i s only one subterm . ’ , ’ 3 ’ =
✹✼✹ ’ Check t h a t t h a r e are not any f r e e v a r i a b l e s i n the CondEquation c o n d i t i o n s . ’ , ’ 4 ’ =
✹✼✺ ’ Check t h a t t h e r e are o nly renames i f t h e r e i s an i n s t a n t i a t i o n , and which are the c o r r e c t renames . ’ ) ;
✹✼✻ a n n o t a t i o n N o t e s _ a b o u t _ v i s i t o r s ( ’ ’ =
✹✼✼ ’ A b s t r a c t S o r t , A b s t r a c t G e n e r i c S o r t , AbstractOperation , AbstracGenericOperation and I n s t a n t i a b l e do not implement any v i s i t o r ’ ) ;
✹✼✽ }
✹✼✾ package multisetmm : multisetmm = ’SATEL .APN. multisetmm ’
✹✽✵ {
✹✽✶ c l a s s M u l t i s e t extends environmentmm : : Environment
✹✽✷ {
✹✽✸ p r o p e r t y msSort : adtmm : : Sort [ ? ] { composes } ;
✹✽✹ p r o p e r t y ownedNumOfTerms : NumOfTerms [ ∗ ] { composes } ; ✹✽✺ p r o p e r t y ownedVariables : adtmm : : V a r i a b l e [ ∗ ] { composes } ;
✹✽✻ }
✹✽✼ c l a s s NumOfTerms
✹✽✽ {
✹✽✾ a t t r i b u t e card : ecore_0 : : E I n t [ 1 ] = ’ 1 ’ ;
✹✾✵ p r o p e r t y ownedElement : MSElement [ 1 ] { composes } ; ✹✾✶ p r o p e r t y next : NumOfTerms [ ? ] ;
✹✾✷ }
✹✾✸ c l a s s MSElement { a b s t r a c t } ;
✹✾✹ c l a s s TermReference extends MSElement
✹✾✺ {
✹✾✻ p r o p e r t y termReferenced : adtmm : : Term [ 1 ] { composes } ;
✹✾✼ }
✹✾✽ }
✹✾✾ }
✺✵✵ }