# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 4 Experimental Results
### Fischer's Mutual Exclusion Protocol
\begin{table}
\begin{tabular}{c c c c c c c c c} \hline \hline \multirow{2}{*}{**Tool**} & \multicolumn{3}{c}{**Options and Parameters**} & \multicolumn{6}{c}{**Formal Verification Results**} \\ \cline{2-9}  & **deltaC** & **N** & **Option** & **States** & **Transitions** & **State-Vector [B]** & **Memory [MB]** & **Time [s]** \\ \hline \multirow{8}{*}{**DT Spin 4.1.1** **(DT Promela)**} & \multirow{4}{*}{2} & 2 & POR & 212 & 275 & 36 & 1.253 & 0.000 \\ \cline{3-9}  & & 3 & POR & 1880 & 2579 & 44 & 1.253 & 0.004 \\ \cline{3-9}  & & 4 & POR & 15,502 & 23,141 &


```
1#include^dtime.h^/*timedfeatures*/
2
3#defineACK1
4#definedX3
5#definedL3
6#defined81
7#defineTo8
8#defineMAX8 /*msnumberofdifferentmessages*/
9
10 chanSt0R=[1]ofbyte,bit)/*channels*/
11 channRt0S=[1]of{bit}
12
13 proctypeSender(chanin,out)
14{
15 cinercs;
16 bytemt;/*messagedata*/
17 bits=0;/*sequencenumber*/
18
19R_h:udelay(sc);/*mboundedstartdelay*/
20 mt=(mt+1){MAX;/*inputfromtheupperlayer*/
21
22s_f:delay(sc,dK);
23 outt,sn;/*sendanddelayinchannelSt0*/
24 act(sc,To-dK);
25
26W_n:do
27::in?-.->
28 if
29:atomic(skip;delay(sc,1);
30 sn=1-sn;gotR_h;);/*ackisOK*/
31::atomic(printf(*MSC;AC&err\
^);
32 gotoS_f);
33 if;
34::expire(sc)->gotS_f;/*timecout*/
35 od;
36}
37
38 proctypeReceiver(chanin,out)
39{
40 timerc;
41 showbytemr;/*receivedmessage*/
42 showbytem=1;/*expectedmessage*/
43 bitrm,es=0;/*receivedandexpectedsequencenumber*/
44
45w_f:in?nr,rsn;
46 if
47:r:nn==ens->gotS_h;/*correctmessageandseq.num*/
48::rsm==1-esn->gotS_a;/*correctmessage,wrongseq.num*/
49+:atomic(printf(*MSC;MSOper\
^);gotW_f;);
50 ifi;
51
52S_h:
53 assert(mr==me);/*expectedmessagereceived*/
54 delay(rc,dB);/*messageprocessingdelay*/
55 atomic(s==1-esn;me=(me+1)XMAX);
56
57S_a:atomic(delay(rc,dL);out!ACK);/*sendanddelayinchannelZtoS*/
58 atomic(delay(rc,1);gotW_f;);
59}
60
61 init
62{
63 atomic(
64 runSender(RtOS,Stock);
65 runReceiver(StoR,RtOS);
66}
67}
```
Listing 8: DT Promela model of PAR protocol. Processes exchange messages using channels. The Receiver process accepts messages from the Server process through the StoR channel that can store one message with two fields, one for the value (byte) and one for the sequence number (bit). Sequence number is used as the positive acknowledgement that the Server process receives from the Receiver process over the RtoS channel. After unbounded delay the Sender generates next message (line 19). Before message value mt and sequence number sn is sent to the StoR channel, the delay in the channel is modeled with delay of the \(dK\) ticks (line 22). Next, timer sc is set to expire at retransmission period _To_. Sender now waits for the reception of acknowledgment (line 27-33) or expiration of the retransmission period. If any signal is received before timer sc expires, it is decided non-deterministically if positive acknowledgment is received or an error is reported and retransmission of the message and the sequence number is started at the label S_f. If acknowledge is accepted, execution is delayed for one tick and a new sequence number is calculated. Execution continues at the label R_h with the calculation of the new message value. If no signal has been received until retransmission period _To_ (timer sc has expired), the execution continues at label S_f with the retransmission of the signal. At the Receiver process, the received sequence number \(rsn\) is compared to the expected sequence number \(esn\) (lines 45-50). If they match, received message value \(rm\) is compared to the expected message value \(em\). For this, an assert statement is used (line 53). Violation of this safety property would be reported during the verification and simulation run. Next, execution is delayed for message execution processing delay \(dR\). It is followed with the calculation of the next expected sequence number and message value. After the delay of \(dL\) ticks in the channel RtoS, acknowledgment is sent to the Sender. Now, the Receiver process is ready to receive the next signal after the delay of one tick.