VIATRA2/Activity Diagrams to Petri Nets
- 1 Aim
- 2 How to obtain
- 3 Background
- 4 Transformation design: mapping Activities into Petri Nets
- 5 Formalization using GT rules
- 6 Exercise: decision and merge
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
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 (also called executable nodes), denoted by smaller rounded blocks; each represent some action that is performed for some time during this process. We will only be interested in the most common kind of activity edges: control flow edges 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.
In the core subset of the formalism, a PN is a directed bipartite graph. One partition of nodes are called places, 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, and will be called arcs to distinguish from UML Activity Edges.
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 enabled or fireable in a state if each of its incoming arcs come from marked places (i.e. containing at least one token). A state change of the Petri Net is the firing of an enabled transition; this consists of removing a token from each incoming place, and adding a token to each place at the end of outgoing arcs from the transition.
Transformation design: mapping Activities into Petri Nets
Action and control flow
We interpret UML Activity semantics in a way such that executing and action is not instantaneous, but can last for some time. Also, there is no obligation for an action to start as soon as the previous one in the sequence is finished, some time can pass in-between. Thus for each Action, the resulting Petri Net should have one or more states where the action is being executed. Likewise for each control flow edge, there should be PN states where the edge is active, i.e. execution has passed the action (or control node) at the source of the control flow edge, but has not yet reached the Activity Node at the target of the edge.
This goal can be achieved by creating a Petri place for each action and each control flow in the Activity model. In the marking belonging to a state of the Petri net, a token in the place corresponding to an action means that an instance of the process is currently executing the action. Similarly, a token in the place corresponding to a control flow means that the activity edge is currently active.
Obviously, we also need transitions, otherwise the Petri Net would be static. For each control flow incoming in an action, a transition should be created to represent the start of execution of the action. This transition has an incoming arc from the place representing the control flow, and an outgoing arc to the place representing the action. Thus the transition is enabled if the activity edge is active, and firing it will start the execution of the action and cease the activation of the edge. Similarly, a transition should represent the termination of the action, with an incoming arc from the place of the action, and an outgoing arc to the place of the edge.
This argument suggests the following principle for the transformation. Each control flow edge will be mapped into a place representing when the edge is active. Each action should be mapped into two transitions and a place in-between, with two arcs linking the three Petri nodes. The first transition represents entering the action, the place (more precisely, a token in the place) represents that the state is during the execution of the action, and the second transition represents exiting the action. Then the entering transition of the action should be linked by an incoming arc to the place representing the incoming activity edge, and the exiting transition should be linked by an outgoing arc to the place representing the outgoing activity edge.
Initial and flow final nodes
When execution reaches a flow final node in the Activity, the instance of the process terminates. More precisely, if there are several threads of execution (due to a fork node), the one that reaches the flow final node terminates, while others are unaffected (this is the difference between the flow final node and a different type of terminating node). In Petri Net terminology, the token representing the activation of the incoming control flow edge should be consumed by the flow final node, without putting a token in any place representing an activity edge or action. This is achieved by a transition that has an incoming arc from the place corresponding to the control flow edge pointing to the flow final node, and no outgoing arcs.
There are at least two ways to interpret an initial node. One possibility is that the node can activate the outgoing control flow edge exactly once, thereby starting the process. In some contexts, however, it makes more sense to assume that the initial node can activate the control flow an arbitrary number of times, launching multiple process instances that are executed concurrently. Both can be easily represented by Petri Nets. In both cases, the initial node is mapped into a transition, with an outgoing arc to the place corresponding to the outgoing control flow edge. We opted to choose the first interpretation; a place marked initially with one token (the only marked place in the initial state) is created and connected by an arc to the transition corresponding to the initial node. This marked place ascertains that the transition can fire only once, as the token will be removed upon the firing, rendering the transition disabled from that time on. The other interpretation can be achieved by simply omitting this place and the arc; in this case the transition would be able to fire any time, an arbitrary number of times.
Fork and join
Formalization using GT rules
Exercise: decision and merge