Jou nal o Objec Technology
Published by AITO — Associa ion In e na ionale pou les Technologies Obje s, c
JOT 2011
Online a h p://www.jo . m.
A Rew i ing Logic Seman ics o ATL
Ja ie T oyaaAn onio Vallecilloa
a. GISUM/A enea Resea ch G oup. Uni e sidad de M´alaga, Spain.
Abs ac As he complexi y o model ans o ma ion (MT) g ows, he
need o ely on o mal seman ics o MT languages becomes a c i ical issue.
Fo mal seman ics p o ide p ecise speci ica ions o he expec ed beha io
o ans o ma ions, allowing use s o unde s and hem and o use hem
p ope ly, and MT ool builde s o de elop co ec MT engines, compile s,
e c. In addi ion, o mal seman ics allow modele s o eason abou he MTs
and o p o e hei co ec ness, some hing specially impo an in case o
la ge and complex MTs (wi h, e.g., hund eds o housands o ules) o
which manual debugging is no longe possible. In his pape we gi e a
o mal seman ics o he ATL 3.0 model ans o ma ion language using
ew i ing logic and Maude, which allows add essing hese issues. Such
o maliza ion p o ides addi ional bene i s, such as enabling he simula ion
o he speci ica ions o gi ing access o he Maude oolki o eason abou
hem.
Keywo ds ATL; Maude; Model T ans o ma ion; seman ics.
1 In oduc ion
Model ans o ma ions (MT) a e a he hea o Model-D i en Enginee ing, and p o-
ide he essen ial mechanisms o manipula ing and ans o ming models. As he
complexi y o model ans o ma ions g ows, he need o ely on o mal seman ics
o MT languages also inc eases. Fo mal seman ics p o ide p ecise speci ica ions o
he expec ed beha io o he ans o ma ions, which a e c ucial o use s o be able
o unde s and and use model ans o ma ions p ope ly, and o ool builde s o de-
elop co ec model ans o ma ion engines, compile s, op imize s, debugge s, e c.
Fu he mo e, MT p og amme s need o know he expec ed beha io o he ules and
ans o ma ions hey w i e, in o de o eason abou hem and p o e hei co ec ness.
This is specially impo an in case o la ge and complex MTs (wi h, e.g., hund eds o
housands o ules) o which manual debugging is no longe possible. Fo ins ance, in
he case o ule-based model ans o ma ion languages, p o ing ha he speci ica ions
a e con luen and e mina ing is equi ed. Also, looking o non- igge ed ules may
help de ec ing po en ial design p oblems in la ge MT sys ems.
ATL [JABK08] is one o he mos popula and widely used model ans o ma ion
languages. As usual in he communi y, he ATL language has been desc ibed in an
in ui i e and in o mal manne , by means o de ini ions o i s main ea u es in na u al
Ja ie T oya, An onio Vallecillo. A Rew i ing Logic Seman ics o ATL. In Jou nal o Objec
Technology, ol. 10, 2011, pages 5:1–29. doi:10.5381/jo .2011.10.1.a5
2·Ja ie T oya, An onio Vallecillo
Figu e 1 – ATL model ans o ma ion schema.
language. Howe e , his lack o igo ous desc ip ion can easily lead o imp ecisions
and misunde s andings ha migh hinde he p ope usage and analysis o he lan-
guage, and he de elopmen o co ec and in e ope able ools. The o he e e ence
implemen a ion o ATL is a ailable as me amodels o he language and i s i ual
machine, and as a compile om he language o he i ual machine and an in e -
p e e o he i ual machine. The p oblem o his kind o implemen a ion is ha i
is no abs ac enough o p o ide meaning ul seman ics, and in an implemen a ion-
independen manne .
In his pape we in es iga e he use o ew i ing logic [Mes92], and i s implemen a-
ion in Maude [CDE+07], o gi ing seman ics o ATL. The use o Maude as a a ge
seman ic domain b ings e y in e es ing bene i s, because i enables he simula ion o
he ATL speci ica ions and he o mal analysis o he ATL p og ams. In his sense,
we p o ide a mo e abs ac encoding han he ATL cu en implemen a ion, oge he
wi h an al e na i e speci ica ion o he ans o ma ions ha can be simula ed and
analyzed o co ec ness.
This pape is an ex ension o he one p esen ed in he ICMT’10 con e ence [TV10a].
He e we deal wi h all new ea u es o ATL e sion 3.0, and in pa icula we o mal-
ize he ATL e ining mode — in addi ion o he ATL de aul execu ion seman ics.
Fu he mo e, we discuss some imp o emen s in he Maude ep esen a ion o he ATL
ules o ob ain be e pe o mance when simula ing he ATL speci ica ions. New ATL
examples a e also shown in his pape .
The s uc u e o he documen is as ollows. A e his in oduc ion, sec ions 2
and 3 p o ide an in oduc ion o ATL and Maude, espec i ely. Then, sec ion 4
p esen s how ATL language cons uc s can be encoded in Maude, and sec ion 5 de-
sc ibes he cu en ool suppo . Finally, sec ion 6 compa es ou wo k wi h o he
ela ed p oposals, and sec ion 7 d aws some conclusions and ou lines some u u e
esea ch ac i i ies.
2 T ans o ma ions wi h ATL
ATL is a hyb id model ans o ma ion language con aining a mix u e o decla a i e
and impe a i e cons uc s. ATL ans o ma ions a e unidi ec ional, ope a ing on
ead-only sou ce models and p oducing w i e-only a ge models (Fig. 1). Du ing he
execu ion o a ans o ma ion, sou ce models may be na iga ed bu changes a e no
allowed. Ta ge models canno be na iga ed.
ATL modules de ine he ans o ma ions. A module con ains a manda o y heade
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·3
(a) Sou ce me amodel. (b) Ta ge me amodel.
Figu e 2 – Me amodels used in he example ans o ma ion.
sec ion, an impo sec ion, and a numbe o helpe s and ans o ma ion ules. The
heade sec ion p o ides he name o he ans o ma ion module and decla es he sou ce
and a ge models (which a e yped by hei me amodels). Helpe s and ans o ma ion
ules a e he cons uc s used o speci y he ans o ma ion unc ionali y.
Decla a i e ATL ules a e called ma ched ules and lazy ules. Lazy ules a e
like ma ched ules, bu a e only applied when called by ano he ule. They bo h
speci y ela ions be ween sou ce pa e ns and a ge pa e ns. The sou ce pa e n
o a ule speci ies a se o sou ce ypes and an op ional gua d gi en as a Boolean
exp ession in OCL. A sou ce pa e n is e alua ed o a se o ma ches in sou ce models.
The a ge pa e n is composed o a se o elemen s. Each o hese elemen s speci ies
a a ge ype om he a ge me amodel and a se o bindings. A binding e e s o a
ea u e o he ype (i.e., an a ibu e, a e e ence o an associa ion end) and speci ies
an exp ession whose alue is used o ini ialize he ea u e. Lazy ules can be called
se e al imes using a collec cons uc . Unique lazy ules a e a special kind o lazy
ules ha always e u n he same a ge elemen o a gi en sou ce elemen . The
a ge elemen is e ie ed by na iga ing he in e nal aceabili y links, as in no mal
ules. Non-unique lazy ules do no na iga e he aceabili y links bu c ea e new
a ge elemen s in each execu ion.
In some cases, complex ans o ma ion algo i hms may be equi ed, and i may
be di icul o speci y hem in a decla a i e way. Fo his eason ATL p o ides wo
impe a i e cons uc s: called ules and ac ion blocks. A called ule is a ule called
by o he s like a p ocedu e. An ac ion block is a sequence o impe a i e s a emen s
and can be used ins ead o o in combina ion wi h a a ge pa e n in ma ched o
called ules. The impe a i e s a emen s in ATL a e he usual cons uc s o a ibu e
assignmen and con ol low: condi ions and loops.
ATL also p o ides he esol eTemp ope a ion o dealing wi h complex ans o -
ma ions. This ope a ion allows o e e o any o he a ge model elemen s gene a ed
om a gi en sou ce model elemen : esol eTemp(s cObj, a ge Pa e nName). The i s
a gumen is he sou ce model elemen , and he second is a s ing wi h he name o
he a ge pa e n elemen . This ope a ion can be called om he a ge pa e n and
impe a i e sec ions o any ma ched o called ule.
ATL has wo execu ion modes, he no mal (de aul ) execu ion mode and he e in-
Jou nal o Objec Technology, ol. 10, 2011
4·Ja ie T oya, An onio Vallecillo
ing one. In he o me , he ATL de elope has o speci y, ei he by ma ched o called
ules, he way o gene a e each o he expec ed a ge model elemen s. This execu-
ion mode sui s o mos ATL ans o ma ions whe e sou ce and a ge me amodels
a e di e en . Using he e ining mode, ATL de elope s can de ine ans o ma ions
ha modi y he sou ce model o ob ain he a ge model, since bo h models con o m
o he same me amodel. This mode is u he explained in sec ion 2.1.
In o de o illus a e ou p oposal o he ATL de aul execu ion mode we will
use he example o Ja aSou ce2Table model ans o ma ion [Ecl10], whose code is
shown below. I has wo ma ched ules, wo lazy ules and wo helpe s. The comple e
desc ip ion o his example and i s encoding in Maude can be ound in he echnical
epo [TBV10]. Al hough he ATL ules a e mos ly sel -explana o y, eade s no
luen in ATL can also consul [JABK08, TV10b] o mo e de ails and examples.
module Ja aSou ce2Table;
c ea e OUT :Table om IN :Ja aSou ce;
helpe de :allMe hodDe s :Sequence(Ja aSou ce!Me hodDe ini ion) =
Ja aSou ce!Me hodDe ini ion.allIns ances()
−>so edBy(e|e.class.name +’_’ +e.name)
−>asSequence() ;
helpe con ex Ja aSou ce!Me hodDe ini ion
de :compu eCon en (col :Ja aSou ce!Me hodDe ini ion) : S ing =
sel .in oca ions −>selec (i|i.me hod.name =col.name and
i.me hod.class.name =col.class.name)−>size();
ule Main {
om s:Ja aSou ce!Ja aSou ce
o :Table!Table (
ows <−Sequence{ i s _ ow, hisModule.allMe hodDe s−>
collec (e| hisModule. esol eTemp(e,’ ow’)) }
),
i s _ ow :Table!Row (cells <−
Sequence{ i s _col, hisModule.allMe hodDe s
−>collec (e| hisModule.ge Con en Fi s Row(e))}),
i s _col :Table!Cell (con en <−’’)
}
ule Me hodDe ini ion {
om m:Ja aSou ce!Me hodDe ini ion
o ow :Table!Row (cells <−Sequence{ i le_cel, hisModule.allMe hodDe s −>
collec (e| hisModule.ge Compu eCon en (m,e))}),
i le_cel :Table!Cell (con en <−m.class.name +’.’ +m.name
}
lazy ule ge Con en Fi s Row {
om m:Ja aSou ce!Me hodDe ini ion
o c:Table!Cell (con en <−m.class.name +’.’ +m.name)
}
lazy ule ge Compu eCon en {
om m1 :Ja aSou ce!Me hodDe ini ion,
m2 :Ja aSou ce!Me hodDe ini ion
o c:Table!Cell (con en <−m1.compu eCon en (m2). oS ing() )
}
The inpu model we ha e used in ou ans o ma ions examples con ains a Ja a-
Sou ce wi h wo ClassDecla a ions. I is shown in Fig. 3. I s co esponding a ge
model when he Ja aSou ce2Table ans o ma ion is applied o e i is he Table model
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·5
Figu e 3 –Ja aSou ce inpu model.
Figu e 4 –Table a ge model.
shown in Fig. 4. A isual explana ion o how he ans o ma ion wo ks is shown in
Fig. 5.
2.1 ATL Re ining Mode
ATL also de ines ano he execu ion mode, in case he ans o ma ion modi ies he
sou ce model. This is he ATL e ining mode, in which he ans o ma ion de ines he
elemen s ha should be changed and how. The es o he elemen s in he model a e
implici ly copied by he ATL engine wi hou modi ica ions.
In he 2004 e sion o ATL, he copying was pe o med implici ly only o con-
ained elemen s o copied elemen s, and i was manda o y o speci y all bindings.
The e o o copying some elemen s o a ans o ma ion, while modi ying o he s, was
educed in he nex e sion o he ATL language in 2006, which in oduced some
changes o he e ining mode. In his new e sion e e y elemen s ays unchanged i
i is no explici ly ma ched by any o he ans o ma ion ules. Howe e , he 2006
e sion did no p o ide suppo o he dele ion o elemen s. The new ATL 2010
compile implemen s a ull in-place s a egy, whe e elemen s can be dele ed by he
ules, and also e e se bindings o he i s ou pu pa e n elemen a e suppo ed.
T ans o ma ions in his mode a e pe o med in wo s eps. In he i s s ep, he ans-
o ma ion engine execu es he ules which, as a esul , p oduce a se o changes ha
is empo a ily s o ed. In he second s ep, his se o changes is applied di ec ly on
he sou ce model. Dele ion is possible using he “d op” keywo d in he o pa e n.
Le us illus a e his execu ion mode using he well-known example o he Pub-
lic2P i a e ans o ma ion, which makes all public a ibu es o a UML model p i a e.
Ge e s and se e s a e also c ea ed app op ia ely, as shown below.
module Public2P i a e;
c ea e OUT :UML e ining IN :UML;
helpe con ex S ing de : oU1Case :S ing =
sel .subs ing(1,1). oUppe () + sel .subs ing(2,sel .size());
ule P ope y {
om publicA ibu e :
Jou nal o Objec Technology, ol. 10, 2011

6·Ja ie T oya, An onio Vallecillo
Figu e 5 – Visual explana ion o he ans o ma ion.
UML!P ope y (publicA ibu e. isibili y = #public)
o p i a eA ibu e :
UML!P ope y ( isibili y <−#p i a e),
ge e :UML!Ope a ion (name <−’ge ’+publicA ibu e.name. oU1Case,
class <−publicA ibu e. e Immedia eComposi e(),
ype <−publicA ibu e. ype),
se e :UML!Ope a ion (name <−’se ’+publicA ibu e.name. oU1Case,
class <−publicA ibu e. e Immedia eComposi e(),
ownedPa ame e <−se e Pa am),
se e Pa am :UML!Pa ame e (name <−publicA ibu e.name,
ype <−publicA ibu e. ype)}
De ailed in o ma ion abou his ans o ma ion can be ound in [Ecl10]. The
e e ence me amodel is a simpli ica ion o he UML me amodel wi h only he ele an
in o ma ion o his example, and is shown in Fig. 6.
3 Rew i ing Logic and Maude
Maude [CDE+07] is a high-le el language and a high-pe o mance in e p e e in he
OBJ algeb aic speci ica ion amily ha suppo s membe ship equa ional logic [BJM00]
and ew i ing logic [Mes92] speci ica ion and p og amming o sys ems. Thus, Maude
in eg a es an equa ional s yle o unc ional p og amming wi h ew i ing logic com-
pu a ion. We in o mally desc ibe in his sec ion hose Maude’s ea u es necessa y
o unde s anding he pape ; he in e es ed eade is e e ed o [CDE+07] o mo e
de ails.
Rew i ing logic is a logic o change ha can na u ally deal wi h s a e and wi h
highly nonde e minis ic concu en compu a ions. A sys em is axioma ized in ew i -
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·7
Figu e 6 – Me amodel used in he Public2P i a e ans o ma ion.
ing logic by a ew i e heo y R= (Σ,E,R), whe e (Σ,E) is an equa ional heo y
desc ibing i s se o s a es as he algeb aic da a ype TΣ/Eassocia ed o he ini ial
algeb a (Σ,E), and Ris a collec ion o ew i e ules. Maude’s unde lying equa ional
logic is membe ship equa ional logic [BJM00], a Ho n logic whose a omic sen ences
a e equali ies = 0and membe ship asse ions o he o m :S, s a ing ha a e m
has so S. Such a logic ex ends o de -so ed equa ional logic, and suppo s so s,
subso ela ions, subso o e loading o ope a o s, and de ini ion o pa ial unc ions
wi h equa ionally de ined domains.
Rew i e ules, which a e w i en c l [l] : => 0i Cond, wi h l he ule label,
and 0 e ms, and Cond a condi ion, desc ibe he local, concu en ansi ions ha
a e possible in he sys em, i.e., when a pa o he sys em s a e i s he pa e n , hen
i can be eplaced by he co esponding ins an ia ion o 0. The gua d Cond ac s as
a blocking p econdi ion, in he sense ha a condi ional ule can be i ed only i i s
condi ion holds.
A condi ion is w i en EqCond1/ ... / EqCondnwhe e each o he EqCondi
is ei he an o dina y equa ion = 0, a ma ching equa ion := 0, a so cons ain
:s, o a e m o so Bool, abb e ia ing he equa ion = ue. In he execu ion
o a ma ching equa ion := 0, he a iables o he e m , which may no appea in
he le hand side o he co esponding condi ional equa ion, become ins an ia ed by
ma ching he e m agains he canonical o m o he bounded subjec e m 0.
4 Encoding ATL in Maude
To gi e a o mal seman ics o ATL using ew i ing logic, we p o ide a ep esen a ion
o he ATL cons uc s and o hei beha io in Maude. We s a by de ining how
he models and me amodels handled by ATL can be encoded in Maude, and hen
we p o ide he seman ics o ma ched ules, lazy ules, unique lazy ules, helpe s,
impe a i e sec ions, he esol eTemp unc ion and he e ining execu ion mode. One
o he bene i s o such an encoding is ha i is sys ema ic and can be au oma ed,
some hing we a e cu en ly implemen ing using ATL ans o ma ions (be ween he
ATL and Maude me amodels).
Jou nal o Objec Technology, ol. 10, 2011
8·Ja ie T oya, An onio Vallecillo
Figu e 7 – Elemen s o a ela ion R(M,N).
4.1 Cha ac e izing Model T ans o ma ions
In ou iew, a model ans o ma ion is jus an algo i hmic speci ica ion (le i be
decla a i e o ope a ional) associa ed o a ela ion R⊆MMS×MMTde ined be ween
wo me amodels which allows o ob ain a a ge model MTcon o ming o MMT
om a sou ce model MS ha con o ms o me amodel MMS[S e07]. In he mos
gene al case, a model ans o ma ion can be de ined be ween mul iple sou ce and
a ge me amodels. In his case MMSand MMT ep esen se s o me amodels.
The idea suppo ing ou p oposal conside s ha model ans o ma ions combine
wo di e en aspec s: s uc u e and beha io . The o me aspec de ines he s uc-
u al ela ion R ha should hold be ween sou ce and a ge models, whils he la e
desc ibes how he speci ic sou ce model elemen s a e ans o med in o a ge model
elemen s. This sepa a ion allows di e en ia ing be ween he ela ion ha he model
ans o ma ion ensu es om he algo i hm i ac ually uses o compu e he a ge
model.
Thus, o ep esen he s uc u al aspec s o a ans o ma ion we will use h ee
models: he sou ce model MS, he a ge model MT ha he ans o ma ion builds,
and he ela ion R(MS,MT) be ween he wo. R(MS,MT) is also called he ace
model, ha speci ies how he elemen s o MSand MTa e consis en ly ela ed by
R. Please no e ha each elemen io R(MS,MT) = { 1, ..., k} ⊆ P(MS)×P(MT)
ela es a se o elemen s o MSwi h a se o elemen s o MT(see Fig. 7).
The beha io al aspec s o an ATL ans o ma ion (i.e., how he ans o ma ion
p og essi ely builds he a ge model elemen s om he sou ce model, and he aces
be ween hem) is de ined using he di e en kinds o ules (ma ched, lazy, unique
lazy); hei possible combina ions and di ec in oca ion om o he ules, and he
inal impe a i e algo i hms ha can be in oked a e each ule.
4.2 Encoding Models and Me amodels in Maude
We will ollow he ep esen a ion o models and me amodels in oduced in [RVD09],
which is inspi ed by he Maude ep esen a ion o objec -o ien ed sys ems. We ep e-
sen models in Maude as s uc u es o so @Model o he o m mm{obj1obj2... objN},
whe e mm is he name o he me amodel and objia e he objec s o he model. An
objec is a eco d-like s uc u e <o:c|a1: 1, ..., an: n>(o so @Objec ), whe e
ois he objec iden i ie (o so Oid), cis he class he objec belongs o (o so
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·9
@Class), and ai: ia e a ibu e- alue pai s (o so @S uc u alFea u eIns ance).
Gi en he app op ia e de ini ions o all classes, a ibu es and e e ences in i s
co esponding me amodel (as we shall see below), he ollowing Maude e m desc ibes
he inpu model shown in sec ion 2.
@ja asou cemm@ {
<’s:Ja aSou ce@ja asou cemm |
classes@Ja aSou ce@ja asou cemm :Sequence[ ’c1 ; ’c2 ]>
<’c1 :ClassDecla a ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"Fi s Class" #
me hods@ClassDecla a ion@ja asou cemm :Sequence[ ’m1 ; ’m2 ]>
<’m1 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :" c_m1" #
in oca ions@Me hodDe ini ion@ja asou cemm :null #
class@Me hodDe ini ion@ja asou cemm : ’c1 >
<’m2 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :" c_m2" #
in oca ions@Me hodDe ini ion@ja asou cemm :Sequence [ ’i1 ; ’i1 ] #
class@Me hodDe ini ion@ja asou cemm : ’c1 >
<’i1 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m1 >
<’c2 :ClassDecla a ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"SecondClass" #
me hods@ClassDecla a ion@ja asou cemm :Sequence [ ’m3 ; ’m4 ]>
<’m3 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"sc_m1" #
in oca ions@Me hodDe ini ion@ja asou cemm : ’i2 #
class@Me hodDe ini ion@ja asou cemm : ’c2 >
<’i2 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m1 >
<’m4 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"sc_m2" #
in oca ions@Me hodDe ini ion@ja asou cemm : ’i3 #
class@Me hodDe ini ion@ja asou cemm : ’c2 >
<’i3 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m3 >
}
No e ha quo ed iden i ie s a e used as objec iden i ie s; e e ences a e encoded as
objec a ibu es by means o objec iden i ie s; and OCL collec ions (Se ,O de edSe ,
Sequence, and Bag) a e suppo ed by means o mOdCL [RD08].
Me amodels a e encoded using a so o e e y me amodel elemen : so @Class
o classes, so @A ibu e o a ibu es, so @Re e ence o e e ences, e c. Thus,
a me amodel is ep esen ed by decla ing a cons an o he co esponding so o
each me amodel elemen . Thus, each class is ep esen ed by a cons an o a so
named a e he class. This so , which will be decla ed as subso o so @Class,
is de ined o suppo class inhe i ance h ough Maude’s o de -so ed ype s uc u e.
O he p ope ies o me amodel elemen s, such as whe he a class is abs ac o no ,
he opposi e o a e e ence ( o ep esen bidi ec ional associa ions), o a ibu es and
e e ence ypes, a e exp essed by means o Maude equa ions. Classes, a ibu es and
e e ences a e quali ied wi h hei con aine s’ names, so ha classes wi h he same
name belonging o di e en packages, as well as a ibu es and e e ences o di e en
classes, a e dis inguished. See [RVD09] o u he de ails.
Jou nal o Objec Technology, ol. 10, 2011
16 ·Ja ie T oya, An onio Vallecillo
cell2 :Table!Cell(con en <−’SecondCell’),
cell3 :Table!Cell(con en <−’Thi dCell’)
do{
cell1.con en <−cell1.con en +’_assignmen ’;
i ( ow.cells −>size() = 3) {
cell2.con en <−’Condi ion_sa is ied’;
}else {
cell2.con en <−’Condi ion_no _sa is ied’;
}
o (i in ow.cells){
i.con en <−i.con en +’_assign_ o ’;
i (i.con en =’Thi dCell_assign_ o ’){
i.con en <−i.con en +’_i _ o _sa is ied’;
}else {
i.con en <−i.con en +’_i _ o _no _sa is ied’;
}
i.con en <−i.con en +’_a e _i _ o ’;
}
hisModule.NewTable(’NewTable’);
}
}
The co esponding encoding in Maude is as ollows:
c l[Main] :
Sequence[...] =>
Sequence[...
(@Tablemm@ {do (
<T@ :Table@ ablemm | ows@Table@ ablemm :R@ >
<R@ :Row@ ablemm |cells@Row@ ablemm :Sequence [C1@ ;C2@ ;C3@ ]>
<C1@ :Cell@ ablemm |con en @Cell@ ablemm :"Fi s Cell" >
<C2@ :Cell@ ablemm |con en @Cell@ ablemm :"SecondCell" >
<C3@ :Cell@ ablemm |con en @Cell@ ablemm :"Thi dCell" >,
Assign(C1@,con en @Cell@ ablemm,
<< C1@ .con en @Cell@ ablemm ;TABLEMODEL@ >> +"_assignmen ") ˆ
I (<< Sequence[C1@ ;C2@ ;C3@]−>size() ; JAVASOURCEMODEL@ >> == 3,
Assign(C2@,con en @Cell@ ablemm,"Condi ion_sa is ied"),
Assign(C2@,con en @Cell@ ablemm,"Condi ion_no _sa is ied")) ˆ --- endI
Fo (<< R@ .cells@Row@ ablemm ;TABLEMODEL2@ >>,
AssignA Fo (con en @Cell@ ablemm,con en @Cell@ ablemm,TABLEMODEL2@,
"_assign_ o ") ˆ
I Fo ("==",con en @Cell@ ablemm,"Thi dCell_assign_ o ",TABLEMODEL3@,
AssignA Fo (con en @Cell@ ablemm,con en @Cell@ ablemm,TABLEMODEL3@,
"_i _ o _sa is ied"),
AssignA Fo (con en @Cell@ ablemm,con en @Cell@ ablemm,TABLEMODEL3@,
"_i _ o _no _sa is ied") ) ˆ --- endI Fo
AssignA Fo (con en @Cell@ ablemm,con en @Cell@ ablemm,TABLEMODEL4@,
"_a e _i _ o ") ) ˆ --- endFo
NewTable(VALUE@CNT@ + 6, "NewTable"))
OBJSETTT@ }
)
]i ...
The i s a gumen o unc ion do is he se o objec s c ea ed in he decla a i e
pa o he ule. Consequen ly, we en o ce he decla a i e pa o he ule o be
Jou nal o Objec Technology, ol. 10, 2011

A Rew i ing Logic Seman ics o ATL ·17
Figu e 8 – T ace class.
execu ed be o e he impe a i e pa . This is he way in which ATL wo ks. The second
a gumen is a sequence o ins uc ions. I con ains, in his case, ou ins uc ions. The
i s ins uc ion execu ed is an Assign. Then, an I block wi h wo assignmen s inside is
execu ed. A e his, a Fo ins uc ion, con aining h ee ins uc ions ( wo assignmen s
and a i block), is execu ed. Finally, he ins uc ion ha ep esen s he called ule,
NewTable, is execu ed.
4.3.6 Resol eTemp
The esol eTemp unc ion looks o he ace ha con ains he sou ce elemen passed
as i s a gumen , and e u ns he iden i ie o he elemen om he sequence o
elemen s c ea ed om he sou ce elemen . I s ep esen a ion in Maude is as ollows:
op esol eTemp :Oid Na @Model @Model −>Oid .
eq esol eTemp(O@ ,N@ ,@T aceMm@{<TR@ :T ace@T aceMm |s cEl@T aceMm :
Sequence[O@] # gEl@T aceMm :SEQ #SFS >OBJSET},SOURCEMODEL@ ) =
i (<< SEQ −>size ( ) <N@ ;SOURCEMODEL@ >>) hen null
else << SEQ −>a (N@) ; SOURCEMODEL@ >>
i.
I has ou a gumen s: he iden i ie o he sou ce model elemen om which he
sea ched a ge model elemen is p oduced; he posi ion o he a ge objec iden i ie
in he sequence gEl@T aceMm; and he ace and class models, espec i ely. I
e u ns he iden i ie o he elemen o be e ie ed. The majo di e ence wi h he
ATL unc ion is ha he e we ecei e as second a gumen he posi ion ha he sea ched
a ge model elemen has among he ones c ea ed by he co esponding ule. In ATL,
ins ead, he a gumen ecei ed is he name o he a iable ha was gi en o he
a ge model elemen when i was c ea ed. This de ia ion om ATL is me ely due o
echnical easons: we do no use a iable names in his unc ion because we do no
s o e a iable names in aces. A ace con ains a sequence wi h he iden i ie s o he
a ge elemen s ha we e c ea ed om he sou ce elemen s. As i is a sequence, i is
o de ed and, consequen ly, e e y elemen iden i ie has a posi ion wi hin he sequence.
The e o e, he di e ence o passing as a gumen he posi ion o he elemen iden i ie
in he sequence ins ead o he a iable name is no signi ican since i is easy o e ie e
he posi ion o he elemen among hose c ea ed by he ATL ule.
4.4 ATL e ining mode in Maude
As explained in sec ion 2.1, he ATL e ining execu ion mode ans o ms he elemen s
iden i ied by he sou ce pa e ns acco ding o he beha iou de ined in he ules.
Those model elemen s ha a e no explici ly a ec ed by he ules (ei he di ec ly o
indi ec ly) emain unchanged.
Jou nal o Objec Technology, ol. 10, 2011
18 ·Ja ie T oya, An onio Vallecillo
The seman ics o his ATL execu ion mode can be speci ied in Maude in a simila
way o he one used o speci y he no mal execu ion mode. Howe e , he aces will be
ea ed in a sligh ly di e en manne , because we do no need o speci y and main ain
aces be ween elemen s ha ha e no been modi ied by he ans o ma ion. In ac ,
aces in his execu ion mode can be conside ed as model di e ences be ween he
elemen s o bo h models: he old and new e sions o he model being ans o med.
Thus, we ha e de ined each ace as an ins ance o he class shown in Fig. 8, which
ollows he app oach used in [RV08].
T aces o ype modi ied ep esen he ans o ma ion o an objec om he sou ce
model in o ano he objec in he a ge model whe e a leas one o i s a ibu es (o
e e ences) ha e been modi ied. T aces whose ype is added, in u n, ep esen he
addi ion o a new objec (o mo e han one) in he a ge model.
In he 2010 implemen a ion o he e ining mode, ATL allows o emo e objec s.
To ep esen his new ea u e we ha e aces o ype dele ed, whose sou ce elemen s
(s cEl) a e he dele ed objec s, and he se o a ge elemen s ( gEl) is emp y. A
Maude ule ha ep esen s an ATL ule whe e objec s a e dele ed simply con ains
hese objec s in i s le hand side, bu no in i s igh hand side, and i c ea es a ace
o ype dele ed as men ioned abo e.
In he encoding o a ans o ma ion in e ining mode in Maude, he Ini ule is also
di e en , since now he sou ce model is copied in o he a ge one. Thus, in case o
he Public2P i a e example in oduced in sec ion 2.1, his ule is as ollows:
l [Ini ] :
Sequence[(@UMLSimpMm@ {OBJSET@ })]
=>
Sequence[(@UMLSimpMm@ {OBJSET@ }) ;
(@T aceMm@ {<’CNT :Coun e @Coun e Mm | alue@Coun e @Coun e Mm : 1 >}) ;
(@UMLSimpMm@ {OBJSET@ })] .
A e he applica ion o his ule, bo h he sou ce and a ge models con ain he
same elemen s. Then, he a ge model is modi ied as he ATL ma ched ules a e
execu ed, “na iga ing” he sou ce model.
Models na igabili y and in-place ans o ma ions
The ATL documen a ion [G o06] s a es ha , bo h in no mal and in e ining execu ion
modes, sou ce models a e ead-only and a ge models a e w i e-only. This means
ha only sou ce models can be na iga ed and, he e o e, he s a e o he a ge model
does no a ec he beha io o he ans o ma ion.
This is an impo an de ail ha signi ican ly a ec s he way in which ATL wo ks
in e ining mode. In ac , i is a common mis ake o con use he beha io o he
ATL e ining mode wi h he ypical beha io o he in-place ans o ma ions used by
mos ew i ing sys ems, including g aph g amma s o e en Maude ules. In hese
ew i ing sys ems, a se o ules modi ies he s a e o a con igu a ion o objec s (i.e.,
a model) one by one. Thus, a e he applica ion o each ule he s a e o he sys em
is changed, and subsequen ules will be applied on he sys em on his new s a e. In
his way, he a ge model a e he applica ion o one ule becomes he sou ce model
in he nex s ep. In o he wo ds, he ans o ma ion na iga es he a ge model,
which is con inuously upda ed by e e y execu ed ule. Howe e , his is no he way
in which he ATL e ining mode wo ks. In ATL he ules always ead (i.e., na iga e)
he s a e o he sou ce model, which emains unchanged du ing all he ans o ma ion
execu ion. This is he app oach we ha e ollowed in ou ep esen a ion in Maude, oo.
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·19
Figu e 9 – In-place beha io : na igabili y on he a ge model.
In o de o illus a e his di e ence, le us go back o he Public2P i a e ans o ma-
ion and imagine ha we add ano he ma ched ule ha changes all p i a e P ope ies,
capi alizing he i s le e o hei names. Le us call his ule P i a e2Capi al.
I ATL wo ked in a pu e in-place manne (i.e., na iga ing he a ge model), he
ans o ma ion would change he names o all p ope ies: all o hem will end up being
p i a e and wi h he i s le e o hei names in capi als (see he example shown in
Fig. 9). Howe e , he ATL e ining mode na iga es he sou ce model. This means
ha , a he end o he execu ion o he Public2P i a e ans o ma ion, only hose
p ope ies ha we e o iginally p i a e in he sou ce model will ha e hei names
capi alized, while he o iginal public p ope ies in he model will be ans o med in o
p i a e p ope ies bu hei names will no be changed (see Fig. 10).
5 Simula ion and Fo mal Analysis
Once he ATL model ans o ma ion speci ica ions a e encoded in Maude, wha we ge
is a ew i ing logic speci ica ion o i . Maude o e s ool suppo o in e es ing possi-
bili ies such as model simula ion, eachabili y analysis and model checking [CDE+07].
Jou nal o Objec Technology, ol. 10, 2011
20 ·Ja ie T oya, An onio Vallecillo
Figu e 10 – ATL e ining mode: na igabili y always on he sou ce model.
5.1 Simula ing he ans o ma ions
Because he ew i ing logic speci ica ions p oduced a e execu able, his speci ica ion
can be used as a p o o ype o he ans o ma ion, which allows us o simula e i .
Maude o e s di e en possibili ies o pe o ming he simula ion, including s ep-by-
s ep execu ion, se e al execu ion s a egies, e c. In pa icula , Maude p o ides wo
di e en ew i e commands, namely ew i e and ew i e, which implemen wo di e -
en execu ion s a egies, a op-down ule- ai s a egy, and a dep h- i s posi ion- ai
s a egy, espec i ely [CDE+07]. The esul o he p ocess is he inal con igu a ion
o objec s eached a e he ew i ing s eps, which is no hing bu a model.
Fo example, he Ja aSou ce2Table ATL model ans o ma ion desc ibed in sec-
ion 2, when execu ed in de aul mode o e he Ja aSou ce sou ce model shown in
Fig. 3, esul s in a sequence o h ee models: he sou ce, he ace and he a ge
model. The encoding in Maude o his las one, which con o ms o he Table me a-
model and is displayed in Fig. 4, is shown below.
@Ja aSou ceMm@ {
<’s:Ja aSou ce@ja asou cemm |
classes@Ja aSou ce@ja asou cemm :Sequence[ ’c1 ; ’c2 ]>
<’c1 :ClassDecla a ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"Fi s Class" #
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·21
me hods@ClassDecla a ion@ja asou cemm :Sequence[ ’m1 ; ’m2 ]>
<’m1 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :" c_m1" #
in oca ions@Me hodDe ini ion@ja asou cemm :null #
class@Me hodDe ini ion@ja asou cemm : ’c1 >
<’m2 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :" c_m2" #
in oca ions@Me hodDe ini ion@ja asou cemm :Sequence [ ’i1 ; ’i1 ] #
class@Me hodDe ini ion@ja asou cemm : ’c1 >
<’i1 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m1 >
<’c2 :ClassDecla a ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"SecondClass" #
me hods@ClassDecla a ion@ja asou cemm :Sequence [ ’m3 ; ’m4 ]>
<’m3 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"sc_m1" #
in oca ions@Me hodDe ini ion@ja asou cemm : ’i2 #
class@Me hodDe ini ion@ja asou cemm : ’c2 >
<’i2 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m1 >
<’m4 :Me hodDe ini ion@ja asou cemm |
name@NamedElemen @ja asou cemm :"sc_m2" #
in oca ions@Me hodDe ini ion@ja asou cemm : ’i3 #
class@Me hodDe ini ion@ja asou cemm : ’c2 >
<’i3 :Me hodIn oca ion@ja asou cemm |
me hod@Me hodIn oca ion@ja asou cemm : ’m3 >}
Al hough he Maude speci ica ions can be used o unning he ATL ans o ma-
ions, and no only o simula ing i , he pe o mance o he Maude speci ica ions is
no compa able wi h ATL (see Sec ion 5.4). Howe e , ou p oposal does no y o
compe e wi h ATL in his espec . I is no he goal o his wo k o use Maude o
implemen ing model ans o ma ions, bu o p o iding seman ics o ATL. The ac
ha Maude speci ica ions a e execu able gi es us an implemen a ion o he ans o -
ma ion, bu such an implemen a ion is no in ended o be used as an al e na i e o
ATL in p ac ice—jus o e i ica ion pu poses.
5.2 Reachabili y analysis
Execu ing he sys em using he ew i e and ew i e commands means explo ing jus
one possible beha io o he sys em. Howe e , a ew i e sys em does no need o
be Chu ch-Rosse and e mina ing,2and he e migh be many di e en execu ion
pa hs. Al hough hese commands a e enough in many p ac ical si ua ions whe e an
execu ion pa h is su icien o es ing execu abili y, he use migh be in e es ed in
explo ing all possible execu ion pa hs om he s a ing model, a subse o hese, o
a speci ic one.
Maude sea ch command allows us o explo e ( ollowing a b ead h i s s a egy up
o a speci ied bound) he eachable s a e space in di e en ways, looking o ce ain
s a es o special in e es . O he possibili ies would include sea ching o any s a e
2Fo membe ship equa ional logic speci ica ions, being Chu ch-Rosse and e mina ing means no
only con luence (a unique no mal o m will be eached) bu also a so dec easingness p ope y,
namely ha he no mal o m will ha e he leas possible so among hose o all o he equi alen
e ms.
Jou nal o Objec Technology, ol. 10, 2011

22 ·Ja ie T oya, An onio Vallecillo
(gi en by a model) in he execu ion ee, le i be inal o no . Fo example, we
could be in e es ed in knowing he pa ial o de in which wo ATL ma ched ules a e
execu ed, checking ha one always occu s be o e he o he . This can be p o ed by
sea ching o s a es ha con ain he second one in he ace model, bu no he i s .
5.3 Checking o he p ope ies
A e he simula ion is comple ed, i is also possible o analyze he ace model looking
o ins ance o ules ha ha e no been execu ed, o o ob aining he aces (and
sou ce model elemen s) ela ed o a pa icula a ge model elemen (o ice e sa).
Al hough his could also be done in any ans o ma ion language ha makes he
ace model explici , he ad an ages o using ou encoding in Maude is ha hese
ope a ions become easy o speci y because o Maude’s acili ies o manipula ing se s
using o de -so ed uni ica ion modulo associa i i y and commu a i i y:
op ge Sou ceElemen s :@Model Oid −>Sequence .
eq ge Sou ceElemen s(@T aceMm@{<TR@ :T ace@T aceMm |s cEl@T aceMm :
SEQ # gEl@T aceMm :Sequence[O@ ;LO] # SFS >OBJSET},O@) = SEQ .
eq ge Sou ceElemen s(@T aceMm@{<TR@ :T ace@T aceMm |s cEl@T aceMm :
SEQ # gEl@T aceMm :Sequence[T@ ;LO] # SFS >OBJSET},O@)
=ge Sou ceElemen s(@T aceMm@{<TR@ :T ace@T aceMm |s cEl@T aceMm :
SEQ # gEl@T aceMm :Sequence[LO] # SFS >OBJSET},O@) .
eq ge Sou ceElemen s(@T aceMm@{OBJSET},O@) = Sequence[m −o d] [owise] .
We can also use a simila ope a ion o a e se he ace model and check ha
e e y sou ce elemen has been ans o med by a mos one ATL ma ch ule. In ac ,
in ATL only one ma ched ule can be applied on a gi en model elemen ( his ensu es
some kind o con luence o he ATL ules, oo).
In gene al he e a e wo ways o dealing wi h such cons ain s, depending on
whe he we wan he Maude ules o en o ce hem du ing hei execu ion o no . In
he i s case hese cons ain s will be added o he Maude ules. In he second case
he mapping o Maude will no conside hem, so hese si ua ions will occu i hey
happen in he ATL code. Bu we will be able o check hem once he ans o ma ion
is done by explo ing he ace model, as men ioned abo e.
Fo example, o check ha no mo e han one ATL ule is applied o e a single
sou ce elemen we ha e de ined he singleApplicabili y ope a ion:
op singleApplicabili y :OCL−Exp S ing @Model In −>@Objec .
eq singleApplicabili y(SR@,NAME,@T aceMm@ {<TR@ :T ace@T aceMm |
s cEl@T aceMm :Sequence[SR@ ;LO] # lName@T aceMm :NAME’ # SFS >OBJSET},
VALUE@CNT@) =
i NAME =/= NAME’ hen
<newId(VALUE@CNT@) : T aceSA@T aceMm | l1Name@T aceMm :NAME #
l2Name@T aceMm :NAME’ # s cEl@T aceMm :SR@ #e Msg@T aceMm :"Rules " +
NAME +" and " +NAME’ + " a e applied o e he same sou ce elemen : " +
SR@ >
else singleApplicabili y(SR@,NAME,@T aceMm@ {<TR@ :T ace@T aceMm |
s cEl@T aceMm :Sequence[LO] # lName@T aceMm :NAME’ # SFS >OBJSET},
VALUE@CNT@)
i.
eq singleApplicabili y(SR@,NAME,TRACEMODEL@,VALUE@CNT@) = none [owise] .
This ope a ion ecei es as a gumen s a sou ce model elemen , a s ing wi h he
name o he ule om which he unc ion is called, he ace model and he coun e
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·23
o c ea e new iden i ie s. The unc ion looks o a ace c ea ed by a di e en ule
(we check ha he names o he ules a e di e en : NAME =/= NAME’) whe e he
elemen ecei ed as a gumen is p esen in he s cEl@T aceMm pa .
The p oblem, as usual, is wha o do when a p oblem is encoun e ed du ing he
execu ion o he ule. In his case ou encoding gene a es a special kind o ace
(T aceSA@T aceMm), which cap u es e e y e o ound. Such aces s o e he p ob-
lema ic ule names ( hose whose le hand side pa s con ain he same sou ce model
elemen ), he sou ce model elemen and an e o message.
As an example o how his unc ion is called, we add a call o i in he Me hod-
De ini ion ma ched ule ha we p esen ed abo e. We can see he call in he nex
lis ing:
c l[Me hodDe ini ion] :
Sequence[
(@Ja aSou cemm@ {<M@ :Me hodDe ini ion@ja asou cemm |SFS >OBJSET@ }) ;
(@T aceMm@ {<CNT@ :Coun e @Coun e Mm | alue@Coun e @Coun e Mm :VALUE@CNT@>
OBJSETT@ }) ;
(@Tablemm@ {OBJSETTT@ }) ]
=>Sequence[
(@Ja aSou cemm@ {<M@ :Me hodDe ini ion@ja asou cemm |SFS >OBJSET@ }) ;
(@T aceMm@ {
<CNT@ :Coun e @Coun e Mm | alue@Coun e @Coun e Mm :VALUE@CNT@ + 4 >
...
singleApplicabili y(M@,"Me hodDe ini ion",@T aceMm@{OBJSETT@},VALUE@CNT@)
OBJSETT@}) ;
(@Tablemm@ {... }) ]
i JAVASOURCEMODEL@ := ...
/ TR@ := newId(VALUE@CNT@ + 1) / R@ := newId(VALUE@CNT@ + 2)
/ TC@ := newId(VALUE@CNT@ + 3) /
/ no al eadyExecu ed(Sequence[M@],"Me hodDe ini ion",@T aceMm@ {OBJSETT@ }).
5.4 Ques ions o e iciency
Ano he imp o emen o e he p oposal p esen ed in [TV10a] is he use o a mo e
compac encoding o he Maude ep esen a ion o he ATL ules. Maude is a e y
exp essi e language, which allows many di e en ways o ep esen he same concep s
o he same beha io s. Each encoding, al hough unc ionally and seman ically equi -
alen , may be di e en ega ding o he non- unc ional aspec s such as pe o mance,
eadabili y o unde s andabili y, among o he s.
In he p e ious sec ions we ha e shown he encoding ha was also used in [TV10a].
This encoding is a he na u al ( o he Maude use s) and con enien o ep esen ing
he beha io o ATL cons uc s and ules. Howe e , when i comes o simula ing and
analyzing he speci ica ions, i may be signi ican ly imp o ed in se e al ways.
The aim o he modi ica ions is o emo e as many gua ds as possible om he
Maude ules, so ha he ew i e p ocess does no need o e alua e condi ions o
igge ing hem. Thus, we ha e a oided he use o auxilia y a iables ha we e
decla ed as gua ds wi h he “:=” ope a o by eplacing hem wi h hei co esponding
exp essions in he places whe e hese auxilia y a iables we e used. We ha e also go
id o he Al eadyExecu ed unc ion, which had o na iga e he ace model in each
ule in oca ion, by in oducing an auxilia y model in he Maude ules ha con ains
he elemen s om he inpu model ha ha e no ye been ans o med by ATL ules.
Jou nal o Objec Technology, ol. 10, 2011
24 ·Ja ie T oya, An onio Vallecillo
O iginal Op imized
encoding encoding ATL
125 Classes, 500 A ibu es 15” 4” 0.3”
250 Classes, 1000 A ibu es 1’37” 15” 0.5”
375 Classes, 1500 A ibu es 5’53” 40” 0.8”
500 Classes, 2000 A ibu es 16’09” 1’37” 1.1”
750 Classes, 3000 A ibu es 58’28” 4’02” 2”
1250 Classes, 5000 A ibu es 3h16’49” 16’37” 3”
2000 Classes, 8000 A ibu es 17h57’15” 1h04’19” 5”
Table 1 – Compa a i e pe o mance igu es.
This new model ini ially coincides wi h he inpu model o he ans o ma ion and,
when a ule is execu ed on a se o elemen s, hese elemen s a e emo ed om he
model. We ha e emo ed he e alua ion o some OCL exp essions in he condi ions o
he Maude ules by checking hem in he inpu model. We ha e also ied o a oid he
use o OCL exp essions in he igh hand side o Maude ules when ini ializing objec s
a ibu es in he a ge model by speci ying a iables o he alues o he objec s’
a ibu es in he inpu model. Please e e o [TBV10] o a comple e desc ip ion o
he pe o med modi ica ions.
This al e na i e encoding p o ides signi ican imp o emen s in e iciency and pe -
o mance, as shown in Table 1 o he ATL Class2Rela ional ans o ma ion [TV10a].
S ill, i is no compa able o he pe o mance o he equi alen ATL ans o ma ion
(shown in he las column).
The p oblem is ha he new Maude encoding is much mo e e bose and less easy o
ead and unde s and. Howe e , his new encoding can be au oma ically ob ained om
he p e ious one, hence allowing an au oma ic ans o ma ion om one o he o he .
This is why we ha e de ailed he e he o iginal encoding, because i is unc ionally
equi alen and much easie o ead and unde s and.
6 Rela ed Wo k
The de ini ion o a o mal seman ics o ATL has ecei ed a en ion by di e en
g oups, using di e en app oaches. Fo example, in [dRJK+06] he au ho s p opose
an ex ension o AMMA, he ATLAS Model Managemen A chi ec u e, o speci y he
dynamic seman ics o a wide ange o Domain Speci ic Languages by means o Ab-
s ac S a e Machines (ASMs), and p esen a case s udy whe e he seman ics o pa
o ATL (namely, ma ched ules) a e o malized. Al hough ASMs a e e y exp essi e,
he decla a i e na u e o ATL does no help p o iding o mal seman ics o he com-
ple e ATL language in his o malism, hinde ing he comple e o maliza ion o he
language—some hing ha we we e pu suing wi h ou app oach.
O he wo ks [BS06, ABK07] ha e p oposed he use o Alloy o o malize and
analyze g aph ans o ma ion sys ems, and in pa icula ATL. These analysis include
checking he eachabili y o gi en con igu a ions o he hos g aph h ough a ini e
sequence o s eps (in oca ions o ules), and e i ying whe he gi en sequences o ules
can be applied on an ini ial g aph. These analysis a e also possible wi h ou app oach,
and we also ob ain signi ican gains in exp essi eness and comple eness. The p oblem
Jou nal o Objec Technology, ol. 10, 2011
A Rew i ing Logic Seman ics o ATL ·25
is ha Alloy exp essi eness and analysis capabili ies a e qui e limi ed [ABK07]: i
has a simple ype sys em wi h only in ege s; models in Alloy a e s a ic, and hus he
app oach p esen ed in [ABK07] can only be used o eason abou s a ic p ope ies o
he ans o ma ions ( o example i is no possible o eason whe he applying a ule
1be o e a ule 2in a model will ha e he same e ec as applying 2be o e 1); only
ATL decla a i e ules a e conside ed, e c. In ou app oach we can deal wi h all he
ATL language cons uc s wi hou ha ing o abs ac away essen ial pa s such as he
impe a i e sec ion, basic ypes, e c. Mo e kinds o analysis a e also possible wi h ou
app oach.
O he wo ks p o ide o mal seman ics o model ans o ma ion languages using
ypes. Fo in ance, Poe nomo [Poe08] uses Cons uc i e Type Theo y (CTT) o
o malizing model ans o ma ion and p o ing hei co ec ness wi h espec o a gi en
p e- and pos -condi ion speci ica ion. This app oach elies on a simple encoding o
Me aClasses as mixed induc i e/co-induc i e s uc u ed ypes which he cu en p oo
assis an does no handle well due o s uc u al gua d cons ain s o co-induc i e
de ini ions [PM10]. Al e na i e app oaches encode models as g aph co e ing ees
and addi ional links [GS10, GSMP11] o as a classical ma hema ical g aphs elying
on nodes and ela ions be ween nodes [TCCG07]. These app oaches can be conside ed
as complemen a y o ou s, each one ocusing on di e en aspec s.
The e a e also he ea ly wo ks in he g aph g amma communi y wi h a logic-based
de ini ion and o maliza ion o g aph ans o ma ion sys ems. Fo example, Cou -
celle [Cou97] p oposes a combina ion o g aph g amma s wi h second o de monadic
logic o s udy g aph p ope ies and hei ans o ma ions. Sch¨u [SWZ99] has also
s udied he o mal speci ica ion o he seman ics o he g aph ans o ma ion language
PROGRES by ansla ing i in o some so o non-mono onic logics.
A di e en line o wo k p oposed in [BHM09] de ines a QVT-like model ans o -
ma ion language eusing he main concep s o g aph ans o ma ion sys ems. They
o malize hei model ans o ma ions as heo ies in ew i ing logic, and in his way
Maude’s eachabili y analysis and model checking ea u es can be used o e i y hem.
Only he educed pa o QVT ela ions ha can be exp essed wi h his language is
co e ed. Ou wo k is di e en : we o malize a comple e exis ing ans o ma ion lan-
guage by p o iding i s ep esen a ion in Maude, wi hou p oposing ye ano he MT
language.
In his pape we ha e deal wi h all new ea u es o ATL e sion 3.0, and in pa -
icula we ha e o malized he ATL e ining mode. Many wo ks ha e been dedica ed
o he seman ics o he de aul execu ion mode, bu no one seems o be ocused on
he e ining mode despi e he impo ance his execu ion mode is gaining. Fo ex-
ample, Tisi e al. p opose in [TCJ10] he use o his execu ion mode o implemen
Highe -O de T ans o ma ions (HOTs). They a e model ans o ma ions ha ana-
lyze, p oduce o manipula e o he model ans o ma ions [TJF+09]. W i ing HOTs
is gene ally conside ed a ime-consuming and e o -p one ask, and o en esul s in
e bose code. Re ining mode is used in [TCJ10] o acili a e he de ini ion o HOTs
in ATL, and hey ecommend he de elope s o conside in-place e ining mode o
e e y ans o ma ion modi ica ion and (de)composi ion.
Finally, Maude has been p oposed as a o mal no a ion and en i onmen o spec-
i ying and e ec i ely analyzing models and me amodels [RVD09, BM08]. Simula ion,
eachabili y and model-checking analysis a e possible using he ools and echniques
p o ided by Maude [RVD09]. We build on hese wo ks, making use o one o hese
o maliza ions o ep esen he models and me amodels ha ATL handles.
Jou nal o Objec Technology, ol. 10, 2011