Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions


Electronic Communications of the EASST
Volume 39 (2011)

Graph Computation Models
Selected Revised Papers from the
Third International Workshop on

Graph Computation Models (GCM 2010)

Formal Specification of Model Transformations by Triple Graph
Grammars with Application Conditions

Ulrike Golas, Hartmut Ehrig and Frank Hermann

26 pages

Guest Editors: Rachid Echahed, Annegret Habel, Mohamed Mosbah
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

Formal Specification of Model Transformations by Triple Graph
Grammars with Application Conditions

Ulrike Golas1, Hartmut Ehrig2 and Frank Hermann23

1 golas@zib.de, Konrad-Zuse-Zentrum für Informationstechnik Berlin, Germany
2 ehrig|frank@cs.tu-berlin.de, Technische Universität Berlin, Germany

3 frank.hermann@uni.lu, SnT, Université du Luxembourg, Luxembourg

Abstract: Triple graph grammars are a successful approach to describe exogenous
model transformations, i.e. transformations between models conforming to differ-
ent meta-models. Source and target models are related by some connection part,
triple rules describe the simultaneous construction of these parts, and forward and
backward rules can be derived modeling the forward and backward model transfor-
mations. As shown already for the specification of visual models by typed attributed
graph transformation, the expressiveness of the approach can be enhanced signifi-
cantly by using application conditions, which are known to be equivalent to first
order logic on graphs.

In this paper, we extend triple rules with a specific form of application conditions,
which enhance the expressiveness of formal specifications for model transforma-
tions. We show how to extend results concerning information preservation, termi-
nation, correctness, and completeness of model transformations to the case with
application conditions. We illustrate our approach and results with a model trans-
formation from statecharts to Petri nets.

Keywords: model transformation, triple graph grammar, application condition

1 Introduction

Specification of models and model transformations play a central role in model-driven software
development. For the specification of visual models and languages, it is common practice to
use UML modeling techniques for the concrete syntax with underlying typed attributed graph
transformation for the abstract syntax. The visual language can be defined in a declarative way
by a meta-model with OCL-constraints or – on the abstract level – by a type graph and suitable
graph constraints. Alternatively, the visual language can be generated on the abstract level by
typed attributed graph grammars [EEPT06]. It is well-known that the expressiveness of such
generative approaches can be enhanced by using graph grammar rules with negative application
conditions (NACs), or even more by using nested application conditions in the sense of [HP09],
which are known to be equivalent to first order logic on graphs and more expressive than NACs.

Graph transformation is a suitable approach to define model transformations [TEG+05]. Espe-
cially for exogenous model transformations, triple graph grammars (TGGs) [Sch94] are a well-
suited formalism [SK08] and they were successfully applied in several domains [KS06, GL06a,
GL06b]. Formal properties concerning information preservation, termination, correctness, and

1 / 26 Volume 39 (2011)

mailto:golas@zib.de
mailto:ehrig$|$frank@cs.tu-berlin.de
mailto:frank.hermann@uni.lu


Triple Graph Grammars with Application Conditions

completeness of model transformations have been studied already in [EEH08, EEHP09] based
on triple rules without NACs, where the decomposition and composition theorem for triple graph
transformation sequences in [EEE+07] plays a fundamental role. In [EHS09], this theorem has
been extended to triple rules with NACs, but not yet to nested application conditions [HP09].

It is the main aim of this paper to extend the theory of model transformations based on TGGs
to rules with nested application conditions, short application conditions, in order to enhance
the expressiveness of model transformations including the generation of the source and target
languages by corresponding source and target rules. We show that the decomposition and com-
position theorem can be extended to rules with application conditions. This allows to enhance the
expressiveness of model transformations and to extend termination, correctness, completeness,
and backward information preservation to this more general framework.

As a case study, we consider a model transformation from statecharts to Petri nets, where we
use a combination of positive and negative application conditions and boolean operators as avail-
able in the framework of general application conditions, but not in the more restrictive framework
of NACs. In our example, only one level of nesting is sufficient to model the necessary condi-
tions, but the theory is developed for more complex situations as introduced in [Gol11].

This paper is organized as follows. In Section 2, we review triple rules and application con-
ditions. We illustrate our approach with a model transformation from statecharts to Petri nets in
Section 3. This case study is used as illustrating example in Section 4, where we define model
transformations based on TGGs with application conditions leading to termination, correctness,
completeness, and backward information preservation. A conclusion including related and future
work is presented in Section 5.

We assume the reader to be familiar with the basics of UML statecharts [OMG09], Petri nets
[Pet80], and graph transformation in the double pushout approach [EEPT06].

2 Review of Triple Graph Grammars and Application Conditions

Triple graph grammars [Sch94] are a well known approach for bidirectional model transforma-
tions. In [KS06], the basic concepts of triple graph grammars are formalized in a set-theoretical
way, which is generalized and extended in [EEE+07] to typed, attributed graphs.

A triple graph G = (GS
sG← GC

tG→ GT ) consists of graphs GS, GC, and GT , called source,
connection, and target component, and two graph morphisms sG and tG mapping the connection
to the source and target components. A triple graph morphism f : G1 → G2 matches the single
components and preserves the connection part.

The typing of a triple graph is done in the same way as for standard graphs via a type graph
T G - in this case a triple type graph - and a typing morphism typeG from the graph G into
this type graph leading to the typed triple graph (G,typeG). A typed triple graph morphism
f : (G1,typeG1)→ (G2,typeG2) is a triple graph morphism f such that typeG2 ◦ f = typeG1 .

Triple graphs and typed triple graphs, together with the component-wise compositions and
identities, form the categories TripleGraphs and Triple-GraphsTG. When speaking of triple
graphs, we consider both triple graphs and typed triple graphs, but do not explicitly mention the
typing. Moreover, we define the morphism class M of injective triple graph morphisms which
is used throughout the paper. Using this class M , both categories can be extended to weak

GCM 2010 2 / 26



ECEASST

adhesive HLR categories [EEPT06] which allows us to instantiate the theory to transformations
of triple graphs. The categorical foundations of weak adhesive HLR categories are not essential
to understand this paper.

L R

G H

LS LC LT

GS GC GT
RS RC RT

HS HC HT

tr

f

m n

sL tL

sG tG

mS
mC mT

sR tR

sH tH

nS nC
nT

trS trC trT

fS fC fT

(1)

A triple rule tr = (L
tr→ R)

consists of triple graphs L and
R, and an M -morphism tr : L →
R. Since triple rules are non-
deleting, we do not need a span
of morphisms for a rule. A direct
triple transformation G =

tr,m
==⇒ H

of a triple graph G via a triple rule tr and a match m : L → G is given by the pushout (1), which
is constructed as the component-wise pushouts in the S-, C-, and T -components, where the mor-
phisms sH and tH are induced by the pushout of the connection component. Note, that due to the
structure of the triple rules, double and single pushout approach are equivalent in this case.

A triple graph transformation system T GS = (T R) is based on triple graphs with a set T R of
rules over them. A triple graph grammar T GG = (T R,S) contains in addition a triple start graph
S. For triple graph grammars, the generated language is defined by V L = {G | ∃ triple trans-
formation S

∗⇒ G via rules in T R}. Moreover, the source language V LS = {GS | (GS
sG← GC

tG→
GT )∈V L} contains all standard graphs that are the source component of a derived triple graph.
Similarly, the target language V LT ={GT | (GS

sG← GC
tG→ GT )∈V L} contains all derivable target

components.

trS =
LS ∅ ∅

RS ∅ ∅

∅ ∅

∅ ∅

trS ∅ ∅

trT =
∅ ∅ LT

∅ ∅ RT

∅ ∅

∅ ∅

∅ ∅ trT

trF =
RS LC LT

RS RC RT

trS◦sL tL

sR tR

idRS trC trT

trB =
LS LC RT

RS RC RT

sL trT◦tL

sR tR

trS trC idRT

From a triple rule, we can derive a source rule trS and a
target rule trT , which specify the changes done by this
rule in the source and target components, respectively.
Moreover, the forward rule trF and the backward rule trB
describe the changes done by the rule to the connection
and target resp. source parts, assuming that the source
resp. target rules have been applied already. Intuitively,
the source rule creates a source model, which can then be
transformed by the forward rules into the corresponding
target model. This means that the forward rules define the
actual model transformation from source to target models.
Vice versa, the target rules create the target model, which
can then be transformed into a source model applying the
backward rules. Thus, the backward rules define the back-
ward model transformation from target to source models.

An important extension is the use of rules with suitable application conditions as done in the
next sections. Simple variants are positive application conditions of the form ∃a for a morphism
a : L → C, demanding a certain structure in addition to L, and negative application conditions
¬∃a, forbidding such a structure. A match m : L → G satisfies ∃a (¬∃a) if there is a (no) M -
morphism q : C → G satisfying q◦a = m. In more detail, we use nested application conditions
[HP09], short application conditions, which are defined recursively. The application condition

3 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

L C

G

acC
a

m q

true is always satisfied. A more complex application condition ∃(a,acC)
on L consists of a morphism a : L →C and an application condition acC
on C. For satisfaction, in addition to the existence of q it is required that q
satisfies acC. Moreover, application conditions are closed under boolean
operations. We use ∃a as a short notion for ∃(a,true) and false for ¬true.
In general, we write m |=∃(a,acC) if m satisfies ∃(a,acC), and acC ∼= ac′C denotes the semantical
equivalence of acC and ac′C on C. In the diagrams, an application condition acC on C is depicted
by a triangle pointing towards C.

In order to handle rules with application conditions there are two important concepts, called
the shift of application conditions over morphisms and morphism spans ([HP09, EHL10]):

1. Given an application condition acL on L and a morphism t : L→L′ then there is an applica-
tion condition Shift(t,acL) on L′ such that for all m′ : L′→G holds: m′ |= Shift(t,acL)⇐⇒
m = m′◦t |= acL.

For acL = ∃(a,ac′L) we define Shift(t,acL) = ∨(a′,t′)∈F∃(a
′,Shift(t′,ac′L)) with

F ={(a′,t′) | (a′,t′) jointly epimorphic,t′ ∈ M ,t′◦a = a′◦t},

L C

L′ C′

acL

Shift(t,acL)

ac′L

Shift(t′,ac′L)

L R

Y X

acR

ac′RL(tr
∗,ac′R)

L(tr,acR) tr

tr∗

b a(1)

a

t t′

a′

2. Given a triple rule tr = (L
tr→ R) and an application condition acR on R then there is an

application condition L(tr,acR) on L such that for all transformations G =
tr,m
==⇒ H with

comatch n holds: m |= L(tr,acR)⇐⇒ n |= acR.

For acR = ∃(a,ac′R) we define L(tr,acR) = ∃(b,L(tr
∗,ac′R)) if a◦tr has a pushout com-

plement (1) leading to tr∗, and L(tr,∃(a,ac′R)) = false otherwise.

R1L1 L2 R2

EL R

ac1 ac2

ac

tr1

tr∗1

e1
u1

tr2

e2

One of the main results for graph transformation
needed in this paper is the Concurrency Theorem,
which is concerned with the execution of transforma-
tions which may be sequentially dependent. Given
an arbitrary sequence G =

tr1,m1
===⇒ H =

tr2,m2
===⇒ G′ of di-

rect transformations it is possible to construct an E-
concurrent rule tr1 ∗E tr2 = (L → R,ac). The object E
is a jointly surjective overlap of R1 and L2. The con-
struction of the concurrent application condition ac =
Shift(u1,ac1)∧L(p∗,Shift(e2,ac2)) and p∗ = (L

s1←C1
t1→ E) is again based on the two shift con-

structions. The Concurrency Theorem states that for the transformation G =
tr1,m1
===⇒ H =

tr2,m2
===⇒ G′

the E-concurrent rule tr1 ∗E tr2 allows us to construct a direct transformation G =
tr1∗E tr2
====⇒ G′ via

tr1 ∗E tr2, and vice versa, each direct transformation tr1 ∗E tr2 can be sequentialized.

GCM 2010 4 / 26



ECEASST

3 Model Transformation from Statecharts to Petri Nets

In this section, we define a model transformation from a variant of UML statecharts [OMG09] to
Petri nets [Pet80] using triple rules and application conditions. Statecharts may have orthogonal
regions as well as state nesting. As a small restriction, we do not handle entry and exit actions,
do not allow extended state variables, allow guards only to be conditions over active states, and
allow only a depth of two for hierarchies of states. For the target language of Petri nets, we use
nets with inhibitor arcs, contextual arcs, and open places. A transition with an inhibitor arc from
a place (denoted by a filled dot instead of an arrow head) is only enabled if there is no token on
this place. A contextual arc between a place and a transition (denoted by an edge without arrow
heads), also known as read arc in the literature, means that this token is required for firing, but
remains on the place. Open places allow the interaction with the environment, i.e. token may
appear or disappear without firing a transition within the net. We assume all places to be open.
With these restrictions for statecharts and extensions for Petri nets we are able to define a model
transformation from statecharts to Petri nets which preserves the semantical behavior, at least on
an informal level.

error

call

repair

prod

produced

prepare

empty

full

wait

consumed

arrive

finish

repair

finish

exit
next

produce
[empty]
/incbuff

fail

inc-
buff

dec-
buff

next
consume
[full]

/decbuff

Figure 1: The example statechart in concrete syntax

In Figure 1, the stat-
echart ProdCons is de-
picted modeling a producer-
consumer system. The
whole state machine con-
tains one region with the
states prod, error, and
a final state. When initial-
ized, the system is in the
state prod, which has three
regions. There, in parallel a producer, a buffer, and a consumer may act. The producer alternates
between the states produced and prepare, where the transition produce models the actual
production activity. It is guarded by a condition that the parallel state empty is also current,
meaning that the buffer is empty and may actually receive a product, which is then modeled by
the action incbuff denoted after the /-dash. Similarly to the producer, the buffer alternates
between the states empty and full, and the consumer between wait and consumed. The
transition consume is again guarded by the state full and followed by a decbuff-action
emptying the buffer.

Two possible events may happen causing a state transition leaving the state prod: the con-
sumer may decide to finish the complete run or there may be a failure detected after the produc-
tion leading to the error-state. Then, the machine has to be repaired before the error-state
can be exited via the corresponding exit-transition and the standard behavior in the prod-state
is executed again.

For the modeling, we use typed attributed graphs, which are an extension of typed graphs by
attributes [EEPT06]. We do not give details here, but use an intuitive approach to attribution,
where the attributes of a node are given in a class diagram-like style. For the values of attributes
in the rules we can also use variables. Note, that for the typing of the edges we omit the edge
types if they are clear from the node types they are connecting.

5 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

SM

name:String

R

E

name:String

T

S

name:String
isInitial:Bool

isFinal:Bool

A

name:String

G

R-T3

E-P

T-T

S-P

S-Pe

S-T1

S-T2

place

transition

pre inhibitor
contextualpost

region

regions

states

trigger

action guard

begin

end

con-
dition

sT G tT G

Figure 2: The triple type graph T G

In Figure 2, the triple type graph T G is depicted, containing in the left the source component of
statecharts in abstract syntax, in the right the target component of Petri nets, and the connection
component inbetween. To obtain valid statechart models, some constraints are needed which are
described in the following but are not shown explicitly.

Each diagram consists of exactly one state machine SM containing one or more regions R. A
region contains states S, where state names are unique within one region. A state may again con-
tain one or more regions. Each region is contained in either exactly one state or the state machine.
Moreover, states may be initial (attribute value isInitial = true) or final (attribute value
isFinal=true), each region has to contain exactly one initial and at most one final state, and
final states cannot contain regions. A transition T begins and ends at a state, is triggered by an
event E, and may be restricted by a guard G and followed by an action A. A guard has one or
more states as conditions. There is a special event with attribute value name="exit" which is
reserved for exiting a state after the completion of all its orthogonal regions, which cannot have
a guard condition. Moreover, final states cannot be the beginning of a transition and their name
attribute has to be set to name="final". In addition, transitions cannot link states in different
orthogonal regions, which means that both regions are directly contained in the same state.

The language V LSC consists of all typed attributed graphs respecting the source component
T GS of the type graph T G and the constraints as described above.

In the following, we present the triple rules that create simultaneously the statechart model,
the connection part, and the corresponding Petri net. For simplicity, we depict the Petri nets
in the target component in concrete syntax, while only writing node names in the connection
component.

0
state0

state2

state1 1

2

T a

state4

state3 3

4

Ta a

Figure 3: The basic correspondences

In general, each state of the state-
chart model is connected to a place in
the Petri net, where a token on it rep-
resents that this state is current. Transi-
tions between states are mapped to Petri
net transitions and fire when the corre-
sponding state transition occurs. Events
are also connected to places, where all
events with the same name share the
same Petri net place. They are connected via a contextual arc to their corresponding transition

GCM 2010 6 / 26



ECEASST

thus enabling the simultaneous firing of all enabled Petri net transitions when a token is placed
there. By using contextual arcs it is possible that all transitions connected to an event with this
name are enabled simultaneously if also their other pre-places are marked. Otherwise, we would
not be able to fire all these transitions concurrently. They would not be independent but compete
for the token. For independence, we had to know in advance how many of these transitions will
fire to allocate that number of tokens on the event’s place. For a guard, the Petri net transition of
its transition in the statechart diagram is the target of a contextual arc from the place connected
to the condition. Thus, we check also in the Petri net that this guard condition is fulfilled, i.e. the
corresponding place holds a token, before firing the transition. Such a basic situation is depicted
in Figure 3, where altogether five states and their corresponding places, two transitions – both
in the statechart and the Petri net – and an event a with its corresponding place are shown. The
hierarchy of the statechart is flattened, since Petri nets do not have such a concept. Note that all
place are open places.

0
state0

state2

state1 1

2

T a

state4

state3 3

4

T

T2 T2

T2 T2

T3 T3

a a

0
state0

state1 1

f

T a

state3 3

f

T

T1

a a

Figure 4: The additional correspondences

Additional places and transi-
tions make sure that the ef-
fects of a state transition con-
cerning involved sub- or super-
states can be simulated also in
the Petri net part. Each substate
is connected via S-T2 to a T2-
transition which is the target of a
pre-arc from its superstate. This
makes sure that, when a state tran-
sition leaves this superstate, also
all substates are no longer cur-
rent. Each region within a state
is connected via R-T3 to a T3-
transition which makes sure that,
when no state inside this region is
current, also the superstate is deactivated. These two situations are depicted in the example
models in the top of Figure 4. Each state that may contain regions is connected via S-T1 to a
T1-transition that is the target of pre-arcs from all places of final states and inhibitor arcs from
all other places in its regions, while the superstate’s place is a contextual place as shown in the

state0
0

state1

1

2

T

af

e

e

exit

TT1

T1

T2

T2

T3

state3

a

exit

Figure 5: The handling of exit-events

bottom of Figure 4. This makes
sure that, when all substates are fi-
nal, these substates are no longer
current and, if it exists, the exit-
action of the superstate can be
initiated. For the handling of
the special "exit"-events, each
state which may be a superstate is
connected via S-Pe to an e-place
which handles the proper execu-
tion of this event regarding T1-

7 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

and T3-transitions. The idea behind this place is, that when all final states are reached and
an exit transition has to be invoked, the T1-transition delivers a token to the e-place which than
triggers the execution of the transition in the Petri net as shown in Figure 5.

For the operational semantics, all places in the Petri net corresponding to currently active
states will be marked. Depending on the semantical steps in the statechart, the open places in the
Petri net produce and delete tokens. For example, triggering an external event in the statechart
leads to a token on the events’s place in the Petri net. Also for the handling of the hierarchical
(de)activation the proper open places may fire triggered by the corresponding semantical rules
for the statecharts. For example, when entering a state it’s initial substates become active. This
has to be handled in the Petri net by firing the corresponding open places. Thus, the Petri net
for itself shows different semantical behavior than the statechart, since arbitrary firing of open
places leads to strange behavior, but every semantical step in the statechart can be simulated by
the Petri net. The rules for the operational semantics of statecharts are given in [GBEE11].

start

L0,S
∅

L0,C
∅

L0,T
∅

∅
R0,S R0,C R0,T

∅
SM

name="sm"

ac0 =¬∃p0
L0 ∅ ∅

SM

name="sm"

tr0,S tr0,C tr0,T

tL0sL0

tR0sR0

p0

Figure 6: The rule start

The start graph is the empty graph, and the first rule
to be applied is the triple rule start shown in Figure 6
which creates the start graph of statecharts in the source
component, and empty connection and target compo-
nents. The application condition ac0 is a so-called neg-
ative application condition (NAC) and forbids that the
right hand side of the rule already exists before the rule is
applied. Since a statemachine has exactly one node SM,
the NAC ensures that the rule cannot be applied twice.

In Figure 7, the triple rules newRegionSM and
newRegionS are depicted which allow to create a new
region of a state machine or of a state, respectively. Since each region has to have an ini-
tial state, this initial state is also created and connected to its corresponding place via S-P.
With newRegionSM, the initial state is also connected to a T1-transition in the target com-
ponent and another place via S-Pe. Moreover, if the new region is created inside a state by
newRegionS the substate is the inhibitor of the superstate’s T1-transition, the superstate in-
hibits a new T2-transition and the region and the substate inhibit a new T3-transition. For the
triple rule newRegionS, the application condition forbids that the superstate is final or already
a substate of another state. newRegionSM has the application condition true which is not de-
picted. Note that we allow parameters for the rules to define the attributes. Thus, the user has to
declare the name of the newly created state when applying these triple rules.

In Figs. 8 and 9, the triple rules for creating new states are shown. With newStateSM and
newStateS, new states inside a region of the state machine or of a state are created, which are
not final states. Similarly, final states are created by the triple rules newFinalStateSM and
newFinalStateS. In all cases, a corresponding place is created in the target component. As
in the case of a new region, if creating a state as a substate of another state, there is a new T2-
transition with this superstate as inhibitor and the new place inhibits the region’s T3-transition.
In case of a non-final substate, this substate inhibits the T1-transition of the superstate, whereas
a final state within a state has to be connected to this superstate’s T1-transition as a pre place.
The application conditions of these rules make sure that the new state name is unique within its
region and that, for final states, only one final state per region is allowed.

GCM 2010 8 / 26



ECEASST

newRegionSM(sname:String)

L1,S L1,C L1,T
1:SM

∅ ∅

R1,S R1,C R1,T

1:SM

R

S

name=sname
isInitial=true

isFinal=false

e

T1

S-P

S-Pe

S-T1

newRegionS(sname:String)

L2,S L2,C L2,T
1:S

S-P
S-Pe
S-T1

e

T1

R2,S R2,C R2,T

1:S

R

S

name=sname
isInitial=true

isFinal=false

e

T2

T3
T1

S-P
S-Pe

S-P

R-T3

S-T2

S-T1

ac2 =¬∃p2 ∧¬∃q2

L2
1:S

isFinal=true

S-P
S-Pe
S-T1

L2 S R 1:S
S-P
S-Pe
S-T1

p2

q2

sL1 tL1

sR1 tR1

tr1,S tr1,C tr1,T

sL2 tL2

sR2 tR2

tr2,S tr2,C tr2,T

Figure 7: The triple rules newRegionSM and newRegionS

For the creation of a new transition, the triple rules newTransitionNewEvent,
newTransitionNewExit, newTransitionOldEvent, and newTransitionOld-
Exit in Figure 10 and Figure 11 are used. A new transition in the source part connected with
a new Petri net transition in the target part is created, and in case of a new event, this event is
connected with a new place which is a contextual place for the transition. Otherwise, the tran-
sition is connected with the place of the already existing event. In case of an exit-event, the
place connected via S-Pe to the begin-state has to be connected to the new transition and the
begin-state’s T1-transition. The application conditions forbid that the begin-state is a final
state and that states over different regions are connected by a transition (r7,s7,t7,u7), and ensure

9 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

newStateSM(sname:String)

L3,S L3,C L3,T

1:SM

2:R

∅ ∅

R3,S R3,C R3,T

1:SM

2:R

S

name=sname
isInitial=false

isFinal=false
T1

S-P

S-T1

eS-Pe

ac3 =¬∃p3 L3 1:SM 2:R
S

name=sname
∅ ∅

newStateS(sname:String)

L4,S L4,C L4,T

1:S

2:R

S-P

R-T3
S-T1 T1

T3

R4,S R4,C R4,T

1:S

2:R

S

name=sname
isInitial=false

isFinal=false
T2

T3 T1

S-T1
S-P

S-P

S-T2

R-T3

ac4 =¬∃p4 L4 1:S 2:R
S

name=sname

S-P

R-T3
S-T1

p3

p4

sL3 tL3

sR3 tR3

tr3,S tr3,C tr3,T

sL4 tL4

sR4 tR4

tr4,S tr4,C tr4,T

Figure 8: The triple rules newStateSM and newStateS

that exit-events only begin at superstates, i.e. a state containing a region. Note that the objects
and morphisms used for the application conditions ac8, ac9, and ac10 are not shown explicitly,
but they correspond to the objects and morphisms used in ac7.

In Figure 12, the triple rules newGuard and nextGuard are shown which create the guard
conditions of a transition. The guard condition is a state whose corresponding place is connected
via a contextual arc to the corresponding net transition. The application conditions ensure that
only one guard per transition is allowed and that a transition with exit-event is not guarded at
all. With the rule newAction in Figure 12, an action is added to a transition in the statechart
model if none is specified yet.

GCM 2010 10 / 26



ECEASST

newFinalStateSM

L5,S L5,C L5,T

1:SM

2:R

∅ ∅

R5,S R5,C R5,T

1:SM

2:R

S

name="final"
isInitial=false

isFinal=true

S-P

ac5 =¬∃p5 L5 1:SM 2:R
S

isFinal=true
∅ ∅

newFinalStateS

L6,S L6,C L6,T

1:S

2:R

S-T1
S-P
R-T3

T1

T3

R6,S R6,C R6,T

1:S

2:R

S

name="final"
isInitial=false

isFinal=true

T1

T2 T3

S-T1

S-P

S-P

R-T3

S-T2

ac6 =¬∃p6 L6 1:S 2:R
S

isFinal=true

S-T1
S-P
R-T3

p5

p6

sL5 tL5

sR5 tR5

tr5,S tr5,C tr5,T

sL6 tL6

sR6 tR6

tr6,S tr6,C tr6,T

Figure 9: The triple rules newFinalStateSM and newFinalStateS

An integrated model containing the statechart example in Figure 1 in its source component
can be constructed by the application of the following triple rules:

1× start creating the state machine,
1× newRegionSM creating the one region inside the state machine and the initial state prod,
1× newStateSM creating the state error,
4× newRegionS creating one region within error including the initial state call and the

three regions within prod including the initial states produced, empty, and wait,
4× newStateS creating the state repair within error and the states prepare, full,

and consumed within prod,

11 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

newTransitionNewEvent(ename:String)

L7,S L7,C L7,T

1:S

2:S

S-P
S-P

R7,S R7,C R7,T

1:S

2:S

T

E

name=ename

T

S-P

S-P

E-P

T-T

ac7 = ename 6= ”exit”∧¬∃p7 ∧¬∃q7 ∧(∃r7 ∨∃s7 ∨∃t7 ∨∃u7)

L7
1:S

2:S

E

name=ename

S-P

S-P
L7

2:S

1:S

isFinal=true
S-P

S-P

L7
R

1:S 2:S

S-P

S-P
L7

RR R

S S1:S 2:S

S-P

S-P

L7

R

S 2:S

R 1:S

S-P

S-P

L7

R

1:S S

R2:S

S-P

S-P

newTransitionNewExit

L8,S L8,C L8,T

1:S

2:S

S-Pe
S-T1
S-P
S-P

e T1

R8,S R8,C R8,T

1:S

2:S

T

E

name="exit"

T

e
T1

S-Pe
S-T1
S-P
S-P

E-P

T-T

ac8 =¬∃p8 ∧¬∃q8 ∧∃v8∧
(∃r8 ∨∃s8 ∨∃t8 ∨∃u8) L8

1:S 2:S

R

S-Pe
S-T1
S-P

S-P
e T1

begin
end

begin
end

sL7 tL7

sR7 tR7

tr7,S tr7,C tr7,T

p7 q7

r7 s7

v8

t7 u7

sL8 tL8

sR8 tR8

tr8,S tr8,C tr8,T

Figure 10: newTransitionNewEvent and newTransitionNewExit

GCM 2010 12 / 26



ECEASST

newTransitionOldEvent

L9,S L9,C L9,T

1:S

2:S

3:E

name=ename

S-P

S-P

E-P

R9,S R9,C R9,T

1:S

2:S

T

E

name=ename

3:E

name=ename

T

S-P

S-P

E-P

E-P

T-T

ac9 = ename 6= ”exit”∧¬∃q9 ∧(∃r9 ∨∃s9 ∨∃t9 ∨∃u9)

newTransitionOldExit

L10,S L10,C L10,T

1:S
2:S

3:E

name="exit"

S-Pe
S-T1
S-P
S-P
E-P

e T1

R10,S R10,C R10,T

1:S

2:S

T

E

name="exit"

3:E

name="exit"
T

e
T1

S-Pe
S-T1
S-P
S-P

E-P
E-P

T-T

ac10 =¬∃q10 ∧(∃r10 ∨∃s10 ∨∃t10 ∨∃u10)∧∃v10

sL9 tL9

sR9 tR9

tr9,S tr9,C tr9,T

begin
end

sL10 tL10

sR10 tR10

tr10,S tr10,C tr10,T

begin
end

Figure 11: newTransitionOldEvent and NewTransitionOldExit

1× newFinalStateSM creating the final state of the state machine,
1× newFinalStateS creating the final state within error,
9× newTransitionNewEvent creating all transition except for the exit-transition be-

tween error and prod and the next-transition between consumed and wait,
1× newTransitionExit creating the exit-transition between error and prod,
2× newTransitionOldEvent creating the next-transition between consumed and wait

with the already known event next,
2× newGuard creating the guards of the produce- and consume-transitions,
2× newAction creating the actions of the produce- and consume-transitions.

In the target component we find the Petri net depicted in Figure 13 (without the initial marking),
where we have labeled the places and transitions with the names of the corresponding statechart
elements and correspondence node names to ease the recognition.

13 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

newGuard

L11,S L11,C L11,T

1:S

2:T

S-P

T-T
T

R11,S R11,C R11,T

1:S

2:T

G

T

S-P

T-T

ac11 =¬∃p11 ∧¬∃q11 ∧¬∃r11 L11 1:S 2:T S-P T-T

L11 1:S 2:T G S-P T-T

L11 1:S 2:T
E

name="exit"
S-P T-T

nextGuard

L12,S L12,C L12,T

1:S

2:T

3:G

S-P

T-T
T

R12,S R12,C R12,T

1:S

2:T

3:G

T

S-P

T-T

ac12 =¬∃p12 ∧¬∃q12

L12 1:S 2:T3:G S-P T-T

L12 1:S 2:T3:G S-P T-T

newAction(aname:String)

L13,S L13,C L13,T
1:T T-T T

R13,S R13,C R13,T
1:T

A

name=aname
TT-T

ac13 =¬∃p13 L13 1:TA T-T

sL12 tL12

sR12 tR12

tr12,S tr12,C tr12,T

q12

p12

sL11 tL11

sR11 tR11

tr11,S tr11,C tr11,T

p11

q11

r11

sL13 tL13

sR13 tR13

tr13,S tr13,C tr13,T

p13

Figure 12: The triple rules newGuard, nextGuard, and newAction

GCM 2010 14 / 26



ECEASST

produced

prepare

empty

f ull

wait

consumed

next

produce

incbu f f

decbu f f

consume

prod

f ail

exit

error

call

repair

f inal

arrive

repair

e

error

e

prod

f inish

f inal

T

T

T

T

T

T

T2 T2 T2

T2 T2 T2

T1

prod

T T

T1

error

T2

T2

T2

T

T

T

T

T3 T3 T3

T3

Figure 13: The Petri net corresponding to the statechart in Figure 1

error

call

repair

prod

produced

prepare

empty

full

wait

consumed

arrive

finish

repair

finish

exit
next

produce
[empty]
/incbuff

fail

inc-
buff

dec-
buff

next
consume
[full]

/decbuff

Figure 14: The statechart after the initialization step

We do not want to show
the weak simulation relation
between the statecharts se-
mantics and the Petri net
completely (see [Gol11]),
but give some intuition how
it works. First, the ini-
tialization takes place. For
the statechart, this leads
to the active states prod,
produced, empty, and wait as shown in Figure 14 with thicker lines, since the initial state
and all its initial substates are invoked. In the Petri nets, the corresponding open places create a
token leading to the initial marking depicted in Figure 13.

For the first semantical step, an external trigger element next appears. The state transition de-

15 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

activates the state produced and activates the state prepare. In the Petri net, the next-place
generates a token. Now the T-transition with next and produced as pre-places is activated
and fires. Since no other transition is activated, deleting the next-token leads to the result-
ing Petri net simulation step with tokens on the places prod, prepare, empty, and wait
corresponding to the statechart’s current semantical state.

The source rules including suitable derived application conditions represent a generating
grammar for our statechart models. All models are typed over the type graph and respect the
specified constraints. For the target rules, only a subset of Petri nets can be generated, but all
models obtained from transformations using the target rules are well-formed, because they are
typed over the Petri net type graph and we cannot generate double arcs. This is due to the fact that
the rules either create only arcs from or to a new element or the multiple application is forbidden
as for the rule newGuard by the expression ¬∃p11 within the application condition ac11.

4 Model Transformations with Application Conditions

As shown by the model transformation from statecharts to Petri nets, rules with application con-
ditions are more expressive and allow to restrict the application of the rules. Thus, we enhance
triple rules and combine a triple rule tr without application conditions with an application condi-
tion ac over L. Then a triple transformation is applicable if the match m satisfies the application
condition ac. From now on, a triple rule denotes a rule with application conditions, while the
absence of application conditions is explicitly mentioned.

First, we introduce triple rules which construct the source, connection, and target parts in one
step. From these triple rules we derive later the operational source and forward rules for the
model transformation.

Definition 1 (Triple rule and transformation) A triple rule tr = (tr : L → R,ac) consists of
triple graphs L and R, an M -morphism tr : L → R, and an application condition ac over L.

A direct triple transformation G =
tr,m
==⇒ H of a triple graph G via a triple rule tr and a match m :

L → G with m |= ac is given by the direct triple transformation G =
tr,m
==⇒ H via the corresponding

triple rule without application conditions.

Example 1 Examples for triple rules using application conditions have been shown in Section 3.

For the extension of the derived rules with application conditions, we need more specialized
application conditions that can be assigned to the source and forward rules.

Definition 2 (Special application conditions) Given a triple rule tr : L → R, an application
condition ac =∃(a,ac′) over L with a : L → P is an

• S-application condition if aC, aT are identities, i.e. PC = LC, PT = LT , and ac′ is an S-
application condition over P, and

• S-extending application condition if aS is an identity, i.e. PS = LS, and ac′ is an S-extending
application condition over P.

GCM 2010 16 / 26



ECEASST

(LS LC LT )

(PS PC = LC PT = LT )

ac

ac′

S-application condition S-extending application condition

(LS LC LT )

(PS = LS PC PT )

ac

ac′

sL tL

sP tP=tL

aS idLC idLT

sL tL

sP tP

idLS aC aT

Moreover, true is an S- and S-extending application condition, and if ac, aci are S- or S-extending
application conditions for some index set I so are ¬ac, ∧i∈I aci, and ∨i∈I aci.

For the assignment of the application condition ac to the derived rules, the application condi-
tion has to be consistent to the source and forward rules, which means that we must be able to
decompose ac into S- and S-extending application conditions.

Definition 3 (S-consistent application condition) Given a triple rule tr = (tr : L → R,ac), then
ac is S-consistent if it can be decomposed into ac ∼= ac′S ∧ac

′
F such that ac

′
S is an S-application

condition and ac′F is an S-extending application condition.

Checking S-consistency for arbitrary application conditions may be complex. Thus, we gen-
erally assume that the designer of the triple rules specifies only conjunctions of S-application
conditions and S-extending application conditions. From the application point of view, this still
provides sufficient expressive power. In fact, the S-application conditions allow for the specifi-
cation of first order logic (FOL) expressions for the source component and the S-extending ones
allow for FOL-expressions on the target component.

Example 2 All triple rules in Section 3 have S-consistent application conditions. For example,
the application condition ac7 of the rule newTransitionNewEvent in Figure 10 is an S-
application condition, thus no decomposition is necessary. Moreover, the application condition
ac11 of the rule newGuard in Figure 12 can be decomposed into the S-application condition
¬∃q11 ∧¬∃r11 and the S-extending application condition ¬∃p11.

For an S-consistent application condition, we obtain the application conditions of the source
and forward rules from the S- and S-extending parts of the application condition, respectively.

Definition 4 (Derived rules with application conditions) Given a triple rule tr = (tr : L→R,ac)
with S-consistent ac ∼= ac′S ∧ac

′
F we translate ac

′
S to an application condition acS = toS(ac

′
s) on

(LS ← ∅ → ∅) and ac′F to an application condition acF = toF(ac
′
F ) on (RS ← LC → LT ) using

the constructions below. This leads to the source rule (trS,acS) and the forward rule (trF ,acF ).
Given an S-application condition ac′S and an S-extending application condition ac

′
F over L, we

define toS(ac′S) and toF(ac
′
F ) by

LS ∅ ∅

PS ∅ ∅
LS LC LT

PS PC = LC PT = LT

toS(ac′S)

toS(ac′′S)

ac′S

ac′′S

sL tL

sP tP=tL

idLS

aS idLC idLT

aS

idPS

RS LC LT

RS PC PT
LS LC LT

PS = LS PC PT

toF(ac′F )

toF(ac′′F )

ac′F

ac′′F

trS◦sL tL

sL tL

trS◦sP
tP

sP tP

trS idLC idLT

idLS
aC

aT

idRS aC aT

trS idPC idPT

17 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

newGuardS

L11,S

1:S

2:T
∅ ∅

R11,S

1:S

2:T

G ∅ ∅

ac11,S =¬∃q11,S ∧¬∃r11,S

L11,S
1:S

2:T G
∅ ∅

L11,S
1:S 2:T

E

name="exit"

∅ ∅

∅ ∅

∅ ∅

tr11,S ∅ ∅

q11,S

r11,S

newGuardF

R11,S L11,C L11,T

1:S

2:T

3:G

S-P

T-T
T

R11,S R11,C R11,T

1:S

2:T

3:G

T

S-P

T-T

ac11,F =¬∃p11,F

L11,F
1:S 2:T

3:G
S-P T-T

tr11,S ◦sL11 tL11

sR11 tR11

idR11,S tr11,C tr11,T

p11,F

Figure 15: The source and forward rules of newGuard

• toS(true) = toF(true) = true,
• toS(∃(a,ac′′S)) =∃((aS,id∅,id∅),toS(ac

′′
S)),

• toF(∃(a,ac′′F )) =∃((idRS ,aC,aT ),toF(ac
′′
F )), and

• recursively for composed application conditions.

Example 3 In Figure 15, the source and forward rules newGuardS and newGuardF of the
rule newGuard in Figure 12 are shown. The S-application condition ¬∃p6 ∧¬∃r6 is translated
to the source rule, where the source graphs of the original application conditions are kept, but
the connection and target graphs are empty now. The S-extending application condition ¬∃q6 is
translated to the forward rule, where the source graph is adapted to the new left-hand side.

Similar to the corresponding result for triple rules without application conditions, in case of
S-consistency each triple rule is the E-concurrent rule of its source and forward rules.

Proposition 1 Given a triple rule tr = (tr : L → R,ac) with S-consistent ac, then tr = trS∗E trF
with E being the domain of the forward rule.

Proof idea. From [EEE+07] we know that this holds for triple rules without application condi-
tions. For the application conditions, this can be shown in two steps using the definition of the
application conditions and the shift properties (see [Gol11]).

For the first step, we have to show that Shift((idLS ,∅LC ,∅LT ),acS)∼= ac
′
S. With acS = toS(ac

′
S)

this is obviously true for ac′S = true. Consider ac
′
S = ∃(a,ac

′′
S) with a : L → P and suppose

Shift((idPS ,∅LS ,∅LC ),toS(ac
′′
S))
∼= ac′′S . It follows that Shift((idLS ,∅LC ,∅LT ),toS(∃(a,ac

′′
S)))
∼=

∃(a,Shift((idPS ,∅LS ,∅LT ),toS(ac
′′
S))
∼= ∃(a,ac′′S) = ac

′
S because the shift construction implies

that only the trivial squares have to be considered for the index set.
For the second step, we have to show that L(e2,Shift(idE,acF )) ∼= ac′F with e2 = (trS,idLC ,

idLT ) : L → E. With acF = toF(ac
′
F ) this is obvious for ac

′
F = true. Consider ac

′
F = ∃(a,ac

′′
F )

with L((LS ← PC → PT ) → (RS ← PC → PT ),Shift(id,toF(ac′′F ))) ∼= ac
′′
F . Then (PS = LS

sP←

GCM 2010 18 / 26



ECEASST

PC
tP→ PT ) is the pushout complement constructed for the left-shift-construction and we have that

L(e2,Shift(idE,toF(∃(a,ac′′F )))) ∼= L(e2,∃((idRS ,aC,aT ),toF(ac
′′
F )))

∼= ∃((idLS ,aC,aT ),
L(((LS ← PC → PT )→ (RS ← PC → PT )),toF(ac′′F ))∼=∃(a,ac

′′
F ) = ac

′
F . �

Now we want to analyze how a triple transformation can be decomposed into a transformation
applying first the source rules followed by the forward rules. Match consistency of the decom-
posed transformation means that the comatches of the source rules define the source part of the
matches of the forward rules. This helps us to define suitable forward model transformations,
which have to be source consistent to ensure a valid model. Note, that triple transformation
sequences always satisfy the application conditions of the corresponding rules.

Definition 5 (Source and match consistency) Given a sequence (tri)i=1,...,n of triple rules with
S-consistent application conditions leading to corresponding sequences (triS)i=1,...,n and

(triF )i=1,...,n of source and forward rules. A triple transformation sequence G00 =
tr∗S
=⇒ Gn0 =

tr∗F
=⇒ Gnn

via first tr1S,...,trnS and then tr1F ,...,trnF with matches miS and miF and comatches niS and niF ,
respectively, is match consistent if the source component of the match miF is uniquely defined
by the comatch niS.

A triple transformation Gn0 =
tr∗F
=⇒ Gnn is called source consistent if there is a match consistent

sequence G00 =
tr∗S
=⇒ Gn0 =

tr∗F
=⇒ Gnn.

We can split a transformation G0 =
tr1
=⇒ G1 ⇒ ... =

trn
=⇒ Gn into transformations G0 =

tr1S
=⇒ G′0 =

tr1F
==⇒

G1 ⇒ ... =
trnS
=⇒ G′n−1 =

trnF
==⇒ Gn. But to apply first the source and then the forward rules, these have

to be independent in a certain sense. In the following theorem, we show that such a decomposi-
tion into a match consistent transformation can be found and, vice versa, each match consistent
transformation can be composed to a transformation via the corresponding triple rules if the
application conditions are S-consistent. This result is an extension of the corresponding result
for triple transformations without application conditions [EEE+07] and with negative applica-
tion conditions [EHS09]. It is essential for concepts and results of model transformations with
application conditions below.

Theorem 1 (Decomposition and composition) For triple transformation sequences with S-
consistent application conditions the following holds:

1. Decomposition: For each triple transformation sequence G0 =
tr1
=⇒ G1 ⇒ ... =

trn
=⇒ Gn there

is a corresponding match consistent triple transformation sequence G0 = G00 =
tr1S
=⇒ G10 ⇒

... =
trnS
=⇒ Gn0 =

tr1F
==⇒ Gn1 ⇒ ... =

trnF
==⇒ Gnn = Gn.

2. Composition: For each match consistent triple transformation sequence G00 =
tr1S
=⇒ G10 ⇒

... =
trnS
=⇒ Gn0 =

tr1F
==⇒ Gn1 ⇒ ... =

trnF
==⇒ Gnn there is a triple transformation sequence G00 =

G0 =
tr1
=⇒ G1 ⇒ ... =

trn
=⇒ Gn = Gnn.

3. Bijective Correspondence: Composition and Decomposition are inverse to each other.

Proof idea. This result has been shown in [EEE+07] for triple rules without application con-
ditions. We use the facts that tri = triS ∗Ei triF , as shown in Prop. 1, and that the transforma-

19 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

tions via triS and tr jF are sequentially independent for i > j. This is shown in [EEE+07] for
rules without application conditions and can be extended to triple rules with application con-
ditions as shown in the following. Thus, the proof from [EEE+07] can be done analogously
for rules with application conditions. The main idea of the proof is that a triple transforma-
tion sequence G0 =

tr1
=⇒ G1 ⇒ ... =

trn
=⇒ Gn can be decomposed into a transformation sequence

G0 =
tr1S
=⇒ G′1 =

tr1F
==⇒ G1 ⇒ ... =

trnS
=⇒ G′n =

trnF
==⇒ Gn. The sequential independence of triS and tr jF

for i > j allows us to shift all source rules to the beginning and all forward rules to the end of
the sequence leading to an equivalent transformation sequence G0 = G00 =

tr1S
=⇒ G10 ⇒ ... =

trnS
=⇒

Gn0 =
tr1F
==⇒ Gn1 ⇒ ... =

trnF
==⇒ Gnn = Gn.

It suffices to show that the transformations G10 =
tr1F ,m1
====⇒ G11 =

tr2S,m2
===⇒ G21 are sequentially inde-

pendent. From the sequential independence without application conditions we obtain morphisms
i : R1F → G11 with i = n1 and j : L2S → G10 with g1 ◦ j = m2.

It remains to show the compatibility with the application conditions:

• j |= ac2S: ac2S = toS(ac′2S), where ac
′
2S is an S-application condition. For ac

′
2S = true,

also ac2S = true and therefore j |= ac2S. Suppose ac′2S = ∃(a,ac
′′
2S) leading to ac2S =

∃((aS,id∅,id∅),toS(ac′′2S)). Moreover, tr1F is a forward rule, i. e. it does not change the
source component and G11,S = G10,S.

L1F R1F

G10 G11

L2S R2S

G21

tr1F

g1

m1 i=n1
j

tr2S

g2

m2 n2

PS ∅ ∅

L2,S ∅ ∅

G10,S G10,C G10,T

G11,S = G10,S G11,C G11,T

toS(ac′′2S)

ac2S

sG10 tG10

sG11 tG11

aS

jS

id g1,C g1,T

pS

We know that m2 = g1 ◦ j |= ac2S, which means that there exists p : P → G11 with p◦
a = g1 ◦ j, p |= toS(ac′′2S), and pC = ∅, pT = ∅. Then there exists q : P → G10 with
q = (pS,∅,∅), q◦a = (pS◦aS,∅,∅) = j, and q |= toS(ac′′2S) because all objects occuring
in toS(ac′′2S) have empty connection and target components. This means that j |= ac2S for
this case, and can be shown recursively for composed ac2S.

• g2 ◦n1 |= acR := R(tr1F ,ac1F ): ac1F = toF(ac′1F ), where ac
′
1F is an S-extending appli-

cation condition. For ac′1F = true also ac1F = true and acR = true, therefore g2 ◦n1 |=
acR. Now suppose ac′1F = ∃(a,ac

′′
1F ) leading to ac1F = ∃((idR1,S ,aC,aT ),toF(ac

′′
1F )) and

acR = ∃((idR1S ,bC,bT ),ac
′
R) by component-wise pushout construction for the right-shift

with ac′R = R(u,toF(ac
′′
1F )). Moreover, tr2S is a source rule which means that g2,C and

g2,T are identities.

From the shift property of application conditions we know that n1 |= acR using that m1 |=
ac1F . This means that there is a morphism p : P → G11 with p◦a = n1, p |= ac′R, and
pS = n1,S. It follows that g2◦ p◦a = g2◦n1 and g2◦ p = (g2,S◦ pS, pC, pT ) |= ac′R, because
it only differs from p in the S-component, which is identical in all objects occuring in ac′R.

GCM 2010 20 / 26



ECEASST

This means that g2 ◦n1 |= acR = ∃(a,ac′R), and can be shown recursively for composed
acR.

R1,S L1,C L1,T

PS = R1,S PC PT
R1,S R1,C R1,T

P′C = R1,S P
′
C P

′
T

tr1,S◦sL tL

sP tP

id aC aT

sR tR

sP′ tP′

id bC bT

id tr1,C tr1,T

id uC uT

P′S = R1,S P
′
C P

′
T

R1,S R1,C R1,T

G11,S G11,C G11,T

G21,S G21,C = G11,C G21,T = G11,T

ac′R

acR

sP tP

sR tR

sG10 tG10

sG11 tG11

id bC bT

n1,S n1,C n1,T

g2,S id id

pS=n1,S pC pT

�

Based on source consistent forward transformations we define model transformations, where
we assume that the start graph is the empty graph.

Definition 6 (Model transformation) A (forward) model transformation sequence (GS,G0 =
tr∗F
=⇒

Gn,GT ) is given by a source graph GS, a target graph GT , and a source consistent forward

transformation G0 =
tr∗F
=⇒ Gn with G0 = (GS

∅←−∅ ∅−→∅) and Gn,T = GT .
A (forward) model transformation MTF : V LS VV LT is defined by all (forward) model trans-

formation sequences.

Definition 7 (Model transformation SC2PN) For our triple transformations, the triple rules are
given by the set T R ={start, newRegionSM, newRegionS, newStateSM, newStateS,
newFinalStateSM, newFinalStateS, newTransitionNewEvent, newTransi-
tionNewExit, newTransitionOldEvent, newTransitionOldExit, newGuard,
nextGuard, newAction, newTriggerElement} as introduced in Section 3.

The model transformation SC2PN from statecharts to Petri nets is defined by all forward model
transformations using the forward rules T RF .

The source rules represent a generating grammar for our statechart models. Moreover, the
restriction of all derived triple graphs to their source part, the language constructed by the source
rules, and the statechart language V LSC are equal.

Proposition 2 (Comparison of statechart languages) Consider the languages V LS = {GS | ∃
triple transformation ∅ =start===⇒=tr

∗
=⇒ (GS ← GC → GT ) via rules in T R}, V LS0 = {GS | ∃ triple

transformation ∅ =
startS
===⇒=

tr∗S
=⇒ (GS ← ∅ → ∅) via source rules in T RS}, and V LSC as defined

by the type graph and constraints. Then we have that V LS = V LS0 = V LSC.

Proof idea. V LS ⊆ V LS0: For a statechart GS ∈ V LS there is a transformation ∅ =
start
===⇒=tr

∗
=⇒

(GS ← GC → GT ) = Gn, which can be decomposed with Theorem 1 into a corresponding se-
quence ∅ =

startS
==⇒=

tr∗S
=⇒ (GS ←∅→∅) =

startF
===⇒=

tr∗F
=⇒ Gn. This means that GS ∈V LS0.

21 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

V LS0 ⊆V LSC: For a statechart GS ∈V LS0 there is a transformation ∅ =
startS
==⇒=

tr∗S
=⇒ (GS ←∅→

∅). GS is typed over the type graph T GS and respects all the specified constraints. This means
that GS ∈V LSC.

V LSC ⊆V LS: Given a statechart model M ∈V LSC we have to show that we find a transforma-
tion sequence ∅ =start===⇒=tr

∗
=⇒ G with GS = M. We can show this by arguing about the composition

of M and how to select the corresponding triple rule creating each element in M in the source
part. This means that M ∈V LS. �

Example 4 As explained for our example transformation in Section 3, applying the correspond-
ing source rule sequence to the empty start graph we obtain our statechart example. This state-
chart model can be transformed into the Petri net via the forward rules. This triple transformation
is source consistent, since the matches of the source parts for the forward rules are uniquely de-
fined by the comatches of the source rules. Thus, we actually obtain a model transformation
sequence from the statechart model in Figure 1 to the Petri net in Figure 13.

For all notions and results concerning source and forward rules, we obtain the dual notions
and results for target and backward rules. Thus, an application condition ac is T -consistent if it
can be decomposed into ac ∼= ac′T ∧ac

′
B, where ac

′
T is a T -application condition with identities

aS,aC and ac′B is a T -extending application condition with identity aT . This leads to target and
backward rules with application conditions and the dual composition and decomposition prop-
erties for triple transformation sequences with T -consistent application conditions. Moreover, a

backward model transformation sequence (GT ,G′0 =
tr∗B
=⇒ G′n,GS) is based on a target consistent

backward transformation G′0 =
tr∗B
=⇒ G′n with G′0 = (∅

∅←−∅ ∅−→ GT ) and G′n,S = GS.

4.1 Results for Model Transformations with Application Conditions

Based on Theorem 1 we can show correctness, completeness, backward information preserva-
tion, and termination of model transformations. The first result shows that transformations are
correct and complete regarding the source and target languages.

Theorem 2 (Correctness and completeness w.r.t. V LS, V LT ) Each model transformation se-
quence (GS,G0 =

tr∗F
=⇒ Gn,GT ) and (GT ,G′0 =

tr∗B
=⇒ G′n,GS) is correct with respect to the source and

target languages, i.e. GS ∈V LS and GT ∈V LT .
For each GS ∈ V LS there is a corresponding GT ∈ V LT such that there is a model transfor-

mation sequence (GS,G0 =
tr∗F
=⇒ Gn,GT ). Similarly, for each GT ∈ V LT there is a corresponding

GS ∈V LS such that there is a model transformation sequence (GT ,G′0 =
tr∗B
=⇒ G′n,GS).

Proof. If G0 =
tr∗F
=⇒ Gn is source consistent we have a match consistent sequence ∅ =

tr∗S
=⇒ G0 =

tr∗F
=⇒

Gn by Definition 5 . By composition in Theorem 1 there is a triple transformation ∅ =
tr∗
=⇒ Gn

with GS = Gn,S ∈V LS and GT ∈V LT .
For GS ∈ V LS there exists a triple transformation ∅ =

tr∗
=⇒ G, which can be decomposed by

Theorem 1 into a match consistent sequence ∅ =
tr∗S
=⇒ G0 = (GS

∅←− ∅ ∅−→ ∅) =
tr∗F
=⇒ G, and by

GCM 2010 22 / 26



ECEASST

definition (GS,G0 =
tr∗F
=⇒ G,GT ) is the required model transformation sequence with GT ∈V LT .

Dually, this holds for backward model transformation sequences.

Example 5 Since our example in Section 3 represents a well-defined model transformation
sequence, our statechart and Petri net are correct. Moreover, for each valid statechart model we
obtain a correct Petri net model, and vice versa. Note, that for the backward translation this
only holds for Petri nets which are correct w.r.t. our target language, and not the language of all
well-formed Petri nets.

A forward model transformation from GS to GT is backward information preserving concern-
ing the source component if there is a backward transformation sequence from GT leading to the
same source graph GS.

Definition 8 (Backward information preserving) A forward transformation sequence G =
tr∗F
=⇒ H

is backward information preserving if for the triple graph H′ = (∅ ∅←− ∅ ∅−→ HT ) there is a
backward transformation sequence H′ =

tr∗B
=⇒ G′ with G′S

∼
= GS.

This theorem is an extension of the corresponding result in [EEE+07] to triple transformations
with application conditions.

Theorem 3 (Backward information preservation) If all triple rules are S- and T -consistent, a
forward transformation G =

tr∗F
=⇒ H is backward information preserving if it is source consistent.

Proof. If G =
tr∗F
=⇒ H is a source consistent sequence then by Def. 5 there exists a match consistent

sequence ∅ =
tr∗S
=⇒ G =

tr∗F
=⇒ H leading to the triple transformation sequence ∅ =tr

∗
=⇒ H using Theo-

rem 1. From the decomposition, we also obtain a match consistent sequence ∅ =
tr∗T
=⇒ H′ =

tr∗B
=⇒ H

using the target and backward rules, with H′T = HT and H
′
C = H

′
S = ∅. Thus, G =

tr∗F
=⇒ H is back-

ward information preserving.

Example 6 The Petri net in Figure 13 can be transformed into the statechart in Figure 1 using
the backward rules of our model transformation in the same order as the forward rules were
used for the forward transformation. Indeed, this holds for each Petri net obtained of a model
transformation sequence from a valid statechart model.

If the source and target rules are creating, i.e. each rule actually creates at least one element,
forward and backward transformation sequences are terminating. This means that we do not find
infinite model transformation sequences.

Theorem 4 (Termination) Consider a source model GS ∈ V LS (target model GT ∈ V LT ) and
a set of triple rules such that GS (GT ) and all rule components are finite on the graph part and
the triple rules are creating on the source (target) component. Then each model transformation

sequence (GS,G0 =
tr∗F
=⇒ Gn,GT ) ((GT ,G′0 =

tr∗B
=⇒ G′n,GS)) is terminating, i.e. any extended sequence

G0 =
tr∗F
=⇒ Gn =

tr′+F
==⇒ Gm (G′0 =

tr∗B
=⇒ G′n =

tr′+B
==⇒ G′m) is not source (target) consistent.

23 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

Proof. Let G0 =
tr∗F
=⇒ Gn be a source consistent forward sequence such that ∅ =

tr∗S
=⇒ G0 =

tr∗F
=⇒ Gn

is match consistent, i.e. each comatch ni,S determines the source component of the match mi,F .
Thus, also each forward match mi,F determines the corresponding comatch ni,S. By uniqueness
of pushout complements along M -morphisms the comatch ni,S determines the match mi,S of the
source step, thus mi,F determines mi,S (∗).

If G0 =
tr∗F
=⇒ Gn =

tr(n+1,F),m(n+1,F)
=========⇒ Gn+1 =

tr′′∗F
==⇒ Gm is a source consistent forward sequence then

there is a corresponding source sequence ∅ =
tr∗S
=⇒ G′ =

trn+1,S
===⇒ G′′ =

tr′′∗S
==⇒ G0 leading to match con-

sistency of the complete sequence ∅ =⇒∗ Gm. Using (∗) it follows that G′ ∼= G0, which implies
that we have a transformation step G0 =

trn+1,S
===⇒ G′′ ⊆ G0, because triple rules are non-deleting.

This is a contradiction to the precondition that each rule is creating on the source component

implying that G′ 6∼= G0. Therefore, the forward transformation sequence G0 =
tr∗F
=⇒ Gn cannot be

extended and is terminating.
Dually, this can be shown for backward model transformation sequences.

Example 7 All triple rules in our example in Section 3 are finite on the graph part and source
creating. Thus, all model transformation sequences based on finite statechart models are termi-
nating. Note, that this does not hold for the backward direction, since the rule newAction is
not target creating. Thus, the corresponding backward rule can be applied infinitary often.

5 Conclusion

In this paper, we have extended the theory of model transformations based on TGGs to rules
with nested application conditions [HP09], which are known to be equivalent to first order logic
(FOL) on graphs. Using the slight restriction to S-consistent application conditions we have
shown that the main results known for model transformations are preserved. In fact, this is a
substantial extension of the existing theory, because S-consistent application conditions provide
the expressive power of FOL separately for the source and target components of triple graphs,
respectively. This enhances the expressiveness of model transformations including that of the
generation of source and/or target languages. We have discussed in detail a model transformation
from statecharts to Petri nets, where the use of application conditions allows to specify and
translate more general statecharts then those considered in [EEPT06]. There, an inplace model
transformation is used, which means that the model itself is changed in contrast to our approach,
where the original source model is kept and an additional target model is created. We have
presented main results for termination, correctness, completeness, and information preservation
extending those for the case with NACs in [EHS09] and without NACs in [EEE+07].

Our new results are based on the Local Church–Rosser, Parallelism, and Concurrency Theo-
rems with nested application conditions in [EHL10]. As future work it remains to extend also
the results concerning functional behaviour in [HEOG10] and [HEGO10] to the case of rules
with nested application conditions based on the “on-the-fly construction” in [EEHP09]. This
would allow to meet the “Grand Research Challenge of the TGG Community” in [SK08] for our
enhanced framework.

It is out of the scope of this paper to show that our model transformation from statecharts to

GCM 2010 24 / 26



ECEASST

Petri nets is semantically correct, where the semantics of the source and target language could
be based on a suitable operational semantics. For statecharts, an operational semantics based on
amalgamated graph transformation is presented in [GBEE11]. In [Gol11], also an operational
semantics for Petri nets using amalgamated graph transformation is defined and the model trans-
formation given in this paper is shown to be semantics-preserving. It is future work to obtain
general criteria for semantical correctness of model transformations.

Another future point of work is the construction of source and forward application conditions
for general, not necessarily s-consistent application conditions. Obviously, in this case a different
property for the compatibility of the source and forward solutions would be required to ensure
the corresponding decomposition and composition result.

Bibliography

[EEE+07] H. Ehrig, K. Ehrig, C. Ermel, F. Hermann, G. Taentzer. Information Preserving Bidi-
rectional Model Transformations. In Dwyer and Lopes (eds.), Proceedings of FASE
2007. LNCS 4422, pp. 72–86. Springer, 2007.

[EEH08] H. Ehrig, C. Ermel, F. Hermann. On the Relationship of Model Transformations
Based on Triple and Plain Graph Grammars. In Karsai and Taentzer (eds.), Pro-
ceedings of GraMoT 2008. Pp. 9–16. ACM, 2008.

[EEHP09] H. Ehrig, C. Ermel, F. Hermann, U. Prange. On-the-Fly Construction, Correctness
and Completeness of Model Transformations Based on Triple Graph Grammars. In
Schürr and Selic (eds.), Proceedings of MODELS 2009. LNCS 5795, pp. 241–255.
Springer, 2009.

[EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Trans-
formation. EATCS Monographs. Springer, 2006.

[EHL10] H. Ehrig, A. Habel, L. Lambers. Parallelism and Concurrency Theorems for Rules
with Nested Application Conditions. ECEASST 26:1–23, 2010.

[EHS09] H. Ehrig, F. Hermann, C. Sartorius. Completeness and Correctness of Model Trans-
formations based on Triple Graph Grammars with Negative Application Conditions.
ECEASST 18:1–18, 2009.

[GBEE11] U. Golas, E. Biermann, H. Ehrig, C. Ermel. A Visual Interpreter Semantics for Stat-
echarts Based on Amalgamated Graph Transformation. ECEASST 39:1–24, 2011.
This volume.

[GL06a] E. Guerra, J. de Lara. Attributed Typed Triple Graph Transformation with Inher-
itance in the Double Pushout Approach. Technical report UC3M-TR-CS-2006-00,
Universidad Carlos III, Madrid, Spain, 2006.

[GL06b] E. Guerra, J. de Lara. Model View Management with Triple Graph Grammars.
In Corradini et al. (eds.), Proceedings of ICGT 2006. LNCS 4178, pp. 351–366.
Springer, 2006.

25 / 26 Volume 39 (2011)



Triple Graph Grammars with Application Conditions

[Gol11] U. Golas. Analysis and Correctness of Algebraic Graph and Model Transformations.
PhD thesis, Technische Universität Berlin, Vieweg + Teubner, 2011.

[HEGO10] F. Hermann, H. Ehrig, U. Golas, F. Orejas. Efficient Analysis and Execution of
Correct and Complete Model Transformations Based on Triple Graph Grammars.
In Bézivin et al. (eds.), Proceedings of MDI 2010. Pp. 22–31. ACM, 2010.

[HEOG10] F. Hermann, H. Ehrig, F. Orejas, U. Golas. Formal Analysis of Functional Behaviour
for Model Transformations Based on Triple Graph Grammars. In Proceedings of
ICGT 2010. LNCS 6372, pp. 155–170. Springer, 2010.

[HP09] A. Habel, K.-H. Pennemann. Correctness of High-Level Transformation Systems
Relative to Nested Conditions. MSCS 19(2):245–296, 2009.

[KS06] A. König, A. Schürr. Tool Integration with Triple Graph Grammars - A Survey.
ENTCS 148(1):113–150, 2006.

[OMG09] OMG. Unified Modeling Language, Superstructure, Version 2.2. 2009.

[Pet80] C. Petri. Introduction to General Net Theory. In Brauer (ed.), Net Theory and Appli-
cations. LNCS 84, pp. 1–19. Springer, 1980.

[Sch94] A. Schürr. Specification of Graph Translators With Triple Graph Grammars. In Tin-
hofer (ed.), Proceedings of WG 1994. LNCS 903, pp. 151–163. Springer, 1994.

[SK08] A. Schürr, F. Klar. 15 Years of Triple Graph Grammars. In Ehrig et al. (eds.), Pro-
ceedings of ICGT 2008. LNCS, pp. 411–425. Springer, 2008.

[TEG+05] G. Taentzer, K. Ehrig, E. Guerra, J. Lara, L. Lengyel, T. Levendovsky,
U. Prange, D. Varró, S. Varró-Gyapay. Model Transformation by Graph
Transformation: A Comparative Study. In Proceedings of MTP 2005. 2005.
http://sosym.dcs.kcl.ac.uk/events/mtip05/submissions/.

GCM 2010 26 / 26


	Introduction
	Review of Triple Graph Grammars and Application Conditions
	Model Transformation from Statecharts to Petri Nets
	Model Transformations with Application Conditions
	Results for Model Transformations with Application Conditions

	Conclusion