Fig.1. A model of a simple protocol with timeout.
Reachability analysis is based on exhaustive analysis of the state space. Usually, the state space of the net model is first generated, and then the required properties are verified by checking the reachable states in some systematic way.
For M-timed nets, the definition of a state must take into account the distribution of (remaining) tokens in places of the net and also the numbers of active firings for each transition; a state s can thus be defined as a pair of functions, s = (m,n), m : P -> {0,1,...}, n : T -> {0,1,...}. Since, in timed nets, all transitions which can initiate their firing, start their firings in the same instant of time in which they become enabled, for each state s = (m,n), the set of transitions enabled by m, the `remaining marking', is empty. Changes of states are thus occurring when a transition terminates its firing. In M-timed nets, firing times of transitions are random variables (with negative exponential distributions), so it is assumed that only one transition terminates its firing at a time. The tokens are then deposited to transition's output places, new transitions can become enabled and new firings initiated. The probability of transition from one state to another depends on the choice of new firings as well as the probability of termination of firing by a specific transition.
For D-timed nets, state definitions are slightly different than for M-timed nets because the `memoryless property' of M--timed nets does not hold for D-timed nets. For D-timed nets, the state descriptions must take into account the `history' of firings. This can be done by including an additional component in state descriptions, the remaining firing time function, which, for each active firing, specifies the remaining part of the firing time at the time instant when the state begins (details are given in [Zu91]). Also, the state transition probabilities are determined slightly differently because the several firings can terminate simultaneously, and there is no randomness in selection of terminating firings. Otherwise, the generation of the state space is quite similar for both classes of nets.
In TPN-tools, all reachable states are systematically generated from a set of initial states of a timed net, and a state graph is created which contains the states, the direct reachability relation represented by directed arcs between states, and transition probabilities associated with these arcs. Since such a state graph is the continuous-time Markov chain representing the behavior of the net, stationary probabilities of states can be obtained by solving the set linear flow equations.
The generation of the state graph and then the solution of stationary probabilities of states is performed by the following two commands:
sgraph; statprob;
Example. The set of reachable states si and stationary probabilities of states x(si) for the net shown in Fig.1 are as follows:
| si | x(si) | mi | ni | sj | q(si,sj) |
| 1 2 3 4 5 6 7 | 1 2 3 4 5 6 7 8 | ||||
| 1 | 0.00000 | 0 0 0 0 0 0 0 | 1 0 0 0 0 0 0 0 | 2 | 1.0 |
| 2 | 0.04762 | 0 0 0 0 0 0 0 | 0 1 0 0 0 1 0 0 | 3 | 0.1 |
| 4 | 0.9 | ||||
| 3 | 0.00000 | 0 0 0 0 0 0 0 | 0 0 1 0 0 1 0 0 | 5 | 1.0 |
| 4 | 0.00000 | 0 0 0 0 0 0 0 | 0 0 0 1 0 1 0 0 | 6 | 1.0 |
| 5 | 0.09524 | 0 0 0 0 0 0 0 | 0 0 0 0 0 1 0 0 | 7 | 1.0 |
| 6 | 0.42857 | 0 0 0 0 0 0 0 | 0 0 0 0 1 1 0 0 | 8 | 1.0 |
| 7 | 0.42857 | 0 0 0 0 0 0 0 | 0 0 0 0 0 0 1 0 | 1 | 1.0 |
| 8 | 0.00000 | 0 0 0 0 0 0 1 | 1 0 0 0 0 1 0 0 | 9 | 1.0 |
| 9 | 0.42857 | 0 0 0 0 0 0 1 | 0 1 0 0 0 2 0 0 | 10 | 0.1 |
| 11 | 0.9 | ||||
| 10 | 0.00000 | 0 0 0 0 0 0 0 | 0 0 1 0 0 1 0 1 | 5 | 1.0 |
| 11 | 0.00000 | 0 0 0 0 0 0 0 | 0 0 0 1 0 1 0 1 | 6 | 1.0 |
Fig.1. A model of a simple protocol with timeout.
It can be observed that all the states with the stationary probabilities equal to zero can be removed as they do not affect the performance of the model. In TPN-tools this can be obtained by using the `enhanced mode' [Zu91]:
mode=H; sgraph; statprob;
Enhanced mode eliminates all vanishing states (i.e., states with zero holding time) during the generation of the state graph, so the equivalent `enhanced' state table is (all immediate transitions, t1, t3, t4, t7 and t8 are eliminated as they do not contribute to the timed behavior of the net; all places which do not participate in timed description could also be removed from state descriptions; e.g., p1, p2, p3, etc.):
| si | x(si) | mi | ni | sj | q(si,sj) |
| 1 2 3 4 5 6 7 | 2 5 6 | ||||
| 1 | 0.04762 | 0 0 0 0 0 0 0 | 1 0 1 | 2 | 0.9 |
| 3 | 0.1 | ||||
| 2 | 0.42857 | 0 0 0 0 0 0 0 | 0 1 1 | 4 | 1.0 |
| 3 | 0.09524 | 0 0 0 0 0 0 0 | 0 0 1 | 1 | 1.0 |
| 4 | 0.42857 | 0 0 0 0 0 0 1 | 1 0 2 | 2 | 0.9 |
| 3 | 0.1 |
The performance characteristics can be derived from the stationary probabilities of states and the detailed definitions of states. For example, since the receipt of an acknowledgement indicates a successfully transmitted message, the throughput of acknowledgments (transition t5) can be used as the throughput of the protocol. The throughput of t5 is equal to the utilization of t5 (i.e., the probability that t5 is firing) multiplied by the service rate (i.e., the firing rate) of t5. The probability that t5 is firing is equal to the sum of stationary probabilities of all those states si in which fi(t5) is positive; for this example, it is s6 only. The throughput of t5 is thus equal to 0.42857/5.0=0.08571 messages per time unit.
A simple `postprocessing' interpreter has been implemented in TPN-tools which performs evaluations based on the analysis of the state graph. The interpreter is invoked by the command eval with an expression as its argument:
<command> ::= eval ( <expr> )
<expr> ::= <term> | <expr> + <term> | <expr> - <term>
<term> ::= <fact> | <term> * <fact> | <term> / <fact>
<fact> ::= ( <expr> ) | <number> | <tori> | [ <cond> ]
<tori> ::= <t_spec> | <i_spec>
<t_spec> ::= t ( <t_id> <occur> )
<t_id> ::= <number> | <name>
<occur> ::= . <name> | <empty>
<i_spec> ::= i ( <p_id> <color> )
<p_id> ::= <number> | <name>
<color> : <name> | <empty>
<cond> ::= <lsum> | <cond> `|' <lsum>
<lsum> ::= <atom> | <lsum> & <atom>
<atom> ::= ( <cond> ) | <morf> <rel> <val>
<morf> ::= <m_spec> | <f_spec>
<m_spec> ::= m ( <p_id> <color> )
<f_spec> ::= f ( <t_id> <occur> )
<val> ::= <number>
Example. The throughput of t5, as discussed earlier, can be evaluated by the following command (for enhanced as well as standard modes):
eval([f(5)=1]/t(5));
where [f(5)=1] denotes a search of the state space that returns the sum of stationary probabilities of all those states for which the firing function of transition t5, f(t5), is equal to 1, while t(5) denotes the firing time of transition t5.
Fig.3. A colored net model of `dining philosophers'.
The state space of the M-timed net shown in Fig.3 contains 61 states; because of symmetry of the model, the throughputs of all 5 occurrences of transition eat (in terms of the number of bowls of spaghetti consumed by each philosopher per one hour) are expected to be equal:
sgraph;
statprob;
eval([f(eat.A)=1]/t(eat));
value : 0.12281
eval([f(eat.B)=1]/t(eat));
value : 0.12281
eval([f(eat.C)=1]/t(eat));
value : 0.12281
eval([f(eat.D)=1]/t(eat));
value : 0.12281
eval([f(eat.E)=1]/t(eat));
value : 0.12281