# VIATRA2/Activity Diagrams to Petri Nets

## Contents

## Aim

This tutorial example presents a transformation from a core subset of UML2 Activities to the domain of Petri-Nets (also known as Place/Transition Nets). This simple transformation imitates a set of complex, real-world model transformations that map high-level engineering models such as BPEL into semantical domains (i.e. mathematical formalisms) such as transition systems, for formal verification and analysis by tools such as SAL.

The example is meant to be the first one to read after completing the Hello World tutorial. As an important point, the tutorial includes an exercise for readers, to help them learn transformation development.

## How to obtain

TODO

## Background

### VIATRA2

The tutorial assumes that the readers have already familiarized themselves with the basic features of the user interface of VIATRA2, the notion of model transformation and the basic concepts of the formalism GTASM. The Getting Started block is recommended reading before starting this tutorial. In particular, the Using Transformations page introduces how to load and use this transformation.

### Source domain: UML Activities

UML Activities form a standard workflow description language, with countless modeling tools and diagram editors available. This tutorial will use the core elements of UML Activity modeling.

An **Activity** is the model of the process, represented in an **Activity Diagram** (AD) by a large box containing nodes and edges. An activity consists of several **Action** nodes, denoted by smaller rounded blocks; each represent some action that is performed for some time during this process. The only kind of action node we are interested in is the **opaque action** which is modeled like a black box, without special features (e.g. message receiving) or internal structure. Visual edges labeled **control flow** connect actions to define their sequence of execution. This sequence starts at the **initial** node, and terminates at the **flow final** node. These two are not actual actions, but special control nodes.

Further control nodes include the **decision** node, that represents a branching into two or more possible paths of execution according to some criterion (the criterion itself is not represented in our subset of UML Activities). These alternative paths meet at control nodes called **merge** nodes, from which point they proceed with the same sequence. A similar pair of control nodes is **fork** and **join**, which denote respectively a point where the execution is split into several concurrent threads, and a point where these threads of events catch up with each other to proceed as a single sequence.

### Target domain: Petri Nets

Petri Nets (PN) are a mathematical formalism for specifying the behaviour of discrete systems. This formalism excels at modeling concurrency and synchronization, resource constraints and loosely dependent subsystems. There are efficient analysis (model checking) tools for Petri Nets, capable of e.g. finding deadlocks, deciding the reachability of states with given properties, proving the conservation of resources or the cyclic nature of a sequence of events.

A PN is a directed bipartite graph. One partition of nodes are called **place**s, and represented by circles in diagrams. The other type of nodes is the **transition**, commonly represented by an elongated rectangle. Edges can flow either from a transition to a place, or from a place to a transition.

A state of the PN is defined by a **marking**, which assigns a natural number (0, 1, or more) to each place. This number is visualized as the number of **tokens** contained in the place, indicated by small dots in the circle. The marking of the initial state is an important part of the definition of the Petri Net.

A transition is said to be **fireable** in a state if each of the its incoming edges come from **marked** places (i.e. containing at least one token). A state change of the Petri Net is the **firing** of a fireable transition; this consists of removing a token form each incoming place, and adding a token to each place at the end of outgoing edges from the transition.

## Mapping Activities into Petri Nets

TODO

## Formalization using GT rules

TODO

## Exercise

TODO