Fig.1. A model of a simple protocol with timeout (inhibitor arc).
In TPN-tools, net descriptions are `transition oriented', i.e., nets are specified as collections of transitions, and each transition contains all parameters associated with it.
The syntax of model descriptions, in the BNF notation, is as follows:
<model-descr> ::= <color-list> <net-class> <net-descr> <imarking>
<color-list> ::= <colors> | <empty>
<net-class> ::= <class> | <empty>
<net-descr> ::= <net-header> ( <transitions> )
<net-header> ::= Mnet | Dnet | net
<transitions> ::= <transition> | <transitions> ; <transition>
<transition> ::= <t-header> = <input-output-list>
| <t-header> <occurrence-list>
<t-header> ::= <t-indent> <type> <time> <prob>
<occurrence-list> ::= <occurrence> | <occurrence-list> , <occurrence>
<occurrence> ::= { <o-header> = <input-output-list> }
<o-header> ::= <o-name> <type> <time> <prob>
<t-ident> ::= # <integer> | # <name>
<o-name> ::= <name> | <empty>
<type> ::= :D | :M | :X | <empty>
<time> ::= * <rational> | <empty>
<prob> ::= , <rational> | , <integer> / <integer> | , <ref> | <empty>
<rational> ::= <integer> | <integer> . <integer>
<ref> ::= [ <place-id> ] | [ <place-id> : <color> ]
<input-output-list> ::= <input-list> | <input-list> / <output-list>
<input-list> ::= <arc> | <input-list> , <arc>
<output-list> ::= <arc> | <output-list> , <arc>
<arc> ::= <place-id> | <place-id> : <weight> <color>
<place-id> ::= <integer> | <name>
<weight> ::= <integer>
<color> ::= <name> | <empty>
<name> ::= <letter> | <name> <letter> | <name> <digit> | <name> _
The type of the net can be indicated in the net header or in the {\tt class} directive:
<class> ::= class = D ; | class = M ;
The type of a transition or an occurrence (M-timed, D-timed) can also
be indicated by the type elements; such a specification overrides the
net type. The specification X indicates the type opposite to the one
indicated for the net.
For occurrences without type time or prob elements,
the values of type, time and prob specified for the
transition are used. Transitions and occurrences with empty time
elements denote immediate transitions and occurrences, i.e., transitions and
occurrences with time equal to 0.
Probability element prob specifies the free-choice probabilities of
occurrences or relative frequencies of conflicting occurrences.
Empty element prob is equivalent to probability equal to 1.
The form <integer>/<integer> is provided as a convenient way
of specifying fractional values.
Marking--dependent relative frequencies are indicated by place/color references
ref of the prob element. During conflict resolution, the
number of (colored) tokens in the place indicated by ref is used as
the relative frequency of transition/occurrence firings. Usually ref
is one of the transition/occurrence's input places.
Arcs without weight are equivalent to arcs with weight equal to 1.
Inhibitor arcs are specified as arcs with weight equal to 0.
All colors used in net descriptions must be declared in the list of colors.
This list must precede the net description:
<colors> ::= color ( <color-list> ) ;
<color-list> ::= <color> | <color-list> , <color>
<color> ::= <name>
The initial marking function is specified as a list of marked places:
<imarking> ::= mark ( <marking-list> ) ;
<marking-list> ::= <marked-place> | <marking-list> , <marked-place>
<marked-place> ::= <place> | <place> : <count> <color>
<count> ::= <integer>
<color> ::= <name> | <empty>
Marked places without the count element are equivalent to places with
the value of count equal to 1.
Example 1. A Petri net model of a simple protocol with a timeout mechanism is shown in Fig.1.
Fig.1. A model of a simple protocol with timeout (inhibitor arc).
A token in p1 represents a message to be sent from a `sender' (p1) to a `receiver' (p3) and confirmed by an acknowledgement sent back to the sender. The message is sent by firing t1, after which a single token is deposited in p2 (the message) and in p5 (the timeout). Enabled t2 and t6 can start their firings concurrently; firing time of t2 represents the `communication delay' of sending a message, and that of t6 the timeout time. When the firing of t2 is finished, a token is deposited in p3, the receiver. p3 is a free-choice place, so t3 and t4 are enabled simultaneously, but only one of them can fire; the random choice is characterized by `choice probabilities' assigned to t3 and t4. t3 represents (in a simplified way) the loss or distortion of the message or its acknowledgement; if t3 is selected for firing (according to its free-choice probability), the token is removed from p3 as well as from the model (t3 is a `token sink'). In such a case the timeout transition t6 finishes its firing with no token in p7, so the inhibitor arc p7,t7) enables t7, and its firing regenerates the lost token in p1, so the message can be `retransmitted'. If the message is received correctly, t4 is selected for firing rather than t3, and after another `communication delay' (modeled by t5) tokens are deposited in p7 and p1 (so another message can be sent to the receiver). The token in p7 waits until the timeout transition t6 finishes its firing, and then removes the timeout token by firing t8 (t7 is disabled in this case by the inhibitor arc).
The transition t4 may seem redundant in this model but in fact it is required due to the restriction that all free-choice classes of transitions must be uniform, i.e., each free-choice class must contain either immediate or timed transitions, but not both.
All immediate transitions (i.e., transitions with zero firing time) are represented by (thin) bars, while timed transitions are represented by (black) rectangles. The firing times of timed transitions are selected in such a way that the timeout time (t6 is greater than the sum of the delays of sending a message (t2 and an acknowledgement (t5). In the following description, the immediate transitions are indicated by the default zero firing times:
Dnet(#t1=p1/p2,p5;
#t2*5=p2/p3;
#t3,1/10=p3;
#t4,9/10=p3/p4;
#t5*5=p4/p1,p7;
#t6*15=p5/p6;
#t7=p6,p7:0/p1;
#t8=p6,p7)
mark(p1);
Fig.2 shows a sightly different model of the same simple protocol, with an interrupt arc to discontinue (and cancel) the timeout if the message and the acknowledgement are transmitted correctly. If the message or acknowledgement are lost or distorted, the timeout transition will finish its firing and regenerate the token in p1. If the transmissions are correct, a token deposited in p6 interrupts the firing of t6, so the `timeout token' is returned to p5, and immediately removed (together with a token in p6) by firing t7.
Fig.2. A model of a simple protocol with timeout (interrupt arc).
The description of this model is as follows:
Dnet(#t1=p1/p2,p5;
#t2*5=p2/p3;
#t3,1/10=p3;
#t4,9/10=p3/p4;
#t5*5=p4/p1,p6;
#t6*15=p5,p6-/p1;
#t7=p5,p6)
mark(p1);
Example 2. A colored Petri net model of `five dining philosophers' is shown in Fig.3. The philosophers are represented by token colors A, B, C, D and E, while forks by colors m, n, o, p and q.
Fig.3. A colored net model of `dining philosophers'.
The net shown in Fig.3 outlines a model of a single philosopher, so the use of colored tokens is essential for this model. The use of colors and the conflicts created by sharing forks can be described by the following `connectivity matrix', in which rows correspond to token colors assigned to places, and columns -- to transition occurrences; the elements ``+1'' represent arcs from transition occurrences to places while elements ``-1'' arcs from places to transition occurrences (the values of the elements are the weights assigned to arcs, in this case they are equal to 1). The elements of the matrix are sets rather than expressions, so the `loops' (e.g. place p3 and transition eat in Fig.3) can also be represented:
| think | eat | ||||||||||
| A | B | C | D | E | A | B | C | D | E | ||
| p1 | A | +1 | -1 | ||||||||
| B | +1 | -1 | |||||||||
| C | +1 | -1 | |||||||||
| D | +1 | -1 | |||||||||
| E | +1 | -1 | |||||||||
| p2 | A | -1 | +1 | ||||||||
| B | -1 | +1 | |||||||||
| C | -1 | +1 | |||||||||
| D | -1 | +1 | |||||||||
| E | -1 | +1 | |||||||||
| p3 | m | -1,+1 | -1,+1 | ||||||||
| n | -1,+1 | -1,+1 | |||||||||
| o | -1,+1 | -1,+1 | |||||||||
| p | -1,+1 | -1,+1 | |||||||||
| q | -1,+1 | -1,+1 | |||||||||
For example, the last column describes the occurrence E of transition eat The occurrence is enabled (elements ``-1'') by a single token of color E in place p1 (philosopher E), one token of color p and one of color q in place p3 (E's `right' and `left' forks). Firing this occurrence removes these tokens from p1 and p3 and when the eating is finished (eating time corresponds to the firing time of this occurrence), one token of color E is deposited in p2 (philosopher E is going to think), and single tokens of color p and q are returned to p3 (the two forks are returned). It should be observed that the name of the occurrence, E, is quite irrelevant, and could be any other name as well. The following model description is a rather straightforward transcription of this connectivity matrix (column by column); it is assumed that the thinking times as well as eating times of all philosophers are exponentially distributed (M-timed model) with the average values equal to 5 and 2, respectively:
color(A,B,C,D,E,m,n,o,p,q);
Mnet(#think*5{A=p2:1A/p1:1A},
{B=p2:1B/p1:1B},
{C=p2:1C/p1:1C},
{D=p2:1D/p1:1D},
{E=p2:1E/p1:1E};
#eat*2{A,1=p1:1A,p3:1q,p3:1m/p2:1A,p3:1q,p3:1m},
{B,1=p1:1B,p3:1n,p3:1m/p2:1B,p3:1n,p3:1m},
{C,1=p1:1C,p3:1n,p3:1o/p2:1C,p3:1n,p3:1o},
{D,1=p1:1D,p3:1o,p3:1p/p2:1D,p3:1o,p3:1p},
{E,1=p1:1E,p3:1q,p3:1p/p2:1E,p3:1q,p3:1p})
mark(p1:1A,p1:1B,p1:1C,p2:1D,p2:1E,p3:1m,p3:1n,p3:1o,p3:1p,p3:1q);
Another version of net descriptions, proposed in Petri Net Newsletter [BVV88], is also supported by TPN-tools (but only for non-colored nets [Zu96a]).