RTCP-nets modelling in CPN Tools

This chapter covers RTCP-nets modelling in CPN Tools environment. This approach to the modelling of RTCP-nets was originally introduced in master's thesis of Joanna Woźniak entitled 'Modelowanie RTCP-sieci z wykorzystaniem środowiska CPN-Tools' in 2014. With her permission, excerpts of her work here will be used to explain the principles of RTCP-nets modelling in the CPN Tools application.


Introduction

CPN Tools is a popular application for editing, analysis and simulation of the coloured Petri nets - RTCP-nets edition is not supported. The presented approach consists in placing additional information in the model. The modified nets are considered to be incorrect by CPN Tools validation tool, but information about them is stored in an XML file. This file can be used as an input for cpn2rtcpn tool which can convert it to standard RTCP-net file format accepted by the RTCPNC compiler.


Declarations

Net model may include, among others, declarations of colour sets, variables and constants. They are located in the Declarations section of the program menu.

Constants

Constants are declared using the val keyword: val id = exp, where: id - the identifier exp - the expression of any type, determining the value assigned to the identifier.

Below are a few examples of constant declarations (operator '^' denotes concatenation):

val NUMBER1 = 1;
val WORD = "a" ^ "b" ^ "c";

Colour sets

Three types of colour sets are distinguished : simple, compound - using previously declared colour sets and timed (unused in the RTCP-networks). Simple types include, for example, types: Boolean, Integer, Real, Time, String, Enumerated and Index. The compound types include Product, Record, List, Union, Subset, and Alias. For type declarations colset keyword is used. Below are examples of colour sets declarations.

colset i = Integer;
colset ab = with a | b;
colset abc = product ab * ab;

Variables

Variables are basically identifiers which values can be changed during the firing of net transitions. Variables can be used in expressions assigned to model elements. Their scope is local to the transition. Variables are declared using the var keyword:

var ID_1, ID_2, …, id_n: cs_name;

where cs_name is the name of the declared type, for example:

var x1, x2: abc;


Expressions

Expressions are assigned to net elements such as places, transitions, arcs and guards. RTCP-net description uses many notations from the coloured Petri nets, though, due to some simplifications and changes in the structure of the RTCP-net, modifications of used notation were introduced.

Places

RTCP-net places can have parameters such as:

  • Name,
  • Type,
  • The initial marking,
  • The value of the local clock,
  • The fusion name,
  • The type of port.

Marking of an RTCP-net has adopted the following format: , where i is an amount and c is the value (colour) of the token. Tokens are of different values are concatenated using the '+' operator. eg. the expression 2 (a) + (b) denotes that 2 tokens of value a and one token of value b. An example of a RTCP-net created in the CPN Tools is presented in the figure below.

The net contains places: A, B, C and D. Places A and B do have an initial marking. Since the initial marking of places C and D is omitted, they both start with empty sets of tokens. Place A is of type ab and has two tokens of value a while place B is of type abc and has four tags: (a, a), (b, b), (a, b) and (b, a). Places of this net do not have time stamp values explicitly assigned - their default value is 0.

The value of the local clock is not supported by the CPN-Tools. Its value is placed on the model in the following notation:

(marking)@local_clock_value.

The figure below shows the net on which to A place time value (1) has been added. The initial marking of place A changes from 2(a) to 2(a)@1.

An example of a fusion is shown in the figure below. It's the fusion of places B and C. They are of the same type and have equivalent initialization functions.

In the next example hierarchical net consisting of two pages is considered. The transition T is a substitution transition, and the page containing it is a superpage.

In figure below is a subpage.

Socket A of the superpage corresponds to the port A of the subpage, and socket B corresponds to port B. These two couples have the same types and the equivalent initial marking.

Transitions

RTCP-net transitions are described by the following parameters:

  • Name,
  • Priority,
  • Guard,
  • An indication of the hierarchy.

The RTCP-nets, in cotrast to the colored nets, time is not associated with transitions. In the model presented in the figure below, there are two transitions: T1 and T2 with priority values 2 and 1 respectively. Two guards were also defined: x = a for transitions T1 and x = b for the transition T2.

Arcs

Arcs in the RTCP-nets may be unidirectional or bidirectional (equivalent of a pair of arcs). In the second case two expressions are assocaited with the arc: the input expression defining tokens added to the place and the output expression specifying tokens removed from it. These expressions can optionally contain time expressions. Therefore, to the arc can be assigned following parameters:

  • Input expression,
  • Output expression,
  • Time input expression,
  • Time output expression.

CPN Tools allows users to associate only one expression. To assign to two expressions to one arc the following format of the label was invented:

in_exp @ time_in_exp | out_exp @ time_out_exp

Parts time_in_exp and time_out_exp can be omitted.

In the figure below the arc connected to place A has value b assigned. It means that b token is added to this place after firing of transition T. Variable x represents the token removed from place A. The output expression has time value assigned and equal to 2. It denotes that the transition can be fired after 2 time units. The arc connecting the transition with place B contains expressions determining a token added to place B (the value of x variable) and the value of the local clock of place B (it will be set to 1).

Go back