=Paper=
{{Paper
|id=None
|storemode=property
|title=Automated Model Transformations Based on STRIPS Planning
|pdfUrl=https://ceur-ws.org/Vol-601/EOMAS10_paper1.pdf
|volume=Vol-601
}}
==Automated Model Transformations Based on STRIPS Planning==
https://ceur-ws.org/Vol-601/EOMAS10_paper1.pdf
Automated Model Transformations Based on
STRIPS Planning
1 2 3
Old°ich Nouza , Vojt¥ch Merunka , and Miroslav Virius
1
Czech Technical University in Prague, Faculty of Nuclear Sciences and Physical
Engineering, Department of Software Engineering in Economy,
nouza@fj .cvut.cz
2
Czech University of Life Sciences Prague, Faculty of Economics and Management,
Department of Information Engineering,
merunka@pef.czu.cz
3
Czech Technical University in Prague, Faculty of Nuclear Sciences and Physical
Engineering, Department of Software Engineering in Economy,
virius@fj .cvut.cz
Abstract. This paper deals with application of STRIPS planning in
automated model transformations. Object oriented model is viewed as a
state space containing possible models as states and elementary transfor-
mations as state transitions. A source model is represented by an initial
state, a target model by a goal state. Automation of model transforma-
tion consists in nding a plan to reach a goal state in this state space.
Key words: automated model transformations, modeling, object ori-
ented approach, refactoring, SBAT, STRIPS planning
1 Introduction
Transformations play a key role in software engineering. Although there exist
satis able solutions of automated transformations of models to text, the same
cannot be said about transformations of models to models. This area is still in
phase of research and exploring of possibilities [1].
According to the approaches of present implemented in several CASE tools,
every model transformation requires application of the corresponding transfor-
mation rule with suitable parameters [3, 4, 6, 13] Unfortunately, as mentioned
in [4], this approach has one big disadvantage, which is a low reusability. For
every transformation that has no rule de ned, it is necessary to either apply a
composition of other rules, or de ne a new transformation rule. In this paper, we
introduce transformation engine named SBAT (STRIPS Based Transformation
Engine) that does not require such steps.
2 Model Transformations
There are several ways how to de ne model transformation. In this paper, we
introduce the de nition presented in [5] and cited by [8]:
J. Barjis, M.M. Narasipuram, G. Rabadi, J. Ralyté, and P. Plebani (Eds.):
CAiSE 2010 Workshop EOMAS’10, Hammamet, Tunisia, pp. 1-13, 2010.
2 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
A transformation is the automatic generation of a target model from a
source model, according to a transformation de nition. A transformation
de nition is a set of transformation rules that together describe how a
model in the source language can be transformed into a model in the
target language. A transformation rule is a description of how one or
more constructs in the source language can be transformed into one or
more constructs in the target language.
2.1 Classi cation of Transformations
Publication [8] describes two criteria of classi cation of model transformations.
The rst one is a dierence of abstraction level of source and target models:
Horizontal transformation A transformation where source and target models
have the same level of abstraction. A typical example is refactoring.
Vertical transformation A transformation where source and target models
have a dierent level of abstraction. A typical example is re nement.
The second classi cation criteria is a dierence of modeling languages in which
the source and targets models are expressed:
Endogenous transformation A transformation where source and target models
are expressed in the same language. Typical examples are refactoring and
normalization.
Exogenous transformation A transformation where source and target models
are expressed in dierent languages. Typical examples are code generation
and reverse engineering.
In this paper, we focus more closely on refactoring.
3 Refactoring
There exist several ways how to de ne refactoring. The de nition presented in
[7] says that refactoring is an improvement of software system without changing
its behavior. In other words, for the same input, the refactored software must
return the same output as the original software. Detail information on refactoring
is available in [2].
3.1 Complex Refactorings and Primitive Refactorings
The idea of complex refactoring as composition of nite primitive (atomic) refac-
torings was rst published in [10], where formal de nition of C++ code refactor-
ing was discussed, and later in [12], where it was demonstrated on refactoring of
UML models. We have used the same idea to construct the SBAT transformation
engine.
Automated Model Transformations Based on STRIPS Planning 3
4 STRIPS Planning
Technical report [9] de nes STRIPS as following:
STRIPS (STanford Research Institute Problem Solver) belongs to the
class of problem solvers that search a space of world models to nd one
in which a given goal is achieved. For any world model, we assume there
exists a set of applicable operators each of which transforms the world
model to some other world model. The task of the problem solver is to
nd some composition of operators that transforms a given initial world
model into one that satis es some particular goal condition.
The STRIPS language is based on the calculus of rst-order predicate logic.
Formally, the STRIPS problem can be expressed by the following de nitions:
De nition 1. STRIPS problem is an ordered triple (I, O, G), where I is an
initial state, O is a set of operators, and G is a goal state condition.
De nition 2. Operator o (x̄) is de ned as an ordered triple(P, A, D), whereP =
(x̄) is an application condition, A = [A1 (x̄) , . . . , Al (x̄)] is a set of formulas
which become true after operator application, D = [D1 (x̄) , . . . Dm (x̄)] is a set
of formulas which become false after operator application, x̄ = (x1 , . . . xn ) are
+ 0
free variables contained in formulas P, A1 , . . . , Al , D1 , . . . Dm , n ∈ N , l, m ∈ N .
Elements of A are called add-eects, elements of D delete-eects.
De nition 3. Let o (x1 , . . . , xn ) = (P, A, D) ∈ O be operator. A transition func-
0
tion o : (x1 × x2 × . . . × xn × S) → S , where S is a state set, is de ned in the
following way:
def (s ∪ A) − D ∅
o' (x1 , . . . , xn , s) = (1)
sP
A goal is to nd such list of operators applications, which cause transition for
initial state to the state satisfying the goal state condition. More formally:
De nition 4. State sm is a solution of problem
(I, O, G), if there exists a list of
operators applications o1 h1 , . . . , om hm , where hi are vectors of constants,
m ∈ N, and:
1. s0 = I
0
2. (∀i ∈ m̂) si = oi−1 hi−1 , si−1
3. sm G
If I G, then the solution, which is I in this case, is called trivial solution.
4 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
5 SBAT Transformation Engine
5.1 Requirements
Resulting from the facts on present state model transformation discussed in
the introduction of this paper, we have decided to design a new transformation
engine ful lling the following requirements:
1. The engine will support model transformations such as refactoring.
2. The input of transformation process will be the source model and conditions
of a target model.
3. The output of transformation process will be a target model, or information
that the source model cannot be transformed to any model ful lling the
input conditions.
4. The source model and the target model will be consistent in light of behavior
of modeled system.
5. The transformation process will be fully automatized, without need to spec-
ify transformation rules on input.
6. The engine will be universal and su ciently reusable for wide scale of object
models.
5.2 Formal De nition of Object Model
In this paper, formal de nition of object model is based on simpli ed metamodel
of UML 2.0 class diagrams, in detail described in [11]. Because of intended gen-
erality, we do not focus on implementation details, such as method parameters
and bodies, access mode of class members, etc.
5.2.1 Model as State Space For our purposes we use the primitive refactor-
ing composition mentioned earlier. For this reason, we de ne model as a state
space, where state set represents model in all possible states and state transitions
represent primitive refactorings.
De nition 5. Let C be a class universe, A attribute universe, and F method
universe. LetObject, Client ∈ C be classes, where ∀ (x ∈ C − [Object]) (Object ≺ c),
which means that Object is parent of all other classes and Client represent a
client class, whose object sends messages to objects of classes in model. Let be
empty value. Model state s is an ordered 5-tuple (Cs , ins , supers , types , sends ),
where
Cs ⊂ C − [Object, Client] is a nite set of classes of model in state s,
ins ⊆ ((A ∪ F ) × Cs ) is a binary relation named is in class de ned as
def
ins = {(x, y) |x ∈ (Attr (y) ∪ M eth (y)) ∧ y ∈ Cs } , (2)
where Attr (y) and M eth (y) are sets of attributes and methods respectively of
class y ,
Automated Model Transformations Based on STRIPS Planning 5
supers ⊆ ((Cs ∪ [Object]) × Cs ) is a binary relation is superclass de ned as
def
supers = {(x, y) |x = super (y) ∧ x, y ∈ Cs } , (3)
where super (y) means a superclass of y ,
types ⊆ (A × Cs ) ∪ (F × (Cs )) is a binary relation named is of type de ned
as
def
types = {(x, y) |x = type (y) ∧ y ∈ Cs } , (4)
where type (y) means a type of y ,
sends ⊆ (F × (Cs ∪ [Client]) × (A ∪ F ) × Cs ) is a 4-ary relation named
sends message de ned as
def
sends = {(x, y, u, v) |(x, y) ∈ ins
∧ (∃w) ((u, w) ∈ ins ∧ (u ≺ w ∨ u = w)) (5)
∧ hx, Λi ∈ M eth (y)} ,
where lambda-expression Λ contains message sending o C u, where o is an
instance of class w .
The following conditions must be ful lled:
in the class hierarchy, each attribute appears at most once, so
(∀x ∈ A) (∀y, z ∈ C) (ins (x, y) ∧ ins (x, z) → ¬ (y ≺ z) ∧ ¬ (z ≺ y)) , (6)
each attribute is of some type, so
(∀x ∈ A) (∃y ∈ Cs ) (types (x, y)) , (7)
each attribute is of at most one type and each method has at most one return
value type, so
(∀x ∈ (A ∪ F )) (∀y, z ∈ Cs ) (types (x, y) ∧ types (x, z) → y = z) . (8)
De nition 6. Model
is a state space (M,
Φ), where M is a nite set of model
n
ϕi : M × E ki → M , (∀i ∈ n̂) (ki ∈ N) is a set of transfor-
S
states and Φ = i=1
mation rules.
5.3 Model Transformation Problem
Each model transformation requires answers to the following questions [8]:
1. What needs to be transformed?
2. What will be the result of the transformation?
To nd answers, we have to formulate the transformation problem and set the
principle of its solution. This can be done by several ways, we have decided to
apply the STRIPS planning.
6 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
5.4 STRIPS Planning application
Let's assume any nite subset B of object universal, containing elements of
all possible model states. To formulate STRIPS problem (I, O, G) for model
transformation, we must describe the model states and transformation rules
using rst-order predicate logic calculus. For this purpose, we de ne predicates
shown in table 1.
Table 1. Predicates for STRIPS problem formulation in SBAT engine
Predicate Declaration De nition
class c is in model inM odel (c) c ∈ Cs
class c is not in outOf M odel (c) c ∈ (B − Cs )
model
attribute a is in class attrInClass (a, c) (a, c) ∈ ins
c
attribute a is not in attrOutOf Class (a, c) ¬ ((a, c) ∈ ins ) ∧ a ∈ (B ∩ A)
class c
method µ is in class methInClass (µ, c) (µ, c) ∈ ins
c
method µ is not in methOutOf Class (µ, c) ¬ ((µ, c) ∈ ins ) ∧ µ ∈ (B ∩ F )
class c
attribute a is of type hasT ype (a, t) (a, t) ∈ types
t
method µ has return hasRetT ype (µ, t) (µ, t) ∈ types
value type t
class c is superclass superClass (c, d) (c, d) ∈ supers
of d
class c is a parent of parent (c, d) c≺d
d
method µof class c sending (µ, c, η, d) (µ, c, η, d) ∈ sends
sends messageη to
objects of class d
5.4.1 Initial State Formulation Let mI = (CI , inI , superI , typeI , sendI ) be
a model in initial state. We construct initial state I of STRIPS problem by the
following steps:
1. Put I := ∅.
2. Add formulas about existence of classes in model:
a) (∀c ∈ CI ) put (I := I ∪ [inM odel (c)]) and
b) (∀c ∈ (B − CI )) put (I := I ∪ [outOf M odel (c)]).
3. Add formulas about class attributes:
a) (∀ (a, c) ∈ (inI ∩ (B ∩ A, CI ))) put
(I := I ∪ attrInClass (a, c)) and
Automated Model Transformations Based on STRIPS Planning 7
b) (∀ (a, c) ∈ ((B ∩ A, B ∩ C) − inI )) put
(I := I ∪ attrOutOf Class (a, c)).
4. Add formulas about class methods:
a) (∀ (µ, c) ∈ (inI ∩ (B ∩ F, CI ))) put
(I := I ∪ methInClass (µ, c)) and
b) (∀ (µ, c) ∈ ((B ∩ F, B ∩ C) − inI )) put
(I := I ∪ methOutOf Class (µ, c)).
5. Add formulas about inheritance:
(∀ (c, d) ∈ superI ) put (I := I ∪ superClass (c, d)).
6. Add formulas about attribute types and return value types of methods:
a) (∀ (a, c) ∈ (typeI ∩ (B ∩ A, CI ))) put
(I := I ∪ hasT ype (a, c)) and
b) (∀ (µ, c) ∈ (typeI ∩ (B ∩ F, CI ))) put (I := I ∪ hasT ype (µ, c)).
7. Add formulas about message sending:
(∀ (a, c, b, d) ∈ sendI ) put (I := I ∪ sending (a, b, c, d)).
5.4.2 Formulation of Goal State Condition A goal state condition G is
de ned by the formula that is true in any goal state.
5.4.3 Formulation of Operator Set The set of operators O is de ned iden-
tically for each particular problem, because it represents a set of primitive refac-
torings. The complete de nition of the operator set is described in table 3 in
appendix.
5.5 Example
5.5.1 Problem Let's suppose a simpli ed class model of le system (see g. 1).
*
+owner
Folder File
*
+name +name
+owner
Fig. 1. File system class model
The goal is to transform this model into state which satis es the composite
design pattern.
8 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
5.5.2 Solution The initial model state ms = (Cs , ins , supers , types , sends ),
where:
Cs = [F older, F ile, String]
ins = [(name, F older) , (owner, F older) , (name, F ile) , (owner, F ile)]
supers = [(Object, F older) , (Object, F ile) , (Object, String)]
types = [(name, String) , (owner, F older)]
sends = {(Client, main, x, y) |(x, y) ∈ ins }
The corresponding initial state of STRIPS problem is the following:
I = [inM odel (F older) , inM odel (F ile) , inM odel (String) ,
outOf M odel (Element) ,
attrInClass (name, F older) , attrInClass (owner, F older) ,
attrInClass (name, F ile) , attrInClass (owner, F ile) ,
attrOutOf Class (name, Elememt) , attrOutOf Class (owner, Element) ,
superClass (Object, F ile) , superClass (Object, F older) ,
hasT ype (owner, F older) , hasT ype (name, String) ,
sending (Client, main, F older, name) ,
sending (Client, main, F older, owner) ,
sending (Client, main, F ile, name) ,
sending (Client, main, F ile, owner)]
(9)
The goal state condition is the following:
G =inM odel (Element) ∧ attrInClass (name, Element) ∧
attrInClass (owner, Element) ∧ superClass (Element, F ile) ∧ (10)
superClass (Element, F odler)
The STRIPS planner reaches the goal state by application of satis able operators
(see table 2).
Automated Model Transformations Based on STRIPS Planning 9
Table 2. List of operators application to reach the goal state
Operator application Description
addClass (Element) Add class Element to the model.
changeSup (F ile, Object, Element) Change superclass Object of class
F ile to Element.
changeSup (F older, Object, Element) Change superclass Object of class
F odler to Element.
attrU p (name, Element, F ile, F older) Move attribute name to class
Element from its subclasses F ile
and F older.
attrU p (owner, Element, F ile, F older) Move attribute owner to class
Element from its subclasses F ile
and F older.
The goal state is as follows:
Goal = [inM odel (F older) , inM odel (F ile) ,
inM odel (String) , inM odel (Element) ,
attrInClass (name, Element) , attrInClass (owner, Element) ,
attrOutOf Class (name, F older) ,
attrOutOf Class (owner, F older) ,
attrOutOf Class (name, F ile) , attrOutOf Class (owner, F ile) ,
(11)
superClass (Element, F ile) , superClass (Element, F older) ,
hasT ype (owner, F older) , hasT ype (name, String) ,
sending (Client, main, F older, name) ,
sending (Client, main, F older, owner) ,
sending (Client, main, F ile, name) ,
sending (Client, main, F ile, owner)]
A class model in UML notation corresponding to the goal state is shown in g. 2.
6 Conclusion and Future Work
In this paper we have introduced SBAT transformation engine based on STRIPS
planning system. This engine automates refactoring of the given source model
to a target model ful lling the input condition.
The main asset of SBAT engine for practice is a contribution to an improve-
ment of automation of object model transformations, which consequently would
implicate saved human resources for software projects. Then, these resources
could be allocated for example on software debugging or testing tasks, rather
than on model transformation ones. Another asset should be a theoretical back-
ground for research activities in the area of model transformations.
10 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
Element
*
+owner
Folder File
+name +name
Fig. 2. File system as Composite design pattern
Several consecutive research topics appeared during the SBAT development,
e.g. the model state space optimization by reduction of states count or imple-
mentation of SBAT in some CASE tool.
Acknowledgment
The authors would like to acknowledge the support of the research grant project
SGS10/094 of the Czech Ministry of Education, Youth and Sports.
References
1. Czarnecki K. and Helsen S.: Feature-based survey of model transformation ap-
proaches. In: IBM Systems Journal 2006, vol. 45, no. 3, pp. 621-645. (2006)
2. Fowler M.: Refactoring. Addison-Wesley. ISBN 0-201-48567-2. (1999)
3. Gray J., Lin Y., and Zhang J.: Automating Change Evolution in Model-Driven
Engineering. In Computer 2006, vol. 31, no. 2, pp. 51. (2006)
4. Jézequel J-M.: Model Transformation Techniques. Available online at http://
modelware.inria.fr/static_pages/slides/ModelTransfo.pdf. (2005)
5. Kleppe A. G., Warmer J., and Bast W.: MDA Explained: The Model Driven Ar-
chitecture: Practice and Promise. Boston (MA, USA): Addison-Wesley Longman
Publishing Co., Inc., 170 p. ISBN:032119442X. (2003)
6. Lin Y amd Gray J: A model transformation approach to automatic model construc-
tion and evolution. In Proceedings of the 20th IEEE/ACM international Confer-
ence on Automated Software Engineering, pp. 448-451. (2005)
7. Markovic S.: Composition of UML Described Refactoring Rules. In OCL and Model
Driven Engineering, UML 2004 Conference Workshop, pp. 45-59. (2004)
8. Mens T., Czarnecki K, and Gorp P. V.: A Taxonomy of Model Transformations.
In Language Engineering for Model-Driven Software Development, ser. Dagstuhl
Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für In-
formatik (IBFI), Dagstuhl (Germany). (2005)
9. Nilson N. J. and Fikes R. E. STRIPS: A new approach to the application of theroem
proving to problem solving. Standford Research Institute, Menlo Park (California)
34 p. (1970).
Automated Model Transformations Based on STRIPS Planning 11
10. Opdyke W. Refactoring Object-Oriented Frameworks. University of Illinois at
Urbana-Champaign, Champaign, (IL, USA), PhD. thesis, 197 p. (1992)
11. Object Management Group (OMG): OMG Uni ed Modeling Language (OMG
UML), Infrastructure: Version 2.2. 226 p. Available online at www.omg.org. (2009)
12. Sunyé G., Pollet D., Le Traon Y., Jézéquel J-M.: Refactoring UML Models. In
Proceedings of the 4th International Conference on The Uni ed Modeling Lan-
guage, Modeling Languages, Concepts, and Tools. Springer-Verlag, London (UK),
pp. 134-148. ISBN 3-540-42667-1. (2001)
13. Zhang J., Lin Y., and Gray, J.: Generic and Domain-Speci c Model Refactoring
using a Model Transformation Engine. In Volume II of Research and Practice in
Software Engineering, pp. 199-218. (2005)
Appendix: Primitive Refactorings as STRIPS Operators
Table 3: Primitive refactorings as STRIPS operators
Primitive STRIPS Operator
refactoring
Declaration addClass (c)
Condition outOf M odel (c)
Add-eects inM odel (c)
Add class c
(∀x ∈ B ∩ C) attrOutOf Class (x, c)
(∀x ∈ B ∩ F ) methOutOf Class (x, c)
Delete-eects outOf M odel (c)
Declaration addAttr (a, t, c)
Add attribute a of Condition (∀x) (attrOutOf Class (x, d)
type t into class c ∨¬superClass (x, c) ∨ ¬superClass (c, x)
∨x 6= c) ∧
(∀x) (¬hasT ype (a, x) ∨ (x = t))
Add-eects attrInClass (a, c)
Delete-eects attrOutOf Class (a, c)
Declaration addM eth (µ, c)
Add method µ to Condition methOutOf Class (µ, c)∧ (∀x, y, z)
class c (¬sending (x, y, µ, z) ∨ ¬parent (z, c)
∨ (z 6= c))
Add-eects methInClass (µ, c)
Delete-eects methOutOf Class (µ, c)
Declaration removeClass (c)
Condition inM odel (c)∧ (∀x) (¬parent (c, x)) ∧
Remove class c
(∀x) ¬attrInClass (x, c) ∧
¬methInClass (x, c)
Add-eects outOf M odel (c)
Delete-eects inM odel (c)
12 Old°ich Nouza, Vojt¥ch Merunka, and Miroslav Virius
Primitive STRIPS Operator
refactoring
Declaration removeAttr (a, c)
Remove
Condition attrInClass (a, c) ∧ (∀x, y, z)
attribute a from
(¬sending (x, y, µ, z) ∨ ¬parent (c, z)
class c
∨ (z 6= c))
Add-eects attrOutOf Class (a, c)
Delete-eects attrInClass (a, c)
Declaration removeM eth (µ, c)
Remove method µ Condition methInClass (µ, c) ∧ (∀x, y, z)
from class c (¬sending (x, y, µ, z) ∨ ¬parent (c, z)
∨ (z 6= c))
∧ (∀x, y) (¬sending (x, y, µ, c) ∨ (y = c))
Add-eects methOutOf Class (µ, c)
Delete-eects methInClass (µ, c)
Declaration changeAtrrT ype (a, t, u)
Change type t of Condition hasT ype (a, t)∧super (u, t)
attribute a to u Add-eects hasT ype (a, u)
Delete-eects hasT ype (a, t)
Declaration changeM ethT ype (µ, t, u)
Change type t of
Condition hasRetT ype (µ, t)∧super (u, t)
values returned by
Add-eects hasRetT ype (µ, u)
method µ to u
Delete-eects hasRetT ype (µ, t)
Declaration changeSup(a, b, c)
Change superclass Condition inM odel (c) ∧
b of class a to c superClass (b, a)∧(¬parent (a, c)) ∧
∀ (x, u, v, w) ((¬superClass (x, c)) ∧
(¬superClass (x, b)) ∨
(¬sending (v, w, u, x))
∧ (¬sending (u, x, v, w)))
Add-eects superClass (c, a)
Delete-eects superClass (b, a)
Move attribute a Declaration attrDown (a, c, (b1 , . . . , bn ))
from class c to its Condition attrInClass (a, c) ∧ (∀x)
all subclasses (x = b1 ∨ . . . ∨ x = bn
b1 , . . . , b n ∨¬superClass (c, x))
∧ (∀x, y) ¬sending (x, y, a, c)
Add-eects attrOutOf Class (a, c)
(∀i ∈ n) attrInClass (a, bi )
Delete-eects attrInClass (a, c)
(∀i ∈ n) attrOutOf Class (a, bi )
Move attribute a Declaration attrUp (a, c, (b1 , . . . , bn ))
to class c from all Condition (attrInClass (a, x) ∨ ¬superClass (c, x))
its subclasses ∧ (∀x) ((x 6= b1 ∨ . . . ∨ x 6= bn )
b1 , . . . , b n ∨¬superClass (c, x))
Add-eects attrInClass (a, c)
(∀i ∈ n) attrOutOf Class (a, bi )
Delete-eects attrOutOf Class (a, c)
(∀i ∈ n) attrInClass (a, bi )
Automated Model Transformations Based on STRIPS Planning 13
Primitive STRIPS Operator
refactoring
Declaration methDown (µ, c, b)
Copy methodµ
Condition methInClass (µ, c) ∧
from class c to its
methOutOf Class (µ, b)
subclass b
∧ (superClass (c, b))
Add-eects methInClass (µ, b)
Delete-eects methOutOf Class (µ, b)
Declaration methUp (µ, c, b)
Copy method µ to
Condition methOutOf Class (µ, c) ∧
class c from its
methInClass (µ, b)
subclass b
∧ (superClass (c, b))
Add-eects methInClass (µ, c)
Delete-eects methOutOf Class (µ, c)
Add message η Declaration addSend (µ, c, η, d)
sent to objects of Condition (¬sending (µ, c, η, d) ∧ methInClass (µ, c)
class d from ∨ (∃x) ((parent (x, d) ∨ (x = d)) ∧
method µ of (methInClass (η, x))
class c ∨ (attrInClass (η, x))))
∧ (∀x, y) (¬sending (x, y, µ, c)
∧ (c 6= Client))
Add-eects sending (µ, c, η, d)
Delete-eects ∅
Remove message η Declaration removeSend (µ, c, η, d)
sent to objects of Condition sending (µ, c, η, d) ∧ (c 6= Client)
class d from ∧ (∀x, y) (¬sending (x, y, µ, c))
method µ of Add-eects ∅
class c Delete-eects sending (µ, c, η, d)
Split message Declaration splitSend (µ, c, η, d, l, e)
sending d C η to Condition sending (µ, c, η, d) ∧ attrInClass (l, d)
(d C l) C η , where ∧hasT ype (l, e)
l is of type e. Add-eects sending (µ, c, l, d)
sending (µ, c, η, e)
Delete-eects sending (µ, c, η, d)
Merge message Declaration mergeSend (µ, c, η, d, l, e)
sending Condition sending (µ, c, η, e) ∧ sending (µ, c, l, d)
(d C l) C η into ∧attrInClass (l, d) ∧ hasT ype (l, e)
d C η , where l is of Add-eects sending (µ, c, η, d)
type e. Delete-eects sending (µ, c, l, d)
sending (µ, c, η, e)